Forgetting for Answer Set Programs Revisited

1 Introduction

The ability of discarding or hiding irrelevant information has been recognized as an important feature for logic-based agent systems and is named variable forgetting or variable elimination in Artificial Intelligence [Lin and Reiter, 1994]. Forgetting has been applied in cognitive robotics [Lin and Reiter, 1994; Liu and Wen, 2011], resolving conflicts [Lang et al., 2003; Zhang and Foo, 2006; Eiter and Wang, 2008], and ontologies [Wang et al., 2010; Konev et al., 2012]. In particular, forgetting has recently received much attention in logic programs under answer sets/stable models semantics - - Answer Set Programming (ASP) [Zhang and Foo, 2006; Eiter and Wang, 2008; Wong, 2009; Wang et al. ], which is one of the major nonmonotonic paradigms for declarative problem solving in Knowledge Representation and Reasoning [Baral, 2003; Brewka et al., 2011].

It is well-known that ASP has two major notions of equivalence: strong equivalence and equivalence. Formally speaking, given two logic programs Π1 and Π2, they are equivalent if they have the same stable models; they are strongly equivalent if Π1 ∪Π and Π2 ∪Π have the same stable models for every logic program Π. The notion of strong equivalence plays an important role in ASP. It acts the same role of equivalence in classical logic and allows to simplify logic programs. By treating a logic program Π as a logical theory ̂Π, the answer sets of Π exactly correspond to the equilibria of ̂Π in equilibrium logic; two logic programs Π and Π′ are strongly equivalent whenever ̂Π and ̂ Π′ are equivalent in the monotonic logic here-and-there (HT) [Lifschitz et al., 2001]. This naturally defines the entailment relationship between logic programs, viz, Π entails Π′ if ̂Π entails ̂ Π′ in HT.

Based on the two notions of equivalence in ASP, several desirable properties have been proposed for forgetting in logic programs, including irrelevance, persistence, existence and so on [Eiter and Wang, 2008; Wong, 2009; Wang et al., 2012], that are outlined in the following. Let L be an ASP language on a signature A, Π a logic program in L, V ⊆ A and f(Π, V ) a result of forgetting about V in Π.

• (E) Existence: f(Π, V ) is expressible in L.
• (IR) Irrelevance: f(Π, V ) is irrelevant to V , i.e., it needs not mention any variables in V .
• (W) Weakening: Π entails f(Π, V ).
• (PP) Positive Persistence: if Π entails Π′ which is irrelevant to V then f(Π, V ) entails Π′ .
• (NP) Negative Persistence: if Π does not entail Π′ which is irrelevant to V then f(Π, V ) does not entail Π′ .
• (SE) Strong Equivalence: If Π andΠ′ are strongly equivalent, then f(Π, V ) and f(Π′ , V ) are strongly equivalent.
• (CP) Consequence Persistence: f(Π, V ) has an answer set X′ whenever Π has an answer set X such that X′ = X \ V .

Zhang and Zhou (2009) firstly proposed (W), (PP), (NP) and (IR) for knowledge forgetting in modal logic S5. Wang et al. (2012) adapted them for HT-forgetting in logic programs, for which both (E) and (SE) were proved being satisfied. However, HT-forgetting fails for (SE). The property (CP) is originally proposed by Eiter and Wang (2008) for a semantical forgetting in disjunctive logic programs in which X′ must be minimal under set inclusion in order to guarantee (E). The semantic forgetting satisfies (IR), but none of (W), (PP), (NP) and (SE).

Skeptical reasoning and credulous reasoning are two major reasoning tasks in ASP 1 . The property (CP) means that the forgetting operator f preserves skeptical and credulous consequences. Recall that strong equivalence allows for simplification of logic programs. The properties (SE) and (CP) are important and useful for various applications, such as conflict resolving [Zhang and Foo, 2006; Eiter and Wang, 2008; Lang and Marquis, 2010].

1 An atom p is a credulous (resp. skeptical) consequence of a logic program Π if p belongs to one (resp. all) answer set(s) of Π.

