Publication details

Saarland University Computer Science

Proof Representations for Higher-Order Logic

Christine Rizkallah

Master's Thesis, Saarland University, December 2009

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.

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009