\n

\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\n

URL:/NewsandEvents/Archives/2014/newsitem/5687/8-J
uly-2014-CICM-2014-workshop-The-Notion-of-Proof-Co
imbra-Portugal
END:VEVENT
END:VCALENDAR
\n In addition to standard\n sc ientific/philosophical papers, descriptions and de monstrations of\n computer systems that bea r on these issues are also welcome.\n Submi ssion deadline is May 31.\n

\n