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.
Recommendations
- The complexity of the falsifiability problem for pure implicational formulas
- Polynomial-time inference of all valid implications for Horn and related formulae
- A note on the computational complexity of the pure classical implication calculus
- The complexity of minimum partial truth assignments and implication in negation-free formulae
- The complexity of circumscriptive inference in Post's lattice
Cites work
- scientific article; zbMATH DE number 3888913 (Why is no real title available?)
- Characterizations of Pushdown Machines in Terms of Time-Bounded Computers
- Constant Depth Reducibility
- Mathematical Foundations of Computer Science 2003
- Satisfiability problems for propositional calculi
- Structure and importance of logspace-MOD class
- The Complexity of Generalized Satisfiability for Linear Temporal Logic
- The Complexity of Reasoning for Fragments of Default Logic
- The Two-Valued Iterative Systems of Mathematical Logic. (AM-5)
- The complexity of satisfiability for fragments of CTL and \(\text{CTL}^*\)
Cited in
(19)- The Complexity of Reasoning for Fragments of Default Logic
- Generalized satisfiability for the description logic \(\mathcal{ALC}\)
- The complexity of circumscriptive inference in Post's lattice
- Strong backdoors for default logic
- scientific article; zbMATH DE number 4114609 (Why is no real title available?)
- A note on the computational complexity of the pure classical implication calculus
- Sets of Boolean connectives that make argumentation easier
- On the applicability of Post's lattice
- Logic for Programming, Artificial Intelligence, and Reasoning
- Strong backdoors for default logic
- Generalized satisfiability for the description logic \(\mathcal{ALC}\) (extended abstract)
- Isomorphic implication
- The complexity of the falsifiability problem for pure implicational formulas
- Lewis dichotomies in many-valued logics
- On the parameterized complexity of non-monotonic logics
- Mathematical Foundations of Computer Science 2005
- The weight in enumeration
- Parameterized Complexity of Logic-based Argumentation in Schaefer’s Framework
- An unexpected Boolean connective
This page was built for publication: The complexity of propositional implication
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q989577)
