On Forgetting Postulates in Answer Set Programming

Introduction

It has been well argued that for cognitive robotics the ability of eliminating or hiding irrelevant symbols in a knowledge base, known as (variable) forgetting, plays an important role in logic-based agent systems [Lin and Reiter, 1994]. In simple words, forgetting is a process on a logical formula that replaces some logic symbols by true on the one hand and by false on the other, to produce a formula that no longer contains these symbols. Forgetting has found several interesting applications in Artificial Intelligence, such as regression and progression in databases and planning [Lin and Reiter, 1997; Liu and Wen, 2011; Rajaratnam et al., 2014], abduction and diagnosis [Lin, 2001], conflict resolution [Lang and Marquis, 2010], and abstracting and comparing ontologies [Wang et al., 2010; Konev et al., 2012].

Logic programming under stable model (or answer set) semantics [Gelfond and Lifschitz, 1988; Ferraris, 2005], com-

∗Corresponding Author.

Jia-Huai You

University of Alberta Edmonton, Canada you@cs.ualberta.ca

Yisong Wang∗

Guizhou University Guiyang, China csc.yswang@gzu.edu.cn

monly referred to as Answer Set Programming (ASP), is a paradigm for declarative problem solving [Baral, 2003]. In ASP, various notions of equivalence have been proposed: (standard) equivalence, strong equivalence [Lifschitz et al., 2001], uniform equivalence [Eiter et al., 2007], and modular equivalence [Janhunen et al., 2009]. Among these, the first two are most relevant in this paper. Informally, given two logic program Π and Π′ , they are equivalent if they have the same answer sets; they are strongly equivalent if Π ∪ Σ and Π′ ∪Σ have the same answer sets for every logic program Σ. The latter allows for "equivalent replacement" in ASP, and can thus be used to simplify logic programs [Lifschitz et al., 2001]. The notion of strong equivalence can be characterized in the logic here-and-there (HT) [Pearce, 1996]. Since HT is a monotonic logic, ASP admits a monotonic entailment relation, written |=HT, between logic programs by regarding a logic program as a logical formula.

Recently, researchers have shown a focused interest in forgetting in ASP [Delgrande and Wang, 2015], with a number of varying notions of forgetting proposed, such as the strong and weak forgetting [Zhang and Foo, 2006], the semantic forgetting [Eiter and Wang, 2008], forgetting operators FW and FS [Wong, 2009], the knowledge forgetting [Wang et al., 2012; 2014], the SM-forgetting [Wang et al., 2013], and the strong AS-forgetting [Knorr and Alferes, 2014]. Forgetting is also investigated for some nonmonotonic logical systems [Wang et al., 2015]. In the above literature, several desirable properties have been formulated, which we briefly introduce below.

Let L be an ASP language on a signature A, Π a logic program in L, V ⊆ A, and f(Π, V ) the result of forgetting about V in Π. Let AS(Π) denote the set of all answer sets of Π. The desirable properties about f can be described informally as follows:

• (E) Existence: f(Π, V ) is expressible in L.
• (IR) Irrelevance: f(Π, V ) is irrelevant to V in terms of strong equivalence.
• (W) Weakening: Π |=HT f(Π, V ).
• (PP) Positive Persistence: if Π |=HT Π′ and Π′ is irrelevant to V then f(Π, V ) |=HT Π′ .
• (NP) Negative Persistence: if Π ̸|=HT Π′ and Π′ is irrelevant to V then f(Π, V ) ̸|=HT Π′ .

• (SE) Strong Equivalence: If Π and Π′ are strongly equivalent, then f(Π, V ) and f(Π′ , V ) are strongly equivalent.
• (CP) Consequence Persistence: AS(f(Π, V )) = {M \ V | M ∈ AS(Π)}.
• (SP) Strong Persistence: AS(f(Π, V )∪Π′ ) = {M\V | M ∈ AS(Π ∪ Π′ )} for all programs Π′ over signature A \ V .

The intended meanings of the first seven properties are easy to understand. For instance, the property (IR) requires that the forgetting result f(Π, V ) is strongly equivalent to a logic program containing no variable from V . The property (SP) says that the result of forgetting should preserve all the semantic dependencies contained in the original program, for all but the atom(s) to be forgotten [Knorr and Alferes, 2014]. It is evident that (CP) is a special case of (SP). It has been shown that these properties together are inconsistent, in the sense that if f satisfies (IR), (E) and (CP) then it violates (W) [Wang et al., 2013].

The first four properties, i.e., (W), (PP), (NP) and (IR), were proposed by Zhang and Zhou (2009) for knowledge forgetting in modal logic S5. The property (CP) was originally proposed by Eiter and Wang (2008) for a semantical notion of forgetting in ASP, which satisfies (E) and (IR), but none of (W), (PP), (NP), (SE), and (SP). Wang et al. (2012) adapted (W), (PP), (NP), and (IR) for knowledge forgetting in ASP, which satisfies both (E) and (SE), but fails for (CP) and (SP). Later, Wang et al. (2013) proposed SM-forgetting in ASP, which satisfies (E), (IR), (SE), (CP), and (PP), but none of (W), (NP), and (SP). Knorr and Alferes (2014) proposed strong AS-forgetting, which satisfies (IR), (SE), (CP), and (SP), but not (E) in general.

