On the lengths of proofs in the propositional calculus.
Robert A. Reckhow · TSpace (University of Toronto) · 1976
Just as P = NP if and only if some NP-complete set ; is a member of P, the class NP is closed under complementation if and only if the complement of some NP- complete set is a member of NP. This in turn leads to the fact that NP is closed under complementa~ion if and only if there exists a system for proving tautologies of the propositional calculus in which each tautology has a (polynomial-time verifiable) proof whose length is no greater than some fixed polynomial in ; the length of the tautology. Such a system is called a polynornial-bqunded verification system. Most of the important proof systems for the propositional calculus that have been proposed in the literature have been investigated, and two types of results are reported. The first are simulation results that show that if one system is polynomial-bounded, then the simulating system is also polynomial-bounded. Such simulations are shown for all Frege systems (called "Hilbert -type" systems by Kleene), natural deduction systems, and Gentzen systems with cut. Frege system with the substitution rule simulate all other systems studied. The second type of results are lower bounds, where certain systems are shown not to be polynomial-bounded. Lower bounds are reported for regular resolution, semantic trees, analytic tableaux, and other systems, and Tseitin's lower bound for regular resolution is improved and applied to certain systems of regular resolution with limited extension.