A FORMAL SYSTEM FOR EUCLID’SELEMENTS
From MaRDI portal
Publication:5850985
Abstract: We present a formal system, E, which provides a faithful model of the proofs in Euclid's Elements, including the use of diagrammatic reasoning.
Recommendations
- scientific article; zbMATH DE number 4030358
- scientific article; zbMATH DE number 51594
- scientific article; zbMATH DE number 4146970
- Euclidean systems
- scientific article; zbMATH DE number 2144363
- scientific article; zbMATH DE number 3863979
- Formal systems of constructive mathematics
- scientific article; zbMATH DE number 703114
Cites work
- scientific article; zbMATH DE number 1577093 (Why is no real title available?)
- scientific article; zbMATH DE number 3119278 (Why is no real title available?)
- scientific article; zbMATH DE number 3930937 (Why is no real title available?)
- scientific article; zbMATH DE number 1313585 (Why is no real title available?)
- scientific article; zbMATH DE number 1317261 (Why is no real title available?)
- scientific article; zbMATH DE number 1150716 (Why is no real title available?)
- A constructive theory of ordered affine geometry
- A graphical user interface for formal proofs in geometry
- Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
- Cut Elimination in the Presence of Axioms
- Euclid and his twentieth century rivals. Diagrams in the logic of Euclidean geometry
- Eudoxos and Dedekind: On the ancient Greek theory of ratios and its relation to modern mathematics
- Logic in philosophy of mathematics
- Machine Proofs in Geometry
- Mathematics in Kant's critical philosophy. Reflections on mathematical practice
- Proof Style and Understanding in Mathematics I: Visualization, Unification and Axiom Choice
- Solving open questions and other challenge problems using proof sketches
- System Description: Spass Version 3.0
- Tarski's System of Geometry
- The axioms of constructive geometry
- Translating higher-order clauses to first-order clauses
Cited in
(50)- A constructive version of Tarski's geometry
- The material reasoning of folding paper
- Automated generation of illustrations for synthetic geometry proofs
- Figures, formulae, and functors
- Euclid's common notions and the theory of equivalence
- Automated theorem proving in GeoGebra: current achievements
- The Euclidean Programme
- Constructive geometry and the parallel postulate
- On the inconsistency of Mumma's Eu
- From mathematical axioms to mathematical rules of proof: recent developments in proof analysis
- Geometric Rules in Infinitary Logic
- Three-dimensional affine spatial logics
- scientific article; zbMATH DE number 6991364 (Why is no real title available?)
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
- Constructibility and Geometry
- Geometrisation of first-order logic
- GeoLogic – Graphical Interactive Theorem Prover for Euclidean Geometry
- Operationalism: an interpretation of the philosophy of ancient Greek geometry
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- Theorem proving as constraint solving with coherent logic
- 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
- Implementing Euclid's straightedge and compass constructions in type theory
- Automated generation of illustrated proofs in geometry and beyond
- Open texture and mathematics
- Mathematical formalization and diagrammatic reasoning: the case study of the braid group between 1925 and 1950
- Informal proofs and mathematical rigour
- Enthymemathical Proofs and Canonical Proofs in Euclid’s Plane Geometry
- A formalization of Kant's transcendental logic
- 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
- Diagrammatic reasoning in Euclid's Elements
- From Euclidean geometry to knots and nets
- 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
- Inconsistency in mathematics and the mathematics of inconsistency
- Cognitive artifacts for geometric reasoning
- Proofs, pictures, and Euclid
- Logic of imagination. Echoes of Cartesian epistemology in contemporary philosophy of mathematics and beyond
- A vernacular for coherent logic
- Brouwer and Euclid
- Reliability of mathematical inference
- Why did Euclid not need the Pasch axiom?
- Prolegomena to a cognitive investigation of Euclidean diagrammatic reasoning
- Proof-checking Euclid
- `Chasing' the diagram -- the use of visualizations in algebraic reasoning
- Carroll's infinite regress and the act of diagramming
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)
