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, ...


20

If SAT had a subexponential-time algorithm, the you would disprove the exponential time hypothesis. For fun consequences: if you showed that circuit SAT over AND,OR,NOT with $n$ variables and $poly(n)$ circuit gates can be solved faster than the trivial $2^n poly(n)$ approach, then by Ryan Williams' paper you show that $NEXP \not\subseteq P/poly$.


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 ...


18

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

Here's an somewhat relevant example we are currently covering in my class. The "storage access function" is defined on $2^k+k$ bits as: $SA(x_1,...,x_{2^k}, a_1,...,a_k) = x_{bin(a_1 \cdots a_k)}$ where $bin(a_1 \cdots a_k)$ is the unique integer in $\{1,\ldots,2^k\}$ corresponding to the string $a_1 \cdots a_k$. $SA$ has formulas of size about $O(k \...


14

In one of my blog posts, I mentioned four problems (Factoring, Parity Games, Stochastic Games, A Lattice Problem) that are known to be in $NP \cap coNP$ but not known to be in $P$. Parity Games and Stochastic Games can be considered as "graph problems". Also, The Two Bicliques Problem is in $NP \cap coNP$. This is a natural graph problem that is not known ...


14

On satisfiable instances of $PHP$, DPLL based SAT solvers will furnish a satisfying assignment in linear time. To see why, observe how the CNF encoding of an unsatisfiable instance of $PHP$ with $n$ holes and $n + 1$ pigeons is sintactically identical to an instance of $k = n$ Graph Coloring, where the input graph is a clique of $n + 1$ vertices. ...


14

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

This might be a slight reach, but the idea of XOR'ing a bunch of things to make a task "harder" shows up in cryptography. It first appeared in the guise of Yao's XOR lemma. If $X$ is a slightly unpredictable random variable, then $Y = X_1 \oplus X_2 \oplus \cdots \oplus X_k$ is extremely unpredictable if $k$ is large enough, where the $X_i$'s are independent ...


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

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

Clarification on terminology The theorem proving community does not use the terms supervised and unsupervised. They use the terms interactive theorem proving or automated theorem proving. If you give a conjecture to the prover and it always comes back with a yes or no answer, such a prover is a decision procedure for a logical theory or simply called a ...


11

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, \...


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, ...


10

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

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

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


9

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).


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

Your definition of $D$ is not clear, if it is $D = \max_f (R(f) - ER(f))$, then it is exponential. There are DNFs whose shortest proofs in ER is exponentially shorter than their shortest proofs in R e.g. PHP (pigeon hole principle) has polynomial size ER-proofs but only exponential size R-proofs. Unsatisfiability of $f$ is the same as $\lnot f$ being a ...


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

Pavel Pudlák has recently shown an exponential lower bound for Resolution refutations of the formulas derived from the Ramsey theorem $n\to (k)^2_2$ for $k=\lfloor \frac12 \log n \rfloor$. These formulas have clauses $\bigvee_{i,j\in K} x_{i,j}$ and $\bigvee_{i,j\in K} \neg x_{i,j}$ for every subset $K\subseteq \{ 1 , \ldots , n \}$ of size $|K| = k$, they ...


8

Another hard example for resolution is the mutilated chessboard formulas. They state that a $2n \times 2n$ chessboard with two diagonally opposite corners missing cannot be covered with $2\times 1$ tiles. See: Michael Alekhnovich. Mutilated chessboard problem is exponentially hard for resolution. Theoretical Compututer Science 310(1-3): 513-525 (2004). http:...


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

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: ...


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 ...


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 ...


7

The third approach mentioned in the linked paper refers to the framework of bounded applicative theories, which are subsystems of Feferman's theory of Explicit Mathematics just as Bounded Arithmetic theories are subsystems of Peano Arithmetic (or higher order extensions of it). These theories contain full lambda calculus (or combinatory logic rather) and ...


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