Semantic browsing of the Mizar mathematical library for authoring Mizar articles

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F04%3A00005580" target="_blank" >RIV/00216208:11320/04:00005580 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Semantic browsing of the Mizar mathematical library for authoring Mizar articles
Original language description
The Mizar system is equipped with a very large library containing tens of thousands of theorems and thousands of definitions, which often use overloaded notation. For efficient authoring of new Mizar articles it is necessary to have good tools for searching and browsing this library. It would be ideal if such tools were simple, intuitive and easy to access. Particularly, they should provide interactive and integrated support during authoring Mizar articles. We describe an approach to this task which uses the extendable MML Query tools to generate a special representation of the Mizar library (MML). This representation, so called Generated Mizar Abstracts, contains human readable form of the MML, completed by additional information which is missing or hidden in regular Mizar abstracts and texts. It also includes semantic information necessary for implementing advanced browsing in the Mizar authoring environment for Emacs (Mizar mode).
Czech name
Integrované sémantické brouzdání matematické knihovny Mizaru pro vytváření článků v Mirazu
Czech description
Popisujeme prístup umožňující interaktivní a integrovanou podporu při vytváření článků v Mizaru. Používá rozšiřitelné MML Query nástroje a Emacs.

Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
BA - General mathematics
OECD FORD branch
—

Publication year
2004
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)