# knowledge_forgetting_in_answer_set_programming__45e02225.pdf

Journal of Artificial Intelligence Research 50 (2014) 31-70 Submitted 08/13; published 05/14

Knowledge Forgetting in Answer Set Programming

Yisong Wang CSC.YSWANG@GZU.EDU.CN Department of Computer Science, Guizhou University, Guiyang, China

Yan Zhang YAN@SCEM.UWS.EDU.AU Yi Zhou YZHOU@SCEM.UWS.EDU.AU Artificial Intelligence Research Group, University of Western Sydney, Australia

Mingyi Zhang ZHANGMINGYI045@GMAIL.COM Guizhou Academy of Sciences, Guiyang, China

The ability of discarding or hiding irrelevant information has been recognized as an important feature for knowledge based systems, including answer set programming. The notion of strong equivalence in answer set programming plays an important role for different problems as it gives rise to a substitution principle and amounts to knowledge equivalence of logic programs. In this paper, we uniformly propose a semantic knowledge forgetting, called HTand FLP-forgetting, for logic programs under stable model and FLP-stable model semantics, respectively. Our proposed knowledge forgetting discards exactly the knowledge of a logic program which is relevant to forgotten variables. Thus it preserves strong equivalence in the sense that strongly equivalent logic programs will remain strongly equivalent after forgetting the same variables. We show that this semantic forgetting result is always expressible; and we prove a representation theorem stating that the HTand FLP-forgetting can be precisely characterized by Zhang-Zhou s four forgetting postulates under the HTand FLP-model semantics, respectively. We also reveal underlying connections between the proposed forgetting and the forgetting of propositional logic, and provide complexity results for decision problems in relation to the forgetting. An application of the proposed forgetting is also considered in a conflict solving scenario.

1. Introduction

Motivated by Lin and Reiter s seminal work (Lin & Reiter, 1994), the notion of forgetting in propositional and first-order logics distilling from a knowledge base only the part that is relevant to a subset of the alphabet has attracted extensive interests in the KR community, (e.g., see Lang & Marquis, 2010; Zhou & Zhang, 2011). In recent years, researchers have developed forgetting notions and theories in other non-classical logic systems from various perspectives, such as forgetting in description logics (Kontchakov, Wolter, & Zakharyaschev, 2008; Wang, Wang, Topor, & Pan, 2010; Lutz & Wolter, 2011; Packer, Gibbins, & Jennings, 2011), forgetting in logic programs (Zhang & Foo, 2006; Eiter & Wang, 2008; Wong, 2009; Wang, Wang, & Zhang, 2013), and forgetting in modal logic (Zhang & Zhou, 2009; Su, Sattar, Lv, & Zhang, 2009; van Ditmarsch, Herzig, Lang, & Marquis, 2009; Liu & Wen, 2011). As a logical notion, forgetting has also been studied under some different terms such as variable elimination (Lang, Liberatore, & Marquis, 2003), irrelevance, independence, irredundancy, novelty, or separability (Bobrow, Subramanian, Greiner, &

c 2014 AI Access Foundation. All rights reserved.

WANG, ZHANG, ZHOU, & ZHANG

Pearl, 1997). It has been shown that in the study of modeling agents behaviors, forgetting plays an important role in conflict resolution (Zhang & Foo, 2006; Lang & Marquis, 2010). In propositional logic, the result of forgetting an atom p from a formula ϕ, written Forget(ϕ, {p}), is the formula ϕ[p/ ] ϕ[p/ ], where ϕ[p/ ] and ϕ[p/ ] is the formula obtained from ϕ by replacing each occurrence of atom p with (false) and (true) respectively. Forgetting a set of atoms from a formula ϕ is defined as Forget(ϕ, V {p}) = Forget(Forget(ϕ, {p}), V ) (Lin, 2001). It is easy to see that the forgetting preserves logical equivalence. That is, logically equivalent formulas (theories) will remain logically equivalent after forgetting the same atoms. It is well known that, if ψ does not mention any atoms from V then

ϕ |= ψ iff Forget(ϕ, V ) |= ψ.

In this sense the forgetting in propositional logic, called propositional forgetting, is a knowledge forgetting since Forget(ϕ, V ) exactly contains the logical content of ϕ that is irrelevant to V . For logic programs under stable model/answer set semantics (Gelfond & Lifschitz, 1988), the issue of logical equivalence is rather complicated due to its different notions of equivalence : (weak) equivalence and strong equivalence. Two logic programs Π1 and Π2 are (weakly) equivalent if and only if Π1 and Π2 have the same stable models; Π1 and Π2 are strongly equivalent if and only if Π1 Π and Π2 Π are equivalent for every logic program Π. It is well known that strong equivalence is an important concept in answer set programming (ASP), because it amounts to knowledge equivalence which captures the logical content of a logic program (Osorio & Zacarias, 2004; Osorio & Cuevas, 2007; Delgrande, Schaub, Tompits, & Woltran, 2013), and can be used for simplifying logic programs where two strongly equivalent rules may be interchangeable without affecting the original logic programs stable models (Pearce, Tompits, & Woltran, 2001; Ferraris, Lee, & Lifschitz, 2011; Lin & Chen, 2007; Lin & Zhou, 2011). The strong equivalence can be characterized in the logic here-and-there (HT), viz, two logic programs are strongly equivalent if and only if they have the same HT-models (Lifschitz, Pearce, & Valverde, 2001). For instance, a rule of the following form p p ϕ has the same HT-models as that of (tautology), where ϕ can be an arbitrary formula. Thus it can be safely removed from every logic programs without changing their stable models. Besides the stable model/answer set semantics of logic programs (Gelfond & Lifschitz, 1988),

FLP-stable model semantics also steadily gains its importance (Faber, Pfeifer, & Leone, 2011; Truszczynski, 2010). The notion of strong equivalence is similarly generalized to logic programs under FLP-stable models semantics: two theories Π1 and Π2 are strongly FLP-equivalent if and only if Π1 Π and Π2 Π have the same FLP-stable models for every logic program Π. It is shown that this strong equivalence can be characterized in terms of FLP-models, viz, two logic programs are strongly FLP-equivalent if and only if they have the same FLP-models (Truszczynski, 2010). When we develop the notion of forgetting in logic programs, preserving strong equivalence is important, like that the propositional forgetting preserves equivalence of propositional logic. Consider that two agents need to achieve an agreement for a certain goal, where each agent s knowledge base is represented by a logic program. Suppose that there are two consistent1 logic programs, but their combination is inconsistent. To achieve a consistent combination, one may forget some atoms from each of the logic programs, so that the combination of their forgetting results is consistent. Then forgetting may be effectively used to solve the conflict between the two agents knowledge

1. A logic program is consistent if it has some stable models.

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

bases (Zhang & Foo, 2006; Eiter & Wang, 2008; Lang & Marquis, 2010). For the purpose of simplicity, on the other hand, agents may also replace their knowledge bases with strongly equivalent but syntactically simpler ones. Let us consider a simple Yale Shooting scenario where the logic program Π consisting of the following rules:2

shoot not aux; aux not shoot; aux, shoot.

Here aux is used to generate possible occurrences of action shoot. One can be interested in which logic program represents the same knowledge as that of Π when the auxiliary atom aux is ignored. This intuitively results in a logic program Π consisting of the rule3:

shoot not not shoot,

which captures exactly the knowledge of Π that is irrelevant to aux. We will see that Π can be obtained from Π by HT-forgetting aux (cf. Example 5 with other atom names), while it cannot be obtained in terms of previous forgetting approaches in logic programming (cf. Example 11). It turns out that preserving strong equivalence in forgetting is challenging. There have been several attempts to define the notion of forgetting in logic programs, but none of these approaches is fully satisfactory. Zhang and Foo (2006) first defined syntax oriented weak and strong forgetting notions for normal logic programs. But these forgetting notions preserve neither (weak) equivalence nor strong equivalence. Eiter and Wang (2008) then proposed a semantic forgetting for consistent disjunctive logic programs, which preserves equivalence but not strong equivalence. They specifically indicated the importance of preserving strong equivalence in logic programming forgetting and raised this issue as a future work. Wong (2009) proposed two forgetting operators for disjunctive logic programs. Although the two operators indeed preserve strong equivalence, it may lose the intuition of weakening under various circumstances (see Section 5 for details). A recently proposed forgetting for logic programs may introduce extra knowledge (cf., see Wang et al., 2013, Ex. 2). Thus it is not a knowledge forgetting. Together with preserving strong equivalence, expressiveness is another desired criterion for logic programming forgetting. Ideally we would expect that the result of forgetting some atoms from a logic program is still expressible by a logic program. This is particularly necessary when we view agents knowledge bases as logic programs and forgetting is employed as a means of conflict solving among these agents knowledge bases (Zhang & Foo, 2006). While previous logic programming forgetting approaches all meet this criterion, as we will see in this paper, once we consider forgetting in arbitrary logic programs, retaining expressibility is challenging objective to achieve for a semantic forgetting notion. Finally, we believe that as a way of weakening, knowledge forgetting in logic programs should obey some common intuitions shared by forgetting in classical logics. For instance, forgetting something from a logic program should lead to a weaker program in certain sense. On the other hand, such weakening should only be associated to the relevant information that has been forgotten. For this purpose, Zhang and Zhou (2009) proposed four forgetting postulates to formalize these common intuitions and showed that forgetting in propositional logic and modal logic S5 can be precisely captured by these postulates. Surprisingly, none of previous forgetting notions in logic

2. This is due to one of the anonymous reviewers. 3. The rule is strongly equivalent to the choice rule 0{shoot}1 but it is not a normal rule.

WANG, ZHANG, ZHOU, & ZHANG

programs actually satisfies Zhang-Zhou s postulates. In this sense these previous forgetting notions for logic programs are not knowledge forgetting operators. In summary, we consider the following criteria that a knowledge forgetting notion in logic programs should meet:

Expressibility. The result of forgetting in an arbitrary logic program should also be expressible via a logic program;

Preserving strong equivalence. Two strongly equivalent logic programs should remain strongly equivalent after forgetting the same variables;

Satisfying common intuitions of forgetting. Preferably, forgetting in logic programs should be semantically characterized by Zhang-Zhou s four forgetting postulates.

In this paper we present a comprehensive study on knowledge forgetting in the context of arbitrary logic programs (propositional theories) under stable model and FLP-stable models semantics, called HTand FLP-forgetting respectively. We show that the HTand FLP-forgetting meet all above criteria, and hence have primary advantages when compared to previous logic program forgetting notions. The main contributions of the paper may be summarized as follows, where {HT, FLP},

- As a starting point, we investigate the model theoretical characterization for strong equivalence of logic programs under stable model and FLP-stable model semantics, and explore their strong equivalence by the equivalence in propositional logic.

- We propose a semantic -forgetting for logic programs under -stable model semantics respectively. Here HT-stable model means stable model. The -forgetting result is always expressible via a logic program and it preserves strong equivalence under stable model and

FLP-stable model semantics.

- We investigate semantic properties of the -forgetting, and show that the -forgetting satisfies Zhang-Zhou s four postulates under the -model respectively. In particular, the forgetting result consists of the logical content that is irrelevant to forgotten atoms.

- We establish the underlying connections between -forgetting and propositional forgetting, based on which we provide complexity results for some decision problems in relation to - forgetting. In particular, we show that resulting checking deciding if a logic program is a result of -forgetting a set of atoms from a logic program is ΠP 2 -complete, while the related inference problem in terms of -forgetting varies from co-NP-complete to ΠP 2 -complete.

The theoretical negative results confirm that it is not a easy task to simplify logic programs by forgetting. But fortunately, this kind of simplification can be computed offline in general. For instance, a problem domain description involves a lot of auxiliary propositional variables. One can firstly simplify the description by forgetting (part of) the auxiliary propositional variables, like a kind of compilation (Lang et al., 2003).

- Finally we consider an application of knowledge forgetting in the solving of conflicts in the context of logic programming.

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

The rest of the paper is organized as follows. Section 2 briefly reviews necessary concepts and notions of answer set programming. Section 3 presents the characterizations for strong equivalence of logic programs. We firstly present a uniform definition of the knowledge forgetting for logic programs in section 4, and then explore their expressibility, forgetting postulates, relationship with propositional forgetting, computational complexity and an application of knowledge forgetting in conflict solving. Section 5 discusses other forgetting approaches in logic programs, and finally, Section 6 concludes the paper with some remarks. All the proofs in the paper are deferred to Appendix for clarity. This paper is the revised and extended version of a paper which appeared in Proceedings of KR 2012 (Wang, Zhang, Zhou, & Zhang, 2012).

2. Answer Set Programming

In this section we briefly recall the basic notions of logic programming under stable model semantics, including its syntax, reduction, stable model (Ferraris, 2005) and FLP-stable models (Truszczynski, 2010) and strong equivalence (Lifschitz et al., 2001; Truszczynski, 2010). In the paper a stable model is called an HT-stable model for convenience, and we assume {HT, FLP}. We assume a propositional language LA over the finite set A of propositional atoms, which is called the signature of the language LA.

The formulas of LA are built from the signature4 A and the 0-place connective ( false ) using the binary connectives , and as follows:

ϕ ::= | p | ϕ ϕ | ϕ ϕ | ϕ ϕ (1)