Since ASP is based on the answer sets semantics which is nonmonotonic, there is no consensus about a suitable set of criteria for forgetting in ASP. This phenomenon is also evidenced by the existence of several different definitions of forgetting in ASP. A fundamental question comes out: is there a rational forgetting in logic programs that satisfies all of the seven desirable properties above? The answer is negative, i.e., it is impossible to define a notion of forgetting that satisfies all of the desirable properties listed above. Especially, for any notion of forgetting in ASP, (W) and (NP) will be violated if (IR), (E) and (CP) are satisfied (cf. Proposition 3 in the paper). So, if we want a notion of forgetting in ASP to satisfy the set of desirable properties

then we have to sacrifice (W) and (NP). Due to the nonmonotonicity of ASP, it would be acceptable for a notion of forgetting in ASP not to satisfy (W) and (NP).

Therefore, we argue that F consists of a suitable set of desirable properties for forgetting in ASP. However, none of the extant definitions of forgetting for ASP satisfies all properties in F. For instance, the semantic forgetting in [Eiter and Wang, 2008], the strong and weak forgetting in [Zhang and Foo, 2006] do not enjoy (SE). Among these three notions of forgetting, the first preserves only skeptical consequence but the other two notions of forgetting preserve neither skeptical nor credulous consequence in ASP. In this sense they do not satisfy (CP). Wong (2009) presented two forgetting operators FW and FS for disjunctive logic programs and Wang et al. (2012) defined the HT-forgetting for logic programs. While these proposals satisfy the property (SE), they do not satisfy the desirable property (CP). Some of these issues are illustrated in the following example.

Suppose Eve has a diet recipe which is represented by a logic program Π consisting of

The logic program has two stable models {apple} and {pear}, which correspond to Eve's two diet schemes. In the case that pear is not available any more, her diet schemes naturally turn into {apple} and {}. According to Π, if banana is provided, then plum should be provided too.

In terms of forgetting, if pear is forgotten in Π, we obtain the following results under the semantic forgetting, FW, FS and the HT-forgetting, respectively:

One can see that the information "plum ← banana" is lost in the semantic forgetting; in terms of FW and HT-forgetting, the only diet scheme is {}; it is {apple} in terms of FS.

Therefore, it is an interesting but yet open problem to introduce a notion of forgetting for ASP that obeys all criteria in F.

In this paper, we tackle this problem by proposing a new semantic forgetting for general answer set programs, named SM-forgetting. Our new notion of (semantic) forgetting fulfils all criteria in F while it also satisfies some other useful properties. By this forgetting, we present a positive answer to Gabbay, Pearce and Valverde's open question: can general answer set programs have uniform interpolation property [Gabbay et al., 2011]? We also develop an algorithm for computing SM-forgetting and study complexities for several reasoning tasks induced by SM-forgetting.

2 Preliminaries

We assume a propositional language LA on a finite set A of propositional variables. A is also referred to as the signature of LA. The formulas of LA are inductively constructed using connectives ⊥, ∧, ∨ and ⊃ as the following:

where p ∈ A. The formula ¬ϕ stands for ϕ ⊃ ⊥, while ⊤ for ⊥ ⊃ ⊥. A theory is a set of propositional formulas. In what follows we assume the signature of a formula/theory consisting of the atoms occurring it, unless stated otherwise.

Let S be a finite set of formulas. We denote ∨ S (resp. ∧ S) the disjunction (resp. conjunction) of all formulas in S. Particularly, ∨ ∅ (resp. ∧ ∅) is ⊥ (resp. ⊤). By ¬S (resp. ¬¬S) we mean {¬φ | φ ∈ S} (resp. {¬¬φ | φ ∈ S}).

2.1 HT logic and stable models

The syntax of HT is the same as propositional language but its semantics is different from propositional logic. An HTinterpretation is a pair 〈H, T〉 such that H ⊆ T ⊆ A. The satisfiability relation in HT, written |=HT, is recursively defined in the following,

