The Complexity of Propositional Implication
arXiv:0811.0959 · doi:10.1016/j.ipl.2009.06.015
Abstract
The question whether a set of formulae G implies a formula f is fundamental. The present paper studies the complexity of the above implication problem for propositional formulae that are built from a systematically restricted set of Boolean connectives. We give a complete complexity classification for all sets of Boolean functions in the meaning of Post's lattice and show that the implication problem is efficentily solvable only if the connectives are definable using the constants {false,true} and only one of {and,or,xor}. The problem remains coNP-complete in all other cases. We also consider the restriction of G to singletons.
Cited by in corpus (10)
- Complexity of Non-Monotonic Logics
- Generalized Satisfiability for the Description Logic ALC
- On the Applicability of Post's Lattice
- On the Parameterized Complexity of Default Logic and Autoepistemic Logic
- Merging fragments of classical logic
- Complexity of Propositional Abduction for Restricted Sets of Boolean Functions
- Generalized Complexity of ALC Subsumption
- Complexity Classifications for Propositional Abduction in Post's Framework
- The Complexity of Reasoning for Fragments of Default Logic
- The Weight in Enumeration