
## 3 Proof Systems For Asp And Sat

```
In this se
         tion we review 
                        on
                           epts related to proof 
                                               omplexity (Cook and Re
                                                                        khow 1979; Beame and Pitassi 1998) in the 
                        ontext of this work, and dis
                                              uss the relationship
                                                             

```

of Resolution and ASP Tableaux (Gebser and S
haub 2006b).

## 3.1 Propositional Proof Systems And Complexity

Formally, a (propositional) proof system is a polynomial-time omputable prediate S su
h that a propositional expression E is unsatisable if and only if there is a proof P for whi
h S(**E, P**) holds. A proof system is thus a polynomial-time pro edure for he king the orre tness of proofs in a ertain format. While proof he king is e ient, nding short proofs may be di ult, or, generally, impossible sin e short proofs may not exist for a too weak proof system. As a measure of hardness of proving unsatisability of an expression E in a proof system S , the
(proof ) 
omplexity of E in S is the length of the shortest proof for E in S . For a family {En} of unsatisable expressions over in
reasing number of variables, the
(asymptoti
) 
omplexity of {En} is measured with respe
t to the sizes of En .

For two proof systems S and S
′
, we say that S
′ polynomial ly simulates S if for all families {En} it holds that CS′ (En) ≤ p(CS (En)) for all En , where p is a polynomial, and CS and CS′ are the 
omplexities in S and S
′
, respe tively. If S
simulates S
′ and vi e versa, then S and S
′ are polynomial ly equivalent. If there is a family {En} for whi
h S
′ does not polynomially simulate S , we say that {En}
separates S from S
′
. If S simulates S
′
, and there is a family {En} separating S
from S
′
, then S is more powerful than S
′
.

## 3.2 Resolution

The well-known Resolution proof system (RES) for sets of 
lauses is based on the resolution rule. Let **C, D** be 
lauses, and x a Boolean variable. The resolution rule states that we an dire tly derive C ∪ D from {x} ∪ C and {x¯} ∪ D by resolving on x.

A RES derivation of a 
lause C from a set C of 
lauses is a sequen
e of 
lauses π = (C1, C2**, . . . , C**n), where Cn = C and ea
h Ci
, where 1 ≤ **i < n**, is either
(i) a lause in C (an initial 
lause), or (ii) derived with the resolution rule from two lauses Cj , Ck , where **j, k < i** (a derived 
lause). The length of π is n, the number of lauses o urring in it. Any derivation of the empty lause ∅ from C is a RES
proof for (the unsatisability of ) C .

Any RES proof π = (C1, C2**, . . . , C**n = ∅) 
an be represented as a dire
ted a
y
li graph, in whi h the leafs are initial lauses and other nodes are derived lauses.

There are edges from Ci and Cj to Ck if and only if Ck has been dire
tly derived from Ci and Cj using the resolution rule. Many Resolution renements, in whi
h the stru ture of the graph representation is restri ted, have been proposed and studied. Of parti ular interest here is Tree-like Resolution (T-RES), in whi
h it is required that proofs are represented by trees. This implies that a derived lause,