• 〈H, T〉|=HTp if p ∈ H; 〈H, T〉 ̸|=HT ⊥;
• 〈H, T〉|=HTϕ∨ψ if 〈H, T〉|=HTϕ or 〈H, T〉|=HTψ;
• 〈H, T〉|=HTϕ∧ψ if 〈H, T〉|=HTϕ and 〈H, T〉|=HTψ;
• 〈H, T〉|=HTϕ ⊃ ψ if both (i) T |= ϕ ⊃ ψ, and (ii) 〈H, T 〉|=HTϕ implies 〈H, T 〉|=HTψ

where p ∈ A, ϕ and ψ are formulas. An HT-interpretation 〈H, T〉 is an HT-model of a formula ϕ if 〈H, T〉|=HTϕ. We denote ModHT(ϕ) the set of all HT-models of ϕ. An HTmodel 〈T, T〉 of a formula ϕ is an equilibrium model of ϕ if there is no T ′ ⊂ T such that 〈T ′ , T〉|=HTϕ.

Given two formulas ϕ and ψ, ϕ entails ψ in HT, written ϕ |=HT ψ, if ModHT(ϕ) ⊆ ModHT(ψ); ϕ ̸|=HT ψ means that ϕ does not entail ψ in HT; ϕ and ψ are HT-equivalent, written ψ≡HTϕ, if ModHT(ϕ) = ModHT(ψ). A formula ϕ is HT-irrelevant to a set V of atoms, denoted IRHT(ϕ, V ), if there is a formula ψ not containing any atoms from V such that ϕ≡HTψ. In this case we assume ϕ does not mention any atoms from V , unless explicitly stated otherwise.

A formula of the following form is called a rule:

where A = {a1, . . . , al}, B = {b1, . . . , bk}, C = {c1, . . . , cm} and D = {d1, . . . , dn}. It is also identified as

which is called a nested expression in [Lifschitz et al., 1999]. A rule r of form (3) is disjunctive if n = 0; it is normal if it is disjunctive and l ≤ 1; it is Horn if it is normal and m = 0; it is a constraint if l = 0. A logic program Π is a finite set of rules of form (3). It is disjunctive (resp. normal and Horn) if all of its rules are disjunctive (resp. normal and Horn). The stable models/answer sets semantics of logic programs is attributed to Gelfond and Lifschitz (1988). By identifying every rule r of form (3) as the formula ̂ r of the form (2), it is well-known that a set T of atoms is a stable model/answer set of a logic program Π iff 〈T, T 〉 is an equilibrium model of ̂Π, where ̂Π = {̂ r|r ∈ Π} [Pearce, 1996; Ferraris, 2005].

Let Π be a logic program. By SM(Π) we denote the set of all stable models of Π. Π is consistent if SM(Π) ̸= ∅. If Π is disjunctive then SM(Π) forms an antichain, i.e., no two elements of SM(Π) are comparable under set inclusion. An atom p is a skeptical (resp. credulous) consequence of Π, denoted by Π |=s p (resp. Π |=c p), if p ∈ ⋂ SM(Π) (resp. p ∈ ⋃ SM(Π)). A logic programs Π′ is equivalent to Π, written Π′ ≡SM Π, if SM(Π′ ) = SM(Π); Π′ is strongly equivalent to Π if SM(Π ∪ Π′′ ) = SM(Π′ ∪ Π′′ ) for every logic program Π′′ . It is well-established that two logic programs are strongly equivalent iff their corresponding theories are HT-equivalent in HT [Lifschitz et al., 2001]. Since very formula in HT can be translated into a conjunction of formulas of the form (2), we will not distinct logic programs from formulas in the following.

2.2 Forgetting and HT-forgetting

By an interpretation we mean a set of atoms. The complement of an interpretation M, written M, is the set A \ M. The complement of a collection M of (HT-)interpretations, denoted byM, is the set of (HT-)interpretations not inM.

Let V ⊆ A and X an interpretation. An interpretation Y is V -bisimilar to X, written Y ∼V X, if Y \ V = X \ V . The V -extension of X, denoted by X†V , is the collection of interpretations that are V -similar to X. Two HT-interpretations 〈H, T〉 and 〈X, Y 〉 are V -bisimilar, denoted by 〈H, T〉 ∼V 〈X, Y 〉, if H ∼V X and T ∼V Y . The V -extension of an HT-interpretation 〈H, T 〉, denoted by 〈H, T 〉†V , is the collection of HT-interpretations that are V -similar to 〈H, T〉. The V -extension of a collectionMof (HT-)interpretations is the collection ⋃β∈M β†V .