where p A. ( true ) is the shorthand of , ϕ for ϕ , and ψ φ for (ψ φ) (φ ψ). A theory is a set of formulas. An interpretation is a set I of atoms from A, where each atom of A is viewed to be true if it is in I, and false otherwise. In propositional logic, the notions of model and satisfaction relation |= are defined as usual. In the following we denote A \ X by

X for X A, Mod(ϕ) for {M|M |= ϕ}, ϕ ψ for Mod(ϕ) = Mod(ψ) (i.e. ϕ is equivalent to ψ) and

M for {I A|I / M} where M 2A. A formula ϕ is irrelevant to a set V of atoms, written IR(ϕ, V ), if there exists a formula ψ mentioning no atoms from V such that ϕ ψ. For convenience, we also define the following notations. Let S be a finite set of formulas. We denote W S (resp. V S) the disjunction (resp. conjunction) of all formulas in S, where W denotes and V denotes , and |S| the cardinality of S. Similarly by S (resp. S) we mean { φ | φ S} (resp. { φ | φ S}).

2.2 Reduct and Stable Models

Let ϕ be a formula and X A. The -reduct of ϕ w.r.t. X, written Red (ϕ, X), is recursively and uniformly defined as follows:

4. In the rest of this paper, whenever there is no confusion, we may not explicitly mention the signature when we talk about formulas of LA.

WANG, ZHANG, ZHOU, & ZHANG

( -R1) Red ( , X) = ;

( -R2) Red (p, X) = p if X |= p, and otherwise;

( -R3) Red (ϕ1 ϕ2, X) = Red (ϕ1, X) Red (ϕ2, X) if X |= ϕ1 ϕ2 where { , }, and otherwise;

(HT-R4) Red HT(ϕ1 ϕ2, X) = Red HT(ϕ1, X) Red HT(ϕ2, X) if X |= ϕ1 ϕ2, and otherwise;

(FLP-R4) Red FLP(ϕ1 ϕ2, X) =

ϕ1 Red FLP(ϕ2, X), if X |= ϕ1 ϕ2; , if X |= ϕ1; , otherwise (i.e. X |= ϕ1 ϕ2).

Definition 1 A set X A is a -stable model of a formula ϕ if X is a minimal (under set inclusion) model of Red (ϕ, X). We denote the set of -stable models of ϕ by SM (ϕ).

Please note that, traditionally, the HT-reduct is named reduct ; Red HT(ϕ, X) is written as ϕX ;

HT-stable model is called stable model (Ferraris, 2005); and Red FLP(ϕ, X) is written as ϕX

(Truszczynski, 2010). It is known that, HT-stable models and FLP-stable models are not comparable in the sense that some HT-stable models are not FLP-stable models, and some FLP-stable models are not HT-stable models (cf., see Truszczynski, 2010, Exs. 1, 2, 4 and 5).

Example 1 Let us consider the following formulas:

Let ϕ = p p p. We have that

Red HT(ϕ, ) , Red HT(ϕ, {p}) , Red FLP(ϕ, ) , Red HT(ϕ, {p}) p.

Thus SMHT(ϕ) = , while SMFLP(ϕ) = {{p}}.

Let ϕ1 = p p and ϕ2 = p p. We have the following:

Red HT(ϕi, ) and Red HT(ϕi, {p}) p, for i = 1, 2,

Red FLP(ϕ1, ) , Red FLP(ϕ1, {p}) p, Red FLP(ϕ2, ) , Red FLP(ϕ2, {p}) .

Thus, while SMFLP(ϕ1) = SMHT(ϕ1) = { , {p}}, SMFLP(ϕ2) = { }.

Definition 2 Two formulas ϕ1 and ϕ2 are -SM-equivalent (under -stable model semantics), written ϕ1 SM ϕ2, iff they have the same -stable models.

Here the notion of HT-SM-equivalence is indeed the notion of equivalence in logic programs under stable model semantics (cf., see Lifschitz et al., 2001, Thm. 1).

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

2.3 Strong Equivalence and Knowledge of Logic Programs

Unlike the equivalence in propositional logic, the equivalence of logic programs does not allow equivalent replacement i.e., ϕ ϕ1 and ϕ ϕ2 may have different stable models, even though ϕ1 and ϕ2 are equivalent.

Example 2 Let ϕ1 = p q and ϕ2 = p p. As SM (ϕ1) = SM (ϕ2) = { }, ϕ1 and ϕ2 are -SM-equivalent; however, p ϕ1 has a -stable model {p, q} while the unique -stable model of p ϕ2 is {p}. Thus it does not allow replacing ϕ1 by ϕ2 in p ϕ1. It also indicates that ϕ1 has different knowledge from ϕ2 under the -stable model semantics.

This motivates the notion of strong equivalence.

Definition 3 Two formulas ϕ1 and ϕ2 are strongly -equivalent (under -stable model semantics) iff ϕ ϕ1 SM ϕ ϕ2 for every formula ϕ. In the case ϕ1 and ϕ2 are strongly -equivalent, they are -knowledge equivalent.

It is known that the notion of strong -equivalence can be captured in terms of -models, where a -interpretation is a pair X, Y such that X Y A. The -satisfiability (thus -models), denoted by |= , is recursively defined as follows:

( -S1) X, Y |= ;

( -S2) X, Y |= p if p X;

( -S3) X, Y |= ϕ1 ϕ2 if X, Y |= ϕ1 or X, Y |= ϕ2;

( -S4) X, Y |= ϕ1 ϕ2 if X, Y |= ϕ1 and X, Y |= ϕ2;

(HT-S5) X, Y |=HT ϕ1 ϕ2 if Y |= ϕ1 ϕ2; and X, Y |=HT ϕ1 implies X, Y |=HT ϕ2;

(FLP-S5) X, Y |=FLP ϕ1 ϕ2 if Y |= ϕ1 ϕ2; and Y |= ϕ1 or X |= ϕ1 or X, Y |=FLP ϕ2.

By Mod (ϕ) we denote the set of all -models of formula ϕ. Please note here that, can be either HT or FLP. In particular, Mod HT(ϕ) (resp. Mod FLP(ϕ)) denotes the set of all HT-models (resp.

FLP-models) of ϕ. For the formulas ϕ1 and ϕ2 in Example 2, one can check that none of , {p} , {p}, {p} or {p}, {p, q} is a -model of ϕ1, while every -interpretation is a -model of ϕ2.

Definition 4 A formula ψ is a logical -consequence of a formula ϕ, written ϕ |= ψ, iff Mod (ϕ) Mod (ψ); two formulas ϕ and ψ are -equivalent (under -model semantics), written ϕ ψ, iff Mod (ϕ) = Mod (ψ).

In the following proposition, item (i) is proved by Lifschitz, Tang, and Turner (cf., see Lifschitz et al., 1999, (iii) of Prop. 6).

Proposition 1 Let A, B, C, D be set of atoms. We have the following

(i) V(A B) W(D C) HT V(A B C) W D.

(ii) V(A B) W(D C) |=FLP V(A B C) W D.

WANG, ZHANG, ZHOU, & ZHANG

Please note here that the inverse of (ii) does not generally hold. For instance, p p FLP while , {p} |=FLP p p. Given two formulas ϕ1 and ϕ2, it is known that ϕ1 and ϕ2 are strongly HT-equivalent under

HT-stable model semantics if and only if they are HT-equivalent, viz. ϕ1 HT ϕ2; ϕ1 and ϕ2 are strongly FLP-equivalent under FLP-stable model semantics if and only if they are FLP-equivalent, viz. ϕ1 FLP ϕ2 (cf., see Truszczynski, 2010, Thm. 7). It is commonly recognized that strong equivalence amounts to knowledge equivalence of formulas. That is, strong -equivalence captures the logical content of a formula under -stable model semantics (Osorio & Zacarias, 2004; Osorio & Cuevas, 2007; Delgrande et al., 2013). Now we formally define the knowledge of logic programs.

Definition 5 The -knowledge of a formula ϕ under -stable model semantics, written Cn (ϕ), consists of the logical -consequence of ϕ, viz, Cn (ϕ) = {ψ | ϕ |= ψ}.

The -knowledge of a formula stands for the -logical content of the formula. For instance, Cn HT( ) = Cn HT(p p) Cn HT(p q). Recall that, under -model semantics, every formula can be transformed into a conjunction of formulas in the following normal form: (B C) _ (A D) (2)

where A, B, C, D are sets of atoms (cf., for = HT, see Cabalar & Ferraris, 2007, Thm. 2; Truszczynski, 2010, Thm. 9 for = FLP). That is, for every formula ϕ, there is a conjunction of formulas in the form (2) which is strongly -equivalent to ϕ. A formula of the form (2) is called a rule, which is also generally written as

a1; . . . ; al; not d1; . . . ; not dn b1, . . . , bk, not c1, . . . , not cm (3)

where A = {ai|1 i l}, B = {bi|1 i k}, C = {ci|1 i m} and D = {di|1 i n}. A logic program is a finite set of rules. Let r be a rule of the form (2). It is said to be

disjunctive if D = ;

positive if C = D = ;

normal if |A| 1 and D = ; and

Horn if |A| 1 and C = D = .

A logic program is disjunctive (resp. positive, normal, and Horn) iff it consists of disjunctive (resp. positive, normal, Horn) rules. A logic program is -consistent (under -stable model semantics) if it has at least one -stable model. It is known that every logic program has the same HT-models and FLP-models (cf., see Truszczynski, 2010, Prop. 8).

Proposition 2 Every logic program has the same HTand FLP-models.

3. Characterizations of Knowledge Equivalence

In the section, from the perspective of -models, we consider the characterization for knowledge equivalence of various logic programs firstly, and relate the knowledge equivalence to the equivalence of propositional logic secondly.

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

3.1 Model Theoretical Characterization

We firstly recall some basic properties of the -satisfiability (Ferraris & Lifschitz, 2005; Ferraris, 2005; Truszczynski, 2010).

Proposition 3 Let ϕ be a formula and X Y A.

(i) If X, Y |= ϕ then Y, Y |= ϕ (i.e., Y |= ϕ).

(ii) X, Y |= ϕ iff Y |= ϕ.

(iii) X, Y |= ϕ iff X |= Red (ϕ, Y ).

A collection M of -interpretations is -expressible whenever there exists a formula ϕ such that Mod (ϕ) = M. A collection M of -interpretations may be not -expressible. For instance, there is no formula whose -models are the ones in M = { , {p} }. The reason is that if there is a formula ϕ such that Mod (ϕ) = M then we have {p}, {p} |= ϕ by (i) of Proposition 3. This requires {p}, {p} belonging to Mod (ϕ), a contradiction. Given a formula ϕ and X Y A, X, Y is a -countermodel of ϕ if X, Y |= ϕ and Y, Y |= ϕ; Y, Y is a -countermodel of ϕ if Y, Y |= ϕ. Let X Y A, we define the following formulas:

λHT(X, Y ) = (X

Y ) _ ((Y \ X) (Y \ X)), (4)

