*** Welcome to piglix ***

Propositional proof system


In propositional calculus and proof complexity a propositional proof system (pps), also called a Cook–Reckhow propositional proof system, is system for proving classical propositional tautologies.

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:

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.

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.


...
Wikipedia

...