Saarland University

Informatics

Programming Systems

Christine S. Rizkallah

Master's Thesis

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 [1]. 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.

**Thesis**

You can find the final thesis here.
It was submitted on Saturday, 05.12.2009.

**First
Talk**

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.

**Proposal Talk**

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.

**Final Talk**

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.

- Intuitionistic Logic.
- Introduction to computational logic, by G. Smolka and C. E. Brown, 2009.
- Jitpro: A JavaScript Interactive higher-order Tableau Prover.

- Stefan Berghofer and Tobias Nipkow. Proof terms for simply typed higher order logic. In
*TPHOLs '00: Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics*, pages 38-52, London, UK, 2000. Springer-Verlag. - R. O. Gandy. On the axiom of extensionality - part I.
*Journal of Symbolic Logic*, 21(1):36-48, 1956. - J.-Y. Girard, P. Taylor, and Y. Lafont.
*Proofs and types*. Cambridge University Press, 1989. - S. Kuroda. Intuitionistische Untersuchgen der formalistischen Logik.
*Nagoya Mathematical Journal*, 2:35-47, 1951. - K. Zdanowski. On second order intuitionistic propositional logic without a universal quantifier.
*Journal of Symbolic Logic*, 74:157-167, 2009.