In this paper, with the focus on the knowledge forgetting operator in propositional ASP - Forget HT - which is known to enjoy the first six properties [Wang et al., 2012; 2014], we investigate possible restrictions for a logic program and a set of forgotten variables under which Forget HT also satisfies (SP). This allows us to explore syntactically restricted subclasses of logic programs for which Forget HT enjoys all of the well-recognized properties.

In addition, as knowledge forgetting is defined semantically [Wang et al., 2012; 2014] and, to our knowledge, there have been no syntactic characterizations for it, we propose a syntax-based approach for knowledge forgetting, which can be used as a syntactic transformation to compute knowledge forgetting.

The main contributions of the paper are as follows:

• We identify a sufficient and necessary condition for a logic program Π and a set of atoms V for which Forget HT satisfies the property (SP), i.e. AS(Forget HT (Π, V ) ∪ Π′ ) = {M \ V | M ∈ AS(Π∪Π′ )} for every logic program Π′ containing no atom from V . This implies that we have found the largest set ∆ of pairs (Π, V ) such that Forget HT satisfies all the properties under ∆ (see Definition 2). We also study the complexity on checking whether a logic program and a set of atoms satisfy the condition.
• We obtain a syntactic counterpart of the (semanticsbased) knowledge forgetting in ASP. It is substantially

different from the syntactic definition for the forgetting in classical propositional logic.

The rest of the paper is organized as follows. Section briefly reviews the necessary concepts about ASP, the logic here-and-there, more details on desirable properties, and knowledge forgetting for ASP. In Section we show a sufficient and necessary condition for knowledge forgetting that satisfies the property (SP), and study the computational complexities on checking the condition. Section presents a syntactic approach for knowledge forgetting. Finally, Section provides concluding remarks along with future directions.

Preliminaries

We assume a propositional language LA over a finite set A of propositional variables (atoms), called the signature of LA. The formulas of LA are inductively constructed using connectives ⊥, ∧, ∨ and ⊃ as the following:

where p ∈ A. The formula ¬ϕ stands for ϕ ⊃ ⊥, while ⊤ for ⊥ ⊃ ⊥. We identify an interpretation with the set of atoms satisfied by it. A set X ⊆ A is a model of a formula ϕ, written X |= ϕ, if X satisfies ϕ in the sense of classical propositional logic. By Mod(ϕ) we denote the set of models of ϕ. A formula ϕ is irrelevant to V ⊆ A, written IR(ϕ, V ), if there is a formula ψ mentioning no atoms from V such that Mod(ϕ) = Mod(ψ), i.e., ϕ is equivalent to ψ.

In the following we recall the basic notions about answer sets of propositional formulas [Ferraris, 2005], the logic of here-and-there [Heyting, 1930; Pearce et al., 2009], and the knowledge forgetting (HT-forgetting) for ASP [Wang et al., 2012; 2014].

Answer sets

Let ϕ, ψ be two formulas and X ⊆ A. The reduct of ϕ relative to X, written ϕX , is defined recursively as follows:

• if X ̸|= ϕ then ϕX = ⊥,
• if X |= p then pX = p, and
• if X |= ϕ⊗ψ then (ϕ⊗ψ)X = ϕX ⊗ψX

where p ∈ A and ⊗ ∈ {∨, ∧, ⊃}. Intuitively, ϕX stands for the formula obtained from ϕ by replacing every outermost subformula not satisfied by X with ⊥. The set X is an answer set of ϕ if it is a subset minimal model of ϕX . By AS(ϕ) we denote the set of answer sets of ϕ.

Under the answer set semantics, two formulas ϕ1 and ϕ2 are equivalent, denoted by ϕ1 ≡AS ϕ2, if they have the same answer sets, viz. AS(ϕ1) = AS(ϕ2); ϕ1 and ϕ2 are strongly equivalent, denoted by ϕ1 ≡sAS ϕ2, if ϕ1 ∧ψ and ϕ2 ∧ψ have the same answer sets for every formula ψ, viz. AS(ϕ1 ∧ψ) = AS(ϕ2∧ψ) for every formula ψ. A formula ϕ is AS-irrelevant to V ⊆ A, written IRAS(ϕ, V ), if there exists a formula ψ mentioning no atoms from V such that ϕ ≡sAS ψ.

A formula ψ is in normal form, if it is a conjunction of formulas (also called rules 1 ) in the following form:

where A, B, C, D are sets of atoms, and we use the notation, for any S ⊆ A, ¬S = {¬p | p ∈ S} and ¬¬S = {¬¬p | p ∈ S}. Every formula ϕ can be translated to a formula ψ in the normal form such that ϕ ≡sAS ψ (cf. Theorem 2 of [Cabalar and Ferraris, 2007]).

A logic program is a finite set of rules. In the following, we identify a logic program Π with the formula ∧ Π unless stated otherwise explicitly.

HT-models

An HT-interpretation is a pair 〈X, Y 〉 such that X ⊆ Y ⊆ A. That an HT-interpretation 〈X, Y 〉 satisfies a formula ϕ, written 〈X, Y 〉 |=HT ϕ, is defined recursively as follows

