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

The findvoc, listvoc and constr programs are utilities included in the Mizar distribution. (See section Constructor explanations, for more utilities working on the constructor representation of Mizar formulas.) Corresponding to these three utilities are the following MizarMode commands(1).

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

The Mizar language is overloaded on the symbol level. For example, the sumbol ’+’ can be used for various operations, such as the sum of two real numbers, the sum of two linear tranformations, or the sum of two group elements. Thus, a symbol may have many meanings. Before checking a proof, Mizar disambiguates overloaded symbols and replaces them with so-called constructors.

Unlike symbols, constructors are unambiguous. Thus, in the statement

for V being RealLinearSpace
for a, b being Real
for L being Linear_Combination of V holds a * (b * L) = (a * b) * L

(which is theorem RLVECT_2:70), the symbol ‘*’ clearly has two meanings. On the left hand side of the equation ‘*’ is used as a binary operation between terms of type ‘Real’ and ‘Linear_Combination of V’, where ‘V’ has type ‘RealLinearSpace’. On the left hand side the first occurence of ‘*’ denotes a binary operation between terms of type Real. When checking a proof, Mizar assigns different constructors to these different occurences of ‘*’. (In the example above, there are four occurences of ‘*’ but only two constructors, viz., meanings, are relevant.)

Mizar formulas. Mizar tools such as MML Query See section MML Query, Mizar Proof Advisor See section Mizar Proof Advisor, and MoMM See section MoMM, often work with constructor representation of statements.

4.2 Irrelevant Utilities

By “irrelevant utilities” we mean those Mizar utilities that check for the “relevancy” of some parts of a Mizar article.

Typically, one uses the irrelevant utilities upon finishing a draft of an article to remove unnecesary proof steps, premises, etc. The irrelevant utilities can illustrate how a proof is unnecessarily complicated; they can even show that the conclusion of a proof differs from proposition one intended 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 ratproof from Mizar Mode is discouraged, since ratproof operates on the file being edited. Instead, the suggested alternative to running ratproof is to execute the command mizar-hide-proofs with an empty prefix argument See section Proof checking. This command emulates ratproof without actually executing it. The menu item <Proof checking> <@proof -> proof on buffer> also corresponds to this command.

Similarly, using miz2prel and miz2abs is not recommended. Unlike ratproof, the programs miz2prel and miz2abs are not well supported nor emulated by MizarMode.

This document was generated by Josef Urban on February 20, 2014 using texi2html 1.82.