Twentieth-century developments in logic and mathematics have led many
people to view Euclid's proofs as inherently informal, especially
due to the use of diagrams in proofs. In Euclid and His
Twentieth-Century Rivals, Nathaniel Miller discusses the history of
diagrams in Euclidean Geometry, develops a formal system for working
with them, and concludes that they can indeed be used
rigorously. Miller also introduces a diagrammatic computer proof
system, based on this formal system. This volume will be of interest
to mathematicians, computer scientists, and anyone interested in the
use of diagrams in geometry.

Nathaniel Miller is assistant professor of Mathematical Sciences at the University of Northern Colorado.

- 1 Background
- 1.1 A Short History of Diagrams, Logic, and Geometry
- 1.2 The Philosophy Behind this Work
- 1.3 Euclid's
*Elements*

- 2 Syntax and Semantics of Diagrams
- 2.1 Basic Syntax of Euclidean Diagrams
- 2.2 Advanced Syntax of Diagrams: Corresponding Graph Structures and DIagram Equivalence Classes
- 2.3 Diagram Semantics

- 3 Diagrammatic Proofs
- 3.1 Construction Rules
- 3.2 Inference Rules
- 3.3 Transformation Rules
- 3.4 Dealing with Areas and Lengths of Circular Arcs
- 3.5
**CDEG**

- 4 Meta-mathematical Results
- 4.1 Lemma Incorporation
- 4.2 Satisfiable and Unsatisfiable Diagrams
- 4.3 Transformations and Weaker Systems

- 5 Conclusions
- Appendix B: Hilbert's Axioms
- Appendix C: Isabel Luengo's DS1
- Appendix D: A CDEG transcript
- References
- Index

April 2007