From informal to formal proofs in Euclidean geometry. (English) Zbl 07055778

Stojanović-Ðurđević, Sana

Ann. Math. Artif. Intell. 85, No. 2-4, 89-117 (2019).

Summary: In this paper, we propose a new approach for automated verification of informal proofs in Euclidean geometry using a fragment of first-order logic called coherent logic and a corresponding proof representation. We use a TPTP inspired language to write a semi-formal proof of a theorem, that fairly accurately depicts a proof that can be found in mathematical textbooks. The semi-formal proof is verified by generating more detailed proof objects expressed in the coherent logic vernacular. Those proof objects can be easily transformed to Isabelle and Coq proof objects, and also in natural language proofs written in English and Serbian. This approach is tested on two sets of theorem proofs using classical axiomatic system for Euclidean geometry created by David Hilbert, and a modern axiomatic system \(E\) created by Jeremy Avigad, Edward Dean, and John Mumma.

MSC:

03B35	Mechanization of proofs and logical operations
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)

Keywords:

informal proofs; coherent logic; Euclidean geometry; interactive theorem proving; automated theorem proving

Software:

Isabelle/HOL; SPASS; TPTP; z3; miz3; Isar; Coq; E Theorem Prover; ArgoCLP; Sledgehammer; HOL Light; Flyspeck; GCLC; VAMPIRE

References:

