On Computationally Efficient Subsystems of Propositional Logic

TL;DR

This paper investigates the computational complexity of derivability in primal propositional logic, showing it remains polynomial-time solvable under certain substitutions but becomes co-NP-hard with others.

Contribution

It identifies specific conditions under which the derivability problem transitions from polynomial-time solvable to co-NP-hard in primal propositional logic.

Findings

Derivability remains polynomial-time solvable with a certain substitution principle.

Adding another substitution principle makes the problem co-NP-hard.

The complexity of propositional logic derivability depends on the form of substitution applied.

Abstract

In this paper, we show that the derivability problem for the primal propositional logic remains solvable in polynomial time upon adding a certain form of the principle of equivalent form substitution; and that, upon adding another form of this principle, it becomes co-NP-hard.