Example 3.4 Re al l the set C = {{x, y}, {x, y¯}, {**x, y** ¯ }, {x, ¯ y¯}} of 
lauses and the orresponding normal logi program nlp(C) presented in Example 2.2. The set C of lauses has a T-RES refutation π = ({x, y}, {x, y¯}, {**x, y** ¯ }, {x, ¯ y¯}, {y}, {y¯}, ∅). Now we onstru t an ASP-T proof T for nlp(C) from π as done in the proof of Theorem 3.2 (ii). The resulting ASP-T proof T is presented in Figure 4. In the tableau we have omitted entries of the form T{l} and F{l} for bodies 
onsisting of a single default literal. The empty lause is obtained resolving on y from {y} and {y¯}, and thus we start with applying the ut rule on ay . The 
lause {y¯} is obtained resolving on x from {x, y¯} and {x, ¯ y¯}. We 
ontinue in the bran
h with Tay by applying the ut rule on ax. Consider now the bran
h with Tay and Tax in the tableau. The bran h orresponds to the lause {x, ¯ y¯} in C . Thus we arrive in a 
ontradi
tion by dedu ing Fc4 from c4 ← ∼ax and c4 ← ∼ay , and Tc4 from **⊥ ← ∼**c4. Other bran hes be ome ontradi tory similarly.

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

## 4 Extended Asp Tableaux

We will now introdu e an extension rule3 to ASP-T, whi
h results in Extended ASP
Tableaux (E-ASP-T), an extended tableau proof system for ASP. The idea is that

```
one 
    an dene names for 
                       onjun
                            tions of default literals.
                                                 

```

Denition 4.1 Given a normal logi program Π and two literals l1, l2 ∈ dlit(Π),
the (elementary) extension rule in E-ASP-T adds the rule p ← l1, l2 to Π, where p 6∈ atom(Π) **∪ {⊥}**.

It is essential that p is a new atom for preserving satisability. After an appli
ation of the extension rule one onsiders the program Π′ = Π∪ {p ← l1, l2} instead of the original program Π. Noti
e that atom(Π′) = atom(Π)∪{p}. Thus when the extension

```
rule is applied several times, the atoms introdu
                                                  ed in previous appli
                                                                        ations of the
                                                                                     

rule 
     an be used in dening further new atoms (see the forth
                                                                oming Example 4.2).
                                                                                     

```
