Thus we obtain a omplete and nonontradi tory tableau for Π ∪ E . Sin
e we annot generate a ontradi tory tableau for Π with tableau rules (a)(g),(h§), and
(i§), we 
annot generate one for Π ∪ E either. This is in 
ontradi
tion with the fa
t that Π is unsatisable.

## 5 Proof Complexity

```
In this se
         tion we study proof 
                              omplexity theoreti
                                                 issues related to E-ASP-T from

```

several viewpoints: we will

- 
onsider the relationship between E-ASP-T and the Extended Resolution proof system (Tseitin 1969),

- give an expli
it separation of E-ASP-T from ASP-T, and
- relate the extension rule to the ee
t of program simpli
ation on proof lengths in ASP-T.

## 5.1 Relationship With Extended Resolution

The system E-ASP-T is motivated by Extended Resolution (E-RES), a proof system originally introdu ed in (Tseitin 1969). The system E-RES 
onsists of the resolution rule and an extension rule that allows one to expand a set of lauses by iteratively introdu ing equivalen es of the form x ≡ l1 ∧ l2 , where x is a new variable, and l1 and l2 are literals in the 
urrent set of 
lauses. In other words, given a set C of lauses, one appli ation of the extension rule adds the lauses {x, ¯l1,
¯l2}, {**x, l** ¯ 1},
and {**x, l** ¯ 2} to C . The system E-RES is known to be more powerful than RES; in fa t, E-RES is polynomially equivalent to, for example, extended Frege systems, and no superpolynomial proof omplexity lower bounds are known for E-RES. We will now relate E-ASP-T with E-RES, and show that they are polynomially equivalent under the translations comp and nlp. Theorem 5.1 E-RES and E-ASP-T are polynomial ly equivalent proof systems in the sense that

(i) 
onsidering tight normal logi programs, E-RES under the translation comp polynomial ly simulates E-ASP-T, and
(ii) 
onsidering sets of lauses, E-ASP-T under the translation nlp polynomial ly simu-

lates E-RES.
Proof

(i): Let T be an E-ASP-T proof for a tight NLP Π, that is, T is an ASP-T proof for Π ∪ E , where E is the set of extending rules generated in the proof. We use the shorthand xl for the variable 
orresponding to default literal l in comp(Π ∪ E),
that is, xl = xa (xl = ¯xa , respe
tively) if l = a (l = ∼a, respe
tively) for a ∈
atom(Π ∪ E). By Theorem 3.2 there is a polynomial RES proof for comp(Π ∪ E).

Now onsider comp(Π). We apply the extension rule in E-RES in the same order in whi h the extension rule in E-ASP-T is applied when generating the set E of