Computability in Europe 2008
Logic and Theory of Algorithms

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