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  <p>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.</p>\
 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