λFLP(X, Y ) = (X

λ(Y, Y ) = (Y

ξ(X, Y ) = (X

Y ) _ (Y \ X). (7)

Here λ (X, Y ) and λ(Y, Y ) is to capture the -countermodel X, Y and Y, Y respectively. The following lemma shows that the -countermodel can be captured by a formula (cf., for = HT, see Cabalar & Ferraris, 2007, Prop. 1; Truszczynski, 2010, Props. 5 and 6 for = FLP).

Lemma 1 Let X Y A and U V A.

(i) U, V is a -countermodel of λ (X, Y ) iff U = X and V = Y .

(ii) U, V is a -countermodel of λ(Y, Y ) iff V = Y .

Proposition 4 A collection M of -interpretations is -expressible iff

X, Y M implies Y, Y M. (8)

Actually, if M satisfy condition (8) then the following logic program

Π = {λ (X, Y )| X, Y / M and Y, Y M} {λ(Y, Y )| Y, Y / M}

captures M in the sense that Mod (Π ) = M.

WANG, ZHANG, ZHOU, & ZHANG

Note that Wong (2009) presented a model-theoretical characterization for the HT-models of disjunctive logic programs (cf., see Wong, 2009, Thm. 2.7). Formally speaking, a collection M of

HT-interpretations is disjunctively HT-expressible, i.e., there is a disjunctive logic program Π such that Mod HT(Π) = M, iff the condition (8) and the following one hold:

if X, Y M, Y Y and Y , Y M then X, Y M. (9)

Together with Proposition 2, we have

Corollary 1 A collection M of FLP-interpretations is disjunctively FLP-expressible iff the conditions (8) and (9) hold.

Actually, if M satisfies the conditions (8) and (9) then the following disjunctive logic program captures M.

Π = {ξ(X, Y )| X, Y / M and Y, Y M} {λ(Y, Y )| Y, Y / M}.

Lemma 2 Let A, B be two sets of atoms, and X Y A. X, Y |= V B W A iff X |= V B W A and Y |= V B W A.

Proposition 5 A set M of -interpretations is positively -expressible, i.e., there is a positive logic program Π s.t Mod (Π) = M, iff M satisfies the criteria:

X, Y M iff X Y, X, X M and Y, Y M. (10)

As a matter of fact, in the case M satisfies the condition (10), the positive logic program Π = {V X W

X| X, X / M} captures M.

Corollary 2 Two positive logic programs are strongly -equivalent if and only if they are equivalent in propositional logic.

Eiter, Fink, Tompits, and Woltran (2004) have showed that a disjunctive logic program Π is strongly equivalent to a normal logic program if and only if Π is closed under here-intersection, i.e., for every pair of HT-models X, Y and X , Y of Π, X X , Y is also an HT-model of Π (cf., see Eiter et al., 2004, Thms. 1 and 2). In terms of the characterization of disjunctive logic programs and Proposition 2, we obtain a -model characterization for normal logic programs as follows.

Corollary 3 A set M of -interpretations is normally -expressible, i.e., there is a normal logic program Π such that Mod (Π) = M, iff M satisfies, in addition to (8) and (9), the following criteria: if X, Y M and X , Y M then X X , Y M. (11)

Proposition 6 A collection M of -interpretations is Horn -expressible, i.e., there is a Horn logic program Π such that Mod (Π) = M, iff M satisfies, in addition to (10), the following criteria:

X, Y M and H, T M X H, Y T M. (12)

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

3.2 Relating Knowledge Equivalence to Propositional Logic

It is proved that strong equivalence of logic programs under stable model semantics can be related to the equivalence in propositional logic (Pearce et al., 2001; Lin, 2002). This holds for the strong

FLP-equivalence of logic programs as we will show in the following. Firstly, we extend the language LA to LA A where A = {p |p A} and p s are fresh atoms. For each expression α of LA, by α we denote the result obtained from α by replacing each atom p from A by the corresponding atom p in A . In the following we denote

(A) = {p p | p A}. (13)

Please note that, for each model M of (A), M has a splitting MA and MA where MA = M A and MA = M A and, for every p MA, the atom p of A belongs to MA . For M A we denote by M the set {p A|p M}.

Definition 6 τHT[.] and τFLP[.] are recursively defined as follows:

(T1) τ [ ] = ;

(T2) τ [p] = p;

(T3) τ [ϕ1 ϕ2] = τ [ϕ1] τ [ϕ2] where { , };

(HT-T4) τHT[ϕ1 ϕ2] = (ϕ 1 ϕ 2) (τHT[ϕ1] τHT[ϕ2]);

(FLP-T4) τFLP[ϕ1 ϕ2] = (ϕ 1 ϕ 2) (ϕ1 ϕ 1 τFLP[ϕ2]).

Please note that the translation τHT is same to the translation τ defined by Pearce, Tompits, and Woltran (2001). One can verify that τHT[ ϕ] = ϕ τHT[ϕ], while τFLP[ ϕ] = ϕ . Given a theory Σ of LA, we define τ [Σ] = {τ [ϕ] | ϕ Σ}. It is evident that τ [Σ] is in linear size of Σ.

Example 3 Let ϕ = p p p. We have that

τHT[ϕ] = ((p p ) p ) ((p p p ) p) p ,

τFLP[ϕ] = ((p p ) p ) ((p p) (p p ) p) p p.

The unique FLP-model (over the signature {p}) of ϕ is {p}, {p} . However, ϕ has two HT-models , {p} and {p}, {p} . Over the signature {p, p }, one can easily check that {τHT[ϕ]} (A) has two models {p, p } and {p }, while {τFLP[ϕ]} (A) has a unique model {p, p }.

Proposition 7 Let ϕ = V(B C) W(A D), where A, B, C, D are subsets of A. Then we have (A) |= τFLP[ϕ] τHT[ϕ].

The following proposition connects the -equivalence with the equivalence in classical propositional logic (cf., for = HT, see Pearce et al., 2001, Lem. 2).

Proposition 8 Let ϕ be a formula of LA and X Y A. Then X, Y is a -model of ϕ iff X Y is a model of (A) {τ [ϕ]}.

WANG, ZHANG, ZHOU, & ZHANG

The following theorem shows that the strong -equivalence of logic programs under -stable model semantics can be reduced to the equivalence in propositional logic (cf., for = HT, see Ferraris et al., 2011, Thm. 9; or Lin & Zhou, 2011, (5) of Thm. 6).

Theorem 4 Two formulas ϕ and ψ have the same -models (over A) iff (A) {τ [ϕ]} and (A) {τ [ψ]} have the same models (over A A ).

Based on the theorem, we obtain the following complexity result (cf., for = HT, see Pearce, Tompits, & Woltran, 2009, Thms. 8 and 11).

Proposition 9 (i) The problem of deciding if a formula is -satisfiable is NP-complete. (ii) The problem of deciding if two formulas are -equivalent is co-NP-complete.

4. Knowledge Forgetting in Logic Programs

As mentioned in the introduction, we concentrate on the knowledge forgetting of logic programs under stable model semantics. It is formally stated as following:

Definition 7 (Knowledge forgetting) Let Π be a logic program and V A. A logic program Σ is a result of -knowledge forgetting V from Π, if and only if Σ consists of the -knowledge of Π that mentions no atom from V .

We will show that such a knowledge forgetting result always exists and it is unique up to strong equivalence (cf. Theorem 6) after a semantic -forgetting is defined and explored. Let V, X, Y be sets of atoms. The set Y is V -bisimilar to X, written Y V X, if Y \V = X\V . It intuitively states that the interpretations X and Y agree with each other on those atoms not in V . Two -interpretations H, T and X, Y are V -bisimilar, written H, T V X, Y , if H V X and T V Y . Now, we are in the position to define the semantic knowledge forgetting in terms of bisimulation.

Definition 8 (Semantic knowledge forgetting) Let ϕ be a formula and V A. A formula ψ is a result of (semantic) -forgetting V from ϕ whenever, for every -interpretation M,

M Mod (ψ) iff M Mod (ϕ) s.t M V M . (14)

According the definition, one can see that the -models of ψ can somehow exactly constructed from those of ψ. This motivates us to define the following notion of extension. Let V, X, Y be sets of atoms. The V -extension of X, denoted by X V , is the collection of interpretations that are V -bisimilar to X. The V -extension of a -interpretation H, T , denoted by H, T V , is the collection of -interpretations that are V -similar to H, T . For instance, let H, T = {p, q}, {p, q} and V = {q, r}. Then H, T V contains {p}, {p} , {p}, {p, q} , {p}, {p, q, r} , {p, q, r}, {p, q, r} and so on. Intuitively speaking, the V -extension of an interpretation M is the collection of interpretations formed from M by freely adding or removing some atoms in V . The V -extension of a collection M of ( -)interpretations, written M V , is the collection S β M β V . In classical propositional logic if M corresponds to a formula ϕ, i.e. M = Mod(ϕ), then M V corresponds to a formula whose truth value has nothing to do with the atoms in V . The intended meaning in the case of -models is similar when M V corresponds to a formula under -model

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

semantics that is relevant to only the atoms not in V . In other words, suppose M V = Mod (ϕ). If X, Y |= ϕ then H, T |= ϕ where H (resp. T) is obtained from X (resp. Y ) by freely adding or removing any atoms in V whenever H T. The following lemma shows an equivalent condition for the semantic -knowledge forgetting.

Lemma 3 Let ϕ be a formula and V A. A formula ψ is a result of -forgetting V from ϕ, iff the following condition holds: Mod (ψ) = Mod (ϕ) V . (15)

This condition of -forgetting is a generalization of the forgetting in propositional logic (Lin & Reiter, 1994) in terms of the following corollary.

Corollary 5 A formula ψ is a result of forgetting a set V of atoms in a formula ϕ iff Mod(ψ) = Mod(ϕ) V , where Mod(.) refers to classical propositional logic.

A syntactic counterpart of the forgetting in propositional logic is defined as follows (Lin, 2001; Lang et al., 2003):

Forget(ϕ, {p}) = ϕ[p/ ] ϕ[p/ ],

Forget(ϕ, V {p}) = Forget(Forget(ϕ, {p}), V )

where ϕ[p/ ] (resp. ϕ[p/ ]) is the formula obtained from ϕ by replacing every occurrence of the atom p with (resp. ). As -interpretations are related to the given signature A, in what follows, we shall assume that the signature of a formula/theory is implicitly given by the atoms occurring in the formula/theory, unless explicitly stated otherwise. The example below illustrates how -forgetting results can be computed.

Example 4 Let ϕ be the following formula

(p q) (q p) ( p ) ( q ).

Over the signature {p, q}, we have Mod (ϕ) = { , {p, q} , {p, q}, {p, q} }. Please note here that can be either HT or FLP. Then from Definition 8, we can verify that Mod (ϕ) {p} = { , {q} , {q}, {q} } {p}. It corresponds to the formula ψ = (p q ) ( p q) under the -model semantics by Proposition 4. As a matter of fact, we have ψ q q. Note that Forget(ϕ, {p}) = ϕ[p/ ] ϕ[p/ ] q and q q. It shows that, unlike the syntactic counterpart of the forgetting in classical propositional logic, the -forgetting results cannot be computed via ϕ[p/ ] ϕ[p/ ] as Mod ( q) = { , {q} , {q}, {q} }, while Mod (q) = { {q}, {q} } (over the signature {q}).

4.1 Expressibility

Please note that Definition 8 does not guarantee the existence of the forgetting results, however the next theorem shows that the -forgetting result always exists. It also implies that the -forgetting result is unique (up to strong -equivalence).

WANG, ZHANG, ZHOU, & ZHANG

Theorem 6 (Expressibility theorem) Let ϕ be a formula and V a set of atoms. There exists a formula ψ such that Mod (ψ) = Mod (ϕ) V .

Here, the uniqueness up to strong -equivalence of the -forgetting result follows from the fact that, if a formula ψ is a result -forgetting V from ϕ as well then Mod (ψ ) = Mod (ϕ) V = Mod (ψ), which shows that ψ and ψ are strongly -equivalent under the -stable model semantics. Based on the expressibility result and by abusing the denotation, we denote the forgetting result by Forget (ϕ, V ):

Definition 9 Let ϕ be a formula and V A. Forget (ϕ, V ) is a formula ψ s.t Mod (ψ) = Mod (ϕ) V , i.e., Forget (ϕ, V ) is a result of -forgetting V from ϕ.

In this sense Forget is an operator which maps a formula and a set of atoms to a formula. According to Definition 8 and the expressibility theorem, the following corollary easily follows.

Corollary 7 Let ψ, ϕ be formulas, V , V1 and V2 be sets of atoms.

(i) Forget (Forget (ϕ, V1), V2) Forget (Forget (ϕ, V2), V1).

(ii) If ψ ϕ then Forget (ψ, V ) Forget (ϕ, V ).

It firstly states that -forgetting is independent of the order of forgotten atoms, and secondly, the -forgetting preserves strong -equivalence of logic programs under -stable model semantics. To further investigate the properties of the forgetting, we introduce a notion of irrelevance under -model semantics.

Definition 10 A formula ψ is -irrelevant to a set V of atoms, denoted as IR (ψ, V ), if there exists a formula φ mentioning no atoms from V and ψ φ.

Some basic properties on -forgetting are presented below.

Proposition 10 Let ψ and ϕ be two formulas and V a set of atoms.

(i) IR (Forget (ψ, V ), V ).

(ii) ψ has a -model iff Forget (ψ, V ) has.

(iii) ψ |= Forget (ψ, V ).

(iv) If ψ |= ϕ then Forget (ψ, V ) |= Forget (ϕ, V ).

(v) Forget (ψ ϕ, V ) Forget (ψ, V ) Forget (ϕ, V ).

(vi) Forget (ψ ϕ, V ) |= Forget (ψ, V ) Forget (ϕ, V ).

(vii) Forget (ψ ϕ, V ) Forget (ψ, V ) ϕ if IR (ϕ, V ).

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

Intuitively, (i) of the Proposition says that the -forgetting result is irrelevant to atoms in V , i.e., those forgotten atoms. In this sense, the signature of -forgetting result can be constrained to A \ V . The intended meaning of the others can be easily read out. E.g., item (iii) says that this forgetting is a kind of weakening, while item (v) shows that the forgetting has a distributive property for disjunction. As mentioned earlier, disjunctive programs, positive programs, normal logic programs and Horn programs are four types of special cases of (arbitrary) logic programs under our setting. Then it is interesting to consider whether the expressibility result also holds for each of these special programs. For instance, we would like to know whether the result of -forgetting in a disjunctive (positive, normal, and Horn) logic program is still expressible by a disjunctive (resp. positive, normal, and Horn) logic program. As indicated by the following two examples, HTand FLP-forgetting in disjunctive, positive and normal logic programs is possibly not expressible in either disjunctive or positive logic programs. For simplicity, we identify a singleton set {α} as α when it is clear from its context, and thus we denote Forget (ψ, {p}) as Forget (ψ, p), and IR (ψ, {p}) as IR (ψ, p), and M {p} as M p etc..

Example 5 Consider the following normal logic program Π over signature {p, q}:

( p q) ( q p) (p q ).

We have that Mod (Π) = { {p}, {p} , {q}, {q} } and

Mod (Π) p = { , , {q}, {q} } {p}.

Here {p}, {p} {p} = , {p}. It implies that Forget (Π, p) q q. It can be easily seen that q q cannot be expressed as a disjunctive logic program because Mod (Π) p does not satisfy (9). Hence Forget (Π, p) cannot be expressed by a normal logic program. Please note that q q HT q q. Thus q q is also a result of HT-forgetting p from Π. However, q q is not a result of FLP-forgetting p from Π as q q FLP FLP q q.

Example 6 Let Π be a positive logic program over signature {p, q, r} as follows:

(p q r) (p q r) (p r q) (q r p).

It is not difficult to verify that, over the signature {p, r}, Mod (Π) {q} consists of

, , , {p, r} , {p}, {p} , {p}, {p, r} , {r}, {r} , {r}, {p, r} , {p, r}, {p, r} .

Clearly it does not satisfy the condition (9). Hence it can not captured by a disjunctive logic program. As a matter of fact, we have the following

Forget HT(Π, q) HT λHT( , {p}) λHT( , {r}) = ( r p p) ( p r r),

Forget FLP(Π, q) FLP λFLP( , {p}) λFLP( , {r}) = ( r p r p) ( p p r r)

in terms of Proposition 4. Interestingly, this example also shows that, though a logic program may have the same HT-models as FLP-models, its HT-forgetting result may be different from its FLPforgetting result.

WANG, ZHANG, ZHOU, & ZHANG

The HTand FLP-forgetting in Horn logic programs is of special interest, because unlike disjunctive, positive and normal logic programs, the result of HTand FLP-forgetting result in a Horn logic program is always expressible by a Horn logic program, as we show below.

Theorem 8 (Horn expressibility) Let Π be a Horn logic program and V A. There is a Horn logic program Π such that Forget (Π, V ) Π .

Having obtained the model-theoretical characterization of the classes of disjunctive and normal logic programs respectively, we can easily derive a sufficient and necessary condition for HTand

FLP-forgetting results to remain in the same class, i.e., the result of HTand FLP-forgetting a set of atoms in a disjunctive (resp. normal) logic program is a disjunctive (resp. normal) logic program.

Proposition 11 Let Π be a disjunctive logic program, V A. We have that Forget (Π, V ) is expressible in disjunctive logic programs if and only if,

H1, T1 |= Π, T2, T2 |= Π and T1 T2 H3, T3 |= Π such that H3, T3 V H1, T2 .

Proposition 12 Let Π be a normal logic program, V A. Then Forget (Π, V ) is expressible in normal logic programs if and only if, in addition to condition (16), the following condition holds,

H1, T1 |= Π, H2, T2 |= Π and T1 V T2 H3, T3 |= Π such that H3 V H1 H2 and (T3 V T1 or T3 V T2). (16)

4.2 Forgetting Postulates

Zhang and Zhou (2009) proposed four forgetting postulates in their work of knowledge forgetting, and showed that their knowledge forgetting can be precisely characterized by the four postulates. They further argued that these postulates should be viewed as a general semantic characterization for knowledge forgetting in other logics. Indeed, the classical propositional forgetting can be also characterized by these postulates. In terms of forgetting in logic programs, as we addressed in the introduction, imposing these postulates is not feasible for existing approaches. In the following, we show that -forgetting is exactly captured by these postulates, which we think is one major advantage over other logic program forgetting approaches. The notion of forgetting is closely related to that of uniform interpolation property (Visser, 1996; Goranko & Otto, 2007), for instance, the forgetting in description logics (Lutz & Wolter, 2011) and the semantic forgetting in logic programs (Gabbay, Pearce, & Valverde, 2011). The following corollary follows from Theorem 6, which actually implies the uniform interpolation property of the logics under -model semantics. Namely, for any formulas ϕ and ψ with ψ |= ϕ, there exists a formula ξ such that ψ |= ξ, ξ |= ϕ and ξ contains only the atoms occurring in both ψ and ϕ. The formula ξ is called a uniform interpolant of ψ and ϕ. This is stated as:

Corollary 9 Let ψ and ϕ be two formulas, V a set of atoms and IR (ϕ, V ).

ψ |= ϕ iff Forget (ψ, V ) |= ϕ.

Let ψ and ϕ be two formulas and V a set of atoms. The following are Zhang-Zhou s four postulates for logic programs under -model semantics.

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

(W) Weakening: ψ |= ϕ.

(PP) Positive persistence: if IR (ξ, V ) and ψ |= ξ then ϕ |= ξ.

(NP) Negative persistence: if IR (ξ, V ) and ψ |= ξ then ϕ |= ξ.

(IR) Irrelevance: IR (ϕ, V ).

By specifying ϕ Forget (ψ, V ), (W), (PP), (NP) and (IR) are called postulates for knowledge forgetting in logic programs under -stable model semantics. Viz, ϕ is a result of -forgetting V in ψ. Based on the uniform interpolation property (cf. Corollary 9), we can show the following representation theorem.

Theorem 10 (Representation theorem) Let ψ and ϕ be two formulas and V a set of atoms. Then the following statements are equivalent:

(i) ϕ Forget (ψ, V ).

(ii) ϕ {ϕ | ψ |= ϕ and IR (ϕ , V )}.

(iii) Postulates (W), (PP), (NP) and (IR) hold.

This theorem justifies that the knowledge forgetting (cf. Definition 7) exists and is unique up to strong equivalence. An obvious consequence follows from the representation theorem is that

Forget (ϕ, V ) {ψ | ϕ |= ψ and IR (ψ, V )}.

It says that the result of -forgetting V from ϕ consists of the -logical consequence of ϕ that is -irrelevant to V . For this reason the forgetting is a knowledge forgetting of logic programs under stable models semantics. As we have mentioned in the introduction that none of the other forgetting approaches in logic programs is a knowledge forgetting since it does not satisfy some of the postulates (see Section 5 for details). One should note that the representation theorem is applicable for the forgetting in classical propositional logic, viz, Forget(ϕ, V ) {ψ | ϕ |= ψ and IR(ψ, V )}.

4.3 Relating to Propositional Forgetting

It has been shown that strong equivalence of logic programs may be related to the equivalence of propositional logic (Pearce et al., 2001; Lin, 2002). As the -forgetting preserves strong equivalence of logic programs under -stable model semantics, it is worth exploring further connections between -forgetting and the forgetting in propositional logic. In this section, we undertake an in-depth investigation on this aspect. We first provide a direct connection between -forgetting and propositional forgetting via the following proposition.

Proposition 13 Let ϕ, ϕ , ψ be formulas and V A such that ϕ Forget (ψ, V ) and ϕ Forget(ψ, V ). Then

WANG, ZHANG, ZHOU, & ZHANG

(ii) ϕ |= ϕ.

The result (i) in Proposition 13 simply says that the result of -forgetting and classical propositional forgetting are equivalent in classical propositional logic. Thus the forgetting in classic propositional logic can be computed by a -forgetting in logic programs. However as we have seen in Example 4, Forget (ψ, V ) is possibly not -equivalent to Forget(ψ, V ). The reverse of (ii) does not hold generally. For instance, Forget ( p, q) p, while Forget( p, q) p, and evidently p |= p. From this result and Theorem 8, we immediately have the following corollary.

Corollary 11 Let Π be a Horn logic program and V a set of atoms. Then Forget(Π, V ) is expressible by a Horn logic program.

The following result states that, for Horn logic programs, -forgetting and the forgetting of propositional logic are strongly -equivalent. Thus it provides a method of computing -forgetting results of Horn logic programs through the propositional forgetting.

Proposition 14 Let Π and Π be two Horn logic programs, and V a set of atoms such that Π Forget(Π, V ). Then Π Forget (Π, V ).

The following proposition states that the -forgetting of double negative formulas is closely connected with the classical propositional forgetting, which will be used to prove some complexity results later.

Proposition 15 Let ψ and ϕ be two formulas and V a set of atoms.

(i) ϕ Forget(ψ, V ) iff ϕ Forget ( ψ, V ).

(ii) Forget(ϕ, V ) Forget(ψ, V ) iff Forget ( ϕ, V ) Forget ( ψ, V ).

As it is known that the strong equivalence of logic programs is closed related to the equivalence in propositional logic by translating logic programs into propositional theories (Pearce et al., 2001; Lin, 2002). This motivates us to investigate the connection between the forgettings in the view of the translations. Now our main result of this section is stated as follows.

Theorem 12 ( -forgetting vs propositional forgetting) Let ψ and ϕ be two formulas of LA and V A. Then

ϕ Forget (ψ, V ) iff (A) |= τ [ϕ] Forget( (A) {τ [ψ]}, V V ).

By Theorem 12, we know that to check whether a formula ϕ is a result of -forgetting a set V of atoms from a formula ψ, it is equivalent to check whether τ [ϕ] is classically equivalent to Forget( (A) {τ [ψ]}, V V ) under the theory (A). The following example shows an application of this theorem.

Example 7 [Example 5 continued] Recall that Π is the following formula:

( p q) ( q p) (p q )

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

and Forget (Π, p) q q. Over the signature {p, q}, (A) = (p p ) (q q ) and, the program translation yields:

τ (Π) ( p q) ( p q ) ( q p) ( q p ) ( p q ).

Now we have that Forget(τ [Π] (A), {p, p }) is equivalent to:

( q q ) (q q ), i.e. (q q) (q q )

which is equivalent to q q under the theory ({q}) = {q q }. One can further check that τ [ q q] = q q q q q (under the theory ({q})). Thus the formula q q is a result of -forgetting p from Π by Theorem 12.

The following example further shows that (A) occurring in Forget ({τ[ψ]} (A), V V ) is necessary for Theorem 12.

Example 8 [Continued from Example 6] Recall that A = {p, q, r}, (A) = {p p , q q , r r } and Π consists of

(p q r) (p q r) (p r q) (q r p).

We have that,

τHT[Π] Π Σ,

(A) |= τ [Π] Π Σ,

τFLP[Π] (p q r) (p q p q r) (p r p r q) (q r q r p) Σ

where Σ = (p q r ) (p r q ) (q r p ). One can check that

Forget(τHT[Π], {q, q }) ,

(A) |= Forget(τFLP[Π], {q, q }) .

Recall that the formula ϕ1 = ( r p p) ( p r r) is a result of HT-forgetting q from Π; and ϕ2 = ( r p r p) ( p p r r) is a result of FLP-forgetting q from Π. We have that

τHT[ϕ1] ϕ 1 ( r r p p p ) ( p p r r r ),

τFLP[ϕ2] ϕ 2 ( r r p r p ) ( p p p r r ).

Under the theory (A), we have

(A) |= τHT[ϕ1] (p p r ) (r r p ),

(A) |= τHT[ϕ1] (p p r ) (r r p ).

One can verify further that the model {p } of (A) is not a model of τHT[ϕ1], nor it is a model of τFLP[ϕ2], i.e. (A) |= τHT[ϕ1] and (A) |= τFLP[ϕ2] . Actually, we have that,

(A) |= Forget({τ [Π]} (A), {q, q }) ((p r ) (p r) (p r )).

One can check further that

(A) |= (p p r ) (r r p ) ((p r ) (p r) (p r )),

which shows that ϕ1 (resp. ϕ2) is a result of HT-forgetting (resp. FLP-forgetting) q from Π.

WANG, ZHANG, ZHOU, & ZHANG

The following result states that we can reduce checking whether the -forgetting results of two formulas are strongly -equivalent to checking whether the propositional forgetting results of corresponding two formulas are equivalent.

Proposition 16 Let ψ and ϕ be two formulas of LA and V a set of atoms. Then Forget (ψ, V ) Forget (ϕ, V ) iff the following condition holds:

Forget({τ [ψ]} (A), V V ) Forget({τ [ϕ]} (A), V V ).

4.4 Computation and Complexity

Theorem 6 and Propositions 4 and 10 imply a naive approach to compute -forgetting results. Formally speaking, given a formula ψ over a signature A and a set V of atoms, Forget (ψ, V ) can be computed as follows:

(Step 1) Evaluating all -models of ψ, denoted by M.

(Step 2) Restrict M to A \ V , denoted by M|V , i.e.

M|V = { H \ V, T \ V | H, T M}.

(Step 3) Enumerating the following formulas (over the signature A \ V ) from M|V :

λ (X, Y ) if X, Y / M|V but Y, Y M|V ,

λ(Y, Y ) if Y, Y / M|V .

(Step 4) Finally, conjunct all the constructed formulas, denoted by ϕ.

Corollary 13 Let ψ, V and ϕ be given as above. Then ϕ Forget (ψ, V ).

Alternatively, in terms of Theorem 10, we can compute Forget (ψ, V ) by enumerating the - consequences of ψ that are -irrelevant to V . As there exist sound and complete axiomatic systems for the HT-logic (Jongh & Hendriks, 2003), checking HT-consequence relation is axiomatically doable. Though a sound and complete axiomatic system for FLP-logic is recently unknown, we still can enumerate all the formulas of form (2) over the signature A \ V and check if they are FLPconsequence of ψ. Nevertheless, it is also observed that from a computational viewpoint, like the propositional forgetting, each of the above two approaches would be expensive. This appears to be inevitable in terms of the following complexity results, unless the complexity hierarchy collapses.

Theorem 14 Let ψ and ϕ be two formulas and V a set of atoms.

(i) The problem of deciding if ψ Forget (ψ, V ) is co-NP-complete.

(ii) The problem of deciding if Forget (ϕ, V ) Forget (ψ, V ) is ΠP 2 -complete.

(iii) The problem of deciding if ϕ Forget (ψ, V ) is ΠP 2 -complete.

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

According to our representation theorem (i.e. Theorem 10), the result (i) in Theorem 14 means that checking if ψ is -irrelevant to V , i.e. IR (ψ, V ), is intractable. The result (ii) of Theorem 14, on the other hand, presents the complexity of -forgetting equivalence checking, i.e., if two formulas are strongly -equivalent when they are restricted to a common signatures. The last result (iii) of Theorem 14 states that checking if a formula is a result of -forgetting is generally difficult.

Proposition 17 Let ψ and ϕ be two formulas and V a set of atoms.

(i) The problem of deciding whether ψ |= Forget (ϕ, V ) is ΠP 2 -complete.

(ii) The problem of deciding whether Forget (ψ, V ) |= ϕ is co-NP-complete.

Theorem 14 and Proposition 17 tell us that for -forgetting, in general the complexity of resulting checking and inference problems is located at the same level of the complexity polynomial hierarchy as the propositional forgetting.

4.5 Conflict Solving Based on Knowledge Forgetting

In the following, we consider the application of the proposed forgetting in conflict solving for logic program contexts, that represent a knowledge system consisting of knowledge bases of multiple agents.

Definition 11 A logic program context is an n-ary tuple Ω= (Π1, . . . , Πn) where Πi is a consistent logic program. Ωis -conflict-free if Π1 Πn is consistent under -stable model semantics.

Definition 12 Let Ω= (Π1, . . . , Πn) be a logic program context. A -solution of Ωis a minimal subset S of A such that (Forget (Π1, S), . . . , Forget (Πn, S)) is -conflict-free, where A is the underlying signature.

It is obvious that is a -solution of -conflict-free logic program context Ω. We consider the following simplified Zhang and Foo s conflict solving scenario (cf., see Zhang & Foo, 2006, Ex. 6).

Example 9 A couple John and Mary are discussing their family investment plan. There are four different shares share A, share B, share C and share D, where share A and share B are of high risk but also have high return; share C and share D are of low risk and may be suitable for a long term investment. John s and Mary s investment preference over these shares are encoded as the following logic programs ΠJ and Πm respectively:

r1 :s A not s B,

r2 :s C not s D,

r3 :s D not s C,

r4 : s C, s D,

r 3 :s B not s A, not s C,

r 4 : s A, s B, where s# stands for share#. The intuitive meaning of these rules can be easily read out. E.g. rule r1 says that John wants to buy share A if he don t buy share B, while rules r2, r3 and r4 mean that John wants to buy share C or share D, but not both of them.

WANG, ZHANG, ZHOU, & ZHANG

As one can see that ΠJ ΠM has no -stable model due to the confliction between rule r4 and r 1, r 2, the logic program context Ω= (ΠJ, ΠM) is not -conflict-free. For S = {s D}, we have the following

Forget HT(ΠJ, S) HT {s A not s B, s C; not s C },

Forget HT(ΠM, S) HT {s C , s B not s A, not s C, s A, s B}.

One can check that Forget HT(ΠJ, S) Forget HT(ΠM, S) has a unique HT-stable model {s A, s C}. Thus S is an HT-solution of Ω. It can be said that John and Mary may have an agreement on their investment plan about shares share A, share B and share C if they agree to give up the belief (knowledge) about share D. It results in an investment to shares share A and share C, but not to share B. One can further check that, under the FLP-stable model semantics, if John and Mary can give up the belief about share D then it results in the same investment plan to shares share A and share C, but not to share share B. The reason is that Forget FLP(ΠJ, S) Forget FLP(ΠM, S) has a unique FLP-stable model {s A, s C}.

5. Related Work

In this section we compare the -forgetting with weak and strong forgetting (Zhang & Foo, 2006), semantic forgetting (Eiter & Wang, 2008) and the forgetting operators FS and FW (Wong, 2009).

5.1 Weak and Strong Forgetting

Let Π be a normal logic program and p a propositional atom. The reduction of Π with respect to p, denoted by Red(Π, {p}), is the normal logic program obtained from Π by

(1) for each rule r of Π with p Head(r), if there is a rule r in Π such that p Body+(r ), then replacing r with Head(r ) Body(r), Body(r ) \ {p}.

(2) if there is such a rule r in Π and it has been replaced by a new rule in the previous step, then removing the rule r from the remaining normal logic program.

Let X be a set of propositional atoms. Then the reduction of Π with respect to X is inductively defined as follows:

Red(Π, ) = Π,

Red(Π, X {p}) = Red(Red(Π, {p}), X).

The strong forgetting p in a normal logic program Π is the normal logic program SForget(Π, {p}) obtained from Red(Π, {p}) by removing each rule r if either r is valid 5 or p Head(r) Body+(r) Body (r). The weak forgetting p in Π is the normal logic program WForget(Π, {p}) obtained from Red(Π, {p}) by firstly removing each rule r if either r is valid, or p Head(r) Body+(r) and then removing not p from the remaining rules.

5. A rule r is valid if Head(r) Body+(r) = or Body+(r) Body (r) = .

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

Let X be a set of atoms. The strong (and weak) forgetting X in Π is recursively defined as

SForget(Π, ) = Π; WForget(Π, ) = Π;

SForget(Π, X {p}) = SForget(SForget(Π, {p}), X);

WForget(Π, X {p}) = WForget(WForget(Π, {p}), X).

It is known that the two forgetting operators are independent of the ordering of forgotten atoms in the sense of strong HT-equivalence of logic programs under HT-stable model semantics (cf., see Zhang & Foo, 2006, Prop. 2).

Example 10 Consider the below two normal logic programs:

Π = {p q, q p, r not p},

Σ = {p q, q p, r not q}.

One can check that Π and Σ are strongly equivalent. We have that

SForget(Π, {p}) = , WForget(Π, {p}) = {r },

SForget(Σ, {p}) = WForget(Σ, {p}) = {r not q}.

The example shows that neither weak forgetting preserves strong equivalence, nor is strong forgetting. One can further verify that Π |= q r and Π |= r for {HT, FLP}. Thus the strong forgetting does not satisfy positive persistence , and the weak forgetting does not satisfy weakening and negative persistence . Actually, for HTand FLP-forgetting, we have the following

Forget HT(Π, p) HT Forget HT(Σ, p) HT { q r },

Forget FLP(Π, p) FLP Forget FLP(Σ, p) FLP { q r }.

Here Π FLP Σ follows from the fact that Π HT Σ and Proposition 2.

5.2 Semantic Forgetting

Having addressed certain issues of weak and strong forgetting, Eiter and Wang (2008) proposed a semantic forgetting for consistent disjunctive logic programs. Formally speaking, let Π be a consistent disjunctive logic program and p an atom. A set M of atoms is a p-stable model of Π iff M is a stable model of Π and there is no stable model M of Π such that M \ {p} M \ {p}. A disjunctive logic program Π represents the result of forgetting about p in Π, if

Π does not mention the atom p, and

a set M of atoms is a stable model of Π iff Π has a p-stable model M such that M p M.

In terms of the above definition, such forgetting results are not unique under strong equivalence. This means, their forgetting does not preserve strong equivalence. To compute the result of forgetting an atom in a consistent disjunctive logic program, they proposed three algorithms forget1, forget2 and forget3 (Eiter & Wang, 2008). The example below further demonstrates the difference between this semantic forgetting and the -forgetting.

WANG, ZHANG, ZHOU, & ZHANG

Example 11 Let Π = {p q} be a program over signature A = {p, q, r}. Although program Π has nothing to do with the atom r, we have that forgeti(Π, r) = (i = 1, 2, 3), which seems not intuitive as it loses some information irrelevant to what we want to forget. However Forget (Π, r) Π.

This example also shows that the semantic forgetting does not satisfy positive persistence postulate as Π |= q p, which is lost in the semantic forgetting result forgeti(Π, r) for i = 1, 2, 3.

5.3 Forgetting Operators FS and FW

Wong (2009) developed his forgetting for disjunctive logic programs. Differently from the work of Zhang and Foo (2006), and Eiter and Wang (2008), Wong s forgetting is defined based on the

HT-logic. In this sense, his approach probably shares a common logic ground with HT-forgetting. Wong also defined two forgetting operators FS and FW, which correspond to two series of program transformations. See Appendix D for the detailed definitions. The interesting feature of Wong s forgetting is that it preserves strong equivalence. However, a major issue with this forgetting is that: on one hand, the forgetting FS may cause unnecessary information loss; on the other hand, the forgetting FW may also introduce extra information that one does not want, as illustrated by the following example.

Example 12 Let us consider the normal logic program Π consisting of:

a x, y a, not z, q not p, p not q, p, q.

Then we have:

FS(Π, {a, p}) HT {y x, not z},

FW(Π, {a, p}) HT {y x, not z, x, q },

Forget HT(Π, {a, p}) HT {y x, not z, q not not q},

Forget FLP(Π, {a, p}) FLP {y x, not z, q not not q}.

Since Π |=HT {q not not q}, which is irrelevant to atoms a and p, it seems to us that forgetting {a, p} from Π should not affect this fact. But FS(Π, {a, p}) |=HT {q not not q}. In this sense, we see that FS has lost some information that we wish to keep. This shows that the operator FS does not satisfy positive persistence postulate. On the other hand, from the fact that Π |=HT q but FW(Π, {a, p}) |=HT q, it appears that FW may introduce unnecessary information, which indeed conflicts our intuition of program weakening via forgetting, i.e., it does not satisfy the weakening postulate.

As we mentioned in the introduction, the following example confirms that an expected result can not be obtained from either one of the above three forgetting approaches.

Example 13 [Continued from Example 5] For the normal logic program Π:

( p q) ( q p) (p q ),

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

we have the following:

SForget(Π, {p}) = forget1(Π, {p}) = FS(Π, {p}) = ,

WForget(Π, {p}) = FW(Π, {p}) = {q}.

Here, the expected logic program that represents the same information of Π when the auxiliary atom p is ignored should be q q.

6. Concluding Remarks

In this paper two semantic knowledge forgetting approaches, called HTand FLP-forgetting respectively, were proposed for logic programs under stable model and FLP-stable model semantics respectively. These knowledge forgetting results can be captured by the corresponding logical consequence of forgotten logic programs that are irrelevant to forgotten atoms. It consequently preserves strong equivalence of logic programs under HTand FLP-stable model semantics respectively. This is a major advantage when compared to other existing forgetting approaches in logic programming. As a starting point, we investigated the model theoretical characterization of logic programs under HTand FLP-stable model semantics, and studied their respective strong equivalence problems using classical propositional logic equivalence. Many properties of forgetting have been explored, such as existence of forgetting results, a representation theorem, and the complexity of some decision problems related to these forgettings. We also considered an application of knowledge forgetting in conflict solving. Although we have presented abstract approaches to computing the forgetting results and we showed the underlying difficulties of the computation, it is valuable to study practical algorithms for different subclasses of logic programs. Another challenging future work is to extend the knowledge forgetting to other nonmonotonic systems, and in particular first-order logic programs (Ferraris et al., 2011). As we have mentioned in the introduction that forgetting can be effectively used to solve some confliction, e.g. the strong and weak forgetting (Zhang & Foo, 2006) and the propositional forgetting (Lang & Marquis, 2010), such an application of knowledge forgetting deserves further studying. As what we concentrate upon in this paper is knowledge forgetting in logic programs, which is based on the notion of strong equivalence, an interesting work is to consider forgetting under the stable model semantics of logic programs along the work (Wang et al., 2013). Last but not least, logic programs under supported model semantics enjoys some similar properties as that of logic programs under HTand FLP-stable models semantics (Truszczynski, 2010), we will consider the knowledge forgetting for logic programs under the supported model semantics in another paper.

Acknowledgments

We thank Mirek Truszczynski for encouraging us to consider knowledge forgetting for logic programs under the FLP-stable model semantics. We thank the anonymous reviewers for their insightful comments, and Robin Bianchi for his help on formatting the paper. Yisong Wang is partially supported by the National Natural Science Foundation of China grant 61370161 and Stadholder Foundation of Guizhou Province under grant (2012)62.

WANG, ZHANG, ZHOU, & ZHANG

Appendix A. Proofs for Section 2

Proposition 1 Let A, B, C, D be set of atoms. We have the following

(i) V(A B) W(D C) HT V(A B C) W D.

(ii) V(A B) W(D C) |=FLP V(A B C) W D.

Proof: (ii) Suppose X, Y is an FLP-model of V(A B) W(D C) but not an FLP-model of V(A B C) W D. It follows that the following conditions hold:

(a) X |= V(A B C), which implies X |= V(A B).

(b) Y |= V(A B C), which implies Y |= V(A B) V C, and

(c) X, Y |=FLP W D, i.e. X |= W D.

The conditions (a) and (b) show that X, Y |=FLP W(D C), i.e. X |= W D or Y |= W C. Together with the conditions (b) and (c), a contradiction follows.

Appendix B. Proofs for Section 3

Proposition 4 A collection M of -interpretations is -expressible iff

X, Y M implies Y, Y M. (17)

Actually, if M satisfy condition (17) then the following logic program

Π = {λ (X, Y )| X, Y / M and Y, Y M} {λ(Y, Y )| Y, Y / M}

captures M in the sense that Mod (Π ) = M.

Proof: The direction from left to right follows from (i) of Proposition 3. We prove the other direction. Let Π be the propositional theory consisting of, for every X Y A,

λ (X, Y ) if X, Y / M and Y, Y M, and

λ(Y, Y ) if Y, Y / M.

By Lemma 1, Mod (Π ) = M.

Lemma 2 Let A, B be two sets of atoms, and X Y A. X, Y |= V B W A iff X |= V B W A and Y |= V B W A.

Proof: According to (iii) of Proposition 3 and Proposition 2, it is sufficient to show that, for the case = HT,

X |= ( B _ A)Y iff X |= B _ A and Y |= B _ A.

( ) Note that Y |= V B W A and X |= (V B)Y implies X |= (W A)Y . Suppose X |= V B W A, i.e. B X and A X = . It follows that Y |= V B due to B Y , and then

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

Y |= W A, i.e. A Y = . Thus we have X |= (V B)Y since (V B)Y = V B. By X |= (W A)Y

i.e. X |= W A, we have X A = , a contradiction. ( ) We need only to show X |= (V B)Y (W A)Y since Y |= V B W A. Suppose X |= (V B)Y and X |= (W A)Y . The former implies B X Y , thus X A = by X |= V B W A. The latter implies X (A Y ) = , which means X A = since X Y , a contradiction.

Proposition 5 A set M of -interpretations is positively -expressible, i.e., there is a positive logic program Π s.t Mod (Π) = M, iff M satisfies the criteria:

X, Y M iff X Y, X, X M and Y, Y M. (18)

Actually, if M satisfy condition (18) then the following logic program

X| X, X / M}

captures M in the sense that Mod (Π ) = M.

Proof: It suffices to prove the case = HT by Proposition 2. ( ) Let Π be a positive logic program whose HT-models are exact the ones in M. For every

HT-interpretation X, Y , by Lemma 2, X, Y |=HT Π iff X Y , X |= Π i.e. X, X |=HT Π, and Y, Y |=HT Π i.e. Y |= Π since every rule of Π is positive. The condition (18) follows. ( ) Let N = {X A| X, X M}. We construct the propositional theory Π consisting of X _

for every X

N(= 2A \ N). Firstly we show Mod(Π) = N. Suppose X |= Π and X N. We have that X

N. It follows that X |= Π as V X W

X belongs to Π. On the other hand, suppose X N and X |= Π. It follows that there exists X

N such that X |= V X W

X , i.e., X X and X

X = , from which we have X = X thus X N, a contradiction. Secondly we show Mod HT(Π) = M. On the one hand, let X, Y |=HT Π. We have that X |= Π and Y |= Π by Lemma 2. It follows X, Y N, which implies X, X M and Y, Y M. Thus X, Y M by (18). On the other hand, let X, Y M. In terms of (18), we have X, X M and Y, Y M. Thus X N and Y N, i.e. X |= Π and Y |= Π. Thus X, Y |=HT Π by Lemma 2.

Proposition 6 A collection M of -interpretations is Horn -expressible, i.e., there is a Horn logic program Π such that Mod (Π) = M, iff M satisfies, in addition to (10), the following criteria:

X, Y M and H, T M X H, Y T M. (19)

Proof: It suffices to prove the case = HT by Proposition 2. ( ) Suppose Π is a Horn logic program such that Mod HT(Π) = M. By Proposition 5, Mod HT(Π) satisfies (18). Suppose X, Y and H, T are two HT-models of Π. It follows that X, Y, H and T are models of Π by Lemma 2. Thus X H |= Π and Y T |= Π, by which X H, Y T |= Π due to X H Y T.

WANG, ZHANG, ZHOU, & ZHANG

( ) Let N and Π be the ones defined in the proof of Proposition 5. If X, Y N then X Y N according to (19). It follows that there exists a Horn logic program (a set of Horn clauses) whose models are exactly the ones in N. As a matter of fact, the Horn program Π can be constructed from Π by replacing each V X W Y with X p1, . . . , X pk (20)

where X Y = and T{Y \ X|X Y and Y N} = {p1, . . . , pk}. We firstly show Π Π by proving

where pi (1 i k) are defined in (20). The direction from right to left is trivial as V X W Y belongs to Π. Let us consider the other direction. Suppose H |= Π, H is a model of V X W Y and H |= V X pi for some i (1 i k). We have that X H and H Y = . It follows that H is some element of {Y \ X|X Y and Y N} and then {p1, . . . , pk} H. It is a contradiction. Finally Mod HT(Π ) = M follows from Mod HT(Π) = M and Proposition 5.

Proposition 7 Let ϕ = V(B C) W(A D), where A, B, C, D are subsets of A. Then we have (A) |= τFLP[ϕ] τHT[ϕ].

Proof: Note that τHT[ p] = p p and τFLP[ p] = p . We have

c C ( c c ) _ A _

d D ( d d )

τFLP[ϕ] = ϕ (B C B C ) _ (A D ) .

Since (A) |= p p p , we have that

(A) |= τHT[ϕ] ϕ

(B C ) _ A _

(A) |= τFLP[ϕ] ϕ (B C ) _ (A D ) .

It completes the proof.

Proposition 8 Let ϕ be a formula of LA and X Y A. X, Y is a -model of ϕ iff X Y is a model of (A) {τ [ϕ]}.

Proof: We prove the case = FLP by induction on the structures of ϕ. Let X Y A.

ϕ = p or ϕ = . It is trivial for ϕ = . On the other hand, X, Y |=FLP p iff X |= p iff X Y |= p.

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

ϕ = ϕ1 ϕ2 where { , }. It follows from the inductive assumption.

ϕ = ϕ1 ϕ2. We have τFLP[ϕ1 ϕ2] = (ϕ 1 ϕ 2) (ϕ1 ϕ 1 τFLP[ϕ2]). Recall that X, Y |=FLP ϕ1 ϕ2 iff

Y |= (ϕ1 ϕ2) and,

either (a) X |= ϕ1, or (b) Y |= ϕ1, or (c) X, Y |=FLP ϕ2.

Y |= (ϕ1 ϕ2) iff Y |= ϕ 1 ϕ 2 iff X Y |= ϕ 1 ϕ 2, and

(a) X |= ϕ1 iff X Y |= ϕ1, (b) Y |= ϕ1 iff Y |= ϕ 1 iff X Y |= ϕ 1, and (c) X, Y |=FLP ϕ2 iff X Y |= τFLP[ϕ2] by the inductive assumption.

It follows that X, Y |=FLP ϕ1 ϕ2 iff X Y |= τFLP[ϕ1 ϕ2].

This completes the proof.

Theorem 4 Two formulas ϕ and ψ have the same -models (over LA) iff (A) {τ [ϕ]} and (A) {τ [ψ]} have the same models (over LA A ).

Proof: We prove the case = FLP. ( ) M |= (A) {τFLP[ϕ]} iff MA MA |= (A) {τFLP[ϕ]} iff MA, M A |=FLP ϕ by Proposition 8, here M A = {p|p MA } iff MA, M A |=FLP ψ since ϕ FLP ψ iff MA MA |= (A) {τFLP[ψ]} by Proposition 8 iff M |= (A) {τFLP[ψ]}. ( ) X, Y |=FLP ϕ iff X Y |= (A) {τFLP[ϕ]} by Proposition 8, here Y = {p |p Y } iff X Y |= (A) {τFLP[ψ]} since (A) {τFLP[ψ]} (A) {τFLP[ϕ]} iff X, Y |=FLP ψ by Proposition 8.

Proposition 9 (i) The problem of deciding if a formula is -satisfiable is NP-complete. (ii) The problem of deciding if two formulas are -equivalent is co-NP-complete.

Proof: (i) Membership. If a formula ϕ is FLP-satisfiable then there exists an FLP-interpretation H, T such that H, T |=FLP ϕ. It is feasible to guess such an FLP-interpretation and check the condition H, T |=FLP ϕ. Thus the problem is in NP. Hardness. It follows from the fact that ϕ is FLP-satisfiable iff ϕ is satisfiable, which is NPhard, by (ii) of Proposition 3. This shows that the problem is NP-hard. (ii) Membership. If ϕ FLP ψ then there exists H, T such that, either

(a) H, T |=FLP ϕ and H, T |=FLP ψ, or

(b) H, T |=FLP ϕ and H, T |=FLP ψ.

WANG, ZHANG, ZHOU, & ZHANG

To guess such an FLP-interpretation H, T and to check the conditions (a) and (b) are feasible in polynomial time in the size of ϕ and ψ. Thus the problem in co-NP. Hardness. We have that ϕ FLP iff ϕ has no FLP-model iff ϕ has no model by (ii) of Proposition 3 iff ϕ is valid, which is co-NP-hard. Thus the problem is co-NP-hard.

Appendix C. Proofs for Section 4

Lemma 3 Let ϕ be a formula and V A. A formula ψ is a result of -forgetting V from ϕ, iff the following condition holds: Mod (ψ) = Mod (ϕ) V .

Proof: ψ is a result of -knowledge forgetting V from ϕ iff, for every -interpretation M, M |= ψ iff there exists M |= ϕ s.t. M V M

iff Mod (ψ) = {M is an -interpretation | M |= ϕ and M V M } iff Mod (ψ) = Mod(ϕ) V .

Lemma 4 Let X, Y, H, T and V be subsets of A.

(i) If X V H and Y V T then X Y V H T and X Y V H T.

(ii) If X V H and Y V T then H T V V X Y .

Proof: (i) Note that (X Y ) \ V =(X \ V ) (Y \ V ) =(H \ V ) (T \ V ) due to X V H and Y V T =(H T) \ V . Thus X Y V T T. We can similarly prove X Y V H T. (ii) Please note that Y = {p |p Y }, V = {p |p V } and T = {p |p V }. We have that (H T ) \ (V V ). = (H \ (V V )) (T \ (V V )) = (H \ V ) (T \ V ) since H V = and T V = = (X \ V ) (Y \ V ) since H V H and T V Y

= (X \ (V V )) (Y \ (V V )) since X V = and Y V = = (X Y ) \ (V V ). It follows that H T V V X Y .

Theorem 6 (Expressibility theorem) Let ϕ be a formula and V a set of atoms. There exists a formula ψ such that Mod (ψ) = Mod (ϕ) V .

Proof: For every X, Y Mod (ϕ) V , there exists H, T |= ϕ such that H, T V X, Y , i.e. X V H and Y V T. By (i) of Proposition 3, T, T |= ϕ. Thus Y, Y Mod (ϕ) V due to Y, Y V T, T . It follows that the collection Mod (ϕ) V satisfies the condition (8), then there is a formula ψ such that Mod (ψ) = Mod (ϕ) V by Proposition 4.

Lemma 5 A formula ϕ is -irrelevant to a set V of atoms iff H, T |= ϕ implies X, Y |= ϕ for every two -interpretations X, Y and H, T with X, Y V H, T

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

Proof: ϕ is -irrelevant to V iff there exists a formula ψ mentioning no atoms in V such that ϕ ψ iff there exists a formula ψ mentioning no atoms in V s.t Mod (ϕ) = Mod (ψ) iff Mod (ϕ) = { X, Y |X Y and H, T V X, Y s.t H, T |= ϕ} iff H, T |= ϕ implies X, Y |= ϕ for every two -interpretations X, Y and H, T such that X, Y V H, T .

Proposition 10 Let ψ and ϕ be two formulas and V a set of atoms.

(i) IR (Forget (ψ, V ), V ).

(ii) ψ has a -model iff Forget (ψ, V ) has.

(iii) ψ |= Forget (ψ, V ).

(iv) If ψ |= ϕ then Forget (ψ, V ) |= Forget (ϕ, V ).

(v) Forget (ψ ϕ, V ) Forget (ψ, V ) Forget (ϕ, V ).

(vi) Forget (ψ ϕ, V ) |= Forget (ψ, V ) Forget (ϕ, V ).

(vii) Forget (ψ ϕ, V ) Forget (ψ, V ) ϕ if IR (ϕ, V ).

Proof: (i) It immediately follows from Lemma 5. (ii) It is evident that Mod (ψ) = iff Mod (ψ) V = by Definition 8. (iii) It is easy to see that Mod (ψ) Mod (ψ) V by Definition 8. (iv) Let ψ |= ϕ, and H, T |= Forget (ψ, V ), i.e. H, T Mod (ψ) V . In terms of Definition 8, there exists H , T |= ψ such that H, T V H , T . It implies that H , T |= ϕ since ψ |= ϕ. Thus H, T Mod (ϕ) V , i.e. H, T |= Forget (ϕ, V ). (v) H, T |= Forget (ψ ϕ, V ) iff H, T Mod (ψ ϕ) V iff H , T |= ψ ϕ such that H, T V H , T iff H , T such that H, T V H , T and, either H , T |= ψ or H , T |= ϕ iff H, T Mod (ψ) V or H, T Mod (ϕ) V iff H, T |= Forget (ψ, V ) or H, T |= Forget (ψ, V ) iff H, T |= Forget (ψ, V ) Forget (ψ, V ). (vi) H, T |= Forget (ψ ϕ, V ) H, T Mod (ψ ϕ) V H , T |= ψ ϕ such that H, T V H , T H , T such that. H, T V H , T , H , T |= ψ and H , T |= ϕ H, T Mod (ψ) V and H, T Mod (ϕ) V H, T |= Forget (ψ, V ) and H, T |= Forget (ϕ, V ) H, T |= Forget (ψ, V ) Forget (ϕ, V ). (vii) The direction from left to right follows from (vi) and the fact IR(ϕ, V ), i.e. Forget (ϕ, V ) ϕ. Let us consider the other direction. H, T |= Forget (ψ, V ) ϕ H, T |= Forget (ψ, V ) and H, T |= ϕ H , T |= ψ such that H, T V H , T , and H, T |= ϕ

WANG, ZHANG, ZHOU, & ZHANG

H, T V H , T such that H , T |= ψ ϕ by IR(ϕ, V ) and Lemma 5 H, T Mod (ψ ϕ) V H, T |= Forget (ψ ϕ, V ).

Theorem 8 (Horn expressibility) Let Π be a Horn logic program and V A. There is a Horn logic program Π such that Forget (Π, V ) Π .

Proof: In terms of Proposition 2, it suffices to prove for = HT. Let M = Mod HT(Π) V . By Proposition 6, it is sufficient to show that M satisfies conditions (5) and (12). We first prove that M satisfies (5). For each HT-interpretation X, Y M, we have that X Y , and there exists H, T Mod HT(Π) such that X, Y V H, T . Note that Π is positive, which shows that H, H and T, T are HT-models of Π by Lemma 2. Thus X, X M and Y, Y M due to X V H and T V Y . On the other hand, suppose X, X M, Y, Y M and X Y . There exist two HT-models H , T and H , T of Π such that H , T V X, X and H , T V Y, Y . By Lemma 2, we have H |= Π, T |= Π, H |= Π and T |= Π. Since models of Horn theories are closed under set intersection (Alfred, 1951), H H |= Π. By Lemma 2 again, we have H H , T |=HT Π. By Lemma 4, H H V X Y (= X). Thus H H , T V X, Y . It follows X, Y M. Now we show that M satisfies (12). Suppose X, Y and H, T are two HT-interpretations in M. It follows that there are two HT-models X , Y and H , T of Π such that X , Y V X, Y and H , T V H, T . Since Π is Horn, we have that H X , T Y |=HT Π by Proposition 6. By Lemma 4, we have H X V H X and Y T V Y T. It implies H X , T Y V X H, Y T , thus X H, Y T M.

Proposition 11 Let Π be a disjunctive logic program, V A. We have that Forget (Π, V ) is expressible in disjunctive logic programs if and only if,

H1, T1 |= Π, T2, T2 |= Π and T1 T2 H3, T3 |= Π such that H3, T3 V H1, T2 .

Proof: By Proposition 2, it suffices to prove = HT. Let Π HT Forget HT(Π, V ). The direction from left to right is obvious. We show the other direction. Suppose that Π is not expressible in disjunctive logic programs. There exists X, Y |=HT Π , Y Y and Y , Y |=HT Π such that X, Y |=HT Π . It follows that, for each H1, T1 |=HT Π and T2, T2 |=HT Π such that H1, T1 V X, Y , T2 V Y and T1 T2, there exists no H3, T3 |=HT Π such that H3, T3 V H1, T2 , viz. H3, T3 V X, Y by X, Y V H1, T2 , a contradiction.

Proposition 12 Let Π be a normal logic program, V A. Then Forget (Π, V ) is expressible in normal logic programs if and only if, in addition to condition (21), the following condition holds,

H1, T1 |= Π, H2, T2 |= Π and T1 V T2 H3, T3 |= Π such that H3 V H1 H2 and (T3 V T1 or T3 V T2). (21)

Proof: By Proposition 2, it suffices to prove = HT. Let Π HT Forget HT(Π, V ). The direction from left to right is easy. We consider the other direction in what follows. In terms of Proposition 11 and Corollary 3, it is sufficient to show that, for each X, Y |=HT Π

and X , Y |=HT Π , X X , Y |=HT Π according to Corollary 3. Suppose that X, Y and

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

X , Y are two HT-models of Π . There are two HT-models H1, T1 and H2, T2 of Π such that X, Y V H1, T1 and X , Y V H2, T2 . It follows that T1 V T2 and, by condition (21), there exists an HT-model H3, T3 of Π satisfying either H3, T3 V H1 H2, T1 or H3, T3 V H1 H2, T2 , which shows H3, T3 V X X , Y , hence X X , Y |=HT Π .

Theorem 10 (Representation theorem) Let ψ and ϕ be two formulas and V a set of atoms. Then the following statements are equivalent:

(i) ϕ Forget (ψ, V ).

(ii) ϕ {ϕ | ψ |= ϕ and IR (ϕ , V )}.

(iii) Postulates (W), (PP), (NP) and (IR) hold.

Proof: Let Σ = {ξ | ψ |= ξ and IR (ξ, V )}. It is evident that IR (Σ , V ). The equivalence between (i) and (ii) follows from Corollary 9. (ii) obviously implies (iii). It suffices to show (iii) (ii). By Positive Persistence, we have ϕ |= ξ for each ξ Σ , from which follows Mod (ϕ) Mod (Σ ). On the other hand, by ( W) ψ |= ϕ and (IR) IR (ϕ, V ), it follows ϕ Σ . Thus Mod (Σ ) Mod (ϕ). Thus ϕ Σ .

Proposition 13 Let ϕ, ϕ , ψ be formulas and V A such that ϕ Forget (ψ, V ) and ϕ Forget(ψ, V ). Then

(ii) ϕ |= ϕ.

Proof: (i) T |= ϕ iff T, T |= ϕ by (i) of Proposition 3 iff T, T |= Forget (ψ, V ) since ϕ Forget (ψ, V ) iff Y, Y |= ψ such that T, T V Y, Y by Definition 8 iff Y |= ψ such that T V Y by (i) of Proposition 3 iff T |= Forget(ψ, V ) by Corollary 5 iff T |= ϕ since ϕ Forget(ψ, V ). (ii) H, T |= ϕ

T |= ϕ by (i) of Proposition 3 T |= Forget( ψ, V ) since ϕ Forget( ψ, V ) Y |= ψ such that Y V T by Corollary 5 H \ V, Y |= ψ such that Y V T by (ii) of Proposition 3 H, T |= Forget ( ψ, V ) due to H \ V, Y V H, T and Definition 8 H, T |= ϕ due to Forget ( ψ, V ) ϕ.

Proposition 14 Let Π and Π be two Horn logic programs, and V a set of atoms such that Π Forget(Π, V ). Then Π Forget (Π, V ).

WANG, ZHANG, ZHOU, & ZHANG

Proof: By Proposition 2, it suffices to show = HT. ( ) H , T |=HT Π

H |= Π and T |= Π by Lemma 2 H, T such that H |= Π, T |= Π, H V H and T V T by Π Forget(Π, V ) H, T such that H T |= Π, T |= Π, H T V H and T V T

H, T such that H T, T |=HT Π and H T, T V H , T H , T |=HT Forget HT(Π, V ). ( ) H , T |=HT Forget HT(Π, V ) H, T |=HT Π such that H , T V H, T H T such that H |= Π, T |= Π and H , T V H, T by Lemma 2 H |= Forget(Π, V ) and T |= Forget(Π, V ) H |= Π and T |= Π due to Π Forget(Π, V ) H , T |=HT Π .

Proposition 15 Let ψ and ϕ be two formulas and V a set of atoms.

(i) ϕ Forget(ψ, V ) iff ϕ Forget ( ψ, V ).

(ii) Forget(ϕ, V ) Forget(ψ, V ) iff Forget ( ϕ, V ) Forget ( ψ, V ).

Proof: (i) ( ) H, T |= ϕ iff T |= ϕ, i.e. T |= ϕ by (ii) of Proposition 3 iff T |= Forget(ψ, V ) since ϕ Forget(ψ, V ) iff Y |= ψ i.e. Y |= ψ such that Y V T by Corollary 5 iff H \ V, Y |= ψ (H \ V T \ V = Y \ V ) by (ii) of Proposition 3 iff H, T |= Forget ( ψ, V ) by Definition 8. ( ) T |= ϕ i.e. T |= ϕ iff H, T |= ϕ by (ii) of Proposition 3 iff H, T |= Forget ( ψ, V ) for H T since ϕ Forget ( ψ, V ) iff X, Y |= ψ such that H, T V X, Y by Definition 8 iff Y |= ψ such that Y V T by (ii) or Proposition 3 iff T |= Forget( ψ, V ) by Corollary 5. (ii) ( ) H, T |= Forget ( ϕ, V ) iff X, Y |= ϕ such that X, Y V H, T by Definition 8 iff Y |= ϕ i.e. Y |= ϕ such that Y V T by (ii) of Proposition 3 iff T |= Forget(ϕ, V ) by Corollary 5 iff T |= Forget(ψ, V ) since Forget(ϕ, V ) Forget(ψ, V ) iff Y |= ψ i.e. Y |= ψ such that Y V T by Definition 8 iff X \ V, Y |= ψ by (ii) of Proposition 3 (X \ V Y \ V = Y \ V ) iff H, T |= Forget ( ψ, V ) by H, T V X \ V, Y and Definition 8. ( ) T |= Forget(ϕ, V ) iff Y |= ϕ i.e. Y |= ϕ such that Y V T by Corollary 5 iff X, Y |= ϕ such that Y V T by (ii) of Proposition 3 iff X \ V, T |= Forget ( ϕ, V ) X \ V, T V X, Y and by Definition 8 iff X \ V, T |= Forget ( ψ, V ) since Forget ( ϕ, V ) Forget ( ψ, V ) iff X , Y |= ψ such that X \ V, T V X , Y by Definition 8

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

iff Y |= ψ i.e. Y |= ψ such that T V Y by (ii) of Proposition 3 iff T |= Forget(ψ, V ) by Corollary 5.

Theorem 12 ( -forgetting vs propositional forgetting) Let ψ and ϕ be two formulas of LA and V A. Then

ϕ Forget (ψ, V ) iff (A) |= τ [ϕ] Forget( (A) {τ [ψ]}, V V ).

Proof: ( ) Let M = MA M A be a model of (A). M |= (A) {τ [ϕ]} iff MA, M A |= ϕ by Proposition 8 iff MA, M A |= Forget (ψ, V ) since ϕ Forget (ψ, V ) iff H, T |= ψ such that H, T V MA, M A by Definition 8 iff H, T |= ψ such that H V MA and T V M A iff H T |= (A) {τ [ψ]} and H V MA and T V MA by Proposition 8 iff H T |= (A) {τ [ψ]} and H T V V MA MA by Lemma 4 iff MA MA |= Forget( (A) {τ [ψ]}, V V ) by Definition 8 iff M |= Forget( (A) {τ [ψ]}, V V ). ( ) X, Y |= ϕ iff X Y |= (A) {τ [ϕ]} by Proposition 8 iff X Y |= (A) Forget( (A) {τ [ψ]}, V V ) iff M |= (A) {τ [ψ]} such that M V V X Y

iff MA, M A |= ψ such that MA M A V X Y by Proposition 8 iff X, Y |= Forget (ψ, V ) due to X, Y V MA, M A by Definition 8.

Proposition 16 Let ψ and ϕ be two formulas of LA and V a set of atoms. Then Forget (ψ, V ) Forget (ϕ, V ) iff the following condition holds:

Forget({τ [ψ]} (A), V V ) Forget({τ [ϕ]} (A), V V ).

Proof: ( ) We show Forget({τ [ψ] (A), V V ) |= Forget({τ [ϕ] (A), V V ). The other side can be similarly proved. M |= Forget({τ [ψ]} (A), V V ) N A A such that N V V M and N |= {τ [ψ]} (A) X, Y |= ψ with N = X Y by Proposition 8 X, Y |= Forget (ψ, V ) by (iii) of Proposition 10 X, Y |= Forget (ϕ, V ) as Forget (ψ, V ) Forget (ϕ, V ) H, T |= ϕ such that H, T V X, Y by Definition 8 H T |= τ [ϕ] (A) by Proposition 8 X Y |= Forget({τ [ϕ]} (A), V V ) as H T V V X Y

M |= Forget({τ [ϕ]} (A), V V ) by M V V X Y (= N). ( ) We show Forget (ψ, V ) |= Forget (ϕ, V ). The other side is similar. H, T |= Forget (ψ, V ) X, Y |= ψ such that H, T V X, Y ) by Definition 8 X Y |= {τ [ψ]} (A) by Proposition 8 X Y |= Forget({τ [ψ]} (A), V V )

WANG, ZHANG, ZHOU, & ZHANG

X Y |= Forget({τ [ϕ]} (A), V V ) H1 T 1 |= {τ [ϕ]} (A) such that H1 T 1 V V X Y

H1, T1 |= ϕ by Proposition 8 X, Y |= Forget (ϕ, V ) as X, Y V H1, T1 by Definition 8 H, T |= Forget (ϕ, V ) as X, Y V H, T .

Theorem 14 Let ψ and ϕ be two formulas and V a set of atoms.

(i) The problem of deciding if ψ Forget (ψ, V ) is co-NP-complete.

(ii) The problem of deciding if Forget (ϕ, V ) Forget (ψ, V ) is ΠP 2 -complete.

(iii) The problem of deciding if ϕ Forget (ψ, V ) is ΠP 2 -complete.

Proof: (i) Membership. Recall that ψ |= Forget (ψ, V ) by (iii) of Proposition 10. We have ψ Forget (ψ, V ) iff Forget (ψ, V ) |= ψ iff X, Y |= Forget (ψ, V ) and X, Y |= ψ iff H, T |= ψ such that H, T V X, Y and X, Y |= ψ. Since both guessing H, T , X, Y and checking the -satisfiability can be done in polynomial time in the size of ψ and V . Thus the complement of ψ Forget (ψ, V ), i.e. ψ Forget (ψ, V ), is in co-NP. The hardness follows from the fact that, by (i) of Proposition 15, ψ Forget ( ψ, V ) iff ψ Forget(ψ, V ), which is co-NP-complete (cf., see Lang et al., 2003, Prop. 10). (ii) Membership. If Forget (ϕ, V ) Forget (ψ, V ) then there exists a -interpretation H, T such that either

(a) H, T |= Forget (ϕ, V ) and H, T |= Forget (ψ, V ), or

(b) H, T |= Forget (ϕ, V ) and H, T |= Forget (ψ, V ).

On the one hand, to guess a -interpretation H, T is feasible by a nondeterministic Turing machine. On the other hand, checking if H, T |= ϕ is feasible by a deterministic Turing machine; and H, T |= Forget (ϕ, V ) iff there exists X, Y |= ϕ such that X, Y V H, T . Thus checking the conditions (a) and (b) can be done in polynomial time in the size of ψ and ϕ by calling a nondeterministic Turing machine. Thus the problem is in ΠP 2 . Note that, by (ii) of Proposition 15, Forget ( ϕ, V ) Forget ( ψ, V ) iff Forget(ϕ, V ) Forget(ψ, V ), which is ΠP 2 -complete (cf., see Lang et al., 2003, Prop. 24). Thus the hardness follows. (iii) Membership. Note that ϕ Forget (ψ, V ) iff there is a -interpretation H, T such that

H, T |= ϕ and H, T |= Forget (ψ, V ), or

H, T |= ϕ and H, T |= Forget (ψ, V ).

Similar to the case of (ii), the guessing and checking are in polynomial time in the size of ϕ, ψ and V by calling a nondeterministic Turing machine. Thus the problem is in ΠP 2 . Note that ϕ Forget (ψ, V ) iff ϕ Forget (ϕ, V ) and Forget (ϕ, V ) Forget (ψ, V ), the latter is ΠP 2 -hard by (ii). Then the hardness follows.

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

Proposition 17 Let ψ and ϕ be two formulas and V a set of atoms.

(i) The problem of deciding whether ψ |= Forget (ϕ, V ) is ΠP 2 -complete.

(ii) The problem of deciding whether Forget (ψ, V ) |= ϕ is co-NP-complete.

Proof: (i) Membership. Recall that ψ |= Forget (ϕ, V ) iff there exists a -model H, T of ψ such that H, T |= Forget (ϕ, V ). As H, T |= Forget (ϕ, V ) iff X, Y |= ϕ for every - interpretation X, Y such that X, Y V H, T . Such H, T can be guessed in polynomial time in the size of ϕ, ψ and V . Checking H, T |= Forget (ϕ, V ) is possible in polynomial time in the size of ϕ, ψ and V by calling a nondeterministic Turing machine. Thus the original problem is in Πp 2. Hardness. It follows from the following fact: |= Forget ( ϕ, V ) iff Forget ( ϕ, V ) iff Forget(ϕ, V ) by (i) of Proposition 15 ( ) iff the QBF

V V ϕ is valid, which is ΠP 2 -complete (Papadimitriou, 1994). (ii) Membership. Note that Forget (ψ, V ) |= ϕ iff H, T |= Forget (ψ, V ) such that H, T |= ϕ iff X, Y |= ψ such that X, Y V H, T and H, T |= ϕ. Since the guessing and checking are both polynomial in the size of ψ, ϕ and V , the original problem is in co-NP. Hardness follows from the fact that Forget (ψ, V ) |= iff ψ |= by (ii) of Proposition 10 iff ψ has no -model, which is co-NP-complete by Proposition 9.

Appendix D. Forgetting Operators FW and FS

Wong proposed six postulates and argued that the postulates should to respected by all forgetting operators in disjunctive logic programs under strong equivalence:

(F-1) If Π |=HT Σ then F(Π, a) |=HT F(Σ, a);

(F-2) If a does not appear in , then F({r} , a) HT F({r}, a) ;

(F-3) F(Π, a) does not contain any atoms not in Π;

(F-4) If F(Π, a) |=HT r then F({s}, a) |=HT r for some s Cn(Π);

(F-5) If F(Π, a) |=HT (A B, not C), then Π |=HT (A B, not C, not a);

(F-6) F(F(Π, a), b) HT F(F(Π, b), a)

where F is a forgetting operator, Π, Σ and are disjunctive logic programs, a and b are atoms, r is a disjunctive rule, and

Cn(Π) ={r| r is a disjunctive rule such that Π |=HT r and var(r) var(Π)}.

WANG, ZHANG, ZHOU, & ZHANG

where var(α) is the set of atoms occurring in α. Accordingly, he proposed two forgetting operators FS and FW: the result of forgetting an atom a from a disjunctive logic program Π is defined by the below procedure:

(1) Let Π1 = Cn(Π).

(2) Form Π1, remove rules of the form (A B, a, not C), replace each rule of the form (A {a} B, not C, not a) with (A B, not C, not a). Let the resulting logic program be Π2.

(3) Replace or remove each rule in Π2, of the form (A B, not C, not a) or (A {a} B, not C) according to the following table:

A B, not C, not a

A {a} B, not C

Let Π3 be the resulting logic program.

The logic program Π3 is the result of forgetting p from Π.

Alfred, H. (1951). On sentences which are true of direct unions of algebras. The Journal of Symbolic Logic, 16(1), 14 21.

Bobrow, D. G., Subramanian, D., Greiner, R., & Pearl, J. (Eds.). (1997). Special issue on relevance 97 (1-2). Artificial Intelligence Journal.

Cabalar, P., & Ferraris, P. (2007). Propositional theories are strongly equivalent to logic programs. Theory and Practice of Logic Programming, 7(6), 745 759.

Delgrande, J. P., Schaub, T., Tompits, H., & Woltran, S. (2013). A model-theoretic approach to belief change in answer set programming. ACM Transactions on Computational Logic, 14(2), A:1 A:42.

Eiter, T., Fink, M., Tompits, H., & Woltran, S. (2004). On eliminating disjunctions in stable logic programming. In Principles of Knowledge Representation and Reasoning: Proceedings of the Ninth International Conference (KR2004), pp. 447 458, Whistler, Canada. AAAI Press.

Eiter, T., & Wang, K. (2008). Semantic forgetting in answer set programming. Artificial Intelligence, 172(14), 1644 1672.

Faber, W., Pfeifer, G., & Leone, N. (2011). Semantics and complexity of recursive aggregates in answer set programming. Artificial Intelligence, 175(1), 278 298.

Ferraris, P. (2005). Answer sets for propositional theories. In Logic Programming and Nonmonotonic Reasoning, 8th International Conference, Vol. 3662 of Lecture Notes in Computer Science, pp. 119 131, Diamante, Italy. Springer.

Ferraris, P., Lee, J., & Lifschitz, V. (2011). Stable models and circumscription. Artificial Intelligence, 175(1), 236 263.

Ferraris, P., & Lifschitz, V. (2005). Mathematical foundations of answer set programming. In Art emov, S. N., Barringer, H., d Avila Garcez, A. S., Lamb, L. C., & Woods, J. (Eds.), We Will Show Them! Essays in Honour of Dov Gabbay, Vol. 1, pp. 615 664. College Publications.

KNOWLEDGE FORGETTING IN ANSWER SET PROGRAMMING

Gabbay, D. M., Pearce, D., & Valverde, A. (2011). Interpolable formulas in equilibrium logic and answer set programming. Journal of Artificial Intelligence Research, 42, 917 943.

Gelfond, M., & Lifschitz, V. (1988). The stable model semantics for logic programming. In Proceedings of the Fifth International Conference and Symposium on Logic Programming, pp. 1070 1080, Seattle, Washington. MIT Press.

Goranko, V., & Otto, M. (2007). Handbook of Modal Logic, Vol. 3, chap. 5 Model Theory Of Modal Logic, pp. 249 329. Elsevier.

Jongh, D. D., & Hendriks, L. (2003). Characterization of strongly equivalent logic programs in intermediate logics. Theory and Practice of Logic Programming, 3(3), 259 270.

Kontchakov, R., Wolter, F., & Zakharyaschev, M. (2008). Can you tell the difference between dl-lite ontologies?. In Principles of Knowledge Representation and Reasoning: Proceedings of the Eleventh International Conference, KR 2008, pp. 285 295, Sydney, Australia. AAAI Press.

Lang, J., Liberatore, P., & Marquis, P. (2003). Propositional independence: Formula-variable independence and forgetting. Journal of Artificial Intelligence Research, 18, 391 443.

Lang, J., & Marquis, P. (2010). Reasoning under inconsistency: A forgetting-based approach. Artificial Intelligence, 174(12-13), 799 823.

Lifschitz, V., Pearce, D., & Valverde, A. (2001). Strongly equivalent logic programs. ACM Transactions on Computational Logic, 2(4), 526 541.

Lifschitz, V., Tang, L. R., & Turner, H. (1999). Nested expressions in logic programs. Annals of Mathematics and Artificial Intelligence, 25(3-4), 369 389.

Lin, F. (2001). On strongest necessary and weakest sufficient conditions. Artificial Intelligence, 128(1-2), 143 159.

Lin, F. (2002). Reducing strong equivalence of logic programs to entailment in classical propositional logic. In Proceedings of the Eights International Conference on Principles and Knowledge Representation and Reasoning (KR-02), pp. 170 176, Toulouse, France. Morgan Kaufmann.

Lin, F., & Chen, Y. (2007). Discovering classes of strongly equivalent logic programs. Journal of Artificial Intelligence Research, 28, 431 451.

Lin, F., & Reiter, R. (1994). Forget it!. In In Proceedings of the AAAI Fall Symposium on Relevance, pp. 154 159.

Lin, F., & Zhou, Y. (2011). From answer set logic programming to circumscription via logic of GK. Artificial Intelligence, 175(1), 264 277.

Liu, Y., & Wen, X. (2011). On the progression of knowledge in the situation calculus. In IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, pp. 976 982, Barcelona, Catalonia, Spain. IJCAI/AAAI.

Lutz, C., & Wolter, F. (2011). Foundations for uniform interpolation and forgetting in expressive description logics. In IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, pp. 989 995, Barcelona, Catalonia, Spain. IJCAI/AAAI.

Osorio, M., & Cuevas, V. (2007). Updates in answer set programming: An approach based on basic structural properties. TPLP, 7(4), 451 479.

WANG, ZHANG, ZHOU, & ZHANG

Osorio, M., & Zacarias, F. (2004). On updates of logic programs: A properties-based approach. In Seipel, D., & Torres, J. M. T. (Eds.), Fo IKS, Vol. 2942 of Lecture Notes in Computer Science, pp. 231 241. Springer.

Packer, H. S., Gibbins, N., & Jennings, N. R. (2011). An on-line algorithm for semantic forgetting. In IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, pp. 2704 2709, Barcelona, Catalonia, Spain. IJCAI/AAAI.

Papadimitriou, C. H. (1994). Computational complexity. Addison Wesley.

Pearce, D., Tompits, H., & Woltran, S. (2001). Encodings for equilibrium logic and logic programs with nested expressions. In Proceedings of the10th Portuguese Conference on Artificial Intelligence on Progress in Artificial Intelligence, Knowledge Extraction, Multi-agent Systems, Logic Programming and Constraint Solving, pp. 306 320, London, UK. Springer-Verlag.

Pearce, D., Tompits, H., & Woltran, S. (2009). Characterising equilibrium logic and nested logic programs: Reductions and complexity. Theory and Practice of Logic Programming, 9(5), 565 616.

Su, K., Sattar, A., Lv, G., & Zhang, Y. (2009). Variable forgetting in reasoning about knowledge. Journal of Artificial Intelligence Research, 35, 677 716.

Truszczynski, M. (2010). Reducts of propositional theories, satisfiability relations, and generalizations of semantics of logic programs. Artificial Intelligence, 174(16-17), 1285 1306.

van Ditmarsch, H. P., Herzig, A., Lang, J., & Marquis, P. (2009). Introspective forgetting. Synthese, 169(2), 405 423.

Visser, A. (1996). Uniform interpolation and layered bisimulation. In G odel 96, pp. 139 164.

Wang, Y., Wang, K., & Zhang, M. (2013). Forgetting for answer set programs revisited. In IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, pp. 1162 1168, Beijing, China. IJCAI/AAAI.

Wang, Y., Zhang, Y., Zhou, Y., & Zhang, M. (2012). Forgetting in logic programs under strong equivalence. In Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference, pp. 643 647, Rome, Italy. AAAI Press.

Wang, Z., Wang, K., Topor, R. W., & Pan, J. Z. (2010). Forgetting for knowledge bases in dl-lite. Annuals of Mathematics and Artificial Intelligence, 58(1-2), 117 151.

Wong, K.-S. (2009). Forgetting in Logic Programs. Ph.D. thesis, The University of New South Wales.

Zhang, Y., & Foo, N. Y. (2006). Solving logic program conflict through strong and weak forgettings. Artificial Intelligence, 170(8-9), 739 778.

Zhang, Y., & Zhou, Y. (2009). Knowledge forgetting: Properties and applications. Artificial Intelligence, 173(16-17), 1525 1537.

Zhou, Y., & Zhang, Y. (2011). Bounded forgetting. In Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2011, pp. 280 285, San Francisco, California, USA. AAAI Press.