[1]	Avigad, J.: Understanding proofs. In: Mancosu, P. (ed.) The Philosophy of Mathematical Practice. Oxford University Press, Oxford (2008)
[2]	Avigad, J., Dean, E., Mumma, J.: A formal system for Euclid’s elements. The Review of Symbolic Logic (2009) · Zbl 1188.03008
[3]	Beeson, M., Narboux, J., Wiedijk, F.: Proof-checking Euclid. CoRR (2017). arXiv:1710.00787
[4]	Bezem, M., Coquand, T.: Automating coherent logic. In: Sutcliffe, G., Voronkov, A. (eds.) 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning — LPAR 2005, Lecture Notes in Computer Science, vol. 3835. Springer (2005) · Zbl 1143.03332
[5]	Bezem, M., Hendriks, D.: On the mechanization of the proof of Hessenberg’s theorem in coherent logic. J. Autom. Reas., 40(1) (2008) · Zbl 1140.03004
[6]	Blanchette, J.C.: Automatic Proofs and Refutations for Higher-Order Logic. Ph.D. thesis. Department of Informatics, Technische Universität München (2012)
[7]	Blanchette, J.C.: Redirecting proofs by contradiction. In: Blanchette, J.C., Urban, J. (eds.) Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013, EPiC Series, vol. 14, pp 11-26. EasyChair (2013)
[8]	Blanchette, JC; Böhme, S.; Paulson, LC, Extending sledgehammer with SMT solvers, J. Autom. Reason., 51, 109-128, (2013) · Zbl 1314.68272
[9]	Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) Frontiers of Combining Systems, 8th International Symposium, Proceedings, Lecture Notes in Computer Science, vol. 6989, pp 12-27. Springer (2011) · Zbl 1348.68214
[10]	Braun, G., Narboux, J.: From Tarski to Hilbert. In: Ida, T., Fleuriot, J. (eds.) Automated Deduction in Geometry 2012. http://hal.inria.fr/hal-00727117, Edinburgh (2012)
[11]	Braun, G., Narboux, J.: A synthetic proof of Pappus’ theorem in Tarski’s geometry. J. Autom. Reason., 1-22 (2016) · Zbl 1405.03034
[12]	Dehlinger, C., Dufourd, J.F., Schreck, P.: Higher-order intuitionistic formalization and proofs in Hilbert’s elementary geometry. In: Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 2061. Springer (2001) · Zbl 0985.68078
[13]	Despotović, R., Tošić, R., Šešelja, B.: Matematika za I razred srednje škole. Zavod za udžbenike i nastavna sredstva, Beograd (2000)
[14]	Ekici, B., Katz, G., Keller, C., Mebsout, A., Reynolds, A.J., Tinelli, C.: Extending smtcoq, a certified checker for smt (extended abstract). In: Blanchette, J.C., Kaliszyk, C. (eds.) Proceedings First International Workshop on Hammers for Type Theories, Coimbra, Portugal, July 1, 2016, Electronic Proceedings in Theoretical Computer Science, vol. 210, pp 21-29. Open Publishing Association (2016)
[15]	Euclid: The Thirteen Books of the Elements, 2nd edn. Dover Publications, New York (1956). Translated with introduction and commentary by Sir Thomas L. Heath, from the text of Heiberg · Zbl 0071.24203
[16]	Fisher, J., Bezem, M.: Skolem machines and geometric logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) 4th International Colloquium on Theoretical Aspects of Computing — ICTAC 2007, Lecture Notes in Computer Science, vol. 4711. Springer (2007) · Zbl 1147.68696
[17]	Ganesalingam, M., Gowers, W.T.: A fully automatic theorem prover with human-style output. J. Autom. Reas., 1-39 (2016). https://doi.org/10.1007/s10817-016-9377-1 · Zbl 1405.03035
[18]	Gonthier, G.; Asperti, A.; Avigad, J.; Bertot, Y.; Cohen, C.; Garillot, F.; Le Roux, S.; Mahboubi, A.; O’Connor, R.; Ould Biha, S.; Pasca, I.; Rideau, L.; Solovyev, A.; Tassi, E.; Théry, L.; Blazy, S. (ed.); Paulin, C. (ed.); Pichardie, D. (ed.), A machine-checked proof of the odd order theorem, 163-179, (2013), Rennes · Zbl 1317.68211
[19]	Hales, T.C.: Introduction to the Flyspeck Project, Mathematics, Algorithms, Proofs, Dagstuhl Seminar Proceedings, vol. 05021. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany (2006)
[20]	Harrison, J.: HOL light: A tutorial introduction. In: Srivas, M.K., Camilleri, A.J. (eds.) Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science, vol. 1166. Springer (1996)
[21]	Hilbert, D.: Foundations of Geometry. Open Court Classics, 10th edn (1971)
[22]	Janicić, P.: GCLC - A tool for constructive Euclidean geometry and more than that. In: Takayama, N., Iglesias, A., Gutierrez, J. (eds.) Proceedings of International Congress of Mathematical Software (ICMS 2006), Lecture Notes in Computer Science, vol. 4151, pp 58-73. Springer (2006) · Zbl 1230.51024
[23]	Kaliszyk, C., Krauss, A.: Scalable LCF-style proof translation. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7998, pp 51-66. Springer (2013) · Zbl 1317.68214
[24]	Kaliszyk, C.; Urban, J., Mizar 40 for mizar 40, J. Autom. Reason., 55, 245-256, (2015) · Zbl 1356.68191
[25]	Kaliszyk, C., Urban, J., Vyskočil, J: Learning to Parse on Aligned Corpora (Rough Diamond), pp 227-233. Springer International Publishing, Cham (2015) · Zbl 1465.68287
[26]	Kaliszyk, C., Urban, J., Vyskočil, J.: Automating Formalization by Statistical and Semantic Parsing of Mathematics, pp 12-27. Springer International Publishing, Cham (2017) · Zbl 1483.68490
[27]	Kaliszyk, C., Urban, J., Vyskočil, J., Geuvers, H.: Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description, pp 435-439. Springer International Publishing, Cham (2014) · Zbl 1304.68172
[28]	Kinyon, M., Veroff, R., Vojtěchovský, P: Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction, pp 151-164. Springer, Berlin (2013) · Zbl 1383.68077
[29]	McCune, W., Solution of the robbins problem, J. Autom. Reason., 19, 263-276, (1997) · Zbl 0883.06011
[30]	Meikle, L., Fleuriot, J.: Formalizing Hilbert’s Grundlagen in Isabelle/Isar. In: Proceedings of TPHOLs, Lecture Notes in Computer Science, vol. 2758. Springer (2003) · Zbl 1279.68291
[31]	Meng, J.; Paulson, LC, Translating higher-order clauses to first-order clauses, J. Autom. Reason., 40, 35-60, (2008) · Zbl 1203.68188
[32]	Meng, J.; Quigley, C.; Paulson, LC, Automation for interactive proof: first prototype, Inf. Comput. Special Issue: Comb. Logical Syst., 204, 1575-1596, (2006) · Zbl 1103.68113
[33]	Mitrović, M., Ognjanović, S., Veljković, M., Petković, L., Lazarević, N.: Geometrija za prvi razred Matematičke gimnazije. KRUG Beograd (1998)
[34]	de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver, pp 337-340. Springer, Berlin (2008)
[35]	Narboux, J.: Mechanical theorem proving in Tarski’s geometry. In: Proceedings of Automated Deduction in Geometry 2006, Lecture Notes in Computer Science, vol. 4869. Springer (2007) · Zbl 1195.03019
[36]	Nikoliċ, M., Janičiċ, P.: CDCL-Based Abstract State Transition System for Coherent Logic, pp 264-279. Springer, Berlin (2012) · Zbl 1360.68761
[37]	Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283. Springer (2002) · Zbl 0994.68131
[38]	Northrop, B.: Automated Diagrammatic Reasoning: A proof checker for the language of E. Master’s thesis, Department of Philosophy Carnegie Mellon University (2011)
[39]	Phillips, JD; Stanovský, D., Automated theorem proving in quasigroup and loop theory, AI Commun., 23, 267-283, (2010) · Zbl 1204.68181
[40]	Polonsky, A.: Proofs, Types and Lambda Calculus. Ph.D. thesis, University of Bergen (2011)
[41]	Riazanov, A.; Voronkov, A., The design and implementation of VAMPIRE, AI Commun., 15, 91-110, (2002) · Zbl 1021.68082
[42]	Rojas, K.: EuclidZ3 - a Computational Proof-Checker for the Language E: Possible Backend for Interactive Geometric Proof Environments. Master’s thesis, Department of Philosophy Carnegie Mellon University (2015)
[43]	Schulz, S., E - a brainiac theorem prover, AI Commun., 15, 111-126, (2002) · Zbl 1020.68084
[44]	Schwabhäuser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer, Berlin (1983) · Zbl 0564.51001
[45]	Scott, P.; Fleuriot, J.; Schreck, P. (ed.); Narboux, J. (ed.); Richter-Gebert, J. (ed.), An investigation of Hilbert’s implicit reasoning through proof discovery in idle-time, 182-200, (2011), Berlin · Zbl 1350.68244
[46]	Stojanović, S.: Formalization and automation of Euclidean geometry (in serbian). Ph.D. thesis, University of Belgrade. Advisor: Predrag Janicić (2016)
[47]	Stojanović, S., Narboux, J., Bezem, M., Janičić, P.: A vernacular for coherent logic. In: S.W., other (eds.) Intelligent Computer Mathematics - CICM 2014, Lecture Notes in Computer Science, vol. 8543. Springer (2014)
[48]	Stojanović, S., Pavlović, V., Janicić, P.: A coherent logic based geometry theorem prover capable of producing formal and readable proofs. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 6877. Springer (2011)
[49]	Stojanović, V.: Matematiskop 3 - Odabrani zadaci (sa rešenjima) za učenike srednjih škola. Beograd, Naučna knjiga (1988)
[50]	Stojanović-Ðurđević, S.: Automated verification of informal proofs from high school geometry (in Serbian) InfoM (2016)
[51]	Stojanović-Ðurđević, S., Narboux, J., Janičić, P.: Automated generation of machine verifiable and readable proofs: A case study of Tarski’s geometry. Annals of Mathematics and Artificial Intelligence (2015) · Zbl 1327.68206
[52]	Sutcliffe, G., The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0, J. Autom. Reason., 43, 337-362, (2009) · Zbl 1185.68636
[53]	The Coq development team: The Coq proof assistant reference manual, Version 8.2. TypiCal Project (2009). http://coq.inria.fr
[54]	Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: Spass version 3.5. In: Automated Deduction - CADE-22 Proceedings, Lecture Notes in Computer Science, vol. 5663, pp. 140-145. Springer (2009)
[55]	Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) Theorem Proving in Higher Order Logics (TPHOLs’99), Lecture Notes in Computer Science, vol. 1690, pp 167-184. Springer (1999)
[56]	Wiedijk, F.: A synthesis of the procedural and declarative styles of interactive theorem proving. Logical Methods Comput. Sci., 8(1) (2012) · Zbl 1238.68147