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 proving Euclid's Elements cut-free proofs for theories with geometric rule-schemes formal axiomatic system reasoning on diagrams Tarski'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

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

Cites Work