• for any atom p, 〈X, Y 〉 |=HT p if p ∈ X,
• 〈X, Y 〉 ̸|=HT ⊥,
• 〈X, Y 〉 |=HT ϕ∧ψ if 〈X, Y 〉 |=HT ϕ and 〈X, Y 〉 |=HT ψ,
• 〈X, Y 〉 |=HT ϕ∨ψ if 〈X, Y 〉 |=HT ϕ or 〈X, Y 〉 |=HT ψ,
• 〈X, Y 〉 |=HT ϕ ⊃ ψ if (i) 〈X, Y 〉 |=HT ϕ implies 〈X, Y 〉 |=HT ψ, and (ii) Y |= ϕ ⊃ ψ.

An HT-interpretation 〈X, Y 〉 is an HT-model of a formula ϕ if 〈X, Y 〉 |=HT ϕ. Two formulas ϕ and ψ are HT-equivalent, denoted by ϕ ≡HT ψ, if they have the same HT-models; ϕ HT-entails ψ, denoted by ϕ |=HT ψ, if every HT-model of ϕ is also an HT-model of ψ. An HT-model 〈Y, Y 〉 of ϕ is an equilibrium model of ϕ if there is no X ⊆ A such that X ⊂ Y and 〈X, Y 〉 |=HT ϕ.

As shown in [Lifschitz et al., 2001; Ferraris, 2005; Cabalar and Ferraris, 2007], the notion of HT-model is closely related to answer set.

Proposition 1 Let ϕ, ψ be two formulas and X ⊆ Y ⊆ A.

• (i) 〈X, Y 〉 |=HT ϕ iff X |= ϕY .
• (ii) X is an answer set of ϕ iff 〈X,X〉 is an equilibrium model of ϕ.
• (iii) ϕ ≡sAS ψ iff ϕ ≡HT ψ.

Postulates for forgetting in ASP

We recall the desirable properties (postulates) for forgetting in ASP as introduced in [Eiter and Wang, 2008; Wong, 2009; Wang et al., 2012; 2013; Knorr and Alferes, 2014].

Let ϕ be a formula and V ⊆ A, and f a forgetting operator in ASP, i.e., a formula ψ = f(ϕ, V ) is the result of forgetting V in ϕ. For S ⊆ 2A, we denote by S‖V the set {S \ V | S ∈ S}. The desirable properties are formally defined as follows:

• (E) Existence: ψ is expressible in LA.
• (W) Weakening: ϕ |=HT ψ.
• (IR) Irrelevance: IRAS(ψ, V ).

1 A rule of the form (2) is written as ∨ A ← ∧(B ∪ notC ∪ not notD) in [Lifschitz et al., 1999], where not S = {not p | p ∈ S} and not not S = {not not p | p ∈ S}.

• (PP) Positive Persistence: for any formula φ, if IRAS(φ, V ) and ϕ |=HT φ then ψ |=HT φ.
• (NP) Negative Persistence: for any formula φ, if IRAS(φ, V ) and ϕ ̸|=HT φ then ψ ̸|=HT φ.
• (CP) Consequence Persistence: AS(ψ) = AS(ϕ)‖V .
• (SE) Strong Equivalence: for any formula φ, if ϕ ≡sAS φ then f(ϕ, V ) ≡sAS f(φ, V ).
• (SP) Strong Persistence: for any formula φ, if IRAS(φ, V ) then AS(ψ ∧ φ) = AS(ϕ ∧ φ)‖V .

For every property above, we say that the operator f satisfies the property, if for every formula ϕ and every V ⊆ A, the property holds for f. For instance, if AS(ϕ)‖V = AS(f(ϕ, V )) for each formula ϕ and V ⊆ A then (CP) holds for f, viz., f satisfies (CP).

The first seven properties can be understood easily. For example, the property (CP) requires that the answer sets of the forgetting result ψ are exactly the ones of the original formula ϕ by discarding the forgotten atoms V . The property (SP) says that the result of forgetting should preserve all the semantic dependencies contained in the original formula, for all but the atom(s) to be forgotten [Knorr and Alferes, 2014]. The property (CP) is a special case of (SP). Note that if f satisfies (IR), (E) and (CP), it will violate (W) (see Proposition 3). Thus, these properties together are inconsistent.

The next two propositions clarify the relationships among these properties.

Proposition 2 Given a forgetting operator f in ASP:

• (i) if it satisfies (SP) then it satisfies (CP);
• (ii) if it satisfies (W) then it satisfies (NP);
• (iii) if it satisfies both (IR) and (NP) then it satisfies (W);
• (iv) if it satisfies both (IR) and (SP) then it satisfies (PP) and (SE).

Proof sketch: (iv) For any 〈X, Y 〉 |=HT f(ϕ, V ) with Y ∩ V = ∅, we can construct formula φ1 = ∧ Y and φ2 = ∧ X∧ ∧p,q∈Y \X p ⊃ q. Then Y is the only answer set of f(ϕ, V ) ∧ φ1 and X ⊂ Y implies Y is not an answer set of f(ϕ, V )∧φ2. From (SP), there exists 〈X∗ , Y ∗ 〉 |=HT ϕ with X∗ \ V = X and Y ∗ \ V = Y . These results imply that (PP) and (SE) should be satisfied.

