-
the mizar mathematical library in omdoc: translation and applications
جزئیات بیشتر مقاله- تاریخ ارائه: 1392/07/24
- تاریخ انتشار در تی پی بین: 1392/07/24
- تعداد بازدید: 803
- تعداد پرسش و پاسخ ها: 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.
مقالات جدیدترین رویدادها
-
استفاده از تحلیل اهمیت-عملکرد در ارائه الگوی مدیریت خلاقیت سازمانی و ارائه راهکار جهت بهبود
-
بررسی تاثیر ارزش وجوه نقد مازاد بر ساختار سرمایه شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر سطح افشای ریسک بر قرارداد بدهی شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر رتبه بندی اعتباری مبتنی بر مدل امتیاز بازار نوظهور بر نقد شوندگی سهام با تأکید بر خصوصی سازی شرکت ها
-
تأثیر آمیخته بازاریابی پوشاک ایرانی بر تصویر ذهنی مشتری پوشاک ایرانی (هاکوپیان)
-
مطالعه تأثیر کارایی مالیاتی بر هزینه بدهی
-
مدیریت دانش، ویژگی ها، اصول، موانع
-
مرور نظامند کیفی مداخلات زوج درمانی شناختی-رفتاری بر ابعاد زندگی زناشویی در ایران (از سال های 1384 تا 1399)
-
حیات در حیاط (نقش آب در خانه های سنتی حاشیه کویر ایران)
-
strains at the myotendinous junction predicted by a micromechanical model
مقالات جدیدترین ژورنال ها
-
مدیریت و بررسی افسردگی دانش آموزان دختر مقطع متوسطه دوم در دروان کرونا در شهرستان دزفول
-
مدیریت و بررسی خرد سیاسی در اندیشه ی فردوسی در ادب ایران
-
واکاوی و مدیریت توصیفی قلمدان(جاکلیدی)ضریح در موزه آستان قدس رضوی
-
بررسی تاثیر خلاقیت، دانش و انگیزه کارکنان بر پیشنهادات نوآورانه کارکنان ( مورد مطالعه: هتل های 3 و 4 ستاره استان کرمان)
-
بررسی تاثیر کیفیت سیستم های اطلاعاتی بر تصمیم گیری موفق در شرکتهای تولیدی استان اصفهان (مورد مطالعه: مدیران شرکتهای تولیدی استان اصفهان)
-
تعیین موانع نوآوری باز در حوزه صنایع غذایی با استفاده از تکنیک تحلیل محتوا
-
ارزیابی اثر شالوده شیب دار و پله ای بر پایداری و ظرفیت فروریزش سازه های احداث شده بر روی شیروانی
-
هنر جرم انگاری
-
behavior of precast prestressed concrete segmental beams
-
the rise of crime in affordable housing in suburbs, case of iran
سوال خود را در مورد این مقاله مطرح نمایید :