×

Theorem proving in large formal mathematics as an emerging AI field. (English) Zbl 1276.68139

Bonacina, Maria Paola (ed.) et al., Automated reasoning and mathematics. Essays in memory of William W. McCune. Berlin: Springer (ISBN 978-3-642-36674-1/pbk). Lecture Notes in Computer Science 7788. Lecture Notes in Artificial Intelligence, 240-257 (2013).
The idea to combine machine learning techniques and automated theorem proving goes back at least to the 1970s. A main approach then was (and still is today) to select automatically a miminal set of premises for a theorem from a database. However, at that time there were problems which made it hard to make such a combination a success; most importantly theorem provers were much weaker and large databases were not available. The authors describe that this has changed considerably and that there are several benefits to be expected from such an approach using machine learning techniques.
To this end many experiments were carried through and described by Urban with varying coauthors. These build on the Mizar Mathematical Library, since it offers a very big collection of mathematical theorems and proofs. The authors relate their work to the QED manifesto, and the earlier work done by Quaife on such a formalization twenty years ago.
There are several advantages of applying machine learning techniques to theorem proving systems, they test theorem provers and can enhance their power. As the authors say, more importantly they offer an excellent field for testing and evaluating machine learning techniques, since there is an objective measure of success: Can the theorem prover prove the theorem with the selected premises or not?
The authors also discuss possible extensions by providing more information for a successful proof attempt, and the basis for a large scale QED project.
For the entire collection see [Zbl 1259.68002].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] The QED Manifesto. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 238–251. Springer, Heidelberg (1994)
[2] Alama, J., Kühlwein, D., Tsivtsivadze, E., Urban, J., Heskes, T.: Premise selection for mathematics by corpus analysis and kernel methods. CoRR, abs/1108.3446 (2011) · Zbl 1315.68217
[3] Alama, J., Kühlwein, D., Urban, J.: Automated and Human Proofs in General Mathematics: An Initial Comparison. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18. LNCS, vol. 7180, pp. 37–45. Springer, Heidelberg (2012) · Zbl 1352.68211 · doi:10.1007/978-3-642-28717-6_6
[4] Althaus, E., Kruglov, E., Weidenbach, C.: Superposition Modulo Linear Arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 84–99. Springer, Heidelberg (2009) · Zbl 1193.03024 · doi:10.1007/978-3-642-04222-5_5
[5] Bancerek, G., Endou, N., Sakai, Y.: On the characterizations of compactness. Formalized Mathematics 9(4), 733–738 (2001)
[6] Benzmüller, C.E., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162–170. Springer, Heidelberg (2008) · Zbl 1165.68446 · doi:10.1007/978-3-540-71070-7_14
[7] Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004) · doi:10.1007/978-3-662-07964-5
[8] Bonacina, M.P., Lynch, C., de Moura, L.M.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reasoning 47(2), 161–189 (2011) · Zbl 1243.68265 · doi:10.1007/s10817-010-9213-y
[9] Brown, C.E.: Satallax: An Automatic Higher-Order Prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 111–117. Springer, Heidelberg (2012) · Zbl 1358.68250 · doi:10.1007/978-3-642-31365-3_11
[10] Carlson, A., Cumby, C., Rosen, J., Roth, D.: SNoW User’s Guide. Technical Report UIUC-DCS-R-99-210, University of Illinois at Urbana-Champaign (1999)
[11] Claessen, K., Sorensson, N.: New Techniques that Improve MACE-style Finite Model Finding. In: Baumgartner, P., Fermueller, C. (eds.) Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (2003)
[12] Dahn, I., Wernhard, C.: First order proof problems extracted from an article in the MIZAR Mathematical Library. In: Bonacina, M.P., Furbach, U. (eds.) Int. Workshop on First-Order Theorem Proving (FTP 1997). RISC-Linz Report Series No. 97-50, vol. (97-50), pp. 58–62. Johannes Kepler Universität, Linz, Austria (1997)
[13] Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a nutshell. Journal of Formalized Reasoning 3(2), 153–245 (2010) · Zbl 1211.68369
[14] Hähnle, R., Kerber, M., Weidenbach, C.: Common Syntax of the DFG-Schwerpunktprogramm Deduction. Technical Report TR 10/96, Fakultät für Informatik, Universät Karlsruhe, Karlsruhe, Germany (1996)
[15] Hales, T.C.: Introduction to the Flyspeck project. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, vol. 05021, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany (2005)
[16] Harrison, J.: HOL Light: A Tutorial Introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996) · doi:10.1007/BFb0031814
[17] Jaskowski, S.: On the rules of suppositions. Studia Logica, 1 (1934) · Zbl 0011.09702
[18] Korovin, K., Voronkov, A.: Integrating Linear Arithmetic into Superposition Calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 223–237. Springer, Heidelberg (2007) · Zbl 1179.03018 · doi:10.1007/978-3-540-74915-8_19
[19] Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mechanized Mathematics and Its Applications 4, 3–24 (2005)
[20] McCune, W.W.: LADR: Library of Automated Deduction Routines, http://www.mcs.anl.gov/AR/ladr
[21] McCune, W.W.: Mace4 Reference Manual and Guide. Technical Report ANL/MCS-TM-264, Argonne National Laboratory, Argonne, USA (2003)
[22] McCune, W.W.: Otter 3.3 Reference Manual. Technical Report ANL/MSC-TM-263, Argonne National Laboratory, Argonne, USA (2003)
[23] Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic 7(1), 41–57 (2009) · Zbl 1183.68560 · doi:10.1016/j.jal.2007.07.004
[24] Niles, I., Pease, A.: Towards a standard upper ontology. In: FOIS 2001: Proceedings of the International Conference on Formal Ontology in Information Systems, pp. 2–9. ACM Press, New York (2001) · doi:10.1145/505168.505170
[25] Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002) · Zbl 0994.68131 · doi:10.1007/3-540-45949-9
[26] Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning, vol. I, pp. 335–367. Elsevier and MIT Press (2001) · Zbl 0992.03018 · doi:10.1016/B978-044450813-3/50008-4
[27] Otten, J., Bibel, W.: leanCoP: Lean Connection-Based Theorem Proving. Journal of Symbolic Computation 36(1-2), 139–161 (2003) · Zbl 1025.68076 · doi:10.1016/S0747-7171(03)00037-3
[28] Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) ESCoR 2006. CEUR, vol. 192, pp. 18–33 (2006)
[29] Quaife, A.: Automated Deduction in von Neumann-Bernays-Godel Set Theory. Journal of Automated Reasoning 8(1), 91–147 (1992) · Zbl 0768.03005 · doi:10.1007/BF00263451
[30] Quaife, A.: Automated Development of Fundamental Mathematical Theories. Kluwer Academic Publishers (1992) · Zbl 0773.03010
[31] Ramachandran, D., Reagan, P., Goolsbey, K.: First-orderized ResearchCyc: Expressiveness and Efficiency in a Common Sense Knowledge Base. In: Shvaiko, P. (ed.) Proceedings of the Workshop on Contexts and Ontologies: Theory, Practice and Applications (2005)
[32] Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications 15(2-3), 91–110 (2002) · Zbl 1021.68082
[33] Schulz, S.: E: A Brainiac Theorem Prover. AI Communications 15(2-3), 111–126 (2002)
[34] Sutcliffe, G.: Semantic Derivation Verification. International Journal on Artificial Intelligence Tools 15(6), 1053–1070 (2006) · Zbl 05421690 · doi:10.1142/S0218213006003119
[35] Sutcliffe, G., Puzis, Y.: SRASS - A Semantic Relevance Axiom Selection System. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 295–310. Springer, Heidelberg (2007) · Zbl 1213.68575 · doi:10.1007/978-3-540-73595-3_20
[36] Sutcliffe, G.: The 4th IJCAR automated theorem proving system competition - CASC-J4. AI Commun. 22(1), 59–72 (2009)
[37] Sutcliffe, G.: The TPTP World – Infrastructure for Automated Reasoning. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 1–12. Springer, Heidelberg (2010) · Zbl 1253.68292 · doi:10.1007/978-3-642-17511-4_1
[38] Urban, J.: Translating Mizar for First Order Theorem Provers. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 203–215. Springer, Heidelberg (2003) · Zbl 1022.68622 · doi:10.1007/3-540-36469-2_16
[39] Urban, J.: MPTP - Motivation, Implementation, First Experiments. Journal of Automated Reasoning 33(3-4), 319–339 (2004) · Zbl 1075.68081 · doi:10.1007/s10817-004-6245-1
[40] Urban, J.: XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, pp. 346–360. Springer, Heidelberg (2006) · Zbl 1151.68681 · doi:10.1007/11618027_23
[41] Urban, J.: MaLARea: a Metasystem for Automated Reasoning in Large Theories. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, pp. 45–58 (2007)
[42] Urban, J.: MPTP 0.2: Design, Implementation, and Initial Experiments. Journal of Automated Reasoning 37(1-2), 21–43 (2007) · Zbl 1113.68095 · doi:10.1007/s10817-006-9032-3
[43] Urban, J., Sutcliffe, G.: ATP Cross-Verification of the Mizar MPTP Challenge Problems. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 546–560. Springer, Heidelberg (2007) · Zbl 1137.68576 · doi:10.1007/978-3-540-75560-9_39
[44] Urban, J., Trac, S., Sutcliffe, G., Puzis, Y.: Combining Mizar and TPTP Semantic Presentation Tools. In: Proceedings of the Mathematical User-Interfaces Workshop 2007 (2007)
[45] Urban, J.: An overview of methods for large-theory automated theorem proving (invited paper). In: Höfner, A., McIver, G. (eds.) ATE Workshop. CEUR Workshop Proceedings, vol. 760, pp. 3–8. CEUR-WS.org (2011)
[46] Urban, J., Alama, J., Rudnicki, P., Geuvers, H.: A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol. 6167, pp. 455–469. Springer, Heidelberg (2010) · Zbl 1286.68434 · doi:10.1007/978-3-642-14128-7_38
[47] Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and Presentation Service for Mizar Formalizations. J. Autom. Reasoning 50(2), 229–241 (2013) · Zbl 1260.68380 · doi:10.1007/s10817-012-9269-y
[48] Urban, J., Sutcliffe, G., Pudlák, P., Vyskočil, J.: MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 441–456. Springer, Heidelberg (2008) · Zbl 1165.68434 · doi:10.1007/978-3-540-71070-7_37
[49] Urban, J., Vyskočil, J., Štěpánek, P.: MaLeCoP Machine Learning Connection Prover. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 263–277. Springer, Heidelberg (2011) · Zbl 1332.68206 · doi:10.1007/978-3-642-22119-4_21
[50] Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009) · Zbl 05587933 · doi:10.1007/978-3-642-02959-2_10
[51] Wiedijk, F.: CHECKER - notes on the basic inference step in Mizar (2000), 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.