21

$S^1_2$ is a theory of bounded arithmetic, that is, a weak axiomatic theory obtained by severely restricting the schema of induction of Peano arithmetic. It is one of the theories defined by Sam Buss in his thesis, other general references include Chapter V of Hájek and Pudlák’s Metamathematics of first-order arithmetic, Krajíček’s “Bounded arithmetic, ...


19

The most natural restriction on the proof DAG is that it be a tree – that is, any "lemma" (intermediate conclusion) is not used more than once. This property is called being "tree-like". General resolution is exponentially more powerful than tree-like resolution, as shown for example by Ben-Sasson, Impagliazzo and Wigderson. The concept has also been ...


19

The basic sum-of-squares proof system, introduced under the name of Positivstellensatz refutations by Grigoriev and Vorobjov, is a “static” proof system for showing that a set of polynomial equations and inequations $$S=\{f_1=0,\dots,f_k=0,h_1\ge0,\dots,h_m\ge0\},$$ where $f_1,\dots,f_k,h_1,\dots,h_m\in\mathbb R[x_1,\dots,x_n]$, has no common solution in $\...


15

This is the same idea as Andrej's answer but with more details. Krajicek and Pudlak [LNCS 960, 1995, pp. 210-220] have shown that if $P(x)$ is a $\Sigma^b_1$-property that defines primes in the standard model and $$S^1_2 \vdash \lnot P(x) \to (\exists y_1,y_2)(1 < y_1, y_2 < x \land x = y_1y_2)$$ then there is a polynomial time factoring algorithm. ...


14

The following example comes from the paper which gives a combinatorial characterization of resolution width by Atserias and Dalmau (Journal, ECCC, author's copy). Theorem 2 of the paper states that, given a CNF formula $F$, resolution refutations of width at most $k$ for $F$ are equivalent to winning strategies for Spoiler in the existential $(k+1)$-pebble ...


13

1) The only non-structural rule is resolution (on atoms). $$ \varphi\lor C, \psi\lor \overline{C} \over \varphi\lor \psi$$ However a rule by itself doesn't give a proof system. See part 3. 2) Think about it this way: is Gentzen's sequent calculus PK complete if we are using some other set of connectives in place of $\{\land, \lor, \lnot\}$? The logical ...


13

1, 2, 4) The best known lower bounds on extended Frege are the same as for Frege: linear number of lines, and quadratic size. This applies e.g. to the tautologies $\neg^{2n}\top$ (basically, any tautology that is not a substitution instance of a shorter tautology, and whose sum of lengths of all subformulas is quadratic). This is proved in Krajíček’s Bounded ...


12

SOS can be considered as a proof system where lines are of the form $p(\vec{x}) \geq 0$ where $p(\vec{x})$ is a polynomial in variables $\vec{x}$. The inference rules are: $\over x^2-x \geq 0$ $\over x-x^2 \geq 0$ $\over p(\vec{x})^2\geq 0$ $p(\vec{x}) \geq 0 \over p(\vec{x})x \geq 0$ $p(\vec{x}) \geq 0 \over p(\vec{x})(1-x) \geq 0$ $p_1(\vec{x}) \geq 0, \...


12

It depends on what kind of a "beginner" level you wish to have. I don't think there is a real good undergraduate level text on proof complexity (this is probably true for most specialized sub-areas in complexity). But for a beginner (graduate level) sources, I would recommend, something like understanding well the basic exponential size lower bound on ...


11

This example is a bit lower in the hierarchy than what Kaveh asks for, but it is an open problem whether the soundness of the uniform $\mathrm{TC}^0$ algorithms for integer division and iterated multiplication by Hesse, Allender, and Barrington can be proved in the corresponding theory $\mathit{VTC}^0$. The argument is pretty elementary, and there should be ...


10

How about the edge coloring number in a dense graph (aka Chromatic index)? You are given the adjacency matrix of an $n$ vertex graph ($n^2$ bit input), but the natural witness describing the coloring has size $n^2\log n$. Of course, there might be shorter proofs for class 1 graphs in Vizing's theorem. See also this possibly related question


10

It sounds like you are interested in all-different constraints (and your last sentence is on the right track). These are non-trivial instances of the pigeonhole principle, where the number of pigeons is not necessarily greater than the number of holes, and in addition some pigeons may be barred from some of the holes. All-different constraints can be ...


10

The AKS primality test seems like a good candidate if Wikipedia is to be believed. However, I would expect such an example to be hard to find. Existing proofs are going to be phrased so that they are obviously not done in bounded arithmetic, but they will likely be "adaptable" to bounded arithmetic with more or less effort (usually more).


10

What proof system is being considered when discussing resolution? Is it just the resolution rule? What are the other rules? I discuss resolution in the context of "clauses", which are sequents made up of only literals. A classical clause would look like $$A_1,\ldots,A_n \to B_1,\ldots,B_m$$ But we can also write it as $${} \to \bar{A}_1,\ldots,\bar{A}_n, ...


9

