The complexity of propositional proofs

TL;DR

This paper investigates the complexity of propositional proofs for classical and intuitionistic tautologies, introducing a polynomial-time decision procedure for certain tautologies and exploring implications for proof system complexity.

Contribution

It presents a nondeterministic polynomial-time decision procedure for intuitionistic implicational tautologies using proof diagrams and extends this to classical tautologies, linking to complexity classes.

Findings

Decides intuitionistic implicational tautologies in nondeterministic polynomial time

Transforms proofs into polynomial-sized forms relative to input formulas

Extends decision procedures to all classical and intuitionistic tautologies

Abstract

In this paper, we consider the complexity of propositional proofs of classical and intuitionistic tautologies. In fact, we describe a nondeterministic polynomial-time decision procedure for intuitionistic implicational tautologies. For this purpose, we reduce a decision problem for intuitionistic implicational tautologies to a decision problem for deductive proof diagrams which are a short form for representing of proofs in the intuitionistic implicational calculus. Next, we transform deductive proof diagrams to a special form in which any proof has the size bounded by a polynomial in the length of input formula. Also, we show that this procedure can be extended to all classical and intuitionistic tautologies, and deduce some corollaries including results about complexity classes and polynomially bounded proof systems.