Proof-checking Euclid
From MaRDI portal
Publication:2631965
DOI10.1007/S10472-018-9606-XOpenAlexW2762220014MaRDI QIDQ2631965
Michael J. 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
Foundations of classical theories (including reverse mathematics) (03B30) Euclidean geometries (general) and generalizations (51M05)
Related Items (12)
Learning to solve geometric construction problems from images ⋮ From informal to formal proofs in Euclidean geometry ⋮ Euclid after Computer Proof-Checking ⋮ Tarski geometry axioms. IV: Right angle ⋮ On the notion of equal figures in Euclid ⋮ Automated generation of illustrated proofs in geometry and beyond ⋮ 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
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On the inconsistency of Mumma's Eu
- A constructive version of Tarski's geometry
- Proofs, pictures, and Euclid
- An introduction to Wu's method for mechanical theorem proving in geometry
- On the application of Buchberger's algorithm to automated geometry theorem proving
- Proving geometry theorems with rewrite rules
- A refutational approach to geometry theorem proving
- Mechanical theorem proving in geometries. Basic principles. Transl. from the Chinese by Xiaofan Jin and Dongming Wang
- Formalization of the arithmetization of Euclidean plane geometry and applications
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
- Automated development of Tarski's geometry
- 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
- Über die Kreisaxiome
- From Tarski to Hilbert
- Automated Theorem Proving: After 25 Years
- A Declarative Language for the Coq Proof Assistant
- Tarski's System of Geometry
- Machine Proofs in Geometry
- CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE
- A FORMAL SYSTEM FOR EUCLID’SELEMENTS
This page was built for publication: Proof-checking Euclid
