4. Running Mizar utilities

Here we deescribe how to use Mizar Mode, to run various compiled Mizar utilities provided in the Mizar distribution.

4.1 Simple constructor and vocabulary utilities

These are compiled utilities available in the Mizar distribution. See section 9. Constructor explanations, for more utilities working on the constructor representation of Mizar formulas.

C-c C-f

mizar-findvoc

C-c C-l

mizar-listvoc

C-c C-t

mizar-constr

Command: mizar-findvoc

Find vocabulary for a symbol.

Command: mizar-listvoc

List vocabulary.

Command: mizar-constr

Show required constructors files.
Constructor files needed for Mizar theorems, definitions, schemes or complete articles can be queried.

4.1.1 Constructors and user symbols

Mizar is overloaded on the symbol level, e.g. the sumbol '+' can be used for various operations. Before proof checking takes place, Mizar disambiguates this overloading and replaces the user symbols with unique "constructors".

Constructors are unambiguous and they are used to express the semantics of Mizar formulas, so tools like MML Query, See section 10. MML Query, Mizar Proof Advisor, See section 11. Mizar Proof Advisor, or MoMM, See section 12. MoMM, often work with constructor representation.

4.2 Irrelevant Utilities

By "Irrelevant utilities" we mean all those Mizar utilities, that check for relevancy of some parts of a Mizar article.

Irrelevant utilities are usually highly relevant when you finish your article, and want to remove unnecesary proof steps, premises, etc. Sometimes you can learn this way, that your proofs are unnecessarily complicated, or even that you were proving something else than what you wanted to prove.

C-c C-h

mizar-irrths

C-c TAB

mizar-relinfer

C-c C-o

mizar-trivdemo

C-c C-s

mizar-reliters

C-c C-y

mizar-relprem

C-c C-b

mizar-chklab

C-c C-v

mizar-irrvoc

C-c C-a

mizar-inacc

Command: mizar-irrths

Call Irrelevant Theorems & Schemes Detector on the article.

Command: mizar-relinfer

Call Irrelevant Inferences Detector on the article.

Command: mizar-trivdemo

Call Trivial Proofs Detector on the article.

Command: mizar-reliters

Call Irrelevant Iterative Steps Detector on the article.

Command: mizar-relprem

Call Irrelevant Premises Detector on the article.

Command: mizar-irrvoc

Call Irrelevant vocabulary Detector on the article.

Command: mizar-inacc

Call Inaccessible Items Detector on the article.

Command: mizar-chklab

Call Irrelevant Label Detector on the article.

4.3 Other Utilities

Additionally, the interface to the Mizar scripts miz2prel and miz2abs and the ratproof utility is available from the menu.

Using the ratproof from the Mizar Mode is discouraged, since it operates directly on the edited file. The suggested replacement is the function mizar-hide-proofs, See section 5.1 Proof checking, run with prefix C-u on the whole buffer. This is also available in menu as <Proof checking> <@proof -> proof on buffer>.

This now also holds about using the scripts miz2prel and miz2abs, however they may get better support in the future.