= Proof complexity
<Proof complexity> measures resources needed to express proofs in a specified <propositional proof system>. Typical quantities include the total number of symbols, the number of inference steps and the <space complexity>[space] needed to retain intermediate formulas. A short theorem statement can require a much longer proof, and changing the allowed rules can change the required length dramatically.
For example, a <resolution> refutation of an unsatisfiable clause set derives the empty clause by resolving pairs of clauses on opposite literals. Verifying a supplied derivation is a local <computation> on its lines; searching for those lines can be much harder. A lower bound must therefore identify the proof rules and the family of clause sets to which it applies.
More generally, a <propositional proof system> can be represented by a <polynomial time>[polynomial-time] computable map whose range is exactly the <tautology>[propositional tautologies]. Every <tautology> then has a proof, and every produced formula is valid. If one such system had polynomial-length proofs for every <tautology>, <tautology>[tautologies] would have <polynomial>[polynomially] checkable certificates, implying $\mathrm{NP}=\mathrm{coNP}$. Conversely that equality would provide such a certificate-based system. This connects proof length to computational verification.
Back to article page
