Chapter 8

Registering to the Library

We would like to explain the Mizar library registration process. Let us assume that we wrote a Mizar article and it passed the checker. However, we cannot register it to the Mizar library because it only passed the checker. Before registering, we have a few other things to do.

8.1 Improvement of an Article

8.1.1 Improvement of the Main Section

First, we need to improve an article. To do this, we need the following commands.



RELPREM   Checks unnecessary citations.
 


CHKLAB    Checks unnecessary labels.



INACC     Checks unnecessary lines.



TRIVDEMO  Checks trivial demonstrations.

Such commands are provided. All these commands are used in the following way.

RELPREM TEXTEXAMPLE1.MIZ

If we execute the following after carrying out each command, the error number will be written into an article.

ERRFLAG TEXTEXAMPLE1.MIZ

RELPREM checks to see if irrelevant matters in reasoning are cited after "by". It also checks for the same thing for "then". If certain things are not needed for reasoning, an error will appear.

CHKLAB later on checks for the labels that are not used after labeling.

INACC later checks for the lines that are not used. If an error occurs from this checker and lines are erased, there may be excess citations and labels due to this; therefore, it needs to be checked again from the beginning.

TRIVDEMO checks to see if there are trivial demonstrations. Trivial matters need to be removed.

These check the main section.

8.1.2 Checking the Environment Section

Others check the environment section. To do this, we need the following commands.



IRRVOC   Checks unnecessary vocabulary.



IRRDEF(not a Mizar version 4.09)



         Checks unnecessary definition.
 


IRRTHS   Checks unnecessary theorems.

The method of using these are the same with the checking commands of the main section. For signature, there is no good way of checking; therefore, there is no IRRSIG at this point. Therefore, use signature sparingly from the beginning and start with 0 and gradually include what is needed.

In addition, the order might become important for signature. Therefore, it is better to first phrase the ones that are made earlier by checking the abstract file and placing them in orderly manner.