The forgetting in propositional logic [Lin and Reiter, 1994] can be equivalently reformulated as following:

Definition 1 (forgetting) Let ϕ be a formula and V ⊆ A. A formula ψ is a result of forgetting V in ϕ if and only if Mod(ψ) = Mod(ϕ)†V .

Such a forgetting result ψ is unique up to equivalence. We denote it by Forget(ϕ, V ).

Similarly, the HT-forgetting in [Wang et al., 2012] can be equivalently reformulated as following:

Definition 2 (HT-forgetting) Let ϕ be a formula and V ⊆ A. A formula ψ is a result of HT-forgetting V in ϕ if and only if ModHT(ψ) = ModHT(ϕ)†V .

It is proved (cf. Theorem 1 of [Wang et al., 2012]) that such a formula ψ always exists, it is unique up to HT-equivalence and it is HT-irrelevant to V . It is denoted by ForgetHT(ϕ, V ).

3 SM-Forgetting

In this section we introduce a new notion of semantic forgetting for logic programs, called SM-forgetting, and study its properties, algorithm and computational complexity.

3.1 Definition and properties

Let V ⊆ A and X an interpretation. The V -exclusion of X, written X‖V , is the set X\V . The V -exclusion of a collection Mof interpretations is {X‖V |X ∈M}, denoted byM‖V .

Definition 3 (SM-forgetting) Let ϕ be a formula and V ⊆ A. A formula ψ is a result of SM-forgetting V in ϕ if and only if ModHT(ψ) is a maximal subset of ModHT(ϕ)†V such that SM(ψ) = SM(ϕ)‖V .

Example 1 For the logic programΠ in Section 1, the following logic program is a result of SM-forgetting pear in Π:

It has two stable models ∅ and {apple}, which correspond to the two intended diet schemes for Eve after forgetting pear. In particular, we note that the knowledge "plum ← banana" of Π, which is irrelevant to pear, is preserved in the result.

The next theorem shows that the result of SM-forgetting a set V of atoms in a formula ϕ exists, and it is unique up to strong equivalence. We denote it by ForgetSM(ϕ, V ).

Theorem 1 (Existence of SM-forgetting) Given any formula ϕ and any set V of atoms, there exists a result of SMforgetting V in ϕ. Moreover, if both ψ and ψ′ are results of SM-forgetting V in ϕ, then ψ and ψ′ are strongly equivalent.

Proof sketch: We denote that

A collection M of HT-interpretations is called HT-valid if there is a logic program Π such that M is the set of HTmodels of Π. It is shown in [Cabalar and Ferraris, 2007] that a collectionMof HT-interpretations is HT-valid iff

We can show that N satisfies (7) and thus, it is HT-valid. Let ModHT(ψ) = N . Removing the HT-interpretations in G ∪ H from ModHT(ϕ)†V assures that the stable models of ψ are exactly the elements of SM(ϕ)‖V .

Recall that ForgetHT(ϕ, V )≡HT{ξ|ϕ|=HTξ & IRHT(ξ, V )} (cf. Theorem 3 of [Wang et al., 2012]). By the construction of ForgetSM(ϕ, V ) in the proof of the above theorem, we have the following proposition.

Proposition 1 The SM-forgetting satisfies the properties (E), (IR), (SE), (CP) and (PP).

The next proposition shows that the SM-forgetting preserves equivalence. Under an additional condition, it satisfies knowledge weakening in the sense that ϕ|=HTψ implies ForgetSM(ϕ, V )|=HTForgetSM(ψ, V ).

Proposition 2 Let ϕ, ψ be two formulas and V ⊆ A. Then