Proposition 3 (Proposition 3 in [Wang et al., 2013]) There is no forgetting operator in ASP that satisfies (W) or (NP) while it also satisfies (IR), (E) and (CP).

The next two corollaries follow from Propositions 2 and 3.

Corollary 1 Given a forgetting operator f in ASP, if it satisfies (W), (IR), (SP) and (E), then it satisfies the rest of the properties, i.e., (PP), (NP), (SE), and (CP).

Corollary 2 There is no forgetting operator in ASP that satisfies (W), (IR), (SP), and (E).

This motivates the following definition which allows us to talk about restrictions on the domain of a forgetting operator.

Definition 1 Let ∆ be a set of pairs (ϕ, V ) where ϕ is a formula and V ⊆ A, and f a forgetting operator. The operator f satisfies a property under ∆ if f(ϕ, V ) has the corresponding property for every (ϕ, V ) ∈ ∆.

For instance, we say that f satisfies (SE) under ∆ if f(ϕ, V ) ≡sAS f(ϕ′ , V ) for every (ϕ, V ) and (ϕ′ , V ) in ∆ with ϕ′ ≡sAS ϕ; f satisfies (CP) under ∆ if AS(f(ϕ, V )) = AS(ϕ)‖V for every (ϕ, V ) ∈ ∆; f satisfies (SP) under ∆ if AS(f(ϕ, V ) ∧ ψ) = AS(ϕ ∧ ψ)‖V for every (ϕ, V ) ∈ ∆ and every formula ψ with IRAS(ψ, V ).

Note that when we say a forgetting operator f satisfies a desirable property, we mean that f satisfies the property under ∆∗ = {(ϕ, V ) | ϕ is a formula of LA, and V ⊆ A}.

By Proposition 3, there is no forgetting operator in ASP that can satisfy all the desirable properties under ∆∗ . For this reason, we are interested in identifying the largest subset ∆ of ∆∗ such that there is a forgetting operator f in ASP satisfying all the desirable properties under ∆. We will show that this forgetting operator f is the knowledge forgetting one in ASP.

The knowledge forgetting

Let X, X′ , V be sets of atoms and ϕ a formula. We define X ∼V X′ if X \ V = X′ \ V . Given two HT-interpretations 〈X, Y 〉 and 〈X′ , Y ′ 〉, we define that 〈X, Y 〉 ∼V 〈X′ , Y ′ 〉 if X ∼V X′ and Y ∼V Y ′ .

Definition 2 (Knowledge forgetting) A formula ψ is a result of HT-forgetting V ⊆ A in a formula ϕ if, 〈X′ , Y ′ 〉 |=HT ψ whenever 〈X′ , Y ′ 〉 ∼V 〈X, Y 〉 for some 〈X, Y 〉 |=HT ϕ.

The result of HT-forgetting always exists and is unique up to the strong equivalence in ASP. Let us denote it by Forget HT (ϕ, V ). Namely, Forget HT is the knowledge forgetting operator in ASP. It has been shown in [Wang et al., 2012] that the Forget HT operator can be characterized precisely in terms of the properties (W), (PP), (NP) and (IR).

Proposition 4 (Theorem 3 in [Wang et al., 2012]) Let ϕ be a formula, V ⊆ A, and f a forgetting operator. Then f(ϕ, V ) ≡sAS Forget HT (ϕ, V ) iff f satisfies the properties (W), (PP), (NP), and (IR).

It can be shown that Forget HT also satisfies (E) and (SE). They are actually implied by (W), (PP), (NP), and (IR). We therefore have the following proposition.

Proposition 5 Let ∆ be a set of pairs (ϕ, V ) where ϕ is a formula and V ⊆ A. The following statements (i) and (ii) are equivalent to each other.

• (i) There exists a forgetting operator f in ASP satisfying all eight properties under ∆.
• (ii) AS(ϕ ∧ φ)‖V = AS(Forget HT (ϕ, V ) ∧ φ) for every (ϕ, V ) ∈ ∆ and every formula φ with IRAS(φ, V ), i.e., Forget HT satisfies the property (SP) under ∆.

From the above proposition, given a set ∆ ⊆ ∆∗ , the problem of deciding whether there exists a forgetting operator that satisfies all desirable properties under ∆ is equivalent to the problem of deciding whether Forget HT satisfies (SP) under ∆.

A Sufficient and Necessary Condition

As mentioned earlier, there is no forgetting operator in ASP that satisfies all the eight desirable properties under ∆∗ . In this section, we identify a sufficient and necessary condition under which the HT-forgetting satisfies the property (SP).

HT-forgetting an atom

In the following, we write a single set {α} as α when it is clear from its context, for convenience. For example, we write Forget HT (ϕ, p) for Forget HT (ϕ, {p}), IRAS(ϕ, p) for IRAS(ϕ, {p}), S‖p for S‖{p}, and so on.

Proposition 6 Let ϕ be a formula and p ∈ A. It holds that AS(ϕ ∧ ψ)‖p ⊆ AS(Forget HT (ϕ, p) ∧ ψ) for every formula ψ with IRAS(ψ, p), iff, for any HT-model 〈X, Y 〉 of ϕ with X ⊂ Y , the following conditions hold:

