In propositional calculus and proof complexity a propositional proof system (pps), also called a Cook–Reckhow propositional proof system, is a system for proving classical propositional tautologies. Mathematical definition Formally a pps is a polynomial-time function P whose range is the set of all propositional tautologies (denoted TAUT). If A is a formula, then any x such that P(x) = A is called a P-proof of A. The condition defining pps can be broken up as follows: Completeness: every propositional tautology has a P-proof, Soundness: if a propositional formula has a P-proof then it is a tautology, Efficiency: P runs in polynomial time. In general, a proof system for a language L is a polynomial-time function whose range is L. Thus, a propositional proof system is a proof system for TAUT. Sometimes the following alternative definition is considered: a pps is given as a proof-verification algorithm P(A,x) with two inputs. If P accepts the pair (A,x) we say that x is a P-proof of A. P is required to run in polynomial time, and moreover, it must hold that A has a P-proof if and only if it is a tautology. If P1 is a pps according to the first definition, then P2 defined by P2(A,x) if and only if P1(x) = A is a pps according to the second definition. Conversely, if P2 is a pps according to the second definition, then P1 defined by (P1 takes pairs as input) is a pps according to the first definition, where is a fixed tautology. Algorithmic interpretation One can view the second definition as a non-deterministic algorithm for solving membership in TAUT. This means that proving a superpolynomial proof size lower-bound for pps would rule out existence of a certain class of polynomial-time algorithms based on that pps. As an example, exponential proof size lower-bounds in resolution for the pigeon hole principle imply that any algorithm based on resolution cannot decide TAUT or SAT efficiently and will fail on pigeon hole principle tautologies. This is significant because the class of algorithms based on resolution includes most of current propositional proof search algorithms and modern industrial SAT solvers. History Historically, Frege's propositional calculus was the first propositional proof system. The general definition of a propositional proof system is due to Stephen Cook and Robert A. Reckhow (1979). Relation with computational complexity theory Propositional proof system can be compared using the notion of p-simulation.