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

Narboux, Julien

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)

Software:

Coq; GeoCoq; GeoProof; Isabelle; Isabelle/Isar