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/2014/newsitem/5687/8-J uly-2014-CICM-2014-workshop-The-Notion-of-Proof-Co imbra-Portugal DTSTAMP:20140512T000000 SUMMARY:CICM-2014 workshop "The Notion of Proof", Coimbra, Portugal DTSTART;VALUE=DATE:20140708 DTEND;VALUE=DATE:20140708 LOCATION:Coimbra, Portugal DESCRIPTION:The traditional notion of mathematical proof faces in the 21st century what we will call "the computer challenge". Three different aspects are worth separating. 'Proof search' has its know n limitations due to undecidability and complexity results. However, special areas, such as semigrou p theory, already enjoy considerable support from computer-generated proofs. 'Proof check' is recent ly the 'hottest' area, in no small part due to the attempt to formally verify the proof of the Keple r conjecture by its author Hales. 'Proof represent ation' seems currently be the stumbling block for convincing the mathematical community to accept co mputer-aided theorem proving as a viable complemen t to everyday mathematical research. For our wor kshop we solicit contributions for discussions abo ut the current state-of-the-art of automated theor em proving (ATP), approaching the topic from the m athematical (or even philosophical) side, as well as from computer science. For more information, see the workshop homepage at http://cicm-conferenc e.org/2014/cicm.php?event=nop. In addition to s tandard scientific/philosophical papers, descripti ons and demonstrations of computer systems that be ar on these issues are also welcome. Submission de adline is May 31. X-ALT-DESC;FMTTYPE=text/html:
\n The traditional notion of mathematical proof faces in the 21st\n century what we will ca ll "the computer\n challenge". Th ree different aspects are worth separating.\n 'Proof search' has its known limitations due to undecidability\n and complexity results. H owever, special areas, such as\n semigroup theory, already enjoy considerable support from\n computer-generated proofs. 'Proof check' i s recently the\n 'hottest' area, in no smal l part due to the attempt to\n formally ver ify the proof of the Kepler conjecture by its\n author Hales. 'Proof representation' seems c urrently be the\n stumbling block for convi ncing the mathematical community to\n accep t computer-aided theorem proving as a viable compl ement\n to everyday mathematical research.\ n
\nFor our workshop we solicit contributions for discussions about the\n c urrent state-of-the-art of automated theorem provi ng (ATP),\n approaching the topic from the mathematical (or even philosophical)\n side , as well as from computer science.\n
\n \n \nFor more information, see th e workshop homepage at\n http://cicm-conference.org/2014/cicm.php ?event=nop.\n
\ n In addition to standard\n scientif ic/philosophical papers, descriptions and demonstr ations of\n computer systems that bear on t hese issues are also welcome.\n Submission deadline is May 31.\n
\n