The condition SM(ϕ)‖V = SM(ψ)‖V is necessary for the statement (ii) in the above proposition. Otherwise, let ϕ = p ∧ ¬q ⊃ ⊥ and ψ = ¬q ⊃ (p ∨ ¬p). One can verify that ϕ|=HTψ, ForgetSM(ϕ, {q})≡HT⊤ but ForgetSM(ψ, {q})≡HTp ∨ ¬p.

As illustrated in the following example, the properties (W) and (NP) may not be satisfied by SM-forgetting.

Example 2 Let us consider the following formulas.

• Let ψ = q ∧ (¬p ⊃ p). It is not difficult to see that, on the signature {p, q}, ModHT(ψ) = {〈{q}, {p, q}〉, 〈{p, q}, {p, q}〉} and then ψ has no stable model. One can verify that

It is evident that ψ|=HTForgetSM(ψ, {q}), but not vice versa; and ForgetSM(ψ, {p})|=HTψ, but not vice versa. It implies that SM-forgetting does not satisfy (W) for ψ.

• Let ϕ = (p∨¬p∨q∨¬q)∧(p ⊃ q∨¬q)∧(q ⊃ p∨¬p). One can check that SM(ϕ) = {∅, {p, q}}, and

Since 〈∅, {q}〉 is an HT-model of ϕ but ϕ′ , it follows ϕ ̸|=HT ϕ′ . Moreover 〈{q}, {p, q}〉 is an HT-model of ϕ′ but not an HT-model of ϕ, it shows ϕ′ ̸|=HT ϕ. Thus ϕ is not comparable with ϕ′ in HT. It implies that SMforgetting falsifies (W) and (NP) for ϕ.

