The complexity of propositional implication

DOI10.1016/J.IPL.2009.06.015zbMATH Open1202.68207arXiv0811.0959OpenAlexW1976656121WikidataQ57998326 ScholiaQ57998326MaRDI QIDQ989577FDOQ989577

Authors: J. Martínez 

Publication date: 20 August 2010

Published in: Information Processing Letters (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/0811.0959

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

zbMATH Keywords

computational complexityPost's latticepropositional implication

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25)

Cites Work

• Title not available (Why is that?)
• The Two-Valued Iterative Systems of Mathematical Logic. (AM-5)
• Structure and importance of logspace-MOD class
• Satisfiability problems for propositional calculi
• Characterizations of Pushdown Machines in Terms of Time-Bounded Computers
• The Complexity of Reasoning for Fragments of Default Logic
• Mathematical Foundations of Computer Science 2003
• Constant Depth Reducibility
• The Complexity of Generalized Satisfiability for Linear Temporal Logic
• The complexity of satisfiability for fragments of CTL and \(\text{CTL}^*\)

Cited In (19)

• Generalized satisfiability for the description logic \(\mathcal{ALC}\)
• Strong backdoors for default logic
• The complexity of circumscriptive inference in Post's lattice
• Title not available (Why is that?)
• A note on the computational complexity of the pure classical implication calculus
• Sets of Boolean connectives that make argumentation easier
• Logic for Programming, Artificial Intelligence, and Reasoning
• On the applicability of Post's lattice
• 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
• The Complexity of Reasoning for Fragments of Default Logic
• 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)