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/2004/newsitem/695/26-M ay-2004-Automath-Symposium-Auditorium-16-TU-Eindho ven DTSTAMP:20040520T000000 SUMMARY:Automath Symposium, Auditorium 16, TU Eind hoven ATTENDEE;ROLE=Speaker:Henk Barendregt, Herman Geuv ers, Freek Wiedijk, N.G. de Bruijn, Georgi Jojgov DTSTART;TZID=Europe/Amsterdam:20040526T143000 DTEND;TZID=Europe/Amsterdam:20040526T000000 LOCATION:Auditorium 16, TU Eindhoven DESCRIPTION:An important question is whether compu ter assisted proofs are acceptable to the scientif ic community. One can distinguish romantic (human understandable) vs cool (machine verified) proofs. The heart of the matter is whether a proof is rel iable. Reliability can be obtained by providing fu lly formalised proofs that can be algorithmically verified. The methodology of de Bruijn's Automath Project delivers proofs that are reliable and huma n-readable. What is the feasibility of construc ting fully formalised proofs for `everyday use' in mathematics? Interactive support from the compute r in developing proofs brings us a step forward, b ut how far can we get? On the occasion of the digi tizing of the Automath Archive a short symposium i s organised on these matters, as a cooperation of the ZIC-colloquium and the Brouwer Seminar of the Foundations group in Nijmegen. All information on the program of this symposium can be found at t he website: http://www.win.tue.nl/automath/. For m ore information, please contact f.dechesne at uvt. nl X-ALT-DESC;FMTTYPE=text/html:\n
\nAn impor tant question is whether computer assisted proofs are acceptable to the scientific community. One ca n distinguish romantic (human understandable) vs c ool (machine verified) proofs. The heart of the ma tter is whether a proof is reliable. Reliability c an be obtained by providing fully formalised proof s that can be algorithmically verified. The method ology of de Bruijn's Automath Project delivers pro ofs that are reliable and human-readable.\n < /p>\n
\nWhat is the feasibility of constru cting fully formalised proofs for `everyday use' i n mathematics? Interactive support from the comput er in developing proofs brings us a step forward, but how far can we get?\nOn the occasion of the di gitizing of the Automath Archive a short symposium is organised on these matters, as a cooperation of the ZIC-colloquium and the Brouwer Seminar of t he Foundations group in Nijmegen.\n
\n \n\n All information on the progr am of this symposium can be found at the website: http://www.win.tue.nl/automath/.\n For more information, please contact f.dechesne at uvt. nl\n
URL:/NewsandEvents/Archives/2004/newsitem/695/26-M ay-2004-Automath-Symposium-Auditorium-16-TU-Eindho ven END:VEVENT END:VCALENDAR