• (i) 〈Y \{p}, Y \{p}〉 |=HT ϕ implies 〈X\{p}, Y \{p}〉 |=HT ϕ, and
• (ii) 〈Y ∪{p}, Y ∪{p}〉 |=HT ϕ implies 〈Y, Y ∪{p}〉 |=HT ϕ or 〈X, Y ∪ {p}〉 |=HT ϕ.

Proof sketch: (⇐) This is easy to verify.

(⇒) If (i) or (ii) is not satisfied then we can construct the following formula

One can verify that AS(ϕ∧ψ′ )‖p ̸⊆ AS(Forget HT (ϕ, p)∧ψ′ ).

The intuition behind (i) and (ii) in the above proposition is as follows. If an HT-interpretation 〈X, Y 〉 |=HT ϕ then 〈X \ {p}, Y \ {p}〉 |=HT Forget HT (ϕ, p). Once X \ {p} ⊂ Y \ {p}, then there exists some formula ψ with IRAS(ψ, p) such that Y \ {p} is not an answer set of Forget HT (ϕ, p) ∧ ψ. Thus, the conditions are to ensure that neither Y ∪ {p} nor Y \ {p} is an answer set of ϕ ∧ ψ.

Proposition 7 Let ϕ be a formula and p ∈ A. It holds that AS(Forget HT (ϕ, p) ∧ ψ) ⊆ AS(ϕ ∧ ψ)‖p for every formula ψ with IRAS(ψ, p), iff, for every Y ⊆ A,

Proof sketch: (⇐) Easy to show.

• (⇒) If the condition (i) is not satisfied then we can construct the following formula

One can verify that Y \ {p} ∈ AS(Forget HT (ϕ, p) ∧ ψ′ ) and neither Y \ {p} nor Y ∪ {p} is an answer set of ϕ ∧ ψ′ .

Intuitively, the condition (i) in Proposition 7 is to avoid the case that Y \ {p} is an answer set of Forget HT (ϕ, p) ∧ ψ. If 〈Y \ {p}, Y 〉 |=HT ϕ∧ψ and 〈Y \ {p}, Y \ {p}〉 ̸|=HT ϕ∧ψ then neither Y \ {p} nor Y ∪ {p} is an answer set of ϕ ∧ ψ.

From Propositions 6 and 7, when forgetting just one atom, we could identify a necessary and sufficient condition under which the HT-forgetting satisfies all of the desirable properties as indicated by the next theorem.

Theorem 3 Let ϕ be a formula and p ∈ A. The following statements (i) and (ii) are equivalent to each other.

• (i) AS(Forget HT (ϕ, p) ∧ ψ) = AS(ϕ ∧ ψ)‖p for every formula ψ with IRAS(ψ, p).
• (ii) for any HT-model 〈X, Y 〉 of ϕ with X ⊂ Y ,
• (a) 〈Y \ {p}, Y \ {p}〉 |=HT ϕ implies
• 〈X \ {p}, Y \ {p}〉 |=HT ϕ, and (b) 〈Y ∪ {p}, Y ∪ {p}〉 |=HT ϕ implies 〈Y, Y ∪ {p}〉 |=HT ϕ or 〈X, Y ∪ {p}〉 |=HT ϕ, (c) 〈Y \ {p}, Y 〉 |=HT ϕ implies 〈Y \ {p}, Y \ {p}〉 |=HT ϕ.

The following theorem shows that it is intractable to check whether the property (SP) holds for HT-forgetting when just one atom is forgotten.

Theorem 4 Let ϕ be a formula and p ∈ A. Each of the following decision problems is co-NP-complete.

• (i) Deciding whether AS(ϕ ∧ ψ)‖p ⊆ AS(Forget HT (ϕ, p) ∧ ψ) for every formula ψ with IRAS(ψ, p).
• (ii) Deciding whether AS(Forget HT (ϕ, p) ∧ ψ) ⊆ AS(ϕ ∧ ψ)‖p for every formula ψ with IRAS(ψ, p).
• (iii) Deciding whether AS(ϕ ∧ ψ)‖p = AS(Forget HT (ϕ, p) ∧ ψ) for every formula ψ with IRAS(ψ, p).

Proof sketch: The memberships are easy. For hardness, let φ be a formula, p ∈ A but not occurring in φ, and ϕ1 = (¬φ∨¬¬p∨q)∧((¬q ⊃ ¬φ)∨¬¬p), ϕ2 = ¬φ∨¬¬p, and ϕ3 = ϕ1 ∧ ϕ2. We can show that, for every formula ψ with IRAS(ψ, p), φ is unsatisfiable iff AS(ϕ1 ∧ ψ)‖p ⊆ AS(Forget HT (ϕ1, p) ∧ ψ) iff AS(Forget HT (ϕ2, p) ∧ ψ) ⊆ AS(ϕ2 ∧ψ)‖p iff AS(ϕ3 ∧ψ)‖p = AS(Forget HT (ϕ3, p) ∧ψ).

HT-forgetting a set of atoms

We are now in the position to identify a sufficient and necessary condition under which the HT-forgetting satisfies the property (SP) in general.

