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 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 computable map whose range is exactly the 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, tautologies would have polynomially checkable certificates, implying . Conversely that equality would provide such a certificate-based system. This connects proof length to computational verification.
Articles by others on the same topic
Proof complexity is a field of computational complexity theory that studies the resources required to prove statements in formal systems. It focuses on understanding the efficiency and limitations of formal proofs, particularly in relation to various proof systems, such as propositional logic, first-order logic, and more advanced logics. Key aspects of proof complexity include: 1. **Proof Length**: One of the primary metrics in proof complexity is the length of proofs.