Computability in Europe 2008
Logic and Theory of Algorithms

Print current page  Print this page

Regular Talk:
Towards Reverse Proofs-as-Programs

Edit abstract data

THIS TALK HAS BEEN CANCELLED!!!
Speaker: Reinhard Kahle

Abstract

In this programmatic paper we renew the well-known question ``What
is a proof?''.  Starting from the challenge of the mathematical
community by computer based theorem provers we discuss how the
experiences from examinations of proofs can help to sharpen the
question. With relation to the notion of equality of
proofs, we propose to investigate proofs in
relation to \textsc{Moschovakis}'s theory of algorithms. This should
be carried out by a ``reverse engineering'' of program extraction
functions underlying the \emph{proofs-as-programs} paradigm.


websites: Arnold Beckmann 2008-06-04 Valid HTML 4.01! Valid CSS!