Abstract
We describe a number of new possibilities for current theorem provers that arise with the existence of large integral bodies of formalized mathematics. Then we describe the implementation of the MPTP system, which makes the largest existing corpus of formalized mathematics available to theorem provers. MPTP (Mizar Problems for Theorem Proving) is a system for translating the Mizar Mathematical Library (MML) into untyped first-order format suitable for automated theorem provers and for generating theorem-proving problems corresponding to MML. The first version generates about 30,000 problems from complete proofs of Mizar theorems and about 630,000 problems from the simple (one-step) justifications done by the Mizar checker. We describe the design and structure of the system, the main problems encountered in this kind of system, their solutions, current limitations, and planned extensions. We present results of first experiments with re-proving the MPTP problems with theorem provers. We also describe first implementation of the Mizar Proof Advisor (MPA) used for selecting suitable axioms from the large library for an arbitrary problem and, again, present first results of this combined MPA/ATP architecture on MPTP.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Bancerek, G. (2000) Development of the theory of continuous lattices in Mizar, in M. Kerber and M. Kohlhase (eds.), Symbolic Computation and Automated Reasoning, The CALCULEMUS-2000 Symposium, A. K. Peters, Natick, MA, pp. 65–80.
Carlson, A. J., Cumby, C. M., Rosen, J. L. and Roth, D. (1999) SNoW user’s guide, UIUC Tech Report UIUC-DCS-R-99-210.
Dahn, I. and Wernhard, C. (1997) First order proof problems extracted from an article in the MIZAR mathematical library, in Proceedings of the International Workshop on First Order Theorem Proving, RISC-Linz Report Series, No. 97-50, Johannes Kepler Universität Linz.
Dahn, I. (1998) Interpretation of a Mizar-like logic in first order logic, in Proceedings of FTP 1998, pp. 137–151.
Dahn, I. (2001) Slicing book technology – Providing online support for textbooks, in Proc. ICDE 2001, International Conference on Distant Education, Düsseldorf.
Ganzinger, H., Meyer, C. and Weidenbach, C. (1997) Soft typing for ordered resolution, in Proc. CADE-14, Springer, pp. 321–335.
Ganzinger, H. and Stuber, J. (2003) Superposition with equivalence reasoning and delayed clause normal form transformation, in Proc. 19th Int. Conf. on Automated Deduction (CADE-19), Miami, Florida, LNAI 2741, Springer, pp. 335–349.
Hähnle, R., Kerber, M. and Weidenbach, C. (1996) Common syntax of the DFGSchwerpunktprogramm deduction, Technical Report TR 10/96, Fakultät für Informatik, Universität Karlsruhe, Karlsruhe, Germany.
Lenat, D. B. (1979) On automated scientific theory formation: A case study using the AM program, in J. Hayes, D. Michie and L. I. Mikulich (eds.), Machine Intelligence 9, Halstead, New York, 1979, pp. 251–283.
Lenat, D. B. (1982) The nature of heuristics, Artificial Intelligence 19(2) 189–249.
McCune, W. W. (1997) Solution of the Robbins problem, J. Automated Reasoning 19(3), 263–276.
MoMM (2004) The MoMM interreduction system by Josef Urban, available online at http://alioth.uwb.edu.pl/twiki/bin/view/Mizar/MoMM.
MPTPResults.sql – SQL structure of the MPTP result database, published online at http://alioth.uwb.edu.pl/twiki/bin/view/Mizar/MpTP.
Naumowicz, A. and Byliński, C. (2002) Basic elements of computer algebra in MIZAR, Mechanized Mathematics and Its Applications 2(1), 9–16.
Nonnengart, A. and Weidenbach, C. (2001) Computing small clause normal forms, in A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, Vol. 1, Elsevier, Chapter 6, pp. 335–367.
Pollock, J. L. (1996) OSCAR: A general purpose defeasible reasoner, J. Appl. Non-Classical Logics 6, 89–113.
Rudnicki, P. (1992) An overview of the Mizar project, in Proceedings of the 1992 Workshop on Types for Proofs and Programs, Chalmers University of Technology, Bastad.
Schulz, S. (2002) E – A brainiac theorem prover, J. AI Comm. 15, 111–126.
Schulz, S. (2001) Learning search control knowledge for equational theorem proving, in F. Baader, G. Brewka and T. Eiter (eds.), Proceedings of the Joint German/Austrian Conference on Artificial Intelligence (KI-2001), LNAI 2174, Springer, pp. 320–334.
Schumann, J. M. (2001) Automated Theorem-Proving in Software Engineering, Springer-Verlag.
Sutcliffe, G. and Suttner, C. B. (1998) The TPTP problem library: CNF release v1.2.1, J. Automated Reasoning 21(2), 177–203.
Sutcliffe, G., Zimmer, J. and Schulz, S. (2003) Communication formalisms for automated theorem proving tools, in V. Sorge, S. Colton, M. Fisher and J. Gow (eds.), Proceedings of the IJCAI-18 Workshop on Agents and Automated Reasoning, pp. 53–58.
Urban, J. (2003) Translating Mizar for first order theorem provers, in A. Asperti, B. Buchberger and J. Davenport (eds.), Mathematical Knowledge Management, Proceedings of MKM 2003, LNCS 2594.
Urban, J. (2004) MoMM – Fast interreduction and retrieval in large libraries of formalized mathematics, in G. Sutcliffe, S. Schultz and T. Tammit (eds.), Proceedings of the IJCAR 2004 Workshop on Empirically Successful First Order Reasoning, ENTCS, accepted. Available online at http://ktiml.mff.cuni.cz/~urban/MoMM/momm.ps
Weidenbach, C. (2001) SPASS: Combining superposition, sorts and splitting, in A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, Vol. II, Elsevier Science and MIT Press, Chapter 27, pp. 1965–2013.
Wiedijk, F. (2000) CHECKER – Notes on the basic inference step in Mizar, available at http://www.cs.kun.nl/~freek/mizar/by.dvi
Wiedijk, F. (2002) Estimating the cost of a standard library for a mathematical proof checker, http://www.cs.kun.nl/~freek/notes
Wiedijk, F. (2003) Comparing mathematical provers, in A. Asperti, B. Buchberger and J. Davenport (eds.), Mathematical Knowledge Management, Proceedings of MKM 2003, LNCS 2594, pp. 188–202.