BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A formal system for Euclidean diagrammatic reasoning - Jeremy Avig
 ad (Carnegie Mellon University)
DTSTART:20091027T130000Z
DTEND:20091027T140000Z
UID:TALK19687@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:This talk presents work carried out jointly with Ed Dean and J
 ohn Mumma.\n\nFor more than two thousand years\, Euclid's Elements was vie
 wed as the paradigm of rigorous argumentation. But this changed in the nin
 eteenth century\, with concerns over the use of diagrammatic inferences an
 d their ability to secure general validity. Axiomatizations by Pasch\, Hil
 bert\, and later Tarski are now taken to  \nrectify these shortcomings\, b
 ut proofs in these axiomatic systems look very different from Euclid's.\n\
 nIn 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 syste
 m with both diagram- and text-based inferences that provides a much more f
 aithful representation of Euclidean reasoning.  \nFor the class of theorem
 s 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.\n\nThe system's one-step inferences ar
 e smoothly verified by current automated reasoning technology. This makes 
 it possible to formally verify Euclidean diagrammatic proofs\, and provide
 s useful insight into the nature of mathematical proof more generally.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR