BEGIN:VCALENDAR
VERSION:2.0
PRODID:ILLC Website
BEGIN:VEVENT
UID:/NewsandEvents/Events/Upcoming-Events/newsitem
/9388/25-October-2017-Proof-checking-Euclid-Michae
l-Beeson
DTSTAMP:20171012T153341
SUMMARY:Proof-checking Euclid, Michael Beeson
ATTENDEE;ROLE=Speaker:Michael Beeson
DTSTART:20171025T120000
DTEND:20171025T140000
LOCATION: Ravensteynzaal, Kromme Nieuwegracht 80,
3512 HM Utrecht
DESCRIPTION:This is joint work with Julien Narboux
and Freek Wiedijk. We used computer proof-checkin
g methods to verify the correctness of our proofs
of the propositions in Euclid Book I. We used axio
ms as close as possible to those of Euclid, in a l
anguage closely related to that used in Tarski's f
ormal geometry. We used proofs as close as possibl
e to those given by Euclid, but filling Euclid's g
aps and correcting errors. Then we checked those p
roofs in the well-known and trusted proof checkers
HOL Light and Coq. The talk will contain many geo
metrical diagrams and discuss both the geometry an
d the proof-checking.
X-ALT-DESC;FMTTYPE=text/html:\n This is joint
work with Julien Narboux and Freek Wiedijk. We use
d computer proof-checking methods to verify the co
rrectness of our proofs of the propositions in Euc
lid Book I. We used axioms as close as possible to
those of Euclid, in a language closely related to
that used in Tarski's formal geometry. We used pr
oofs as close as possible to those given by Euclid
, but filling Euclid's gaps and correcting errors.
Then we checked those proofs in the well-known an
d trusted proof checkers HOL Light and Coq. The ta
lk will contain many geometrical diagrams and disc
uss both the geometry and the proof-checking.

\
n
URL:http://www.michaelbeeson.com/research/Foundati
onsOfGeometry/index.php?include=CheckingEuclid
CONTACT:Professor A. Visser at a.visser at uu.nl
END:VEVENT
END:VCALENDAR