Saarland University
Informatics
Programming Systems
Christine S. Rizkallah
Master's Thesis


Master's Thesis: Proof Representations for Higher Order Logic

Author: Christine Rizkallah
Advisor: Chad E Brown
Supervisor: Gert Smolka

Introduction

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.

Goal

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 Abstract

We provide a mapping from classical extensional tableau proofs of higher-order formulas to intuitionistic non-extensional natural deduction proofs of semantically equivalent formulas. We show that the Kuroda transformation, which is known to map from first-order classical logic to first-order intuitionistic logic, extends to elementary type theory. Moreover, we introduce a transformation that we call Girard-Kuroda-Per and prove that this transformation maps from classical extensional to intuitionistic non-extensional simple type theory.

Downloads


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.

Related Links

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

Important References

  1. 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.
  2. R. O. Gandy. On the axiom of extensionality - part I. Journal of Symbolic Logic, 21(1):36-48, 1956.
  3. J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and types. Cambridge University Press, 1989.
  4. S. Kuroda. Intuitionistische Untersuchgen der formalistischen Logik. Nagoya Mathematical Journal, 2:35-47, 1951.
  5. K. Zdanowski. On second order intuitionistic propositional logic without a universal quantifier. Journal of Symbolic Logic, 74:157-167, 2009.