Current Research Activities:
Reasoning with Geometric Diagrams - It has long been assumed in
mathematical communities that diagrams can be properly used only as aids
to human intuition which have no place in formal proofs, reducing diagrams
to second-class citizens of the mathematical world. My research aims
to show that diagrams can be used rigorously and fruitfully in formal mathematics,
and, indeed, that the formal proofs that one gets using diagrams are more
understandable and correspond better to normal informal proofs (of
the kind that one finds in Euclid's Elements, for example) than
traditional linguistic formal proofs.
- The most complete and up to date version of my work with diagrams is found in my book Euclid and His Twentieth Century Rivals: Diagrams in the Logic of Euclidean Geometry, available here from the University of Chicago Press. It is also available from most online booksellers.
- An extended abstract of this book was presented at the Diagrams 2006 conference at Stanford University and appeared the Springer-Verlag Lecture Notes in AI Series volume 4045 Diagrammatic Representation and Inference, Barker-Plummer, Cox, and Swoboda, eds.,
© 2006 Springer-Verlag. You can download it here: extabstract.pdf.
- The most technical results about the computational complexity of using diagrams in Euclidean geometry can be found in my article "Computational Complexity of Diagram Satisfaction in Euclidean Geometry," Journal of Complexity 22 (2006) 250-274, which is available here.
- My 2001 Cornell Ph.D.
dissertation is A Diagrammatic Formal System for Euclidean Geometry.
You can download it in pdf form here: thesis.pdf.
In addition to describing my formal system FG for giving diagrammatic
proofs in Euclidean Geometry, it contains: a short history of diagrams,
logic, and geometry, from 1700 B.C. up to the present; examples of
how to use weaker subsystems of FG to determine the logical structure
of geometry; discussion of the unique role of lemmas in diagrammatic proofs
in geometry; sample transcripts from CDEG, the computer system
implementation of FG; proofs that the question of whether or not
a given diagram is satisfiable (that is, whether or not it represents a
physically realizable situation) is decidable, but is NP-hard, and therefore
not solvable in a reasonable amount of time; a discussion of
earlier work by Isabel Luengo developing a different diagrammatic formal
system for geometry, and an explaination of why her system in unsound;
and a general discussion of why a formal system like FG is useful.
This is a three page non-technical overview of some of my work, in pdf
It was published in the Springer-Verlag Lecture Notes in AI Series volume Theory and Application of Diagrams, Anderson, Cheng, and Haarslev, eds.,
© 2000 Springer-Verlag.
I presented an expanded version of this overview as a poster at the Diagrams
2000 conference at the University of Edinburgh; you can download
the full text of the poster in pdf format here.
Here is the paper "Case Analysis in Euclidean
Geometry," which is refered to in this overview:
- Generalized Baseball Curves: Three Symmetries and You're In!, written with Dean Allison and Ricardo Diaz, was published in the online MAA journal Loci. The curve traced out on a baseball by its seam has many symmetries. This article explores the class of closed spherical curves with the same symmetries, which we call generalized baseball curves.
- "Visualization on Cones and Pool Tables Using Geometer's Sketchpad" describes several activities that I have developed for use in an undergraduate modern geometry course for pre-service K-12 teachers. It was published in PRIMUS, Vol. XVI, No. 3 (September 2006), pp. 257 - 274, and can be downloaded here: primus.pdf. (Unfortunately, it is a very large file.)
- "A Brief Proof of the Full Completeness of Shin's Venn Diagram Proof System" was published in the Journal of Philosophical Logic (2006) 35: 289-291, and is available here.
To read the pdf files, you need the Adobe Acrobat reader, which you can download
for free here.