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.
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