www.lsi.upc.es/~esteban
**Abstract**

This work is a contribution to the field of Proof Complexity, which
studies the complexity of proof systems in terms of the resources needed
to prove or refute propositional formulas. Proof Complexity is an interesting
field which has several connections to other fields of Computer Science
like Computational Complexity or Automatic Theorem Proving among others.
This work focuses in complexity measures for refutational proof systems
for CNF formulas. We consider several proof systems, namely Resolution,
R(k) and Cutting Planes and our results concern mainly to
the size and space complexity measures.

We improve previous size separations between treelike and general versions
of Resolution and Cutting Planes. To do so we extend a size lower bound
for monotone boolean circuits by Raz and McKenzie, to monotone real circuits.
This kind of separations is interesting because some automated theorem
provers rely on the treelike version of proof systems, so the separations
show that is not always a good idea to restrict to the treelike version.
What we do is to prove treelike Cutting Planes exponential lower bounds
for certain formulas via the feasible monotone interpolation property,
which clearly are also lower bounds for treelike Resolution. To get the
separation we show Resolution polynomial size upper bounds for the same
formulas, which clearly are also upper bounds for Cutting Planes. In fact
we can separate not only treelike Resolution from Resolution, also we can
separate treelike Resolution from certain restrictions of Resolution like
regular Resolution and negative Resolution. The separation result for treelike
Resolution and Resolution was later improved by Ben-Sasson,
Impagliazzo and Wigderson.

After the recent apparition of R(k) which is a proof system
lying between Resolution and bounded-depth Frege it was important
to study how powerful it is and its relation with other proof systems.
We solve an open problem posed by Krajícek, namely we show that
R(2) does not have the feasible monotone interpolation
property. To do so, we show that R(2) is strictly more
powerful than Resolution. We give a R(2) polynomial size
upper bound for a certain Clique-Coclique Principle
reducing it to a Pigeonhole Principle with parameters that ensures polynomial
size Resolution refutations. But as Resolution has the feasible monotone
interpolation property, and it is known that circuits separating cliques
from cocliques require superpolynomial size, then Resolution refutations
for this Clique-Coclique Principle also require superpolynomial
size. As now we know that R(2) is more powerful that Resolution
and treelike R(2) more powerful than treelike Resolution,
a natural question is to find out whether we can separate successive levels
of R(k) or treelike R(k). We show exponential
separations between successive levels of what we can call now the treelike
R(k) hierarchy. That means that there are formulas that require
exponential size R(k) refutations whereas they have polynomial
size R(k+1) refutations. Segerlind, Buss and Impagliazzo extended
this result to R(k). We also prove that Resolution dominates
treelike R(k). This is a particular case of a known simulation
due to Krajícek, but we show that an increment by factor 2, independent
of k, suffices.

We have proposed a new definition for Resolution space improving a previous
one from Kleine-Büning and Lettmann. There is also
an equivalent
definition of Resolution space from Alekhnovich, Ben-Sasson,
Razborov and Wigderson. We give general results for Resolution and treelike
Resolution space, namely that any CNF with n variables requires at most
space n+1 and relationships between space and size among others.
We also give a combinatorial characterization of treelike Resolution space
via a Player-Adversary game over CNF formulas. The
characterization allows to prove lower bounds for treelike Resolution
space with no need to use the concept of Resolution or Resolution
refutations at all. For
a long time it was not known whether Resolution space and treelike Resolution
space coincided or not. We have answered this question in the negative
because we give the first space separation from Resolution to treelike
Resolution. We have also studied space for R(k). We show that,
as happened with respect to size, treelike R(k) forms a hierarchy
respect to space. So, there are formulas that require nearly linear space
for treelike R(k) whereas they have constant space treelike
R(k+1) refutations. We extend all known Resolution space lower
bounds to R(k) in an easier and unified way, that also holds
for Resolution, using the concept of dynamical satisfiability introduced
in this work.

**Table of Contents**

1. Introduction and definitions
*1.1 Proof Systems*

*1.2 Complexity Measures*

*1.3 Formulas*

*1.4 Circuit Complexity*

*1.5 Overview of results in the area*

*1.6 Summary of results and organization of this work*

2. Size
*2.1 Size separation between CP* and R(1)*

*2.2 R(2) has not the monotone interpolation property*

*2.3 R(2) and PHP(n*^{2},n)

*2.4 Size and R*(k)*

3. Space and width
*3.1 Space for R(1)*

*3.2 Combinatorial characterization of R*(1) space*

*3.3 Separation between R(1) space and
R*(1) space*

*3.4 Space separations for R*(k)*

*3.5 Space lower bounds for R(k)*

4. Recapitulation

**Number of pages:** 105