Proof complexity

In computer science, proof complexity is about the efficiency of automated theorem proving methods on proving contradiction. Proof complexity is mainly concerned with the relative size of proofs in propositional logic.

Different algorithms for theorem proving in propositional logic, such as resolution, the DPLL algorithm, etc. produce different proofs when applied to the same formula. Comparing the lenght of these proofs is a way for measuring the efficiency of these methods.

There are two points that make the study of proof complexity non-trivial:

1. the size of a proof depends on the formula that is to be proved inconsistent; therefore, a method may produce a short proof on a formula and a large proof on another formula, while a second method may exhibit the opposite behavior;
2. proof methods are typically non-deterministic, in that some steps are not univocally specified; for example, resolution is based on iteratively choosing a pair of clauses containing opposite literals and producing a new clause that is a consequence of them; several pairs of clauses may be available at each step, and these choices affect the proof lenght.

The first point is taken into account making a comparison for all possible formulae. The second point is taken into account by assuming that, for each formula, the shorter possible proof the considered method can produce. When comparing two proof methods, two outcomes are possible:

1. for every proof of a formula produced using the first method, there is a proof of comparable size of the same formula produced by the second method;
2. there exists a formula such that the first method can produce a short proof while all proofs obtained by the second method are consistently larger.

Comparison of size is done using the relationship between formula size and proof size in the asymptotic behavior, and considering a polynomial increase not to constitute a difference. These are standard assumptions in computational complexity.

See also

• Automated theorem proving
• Computational complexity

References

• P. Beame and T. Pitassi. Propositional proof complexity: past, present and future. Technical Report TR98-067, Electronic Colloquium on Computational Complexity, 1998.