Proposition 8 Let ϕ be a formula and V ⊆ A. It holds that, for every formula ψ with IRAS(ψ, V ), AS(ϕ ∧ ψ)‖V ⊆ AS(Forget HT (ϕ, V ) ∧ ψ), iff, for each HT-model 〈X, Y 〉 of ϕ with X \ V ⊂ Y \ V , if there exists a set Y ′ with Y \ V ⊆ Y ′ ⊆ Y ∪ V and 〈Y ′ , Y ′ 〉 |=HT ϕ, then

• (i) there exists a set Y ′′ with Y \ V ⊆ Y ′′ ⊂ Y ′ such that 〈Y ′′ , Y ′ 〉 |=HT ϕ, or
• (ii) there exists a set X′ withX′ ⊆ Y ′ andX′ \V =X\V such that 〈X′ , Y ′ 〉 |=HT ϕ.

Proof sketch: (⇐) Easy.

(⇒) If both conditions (i) and (ii) are not satisfied then we can construct the formula

One can verify that AS(ϕ∧ψ′ )‖V ̸⊆ AS(Forget HT (ϕ,V )∧ψ′ ).

Intuitively, if 〈Y ′ , Y ′ 〉 |=HT ϕ then either (i) or (ii) in the above proposition should be satisfied, which ensures that Y ′ cannot be an answer set of ϕ ∧ ψ for some formula ψ with IRAS(ψ, V ).

Proposition 9 Let ϕ be a formula and V ⊆ A. It holds that, for every formula ψ with IRAS(ψ, V ), AS(Forget HT (ϕ, V ) ∧ ψ) ⊆ AS(ϕ ∧ ψ)‖V , iff, for each Y ⊆ A, if there exists a set Y ′ with Y \ V ⊆ Y ′ ⊂ Y and 〈Y ′ , Y 〉 |=HT ϕ, then

• (i) there exists a set Y ′′ with Y \ V ⊆ Y ′′ ⊆ Y ∪ V such that 〈Y ′′ , Y ′′ 〉 |=HT ϕ and there does not exist a set Y ′′′ with Y \ V ⊆ Y ′′′ ⊂ Y ′′ and 〈Y ′′′ , Y ′′ 〉 |=HT ϕ.

Proof sketch: (⇐) Easy.

• (⇒) If the condition (i) is not satisfied then we can construct the formula

It is not difficult to verify that Y \ V ∈ AS(Forget HT (ϕ, V ) ∧ ψ′ ) and there does not exist a set Y ′ with Y ′ ∼V Y such that Y ′ ∈ AS(ϕ ∧ ψ′ ).

Intuitively, the condition (i) in Proposition 9 is to avoid the case that Y \ V is an answer set of Forget HT (ϕ, V ) ∧ψ while there does not exist a set Y ′ with Y ′ ∼V Y and Y ′ is an answer set of ϕ∧ψ.

The next theorem follows from Propositions 8 and 9.

Theorem 5 (Main theorem) Let ϕ be a formula and V ⊆ A. The statements (i) and (ii) are equivalent to each other.

• (i) AS(Forget HT (ϕ, V ) ∧ψ) = AS(ϕ∧ψ)‖V for every formula ψ with IRAS(ψ, V ).
• (ii) The following conditions (a) and (b) hold:
• (a) for each HT-model 〈X, Y 〉 of ϕ with X \ V ⊂ Y \ V , if there exists a set Y ′ with Y \V ⊆ Y ′ ⊆ Y ∪V and 〈Y ′ , Y ′ 〉 |=HT ϕ, then
• there exists a set Y ′′ with Y \ V ⊆ Y ′′ ⊂ Y ′ such that 〈Y ′′ , Y ′ 〉 |=HT ϕ, or
• there exists a set X′ withX′ ⊆ Y ′ andX′ \V = X \ V such that 〈X′ , Y ′ 〉 |=HT ϕ;
• (b) for each Y ⊆ A, if there exists a set Y ′ with Y \ V ⊆ Y ′ ⊂ Y and 〈Y ′ , Y 〉 |=HT ϕ, then
• there exists a set Y ′′ with Y \V ⊆ Y ′′ ⊆ Y ∪V such that 〈Y ′′ , Y ′′ 〉 |=HT ϕ and there does not exist a set Y ′′′ with Y \ V ⊆ Y ′′′ ⊂ Y ′′ and 〈Y ′′′ , Y ′′ 〉 |=HT ϕ.

From Proposition 5, the condition (ii) in Theorem 5 specifies the largest set ∆ of (ϕ, V ) such that there exists a forgetting operator in ASP satisfying all eight properties under ∆. In the following, we use ∆◦ to denote the largest set.

The next example shows a possibility of (ϕ, V ) /∈ ∆◦ even if V contains all atoms occurring in the formula ϕ.

Example 1 Let A = {p, q}, ϕ = ¬p ⊃ p, V = {p} and ψ = q. One can check that ϕ ∧ ψ has no answer set and Forget HT (ϕ, V ) = ⊤. Thus, Forget HT (ϕ, V ) ∧ ψ has a unique answer set {q}. It follows that AS(ϕ ∧ ψ)‖V ̸= AS(Forget HT (ϕ, V ) ∧ ψ).

