- Proper disambiguation of overloaded mathematical symbols. Overloading is necessary in a large body of mathematics including all kinds of subfields, but at the same time makes it difficult for readers of the textual versions of the articles to understand the precise meaning of the overloaded symbols.

- Explicit access to formulae for definition correctness, and formulae expressing properties (projectivity, antisymmetry, etc.) that are computed by the verifier. Making these explicit in the HTML presentation can help users.

- Explicit representation of other features that are implicit in Mizar verification, e.g., definitional expansions, original versions of constructors that have been redefined, etc. Making these explicit in the HTML presentation can also help users.

The static HTMLized MML is an important resource used by MizAR. The articles submitted to MizAR are dynamically linked to the static HTMLized MML. This is a notable difference to SystemOnTPTP, which treats each problem as an independent entity. The first implementation of MizAR has focused on developing the services for a fixed version of the MML. However, management of library versions is a nontrivial and interesting problem. Allowing users to verify new articles and also refactor existing ones will ultimately lead into the area of formal mathematical wikis [6, 5].

The main functions of the HTMLization service are to (i) provide quick linking to the static HTMLized MML (thus providing the disambiguation and explanation functions described above), and (ii) allow a number of additional
(mainly automated reasoning and AI) services to be launched by suitable CGI
and AJAX calls from links in the HTML. These additional services are described in the following subsections. The main features of server-side HTMLization are increased speed, and the availability of additional programs and features. While the Mizar HTML processing was designed to be locally available, using just a browser-based XSL processor (i.e., loading the XML produced by Mizar directly into a browser, which applies the appropriate style sheet), even the basic XSL processing in the browser can take a long time (minutes). Again, having a specialized fast XSL processor installed on the server helps quite a lot, and the HTMLization can be parallelized using techniques similar to the parallelization of the basic verification process. This provides a much better HTMLization response, and also makes additional XSL-based preprocessing possible. This is needed for better HTML quality, and for the translation to ATP formats.

## 3.3 Generation Of Atp Problems In Tptp Format

One of the main objectives of MizAR (as suggested by its name) is to allow easy experimentation with ATP systems over the large body of formal mathematics available in the MML, and to apply ATP functionalities on Mizar articles.

The MPTP system [32, 31] for translating Mizar articles to the TPTP format has been modified to work in a fast real-time mode, generating ATP problems corresponding to Mizar proof obligations. The MPTP system translates Mizar articles to the MPTP format, which is an extension of the TPTP format with