محبوبترین نویسندگان :
نویسندگان مقالات پربازدید :
مجله استدلال خودکار 2013
جزئیات رویداد
همایش ، رویداد ، ژورنال
اینستاگرام تی پی بین

  • the mizar mathematical library in omdoc: translation and applications

    نویسندگان :
    کلمات کلیدی :
    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 799
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     the mizar mathematical library is one of the largest libraries of formalized and mechanically verified mathematics. its language is highly optimized for authoring by humans. as in natural languages, the meaning of an expression is influenced by its (mathematical) context in a way that is natural to humans, but harder to specify for machine manipulation. thus its custom file format can make the access to the library difficult. indeed, the mizar system itself is currently the only system that can fully operate on the mizar library. this paper presents a translation of the mizar library into theomdoc format (open mathematical documents), an xml-based representation format for mathematical knowledge. omdoc is geared towards machine support and interoperability by making formula structure and context dependencies explicit. thus, the mizar library becomes accessible for a wide range of omdoc-based tools for formal mathematics and knowledge management. we exemplify interoperability by indexing the translated library in the mathwebsearch engine, which provides an “applicable theorem search” service (almost) out of the box.

سوال خود را در مورد این مقاله مطرح نمایید :

با انتخاب دکمه ثبت پرسش، موافقت خود را با قوانین انتشار محتوا در وبسایت تی پی بین اعلام می کنم
مقالات جدیدترین رویدادها
مقالات جدیدترین ژورنال ها