Actually, one can further verify that 〈{p}, {p, q}〉 |=HT ϕ and 〈{q}, {p, q}〉 |=HT ϕ, but 〈{q}, {q}〉 ̸|=HT ϕ, i.e., the condition (c) in Theorem 3 does not hold.

Proposition 10 Let ∆ be a set of pairs (ϕ, V ) where ϕ is a formula and V ⊆ A. The statements (i) and (ii) are equivalent to each other.

• (i) There exists a forgetting operator f in ASP satisfying all either properties under ∆.
• (ii) For each pair (ϕ, V ) ∈ ∆, ϕ and V satisfy the condition (ii) in Theorem 5.

The following theorem indicates that it is difficult to check whether Forget HT satisfies (SP) in general.

Theorem 6 Let ϕ be a formula and V ⊆ A. Each of the following decision problems is ΠP 2 -complete.

• (i) Deciding whether AS(ϕ∧ψ)‖V ⊆ AS(Forget HT (ϕ, V )∧ ψ) for every formula ψ with IRAS(ψ, V ).
• (ii) Deciding whether AS(Forget HT (ϕ, V ) ∧ ψ) ⊆ AS(ϕ ∧ ψ)‖V for every formula ψ with IRAS(ψ, V ).
• (iii) Deciding whether AS(ϕ∧ψ)‖V = AS(Forget HT (ϕ, V )∧ ψ) for every formula ψ with IRAS(ψ, V ).

Proof sketch: The memberships are easy. The hardness follows from the following fact: Given two formulas ψ′ and ϕ′ , the problem of deciding whether ψ′ |=HT Forget HT (ϕ′ , V ) is ΠP 2 -complete (cf. Theorem 14 in [Wang et al., 2014]).

Though it is in general difficult to verify if (ϕ, V ) ∈ ∆◦ for a formula ϕ and V ⊆ A, there exist some trivial syntactic conditions as shown in the next proposition.

Proposition 11 Let ϕ be a formula and V ⊆ A. If ϕ = ∧(A∪¬B) then (ϕ, V ) ∈ ∆◦ , where A, B are sets of atoms.

Proof sketch: Let A′ = A \ V and B′ = B′ \ V and ψ a formula with IRAS(ψ, V ). Note that Forget HT (ϕ, V ) ≡HT ∧(A′ ∪ ¬B′ ). We can show that AS(∧(A ∪ ¬B) ∧ ψ) = AS(∧(A ∪ ¬B) ∧ (ψ|A→⊤)|B→⊥) = AS(∧(A ∪ ¬B) ∧ (ψ|A′→⊤)|B′→⊥) due to IRAS(ψ, V ). Please see the next section for the definition of ψ|V→⋆ for ⋆ ∈ {⊤, ⊥}.

As mentioned in Introduction, knowledge forgetting based on the operator Forget HT is defined semanticaly and no syntactic characterizations are known. As it is ΠP 2 -complete to check whether ψ ≡HT Forget HT (ϕ, V ) holds for two given formulas ϕ and ψ and a set V ⊆ A [Wang et al., 2014], it is intractable to compute the results of knowledge forgetting. In the next section, we present a syntactic approach for knowledge forgetting. Similar to the syntactic definition of forgetting in classical propositional logic, it may inevitably result in exponential explosion.

A Syntactic Approach

In this section, we provide a syntactic characterization of HT-forgetting and a corresponding algorithm for computing knowledge forgetting, for formulas in normal form.

First, we introduce some notations. Let ϕ be a formula and p ∈ A. By ϕ|p→⋆ we mean the formula obtained from ϕ by replacing every occurrence of the atom p by ⋆, where ⋆ ∈ {⊤,⊥}. Let V = {p1, . . . , pn} ⊆ A. By ϕ|V→⋆ we denote the formula (· · · (ϕ|p1→⋆) · · · )|pn→⋆. Please note that the forgetting in propositional logic can be syntactically defined as Forget(ϕ, p) = ϕ|p→⊤ ∨ ϕ|p→⊥ and Forget(ϕ, V ∪ {p}) = Forget(Forget(ϕ, p), V ) [Lang et al., 2003].

Definition 3 Let ϕ be a formula in normal form and X ⊆ A. The semi-reduct of ϕ w.r.t. X, written ϕX, is the formula obtained from ϕ by replacing every occurrence of an atom p ∈ X in the range of ¬ with ⊤.

Please note that, ϕX is slightly different from the GLreduction [Lifschitz et al., 1999] in that the GL-reduction also handles the negative occurrence of the atoms not in X.

Example 2 Consider the formula ϕ:

Let X = {p}. Then ϕX is the formula:

which is strongly equivalent to

It has a unique answer set {p, r}. One should note here that the GL-reduct of ϕ w.r.t.X is ϕX = p∧r whose unique answer set is {p, r}. It is not difficult to verify that ϕX |=HT ϕX, but not vice versa.

The next theorem identifies an alternative sufficient and necessary condition under which Forget HT satisfies (SP) when forgetting one atom.

Theorem 7 Let ϕ be a formula in normal form and p an atom. Then, AS(Forget HT (ϕ, p)∧ψ) = AS(ϕ∧ψ)‖p for every formula ψ with IRAS(ψ, p), iff the following conditions hold:

