BEGIN:VCALENDAR
VERSION:2.0
PRODID:ILLC Website
X-WR-TIMEZONE:Europe/Amsterdam
BEGIN:VTIMEZONE
TZID:Europe/Amsterdam
X-LIC-LOCATION:Europe/Amsterdam
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
UID:/NewsandEvents/Archives/2017/newsitem/9388/25-
October-2017-Proof-checking-Euclid-Michael-Beeson
DTSTAMP:20171012T153341
SUMMARY:Proof-checking Euclid, Michael Beeson
ATTENDEE;ROLE=Speaker:Michael Beeson
DTSTART;TZID=Europe/Amsterdam:20171025T120000
DTEND;TZID=Europe/Amsterdam: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