Det matematiska biblioteket Mizar är ett av de största biblioteken för formaliserad och mekaniskt verifierad matematik. Dess språk är mycket optimerat för författarskap av människor. Liksom i naturliga språk påverkas betydelsen av ett uttryck av dess (matematiska) sammanhang på ett sätt som är naturligt för människor, men svårare att specificera för maskinmanipulering. På så sätt kan dess egna filformat göra det svårt att få tillgång till biblioteket. Själva Mizarsystemet är för närvarande det enda system som kan fungera fullt ut på biblioteket i Mizar. Här presenteras en översättning av Mizarbiblioteket till OMDAC-formatet (Open Mathematical Documents), ett XML-baserat representationsformat för matematisk kunskap. OMDAC är inriktat på maskinstöd och driftskompatibilitet genom att göra formelstruktur och kontextberoenden explicita. Mizarbiblioteket blir därmed tillgängligt för ett brett utbud av OMDoc-baserade verktyg för formell matematik och kunskapshantering. Vi exemplifierar interoperabilitet genom att indexera det översatta biblioteket i MathWebSearch-motorn, som ger en "tillämplig theorem search" tjänst (nästan) ut ur rutan.
Utlåtandet av teorem i hela Mizar Mathematical Library (MML) har exporterats till MMT logiska ramverk REF.
The Mizar Mathematical Library in OMDoc: Translation and Applications
{'venue': 'Journal of Automated Reasoning', 'journal': 'Journal of Automated Reasoning', 'mag_field_of_study': ['Computer Science']}