Proof-checking Euclid
From MaRDI portal
Publication:2631965
DOI10.1007/S10472-018-9606-XOpenAlexW2762220014MaRDI QIDQ2631965FDOQ2631965
Authors: Michael Beeson, Julien Narboux, Freek Wiedijk 
Publication date: 16 May 2019
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1710.00787
Recommendations
Foundations of classical theories (including reverse mathematics) (03B30) Euclidean geometries (general) and generalizations (51M05)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Declarative Language for the Coq Proof Assistant
- Title not available (Why is that?)
- Title not available (Why is that?)
- Machine Proofs in Geometry
- A FORMAL SYSTEM FOR EUCLID’SELEMENTS
- On the application of Buchberger's algorithm to automated geometry theorem proving
- From Tarski to Hilbert
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Über die Kreisaxiome
- Euclid and his twentieth century rivals. Diagrams in the logic of Euclidean geometry
- Tarski's System of Geometry
- Proofs, pictures, and Euclid
- An introduction to Wu's method for mechanical theorem proving in geometry
- Proving geometry theorems with rewrite rules
- Mechanical theorem proving in geometries. Basic principles. Transl. from the Chinese by Xiaofan Jin and Dongming Wang
- Automated Theorem Proving: After 25 Years
- On the inconsistency of Mumma's Eu
- A constructive version of Tarski's geometry
- Constructive geometry and the parallel postulate
- A refutational approach to geometry theorem proving
- Automated development of Tarski's geometry
- Formalization of the arithmetization of Euclidean plane geometry and applications
- Title not available (Why is that?)
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- A synthetic proof of Pappus' theorem in Tarski's geometry
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
Cited In (12)
- Euclid after Computer Proof-Checking
- Learning to solve geometric construction problems from images
- From informal to formal proofs in Euclidean geometry
- Automated generation of illustrated proofs in geometry and beyond
- On the notion of equal figures in Euclid
- Newton's experimental proofs
- Sharing proofs with predicative theories through universe-polymorphic elaboration
- Formal ontology and mathematics. A case study on the identity of proofs
- Euclid's fourth postulate: its authenticity and significance for the foundations of Greek mathematics
- Automated generation of illustrations for synthetic geometry proofs
- Theorem proving as constraint solving with coherent logic
- Tarski geometry axioms. IV: Right angle
Uses Software
This page was built for publication: Proof-checking Euclid
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2631965)
