whi h is non-tight with the additional self-loops {pi,j ← pi,j}, but preserves (un)satisability of PHPn+1 n for all n. Sin
e the self-loops do not 
ontribute to the proofs for PHPn+1 n , ASP-T still has exponential-length minimal proofs for these programs, while the polynomial-length E-ASP-T proof presented in the proof of Theorem 5.2 is still valid.

The generality of the arguments used in the proof of Theorem 5.2 is not limited to the spe i family PHPn+1 n of NLPs. For understanding the general idea behind the expli it onstru tion of EPHPn+1 n, it is informative to noti
e the following. Instead of onsidering PHPn+1 n, one 
an apply the argument in the proof Theorem 5.2 using any tight NLP Π whi
h represents a set of 
lauses C for whi
h (i) there is no polynomial-length RES proof, but for whi
h (ii) there is a polynomial-length E-RES
proof . By property (ii) we know from Theorem 5.1 (ii) that there is a polynomiallength E-ASP-T proof for Π.

## 5.3 Program Simpli Ation And Complexity

```
We will now give an interesting 
                     orollary of Theorem 5.2, addressing the ee
                                                 t of
                                                   

```

program simpli ation on the length of proofs in ASP-T.

Tightly related to the development of e ient solver implementations for ASP

programs arising from pra ti al appli ations is the development of te hniques for simplifying programs. Pra ti ally relevant programs are often generated automati ally, and in the pro ess a large number of redundant onstraints is produ ed.

Therefore e ient program simpli ation through lo al transformation rules is important. While various satisability-preserving lo al transformation rules for simplifying logi programs have been introdu ed (see (Eiter et al. 2004) for example),

```
the ee
       t of applying su
                       h transformations on the lengths of proofs has not re
                                                                         eived
                                                                              

```

attention.

Taking a rst step into this dire tion, we now show that even simple transfor-

```
mation rules may have a drasti
                            negative ee
                                       t on proof 
                                                  omplexity. Consider the
                                                                      

```

lo al transformation rule

$$\begin{array}{r c l}{{\mathsf{red}(\Pi)}}&{{=}}&{{\Pi\setminus\{r\in\Pi\mid\mathsf{head}(r)\not\in\bigcup_{B\in\mathsf{body}(\Pi)}(B^{+}\cup B^{-}){\mathrm{~and~}}\mathsf{head}(r)\not=\bot\}.}}\end{array}$$

A polynomial-time simpli ation algorithm red∗(Π) is obtained by 
losing program Π under red. Noti
e that we have red∗(EPHPn+1 n ) = PHPn+1 n . Thus, by Theorem 5.2, red∗transforms a program family having polynomial 
omplexity in ASP Tableaux into one with exponential omplexity with respe t to n.

The rules removed by red∗are redundant with respe
t to satisability of the program in the sense that red∗preserves visible equivalen
e (Janhunen 2006). The visible equivalen e relation takes the interfa es of programs into a ount: atom(Π)
is partitioned into v(Π) and h(Π) determining the visible and the hidden atoms in Π,
respe tively. Programs Π1 and Π2 are visibly equivalent, denoted by Π1 ≡v Π2 , if and only if v(Π1) = v(Π2) and there is a bije
tive 
orresponden
e between the stable models of Π1 and Π2 mapping ea
h a ∈ v(Π1) onto itself. Now if one denes v(Π) =
atom(red∗(Π)) = v(red∗(Π)), that is, assuming that the atoms removed by red∗are