On Interpolation and Automatization for Frege Systems.
The interpolation method has been one of the main tools for proving lower bounds for propositional proof systems. Loosely speaking, if one can prove that a particular proof system has the  feasible interpolation property, then a generic reduction can (usually) be applied to prove lower bounds for the proof system, sometimes assuming a (usually modest) complexity-theoretic assumption. In this paper, we show that this method  cannot be used to obtain lower bounds for Frege systems, or even for TC0-Frege systems. More specifically, we show that unless factoring (of Blum integers) is feasible, neither Frege nor TC0-Frege has the feasible interpolation property. In order to carry out our argument, we show how to carry out proofs of many elementary axioms/theorems of arithmetic in polynomial-sized TC0-Frege.As a corollary, we obtain that TC0-Frege, as well as any proof system that polynomially simulates it, is not automatizable (under the assumption that factoring of Blum integers is hard). We also show under the same hardness assumption that the k-provability problem for Frege systems is hard.
Introduction
One of the most important questions in propositional proof complexity is to show that there is a
family of propositional tautologies requiring superpolynomial size proofs in a Frege or Extended
Frege proof system. The problem is still open, and it is thus a very important question to
understand which techniques can be applied to prove lower bounds for these systems, as well
as for weaker systems. In recent years, the interpolation method has been one of the most
promising approaches for proving lower bounds for propositional proof systems and for bounded
arithmetic. Here we show that this method is not likely to work for Frege systems and some
weaker systems. The basic idea behind the interpolation method is as follows.
Department of LSI, Universidad Polit'ecnica de Catalu~na, Barcelona, Spain, bonet@lsi.upc.es. Research
partly supported by EU HCM network console, by ESPRIT LTR Project no. 20244 (ALCOM-IT), CICYT
TIC98-0410-C02-01 and TIC98-0410-C02-01
y Department of Computer Science, University of Arizona, toni@cs.arizona.edu. Research supported by NSF
Grant CCR-9457782, US-Israel BSF Grant 95-00238, and Grant INT-9600919/ME-103 from NSF and M - SMT
(Czech Republic)
z Department of Applied Math, Weizmann Institute, ranraz@wisdom.weizmann.ac.il. Research supported by
US-Israel BSF Grant 95-00238
We begin with an unsatisfiable statement of the form F (x;
z denotes a vector of shared variables, and x and y are vectors of private variables for formulas
A 0 and A 1 respectively. Since F is unsatisfiable, it follows that for any truth assignment ff
to z , either A 0 (x; ff) is unsatisfiable or A 1 (y; ff) is unsatisfiable. An interpolation function
associated with F is a boolean function that takes such an assignment ff as input, and outputs
only if A 0 is unsatisfiable, and 1 only if A 1 is unsatisfiable. (Note that both A 0 and A 1 can
be unsatisfiable in which case either answer will suffice).
How hard is it to compute an interpolation function for a given unsatisfiable statement F
as above ? It has been shown, among other things, that interpolation functions are not always
computable in polynomial time unless Nevertheless, it is
possible that such a procedure exists for some special cases. In particular, a very interesting
and fruitful question is whether one can find (or whether there exists) a polynomial size circuit
for an interpolation function, in the case where F has a short refutation in some proof system
S . We say that a proof system S admits feasible interpolation if whenever S has a polynomial
size refutation of a formula F (as above), an interpolation function associated with F has
a polynomial size circuit. Kraj'i-cek [K2] was the first to make the connection between proof
systems having feasible interpolation and circuit complexity.
There is also a monotone version of the interpolation idea. Namely, for conjunctive normal
monotone if the variables of z occur only
positively in A 1 and only negatively in A 0 . In this case, an associated interpolant function
is monotone, and we are thus interested in finding a polynomial size monotone circuit for an
interpolant function. We say that a proof system S admits monotone feasible interpolation
if whenever S has a polynomial size refutation of a monotone F , a monotone interpolation
function associated with F has a monotone polynomial size circuit.
Beautiful connections exist between circuit complexity, and proof systems having feasible
interpolation, in both (monotone and non-monotone) cases:
In the monotone case, superpolynomial lower bounds can be proven for a (sufficiently
strong) proof system that admits feasible interpolation. This was presented by the sequence of
papers [IPU, BPR, K1], and was first used in [BPR] to prove lower bounds for propositional
proof systems. (The idea is also implicit in [Razb2]).
In short, the statement F that is used is the Clique interpolation formula, A 0 (g; x)-A 1 (g; y) ,
where A 0 states that g is a graph containing a clique of size k (where the clique is described
by the x variables), and A 1 states that g is a graph that can be colored with
(where the coloring is described by the y variables). By the pigeonhole principle, this formula
is unsatisfiable. However, an associated monotone interpolation function would take as input
a graph g , and distinguish between graphs containing cliques of size k from those that can be
colored with , such a circuit is of exponential
size. Thus, exponential lower bounds follow for any propositional proof system S that admits
feasible monotone interpolation.
Similar ideas also work in the case where S admits feasible interpolation (but not necessarily
monotone feasible interpolation). The first such result, by [Razb2], gives explicit superpolynomial
lower bounds for (sufficiently strong) proof systems S admitting feasible interpolation,
under a cryptographic assumption. In particular, it was shown that a (non-monotone)
interpolation function, associated with a certain statement expressing P 6= NP , is computable
by polynomial size circuits only if there do not exist pseudorandom number generators.
Therefore, lower bounds follow for any (sufficiently strong) propositional proof system that
admits feasible interpolation (conditional on the cryptographic assumption that there exist
pseudorandom number generators). It is also possible to prove nonexplicit superpolynomial
lower bounds for a (sufficiently strong) proof system under the assumption that NP is not
computable by polynomial sized circuits.
Many researchers have used these ideas to prove lower bounds for propositional proof
systems. In particular, in the last five years, lower bounds have been shown for all of
the following systems using the interpolation method: Resolution [BPR], Cutting Planes
[IPU, BPR, Pud, CH], generalizations of Cutting Planes [BPR, K1, K3], relativized bounded
arithmetic [Razb2], Hilbert's Nullstellensatz [PS], the polynomial calculus [PS], and the Lovasz-
Schriver proof system [Pud3].
1.1 Automatizability and k-provability
As explained in the previous paragraphs, the existence of feasible interpolation for a particular
proof system S gives rise to lower bounds for S . Feasible interpolation, moreover, is a very
important paradigm for proof complexity (in general) for several other reasons. In this section,
we wish to explain how the lack of feasible interpolation for a particular proof system S implies
that S is not automatizable.
We say that a proof system S is automatizable if there exists a deterministic procedure
D that takes as input a formula f and returns an S -refutation of f (if one exists) in time
polynomial in the size of the shortest S -refutation of f . Automatizability is a crucial concept
for automated theorem proving: in proof complexity we are mostly interested in the length of
the shortest proof, whereas in theorem proving it is also essential to be able to find the proof.
While there are seemingly powerful systems for the propositional calculus (such as Extended
Resolution or even ZFC), they are scarce in theorem proving because it seems difficult to search
efficiently for a short proof in such systems. In other words, there seems to be a tradeoff
between proof simplicity and automatizability - the simpler the proof system, the easier it is to
find the proof.
In this section, we formalize this tradeoff in a certain sense. In particular, we show that if
S has no feasible interpolation then S is not automatizable. This was first observed by Russell
Impagliazzo. The idea is to show that if S is automatizable (using a deterministic procedure
D ), then S has feasible interpolation.
Theorem 1 If a proof system S does not have feasible interpolation, then S is not automatiz-
able.
Proof Suppose that S is automatizable, and suppose D is the deterministic procedure to find
proofs, and moreover, D is guaranteed to run in time n c , where n is the size of the shortest
proof of the input formula. Let A 0 (x; z) - A 1 (y; z) be the interpolant statement, and let ff
be an assignment to z . We want to output an interpolant function for A 0 (x; ff) - A 1 (y; ff) .
First, we run D on A 0 (x; z) - A 1 (y; z) to obtain a refutation of size s . Next, we simulate D
on A 0 (x; ff) for T (s) steps, and return 0 if and only if D produces a refutation of A 0 (x; ff)
will be chosen to be the maximum time for D to produce a refutation
for a formula that has a refutation of size s ; thus T c in this case. This works because
in the case where A 1 (y; ff) is satisfiable with satisfying assignment fl , we can plug fl into the
refutation of A 0 (x; ff) - A 1 (y; ff) to obtain a refutation of A 0 (x; ff) of size s . Therefore S has
feasible interpolation. ut
Thus, feasible interpolation is a simple measure that formalizes the complexity/search trade-
off: the existence of feasible interpolation implies superpolynomial lower bounds (sometimes
modulo complexity assumptions), whereas the nonexistence of feasible interpolation implies
that the proof system cannot be automatized.
A concept that is very closely related to automatizability is k-provablity. The k-symbol
provability problem for a particular Frege system S is as follows. The problem is to determine,
given a propositional formula f and a number k , whether or not there is a k-symbol S proof
of f . The k -line provability problem for S is to determine whether or not there is a k -line
S proof of f . The k -line provability is an undecidable problem for first-order logic [B1]; and
the first complexity result for the k-provability problem for propositional logic was provided
by Buss [B2] who proved the rather surprising fact that the k-symbol propositional provability
problem is NP -complete for a particular Frege system. More recently, [ABMP] show that the
k-symbol and k -line provability problems cannot be approximated to within linear factors for
a variety of propositional proof systems, including Resolution and all Frege systems, unless
The methods in our paper show that both the k-symbol and k -line provability problems
cannot be solved in polynomial time for any TC 0 -Frege system, Frege system, or Extended Frege
system, assuming hardness of factoring (of Blum integers). More precisely, using the same idea
as above, we can show that if there is a polynomial time algorithm A solving the k-provability
problem for S , then S has feasible interpolation: Suppose that is the
unsatisfiable statement. We first run A with first verifies that
there is a size proof of F for some fixed value of c . Now let ff be an assignment
to z . As above, we run A to determine if there is an O(s)-symbol (or O(s)-line) refutation
of A 0 (x; ff) and return 0 if and only if A accepts. In fact, this proof can be extended easily
to show that both the k-symbol and k -line provability problems cannot be approximated to
within polynomial factors for the same proof systems (TC 0 -Frege, Frege, Extende Frege) under
the same hardness assumption.
1.2 Interpolation and one way functions
How can one prove that a certain propositional proof system S does not admit feasible
interpolation ? One idea, due to Kraj'i-cek and Pudl'ak [KP], is to use one way permutations in
the following way. Let h be a one way permutation and let A 0 (x; z); A 1 (y; z) be the following
formulas.
The formula A
th bit of x is 0.
The formula
th bit of y is 1.
Since h is one to one, A 0 (x; z) - A 1 (y; z) is unsatisfiable. Assume that A 0 ; A 1 can be
formulated in the proof system S , and that in S there exists a polynomial size refutation for
A 0 (x; z) -A 1 (y; z) . Then, if S admits feasible interpolation it follows that given an assignment
ff to z there exists a polynomial size circuit that decides whether A 0 (x; ff) is unsatisfiable or
A 1 (y; ff) is unsatisfiable. Obviously, such a circuit breaks the i th bit of the input for h . Since
can be constructed for any i , all bits of the input for h can be broken. Hence, assuming
that the input for h is secure, and that in the proof system S there exists a polynomial size
refutation for A 0 - A 1 , it follows that S does not admit feasible interpolation.
A major step towards the understanding of feasible interpolation was made by Kraj'i-cek
and Pudl'ak [KP]. They considered formulas A 0 ; A 1 based on the RSA cryptographic scheme,
and showed that unless RSA is not secure, Extended Frege systems do not have feasible
interpolation. It has been open, however, whether or not the same negative results hold for
Frege systems, and for weaker systems such as bounded depth threshold logic or bounded depth
Frege.
1.3 Our results
In this paper, we prove that Frege systems, as well as constant-depth threshold logic (referred
to below as do not admit feasible interpolation, unless factoring of Blum integers
is computable by polynomial size circuits. (Recall that Blum integers are integers P of the
are both primes such that p 1 mod
our result significantly extends [KP] to weaker proof systems. In addition, our cryptographic
assumption is weaker.
To prove our result, we use a variation of the ideas of [KP]. In a conversation with Moni
Naor, he observed that the cryptographic primitive needed here is not a one way permutation
as in [KP], but the more general structure of bit commitment. Our formulas A 0 ; A 1 are based
on the Diffie-Hellman secret key exchange scheme [DH]. For simplicity, we state the formulas
only for the least significant bit. (Our argument works for any bit).
Informally, our propositional statement DH will be
The common variables are two integers X;Y , and P and g . P represents a number (not
necessarily a prime) of length n , and g an element of the group Z
. The private variables for
A 0 are integers a; b , and the private variables for A 1 are integers c; d .
Informally, A 0 say that g a mod that
ab mod P is even. Similarly, A 1 d) will say that
and g cd mod P is odd. The statement A 0 - A 1 is unsatisfiable since (informally) if A 0 ; A 1 are
both true we have
ab mod
We will show that the above informal proof can be made formal with a (polynomial size)
proof. On the other hand, an interpolant function computes one bit of the
secret key exchanged by the Diffie-Hellman procedure. Thus, if TC 0 -Frege admits feasible
interpolation, then all bits of the secret key exchanged by the Diffie-Hellman procedure can be
broken using polynomial size circuits, and hence the Diffie-Hellman cryptographic scheme is not
secure. Note, that it was proved that for are both primes such that
breaking the Diffie-Hellman cryptographic
scheme is harder than factoring P ! [BBR] (see also [Sh, Mc]).
It will require quite a bit of work to formalize the above statement and argument with a
short proof. Notice that we want the size of the propositional formula expressing the
Diffie Hellman statement to be polynomially bounded in the number of binary variables. And
additionally, we want the size of the proof of the statement to also be polynomially
bounded. A key idea in order to define the statement and prove it efficiently, is to introduce
additional common variables to our propositional Diffie-Hellman statement. The bulk of the
argument then involves showing how (with the aid of the auxillary variables) one can formalize
the above proof by showing that basic arithmetic facts, including the Chinese Remainder
Theorem, can be stated and proven efficiently within
1.4 Section description
The paper is organized as follows. In Section 2, we define our system. In Section
3, we define the used for the proof. In Section 4, we define precisely the
interpolation formulas which are based on the Diffie-Hellman cryptographic scheme. In Section
5 we show how to prove our main theorem, provided we have some technical lemmas that will
be proved fully in section 7. In Section 6 there is a discussion and some open problems. Finally
in section 7 we prove all the technical lemmas required for the main theorem.
The unusual organization of the paper is due to the many very technical lemmas required
to show the result, that are essential to the correctness of the argument, but not every reader
might want to go through. Sections 1-6 give an exposition of the result, relying on the complete
proofs in the technical part.
systems
For clarity, we will work with a specific bounded-depth threshold logic system, that we call
reasonable definition of such a system should also suffice. Our system
is a sequent-calculus logical system where formulas are built up using the connectives - ,
only if the number of 1's in x is at least k , and
\Phi i (x) is true if and only if the number of 1's in x is i mod 2.)
Our system is essentially the one introduced in [MP]. (Which is, in turn, an extension of
the system PTK introduced by Buss and Clote [BC, Section 10].)
Intuitively, a family of formulas f each
formula has a proof of size polynomial in the size of the formula, and such that every line in the
proof is a
are built up using the connectives -, Th k , \Phi 1 , \Phi 0 , :. All
connectives are assumed to have unbounded fan-in. Th k interpreted to be true if
and only if the number of true A i 's is at least k ; \Phi j interpreted to be true if and
only if the number of true A i 's is equal to j mod 2.
The formula denotes the logical AND of the multi-set consisting of A
and similarly for - , \Phi j and Th k . Thus commutativity of the connectives is implicit. Our proof
system operates on sequents which are sets of formulas of the form A
The intended meaning is that the conjunction of the A i 's implies the disjunction of the B j 's.
A proof of a sequent S in our logic system is a sequence of sequents, S 1 ; :::; S q , such that each
sequent S i is either an initial sequent, or follows from previous sequents by one of the rules of
inference, and the final sequent, S q , is S . The size of the proof is
its depth
is
The initial sequents are of the form: (1) A ! A where A is any formula; (2)
. The
rules of inference are as follows. Note that the logical rules are defined for n - 1 and k - 1 .
First we have simple structural rules such as weakening (formulas can always be added to the
left or to the right), contraction (two copies of the same formula can be replaced by one), and
permutation (formulas in a sequent can be reordered). The remaining rules are the cut rule,
and logical rules which allow us to introduce each connective on both the left side and the right
side. The cut rule allows the derivation of \Gamma;
The logical rules are as follows.
1. , we can derive
2. (Negation-right) From
3. (And-left) From A 1 ;
4. (And-right) From
5. (Or-left) From A
6.
7. (Mod-left) From A 1 ; \Phi 1\Gammai derive
8. (Mod-right) From A derive
9. (Threshold-left) From Th k
derive
derive
A proof is a bounded-depth proof in our system of polynomial size. More formally we
have the following definitions.
Ng be a family of sequents. Then fR
family of TC 0 proofs for F if there exist constants c and d such that the following conditions
hold: (1) Each R n is a valid proof of (\Gamma our system, and 2) For all i, the depth of
R n is at most d; and (3) For all n, the size of R n is at most
We note that we have defined a specific proof system for clarity; our result still holds for
any reasonable definition of a proof (it can be shown that our system polynomially
simulates any Frege-style system). The difference between a polynomial size proof in our system
and a polynomial size TC 0 proof is similar to the difference between NC 1 and TC 0 .
3 The
In this section we will describe some of the needed to formulate and to refute the
Diffie-Hellman formula. For simplicity of the description, let us assume that we have a fixed
number N which is an upper bound for the length of all numbers used in the refutation of
the Diffie-Hellman formula. The number N will be used to define some of the formulas below.
After seeing the statement and the refutation of the Diffie-Hellman formula, it will be clear that
it is enough to take N to be a small polynomial in the length of the number P used for the
Diffie-Hellman formula.
3.1 Addition and subtraction
We will use the usual carry-save AC 0 -formulas to add two n-bit numbers. Let
be two numbers. Then x denote the following AC 0 -formula: There will
be . The bit z i will equal the mod 2 sum of C i , x i and y i , where
C i is the carry bit. Intuitively, C i is 1 if there is some bit position less than i that generates
a carry that is propagated by all later bit positions until bit i . Formally, C i is computed
by OR(R
th bit position generates a carry, and P k is 1 if the k th bit
position propagates but does not generate a carry.)
As for subtraction, let us show how to compute z . Think of x; y as N -bit numbers.
y is the complement (modulo 2) of
the N bits of y , and x is the complement of the N bits of x . Denote
note that s is equal to 2 N similarly t is equal to 2 N
we know that x \Gamma y - 0 and thus we know that y
and thus . Thus, for any i , we can compute z i by (s N+1 - s i
3.2 Iterated addition
We will now describe the inputs m numbers, each n bits
long, and outputs their sum x 1 We assume that m - N . The
main idea is to reduce the addition of m numbers to the addition of two numbers. Let x i
be x i;n ; :::; x i;1 (in binary representation). Let l = dlog 2 Ne . Let
2l
, and assume (for
simplicity) that r is an integer.
Divide each x i into r blocks where each block has 2l bits, and let S i;k be the number in
the k th block of x i . That is,
2l
Now, each S i;k has 2l bits. Let L i;k be the low-order half of S i;k and let H i;k be the high order
half. That is, S
Denote
r
r
Then,
r
r
r
Hence, we just have to show how to compute the numbers H;L . Let us show how to compute
L , the computation of H is similar.
Denote
r
Since each L i;k is of length l , each L k is of length at most l which is at most 2l .
Hence, the bits of L are just the bits of the L k 's combined. That is,
As for the computation of the L k 's, note that since each L k is a poly-size sum of logarithmic
length numbers, it can be computed using poly-size threshold gates.
3.3 Modular arithmetic
Next, we describe our that compute the quotient and remainder of a number
z modulo p , where z is of length n . remainder and The inputs for the remainder and the
quotient formulas are as follows:
1. the number z ;
2. numbers
3. numbers k i and r i for all 1 - i - n .
The intended values for the variables k i and r i are such that 2
(for all 1 - i - n). The intended values for the variables p i are i \Delta p .
Suppose that z assume that the input variables k i , r i and
take the right values. Then our formula [z] p will output r , and our formula div p (z) will
output k . The formulas are computed as follows.
Suppose that the k i , r i and p i variables satisfy
(p
l be such that l \Delta
and can therefore be computed by
div p (z) is computed by SUM n
Notice that if the k i , r i and p i 's are not such that 2
then the formulas are not required to compute the correct values of the quotient or remainder,
and can give junk.
3.4 Product and iterated product
We will write x \Delta y to denote the formula SUM i;j [2 i+j \Gamma2 x computing the product of two
n-bit numbers x and y . By 2 i+j \Gamma2 x i y j we mean 2 i+j \Gamma2 if both x i and y j are true, and 0
otherwise.
Lastly, we will describe our computing the iterated product of m numbers.
This formula is basically the original formula of [BCH], and articulated as a TC 0 -formula in
[M].
The iterative product, PROD[z gives the product of z 1 ; :::; z m , where each z i is of
length n , and we assume that m;n are both bounded by N . The basic idea is to compute the
product modulo small primes using iterated addition, and then to use the constructive Chinese
Remainder Theorem to construct the actual product from the product modulo small primes.
Let Q be the product of the first t primes is the first integer that gives a
number Q of length larger than N 2 . Since q 1 ; :::; q t are all larger than 2, t is at most N 2 , and
by the well known bounds for the distribution of prime numbers the length of each q j is at most
O(log N) . For each q j , let g j be a fixed generator for Z
. Also, for each q j , let u j - Q be a
fixed number with the property that u j mod q (such a
number exists by the Chinese Remainder Theorem). PROD[z computed as follows.
1. First we compute r
, for all . This is calculated using the modular arithmetic
described earlier.
2. For each 1 -
a. Compute a ij such that (g a ij
. This is done by a table lookup.
b. Calculate c
c. Compute r j such that g c j
. This is another table lookup.
3. Finally compute
We will hardwire the values . Thus, this computation is obtained by
doing a table lookup to compute followed by an iterated sum followed by a mod Q
calculation.
3.5 Equality, and inequality
Often we will write are both vectors of variables or formulas:
When we
We apply the same conventions when writing 6=; !; - .
4 The Diffie-Hellman Formula
We are now ready to formally define our propositional statement DH . DH will be the
conjunction of A 0 and A 1 . The common variables for the formulas will be:
a) P and g representing n-bit integers, and for every i - 2n , we will also add common
variables for g 2 i
mod P .
b) X;Y , and for every i - 2n , we will also add common variables for X 2 i
mod P , and for
mod P .
c) We also add variables for P These variables
are needed to define arithmetic modulo P (see section 3.3).
For the following: the common
variable
mod
mod
. The
will be the conjunction of the following
1.
(Which means g a mod
2. For every j - n ,
mod P:
(Which means (g 2 j
modP .) Note that from this it is easy to prove for
3. Similar formulas for g b mod
mod P .
4. PROD i;j
is even. (Which means g ab mod P is even.)
5. For every i - N , formulas expressing
formulas are added to guarantee that the modulo P arithmetic is computed correctly).
Similarly, the formula A 1 d) will be the conjunction of the above formulas, but
with a replaced by c , b replaced by d , and the fourth item stating that g cd mod P is odd.
Note that the definition of the iterated product (PROD ) requires the primes q 1 ; :::; q t (as
well as their product Q , and the numbers u are fixed for the length n . So we
are going to hardwire the numbers q well as the correct values for the r i 's
and k i 's needed for the modulo q j arithmetic, for each one of these numbers.
refutation for DH
We want to describe a refutation for DH . As mentioned above the proof proceeds
as follows.
1. Using A 0 , show that g ab mod
2. Using A 1 , show that X b mod
3. Show that g cb mod
4. Using A 0 , show that g bc mod
5. Using A 1 , show that Y c mod
6. Show that g dc mod
We can conclude from the above steps that A 0 and A 1 imply that g ab mod
but now we can reach a contradiction since A 0 states that g ab mod P is even, while A 1 states
that g cd mod P is odd.
We formulate g ab mod P as
PROD i;j
and X b mod P as
Thus, step 1 is formulated as
PROD i;j
and so on.
Steps 1,2,4,5 are all virtually identical. Steps 3 and 6 follow easily because our formulas
defining g ab make symmetry obvious. Thus the key step is to show step 1; that is, to show how
to prove g ab mod As mentioned above, this is formulated as follows.
PROD i;j
We will build up to the proof that g ab mod P equals X b mod P by proving many lemmas
concerning our basic -formulas. The final lemma that we need is the following:
Lemma 4 For every z 1;1 ; :::; z m;m 0 and p, there are TC 0 -Frege proofs of
The proof of the lemma is given in section 7.
Using Lemma 4 for the first equality, and point 2 from section 4 for the second equality, we
can now obtain:
PROD i;j
which proves step 1.
The main goal of Section 7 is hence to show that the statement
has a short proof. This is not trivial because our are quite
complicated (and in particular the formulas for iterated product and modular arithmetic).
In order to prove the statement, we will need to carry out a lot of the basic arithmetic in
Before we go on to the technical part, we will try to give some intuition on how the
proof of the main lemma is built.
We organized the proof as a sequence of lemmas that show how many basic facts of
arithmetic can be formulated and proved in TC 0 -Frege (using our formulas). The proofs
of these lemmas require careful analysis of the exact formula used for each operation. The proof
of some of these lemmas is straightforward (using the well known while the
proof of other lemmas require some new tricks.
In short, the main lemmas that are used for the proof of the final statement
(Lemma are the following:
1. (Lemma 38). For every x; y and p , there are TC 0 -Frege proofs of
2. (Lemma 41). For every z are -Frege proofs of
3. (Lemma 47). For every z 1 ; z 2 , there are TC 0 -Frege proofs of
First, we prove some basic lemmas about addition, subtraction, multiplication, iterative-
sum, less-than, and modular arithmetic. Among these lemmas will be Lemma 38.
The proof of Lemma 41 is cumbersome, but it is basically straightforward, given some basic
facts about modular arithmetic. Recall that to do the iterated product we have to first compute
the product modulo small primes and then combine all these products to get the right answer
using iterated sum. Therefore, many basic facts of the modulo arithmetic need to be proven in
advance, as well as some basic facts of the iterated sum.
Once this is done we need to obtain the same fact modulo p (Lemma 48). At this point it is
easier to go through the regular product, where the basic facts of modular arithmetic are easier
to prove. Therefore it is important to show that TC 0 -Frege can prove
(Lemma 47). In our application z 1 and z 2 will themselves be iterated products.
To show this fact we use the Chinese Remainder Theorem. We first prove the equality
modulo small primes. This is relatively easy, since the sizes of these primes are sufficiently small
(O(log N)), and we can basically check all possible combinations. Once this is done, we apply
the Chinese Remainder theorem to obtain the equality modulo the product of the primes, and
since this product is big enough, we obtain the desired result.
Our proof of the Chinese Remainder Theorem, is different than the standard
textbook one. The main fact that we need to show is that if for every j , [R] q j
there are TC 0 -Frege proofs of [R] The usual proofs use some
basic facts of division of primes, that would be hard to implement here. Instead we prove by
induction on
This method allows us to work
with numbers smaller than the q i 's and again since these numbers are sufficiently small, we can
verify all possibilities.
6 Discussion and open problems
We have shown that TC 0 -Frege does not have feasible interpolation, assuming that factoring
of Blum integers is not efficiently computable. This implies (under the same assumptions)
that -Frege as well as any system that can polynomially-simulate -Frege is not
automatizable. It is interesting to note that our proof and even the definition of the Diffie-Hellman
formula itself is nonuniform, essentially due to the nonuniform nature of the iterated
product formulas that we use. It would be interesting to know to what extent our result holds
in the uniform TC 0 proof setting.
A recent paper [BDGMP] extends our results to prove that bounded-depth Frege doesn't
have feasible interpolation assuming factoring Blum integers is sufficiently hard (actually
their assumptions are stronger than ours). As a consequence bounded-depth Frege is not
automatizable under somewhat weaker hardness assumptions.
An important question that is still open is whether resolution, or some restricted forms
of it, is automatizable. A positive answer to this question would have important applied
consequences.
7 Formal proof of main lemma
The goal of this section is to prove Lemma 4. As mentioned earlier, we will build up to the
proof of this lemma, by showing that basic facts concerning arithmetic, multiplication, iterated
multiplication and modulus computations can be efficiently carried out in our proof system.
Before we begin the formal presentation, we would like to note that we will be giving a precise
description of a sequence of lemmas that are sufficient in order to carry out a full, formal proof
Lemma 4. However, since there are many lemmas and many of them have obvious proofs, we
will describe at a meta-level what is required in order to formalize the argument in TC 0 -Frege,
rather than give an excessively formal -Frege proof of each lemma.
In what follows, x , y and z will be numbers. Each one of them will denote a vector of
n variables or formulas (representing the number), where n - N and x i (respectively y i , z i )
denotes the i th variable of x (representing the i th bit of the number x). When we need to talk
about more than three numbers, we will write z 1 ; :::; z m to represent a sequence of m n-bit
(where m;n - N ), and now z i;j is the j th variable of z i (representing the j th bit in
the i th number).
Recall that whenever we say below "there are TC 0 -Frege proofs" we actually mean to say
"there are polynomial size TC 0 -Frege proofs". Some trivial properties like
are not stated here.
7.1 Some basic properties of addition, subtraction and multiplication
Lemma 5 For every x; y , there are TC 0 -Frege proofs of x
Proof of Lemma 5 Immediate from the fact that the addition formula was defined in a
symmetric way. ut
Lemma 6 For every x; z , there are TC 0 -Frege proofs of x
Proof of Lemma 6 By the definition of the addition formula, the i th bit of ((x
equal to \Phi 1 (\Phi 1 is the carry bit going into the
th position, when we add x and y , and C similarly defined to be the carry bit
going into the i th position when we add
Using basic properties of \Phi 1 and the above definitions, there is a simple
proof that if \Phi 1 (C i (x;
Thus it is left to show that for all i
We will show how to prove the stronger equality
(It can be verified that this is the strongest equality possible for the 4 quantities
That is, all 6 assignments for
that satisfy the above equality are actually
possible.)
We will prove this by induction on i . For the carry bits going into the first
position are zero, so the above identity holds trivially. To prove the above equality for i ,
we assume that it holds for We will prove the equality by considering many cases,
where a particular case will assume a fixed value to each of the following seven quantities:
subject to the condition
that C It is easy to check that the
number of cases is 48 since there are 2 choices for x choices for y choices for z
and 6 choices in total for C
Each case will proceed in the same way. We will first show how to compute
using the above seven values. Then we
simply verify that in all 48 cases where the inductive hypothesis holds, the equality is true.
First, we will show that
This requires a proof along the following lines. If x then the left-hand side of the
above statement is true since position a carry, and also the right-hand side of
the statement is also true. Similarly, if x both sides of the above statement
are false (since position carry). The last case is when x
vice-versa). In this case, position propagates a carry, so the i th carry bit is 1 if and only if
there exists a such that the j th position generates a carry, and all positions between
carries - but this is exactly the definition of C . Thus, we have
in this last case that both sides of the statement are true if and only if C
Using the above fact, and also that
only if z
arguments show that C i (y; can also be computed as simple
formulas of the seven pieces of information. ut
Lemma 7 For every x; y , there are TC 0 -Frege proofs of
Proof of Lemma 7 computed by taking the first N bits of
that by the definition of the addition formula it follows easily that all bits of (y + y) are 1, and
hence that ((y
and hence the first N bits of this number are the same as the first N bits of x . ut
Lemma 8 For every x; y , there are
Proof of Lemma 8 computed by taking the first N bits of x By the
definition of the addition formula, and since x - y , it can be proved that the (N th bit of
hence that
Therefore, as in Lemma 7,
In particular, the first N bits of are the same as those of x
Lemma 9 For every x; z , there are TC 0 -Frege proofs of x
Proof of Lemma 9 Follows immediately from Lemma 7 and Lemma 6 as follows:
For every z , there are TC 0 -Frege proofs of
Proof of Lemma 10 We need to show that for every j ,
This is shown by a rather tedious but straightforward proof following the definition of the
formula SUM for iterated addition. Namely, we show first that
and similarly that
Secondly, we show that [H using the definition of + . This second step is not
difficult because all carry bits are zero. ut
Lemma 11 For every z 1 ; :::; z m , and every fixed permutation ff , there are TC 0 -Frege proofs of
(That is, the iterated sum is symmetric.)
Proof of Lemma 11 Immediate from the fact that the formula SUM was defined in a
symmetric way. ut
Lemma 12 For every z , there are TC 0 -Frege proofs of
Proof of Lemma 12 By definition of the iterated addition formula SUM , it is straightforward
to prove that
and similarly that
Then it is also straightforward to show, using the definition of the formula for + , that
for every j . (Again, all carry bits are zero.) ut
Lemma 13 For every z 1 ; :::; z m , there are TC 0 -Frege proofs of
Proof of Lemma 13 Recall that SUM [z computed by adding two numbers H;L .
Recall that L is computed by first computing the numbers L
is the
low-order half of the k th block of z i . The first equality follows from Lemma 13, and Similarly,
computed by H 0 +L 0 , where L 0 is computed by first computing the numbers
In both L k ; L 0
k the sum is computed using poly-size threshold gates, e.g. by using the unary
representation of each L i;k . It is therefore straightforward to prove for each k , L
(e.g. by trying all the possibilities for L 0
proving the formula separately for each
possibility).
Now consider the formula Since in this addition there is no carry flow from one
block to the next one, and since the bits of L; L in each block are just the bits of L k ; L 0
(respectively), we can conclude that in a similar way we can prove that
we are now able to conclude
ut
Lemma 14 For every z 1 ; :::; z m , there are TC 0 -Frege proofs of
Proof of Lemma 14 Can be proved easily from Lemma 13, and Lemma 6 as follows:
Lemma 15 For every z 1 ; :::; z m , and every 1 - k - m, there are TC 0 -Frege proofs of
Proof of Lemma 15 By Lemma 13, Lemma 14 and Lemma 11, we have
The proof now follows by repeating the same argument m \Gamma k times, where Lemma 12 is used
for the base case. ut
Lemma 16 For every x; y , there are TC 0 -Frege proofs of
x
Proof of Lemma 16 Immediate from the fact that the product formula was defined in a
symmetric way. ut
Lemma 17 For every x; x is a power of 2, there are TC 0 -Frege proofs of
x
Proof of Lemma 17 It is straightforward to prove that 2 i \Delta y where y is any sequence of bits,
consists of adding to the end of y , i 0's. The lemma easily follows. ut
Lemma For every z 1 ; :::; z m , and every x where x is a power of 2, there are
proofs of
Proof of Lemma The proof of this lemma is like the proof of Lemma 21, but using
Lemma 17 instead of 20. ut
Lemma 19 For every x; are powers of 2 there are TC 0 -Frege proofs of
x
Proof of Lemma 19 Same as the proof of Lemma 17. ut
The following three lemmas are generalizations of the previous three lemmas.
Lemma 20 For every x; y; z there are TC 0 -Frege proofs of
x
Proof of Lemma 20 By definition of the product formula,
x
Similarly,
x
By iterative application of Lemma 15 (using also Lemma 11),
Similarly (using also Lemma 13, and Lemma 14),
and in the same way (using the same lemmas)
Thus, we have to prove
We will prove this by proving that for every i ,
this is trivial. Otherwise, x using Lemma 19, Lemma 18, and Lemma
we have
In the same way, (using also Lemma 17),
ut
Lemma 21 For every z 1 ; :::; z m , and every x, there are TC 0 -Frege proofs of
Proof of Lemma 21 We will show that for every i ,
The lemma then follows by the combination of all these equalities. The case proven as
follows:
The first equality follows by applying Lemma 13, and the second equality by Lemma 12.
For the general step:
The first equality follows from Lemmas 13 and the second equality follows from Lemma 20; the
third equality follows from Lemma 13. ut
Lemma 22 For every x; z , there are TC 0 -Frege proofs of
x
Proof of Lemma 22 We will show that x \Delta (y \Delta z) is equal to SUM i;j;k [2 i+j+k\Gamma3 x . The
same will be true for and the lemma follows.
By the definition of the product,
y
Hence, by Lemma 10, and two applications of Lemma 21 (and using freely Lemma 16),
x
Since it can be easily verified that (2 , the above is equal to
and by an iterative application of Lemma 15 (using also Lemma 11) the above is equal to
7.2 Some basic properties of less-than
Lemma 23 For every x; y , there are also of
Proof of Lemma 23 Either there is a bit i such that i is the most significant bit where x
and y differ, or not. If all bits are equal, then But if there is i such that it is the most
significant bit where they differ, then if x
Lemma 24 For every x; y , there are
Proof of Lemma 24 By lemma 23, Suppose for a contradiction
that and we get x ? x (which is easily proved to be
false).
Lemma 25 For every x; y; z there are
Proof of Lemma 25 If then the proof of the first statement is obvious. Otherwise,
suppose that i is the most significant bit where x i 6= y i and that x Similarly,
suppose that j is the most significant bit where y j 6= z j and y
it is easy to show that i is the most significant bit where x i 6= z i , and x
thus x ? z . Similarly, if j ? i , then j is the most significant bit where x j 6= z j and x
reasoning also implies the second statement in the lemma. ut
Lemma 26 For every x; z , there are TC 0 -Frege proofs of x+z - x; and also z ?
Proof of Lemma 26 If z = 0 , then it is clear that x show
inductively for decreasing k that
Then when
Assuming that z ? 0 , let z i 0 be the most significant bit such that z i . The base case
of the induction will be to show that x Because z
and applying Lemma 12, it suffices to show that x There are two
cases. If x is equal to x n x
The other case is when x be the most significant bit position greater than i 0 such
that x One clearly exists because x
higher bits are equal, and thus x
For the inductive step, we assume that x want to show
that x Using the same argument as in the base case, one can
prove that (a) x . By the inductive
hypothesis, (b) x Applying Lemma 25 to (a) and (b), we obtain
as desired. ut
Lemma 27 For every x; y; z there are
Proof of Lemma 27 If
Lemma 26. Then by Lemma
Lemma 28 For every x; y; z there are
Proof of Lemma 28
The first equality follows from Lemma 8, and the second from Lemma 26, and the fact that
Lemma 29 For every x; y , there are TC 0 -Frege proofs of y
Proof of Lemma 29 x by definition. Also, since y ? 0 there is a bit
of y that is 1 , and suppose that it is y l . Then
x
ut
7.3 Some basic properties of modular arithmetic
Recall that the formulas for [z] p and div p (z) take as inputs not only the variables p and z , but
also variables k . The formulas give the right
output if n). So the following theorems
will all have the hypothesis that the values for the variables k i , r i and p i are correct, and that
there are short We will state this
hypothesis for the first lemma, and omit it afterwards for simplicity. For simplicity, we will also
use the notations k
The lemmas will be used with either is the number used for the DH
formula, or with fixed hardwired value (e.g.,
q j is one of the primes used for the iterated product formula, and Q is the product of all these
primes). If hardwired q then k can also be hardwired. Hence,
there values are correct and it is straightforward to check (i.e. to prove) that the non-variable
are all correct. If
are inputs for the DH formula itself, and the requirements 2
are part of the requirements in the DH formula.
Lemma z and p be n-bit numbers. Then there are TC 0 -Frege proofs of
Proof of Lemma
ut
Lemma 31 For every z and p, there are TC 0 -Frege proofs of
Also, the following uniqueness property has a
then
Proof of Lemma 31 From the previous lemma, we can express z as SUM i [(r
Let l be the same as in the definition of the modulo formulas. Then
The first equality follows from the definitions of the formulas [z] p and div p (z) . The remaining
equalities follow from the following Lemmas: 20, 6, 8, 21, 13, 15, 14 and 30.
Let us now prove the uniqueness part. Suppose
then we are done. But if div p (z) ? y , then by the claim bellow
which is a contradiction. (And a similar argument holds when div
Proof of the claim Since v ? y , by Lemma 8, and Lemma
Lemma 9 we get that Therefore by Lemmas 29 and 26,
and by Lemma 25 we get p - x . ut
Lemma 33 For every z; k and p, there are TC 0 -Frege proofs of
Proof of Lemma 33 Let
(by Lemma 31).
Therefore,
By the uniqueness part of Lemma 31 applied to x , [z]
Lemma 34 For every x; y; z and p, there are -Frege proofs of
and also of
and
Proof of Lemma 34 By Lemma 31,
and by Lemma 33,
A similar argument shows that [x
Lemma 35 For every z 1 ; :::; z m and p, there are TC 0 -Frege proofs of
Proof of Lemma 35 The lemma follows easily from Lemma 13 and Lemma 34. ut
Lemma 36 For every x; y and p, there are TC 0 -Frege proofs of
Proof of Lemma 36
The first equality follows from Lemma 34; the next equality follows from the assumption that
and the third equality follows from Lemma 34. ut
Lemma 37 For every x; y; z and p, there are -Frege proofs of
Proof of Lemma 37 Assuming that [x it follows from the above Lemma 36
that [x . The left side of the equation is equal to:
The first equality follows from Lemma 34; the second equality follows from Lemmas 5, 6 and
7; the third equality follows from Lemma 33. Similarly, it can be shown that [y
and thus the lemma follows. ut
Lemma 38 For every x; y and p, there are TC 0 -Frege proofs of
Proof of Lemma 38
where the last equality follows from Lemma 33. ut
Lemma fixed numbers such that A = BC . Then for every z , there are
-Frege proofs of
This lemma will be used in situations where . Recall that the
numbers Q; are hardwired and also their corresponding k i , r i and the variables for the
's. Hence, we think of A; B; C as hardwired.
Proof of Lemma 39 Using Lemmas 31,33,22, we get
ut
7.4 Some basic properties of iterative product
Lemma 40 For every z 1 ; :::; z m , and every fixed permutation ff , there are TC 0 -Frege proofs of
(That is, the iterated product is symmetric.)
Proof of Lemma 40 This lemma is immediate from the symmetric definition of PROD . ut
Lemma 41 For every z 1 ; :::; z m , and every 1 - k - m, there are TC 0 -Frege proofs of
Proof of Lemma 41 Recall that we have hard-coded the numbers u j , such that u j mod q
and for all i . For all primes q j dividing Q , and for all m ,
we can verify the following statements:
that these statements are variable-free and hence they can be easily proven by doing a formula
evaluation.)
Recall that for any k , the iterated product of the numbers z k ; :::; z m is calculated as follows:
where r [k;:::;m]
j is computed like r j as defined in Section 3.4, but using r ij only for i such that
In the same way,
where r [1;::;k\Gamma1;[k;::;m]]
j is calculated as before by the following steps:
1. For
, and also calculate r
2. For calculate a i;j such that (g a i;j
also a  ;j such that (g a  ;j
3. Calculate c 0
4. Calculate r [1;::;k\Gamma1;[k;::;m]]
j such that g c 0
by table-lookup.
Therefore, all we have to do is to show that
Hence, all we need to do to prove Lemma 41 is to show the following claim:
42 For every j , there are TC 0 -Frege proofs of r [1;:::;k\Gamma1;[k;:::;m]]
.
The first step is to prove the following claim:
43 There are
.
43 is proven as follows.
[r [k;::;m]
The second equality follows by Lemma 39; the third equality follows by Lemma 35, and
Lemma 11. To prove the fourth equality, we need to use the fact that [u j \Delta r [k;:::;m]
and also for all i
These facts can be easily proved just by checking
all possibilities for r [k;:::;m]
(proving the statement for each possibility is easy, because these
statements are variable-free and hence they can be easily proven by doing a formula evaluation).
In order to prove the fourth equality formally, we can show that SUM i6=j [u i \Delta r [k;:::;m]
equals
zero by induction on the number of terms in the sum. ut
We can now turn to the proof of Claim 42. The quantity r [1;:::;m]
j is obtained by doing a
table lookup to find the value equal to g c j
\Gamma1) . Similarly,
the quantity r [1;:::;k\Gamma1;[k;:::;m]]
j is obtained by doing a table lookup to find the value equal to
Hence, it is enough to prove that c
. Using previous lemmas
Thus, it suffices to show that
Recall that a  ;j is the value obtained by table-lookup such that (g a  ;j
by Claim 43, we have that r
j , in turn, is the value obtained by
table-lookup to equal (g d
Now it is easy to verify that our table-lookup is one-to-one. That is, for every x;
. Using this property (with
7.5 The Chinese Remainder Theorem and other properties of iterative prod-
uct
The heart of our proof is a proof for the following lemma, which gives the hard
direction of the Chinese Remainder Theorem (a proof for the other direction is
simpler).
Lemma 44 Let R; S be two integers, such that for every j , [R] q j
: Then there are
-Frege proofs of
(where are the fixed primes used for the PROD formula (i.e., the first t primes), and
Q is their product.)
Proof of Lemma 44 Without loss of generality, we can assume that 0 - R; S -
prove that R = S . Otherwise, define R use Lemma 39 to show
that for every j , [R 0
. Since 0 - R 0 conclude that
For every k , let Q k denote
Note that the numbers Q k can be hardwired, and that
one can easily prove the following statements. (These statements are variable-free and hence
they can be easily proven by doing a formula evaluation.)
For every i ,
The proof of the lemma is by induction on t (the number of q j 's). For
the lemma is trivial. Assume therefore by the induction hypothesis that
and hence
Denote,
[R] , and D
[S] . Then by Lemma 31,
and
and since we know that [R] q t
; we have
and by [R] Q
, and Lemma 37
Since R; S are both lower than Q , it follows that DR ; D S are both lower than q t . Hence,
by Claim Therefore, we can conclude that
For every i, there are
then
Proof Since d 1 are only O(log n) possibilities for d 1 ; d 2 . Therefore, one can just
check all the possibilities for d 1 ; d 2 . Proving the statement for each possibility is easy, because
these statements are variable-free and hence they can be easily proven by doing a formula
evaluation.
Alternatively, one can define the function
, in the domain f0; :::; q i g , and
prove that f(x) is onto the range f0; :::; q i g . Then, by applying the propositional pigeonhole
principle, which is efficiently provable in TC 0 -Frege, it follows that f is one to one. ut
We are now able to prove the following lemmas.
Lemma 46 For every z , there are TC 0 -Frege proofs of
Proof of Lemma 46 Recall that PROD[z] is calculated as follows:
where r j is computed by r
By Claim 43, for every i , PROD[z] q i
thus have for every i , PROD[z] q i
The proof of the lemma now follows by Lemma 44.
ut
Lemma 47 For every z 1 ; z 2 , there are TC 0 -Frege proofs of
Proof of Lemma us prove that for every i ,
The proof of the lemma then follows by Lemma 44. By two applications of Lemma 38 it is
enough to prove for every i ,
Recall that PROD[z 1 ; z 2 ] is calculated as follows:
where r [1;2]
j is computed like r j as defined in Section 3.4. By Claim 43, for every i ,
Recall that [z 1
r 2;i . Therefore, all we have to prove is that for every
r [1;2]
By the definitions: r
Also,
r [1;2]
Therefore, one can just check all the possibilities for a 1;i ; a 2;i .
ut
Using the previous lemmas, we are now able to prove the following:
Lemma 48 For every z every p, there are TC 0 -Frege proofs of
(as before, given that 2
Proof of Lemma 48
The lemmas used for each equality in turn are: Lemmas 41,47, 38,47,41, and 41. ut
We are now ready to prove Lemma 4:
For every z 1;1 ; :::; z m;m 0 and p , there are TC 0 -Frege proofs of
(given that 2
Proof of Lemma 4 By an iterative application of the previous lemma. ut

Acknowledgments

We are very grateful to Omer Reingold and Moni Naor for collaboration at early stages of this
work, and in particular for suggesting the use of the Diffie-Hellman cryptographic scheme. We
also would like to thank Uri Feige for conversations and for his insight about extending this
result to bounded-depth Frege. Part of this work was done at Dagstuhl, during the Complexity
of Boolean Functions workshop (1997).



--R

"The Monotone Circuit Complexity of Boolean Functions"
"Minimal propositional proof length is NP-hard to linearly approximate"
"Generalized Diffie-Hellman modulo a composite is not weaker than factoring"
" Log depth circuits for division and related problems,"
"Non-automatizability of bounded-depth Frege proofs"
"Lower bounds for Cutting Planes proofs with small coefficients,"
"The Undecidability of k-Provability"
"On Godel's theorems on lengths of proofs II: Lower bounds for recognizing k symbol provability,"
"Cutting planes, connectivity and threshold logic,"
"An Exponential Lower Bound for the Size of Monotone Real Circuits,"
"Constant depth reducibility,"
"New directions in cryptography,"
"Upper and lower bounds for tree-like Cutting Planes proofs,"
"Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic"

"Discretely ordered modules as a first-order extension of the cutting planes proof system,"

"Threshold circuits of small majority depth,"
"A key distribution system equivalent to factoring,"

"A lower bound for the complexity of Craig's interpolants in sentential logic,"

"Lower bounds for resolution and cutting planes proofs and monotone computations,"
"Algebraic models of computation and interpolation for algebraic proof systems,"

"Lower Bounds for the Monotone Complexity of some Boolean Func- tions"
"Unprovability of lower bounds on the circuit size in certain fragments of bounded arithmetic,"
"Composite Diffie-Hellman public-key generating systems are hard to break,"
--TR

--CTR
Alexander Razborov, Propositional proof complexity, Journal of the ACM (JACM), v.50 n.1, p.80-82, January
Pavel Pudlk, On reducibility and symmetry of disjoint NP pairs, Theoretical Computer Science, v.295 n.1-3, p.323-339, 24 February
Olaf Beyersdorff, Classes of representable disjoint NP-pairs, Theoretical Computer Science, v.377 n.1-3, p.93-109, May, 2007
Albert Atserias, Conjunctive query evaluation by search-tree revisited, Theoretical Computer Science, v.371 n.3, p.155-168, March, 2007
Samuel R. Buss, Polynomial-size Frege and resolution proofs of st-connectivity and Hex tautologies, Theoretical Computer Science, v.357 n.1, p.35-52, 25 July 2006
Paolo Liberatore, Complexity results on DPLL and resolution, ACM Transactions on Computational Logic (TOCL), v.7 n.1, p.84-107, January 2006
Maria Luisa Bonet , Nicola Galesi, Optimality of size-width tradeoffs for resolution, Computational Complexity, v.10 n.4, p.261-276, May 2002
Albert Atserias , Mara Luisa Bonet, On the automatizability of resolution and related propositional proof systems, Information and Computation, v.189 n.2, p.182-201, March 15, 2004
Juan Luis Esteban , Nicola Galesi , Jochen Messner, On the complexity of resolution with bounded conjunctions, Theoretical Computer Science, v.321 n.2-3, p.347-370, August 2004
diffie-hellman;threshold circuits;propositional proof systems;frege proof systems