Actually, on the signature {q}, q∨¬q is the only formula (up to HT-equivalence) having the stable models ∅ and {q}. In other words, there is no ψ∗ (on the signature

This example shows that, to ensure (IR), (E) and (CP) of a forgetting in answer set programming, one cannot demand (W) or (NP), no matter logic programs are consistent or not.

Proposition 3 There is no forgetting for ASP satisfies (W) or (NP) that satisfies (IR), (E) and (CP).

To satisfy the property (W), the next proposition presents a sufficient and necessary condition for the SM-forgetting.

Proposition 4 Let ϕ be a formula and V ⊆ A. Then we have ϕ|=HTForgetSM(ϕ, V ) iff, for every Y ⊆ A,

• 〈X, Y 〉 ̸|=HT ϕ for every X ⊂ Y if Y ∈ SM(ϕ)‖V ,
• Y |= ϕ implies 〈X, Y 〉|=HTϕ for some X ⊂ Y , otherwise.

The following result guarantees that SM-forgetting a set V of atoms can be done through SM-forgetting one atom by one atom in V and it is irrelevant to the order of atoms.

Theorem 2 Let ϕ be a formula, V1, V2 two sets of atoms. ForgetSM(ϕ, V1 ∪ V2)≡HTForgetSM(ForgetSM(ϕ, V1), V2).

Proof sketch: Let's denote

We can show that, if Y /∈ SM(ϕ)‖V then

The remain is to prove 〈X, Y 〉|=HTψ iff 〈X, Y 〉|=HTψ2 by two cases Y ∈ SM(ϕ)‖V and Y /∈ SM(ϕ)‖V .

3.2 Expressibility in disjunctive logic programs

Recall that the results of SM-forgetting are expressible in general (propositional) logic programs by Theorem 1. In this subsection we investigate the validity of this result for smaller classes of logic programs, including disjunctive logic programs and Horn logic programs.

Recall that Eiter et al. (2005) and Wong (2009) showed that a collection M of HT-interpretations is disjunctive HTvalid, i.e., there is a disjunctive logic program Π such that ModHT(Π) =M, iffMsatisfies (7) and the condition:

The next example shows that SM-forgetting results for some important classes of logic programs, including normal programs with and without constraints, are not expressible in disjunctive logic programs. Thus SM-forgetting results for disjunctive logic programs may be not expressible in disjunctive logic programs yet.

Example 3 Consider the following normal logic programs.

• Let Π1 consists of

It has two stable models {p, r} and {q, r}. We have

The stable models of ForgetSM(Π1, {q}) are {r} and {p, r}, that cannot form an antichain. Thus, there is no disjunctive logic program (on the signature {p, r}) that can capture ForgetSM(Π1, {q}), even if ForgetHT(Π1, {q}) is disjunctive.

• Let Π2 = {← p, q, r; ← p, q, not r}. Its unique stable model is ∅. We have

≡HT{p ∨ q ← not not p, not not q}, which cannot be captured by a disjunctive logic program (on the signature {p, q}), even if SM(Π)‖V forms an antichain. The reason is that 〈∅, ∅〉 and 〈{p, q}, {p, q}〉 are HT-models of ForgetSM(Π2, {r}), but 〈∅, {p, q}〉 is not.

We present a sufficient and necessary condition for the disjunctive expressibility of SM-forgetting results.

Proposition 5 Let ϕ be a formula and V ⊆ A. There is a disjunctive logic program Π such that Π≡HTForgetSM(ϕ, V ) iff, for every HT-models 〈X1, Y1〉, 〈Y2, Y2〉 of ϕ such that Y1 ⊆ Y2, there exists an HT-model 〈X3, Y3〉 of ϕ such that 〈X3, Y3〉 ∼V 〈X1, Y2〉 and, noM ∈ SM(ϕ) withM ∼V Y3.

For Horn logic programs, SM-forgetting has an interesting property, which implies that SM-forgetting results in Horn logic programs can be expressed in Horn logic programs and thus expressible in disjunctive logic programs.

Theorem 3 Let Π be a Horn logic program and V ⊆ A. Then ForgetSM(Π, V )≡HTForgetHT(Π, V ).

Proof sketch: Firstly we can show that X is the least model of Π iff X \ V is the least model of ForgetHT(Π, V ).

Secondly we denote:

N = ModHT(Π)†V .

It is evident that H = ∅. We can further show N ∩ G = ∅.

As HT-forgetting results of Horn logic programs are Horn expressible and HT-forgetting enjoys "modularity" (cf. Theorem 2 and (vi) of Proposition 3 in [Wang et al., 2012] respectively). The following corollary follows by Theorem 3.

Corollary 4 Let Π, Π′ be Horn logic programs and V ⊆ A.

• (i) ForgetHT(Π, V ) is Horn expressible;
• (ii) ForgetSM(Π ∪ Π′ , V )≡HTForgetSM(Π, V ) ∪ Π′ if IRHT(Π′ , V ).

3.3 Relation to other forms of forgetting

In this subsection, we first reveal a connection between SMforgetting and HT-forgetting and then provide two results on relationships of SM-forgetting with the forgetting in propositional logic and a uniform interpolation for answer set programs respectively.

Proposition 6 Let ϕ be a formula and V ⊆ A. Then we have ForgetSM(ϕ, V )≡HTForgetHT(ϕ, V ) if and only if SM(ForgetHT(ϕ, V )) = SM(ϕ)‖V .

The notion of loop formulas plays an important role in ASP [Lin and Zhao, 2004]. As stable models of a logic program Π can be captured by models of its loop formulas LF(Π) in propositional logic (cf. Theorem 2 of [Ferraris et al., 2006]). Accordingly the following proposition partly connects SMforgetting with the forgetting in propositional logic.

Proposition 7 Let Π be a logic program and V a set of atoms. Then X is a stable model ForgetSM(Π, V ) iff X is a model of Forget(LF (Π), V ).

Uniform interpolation. In monotonic logics, forgetting is closely related to uniform interpolation [Visser, 1996]. Gabbay et al. (2011) show that the class of disjunctive logic programs enjoys the uniform interpolation property with queries being disjunctions of literals. They first introduced a (nonmonotonic) inference |∼ between formulas in ASP:

A class of formulas in ASP has the uniform interpolation property iff for any formula ϕ and any set V of atoms, there is a formula ψ such that the following conditions hold:

• (ii) for any formula α with var(α) ∩ V = ∅,

where var(α) is the set of atoms occurring in α.

Gabbay et al. (2011) showed that the class of disjunctive logic programs enjoy the uniform interpolation property 2 and they raised an interesting open question: Given a signature A, does LA, the class of all formulas in ASP, possess the uniform interpolation property too?

This open question can be affirmatively answered.

Proposition 8 Let A be a set of atoms. Then LA, the class of all formulas in ASP, has the uniform interpolation property.

3.4 Computation for SM-forgetting

According to Theorem 1 and the notion of countermodels 3 in here-and-there [Cabalar and Ferraris, 2007], we present an algorithm to compute SM-forgetting result - Algorithm 1, where the underlying signature A consists of the atoms occurring in Π and λX,Y denotes the following formula:

In particular, λY,Y = ∧ Y ∧ ∧ ¬Y ⊃ ⊥ since ∨ ∅ is ⊥.

Recall that λY,Y captures the countermodel 〈Y, Y 〉 of Π, while λX,Y captures the countermodel 〈X, Y 〉 of Π where X ⊂ Y and 〈Y, Y 〉 is an HT-model of Π. The intuition of the algorithm is as follows:

1. The foreach loop (Lines 3-5) ensures all stable models in SM(Π) are preserved when V is forgotten.
2. The foreach loop (Lines 6-22) asserts no other stable models for Σ by Lines 17 and 20.
3. The foreach loop (Lines 9-15) removes the countermodel 〈X, Y 〉 that cannot be derived from Π.

Theorem 5 Algorithm 1 outputs ForgetSM(Π, V ).

In the algorithm, since SM(Π) is possibly exponential in the size of |Π| and the foreach loop (Line 9) considers all subsets of Y , it outputs an exponentially larger size logic program in the worst case.

Example 4 Let's consider Π1 from Example 3 where A = {p, q, r}. Let V = {q}. Note that M = {{p, r}, {q, r}} and M‖V = {{p, r}, {r}}. Now Σ is constructed as follows:

2 The query α in (9) is restricted being a disjunction of literals.

3 An HT-interpretation is a countermodel of a formula ϕ if it not an HT-model of ϕ.

Algorithm 1: SM-forgetting

input : A logic programΠ and a set V of atoms output: A result of SM-forgetting V in Π 1 Σ← ∅; 2 M← SM(Π)‖V ; 3 foreach Y ∈Mdo 4 foreach X ⊂ Y do Σ ← Σ ∪ {λX,Y }; 5 ; 6 end 7 foreach Y /∈Mdo 8 if ∃Y ′ |= Π s.t Y ′ ∼V Y then 9 if ∃〈X′ , Y ′ 〉|=HTΠ s.t Y ′ ∼V Y and X′ \ V ⊂ Y then 10 foreach X ⊂ Y do 11 if ∃〈H, T〉|=HTΠ s.t 〈H, T〉 ∼V 〈X, Y 〉 then 12 Continued; 13 else 14 Σ ← Σ ∪ {λX,Y }; 15 end 16 end 17 else 18 Σ ← Σ ∪ {λY,Y }; 19 end 20 else 21 Σ ← Σ ∪ {λY,Y }; 22 end 23 end 24 return Σ;

1. According to Lines 3-5 of Algorithm 1, Σ includes:
2. For ∅ /∈M, the two sets ∅ and {q} are not models of ϕ, according to Lines 6-22, Σ includes ¬p ∧ ¬r ⊃ ⊥.
3. For {p} /∈ M, the two sets {p} and {p, q} are not models of ϕ, according to Lines 6-22, Σ contains p ∧ ¬r ⊃ ⊥.

p ∨ r ∨ ¬p ∨ ¬r, p ⊃ r ∨ ¬r, r ⊃ p ∨ ¬p, ¬p ⊃ r ∨ ¬r.

One can further verify that Σ≡HT(p ∨ ¬p) ∧ r.

3.5 Some complexity results

It is known that the credulous and skeptical reasoning problem of ASP is ΣP2 -complete and ΠP2 -complete respectively, and the consistency problem (i.e., deciding if a formula has a stable model) is ΣP2 -complete (cf. Theorem 10 of [Pearce et al., 2009]). The following corollary follows.

Corollary 6 Let Π be a (disjunctive) logic program, V a set of atoms and p an atom not in V . The following hold:

(i) deciding if SM(ForgetSM(Π, V )) ̸= ∅ is ΣP2 -complete. (ii) deciding if ForgetSM(Π, V ) |=s p is ΠP2 -complete, (iii) deciding if ForgetSM(Π, V ) |=c p is ΣP2 -complete.

As noted in the previous section that the algorithm of computing SM-forgetting result is quite expensive, this might not be avoided generally in terms of the following theorem.

Theorem 7 Let Σ and Π be two logic programs, V ⊆ A.

• (i) Deciding if Σ≡HTForgetSM(Π, V ) is ΠP2 -complete.
• (ii) Deciding if Σ≡HTForgetSM(Π, V ) is co-NP-complete if both Σ and Π are Horn logic programs.

Proof sketch: (i) Membership: If Σ ̸≡HT ForgetSM(Π, V ) then there exists an HT-interpretation 〈X, Y 〉 such that either (a) 〈X, Y 〉|=HTΣ and 〈X, Y 〉 ̸|=HT ForgetSM(Π, V ), or (b) 〈X, Y 〉 ̸|=HT Σ and 〈X, Y 〉|=HTForgetSM(Π, V ). We consider the case (a). The case (b) is similar.

Note that checking if 〈X, Y 〉|=HTΣ is feasible in polynomial time of Σ. Moreover, 〈X, Y 〉 ̸|=HT ForgetSM(Π, V ) iff either (i.a) 〈X, Y 〉 ̸|=HT ForgetHT(Π, V ), X ⊂ Y and Y ∈ SM(Π)‖V , or (i.b) X = Y and Y ∈ SM(ForgetHT(Π, V )) \ SM(Π)‖V . The case (i.a) is feasible in polynomial by calling an NP-oracle. We consider the case (i.b). Note further that Y ∈ SM(ForgetHT(Π, V )) iff Y |= ForgetHT(Π, V ), which is feasible in polynomial time of Π by calling an NPoracle, and 〈X, Y 〉 ̸|=HT ForgetHT(Π, V ) for every X ⊂ Y , whose complement is 〈X, Y 〉|=HTForgetHT(Π, V ) for some X ⊂ Y iff there is 〈X′ , Y ′ 〉|=HTΠ such that Y ∼V Y ′ and X′ \ V ⊂ Y , which is feasible in polynomial time of Π by calling an NP-oracle as well.

Note that Σ≡HTForgetSM(Π, V ) iff (a) Σ|=HTForgetHT(Π, V ), (b) SM(Σ) = SM(Π)‖V and (c) there is no Σ′ such that ModHT(Σ) ⊂ ModHT(Σ′ ) and Σ′ satisfies the conditions (a) and (b) in the place of Σ. Its hardness follows from the fact that the condition (a) is ΠP2 -complete (cf. (ii) of Theorem 5 in [Wang et al., 2012]).

• (ii) The membership is proved by showing 〈H, T〉|=HTForgetSM(Π, V ) iff the least model M of Π satisfies the condition M‖V ⊆ H ∩ T. Its hardness follows from the fact that Σ≡HTForgetSM(Π, V ) iff Σ ≡ Forget(Π, V ) which is co-NP-complete.

4 Concluding Remarks and FutureWork

In this paper, we presented a new semantic forgetting for general logic programs based on stable models semantics, called SM-forgetting. Different from the other forgetting for logic programs, it preserves skeptical and credulous consequence on unforgotten variables and (strong) equivalence. This provides a positive answer to Gabbay, Pearce and Valverde's open question (2011). Its properties, algorithm and computational complexities are extensively explored.

Though this forgetting is developed for answer set programs, we believe that the proposed criteria should somehow be also respected by a semantic forgetting in other nonmonotonic logic systems, which deserves our further efforts.

Acknowledgement

We thank reviewers for their helpful comments. This work was partially supported by the Australia Research Council (ARC) grants DP1093652 and DP110101042. Yisong Wang was also partially supported by NSFC grant 60963009, Open Funds of the State Key Laboratory of Computer Science of Chinese Academy of Science grant SYSKF1106 and Stadholder Fund of Guizhou Province grant (2012)62.