12 M. Järvisalo and E. Oikarinen

![0_image_0.png](0_image_0.png)

to lause {x¯a, x{b,∼a}} in comp(Π), and the partial assignment in the bran
h with entries Ta and T{b, ∼a} is 
ontradi
tory to 
lause {x¯{b,∼a}, x¯a} in comp(Π). Thus we resolve on x{b,∼a} and obtain the 
lause {x¯a}, whi
h is 
ontradi
tory to the

```
single entry Ta in the prex of the two leftmost bran
hes in T
                                                                   ′
                                                                    . Similarly, we 
                                                                                     an
                                                                                        
 onstru
        t a resolution tree for 
                                 lause {xa} 
orresponding to the right side of T
                                                                                  ′
                                                                                   . We
                                                                                        
nish the proof by resolving on xa . The 
omplete T-RES proof 
orresponding to the

 ut tree T
          ′
            is shown in Figure 3 (right).
                                          

```

## Proof Of Theorem 3.2 (Ii)

Let π = (C1**, . . . , C**n = ∅) be a T-RES refutation of a set C of 
lauses. Re
all that ea h derived lause Ci in π is obtained by resolving on x from Cj = C ∪ {x} and Ck = D ∪ {x¯} for some **j, k < i**.

An ASP-T proof T for nlp(C) is obtained from π as follows. We start from Cn ,
whi h is obtained from lauses Cj = {x} and Ck = {x¯} by resolving on x ∈ var(C),
and apply in T the 
ut rule on ax 
orresponding to x. Then we re
ursively 
ontinue the same way with Cj (Ck , respe
tively) in the generated bran
h with Fax (Tax ,
respe tively). Sin e π is tree-like, ea
h 
lause in the prex (C1, . . . , Cmax{j,k}) of π is either used in the derivation of Cj or Ck , but not in both. By 
onstru
tion when rea hing C1 the bran
hes of T 
orrespond one-to-one to the paths in π (seen as a tree) from Cn to the leaf 
lauses of π. For a parti
ular leaf 
lause C , we have for ea h literal l ∈ C (l = x or l = ¯x) 
ontradi
ting entries for ax in the 
orresponding bran h of T , that is, Fax if l = x and Tax if l = ¯x. Now we 
an dire
tly dedu
e for ea h Fax the entry F{ax} and for ea
h Tax the entry F{∼ax}. These entries together will allow us to dire tly dedu e Fc (all the bodies of rules with atom c as the head are false). Sin e we have **⊥ ← ∼**c ∈ nlp(C), we 
an dedu
e Tc, and the bran h be omes ontradi tory.

The following example illustrates the strategy used in the proof of Theorem 3.2 (ii).