Three stages: normalization, itemization, and minimization.
A further problem is to report the results. The goal is a dependency table that shows, for each Mizar "item", which Mizar items it depends upon.
The ontology of items should be compatible with the standard Mizar ontology of items.
At the end of normalization of an article of the MML, the normalized article has the following properties:
-
There are no reserved variables.
-
All toplevel non-theorem lemmas contain at least one local constant.
In other words, if a toplevel non-theorem lemma could be a theorem, it is rewritten as one.
-
Every definition block defines exactly one functor/predicate/notation, etc.
-
For non-redefinition functor definitions, the existence and uniqueness conditions are justified by a single previous theorem.
A consequence is that if, in the original article, the existence or uniqueness condition is obvious, a "dummy" theorem must be created and cited as the justification.
-
Likewise, all properties of all constructors are justified by a single previous theorem. (This holds even in the case where, in the original article, the existence or uniqueness condition is obvious.)
A consequence is that if, in the original article, the property is obvious, a "dummy" theorem must be created and cited as the justification.
- Distinguish schemes from scheme instances.