The Complexity of Propositional Implication

TL;DR

This paper classifies the computational complexity of propositional implication problems based on different Boolean connectives, showing efficient solutions only for certain restricted connectives and coNP-completeness otherwise.

Contribution

It provides a complete complexity classification for propositional implication across all Boolean function sets in Post's lattice, highlighting cases with efficient solutions.

Findings

Implication is efficiently solvable only with connectives definable from {false,true} and one of {and,or,xor}.

In all other cases, the implication problem is coNP-complete.

The complexity classification covers all Boolean function sets in Post's lattice.

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.