On Some Properties of Forgetting in ASP Ricardo Gonçalves and Matthias Knorr and João Leite1 Abstract. Many approaches for forgetting in Answer Set Program- the so-called existence, which requires that the result of forgetting ming (ASP) have been proposed in recent years, in the form of spe- belongs to the same class of programs admitted by the forgetting op- cific operators, or classes of operators, following different principles erator, so that the same reasoners can be used and the operator be and obeying different properties. Whereas each approach was devel- iterated, among many others. oped to somehow address some particular view on forgetting, thus The result is a complex landscape filled with operators and prop- aimed at obeying a specific set of properties deemed adequate for erties, of difficult navigation. This problem was tackled in [17] by such view, only a recently published comprehensive overview of ex- presenting a systematic study of forgetting in ASP, thoroughly inves- isting operators and properties provided a uniform and complete pic- tigating the different approaches found in the literature, their proper- ture, including many novel (even surprising) results on relations be- ties and relationships, giving rise to a comprehensive guide aimed at tween properties and operators. Yet, this overview ignored to a large helping users navigate this topic’s complex landscape and ultimately extent a different set properties for forgetting in ASP, and in this pa- assist them in choosing suitable operators for each application. per we close this gap. It turns out that, while some of these properties However, [17] ignores to a large extent the postulates on forgetting are closely related to the properties previously studied, four of them in ASP introduced by Wong in [53].2 In this paper, we close this gap are distinct providing novel results and insights further strengthening by thoroughly investigating them, their relationships with other prop- established relations between existing operators. erties and existing operators, concluding that, while some of them are straightforwardly implied by one of the previously studied proper- ties, hence ultimately weaker than these and thus of less importance, 1 Introduction others turn out to be distinct and provide additional novel results fur- Forgetting – or variable elimination – is an operation that allows ther strengthening the relations between properties and classes of op- the removal, from a knowledge base, of middle variables no longer erators as established previously. deemed relevant, whose importance is witnessed by its application to Besides space considerations, the main reason why these postu- cognitive robotics [35, 36, 39], resolving conflicts [26, 54, 11, 27], lates were left out of [17] was the fact that, thus far, they had not and ontology abstraction and comparison [50, 25, 23, 24]. With its played a significant role in the literature on forgetting. Whereas com- early roots in Boolean Algebra [32], it has been extensively studied pleting the picture presented in [17] would be sufficient reason to within classical logic [3, 26, 28, 29, 37, 38, 51]. thoroughly investigate these postulates, recent findings in [18] made Only more recently, the operation of forgetting began to receive it even more relevant. It was shown in [18] that it is not always possi- attention in the context of logic programming and non-monotonic ble to forget while preserving so-called strong persistence – an essen- reasoning, notably of Answer Set Programming (ASP). It turns out tial property for forgetting in ASP that encodes the required preserva- that the rule-based nature and non-monotonic semantics of ASP tion, under forgetting, of all relations between non-forgotten atoms – create very unique challenges to the development of forgetting op- shifting the attention to the question of when (and how) it is possible erators, – just as it happened with the development of other be- to forget, which is to some extent related to some of Wong’s pos- lief change operators such as those for revision and update, cf. tulates. In particular, investigating Wong’s postulates led us to prove [31, 2, 10, 30, 40, 41, 42, 8, 43, 44] – making it a special endeavour that it may be impossible to step-wise iteratively forget a set of atoms with unique characteristics distinct from those for classical logic. that can be forgotten as a whole, while preserving strong persistence. Over the years, many have proposed different approaches to for- To make the presentation self-contained, we first adapt part of getting in ASP, through the characterization of the result of forget- the material presented in [17]. Namely, we present general nota- ting a set of atoms from a given program up to some equivalence tion on HT-models, logic programs, answer sets, and on forgetting in class, and/or through the definition of concrete operators that pro- ASP, recall existing properties of forgetting, as discussed in [17], the duce a program given an input program and atoms to be forgotten classes of operators existing in the literature, and results on relations [54, 11, 53, 48, 47, 21, 49, 9]. of properties and classes of operators. Subsequently, we introduce All these approaches were typically proposed to obey some spe- the postulates from [53] and present our results on relations w.r.t. cific set of properties deemed adequate by their authors, some previously established properties and on which classes of operators adapted from the literature on classical forgetting [55, 48, 49], oth- satisfy which postulates. We then investigate possible generalisations ers specifically introduced for the case of ASP [11, 53, 48, 47, 21, 9]. of Wong’s postulates, and the novel impossibility result concerning Examples of properties include strengthened consequence, which re- step-wise iterative forgetting, before concluding. quires that the answer sets of the result of forgetting be bound to the answer sets of the original program modulo the forgotten atoms, or 2 We use the term postulate to follow [53] and easily distinguish them from 1 NOVA LINCS, Departamento de Informática, Faculdade de Ciências e Tec- the properties discussed in [17]. However, their role is the same as the role nologia, Universidade Nova de Lisboa, email: {rjrg|mkn|jleite}@fct.unl.pt. of other properties. 2 Preliminaries This class of logic programs, Ce , includes a number of special kinds of rules r: if n = 0, then we call r disjunctive; if, in addi- We assume a propositional language LA over a signature A, a fi- tion, k ≤ 1, then r is normal; if on top of that m = 0, then we call nite set of propositional atoms. The formulas of LA are inductively r Horn, and fact if also l = 0. The classes of disjunctive, normal defined using connectives ⊥, ∧, ∨, and ⊃: and Horn programs, Cd , Cn , and CH , are defined resp. as a finite set of disjunctive, normal, and Horn rules. We also call extended rules ϕ ::= ⊥ | p | ϕ ∨ ϕ | ϕ ∧ ϕ | ϕ ⊃ ϕ (1) with k ≤ 1 non-disjunctive, thus admitting a non-standard class Cnd , where p ∈ A. In addition, ¬ϕ and > are resp. W shortcutsVfor ϕ ⊃ ⊥ called non-disjunctive programs, different from normal programs. and ⊥ ⊃ ⊥. Given a finite set S of formulas, S and S denote We have CH ⊂ Cn ⊂ Cd ⊂ Ce and also Cn ⊂ Cnd ⊂ Ce . resp.Wthe disjunction V and conjunction of all formulas in S. In particu- We now recall the answer set semantics [14] for logic programs. lar, ∅ and ∅ stand for resp. ⊥ and >, and ¬S and ¬¬S represent Given a program P and a set I of atoms, the reduct P I is P I = resp. {¬ϕ | ϕ ∈ S} and {¬¬ϕ | ϕ ∈ S}. We assume that the under- {A ← B : r of the form (3) in P, C ∩ I = ∅, D ⊆ I}. A set I 0 of lying signature for a particular formula ϕ is A(ϕ), the set of atoms atoms is a model of P I if, for each r ∈ P I , I 0 |= B implies I 0 |= A. appearing in ϕ. I is minimal in a set S, denoted by I ∈ MIN (S), if there is no I 0 ∈ S s.t. I 0 ⊂ I. I is an answer set of P iff I is a minimal model HT-models Regarding the semantics of propositional formulas, of P I . Note that, for Cnd and its subclasses, this minimal model is we consider the monotonic logic here-and-there (HT) and equilib- in fact unique. The set of all answer sets of P is denoted by AS(P ). rium models [33]. An HT -interpretation is a pair hH, T i s.t. H ⊆ Note that, for Cd and its subclasses, all I ∈ AS(P ) are pairwise T ⊆ A. The satisfiability relation in HT, denoted |=HT , is recursively incomparable. If P has an answer set, then P is consistent. The V - defined as follows for p ∈ A and formulas ϕ and ψ: exclusion of a set of answer sets M, denoted MkV , is {X \V | X ∈ M}. Two programs P1 , P2 are equivalent if AS(P1 ) = AS(P2 ) • hH, T i |=HT p if p ∈ H; and strongly equivalent if P1 ≡HT P2 . It is well-known that answer • hH, T i 6|=HT ⊥; sets and equilibrium models coincide [33]. • hH, T i |=HT ϕ ∧ ψ if hH, T i |=HT ϕ and hH, T i |=HT ψ; We also recall notions on forgetting from [17]. Given a class of • hH, T i |=HT ϕ ∨ ψ if hH, T i |=HT ϕ or hH, T i |=HT ψ; logic programs C over A, a forgetting operator is a partial function • hH, T i |=HT ϕ ⊃ ψ if both (i) T |= ϕ ⊃ ψ,3 and (ii) f : C × 2A → C s.t. f(P, V ) is a program over A(P ) \ V , for each hH, T i |=HT ϕ implies hH, T i |=HT ψ. P ∈ C and V ∈ 2A . We call f(P, V ) the result of forgetting about V from P . Furthermore, f is called closed for C 0 ⊆ C if, for every An HT -interpretation is an HT -model of a formula ϕ if P ∈ C 0 and V ∈ 2A , we have f(P, V ) ∈ C 0 . A class F of forgetting hH, T i |=HT ϕ. We denote by HT (ϕ) the set of all HT-models of operators is a set of forgetting operators. ϕ. In particular, hT, T i ∈ HT (ϕ) is an equilibrium model of ϕ if there is no T 0 ⊂ T s.t. hT 0 , T i ∈ HT (ϕ). Given two formulas ϕ and ψ, if HT (ϕ) ⊆ HT (ψ), then ϕ entails 3 Forgetting ψ in HT, written ϕ |=HT ψ. Also, ϕ and ψ are HT-equivalent, written The principal idea of forgetting in logic programming is to remove ϕ ≡HT ψ, if HT (ϕ) = HT (ψ). or hide certain atoms from a given program, while preserving its se- For sets of atoms X, Y and V ⊆ A, Y ∼V X denotes that Y \ mantics for the remaining atoms. [17]. V = X \V . For HT -interpretations hH, T i and hX, Y i, hH, T i ∼V hX, Y i denotes that H ∼V X and T ∼V Y . For a set M of HT - Example 1 Consider the following program P = {d ← not c; a ← interpretations, M†V denotes the set {hX, Y i | hH, T i ∈ M and e; e ← b; b ←}. The result of forgetting about atom e from P should hX, Y i ∼V hH, T i}. be a program over the remaining atoms of P , i.e., it should not con- tain e. Intuitively, in the result, the fact b ← should persist since it Logic Programs An (extended) logic program P is a finite set of is independent of e. In addition, the link between a and b should be rules, i.e., formulas of the form preserved in some way, even if e is absent. Also, d should still follow ^ ^ ^ _ from the result of forgetting as the original rule d ← not c does not ¬¬D ∧ ¬C ∧ B⊃ A, (2) contain e. where all elements in A = {a1 , . . . , ak }, B = {b1 , . . . , bl }, C = {c1 , . . . , cm }, D = {d1 , . . . , dn } are atoms.4 Such rules r are also As the example indicates, preserving the semantics for the remain- commonly written as ing atoms is not necessarily tied to one unique program. Rather often, a representative up to some notion of equivalence between programs a1 ∨ . . . ∨ ak ← b1 , ..., bl , not c1 , ..., not cm , is considered. In this sense, many notions of forgetting for logic pro- not not d1 , ..., not not dn , (3) grams are defined semantically, i.e., they introduce a class of opera- tors that satisfy a certain semantic characterization. Each single oper- and we use both forms interchangeably. Given r, we distinguish its ator in such a class is then a concrete function that, given a program head, head (r) = A, and its body, body(r) = B ∪ ¬C ∪ ¬¬D, P and a set of atoms V to be forgotten, returns a unique program, the representing a disjunction and a conjunction. result of forgetting about V from P . As shown by Cabalar and Ferraris [6], any set of (propositional) formulas is HT-equivalent to an (extended) logic program which is Definition 1 Given a class of logic programs C over A, a forgetting why we can focus solely on these. operator is a partial function f : C × 2A → C s.t. f(P, V ) is a 3 |= is the standard consequence relation from classical logic. program over A(P ) \ V , for each P ∈ C and V ∈ 2A . We call 4 Extended logic programs [34] are actually more expressive, but this form is f(P, V ) the result of forgetting about V from P . Furthermore, f is sufficient here. called closed for C 0 ⊆ C if, for every P ∈ C 0 and V ∈ 2A , we have 2 f(P, V ) ∈ C 0 . A class F of forgetting operators is a set of forgetting 1. (CP) is incompatible with (W) as well as with (NP) (for F closed operators. for C, where C contains normal logic programs); [47] 2. (W) is equivalent to (NP); [20] Note that the requirement for being a partial function is a natural one 3. (SP) implies (PP); [20] given the existing notions in the literature, where some are not closed 4. (SP) implies (SE); [21] for certain classes of programs. 5. (W) and (PP) together imply (SE); [17] To remain as general and uniform as possible, we focus on classes 6. (CP) and (SI) together are equivalent to (SP); [17] of operators. Whenever a notion of forgetting in the literature is de- 7. (sC) and (wC) together are equivalent to (CP); [17] fined through a concrete forgetting operator only, we consider the 8. (CP) implies (wE); [17] class containing that single operator. 9. (SE) and (SI) together imply (PP). [17] 4 Properties of Forgetting 5 Operators of Forgetting Previous work on forgetting in ASP has introduced a variety of de- We now review existing approaches to operators of forgetting in ASP sirable properties which we recall next. Unless stated otherwise, F is following [17]. a class of forgetting operators, and C the class of programs over A of Strong and Weak Forgetting The first proposals are due to Zhang a given f ∈ F. and Foo [54] introducing two syntactic operators for normal logic programs, termed Strong and Weak Forgetting. Both start by comput- (sC) F satisfies strengthened Consequence if, for each f ∈ F, P ∈ C ing a reduction corresponding to the well-known weak partial evalu- and V ⊆ A, we have AS(f(P, V )) ⊆ AS(P )kV . ation (WGPPE) [4], defined as follows: for a normal logic program (wE) F satisfies weak Equivalence if, for each f ∈ F, P, P 0 ∈ C P and a ∈ A, R(P, a) is the set of all rules in P and all rules of the and V ⊆ A, we have AS(f(P, V )) = AS(f(P 0 , V )) whenever form head (r1 ) ← body(r1 ) \ {a} ∪ body(r2 ) for each r1 , r2 ∈ P AS(P ) = AS(P 0 ). s.t. a ∈ body(r1 ) and head (r2 ) = a. Then, the two operators dif- (SE) F satisfies Strong Equivalence if, for each f ∈ F, P, P 0 ∈ C fer on how they subsequently remove rules containing a, the atom to and V ⊆ A: if P ≡HT P 0 , then f(P, V ) ≡HT f(P 0 , V ). be forgotten. In Strong Forgetting, all rules containing a are simply (W) F satisfies Weakening if, for each f ∈ F, P ∈ C and V ⊆ A, removed: we have P |=HT f(P, V ). fstrong (P, a) = {r ∈ R(P, a) | a 6∈ A(r)} (PP) F satisfies Positive Persistence if, for each f ∈ F, P ∈ C and V ⊆ A: if P |=HT P 0 , with P 0 ∈ C and A(P 0 ) ⊆ A \ V , then In Weak Forgetting, rules containing not a in their bodies are kept, f(P, V ) |=HT P 0 . without the not a. (NP) F satisfies Negative Persistence if, for each f ∈ F, P ∈ C and fweak (P, a) = {head (r) ← body(r) \ {not a} | V ⊆ A: if P 6|=HT P 0 , with P 0 ∈ C and A(P 0 ) ⊆ A \ V , then f(P, V ) 6|=HT P 0 . r ∈ R(P, a), a 6∈ head (r) ∪ body(r)} (SI) F satisfies Strong (addition) Invariance if, for each f ∈ F, P ∈ The motivation for this difference is whether such not a is seen C and V ⊆ A, we have f(P, V ) ∪ R ≡HT f(P ∪ R, V ) for all as support for the rule head (Strong) or not (Weak). In both cases, programs R ∈ C with A(R) ⊆ A \ V . the actual operator for a set of atoms V is defined by the sequential (EC ) F satisfies Existence for C, i.e., F is closed for a class of pro- application of the respective operator to each a ∈ V . Both operators grams C if there exists f ∈ F s.t. f is closed for C. are closed for Cn . The corresponding singleton classes are defined as (CP) F satisfies Consequence Persistence if, for each f ∈ F, P ∈ C follows. and V ⊆ A, we have AS(f(P, V )) = AS(P )kV . (SP) F satisfies Strong Persistence if, for each f ∈ F, P ∈ C and Fstrong = {fstrong } Fweak = {fweak } V ⊆ A, we have AS(f(P, V ) ∪ R) = AS(P ∪ R)kV , for all Semantic Forgetting Eiter and Wang [11] proposed Semantic For- programs R ∈ C with A(R) ⊆ A \ V . getting to address some shortcomings of the two purely syntax-based (wC) F satisfies weakened Consequence if, for each f ∈ F, P ∈ C operators fstrong and fweak . Semantic Forgetting introduces the fol- and V ⊆ A, we have AS(P )kV ⊆ AS(f(P, V )). lowing class of operators for consistent disjunctive programs:6 Throughout the paper, whenever we write that a single operator f Fsem = {f | AS(f(P, V )) = MIN (AS(P )kV )} obeys some property, we mean that the singleton class composed of The basic idea is to characterize a result of forgetting just by its that operator, {f}, obeys such property. answer sets, obtained by considering only the minimal sets among Some notions of forgetting do only require that atoms to be for- the answer sets of P ignoring V . Three concrete algorithms are pre- gotten be irrelevant: sented, two based on semantic considerations and one syntactic. Un- like the former, the latter is not closed for classes7 Cd+ and Cn+ , since (IR) f(P, V ) ≡HT P 0 for some P 0 not containing any v ∈ V . double negation is required in general. However, this is not a restriction, as argued in [17], and, implicitly, Semantic Strong and Weak Forgetting Wong [53] argued that se- any F satisfies (IR). mantic forgetting should not focus on answer sets only, as they do The following proposition establishes all known relevant relations not contain all the information present in a program, and defined two between them. classes of forgetting operators for disjunctive programs, building on 6 Actually, classical negation can occur in scope of not , but due to the re- Proposition 1 The following relations hold for all F:5 striction to consistent programs, this difference is of no effect [14], so we ignore it here. 5 To ease the reading, here “(P)” stands for “F satisfies (P)”. 7 Here, + denotes the restriction to consistent programs. 3 HT-models.8 For program P and atom a, the set of consequences of system by Wong [52] that preserves strong equivalence. Given that P is Cn(P, a) = {r | r disjunctive, P |=HT r, A(r) ⊆ A(P )}. We `s is the consequence relation of this system, CnA (P ) is {r ∈ LA | obtain PS (P, a) and PW (P, a), the results of strongly and weakly r disjunctive, P `s r}. The class is defined by: forgetting atom a from P , as follows: FSE = {f | f(P, V ) ≡HT CnA (P ) ∩ LA(P )\V } 1. Obtain P1 by removing from Cn(P, a): (i) r with a ∈ body(r), An operator is provided, which is closed for Cd . (ii) a from the head of each r with not a ∈ body(r). To ease later comparisons, we also include in Fig. 1 the results on 2. Obtain PS (P, a) and PW (P, a) from P1 by replacing/removing satisfaction of properties for known classes of forgetting operators rules r as follows: obtained in [17]. r with not a in body r with a in head S (remove) (remove) 6 Wongs Properties of Forgetting W remove only not a remove only a With all concepts and notation in place regarding forgetting in ASP, The generalization to sets of atoms V , i.e., PS (P, V ) and PW (P, V ), the properties commonly considered, and the existing classes of for- can be obtained by simply sequentially forgetting each a ∈ V , yield- getting operators, we can now turn our attention to the postulates in- ing the following classes of operators. troduced by Wong [53]. These postulates were defined in a somewhat different way when compared to the properties presented in Sec. 4. FS = {f | f(P, V ) ≡HT PS (P, V )} Namely, they only considered forgetting a single atom, were defined FW = {f | f(P, V ) ≡HT PW (P, V )} for disjunctive programs (the maximal class of programs considered in [53]), and used a generic formulation which allowed different no- While both steps are syntactic, different strongly equivalent rep- tions of equivalence. Here, we only consider HT-equivalence, i.e., resentations of Cn(P, a) exist, thus providing different instances. strong equivalence, as, in the literature, this is clearly the more rel- Wong [53] defined one construction based on inference rules for HT- evant of the two notions considered in [53] (the other one being the consequence, closed for Cd . non-standard T-equivalence) and in line with previously presented HT-Forgetting Wang et al. [48, 49] introduced HT-Forgetting, build- material here and in [17]. ing on properties introduced by Zhang and Zhou [55] in the context We start by recalling these postulates9 adjusting them to our nota- of modal logics, with the aim of overcoming problems with Wongs tion and extending them to the most general class of extended logic notions, namely that each of them did not satisfy one of the proper- programs considered here, but maintaining, for now, the restriction ties (PP) and (W). HT-Forgetting is defined for extended programs to forgetting only single atoms. and uses representations of sets of HT-models directly. FHT = {f | HT (f(P, V )) = HT (P )†V } (F0) F satisfies (F0) if, for each f ∈ F, P, P 0 ∈ C and a ∈ A: if P ≡HT P 0 , then f(P, {a}) ≡HT f(P 0 , {a}). A concrete operator is presented [49] that is shown to be closed for (F1) F satisfies (F1) if, for each f ∈ F, P, P 0 ∈ C and a ∈ A: if Ce and CH , and it is also shown that no operator exists that is closed P |=HT P 0 , then f(P, {a}) |=HT f(P 0 , {a}). for either Cd or Cn . (F2) F satisfies (F2) if, for each f ∈ F, P, P 0 ∈ C and a ∈ A: if a SM-Forgetting Wang et al. [47] introduced SM-Forgetting for ex- does not appear in R, then f(P ∪ R, {a}) ≡HT f(P 0 , {a}) ∪ R tended programs, aiming at preserving the answer sets of the original for all R ∈ C. program (modulo forgotten atoms). (F2-) F satisfies (F2-) if, for each f ∈ F, P ∈ C, and a ∈ A: if FSM = {f | HT (f(P, V )) is a maximal subset of P |=HT r and a does not occur in r, then f(P, {a}) |=HT r for all HT (P )†V s.t. AS(f(P, V )) = AS(P )kV } rules r expressible in C. (F3) F satisfies (F3) if, for each f ∈ F, P ∈ C and a ∈ A: f(P, {a}) A concrete operator is provided that, like for FHT , is shown to be does not contain any atoms that are not in P . closed for Ce and CH . It is also shown that no operator exists that is (F4) F satisfies (F4) if, for each f ∈ F, P ∈ C and a ∈ A: closed for either Cd or Cn . if f(P, {a}) |=HT r, then f({r0 }, {a}) |=HT r for some r0 ∈ Strong AS-Forgetting Knorr and Alferes [21] introduced Strong CnA (P ). AS-Forgetting with the aim of preserving not only the answer sets (F5) F satisfies (F5) if, for each f ∈ F, P ∈ C and a ∈ A: if of P itself but also those of P ∪ R for any R over the signature with- f(P, {a}) |=HT A ← B ∪ ¬C ∪ ¬¬D, then P |=HT A ← out the atoms to be forgotten. The notion is defined abstractly for B ∪ ¬C ∪ {¬a} ∪ ¬¬D. classes of programs C. (F6) F satisfies (F6) if, for each f ∈ F, P ∈ C and a, b ∈ A: FSas = {f | AS(f(P, V ) ∪ R) = AS(P ∪ R)kV for all f(f(P, {b}), {a}) ≡HT f(f(P, {a}), {b}). programs R ∈ C with A(R) ⊆ A(P ) \ V } These postulates represent the following: Forgetting about atom a A concrete operator is defined for Cnd , but not closed for Cn and only from HT-equivalent programs preserves HT-equivalence (F0); if a defined for certain programs with double negation. program is an HT-consequence of another program, then forgetting SE-Forgetting Delgrande and Wang [9] recently introduced SE- about atom a from both programs preserves this HT-consequence Forgetting based on the idea that forgetting an atom from program (F1); when forgetting about an atom a, it does not matter whether we P is characterized by the set of those SE-consequences, i.e., HT- add a set of rules over the remaining language before or after forget- consequences, of P that do not mention atoms to be forgotten. The ting (F2); any consequence of the original program not mentioning notion is defined for disjunctive programs building on an inference atom a is also a consequence of the result of forgetting about a (F2-); 8 Without loss of generality, we consider HT-models instead of SE-models 9 As mentioned before, we use the term postulate to follow [53] and ease [46] as in [53]. readability. Technically, they are treated as every other property. 4 sC wE SE W PP NP SI CP SP wC ECH ECn ECd ECnd ECe Fstrong × × × X × X X × × × X X - - - Fweak × × × × X × X × × × X X - - - Fsem X X × × × × × × × × X X X - - FS × × X X X X × × × × X × X - - FW X X X × X × X × × × X X X - - FHT × × X X X X X × × × X × × × X FSM X X X × X × × X × X X × × × X FSas X X X × X × X X X X X × × × × FSE × × X X X X × × × × X × X - - Figure 1. Satisfaction of properties for known classes of forgetting operators. For class F and property P, ’X’ represents that F satisfies P, ’×’ that F does not satisfy P, and ’-’ that F is not defined for the class C in consideration. the result of forgetting about an atom from a program only contains Proposition 4 FS , FW , FHT and FSE satisfy (F1). Fstrong , Fweak , atoms occurring in the original program (F3); any rule which is a Fsem , FSM and FSas do not satisfy (F1). consequence of the result of forgetting about an atom from program P is a consequence of the result of forgetting about that atom from a The fact that FS and FW satisfy (F1) was proved in [53]. For FHT and single rule among the HT-consequences of P (F4); a rule obtained by FSE , this result follows from Prop. 2 and Fig. 1 and because FHT and extending with not a the body of a rule which is an HT-consequence FSE satisfy both (W) and (PP). of the result of forgetting about an atom a from program P is an For the negative results, Fstrong , Fweak and Fsem cannot satisfy HT-consequence of P (F5); and the order is not relevant when se- (F1), since they do not satisfy (F0). For FSM and FSas , consider the quentially forgetting two atoms (F6). following programs P = {a ← not p; p ← not a} and P 0 = {a ← Note that CnA (P ) for (F4) is defined over the class of programs not p}. Then, clearly P |=HT P 0 , but since f(P, p) ≡HT {a ← considered in each operator, and, likewise, that the kind of rules con- not not a} and f(P 0 , p) ≡HT {a ←}, for any f ∈ FSM ∪ FSas , we sidered in (F5) is restricted according to the class of programs con- have that f(P, p) 6|=HT f(P 0 , p). sidered in a given operator. Thus, (F1) is distinct per se, as it provides a unique set of classes The following proposition relates these postulates and the proper- of operators of forgetting for which it is satisfied. In particular, unlike ties in Sec. 4. the weaker property (F0) and the related (SE), FSM and FSas do not satisfy (F1), most likely because the premise in the condition for Proposition 2 The following relations hold for all F: satisfying (F1) is weaker than that of (F0). As argued in [53], it should not matter whether we add new rules 1. (F1) implies (F0); [53] before or after forgetting, as long as these rules do not refer to the 2. (F2) and (F1) imply (F2-); [53] forgotten atom(s). Similar to (F0), postulate (F2) is a special case of 3. (SE) implies (F0); one of the properties considered in Sec. 4. 4. (W) and (PP) together imply (F1); 5. (SI) implies (F2); Proposition 5 Fstrong , Fweak , FW , FHT and FSas satisfy (F2). FS , 6. (PP) implies (F2-); Fsem , FSM and FSE do not satisfy (F2). 7. (W) implies (F5). It was proved in [53] that FW satisfies (F2). The classes Fstrong , Postulates (F0), (F2), (F2-), and (F5) are implied by existing prop- Fweak , FHT and FSas do satisfy (F2), since they satisfy (SI) and by erties presented in [17], while (F1) is implied by a pair of these. We Prop. 2 and Fig. 1. Regarding the negative results, it was proved in discuss this in more detail next, while investigating which operators [53] that FS and Fsem do not satisfy (F2). For FSM and FSE , the from Sec. 5 satisfy which of the new postulates. counterexample given in [17] for (SI) also applies for (F2). Thus, all We start with (F0), which can readily be seen as a special case of results coincide with those of (SI). (SE), obtained by only considering forgetting one atom instead of a In [53], (F2-) was introduced as a weakening of (F2). Surprisingly, set. It shares with (SE) the intuition that forgetting the same atom(s) it turns out to be a special case of (PP) by definition of both these should preserve strong equivalence of programs. properties. Proposition 3 FS , FW , FHT , FSM , FSas and FSE satisfy (F0). Proposition 6 Fweak , FS , FW , FHT , FSM , FSas and FSE satisfy Fstrong , Fweak and Fsem do not satisfy (F0). (F2-). Fstrong and Fsem do not satisfy (F2-). The fact that classes FS , FW , FHT , FSM , FSas and FSE satisfy The positive results follow from Prop. 2 and Fig. 1. Regarding the (F0) follows from Prop. 2 and Fig. 1, since they all satisfy (SE). In two negative results, the counterexamples given in [49] for (PP) also [53], Fstrong and Fweak are shown to not satisfy (F0). For Fsem , the apply for (F2-). Thus, all results coincide with those of (PP). argument given in [11] to show that Fsem does not satisfy (SE) also In [53], two variations of (F2) are considered. One, (F2’), is dis- applies to (F0). Hence, even though (F0) is weaker than (SE), the carded right away as being insufficient to solve the incompatibility results for all considered classes of operators coincide with those for between FS and (F2). The other, (F2*) restricts the program R to a (SE) (see Fig.1). single rule, only for the sake of FS satisfying this restricted version As per (F1), forgetting the same atom(s) should preserve HT- of (F2). But in our view, permitting only the addition of single rules consequence between two programs. As argued in [53], this postulate is of little value, which is why we have omitted this variant from our can be seen as a strengthening of (F0). considerations. 5 Postulate (F3) encodes that forgetting is meant to simplify the lan- the same set of known operators. We conjecture that this is so be- guage of a program by removing unwanted atoms. This is reasonable, cause both are rather closely tied to the concrete definitions of FS otherwise, if atoms not occurring in a program were allowed in the and FW along which they were introduced. result of forgetting, a trivial solution for forgetting would be to sim- Finally, (F6) encodes the irrelevance of the order in which two ply rename the atoms to be forgotten using such extra atoms. atoms are forgotten. Proposition 7 All classes of operators Fstrong , Fweak , Fsem , FS , Proposition 10 Fstrong , Fweak , Fsem , FS , FW , FHT , FSM and FSE FW , FHT , FSM , FSas and FSE satisfy (F3). satisfy (F6). FSas does not satisfy (F6). Our definition of (classes of) forgetting operators ensures satisfac- The positive result for each operator was proved in the paper where tion of (F3). Hence, similar to (IR) (see Sec. 4), it can be omitted the operator was defined (cf. Sec. 5). The negative result for FSas from further considerations. follows from the fact that FSas satisfies (SP) which, as shown in The postulate (F4) states that every rule which is an HT- [18], implies that in certain cases it is not possible to forget certain consequence of the result of forgetting about atom a from P is an atoms. Take P = {p ← not not p; a ← p; b ← not p}. Forgetting HT-consequence of the result of forgetting about a from a single rule about b from P first is strongly equivalent to removing the third rule, which is itself an HT-consequence of P . and subsequently forgetting about p is strongly equivalent to {a ← not not a}. However, forgetting about p from P first while satisfying Proposition 8 Fstrong , Fweak , FS , FW , FHT , and FSE satisfy (F4). (SP) is simply not allowed. Hence, the order of forgetting matters for Fsem , FSM and FSas do not satisfy (F4). FSas . This postulate is succinct and there is no property considered in [17] which is satisfied by all classes but FSas . In fact, we will see The positive result for FS , FW and FSE was shown in [53]. in the next section that (F6) and its generalizations are of interest For FHT , this follows directly from the alternative definition of HT- for open questions related to the property (SP) recently investigated forgetting in [49]. For Fstrong and Fweak , the result follows from in detail in [18], where it was shown that forgetting is not always the fact that this postulate is already shown to hold for a stronger no- possible in a meaningful way, shifting the focus to investigating what tion of equivalence in [53], and since the additional derivation rules can be forgotten. distinguishing this notion of equivalence and HT-equivalence do not affect the result. 7 Conclusions The negative results for FSas and FSM can be shown with a coun- terexample based on program P = {a ← p; p ← not not p}. For We have studied eight postulates of forgetting in ASP introduced any operator in either class of forgetting operators, the result of for- in [53], to fill a gap in a recent comprehensive guide on properties getting about p from P is strongly equivalent to a ← not not a. and classes of operators for forgetting in ASP, and relations between However, neither this nor any other rule over {a}, which has this rule these [17]. as an HT-consequence, appears in CnA (P ). In the case of Fsem , It turns out that four of them are actually directly implied by previ- the negative result follows from the rather relaxed definition of the ously considered single properties and for three among these, the sets class and the fact that for satisfying (F4) any operator in Fsem has to of classes of forgetting operators which satisfy the stronger and the satisfy it: we can easily define an operator that is still in Fsem , but weaker properties precisely coincide. This suggests that these three, returns an arbitrary program – then (F4) clearly does not hold. (F0), (F2), and (F2-) can safely be ignored. Postulate (F3) can also Therefore, this postulate turns out to be of interest as no previously be safely ignored as it is always satisfied by definition of forgetting studied property is satisfied by precisely the same set of classes of operators. forgetting operators. Three of the remaining four properties, (F1), (F4), and (F5), are The intuition of (F5), according to [53], is that any rule which in fact distinct (even though (F5) is implied by an existing property), is an HT-consequence of the result of forgetting must be an HT- and no other already existing property is satisfied by precisely the consequence of the program itself in the situations where the atom same set of classes of forgetting operators in each of these cases. to be forgotten is not known. They are worth being considered for inclusion in the set of relevant properties as not only they would provide further distinguishing cri- Proposition 9 Fstrong , Fweak , FS , FW , FHT and FSE satisfy (F5). teria for existing classes of operators, as they would help further clar- Fsem , FSM and FSas do not satisfy (F5). ify the relation between properties (SE), (W), and (PP) considered before, and even provide additional means to axiomatically charac- The positive result for FS , FW and FSE was shown in [53]. A terieze many classes of forgetting operators. similar argument can be used for Fweak . For Fstrong and FHT , the Finally, postulate (F6) is not always satisfied, but it seems that this result follows from Prop. 2 and the fact that these classes satisfy (W) is solely tied to the incompatibility with the crucial property, (SP). (cf. Fig. 1). The negative result for Fsem was shown in [53]. For FSM Though not fundamental to distinguish known classes of operators, it and FSas , consider the program P = {a ← p; p ← not not p}. helped establishing one of the fundamental results of this paper: that Then, for f ∈ FSM or f ∈ FSas , we have that f(P, {p}) ≡HT {a ← even if it is possible to forget a set of atoms, it may be impossible to not not a}. Therefore, f(P, {p}) |=HT a ← not not a, but it is not step-wise iteratively forget its subsets. the case that P |=HT a ← not not a, not p. Left open, for future work, is the investigation of these postulates Thus, surprisingly, even though the postulate is implied by the ex- for forgetting for semantics other than ASP, such as [49] based on the isting property (W), the set of classes of forgetting operators that FLP-semantics [45], or [1, 21] based on the well-founded semantics satisfy it does not coincide with that of the stronger property, which [13], as well as forgetting in the context of hybrid theories such as makes (F5) also a property of interest in the context of distinguish- [22, 15, 44] and reactive/evolving multi-context systems [16, 5], as ing existing classes of forgetting operators. Also, notably, while the well as the development of concrete syntactical forgetting operators properties (F4) and (F5) are different, they turn out to be satisfied by that can be integrated in reasoning tools such as [12, 19, 7]. 6 ACKNOWLEDGEMENTS [19] Vadim Ivanov, Matthias Knorr, and João Leite, ‘A query tool for EL with non-monotonic rules’, in Procs. of ISWC, eds., Harith We would like to thank the reviewers for their comments, which Alani, Lalana Kagal, Achille Fokoue, Paul T. Groth, Chris Biemann, helped improve this paper. R. Gonçalves, M. Knorr and J. Leite were Josiane Xavier Parreira, Lora Aroyo, Natasha F. Noy, Chris Welty, and Krzysztof Janowicz, volume 8218 of LNCS, pp. 216–231. Springer, partially supported by FCT under strategic project NOVA LINCS (2013). (PEst/UID/CEC/04516/2013). R. Gonçalves was partially supported [20] Jianmin Ji, Jia-Huai You, and Yisong Wang, ‘On forgetting postulates by FCT grant SFRH/BPD/100906/2014 and M. Knorr by FCT grant in answer set programming’, in Procs. of IJCAI, eds., Qiang Yang and SFRH/BPD/86970/2012. Michael Wooldridge, pp. 3076–3083. AAAI Press, (2015). [21] Matthias Knorr and José Júlio Alferes, ‘Preserving strong equivalence while forgetting’, in Procs. of JELIA, eds., Eduardo Fermé and João REFERENCES Leite, volume 8761 of LNCS, pp. 412–425. Springer, (2014). [22] Matthias Knorr, José Júlio Alferes, and Pascal Hitzler, ‘Local closed [1] José Júlio Alferes, Matthias Knorr, and Kewen Wang, ‘Forgetting under world reasoning with description logics under the well-founded seman- the well-founded semantics’, in Procs. of LPNMR, eds., Pedro Cabalar tics’, Artif. Intell., 175(9-10), 1528–1554, (2011). and Tran Cao Son, volume 8148 of LNCS, pp. 36–41. Springer, (2013). [23] Boris Konev, Michel Ludwig, Dirk Walther, and Frank Wolter, ‘The [2] José Júlio Alferes, João Alexandre Leite, Luı́s Moniz Pereira, Halina logical difference for the lightweight description logic EL’, J. Artif. In- Przymusinska, and Teodor C. Przymusinski, ‘Dynamic updates of non- tell. Res. (JAIR), 44, 633–708, (2012). monotonic knowledge bases’, The Journal of Logic Programming, [24] Boris Konev, Carsten Lutz, Dirk Walther, and Frank Wolter, ‘Model- 45(1-3), 43–70, (September/October 2000). theoretic inseparability and modularity of description logic ontologies’, [3] W. W. Bledsoe and Larry M. Hines, ‘Variable elimination and chaining Artif. Intell., 203, 66–103, (2013). in a resolution-based prover for inequalities’, in Procs. of CADE, eds., [25] Roman Kontchakov, Frank Wolter, and Michael Zakharyaschev, Wolfgang Bibel and Robert A. Kowalski, volume 87 of LNCS, pp. 70– ‘Logic-based ontology comparison and module extraction, with an ap- 87. Springer, (1980). plication to dl-lite’, Artif. Intell., 174(15), 1093–1141, (2010). [4] Stefan Brass and Jürgen Dix, ‘Semantics of (disjunctive) logic pro- [26] Jérôme Lang, Paolo Liberatore, and Pierre Marquis, ‘Propositional in- grams based on partial evaluation’, J. Log. Program., 40(1), 1–46, dependence: Formula-variable independence and forgetting’, J. Artif. (1999). Intell. Res. (JAIR), 18, 391–443, (2003). [5] Gerhard Brewka, Stefan Ellmauthaler, and Jörg Pührer, ‘Multi-context [27] Jérôme Lang and Pierre Marquis, ‘Reasoning under inconsistency: A systems for reactive reasoning in dynamic environments’, in Procs. of forgetting-based approach’, Artif. Intell., 174(12-13), 799–823, (2010). ECAI, eds., Torsten Schaub, Gerhard Friedrich, and Barry O’Sullivan, [28] Javier Larrosa, ‘Boosting search with variable elimination’, in Procs. of volume 263 of Frontiers in Artificial Intelligence and Applications, pp. CP, ed., Rina Dechter, volume 1894 of LNCS, pp. 291–305. Springer, 159–164. IOS Press, (2014). (2000). [6] Pedro Cabalar and Paolo Ferraris, ‘Propositional theories are strongly [29] Javier Larrosa, Enric Morancho, and David Niso, ‘On the practical use equivalent to logic programs’, TPLP, 7(6), 745–759, (2007). of variable elimination in constraint optimization problems: ’still-life’ [7] Nuno Costa, Matthias Knorr, and João Leite, ‘Next step for nohr: as a case study’, J. Artif. Intell. Res. (JAIR), 23, 421–440, (2005). OWL 2 QL’, in Procs. of ISWC, eds., Marcelo Arenas, Óscar Cor- [30] João Alexandre Leite, Evolving Knowledge Bases, volume 81 of Fron- cho, Elena Simperl, Markus Strohmaier, Mathieu d’Aquin, Kavitha tiers of Artificial Intelligence and Applications, xviii + 307 p. Hard- Srinivas, Paul T. Groth, Michel Dumontier, Jeff Heflin, Krishnaprasad cover, IOS Press, 2003. Thirunarayan, and Steffen Staab, volume 9366 of LNCS, pp. 569–586. [31] João Alexandre Leite and Luı́s Moniz Pereira, ‘Generalizing updates: Springer, (2015). From models to programs’, in Procs. LPKR, eds., Jürgen Dix, Luı́s Mo- [8] James P. Delgrande, Torsten Schaub, Hans Tompits, and Stefan niz Pereira, and Teodor C. Przymusinski, volume 1471 of LNCS, pp. Woltran, ‘A model-theoretic approach to belief change in answer set 224–246. Springer, (1997). programming’, ACM Trans. Comput. Log., 14(2), 14, (2013). [32] C. I. Lewis, A survey of symbolic logic, University of California Press, [9] James P. Delgrande and Kewen Wang, ‘A syntax-independent approach 1918. Republished by Dover, 1960. to forgetting in disjunctive logic programs’, in Procs. of AAAI, eds., [33] Vladimir Lifschitz, David Pearce, and Agustı́n Valverde, ‘Strongly Blai Bonet and Sven Koenig, pp. 1482–1488. AAAI Press, (2015). equivalent logic programs’, ACM Trans. Comput. Log., 2(4), 526–541, [10] Thomas Eiter, Michael Fink, Giuliana Sabbatini, and Hans Tompits, (2001). ‘On properties of update sequences based on causal rejection’, Theory [34] Vladimir Lifschitz, Lappoon R. Tang, and Hudson Turner, ‘Nested ex- and Practice of Logic Programming (TPLP), 2(6), 721–777, (2002). pressions in logic programs’, Ann. Math. Artif. Intell., 25(3-4), 369– [11] Thomas Eiter and Kewen Wang, ‘Semantic forgetting in answer set pro- 389, (1999). gramming’, Artif. Intell., 172(14), 1644–1672, (2008). [35] Fangzhen Lin and Raymond Reiter, ‘How to progress a database’, Artif. [12] Martin Gebser, Benjamin Kaufmann, Roland Kaminski, Max Os- Intell., 92(1-2), 131–167, (1997). trowski, Torsten Schaub, and Marius Thomas Schneider, ‘Potassco: The [36] Yongmei Liu and Ximing Wen, ‘On the progression of knowledge in the potsdam answer set solving collection’, AI Commun., 24(2), 107–124, situation calculus’, in Procs. of IJCAI, ed., Toby Walsh, pp. 976–982. (2011). IJCAI/AAAI, (2011). [13] Allen Van Gelder, Kenneth A. Ross, and John S. Schlipf, ‘The well- [37] Aart Middeldorp, Satoshi Okui, and Tetsuo Ida, ‘Lazy narrowing: founded semantics for general logic programs’, J. ACM, 38(3), 620– Strong completeness and eager variable elimination’, Theor. Comput. 650, (1991). Sci., 167(1&2), 95–130, (1996). [14] Michael Gelfond and Vladimir Lifschitz, ‘Classical negation in logic [38] Yves Moinard, ‘Forgetting literals with varying propositional symbols’, programs and disjunctive databases’, New Generation Comput., 9(3-4), J. Log. Comput., 17(5), 955–982, (2007). 365–385, (1991). [39] David Rajaratnam, Hector J. Levesque, Maurice Pagnucco, and [15] Ricardo Gonçalves and José Júlio Alferes, ‘Parametrized logic pro- Michael Thielscher, ‘Forgetting in action’, in Procs. of KR, eds., Chitta gramming’, in Procs. of JELIA’10, eds., Tomi Janhunen and Ilkka Baral, Giuseppe De Giacomo, and Thomas Eiter. AAAI Press, (2014). Niemelä, volume 6341 of LNCS, pp. 182–194. Springer, (2010). [40] Chiaki Sakama and Katsumi Inoue, ‘An abductive framework for com- [16] Ricardo Gonçalves, Matthias Knorr, and João Leite, ‘Evolving multi- puting knowledge base updates’, Theory and Practice of Logic Pro- context systems’, in Procs. of ECAI, eds., Torsten Schaub, Gerhard gramming (TPLP), 3(6), 671–713, (2003). Friedrich, and Barry O’Sullivan, volume 263 of Frontiers in Artificial [41] Martin Slota and João Leite, ‘Robust equivalence models for seman- Intelligence and Applications, pp. 375–380. IOS Press, (2014). tic updates of answer-set programs’, in Procs. of KR, eds., Gerhard [17] Ricardo Gonçalves, Matthias Knorr, and João Leite, ‘The ultimate Brewka, Thomas Eiter, and Sheila A. McIlraith, pp. 158–168. AAAI guide to forgetting in ASP’, in Procs. of KR, eds., Chitta Baral, James P. Press, (2012). Delgrande, and Frank Wolter, pp. 135–144. AAAI Press, (2016). [42] Martin Slota and João Leite, ‘A unifying perspective on knowledge up- [18] Ricardo Gonçalves, Matthias Knorr, and João Leite, ‘You can’t always dates’, in Procs. of JELIA, eds., Luis Fariñas del Cerro, Andreas Herzig, forget what you want: on the limits of forgetting in answer set program- and Jérôme Mengin, volume 7519 of LNAI, pp. 372–384. Springer, ming’, in Procs. of ECAI, eds., Maria S. Fox and Gal A. Kaminka. IOS (2012). Press, (2016). 7 [43] Martin Slota and João Leite, ‘The rise and fall of semantic rule updates based on se-models’, TPLP, 14(6), 869–907, (2014). [44] Martin Slota, João Leite, and Theresa Swift, ‘On updates of hybrid knowledge bases composed of ontologies and rules’, Artif. Intell., 229, 33–104, (2015). [45] Miroslaw Truszczynski, ‘Reducts of propositional theories, satisfiabil- ity relations, and generalizations of semantics of logic programs’, Artif. Intell., 174(16-17), 1285–1306, (2010). [46] Hudson Turner, ‘Strong equivalence made easy: nested expressions and weight constraints’, TPLP, 3(4-5), 609–622, (2003). [47] Yisong Wang, Kewen Wang, and Mingyi Zhang, ‘Forgetting for an- swer set programs revisited’, in Procs. of IJCAI, ed., Francesca Rossi. IJCAI/AAAI, (2013). [48] Yisong Wang, Yan Zhang, Yi Zhou, and Mingyi Zhang, ‘Forgetting in logic programs under strong equivalence’, in Procs. of KR, eds., Gerhard Brewka, Thomas Eiter, and Sheila A. McIlraith, pp. 643–647. AAAI Press, (2012). [49] Yisong Wang, Yan Zhang, Yi Zhou, and Mingyi Zhang, ‘Knowledge forgetting in answer set programming’, J. Artif. Intell. Res. (JAIR), 50, 31–70, (2014). [50] Zhe Wang, Kewen Wang, Rodney W. Topor, and Jeff Z. Pan, ‘Forget- ting for knowledge bases in DL-Lite’, Ann. Math. Artif. Intell., 58(1-2), 117–151, (2010). [51] Andreas Weber, ‘Updating propositional formulas’, in Expert Database Conf., pp. 487–500, (1986). [52] Ka-Shu Wong, ‘Sound and complete inference rules for SE- consequence’, J. Artif. Intell. Res. (JAIR), 31, 205–216, (2008). [53] Ka-Shu Wong, Forgetting in Logic Programs, Ph.D. dissertation, The University of New South Wales, 2009. [54] Yan Zhang and Norman Y. Foo, ‘Solving logic program conflict through strong and weak forgettings’, Artif. Intell., 170(8-9), 739–778, (2006). [55] Yan Zhang and Yi Zhou, ‘Knowledge forgetting: Properties and appli- cations’, Artif. Intell., 173(16-17), 1525–1537, (2009). 8