Mechanical Theorem Proving in Tarski’s Geometry
From MaRDI portal
Publication:5453489
DOI10.1007/978-3-540-77356-6_9zbMATH Open1195.03019OpenAlexW2144907233MaRDI QIDQ5453489FDOQ5453489
Authors: 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
Recommendations
Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to geometry (51-04)
Cites Work
- A graphical user interface for formal proofs in geometry
- The axioms of constructive geometry
- Title not available (Why is that?)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Title not available (Why is that?)
- Machine Proofs in Geometry
- Tarski's System of Geometry
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automated Deduction in Geometry
- Formalizing Hilbert's Grundlagen in Isabelle/Isar
- Design and formal proof of a new optimal image segmentation program with hypermaps
- Title not available (Why is that?)
- Automated development of Tarski's geometry
Cited In (31)
- Tarski geometry axioms. V: Half-planes and planes
- A synthetic proof of Pappus' theorem in Tarski's geometry
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- A graphical user interface for formal proofs in geometry
- Tarski geometry axioms. III
- Automated development of Tarski's geometry
- Finding proofs in Tarskian geometry
- OTTER proofs in Tarskian geometry
- Formalization of the Poincaré disc model of hyperbolic geometry
- Title not available (Why is that?)
- The area method. A recapitulation
- A case study in formalizing projective geometry in Coq: Desargues theorem
- Towards a certified version of the encyclopedia of triangle centers
- Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method
- From informal to formal proofs in Euclidean geometry
- Two cryptomorphic formalizations of projective incidence geometry
- Formalization of Wu's simple method in Coq
- Formalization of the arithmetization of Euclidean plane geometry and applications
- Implementing Euclid's straightedge and compass constructions in type theory
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- Formalizing complex plane geometry
- Formalizing Hilbert's Grundlagen in Isabelle/Isar
- Title not available (Why is that?)
- Tarski geometry axioms
- Tarski geometry axioms. II
- Tarski geometry axioms. IV: Right angle
- Towards an intelligent and dynamic geometry book
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- From Tarski to Hilbert
- Title not available (Why is that?)
Uses Software
This page was built for publication: Mechanical Theorem Proving in Tarski’s Geometry
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5453489)
