×

Mechanical theorem proving in Tarski’s geometry. (English) Zbl 1195.03019

Botana, Francisco (ed.) et al., Automated deduction in geometry. 6th international workshop, ADG 2006, Pontevedra, Spain, August 31–September 2, 2006. Revised papers. Berlin: Springer (ISBN 978-3-540-77355-9/pbk). Lecture Notes in Computer Science 4869. Lecture Notes in Artificial Intelligence, 139-156 (2007).
Summary: This paper describes the mechanization of the proofs of the first eight chapters of W. Schwabhäuser, W. Szmielew and A. Tarski’s book [Metamathematische Methoden in der Geometrie. Berlin: Springer (1983; Zbl 0564.51001)]. The proofs are checked formally using the Coq proof assistant. The goal of this development is to provide foundations for other formalizations of geometry and implementations of decision procedures. We compare the mechanized proofs with the informal proofs. We also compare this piece of formalization with the previous work done about Hilbert’s Grundlagen der Geometrie. We analyze the differences between the two axiom systems from the formalization point of view.
For the entire collection see [Zbl 1132.68006].

MSC:

03B35 Mechanization of proofs and logical operations
51-04 Software, source code, etc. for problems pertaining to geometry
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Citations:

Zbl 0564.51001
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Coq development team, The: The Coq proof assistant reference manual, Version 8.0. LogiCal Project (2004)
[2] Dehlinger, C.; Dufourd, J. F.; Schreck, P.; Richter-Gebert, J.; Wang, D., Higher-order intuitionistic formalization and proofs in Hilbert’s elementary geometry, Automated Deduction in Geometry, 306-324 (2001), Heidelberg: Springer, Heidelberg · Zbl 0985.68078 · doi:10.1007/3-540-45410-1_17
[3] Paulson, L.C.: The Isabelle reference manual (2006)
[4] Meikle, L.; Fleuriot, J.; Basin, D.; Wolff, B., Formalizing Hilbert’s Grundlagen in Isabelle/Isar, Theorem Proving in Higher Order Logics, 319-334 (2003), Heidelberg: Springer, Heidelberg · Zbl 1279.68291 · doi:10.1007/10930755_21
[5] Tarski, A., Givant, S.: Tarski’s system of geometry. The bulletin of Symbolic Logic 5(2) (1999) · Zbl 0932.01031
[6] Schwabhäuser, W.; Szmielew, W.; Tarski, A., Metamathematische Methoden in der Geometrie (1983), Berlin: Springer, Berlin · Zbl 0564.51001
[7] Quaife, A., Automated development of Tarski’s geometry, Journal of Automated Reasoning, 5, 1, 97-118 (1989) · Zbl 0683.68082 · doi:10.1007/BF00245024
[8] Narboux, J.: Toward the use of a proof assistant to teach mathematics. In (ICTMT7). Proceedings of the 7th International Conference on Technology in Mathematics Teaching (2005)
[9] Narboux, J.: A graphical user interface for formal proofs in geometry. The Journal of Automated Reasoning special issue on User Interface for Theorem Proving 39(2) (2007), http://www.informatik.uni-bremen.de/ · Zbl 1131.68094
[10] Guilhot, F., Formalisation en coq et visualisation d’un cours de géométrie pour le lycáe, Revue des Sciences et Technologies de l’Information, Technique et Science Informatiques, Langages applicatifs, 24, 1113-1138 (2005)
[11] Pichardie, D.; Bertot, Y.; Boulton, R. J.; Jackson, P. B., Formalizing convex hulls algorithms, Theorem Proving in Higher Order Logics, 346-361 (2001), Heidelberg: Springer, Heidelberg · Zbl 1005.68557 · doi:10.1007/3-540-44755-5_24
[12] Meikle, L.; Fleuriot, J.; Hong, H.; Wang, D., Mechanical theorem proving in computation geometry, Automated Deduction in Geometry, 1-18 (2006), Heidelberg: Springer, Heidelberg · Zbl 1159.68556 · doi:10.1007/11615798_1
[13] Dufourd, J. F., Design and formal proof of a new optimal image segmentation program with hypermaps, Pattern Recognition (2007), Amsterdam: Elsevier, Amsterdam · Zbl 1118.68725
[14] Narboux, J.; Slind, K.; Bunker, A.; Gopalakrishnan, G. C., A decision procedure for geometry in Coq, Theorem Proving in Higher Order Logics (2004), Heidelberg: Springer, Heidelberg
[15] Narboux, J.: Formalisation et automatisation du raisonnement géométrique en Coq. PhD thesis, Université Paris Sud (September 2006)
[16] Chou, S. C.; Gao, X. S.; Zhang, J. Z., Machine Proofs in Geometry (1994), Singapore: World Scientific, Singapore · Zbl 0941.68503
[17] Tarski, A.: A decision method for elementary algebra and geometry. University of California Press (1951) · Zbl 0044.25102
[18] Tarski, A.: The completeness of elementary algebra and geometry (1967)
[19] Tarski, A.: What is elementary geometry? In: Henkin, L., Tarski, P.S. (eds.) The axiomatic Method, with special reference to Geometry and Physics, Amsterdam, North-Holland, pp. 16-29 (1959) · Zbl 0092.38504
[20] Gupta, H.N.: Contributions to the axiomatic foundations of geometry. PhD thesis, University of California, Berkley (1965)
[21] Huet, G., Kahn, G., Paulin-Mohring, C.: The Coq Proof Assistant - A tutorial - Version 8.0 (April 2004)
[22] Bertot, Y.; Castéran, P., Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science (2004), Heidelberg: Springer, Heidelberg · Zbl 1069.68095
[23] Coquand, T.; Paulin-Mohring, C.; Martin-Löf, P.; Mints, G., Inductively defined types, COLOG-88 (1990), Heidelberg: Springer, Heidelberg
[24] von Plato, J., The axioms of constructive geometry, Annals of Pure and Applied Logic, 76, 169-200 (1995) · Zbl 0836.03034 · doi:10.1016/0168-0072(95)00005-2
[25] Kahn, G.: Constructive geometry according to Jan von Plato. Coq contribution, Coq V5.10 (1995)
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.