Proof-checking Euclid

DOI10.1007/S10472-018-9606-XMaRDI QIDQ2631965zbMATH OpenOpenAlexFDO

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)

Copyright license Creative Commons Attribution 4.0 International

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)

Recommendations

• Euclid after Computer Proof-Checking
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Automated production of traditional proofs for theorems in Euclidean geometry. I: The Hilbert intersection point theorems
• scientific article; zbMATH DE number 871441
• Mechanical Theorem Proving in Tarski’s Geometry

Cites work

• scientific article; zbMATH DE number 3119278 (Why is no real title available?)
• scientific article; zbMATH DE number 3899653 (Why is no real title available?)
• scientific article; zbMATH DE number 41286 (Why is no real title available?)
• scientific article; zbMATH DE number 3586510 (Why is no real title available?)
• scientific article; zbMATH DE number 1461211 (Why is no real title available?)
• scientific article; zbMATH DE number 6984221 (Why is no real title available?)
• scientific article; zbMATH DE number 5203535 (Why is no real title available?)
• scientific article; zbMATH DE number 3363463 (Why is no real title available?)
• A Declarative Language for the Coq Proof Assistant
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• A constructive version of Tarski's geometry
• A refutational approach to geometry theorem proving
• A synthetic proof of Pappus' theorem in Tarski's geometry
• An introduction to Wu's method for mechanical theorem proving in geometry
• Automated Theorem Proving: After 25 Years
• Automated development of Tarski's geometry
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• Constructive geometry and the parallel postulate
• Euclid and his twentieth century rivals. Diagrams in the logic of Euclidean geometry
• Formalization of the arithmetization of Euclidean plane geometry and applications
• From Tarski to Hilbert
• Machine Proofs in Geometry
• Mechanical theorem proving in geometries. Basic principles. Transl. from the Chinese by Xiaofan Jin and Dongming Wang
• On the application of Buchberger's algorithm to automated geometry theorem proving
• On the inconsistency of Mumma's Eu
• Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
• Proofs, pictures, and Euclid
• Proving geometry theorems with rewrite rules
• Tarski's System of Geometry
• Über die Kreisaxiome

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

Describes a project that uses

Uses Software

• GeoCoq
• HOL Light
• Coq

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)