Integrated semantic browsing of the Mizar Mathematical Library for authoring Mizar articles

Motivation

• Exact browsing of the overloaded Mizar notation
• Presentation of automatically generated Mizar items (definientia)
• Resolving and browsing symbols from the currently wriiten article
• Integration in the authoring user interface

Availability and Installation

• The complete system is about 5 MB big and unpacks to 64 MB.
• It is available at http://merak.pb.bialystok.pl/gab/gab-4.05.838.tar.gz
• eventually this will become a standard part of the Mizar distribution.

Previous and related work

• JFM http://markun.cs.shinshu-u.ac.jp/Mirror/mizar.org/JFM/
• MmlQuery http://merak.pb.bialystok.pl/mmlquery/three.html
• MizarMode

Overview of the implementation

• The customized MMLQuery tools (output filters) used for producing the Generated Mizar Abstracts from MML.
• The Generated Mizar Abstracts, containing a simple and easy-to-parse Emacs-based markup used for locating the Mizar items in them.
• The Emacs parsing and presentation of the Generated Mizar Abstracts, and browsing of the Mizar items in them.
• Additional Emacs support for disambiguating parts of the article currently developed by the author into the Mizar items, which allows immediate precise browsing.

Mizar items

• Detailed classification of Mizar
• http://merak.pb.bialystok.pl/mmlquery/mmlquery.html#Library-item
• http://megrez.mizar.org/mmlquery/description.html
• Multiple items can be created from one language construct - notation, constructor, definition, definiens

The Generated Mizar Abstracts

• Every GAB corresponds to exactly one normal Mizar abstract, and it consists of all Mizar items defined in the original abstract in the same order of appearance.
• Particularly, the parts of normal abstracts that are not Mizar items are not present in GABs. This means that e.g. comments, reservations do not appear here. All variables in all items are fully qualified, while in the original abstracts, it is often necessary to search the reservations for their types.
• The items which are not explicitely written in the original abstract are by default hidden, and only their names are visible, so that the default GAB looked as close as possible to the original abstract. The presentation obviously implements functions for easy changing and customization of the visibility of items.
• All symbols inside terms and formulas presented in GABs are disambiguated and tagged with the appropriate constructor, which allows precise browsing.

Encoding of the Generated Mizar Abstracts

• modified version of the text/enriched MIME Content-type text/mmlquery
• RFC-1896,RFC-1563,RFC-1522 ftp://ftp.rfc-editor.org/in-notes/rfc1523.txt
• light-weight format in comparison with formats like HTML or XML
• generally implemented standard Emacs parser of the text/enriched format

-- JosefUrban - 19 Sep 2004