A polynomial time complete disjunction property in intuitionistic propositional logic

2013/12/11 by Arai, Toshiyasu
#03F99 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1312.3059

Abstract

We extend the polynomial time algorithms due to Buss and Mints(APAL 1999) and Ferrari, Fiorentini and Fiorino(LPAR 2002) to yield a polynomial time complete disjunction property in intuitionistic propositional logic.

Related

• The complexity of propositional proofs
• First-Order Intuitionistic Logic with Decidable Propositional Atoms
• On Computationally Efficient Subsystems of Propositional Logic
• Ruitenburg's Theorem Mechanized and Contextualized
• Proof search in multi-succedent sequent calculi for intuitionistic logic under the Schuette's schema