= Propositional proof system
A <propositional proof system> specifies efficiently checkable certificates for <logical tautologies>. In the functional formulation, it is a polynomial-time computable surjection from finite <binary strings> onto the encoded tautologies: the input is a proof and the output is the formula proved. Soundness means no false formula is output; completeness means every <logical tautology> has some proof.
For example, a <truth table> can certify $p\lor\neg p$ by checking its two assignments. The same method for $n$ variables may require $2^n$ rows, so efficient verification in the proof's length does not imply short proofs in the formula's length. <Proof complexity> asks which formulas require long certificates in particular systems. Searching for a proof and checking a supplied proof are different computational tasks.<The Relative Efficiency of Propositional Proof Systems by Stephen Cook and Robert A. Reckhow>[§1, Definition 1.3 and pp.38–39, proof-system encoding]{ref}
Back to article page
