Publication details

Saarland University Computer Science

From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction

Chad E. Brown, Christine Rizkallah

June 2013

We define a translation that maps higher-order formulas provable in a classical ex- tensional setting to semantically equivalent formulas provable in an intuitionistic intensional setting. For the classical extensional higher-order proof system we define a Henkin-complete tableau calculus. For the intuitionistic intensional higher-order proof system we give a natural deduction calculus. We prove that tableau provability of a formula implies provability of a translated formula in the natural deduction calculus. Implicit in this proof is a method for translating classical extensional tableau refutations into intuitionistic intensional natural deduction proofs.

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy