A formal system for Euclidean diagrammatic reasoning

Add to your list(s) Download to your calendar using vCal

• Jeremy Avigad (Carnegie Mellon University)
• Tuesday 27 October 2009, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact Thomas Tuerk.

This talk presents work carried out jointly with Ed Dean and John Mumma.

For more than two thousand years, Euclid’s Elements was viewed as the paradigm of rigorous argumentation. But this changed in the nineteenth century, with concerns over the use of diagrammatic inferences and their ability to secure general validity. Axiomatizations by Pasch, Hilbert, and later Tarski are now taken to rectify these shortcomings, but proofs in these axiomatic systems look very different from Euclid’s.

In this talk, I will argue that proofs in the Elements, taken at face value, can be understood in formal terms. I will describe a formal system with both diagram- and text-based inferences that provides a much more faithful representation of Euclidean reasoning. For the class of theorems that can be expressed in the language, the system is sound and complete with respect to Euclidean fields, that is, the semantics corresponding to ruler and compass constructions.

The system’s one-step inferences are smoothly verified by current automated reasoning technology. This makes it possible to formally verify Euclidean diagrammatic proofs, and provides useful insight into the nature of mathematical proof more generally.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.