Mechanical Theorem Proving in Tarski’s Geometry

DOI10.1007/978-3-540-77356-6_9zbMath1195.03019OpenAlexW2144907233MaRDI QIDQ5453489

Julien Narboux

Publication date: 1 April 2008

Published in: Automated Deduction in Geometry (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00118812/file/adg06-narboux.pdf

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to geometry (51-04)

Related Items

A synthetic proof of Pappus' theorem in Tarski's geometry, Towards a certified version of the encyclopedia of triangle centers, From informal to formal proofs in Euclidean geometry, Implementing Euclid's straightedge and compass constructions in type theory, Two cryptomorphic formalizations of projective incidence geometry, Formalization of the arithmetization of Euclidean plane geometry and applications, Tarski geometry axioms. IV: Right angle, Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method, Towards an intelligent and dynamic geometry book, The area method. A recapitulation, A case study in formalizing projective geometry in Coq: Desargues theorem, Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq, A graphical user interface for formal proofs in geometry, Tarski geometry axioms. II, Tarski geometry axioms, Formalization of the Poincaré disc model of hyperbolic geometry, Tarski geometry axioms. III, A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs, Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL, Formalizing complex plane geometry, Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry

Uses Software

• Coq
• Isabelle
• Isabelle/Isar
• GeoProof
• GeoCoq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Automated development of Tarski's geometry
• The axioms of constructive geometry
• A graphical user interface for formal proofs in geometry
• Design and formal proof of a new optimal image segmentation program with hypermaps
• Formalizing Hilbert’s Grundlagen in Isabelle/Isar
• Tarski's System of Geometry
• Machine Proofs in Geometry
• Automated Deduction in Geometry