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 by checking its two assignments. The same method for variables may require 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.[ref]
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
Articles by others on the same topic
A **propositional proof system** is a formal system in mathematical logic that is used to establish the validity of propositional formulas. It consists of a set of rules and axioms that allow for the derivation of logical statements from other statements. The goal of such a system is to demonstrate that certain propositions can be proven true based on established truths, regardless of the specific interpretation of the involved propositions.