Graph Drawing for Formalized Diagrammatic Proofs in Geometry

摘要

CDEG, "Computerized Diagrammatic Euclidean Geometry," is a computerized formal system for giving diagrammatic proofs in Euclidean geometry which uses planar graphs in drawing its diagrams. Here we discuss some of the graph-theoretic problems that arise in this context. This computer proof system implements a diagrammatic formal system for giving diagram-based proofs of theorems of Euclidean geometry that are similar to the informal proofs found in Euclid's Elements. The theoretical ideas underlying this system and the original version of CDEG are described in detail in the book Euclid and his Twentieth Century Rivals: Diagrams in the Logic of Euclidean Geometry [4]. A much updated version of CDEG is now publicly available at [1]. Interested readers are encouraged to download CDEG and to try it out for themselves.