Mechanical Theorem Proving in Tarski’s Geometry
From MaRDI portal
Publication:5453489
Recommendations
Cites work
- scientific article; zbMATH DE number 3151263 (Why is no real title available?)
- scientific article; zbMATH DE number 3899653 (Why is no real title available?)
- scientific article; zbMATH DE number 1745043 (Why is no real title available?)
- scientific article; zbMATH DE number 1863395 (Why is no real title available?)
- scientific article; zbMATH DE number 3068536 (Why is no real title available?)
- A graphical user interface for formal proofs in geometry
- Automated Deduction in Geometry
- Automated development of Tarski's geometry
- Design and formal proof of a new optimal image segmentation program with hypermaps
- Formalizing Hilbert's Grundlagen in Isabelle/Isar
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Machine Proofs in Geometry
- Tarski's System of Geometry
- The axioms of constructive geometry
Cited in
(32)- Formalization of Wu's simple method in Coq
- A graphical user interface for formal proofs in geometry
- scientific article; zbMATH DE number 3926284 (Why is no real title available?)
- Tarski geometry axioms. V: Half-planes and planes
- Formalization of the Poincaré disc model of hyperbolic geometry
- Tarski geometry axioms
- Automated development of Tarski's geometry
- Tarski geometry axioms. III
- A synthetic proof of Pappus' theorem in Tarski's geometry
- Finding proofs in Tarskian geometry
- 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 coherent logic based geometry theorem prover capable of producing formal and readable proofs
- Implementing Euclid's straightedge and compass constructions in type theory
- Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method
- OTTER proofs in Tarskian geometry
- Tarski geometry axioms. IV: Right angle
- From informal to formal proofs in Euclidean geometry
- Two cryptomorphic formalizations of projective incidence geometry
- scientific article; zbMATH DE number 2155188 (Why is no real title available?)
- Formalization of the arithmetization of Euclidean plane geometry and applications
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- Formalizing complex plane geometry
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- From Tarski to Hilbert
- Tarski geometry axioms. II
- Formalizing Hilbert's Grundlagen in Isabelle/Isar
- Towards a certified version of the encyclopedia of triangle centers
- Towards an intelligent and dynamic geometry book
- scientific article; zbMATH DE number 1745043 (Why is no real title available?)
- Proof-checking Euclid
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)
