2004 | OriginalPaper | Buchkapitel
Improving Mizar Texts with Properties and Requirements
verfasst von : Adam Naumowicz, Czesław Byliński
Erschienen in: Mathematical Knowledge Management
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In this paper we report on the current state of implementation of two features of the Mizar system – properties and requirements. These two mechanisms provide elements of basic computer algebra to strengthen the capabilities of the Mizar checker by automation of some frequently used reasoning steps. This, in turn, allows for a notable reduction of the size of users’ input in some reasonings. As a result, the size of the Mizar library can be reduced, and, at the same time, Mizar articles can become more like informal mathematical papers.