A FORMAL SYSTEM FOR EUCLID’SELEMENTS

DOI10.1017/S1755020309990098zbMath1188.03008arXiv0810.4315OpenAlexW1990493960MaRDI QIDQ5850985

Jeremy Avigad, Edward T. Dean, John Mumma

Publication date: 21 January 2010

Published in: The Review of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/0810.4315

zbMATH Keywords

automated geometric theorem provingEuclid's Elementscut-free proofs for theories with geometric rule-schemesformal axiomatic systemreasoning on diagramsTarski's ruler-and-compass geometry

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Foundations of classical theories (including reverse mathematics) (03B30) Euclidean geometries (general) and generalizations (51M05) History of Greek and Roman mathematics (01A20)

Related Items (46)

GeoLogic – Graphical Interactive Theorem Prover for Euclidean Geometry ⋮ Automated theorem proving in GeoGebra: current achievements ⋮ From informal to formal proofs in Euclidean geometry ⋮ Implementing Euclid's straightedge and compass constructions in type theory ⋮ Proof-checking Euclid ⋮ Can one design a geometry engine? Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries ⋮ Euclid's common notions and the theory of equivalence ⋮ Operationalism: an interpretation of the philosophy of ancient Greek geometry ⋮ Informal proofs and mathematical rigour ⋮ The twofold role of diagrams in Euclid's plane geometry ⋮ Constructive geometrical reasoning and diagrams ⋮ Human diagrammatic reasoning and seeing-as ⋮ And so on \dots : reasoning with infinite diagrams ⋮ Uses of construction in problems and theorems in Euclid's \textit{Elements} I--VI ⋮ Figures, Formulae, and Functors ⋮ CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE ⋮ Brouwer and Euclid ⋮ Why did Euclid not need the Pasch axiom? ⋮ Three-dimensional affine spatial logics ⋮ The material reasoning of folding paper ⋮ Automated generation of illustrated proofs in geometry and beyond ⋮ Reliability of mathematical inference ⋮ Mathematical formalization and diagrammatic reasoning: the case study of the braid group between 1925 and 1950 ⋮ Logic of imagination. Echoes of Cartesian epistemology in contemporary philosophy of mathematics and beyond ⋮ Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq ⋮ Enthymemathical Proofs and Canonical Proofs in Euclid’s Plane Geometry ⋮ A constructive version of Tarski's geometry ⋮ Open texture and mathematics ⋮ Prolegomena to a cognitive investigation of Euclidean diagrammatic reasoning ⋮ ‘CHASING’ THE DIAGRAM—THE USE OF VISUALIZATIONS IN ALGEBRAIC REASONING ⋮ Inconsistency in mathematics and the mathematics of inconsistency ⋮ Proofs, pictures, and Euclid ⋮ Unnamed Item ⋮ GEOMETRISATION OF FIRST-ORDER LOGIC ⋮ From mathematical axioms to mathematical rules of proof: recent developments in proof analysis ⋮ Carroll's infinite regress and the act of diagramming ⋮ Cognitive artifacts for geometric reasoning ⋮ Constructibility and Geometry ⋮ From Euclidean geometry to knots and nets ⋮ A FORMALIZATION OF KANT’S TRANSCENDENTAL LOGIC ⋮ A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs ⋮ A Vernacular for Coherent Logic ⋮ Theorem proving as constraint solving with coherent logic ⋮ Geometric Rules in Infinitary Logic ⋮ Automated generation of geometric theorems from images of diagrams ⋮ Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry

Uses Software

• Geometer's Sketchpad
• cvc3
• z3
• Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A constructive theory of ordered affine geometry
• Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
• The axioms of constructive geometry
• A graphical user interface for formal proofs in geometry
• Translating higher-order clauses to first-order clauses
• Eudoxos and Dedekind: On the ancient Greek theory of ratios and its relation to modern mathematics
• System Description: Spass Version 3.0
• Cut Elimination in the Presence of Axioms
• Tarski's System of Geometry
• Machine Proofs in Geometry
• Proof Style and Understanding in Mathematics I: Visualization, Unification and Axiom Choice
• Solving open questions and other challenge problems using proof sketches

This page was built for publication: A FORMAL SYSTEM FOR EUCLID’SELEMENTS