Transcript CDEG - University of Northern Colorado

CDEG: Computerized Diagrammatic Euclidean Geometry 2.0
Nathaniel Miller
University of Northern Colorado, Greeley, CO, USA
http://www.unco.edu/NHS/mathsci/facstaff/Miller/personal/CDEG
[email protected]
This poster briefly describes the computer proof system CDEG, version 2.0. CDEG stands for “Computerized Diagrammatic Euclidean Geometry.” 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. It is
based on the diagrammatic formal system FG, which is described in detail in the book Euclid and his Twentieth Century Rivals: Diagrams in the Logic of Euclidean Geometry. That book
also describes an earlier version of CDEG; however, CDEG has evolved significantly since the publication of the book. In particular, a beta version of CDEG is now publicly available,
and can be downloaded from the website given above. I encourage anyone who is interested in this research to download CDEG and to try it out for themselves.
CDEG Diagrams
CDEG diagrams contain several numbered
elements:
* circles, which represent points;
• solid line segments, which represent straight
lines;
• dotted line segments, which represent circles;
• A bold line around the edge, called the frame,
which encloses our diagram; and
• rectangles, which label regions in the diagram.
A sample diagram is shown below.
This
diagram shows two points, the segment
connecting them, and the circle drawn on this
segment.
CDEG diagrams are based on the idea that all of the
information contained in a diagram is reflected in the planar
topology of the diagram, and two diagrams with the same
planar topology are equivalent. (Two diagrams have the
same planar topology if one can be stretched into the other
while staying in the plane.)
CDEG vs. Euclid’s Elements
CDEG’s commands are closely related to Euclid’s
Postulates, Common Notions, and Definitions from
the Elements, so that most proofs from the
Elements can be formalized using CDEG. The two
tables shown here summarize these connections.
A second, more complicated diagram is shown below. This
diagram, which occurs in the proof of Euclid’s first Proposition,
shows two intersecting circles that contain an equilateral
triangle.
Why a Computer System?
CDEG is essentially a computer implementation of the formal system FG described in [14]. Why would we want
to implement an existing formal system on a computer?
1.To demonstrate that this system really is completely formal and works as advertised. This worry is not just
academic. A number of other published diagrammatic formal systems for Euclidean geometry that were not
implemented on a computer have later turned out to be unsound, inconsistent, and did not work as their authors
intended. A computer implementation shows that the system is fully formalized and gives the opportunity to
check that it works as intended.
Note that different circles and lines are identified
by the use of different colors.
Selected References
1.
2.
3.
4.
Euclid. 1956. The Elements. New York: Dover, 2nd edn. Translated with introduction and commentary by Thomas L. Heath.
Hilbert, David. 1971. Foundations of Geometry. La Salle, Ill.: Open Court Publishing Co., 4th edn. Translated by Leo Unger.
Miller, Nathaniel. CDEG User’s Manual. Availablefrom http://www.unco.edu/NHS/mathsci/facstaff/Miller/personal/CDEG/.
Miller, Nathaniel. 2007. Euclid and his twentieth century rivals: Diagrams in the logic of Euclidean geometry. Stanford, CA: CSLI Press.
2.To make it available for other people to try out. Few people are going to take the time to try to understand
exactly how a formal system works. A computer implementation makes it much more likely that they will try it
out. If you’ve read this far, you may be interested enough to want to try it. I encourage you to try it out!
3. In order to explore exactly what it can prove. This system is intended to formalize Euclid’s proof methods
from the Elements, and it should be able to duplicate most or all of the proofs in the first four books of the
Elements. Without a working computer implementation, this claim is essentially unverifiable. With the computer
implementation, verifying this is now an ongoing research project.