CSLI Publications logo
new books
knuth books
for authors
CSLI Publications
Euclid and His Twentieth Century Rivals cover

Euclid and His Twentieth Century Rivals

Diagrams in the Logic of Euclidean Geometry

Nathaniel Miller

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

ISBN (Paperback): 9781575865089
ISBN (Cloth): 9781575865072
ISBN (electronic): 9781575868172

Add to Cart
View Cart

Check Out

Distributed by the
University of
Chicago Press

pubs @ csli.stanford.edu