Christine S. Rizkallah
Author: Christine Rizkallah
Advisor: Chad E Brown
Supervisor: Gert Smolka
By the Curry-Howard(-deBruijn) correspondence we can think of propositions as types and (natural deduction) proofs as terms. Following this tradition, a notion of proof term for simply typed (intuitionistic) higher-order logic are given in . One can then add constants to include classical or extensional reasoning principles.
Automated theorem provers typically do not search for natural deduction proofs. Even many interactive theorem provers do not primarily use natural deduction. With Jitpro, for example, users construct a tableau proof. A tableau proof can be seen as a special kind of sequent calculus proof.
The goal of this project is to define proof representations for simple type theory and give translations between them. In particular, a translation from tableau proofs to natural deduction proof terms should be given. If time allows, the procedure could be implemented or proven correct.
You can find the final thesis here. It was submitted on Saturday, 05.12.2009.
I gave two introductory talks concerning my thesis. One at Max-Planck Institute für Informatik on Monday, 12.01.2009. The other in the Programming Systems group on Friday, 16.01.2009.
For viewing the abstract of the talks, click here.
I gave the proposal talk in the Programming Systems group on Friday, 17.04.2009.
For viewing the abstract of the proposal talk, click here.
I gave the final talk in the Programming Systems group on Friday, 18.12.2009.
For viewing the abstract of the final talk, click here.