A FORMAL SYSTEM FOR EUCLID’SELEMENTS
DOI10.1017/S1755020309990098zbMATH Open1188.03008arXiv0810.4315OpenAlexW1990493960MaRDI QIDQ5850985FDOQ5850985
Authors: 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
Recommendations
automated geometric theorem provingEuclid's Elementscut-free proofs for theories with geometric rule-schemesformal axiomatic systemreasoning on diagramsTarski's ruler-and-compass geometry
History of Greek and Roman mathematics (01A20) Cut-elimination and normal-form theorems (03F05) Foundations of classical theories (including reverse mathematics) (03B30) Mechanization of proofs and logical operations (03B35) Euclidean geometries (general) and generalizations (51M05)
Cites Work
- A graphical user interface for formal proofs in geometry
- Cut Elimination in the Presence of Axioms
- A constructive theory of ordered affine geometry
- The axioms of constructive geometry
- Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
- Title not available (Why is that?)
- Translating higher-order clauses to first-order clauses
- Machine Proofs in Geometry
- Title not available (Why is that?)
- Title not available (Why is that?)
- Eudoxos and Dedekind: On the ancient Greek theory of ratios and its relation to modern mathematics
- Title not available (Why is that?)
- Euclid and his twentieth century rivals. Diagrams in the logic of Euclidean geometry
- Title not available (Why is that?)
- Tarski's System of Geometry
- Mathematics in Kant's critical philosophy. Reflections on mathematical practice
- System Description: Spass Version 3.0
- Title not available (Why is that?)
- Solving open questions and other challenge problems using proof sketches
- Proof Style and Understanding in Mathematics I: Visualization, Unification and Axiom Choice
- Logic in philosophy of mathematics
Cited In (49)
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
- Logic of imagination. Echoes of Cartesian epistemology in contemporary philosophy of mathematics and beyond
- Diagrammatic reasoning in Euclid's Elements
- From Euclidean geometry to knots and nets
- Proof-checking Euclid
- On the inconsistency of Mumma's Eu
- Enthymemathical Proofs and Canonical Proofs in Euclid’s Plane Geometry
- Automated theorem proving in GeoGebra: current achievements
- Geometric Rules in Infinitary Logic
- A formalization of Kant's transcendental logic
- ‘CHASING’ THE DIAGRAM—THE USE OF VISUALIZATIONS IN ALGEBRAIC REASONING
- Can one design a geometry engine? Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries
- From informal to formal proofs in Euclidean geometry
- Figures, Formulae, and Functors
- Automated generation of illustrated proofs in geometry and beyond
- Informal proofs and mathematical rigour
- The material reasoning of folding paper
- Brouwer and Euclid
- Operationalism: an interpretation of the philosophy of ancient Greek geometry
- Inconsistency in mathematics and the mathematics of inconsistency
- From mathematical axioms to mathematical rules of proof: recent developments in proof analysis
- Implementing Euclid's straightedge and compass constructions in type theory
- 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 of construction in problems and theorems in Euclid's \textit{Elements} I--VI
- Mathematical formalization and diagrammatic reasoning: the case study of the braid group between 1925 and 1950
- A Vernacular for Coherent Logic
- Prolegomena to a cognitive investigation of Euclidean diagrammatic reasoning
- Euclid's common notions and the theory of equivalence
- Carroll's infinite regress and the act of diagramming
- Constructibility and Geometry
- CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE
- GeoLogic – Graphical Interactive Theorem Prover for Euclidean Geometry
- Cognitive artifacts for geometric reasoning
- A constructive version of Tarski's geometry
- Automated generation of illustrations for synthetic geometry proofs
- Three-dimensional affine spatial logics
- Theorem proving as constraint solving with coherent logic
- Reliability of mathematical inference
- Title not available (Why is that?)
- Geometrisation of first-order logic
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- And so on \dots : reasoning with infinite diagrams
- Constructive geometrical reasoning and diagrams
- Human diagrammatic reasoning and seeing-as
- The twofold role of diagrams in Euclid's plane geometry
- Why did Euclid not need the Pasch axiom?
- Open texture and mathematics
- Proofs, pictures, and Euclid
Uses Software
This page was built for publication: A FORMAL SYSTEM FOR EUCLID’SELEMENTS
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5850985)
