MPTP 0.1 – system description. (English) Zbl 1261.68107
Dahn, Ingo (ed.) et al., FTP’2003: 4th international workshop on first-order theorem proving. Proceedings of the workshop (in connection with RDP’03, federated conference on rewriting, deduction and programming), Valencia, Spain, June 12–14, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 86, No. 1, 147-152 (2003).
Summary: 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, allowing generating theorem proving problems corresponding to MML. The first version generates about 30000 problems from complete proofs of Mizar theorems, and about 630000 problems from the simple (one-step) justifications done by the Mizar checker. We describe the design and structure of the system, some limitations, and planned future extensions.
For the entire collection see [Zbl 1109.03302].
For the entire collection see [Zbl 1109.03302].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
References:
| [1] | Ingo Dahn. Interpretation of a Mizar-like Logic in First Order Logic. Proceedings of FTP 1998. pp. 137-151.; Ingo Dahn. Interpretation of a Mizar-like Logic in First Order Logic. Proceedings of FTP 1998. pp. 137-151. · Zbl 0960.03007 |
| [2] | H. Ganzinger, C. Meyer, C. Weidenbach: Soft Typing for Ordered Resolution. In Proc. CADE-14, pp. 321-335, Springer, 1997.; H. Ganzinger, C. Meyer, C. Weidenbach: Soft Typing for Ordered Resolution. In Proc. CADE-14, pp. 321-335, Springer, 1997. · Zbl 1430.68407 |
| [3] | R. Hähnle, M. Kerber, and C. Weidenbach. Common Syntax of the DFGSchwerpunktprogramm Deduction. Technical Report TR 10/96, Fakultät für Informatik, Universät Karlsruhe, Karlsruhe, Germany, 1996.; R. Hähnle, M. Kerber, and C. Weidenbach. Common Syntax of the DFGSchwerpunktprogramm Deduction. Technical Report TR 10/96, Fakultät für Informatik, Universät Karlsruhe, Karlsruhe, Germany, 1996. |
| [4] | MPTPResults.sql - SQL structure of the MPTP result database, published online at http://alioth.uwb.edu.pl/twiki/bin/view/Mizar/MpTP; MPTPResults.sql - SQL structure of the MPTP result database, published online at http://alioth.uwb.edu.pl/twiki/bin/view/Mizar/MpTP |
| [5] | Adam, Naumowicz; Czeslaw, Byliński, Basic Elements of Computer Algebra in MIZAR, Mechanized Mathematics and Its Applications, Vol.2, 1 (August 2002) |
| [6] | Rudnicki P., An Overview of the Mizar Project, Proceedings of the 1992 Workshop on Types for Proofs and Programs, Chalmers University of Technology, Bastad, 1992.; Rudnicki P., An Overview of the Mizar Project, Proceedings of the 1992 Workshop on Types for Proofs and Programs, Chalmers University of Technology, Bastad, 1992. |
| [7] | Schulz S., System abstract: E 0.3. In H. Ganzinger, ed., 16th International Conference on Automated Deduction, CADE-16, Vol. 1632; Schulz S., System abstract: E 0.3. In H. Ganzinger, ed., 16th International Conference on Automated Deduction, CADE-16, Vol. 1632 |
| [8] | C. Suttner and G. Sutcliffe. The TPTP problem library (TPTP v2.2.0). Technical Report 9704, Department of Computer Science, James Cook University, Townsville, Australia, 1998.; C. Suttner and G. Sutcliffe. The TPTP problem library (TPTP v2.2.0). Technical Report 9704, Department of Computer Science, James Cook University, Townsville, Australia, 1998. · Zbl 0910.68197 |
| [9] | Josef Urban. Translating Mizar for First Order Theorem Provers. In Andrea Asperti, Bruno Buchberger, James Davenport (eds.), Mathematical Knowledge Management, Proceedings of MKM 2003, LNCS 2594, 2003.; Josef Urban. Translating Mizar for First Order Theorem Provers. In Andrea Asperti, Bruno Buchberger, James Davenport (eds.), Mathematical Knowledge Management, Proceedings of MKM 2003, LNCS 2594, 2003. · Zbl 1022.68622 |
| [10] | Weidenbach C., Afshordel B., Brahm U., Cohrs C., Engel T., Keen R., Theobalt C. and Topic D., System description: Spass version 1.0.0, in H. Ganzinger, ed., ’16th International Conference on Automated Deduction, CADE-16’, Vol. 1632; Weidenbach C., Afshordel B., Brahm U., Cohrs C., Engel T., Keen R., Theobalt C. and Topic D., System description: Spass version 1.0.0, in H. Ganzinger, ed., ’16th International Conference on Automated Deduction, CADE-16’, Vol. 1632 |
| [11] | Freek Wiedijk. CHECKER - at http://www.cs.kun.nl/ freek/mizar/by.dvi; Freek Wiedijk. CHECKER - at http://www.cs.kun.nl/ freek/mizar/by.dvi |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
