A formal system for Euclid's Elements

2008/10/31 by Jeremy Avigad, Edward Dean, John Mumma · 1 citation
Mathematics · #math.LO #msc:03B30 #msc:51M05 #msc:03B35

paper · pdf · doi:10.1017/s1755020309990098

published as Review of Symbolic Logic 2:4 (2009) 700-768

arxiv created 2009/05/04 · arxiv updated 2014/01/03

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.

Cited by

• Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

Related

• Proof-checking Euclid
• On diagrams accompanying reductio ad absurdum proofs in Euclid's Elements book I. Reviewing Hartshorne and Manders
• Parts, Wholes, and Quantity in Euclid’s Elements
• A new proof of Euclid's algorithm
• Book I of Euclid's Elements and application of areas