Proof complexity
   HOME

TheInfoList



OR:

In
logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
and
theoretical computer science Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory. It is difficult to circumsc ...
, and specifically
proof theory Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Jon Barwise, Barwise (1978) consists of four correspo ...
and
computational complexity theory In theoretical computer science and mathematics, computational complexity theory focuses on classifying computational problems according to their resource usage, and relating these classes to each other. A computational problem is a task solved by ...
, proof complexity is the field aiming to understand and analyse the computational resources that are required to prove or refute statements. Research in proof complexity is predominantly concerned with proving proof-length lower and upper bounds in various
propositional proof system 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 ...
s. For example, among the major challenges of proof complexity is showing that the
Frege system In 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. Frege systems (more often known as Hilbert systems in genera ...
, the usual
propositional calculus Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
, does not admit polynomial-size proofs of all tautologies. Here the size of the proof is simply the number of symbols in it, and a proof is said to be of polynomial size if it is polynomial in the size of the tautology it proves. Systematic study of proof complexity began with the work of
Stephen Cook Stephen Arthur Cook (born December 14, 1939) is an American-Canadian computer scientist and mathematician who has made significant contributions to the fields of complexity theory and proof complexity. He is a university professor at the Unive ...
and Robert Reckhow (1979) who provided the basic definition of a propositional proof system from the perspective of computational complexity. Specifically Cook and Reckhow observed that proving proof size lower bounds on stronger and stronger propositional proof systems can be viewed as a step towards separating NP from
coNP In computational complexity theory, co-NP is a complexity class. A decision problem X is a member of co-NP if and only if its complement (complexity), complement is in the complexity class NP (complexity), NP. The class can be defined as follows: ...
(and thus P from NP), since the existence of a propositional proof system that admits polynomial size proofs for all tautologies is equivalent to NP=coNP. Contemporary proof complexity research draws ideas and methods from many areas in computational complexity,
algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algorithms are used as specificat ...
s and mathematics. Since many important algorithms and algorithmic techniques can be cast as proof search algorithms for certain proof systems, proving lower bounds on proof sizes in these systems implies run-time lower bounds on the corresponding algorithms. This connects proof complexity to more applied areas such as SAT solving.
Mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
can also serve as a framework to study propositional proof sizes. First-order theories and, in particular, weak fragments of
Peano arithmetic In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
, which come under the name of
bounded arithmetic Bounded arithmetic is a collective name for a family of weak subtheories of Peano axioms, Peano arithmetic. Such theories are typically obtained by requiring that Quantifier (logic), quantifiers be bounded in the induction axiom or equivalent postul ...
, serve as uniform versions of propositional proof systems and provide further background for interpreting short propositional proofs in terms of various levels of feasible reasoning.


Proof systems

A propositional proof system 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 ''A'' is a tautology. Examples of propositional proof systems include
sequent calculus In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology i ...
,
resolution Resolution(s) may refer to: Common meanings * Resolution (debate), the statement which is debated in policy debate * Resolution (law), a written motion adopted by a deliberative body * New Year's resolution, a commitment that an individual mak ...
, cutting planes and
Frege system In 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. Frege systems (more often known as Hilbert systems in genera ...
s. Strong mathematical theories such as ZFC induce propositional proof systems as well: a proof of a tautology \tau in a propositional interpretation of ZFC is a ZFC-proof of a formalized statement '\tau is a tautology'.


Proofs of polynomial size and the NP versus coNP problem

Proof complexity measures the efficiency of the proof system usually in terms of the minimal size of proofs possible in the system for a given tautology. The size of a proof (respectively formula) is the number of symbols needed to represent the proof (respectively formula). A propositional proof system ''P'' is ''polynomially bounded'' if there exists a constant c such that every tautology of size n has a ''P''-proof of size (n+c)^c. A central question of proof complexity is to understand if tautologies admit polynomial-size proofs. Formally,
Problem (NP vs. coNP) Does there exist a polynomially bounded propositional proof system?
Cook and Reckhow (1979) observed that there exists a polynomially bounded proof system if and only if NP=coNP. Therefore, proving that specific proof systems do not admit polynomial size proofs can be seen as a partial progress towards separating NP and coNP (and thus P and NP).


Optimality and simulations between proof systems

Proof complexity compares the strength of proof systems using the notion of simulation. A proof system ''P'' ''p-simulates'' a proof system ''Q'' if there is a polynomial-time function that given a ''Q''-proof of a tautology outputs a ''P''-proof of the same tautology. If ''P'' p-simulates ''Q'' and ''Q'' p-simulates ''P'', the proof systems ''P'' and ''Q'' are ''p-equivalent''. There is also a weaker notion of simulation: a proof system ''P'' ''simulates'' a proof system ''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'', ). For example, sequent calculus is p-equivalent to (every) Frege system. A proof system is ''p-optimal'' if it ''p''-simulates all other proof systems, and it is ''optimal'' if it simulates all other proof systems. It is an open problem whether such proof systems exist:
Problem (Optimality) Does there exist a p-optimal or optimal propositional proof system?
Every propositional proof system ''P'' can be simulated by Extended Frege extended with axioms postulating soundness of ''P''. The existence of an optimal (respectively p-optimal) proof system is known to follow from the assumption that NE=coNE (respectively E= NE). For many weak proof systems it is known that they do not simulate certain stronger systems (see below). However, the question remains open if the notion of simulation is relaxed. For example, it is open whether Resolution ''effectively polynomially simulates'' Extended Frege.


Automatability of proof search

An important question in proof complexity is to understand the complexity of searching for proofs in proof systems.
Problem (Automatability) Are there efficient algorithms searching for proofs in standard proof systems such as Resolution or the Frege system?
The question can be formalized by the notion of automatability (also known as automatizability). A proof system ''P'' is ''automatable'' if there is an algorithm that given a tautology \tau outputs a ''P''-proof of \tau in time polynomial in the size of \tau and the length of the shortest ''P''-proof of \tau. Note that if a proof system is not polynomially bounded, it can still be automatable. A proof system ''P'' is ''weakly automatable'' if there is a proof system ''R'' and an algorithm that given a tautology \tau outputs an ''R''-proof of \tau in time polynomial in the size of \tau and the length of the shortest ''P''-proof of \tau. Many proof systems of interest are believed to be non-automatable. However, currently only conditional negative results are known. * Krajíček and Pudlák (1998) proved that Extended Frege is not weakly automatable unless RSA is not secure against
P/poly In computational complexity theory, P/poly is a complexity class representing problems that can be solved by small circuits. More precisely, it is the set of formal languages that have polynomial-size circuit families. It can also be defined equiva ...
. * Bonet, Pitassi and Raz (2000) proved that the TC^0-Frege system is not weakly automatable unless the Diffie–Helman scheme is not secure against P/poly. This was extended by Bonet, Domingo, Gavaldá, Maciel and Pitassi (2004) who proved that constant-depth Frege systems of depth at least 2 are not weakly automatable unless the Diffie–Helman scheme is not secure against nonuniform adversaries working in subexponential time. * Alekhnovich and Razborov (2008) proved that tree-like Resolution and Resolution are not automatable unless FPT=W This was extended by Galesi and Lauria (2010) who proved that Nullstellensatz and Polynomial Calculus are not automatable unless the fixed-parameter hierarchy collapses. Mertz, Pitassi and Wei (2019) proved that tree-like Resolution and Resolution are not automatable even in certain
quasi-polynomial time In computer science, the time complexity is the computational complexity that describes the amount of computer time it takes to run an algorithm. Time complexity is commonly estimated by counting the number of elementary operations performed by ...
assuming the
exponential time hypothesis In computational complexity theory, the exponential time hypothesis is an unproven computational hardness assumption that was formulated by . It states that satisfiability of 3-CNF Boolean formulas cannot be solved more quickly than exponential t ...
. * Atserias and Müller (2019) proved that Resolution is not automatable unless P=NP. This was extended by de Rezende, Göös, Nordström, Pitassi, Robere and Sokolov (2020) to NP-hardness of automating Nullstellensatz, Polynomial Calculus, Sherali–Adams; by Göös, Koroth, Mertz and Pitassi (2020) to NP-hardness of automating Cutting Planes; and by Garlík (2020) to NP-hardness of automating ''k''- DNF Resolution. It is not known if the weak automatability of Resolution would break any standard complexity-theoretic hardness assumptions. On the positive side, * Beame and Pitassi (1996) showed that tree-like Resolution is automatable in quasi-polynomial time and Resolution is automatable on formulas of small width in weakly subexponential time.


Bounded arithmetic

Propositional proof systems can be interpreted as nonuniform equivalents of theories of higher order. The equivalence is most often studied in the context of theories of
bounded arithmetic Bounded arithmetic is a collective name for a family of weak subtheories of Peano axioms, Peano arithmetic. Such theories are typically obtained by requiring that Quantifier (logic), quantifiers be bounded in the induction axiom or equivalent postul ...
. For example, the Extended Frege system corresponds to Cook's theory \mathrm _1 formalizing polynomial-time reasoning and the Frege system corresponds to the theory \mathrm ^1 formalizing \mathsf^1 reasoning. The correspondence was introduced by Stephen Cook (1975), who showed that coNP theorems, formally \Pi^b_1 formulas, of the theory \mathrm _1 translate to sequences of tautologies with polynomial-size proofs in Extended Frege. Moreover, Extended Frege is the weakest such system: if another proof system ''P'' has this property, then ''P'' simulates Extended Frege. An alternative translation between
second-order Second-order may refer to: Mathematics * Second order approximation, an approximation that includes quadratic terms * Second-order arithmetic, an axiomatization allowing quantification of sets of numbers * Second-order differential equation, a di ...
statements and propositional formulas given by Jeff Paris and
Alex Wilkie Alex James Wilkie FRS (born 1948 in Northampton) is a British mathematician known for his contributions to model theory and logic. Previously Reader in Mathematical Logic at the University of Oxford, he was appointed to the Fielden Chair of Pur ...
(1985) has been more practical for capturing subsystems of Extended Frege such as Frege or constant-depth Frege.
draft from 2008
While the above-mentioned correspondence says that proofs in a theory translate to sequences of short proofs in the corresponding proof system, a form of the opposite implication holds as well. It is possible to derive lower bounds on size of proofs in a proof system ''P'' by constructing suitable
model A model is an informative representation of an object, person or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin ''modulus'', a measure. Models c ...
s of a theory ''T'' corresponding to the system ''P''. This allows to prove complexity lower bounds via
model-theoretic In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the st ...
constructions, an approach known as Ajtai's method.


SAT solvers

Propositional proof systems can be interpreted as nondeterministic algorithms for recognizing tautologies. Proving a superpolynomial lower bound on a proof system ''P'' thus rules out the existence of a polynomial-time algorithm for SAT based on ''P''. For example, runs of the
DPLL algorithm In logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solvi ...
on unsatisfiable instances correspond to tree-like Resolution refutations. Therefore, exponential lower bounds for tree-like Resolution (see below) rule out the existence of efficient DPLL algorithms for SAT. Similarly, exponential Resolution lower bounds imply that SAT solvers based on Resolution, such as
CDCL In computer science, conflict-driven clause learning (CDCL) is an algorithm for solving the Boolean satisfiability problem (SAT). Given a Boolean formula, the SAT problem asks for an assignment of variables so that the entire formula evaluates to t ...
algorithms cannot solve SAT efficiently (in worst-case).


Lower bounds

Proving lower bounds on lengths of propositional proofs is generally very difficult. Nevertheless, several methods for proving lower bounds for weak proof systems have been discovered. * Haken (1985) proved an exponential lower bound for Resolution and the pigeonhole principle. * Ajtai (1988) proved a superpolynomial lower bound for the constant-depth Frege system and the pigeonhole principle. This was strengthened to an exponential lower bound by Krajíček, Pudlák and Woods and by Pitassi, Beame and Impagliazzo. Ajtai's lower bound uses the method of random restrictions, which was used also to derive AC0 lower bounds in
circuit complexity In theoretical computer science, circuit complexity is a branch of computational complexity theory in which Boolean functions are classified according to the size or depth of the Boolean circuits that compute them. A related notion is the circui ...
. * Krajíček (1994) formulated a method of feasible interpolation and later used it derive new lower bounds for Resolution and other proof systems. * Pudlák (1997) proved exponential lower bounds for cutting planes via feasible interpolation. * Ben-Sasson and Wigderson (1999) provided a proof method reducing lower bounds on size of Resolution refutations to lower bounds on width of Resolution refutations, which captured many generalizations of Haken's lower bound. It is a long-standing open problem to derive a nontrivial lower bound for the Frege system.


Feasible interpolation

Consider a tautology of the form A(x,y) \rightarrow B(y,z) . The tautology is true for every choice of y, and after fixing y the evaluation of A and B are independent because they are defined on disjoint sets of variables. This means that it is possible to define an ''interpolant'' circuit C(y), such that both A(x,y) \rightarrow C(y) and C(y) \rightarrow B(y,z) hold. The interpolant circuit decides either if A(x,y) is false or if B(y,z) is true, by only considering y. The nature of the interpolant circuit can be arbitrary. Nevertheless, it is possible to use a proof of the initial tautology A(x,y) \rightarrow B(y,z) as a hint on how to construct C. A proof systems ''P'' is said to have ''feasible interpolation'' if the interpolant C(y) is efficiently computable from any proof of the tautology A(x,y) \rightarrow B(y,z) in ''P''. The efficiency is measured with respect to the length of the proof: it is easier to compute interpolants for longer proofs, so this property seems to be anti-monotone in the strength of the proof system. The following three statements cannot be simultaneously true: (a) A(x,y) \rightarrow B(y,z) has a short proof in a some proof system; (b) such proof system has feasible interpolation; (c) the interpolant circuit solves a computationally hard problem. It is clear that (a) and (b) imply that there is a small interpolant circuit, which is in contradiction with (c). Such relation allows the conversion of proof length upper bounds into lower bounds on computations, and dually to turn efficient interpolation algorithms into lower bounds on proof length. Some proof systems such as Resolution and Cutting Planes admit feasible interpolation or its variants. Feasible interpolation can be seen as a weak form of automatability. In fact, for many proof systems, such as Extended Frege, feasible interpolation is equivalent to weak automatability. Specifically, many proof systems ''P'' are able to prove their own soundness, which is a tautology \mathrm_P(\pi,\phi,x) stating that `if \pi is a ''P''-proof of a formula \phi(x) then \phi(x) holds'. Here, \pi,\phi,x are encoded by free variables. Moreover, it is possible to generate ''P''-proofs of \mathrm_P(\pi,\phi,x) in polynomial-time given the length of \pi and \phi. Therefore, an efficient interpolant resulting from short ''P''-proofs of soundness of ''P'' would decide whether a given formula \phi admits a short ''P''-proof \pi. Such an interpolant can be used to define a proof system ''R'' witnessing that ''P'' is weakly automatable. On the other hand, weak automatability of a proof system ''P'' implies that ''P'' admits feasible interpolation. However, if a proof system ''P'' does not prove efficiently its own soundness, then it might not be weakly automatable even if it admits feasible interpolation. Many non-automatability results provide evidence against feasible interpolation in the respective systems. * Krajíček and Pudlák (1998) proved that Extended Frege does not admit feasible interpolation unless RSA is not secure against P/poly. * Bonet, Pitassi and Raz (2000) proved that the TC^0-Frege system does not admit feasible interpolation unless the Diffie–Helman scheme is not secure against P/poly. * Bonet, Domingo, Gavaldá, Maciel, Pitassi (2004) proved that constant-depth Frege systems of do not admit feasible interpolation unless the Diffie–Helman scheme is not secure against nonuniform adversaries working in subexponential time.


Non-classical logics

The idea of comparing the size of proofs can be used for any automated reasoning procedure that generates a proof. Some research has been done about the size of proofs for propositional
non-classical logic Non-classical logics (and sometimes alternative logics) are formal systems that differ in a significant way from standard logical systems such as propositional and predicate logic. There are several ways in which this is done, including by way of ...
s, in particular,
intuitionistic In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of fu ...
, modal, and
non-monotonic logic A non-monotonic logic is a formal logic whose conclusion relation is not monotonic. In other words, non-monotonic logics are devised to capture and represent defeasible inferences (cf. defeasible reasoning), i.e., a kind of inference in which rea ...
s. Hrubeš (2007–2009) proved exponential lower bounds on size of proofs in the Extended Frege system in some modal logics and in intuitionistic logic using a version of monotone feasible interpolation.


See also

*
Computational complexity In computer science, the computational complexity or simply complexity of an algorithm is the amount of resources required to run it. Particular focus is given to computation time (generally measured by the number of needed elementary operations) ...
*
Circuit complexity In theoretical computer science, circuit complexity is a branch of computational complexity theory in which Boolean functions are classified according to the size or depth of the Boolean circuits that compute them. A related notion is the circui ...
*
Communication complexity In theoretical computer science, communication complexity studies the amount of communication required to solve a problem when the input to the problem is distributed among two or more parties. The study of communication complexity was first intro ...
*
Mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
*
Proof theory Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Jon Barwise, Barwise (1978) consists of four correspo ...
*
Complexity classes In computational complexity theory, a complexity class is a set of computational problems of related resource-based complexity. The two most commonly analyzed resources are time and memory. In general, a complexity class is defined in terms of a ...
*
NP (complexity) In computational complexity theory, NP (nondeterministic polynomial time) is a complexity class used to classify decision problems. NP is the set of decision problems for which the problem instances, where the answer is "yes", have proofs ver ...
*
coNP In computational complexity theory, co-NP is a complexity class. A decision problem X is a member of co-NP if and only if its complement (complexity), complement is in the complexity class NP (complexity), NP. The class can be defined as follows: ...


References


Further reading

* *
draft from 2008
* * * Krajíček, Jan

Cambridge University Press, 2019. *{{citation , last = Pudlák , first = Pavel , editor-last = Buss , editor-first = S. R. , contribution = The lengths of proofs , doi = 10.1016/S0049-237X(98)80023-2 , location = Amsterdam , mr = 1640332 , pages = 547–637 , publisher = North-Holland , series = Studies in Logic and the Foundations of Mathematics , title = Handbook of Proof Theory , volume = 137 , year = 1998


External links




Proof complexity mailing list.
Computational complexity theory Logic in computer science Automated theorem proving