Proof-checking Euclid

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

zbMATH Keywords

Euclidean geometryCoqEuclidproof-checkingHOL light

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Euclidean geometries (general) and generalizations (51M05)

Related Items

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 ⋮ Theorem proving as constraint solving with coherent logic

Uses Software

• Coq
• HOL Light
• GeoCoq

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