EasyChair Publications
Search
Paper Information
Paper:Chad Brown and Christine Rizkallah
From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction
Title:From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction
Authors:Chad Brown and Christine Rizkallah
Keyphrases:higher order logic, simple type theory, classical, extensional, intuitionistic, intensional, proof theory, tableaux, analytic tableaux
Paper:
Abstract:We define a translation that maps higher-order formulas provable in a classical extensional 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.
Volume:Jasmin Christian Blanchette and Josef Urban (editors). PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Series:EPiC Series in Computing
Volume number:14
Pages:27-42
Editors:Jasmin Christian Blanchette and Josef Urban
Page views:29
Downloads:21
BibTeX entry:
@inproceedings{PxTP2013:From_Classical_Extensional_Higher-Order_Tableau_to_Intuitionistic_Intentional_Natural_Deduction,
  author    = {Chad E. Brown and Christine Rizkallah},
  title     = {From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction},
  booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
  editor    = {Jasmin Christian Blanchette and Josef Urban},
  series    = {EPiC Series in Computing},
  volume    = {14},
  pages     = {27-42},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}