if subsequently used multiple times in the proof, must be derived anew ea h time from initial lauses.

T-RES is a proper RES renement, that is, RES is more powerful than T-RES (Ben-Sasson et al. 2004).

On the other hand, it is well known that the DPLL method (Davis and Putnam 1960; Davis et al. 1962), the basis of most state-of-the-art SAT solvers, is polynomially equivalent to T-RES. However, 
oni
t-learning DPLL is more powerful than T-RES,
and polynomially equivalent to RES under a slight generalization (Beame et al. 2004).

## 3.3 Asp Tableaux

Although ASP solvers for normal logi programs have been available for many years, the dedu tion rules applied in su h solvers have only re ently been formally dened as a proof system, whi h we will here refer to as ASP Tableaux or ASP-T (Gebser and S
haub 2006b).

An ASP tableau for a NLP Π is a binary tree of the following stru
ture. The root of the tableau onsists of the rules Π and the entry F⊥ for 
apturing that ⊥
is always false. The non-root nodes of the tableau are single entries of the form Ta or Fa, where a ∈ atom(Π) ∪ body(Π). As typi
al for tableau methods, entries are generated by extending a bran h (a path from the root to a leaf node) by applying one of the rules in Figure 1; if the prerequisites of a rule hold in a bran h, the bran h an be extended with the entries spe ied by the rule. For onvenien e, we use shorthands tl and fl for default literals:

$$\begin{array}{r c l}{{\mathbf{t}l}}&{{=}}&{{\begin{cases}\mathbf{T}a,\mathrm{~if~}l=a\mathrm{~is~positive,}\\ \mathbf{F}a,\mathrm{~if~}l=\sim}a\mathrm{~is~negative;~and~}\end{cases}}\\ {{\mathbf{f}l}}&{{=}}&{{\begin{cases}\mathbf{T}a,\mathrm{~if~}l=\sim}a\mathrm{~is~negative,}\\ \mathbf{F}a,\mathrm{~if~}l=a\mathrm{~is~positive.}\end{cases}}\end{array}$$

A bran h is losed under the dedu tion rules (b)(i) if the bran h annot be extended using the rules. A bran h is ontradi tory if there are the entries Ta and Fa for some a. A bran
h is 
omplete if it is 
ontradi
tory, or if there is the entry Ta or Fa for ea
h a ∈ atom(Π) ∪ body(Π) and the bran
h is 
losed under the dedu tion rules (b)(i). A tableau is ontradi tory, if all its bran hes in are ontradi tory, and nonontradi tory otherwise. A tableau is omplete if all its bran hes are omplete. A 
ontradi tory tableau from Π is an ASP-T proof for (the unsatisability of ) Π. The length of an ASP-T proof is the number of entries in it.

Example 3.1 An ASP-T proof for the NLP Π = {a ← b, ∼a. b ← c. c ← ∼b} is shown in Figure 2, with the rule applied for dedu ing ea h entry given in parentheses. For example, the entry Fa has been dedu
ed from a ← b, ∼a in Π and the entry T{b, ∼a} in the left bran
h by applying the rule (g) Ba
kward True Body. On the other hand, T{b, ∼a} has been dedu
ed from a ← b, ∼a in Π and the entry Ta in the left bran h by applying the rule (i§), that is, rule (i) by the fa
t that the ondition § Ba
kward True Atom is full led (in Π, the only body with atom a in the head is {b, ∼a}). The tableau in Figure 2 has two 
losed bran
hes:
(Π ∪ {F⊥}, Ta, T{b, ∼a}, Fa) and