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

Related Items (21)

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

This page was built for publication: Mechanical Theorem Proving in Tarski’s Geometry