program Π, the 
orresponding 
ut tree is obtained as follows. Starting from the root of T , we repla
e ea
h non-leaf entry generated by a dedu
tion rule in T by an

```
appli
     ation of the 
               ut rule on the 
                            orresponding entry. For example, the 
                                                            ut tree T
                                                                    ′

```

orresponding to the ASP-T proof T in Figure 2 is given in Figure 3 (left).

Proof of Theorem 3.2 (i)

Let T be an ASP-T proof for a tight normal logi program Π. Without loss of generality, we will assume that bran hes in T have not been extended further after

```
they have be
             ome 
                  ontradi
                          tory. We now show that we 
                                                      an 
                                                          onstru
                                                                 t a T-RES

proof π for comp(Π) using the 
ut tree T
                                        ′
                                          
                                           orresponding to T . Furthermore, we

```

show that for su h a proof π it holds that, given any prex p of an arbitrary

```
bran
   h B in T
          ′
           there is a 
                    lause C ∈ π 
ontradi
tory to the partial assignment

```

in p, that is, there is the entry Fa (Ta) for a ∈ atom(Π) ∪ body(Π) in p for ea
h orresponding positive literal xa (negative literal x¯a) in C .

Consider rst the partial assignment in an arbitrary (full) bran h B in T
′
. Assume that there is no lause in comp(Π) 
ontradi
tory to the partial assignment in B ,
that is, we an obtain a truth assignment τ based on the entries in B su
h that every lause in comp(Π) is satised in τ . But this leads to 
ontradi
tion sin
e comp(Π) is satised if and only if Π is satised. Thus there is a 
lause C ∈ comp(Π) 
ontradi
-
tory to the partial assignment in B , and we take the 
lause C into our resolution proof π.

Assume that we have onstru ted π su
h that for any prex p of length n for any bran h B in T
′
, there is a lause C ∈ π 
ontradi
tory to the partial assignment in p.

Consider an arbitrary prex p of length n − 1. Now, in T
′ we have the prexes p
′
and p
′′ of length n whi
h have been obtained through extending p by applying the ut rule on some a ∈ atom(Π) ∪body(Π). In other words, p
′
is p with Ta appended in the end (p
′′ is p with Fa appended in the end). Sin
e p
′
(p
′′
, respe tively) is of length n, there is a 
lause C (D, respe
tively) in π 
ontradi
tory to the partial assignment in p
′
(p
′′
, respe tively). Now there are two possibilities. If C = {x¯a}∪C
′
and D = {xa} ∪ D′, we 
an resolve on xa adding C
′ ∪ D′to π. Thus we have a lause C
′∪D′ ∈ π 
ontradi
tory to the partial assignment in the prex p. Otherwise we have that x¯a 6∈ C or xa 6∈ D, and hen
e either C ∈ π or D ∈ π is 
ontradi
tory to the partial assignment in the prex p.

When rea hing the root of T
′
, we must have derived ∅ sin
e it is the only 
lause ontradi tory with the empty assignment. Furthermore, the T-RES derivation π is of polynomial length with respe t to T
′
(and T ).

The following example illustrates the RES proof 
onstru
tion used above in the proof of Theorem 3.2 (i).

Example 3.3 Consider again the tight NLP Π = {a ← b, ∼a. b ← c. c ← ∼b}
from Example 2.3 and the ASP-T proof T for Π in Figure 2. We now 
onstru
t a T-RES proof for the 
ompletion comp(Π) (see Example 2.3 for details) using the strategy from the proof of Theorem 3.2 (i). First, T is transformed into a 
ut

```
tree T
      ′
        given in Figure 3 (left). Consider now the two leftmost bran
                                                                           hes in T
                                                                                    ′
                                                                                     . The
                                                                                           

```

partial assignment in the bran h with entries Ta and F{b, ∼a} is 
ontradi
tory