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)- scientific article; zbMATH DE number 1745043 (Why is no real title available?)
- Tarski geometry axioms. V: Half-planes and planes
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
- A synthetic proof of Pappus' theorem in Tarski's geometry
- 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
- Proof-checking Euclid
- Formalization of the Poincaré disc model of hyperbolic geometry
- The area method. A recapitulation
- A case study in formalizing projective geometry in Coq: Desargues theorem
- scientific article; zbMATH DE number 3926284 (Why is no real title available?)
- 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
- scientific article; zbMATH DE number 2155188 (Why is no real title available?)
- 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
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)
