well together. This is important for supporting existing users and attracting new users of Mizar, by providing them with an attractive environment for exploring the world of formal reasoning in mathematics. Fast server-based solutions make systems easy to use, to the extent of just "pushing a button" (clicking on a HTML link), rather than having to go through the pains of building an adequate local hardware and software installation, for benefits that might initially not be clear. Server-based solutions are becoming an important part of general computer use, and formal mathematics is no exception. It is not possible to name all the server-based services that already exist for informal mathematics, starting e.g., from the arXiv, Wikipedia, MathOverflow, PolyMath, Wolfram MathWorld, PlanetMath, ProofWiki, the SAGE system for working with CASes, etc.

This paper describes the *Automated Reasoning for Mizar* (MizAR) web service, which combines several automated reasoning and proof presentation tools with the Mizar system for formalization of mathematics, to form a useful mathematical service. MizAR runs in the context of the Mizar Mathematical Library
(MML), and uses the Mizar language that is oriented towards human mathematicians. The main inspiration for MizAR is the SystemOnTPTP ATP service [22].

SystemOnTPTP allows users to easily experiment with many first-order ATP systems in a common framework, and provides additional services such as proof presentation with the IDV system [28], discovery of interesting lemmas with the AGInT system [18], and independent proof verification with the GDV verifier
[23]. Pieces of the SystemOnTPTP infrastructure also served in the initial implementation of the MizAR web service. SystemOnTPTP's infrastructure is briefly described in Section 2. Section 3 describes the implemented MizAR service, and demonstrates its use. Section 4 considers a number of possible future extensions, and concludes.

## 2 Systemontptp

The core of SystemOnTPTP is a utility that allows an ATP problem or solution to be easily and quickly submitted in various ways to a range of ATP systems and tools. SystemOnTPTP uses a suite of currently available systems and tools, whose properties (input format, reporting of result status, etc) are stored in a simple text database. The input can be selected from the TPTP (Thousands of Problems for Theorem Provers) problem library or the TSTP (Thousands of Solutions from Theorem Provers) solution library [24], or provided in TPTP format [25] by the user. The implementation relies on several subsidiary tools to preprocess the input, control the execution of the chosen ATP system(s), and postprocess the output. On the input side TPTP2X or TPTP4X is used to prepare the input for processing. A strict resource limiting program called TreeLimitedRun is used to limit the CPU time and memory used by an ATP
system or tool. TreeLimitedRun monitors processes' resource usage more tightly than is possible with standard operating system calls. Finally a program called X2tptp converts an ATP system's output to TPTP format, if requested by the user.