Proof sketch: It is not difficult to verify that the condition (a) (resp. (b) and (c)) in the theorem is equivalent to the condition (a) (resp. (b) and (c)) in Theorem 3.

Proposition 12 Let ϕ be a formula in normal form, p ∈ A, and 〈X, Y 〉 an HT-interpretation with p /∈ Y . The following hold:

Proof sketch: (i) and (ii) follows from the definition of HTsatisfiability. (iii) follows from the following properties

• 〈X, Y 〉 |=HT ¬¬ϕ|p→⊤ iff Y ∪ {p} |= ϕ;
• 〈X, Y ∪ {p}〉 |=HT ϕ implies 〈X, Y 〉 |=HT ϕ{p}|p→⊥ ∨ ϕ{p}|p→⊤;
• 〈X, Y 〉 |=HT ϕ{p}|p→⊥ ∨ ϕ{p}|p→⊤ and Y ∪ {p} |= ϕ implies 〈X, Y ∪{p}〉 |=HT ϕ or 〈X∪{p}, Y ∪{p}〉 |=HT ϕ.

Algorithm 1: HT-forgetting

input : A formula ϕ and V ⊆ A output: A result of HT-forgetting V in ϕ

ϕ′ ← the normal form of ϕ;

return ϕ′ ;

Theorem 8 Let ϕ be a formula in normal form and p ∈ A. It holds that

Proof sketch: Let 〈X, Y 〉 be an HT-interpretation with p /∈ Y . Then 〈X, Y 〉 |=HT Forget HT (ϕ, p) iff 〈X, Y 〉 |=HT ϕ, 〈X, Y ∪ {p}〉 |=HT ϕ, or 〈X ∪ {p}, Y ∪ {p}〉 |=HT ϕ. Thus the claim follows from Proposition 12.

Recall that, for any formula ϕ, atom p, and V ⊆ A, Forget HT (ϕ, V ∪ {p}) ≡sAS Forget HT (Forget HT (ϕ, p), V ) (cf. Corollary 7 of [Wang et al., 2014]). Moreover, every formula ϕ can be translated to a formula ψ in normal form such that ϕ ≡sAS ψ. Therefore the above theorem implies a syntactic approach to computing the result of HT-forgetting for a formula ϕ and V ⊆ A. The details are given in Algorithm 1.

Corollary 9 Algorithm 1 outputs Forget HT (ϕ, V ).

Let NF(ϕ) be a formula in normal form strongly equivalent to the formula ϕ. The syntactic knowledge forgetting is formally defined below.

Definition 4 (Syntactic knowledge forgetting) Let ϕ be a formula. We define:

• Forget HT (ϕ, p) = NF(ϕ)|p→⊤ ∨ NF(ϕ)|p→⊥∨ ((NF(ϕ){p}|p→⊥ ∨ NF(ϕ){p}|p→⊤) ∧ ¬¬NF(ϕ)|p→⊤),
• Forget HT (ϕ, {p} ∪ V ) = Forget HT (Forget HT (ϕ, p), V ) where p ∈ A and V ⊆ A.

Example 3 (Continued from Example 2) Note that,

Then, Forget HT (ϕ, p) is strongly equivalent to ¬q ⊃ r. Its unique answer set is {r}.

Concluding Remarks

Lately, the literature on forgetting has shown extensive interest in the desirable properties of forgetting operators in ASP.

In this paper, we have identified a precise condition for a formula ϕ and V ⊆ A under which Forget HT (ϕ, V ) satisfies the property (SP). This leads to the largest set ∆◦ of pairs (ϕ, V ) where ϕ ∈ LA and V ⊆ A such that Forget HT enjoys all the eight properties under ∆◦ . This condition provides a guideline to explore subclasses of logic programs for which the HT-forgetting enjoys all of the desirable properties. Though a trivial subclass of logic programs occurring in ∆◦ is identified, cf. Proposition 11, it is still worthy to identify more interesting subclasses of logic programs for which the HTforgetting enjoys (SP). It is also interesting to investigate the property (SP) for forgetting in other nonmonotonic logical systems, such as in circumscription [Wang et al., 2015].

Secondly, we have proposed a syntactic approach to computing HT-forgetting results. Using this approach to compute the result of HT-forgetting a set V ⊆ A from a formula ϕ, one needs to compute the normal form of ϕ. This can be time consuming as an exponential explosion in the worst case is inevitable. To extend the syntactic approach for arbitrary formulas is a challenging future task.

Acknowledgement

We thank reviewers for their helpful comments. We are grateful to Fangzhen Lin for many helpful and informative discussions. We would also like to thank Xiaoping Chen and his research group for their useful discussions. Jianmin Ji's research was partially supported by the National Natural Science Foundation of China under grand 61175057, the National Natural Science Foundation for the Youth of China under grand 61403359, as well as the USTC Key Direction Project and the USTC 985 Project. Yisong Wang was partially supported by the National Natural Science Foundation of China under grand 61370161, the Stadholder Foundation of Guizhou Province under grant (2012)62 and the Natural Science Foundation of Guizhou Province under grant [2014]7640.