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

Legal notice, Privacy policy