Propositional proof system
Encyclopedia
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.
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.
was the first propositional proof system. The general definition of a propositional proof system is due to Stephen Cook
and Robert A. Reckhow (1979).
A propositional proof system is called p-optimal if it p-simulates all other propositional proof systems, and it is optimal if it simulates all other pps. A propositional proof system P is polynomially bounded (also called super) if every tautology has a short (i.e., polynomial-size) P-proof.
If P is polynomially bounded and Q simulates P, then Q is also polynomially bounded.
The set of propositional tautologies is a coNP-complete. A propositional proof system is a certificate-verifier for membership in TAUT. Existence of a polynomially bounded propositional proof system means that there is a verifier with polynomial-size certificates, i.e., TAUT is in NP
. In fact these two statements are equivalent, i.e., there is a polynomially bounded propositional proof system if and only if the complexity classes NP
and coNP are equal.
Propositional calculus
In mathematical logic, a propositional calculus or logic is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules and axioms allows certain formulas to be derived, called theorems; which may be interpreted as true...
and proof complexity
Proof complexity
In computer science, proof complexity is a measure of efficiency of automated theorem proving methods that is based on the size of the proofs they produce. The methods for proving contradiction in propositional logic are the most analyzed...
a propositional proof system (pps), also called a Cook–Reckhow propositional proof system, is system for proving classical
Classical logic
Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...
propositional tautologies.
Mathematical definition
Formally a pps is a polynomial-time function P whose rangeRange (mathematics)
In mathematics, the range of a function refers to either the codomain or the image of the function, depending upon usage. This ambiguity is illustrated by the function f that maps real numbers to real numbers with f = x^2. Some books say that range of this function is its codomain, the set of all...
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:
- CompletenessCompletenessIn general, an object is complete if nothing needs to be added to it. This notion is made more specific in various fields.-Logical completeness:In logic, semantic completeness is the converse of soundness for formal systems...
: every propositional tautologyTautologyTautology may refer to:*Tautology , using different words to say the same thing even if the repetition does not provide clarity. Tautology also means a series of self-reinforcing statements that cannot be disproved because the statements depend on the assumption that they are already...
has a P-proof, - SoundnessSoundnessIn mathematical logic, a logical system has the soundness property if and only if its inference rules prove only formulas that are valid with respect to its semantics. In most cases, this comes down to its rules having the property of preserving truth, but this is not the case in general. The word...
: if a propositional formula has a P-proof then it is a tautology, - EfficiencyEfficiencyEfficiency in general describes the extent to which time or effort is well used for the intended task or purpose. It is often used with the specific purpose of relaying the capability of a specific application of effort to produce a specific outcome effectively with a minimum amount or quantity of...
: 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.History
Historically, Frege's propositional calculusFrege's propositional calculus
In mathematical logic Frege's propositional calculus was the first axiomatization of propositional calculus. It was invented by Gottlob Frege, who also invented predicate calculus, in 1879 as part of his second-order predicate calculus .It...
was the first propositional proof system. The general definition of a propositional proof system is due to Stephen Cook
Stephen Cook
Stephen Arthur Cook is a renowned American-Canadian computer scientist and mathematician who has made major contributions to the fields of complexity theory and proof complexity...
and Robert A. Reckhow (1979).
Relation with computational complexity theory
Propositional proof system can be compared using the notion of p-simulation. A propositional proof system P p-simulates Q (written as P ≤pQ) when there is a polynomial-time function F such that P(F(x)) = Q(x) for every x. That is, given a Q-proof x, we can find in polynomial time a P-proof of the same tautology. If P ≤pQ and Q ≤pP, the proof systems P and Q are p-equivalent. There is also a weaker notion of simulation: a pps P simulates a pps Q if there is a polynomial p such that for every Q-proof x of a tautology A, there is a P-proof y of A such that the length of y, |y| is at most p(|x|). (Some authors use the words p-simulation and simulation interchangeably for either of these two concepts, usually the latter.)A propositional proof system is called p-optimal if it p-simulates all other propositional proof systems, and it is optimal if it simulates all other pps. A propositional proof system P is polynomially bounded (also called super) if every tautology has a short (i.e., polynomial-size) P-proof.
If P is polynomially bounded and Q simulates P, then Q is also polynomially bounded.
The set of propositional tautologies is a coNP-complete. A propositional proof system is a certificate-verifier for membership in TAUT. Existence of a polynomially bounded propositional proof system means that there is a verifier with polynomial-size certificates, i.e., TAUT is in NP
NP
-Locations:* NP postcode area, Newport, United Kingdom* NP, country code for Nepal ** .np, the country code top level domain for Nepal* NP, anabbreviation for Ngee Ann Polytechnic, Singapore...
. In fact these two statements are equivalent, i.e., there is a polynomially bounded propositional proof system if and only if the complexity classes NP
NP
-Locations:* NP postcode area, Newport, United Kingdom* NP, country code for Nepal ** .np, the country code top level domain for Nepal* NP, anabbreviation for Ngee Ann Polytechnic, Singapore...
and coNP are equal.
Examples of propositional proof systems
Some examples of propositional proof systems studied are:- ResolutionResolutionResolution may refer to:* Resolution , a measure of digital audio quality* Resolution , a rule of inference used for automated theorem proving* Resolution , a written motion adopted by a deliberative body...
and various extensions of it like DPLL algorithmDPLL algorithmThe Davis–Putnam–Logemann–Loveland algorithm is a complete, backtracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem.... - Natural deductionNatural deductionIn logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning...
- Sequent calculusSequent calculusIn proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
- Frege systemFrege systemIn proof complexity, a Frege system is a propositional proof system whose proofs are sequences of formulas derived using a finite set of sound and implicationally complete inference rules...
- Extended Frege
- Polynomial calculus
- Nullstellensatz system
- Cutting-plane methodCutting-plane methodIn mathematical optimization, the cutting-plane method is an umbrella term for optimization methods which iteratively refine a feasible set or objective function by means of linear inequalities, termed cuts...
Further reading
- Samuel Buss (1998), "An introduction to proof theory", in: Handbook of Proof Theory (ed. S.R.Buss), Elsevier (1998).
- P. Pudlák (1998), "The lengths of proofs", in: Handbook of Proof Theory (ed. S.R.Buss), Elsevier, (1998).
- P. Beame and T. Pitassi (1998). Propositional proof complexity: past, present and future. Technical Report TR98-067, Electronic Colloquium on Computational Complexity.
- Nathan Segerlind (2007) "The Complexity of Propositional Proofs", Bulletin of Symbolic Logic 13(4): 417–481
- J. Krajíček (1995), Bounded Arithmetic, Propositional Logic, and Complexity Theory, Cambridge University Press.
- J. Krajíček, Proof complexity, in: Proc. 4th European congress of mathematics (ed. A. Laptev), EMS, Zurich, pp. 221–231, (2005).
- J. Krajíček, Propositional proof complexity I. and Proof complexity and arithmetic.
- Stephen Cook and Phuong Nguyen, Logical Foundations of Proof Complexity, Cambridge University Press, 2010 (draft from 2008)