Natural examples of propositional proof systems that do not fall under this definition are algebraic proof systems where the lines in the proof are arbitrary polynomials (not necessarily fully expanded). To verify the correctness of such proofs, among other things one has to test the identity of polynomials, which is not known to be possible in deterministic ...


8

Think of $\Sigma^{*}$ encoding some sort of objects, and $Q$ as the set of all objects satisfying some property. Think of $P$ as a function which accepts (the encoding of) a pair $(x, p)$ where $x$ is an object and $p$ is alleged "evidence" of $x \in Q$. The function $P$ is a "proof checker": it verifies that $p$ actually represents valid evidence that $x \...


8

It is over two years since this question was asked, but in that time, there have been more papers published about algorithms for computing Craig interpolants. This is a very active research area and it is not feasible to give a comprehensive list here. I have chosen articles rather arbitrarily below. I would suggest following articles that reference them and ...


8

Müller and Szeider study Resolution proofs where the proof DAG has bounded tree-width or bounded path-width (for suitable extensions of these graph complexity measures to directed graphs.) They show that the path-width of the DAG is essentially the same as the space complexity of the proof, and define a generalized notion of proof space which is equivalent ...


8

I came along some quite natural NP-complete problems that seemingly require long witnesses. The problems, parameterized by integers $C$ and $D$ are as follows: Input: A one-tape TM $M$ Question: Is there some $n\in\mathbb{N}$, such that $M$ makes more than $Cn+D$ steps on some input of length $n$? Sometimes the complement of the problem is easier to state: ...


7

Here is an example, which appears a natural problem. Instance: Positive integers, $d_1,\ldots,d_n$ and $k$, all bounded from above by $n$. Question: Does there exist a $k$-colorable graph with degree sequence $d_1,\ldots,d_n$ ? Here the input can be described with $O(n\log n)$ bits, but the witness may require $\Omega(n^2)$ bits. Remark: I do not have ...


7

Let $m$ be the number of pigeons and $n$ be the number of holes. Let the propositional variables $B_{i,0}$ ... $B_{i,log(n)}$ encode the binary representation of $j-1$ if the $i$th pigeon is put into the $j$th hole. (Example, if pigeon 1 were placed in hole 10, $j - 1 = 9$, which is binary 1001. So $B_{1,3}$ = true, $B_{1,2}$ = false, $B_{1,1}$ = false and ...


6

I find these introductory lecture notes easy to read: Paul Beame's IAS Lectures


6

For the more algebraic side of proof complexity I recommend starting with Pitassi's 1996 survey paper: T. Pitassi. Algebraic propositional proof systems, in DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Volume 31, Descriptive Complexity and Finite Models, Immerman and Kolaitis (Eds.), pp. 215-244, 1996. For a quick overview you ...


6

For strong enough proof systems the graph representation of a proof in the system seems less consequential, since (as Joshua Grochow already commented), DAG-like and tree-like Frege proofs are polynomially equivalent (see Krajicek's 1995 monograph for a proof of this fact). For weaker proof systems such as resolution, tree-like is exponentially weaker than ...


6

Maybe this is a silly "reason/explanation", but for many NP-Complete problems, a solution is a subset of the input (knapsack, vertex cover, clique, dominating set, independent set, max cut, subset sum, ...) or a permutation of or assignment to a subset of the input (Hamiltonian path, traveling salesman, SAT, graph isomorphism, graph coloring, ...). We could ...


6

$f$ is not a prover, it's a proof-checker. $w$ is the proof. And the polynomial is a polynomial of the length of the proof, which could be much larger than the length of the thing being proved. If you have a proof system for which checking whether something really is a proof (or figuring out what it's a proof of) takes more than polynomial time, then your ...


6

Cook-Reckhow propositional proof systems are nonunifrom. E.g. the computational complexity counterpart to the class of polynomial-size $\mathsf{Extended Frege}$ proofs is the nonuniform complexity class $\mathsf{P/poly}$. We have to look at their uniform counterparts: E.g. the proof complexity counterpart for $\mathsf{P}$ are bounded arithmetic theories ...


6

First, ER p-simulates SR: for example, ER is p-equivalent to the extended Frege proof system (EF) which is p-equivalent to the substitution Frege proof system (SF), and it is easy to see that SF p-simulates SR (the symmetry rule amounts to substitution of a special kind). On the other hand, Urquhart [1] proves an exponential lower bound on SR refutations of ...


6

With the caveat that I am posting this quickly in a sleep-deprived state, I think the answer is "no" to all three questions. Take the pigeonhole principle formulas PHP^m_n for m pigeons and n holes. The miniminal length of a resolution refutation for m = n+1 is exp(Omega(n)) by Haken. However, Buss and Pitassi proved that for m = exp(\sqrt(n log n)) pigeons ...


6

For each of these proof systems we know that there are some formulas where the shortest proof needs to have exponential length. Some of the earliest examples are an exponential lower bound for the pigeonhole principle in polynomial calculus (Razborov '98, IPS '99), and an exponential lower bound for the clique-colouring formula in cutting planes (Pudlák '99)....


Only top voted, non community-wiki answers of a minimum length are eligible