Solving Logic Program Conflict through Strong and Weak Forgettings

1 Introduction

One promising approach in the research of reasoning about knowledge dynamics is to represent agents' knowledge bases as logic programs on which necessary updates are conducted as a way to model agents' knowledge evolution. A key issue in this study is to solve various con�icts and inconsistencies in logic programs, e.g. [Leite, 2003].

While different logic program update approaches have been developed recently, we observe that some typical con�ict solving problems in logic programs have yet to be thoroughly investigated in the literature. Let us consider a scenario. John wants Sue to help him to complete his assignment. He knows that Sue will help him if she is not so busy. Tom is a good friend of John and wants John to let him copy John's assignment. Then John also learns that Sue hates Tom, and will not help him if he lets Tom copy his assignment, which will be completed under Sue's help. While John does not care whether Sue hates Tom or not, he has to consider Sue's condition to offer him help. What is John going to do? We formalize this scenario in a logic programming setting. John's knowledge base ΠJ :

r1 : Complete(John,Assignment) ← Help(Sue, John), r2 : Help(Sue, John) ← notBusy(Sue),

School of Comp. Sci. & Eng. University of New South Wales NSW 2052, Australia School of Computing & IT Grif�th University QLD 4111, Australia

r3 : Goodfriend(John, Tom) ←, r4 : Copy(Tom,Assignment) ← Goodf riend(J ohn, T om), Complete(J ohn, Assignment),

and Sue's knowledge base ΠS:

r5: Hate(Sue, T om) ←, r6: ← Help(Sue, John), Copy(T om, Assignment).

In order to take Sue's knowledge base into account, suppose John updates his knowledge base ΠJ in terms of Sue's ΠS . By applying proper logic program update approach, John may obtain a solution: Πf inal J = {r1, r2, r3, r5, r6} or its stable model, from which we know that Sue will help John to complete the assignment and John will not let T om copy his assignment. Although the con�ict between ΠJ and ΠS has been solved by updating, the result is somehow not always satisfactory. For instance, while John wants Sue to help him, he may have no interest at all in integrating the information that Sue hates Tom into his new knowledge base.

As an alternative, John may just weaken his knowledge base by forgetting atom Copy(T om, Assignment) from ΠJ in order to accommodate Sue's constraint. Then John may have a new program Πfinal J = {r1, r2, r3} - John remains a maximal knowledge subset which is consistent with Sue's condition without being involved in Sue's personal feeling about Tom.

The formal notion of forgetting in propositional theories was initially considered by Lin and Reiter from a cognitive robotics perspective [Lin and Reiter, 1994] and has recently received a great attention in KR community. It has been shown that the theory of forgetting has important applications in solving knowledge base inconsistencies, belief update and merging, abductive reasoning, causal theories of actions, and reasoning about knowledge under various propositional (modal) logic frameworks, e.g. [Lang and Marquis, 2002; Lang et al., 2003; Lin, 2001; Su et al., 2004].

In this paper, we consider how to forget a set of atoms from a propositional normal logic program and how this idea can be used in general con�ict solving under the context of logic programs. The rest of this paper is organized as follows. We present preliminary de�nitions and concepts in section 2. In section 3, we give formal de�nitions of strong and weak forgettings in logic programs. Based on these notions, in section 4, we propose a framework called logic program contexts for general con�ict solving in logic programs. In section 5, we investigate related semantic and computational properties. In section 6 we conclude the paper with some discussions.

2 Preliminaries

We consider �nite propositional normal logic programs in which each rule has the form:

where a is either a propositional atom or empty, and b1, · · · , bm, c1, · · · , cn are propositional atoms. When a is empty, rule (1) is called a constraint. Given a rule r of the form (1), we denote head(r) = {a}, pos(r) = {b1, · · · , bm} and neg(r) = {c1, · · · , cn}, and therefore, rule (1) may be represented as the form:

We also use Atom(r) to denote the set of all atoms occurring in rule r. For a program Π, we de�ne notions head(Π) = ⋃r∈Π head(r), pos(Π) = ⋃r∈Π pos(r), neg(Π) = ⋃r∈Π neg(r), Atom(Π) the set of all propositional atoms occurring in program Π. Given sets of atoms P and Q, we may use notion

to denote rule r′ obtained from r by removing all atoms occurring in P and Q in the positive and negation as failure parts respectively.

The stable model of a program Π is de�ned as follows. Firstly, we consider Π to be a program in which each rule does not contain negation as failure sign not. A �nite set S of propositional atoms is called a stable model of Π if S is the smallest set such that for each rule a ← b1, · · · , bm from Π, if b1, · · · , bm ∈ S, then a ∈ S. Now let Π be an arbitrary normal logic program. For any set S of atoms, programΠS is obtained from Π by deleting (1) each rule from Π that contains not c in the body and c ∈ S; and (2) all forms of not c in the bodies of the remaining rules. Then S is a stable model of Π if and only if S is a stable model of ΠS . A program may have one, more than one, or no stable models at all. A program is called consistent if it has a stable model. We say that an atom a is entailed from program Π, denoted as Π |= a if a is in every stable model of Π.

Given two programs Π1 and Π2. Π1 and Π2 are equivalent if Π1 and Π2 have the same stable models. Π1 and Π2 are called strongly equivalent if for every program Π, Π1 ∪ Π and Π2 ∪ Π are equivalent [Lifschitz et al., 2001].

Observation: Let Π be a logic program. If each rule r in Π is of one of the following two forms: (1) head(r) ̸= ∅ and head(r) ⊆ pos(r), or (2) pos(r) ∩ neg(r) ̸= ∅, then Π is strongly equivalent to the empty set.

For a later reference, we call the two types of rules mentioned above redundant rules.

Let Π be a logic program. We use [Π]C to denote the conjunctive normal form obtained from Π by translating each rule of the form (1) in Π in to the clause: a∨¬b1∨· · ·∨¬bm∨ c1 ∨ · · · ∨ cn. For instance, if Π = {a ← notb, c ← a}, then we have [Π]C = (a ∨ b) ∧ (c ∨ ¬a). In general, we may write [Π]C = {C1, · · · ,Cn} where each Ci is a conjunct of [Π]C .

If Ci is a clause, we call any sub formula of Ci a subclause of Ci.

Now we introduce the notion of forgetting in a classical propositional theory [Lin and Reiter, 1994; Lin, 2001]. Let T be propositional theory. We use T(p/true) (or T(p/false), resp.) to denote the theory obtained from T by substituting all occurrences of propositional atom p with true (or false, resp.). For instance, if T = {p ⊃ q, (q ∧ r) ⊃ s}, then T (q/true) = {r ⊃ s} and T(q/false) = {¬p}. Then we can de�ne the notion of forgetting in terms of a propositional theory. For a given propositional theory T and a set of propositional atoms P , the result of forgetting P in T , denoted as Forget(T, P), is de�ned inductively as follows:

It is easy to see that the ordering in which atoms in P are considered does not affect the �nal result of forgetting P from T . Consider T = {p ⊃ q, (q∧r) ⊃ s} again. From the above de�nition, we have Forget (T, {q}) = {(r ⊃ s) ∨ ¬p}.

3 Strong andWeak Forgettings in Logic Programs

Let us consider how to forget a set of atoms from a logic program. Intuitively, we would expect that after forgetting a set of atoms, all occurrences of these atoms in the underlying program should be eliminated in some way, and moreover, other atoms having connections to them through rules in the programmight also be affected. We observe that the notion of forgetting in propositional theories is not applicable to logic programs since there is no disjunctive operation for logic programs. Further, different ways of handling negation as failure in forgetting may also lead to different resulting programs. To formalize our idea of forgetting in logic programs, we �rst introduce a program transformation called reduction.

De�nition 1 (Program reduction) Let Π be a program and p an atom. We de�ne the reduction of Π with respect to p, denoted as Reduct (Π, {p}), to be a program obtained from Π by (1) for each rule r with head(r) = p and each rule r ′ with p ∈ pos(r′ ), replacing r′ with a new rule r′′ : head(r′ ) ← (pos(r)∪pos(r′ )-{p}), not(neg(r)∪neg(r′ )); (2) if there is such rule r′ in Π and has been replaced by r′′ in (1), then removing rule r from the remaining program. Let P be a set of atoms. Then the reduction of Π with respect to P is inductively de�ned as follows:

Note that in our program reduction de�nition, step (1) is the same as logic program unfolding [Brass and Dix, 1999]. While unfolding is to eliminate positive body occurrences of an atom in a logic program, the reduction, on other hand, is further to remove those rules with heads of this atom.

Example 1 Let Π1 = {a ← notb, a ← d, c ← a, note}, Π2 = {a ← c, notb, c ← notd}, and Π3 = {a ← b, b ← notd, c ← a, note}. Then Reduct(Π1, {a}) = {c ← notb, note, c ← d, note}, Reduct(Π2, {a}) = Π2, and Reduct (Π3, {a, b}) = {c ← notd, note}. □

De�nition 2 (Strong forgetting) Let Π be a logic program, and p an atom. We de�ne a program to be the result of strongly forgetting p in Π, denoted as SForgetLP(Π, {p}), if it is obtained from the following transformation:

1. Π′ =Reduct(Π, {p});

2. Π′ =Π′ -{r | r is a redundant rule}; 3. Π′ =Π′ -{r | head(r) = p}; 4. Π′ =Π′ -{r | p ∈ pos(r)}; 5. Π′ =Π′ -{r | p ∈ neg(r)}; 6. SForgetLP(Π, {p}) = Π′ .

Let us take a closer look at De�nition 2. Step 1 is just to perform reduction on Π with respect to atom p. This is to replace those positive body occurrences of p in rules with other rules having p as the head. Step 2 is to remove all redundant rules which may be introduced by the reduction of Π with respect to p. From Observation in section 2, we know that this does not change anything in the program. Steps 3 and 4 are to remove those rules which have p as the head or in the positive body. Note that after Steps 1 and 2, there does not exist any pair of rules r and r′ such that head(r) = {p} and p ∈ pos(r′ ). Then the intuitive meaning of Steps 3 and 4 is that after forgetting p, any atom's information in rules having p as their heads or positive bodies will be lost because they are all relevant to p, i.e. these atoms either serve as a support for p or p is in part of the supports for these atoms. On the other hand, Step 5 states that any rule containing p in its negation as failure part will be also removed. The consideration for this step is as follows. If we think neg(r) is a part of support of head(r), then when p ∈ neg(r) is forgotten, head(r)'s entire support is lost as well. Clearly, such treatment of negation as failure in forgetting is quite strong in the sense that more atoms may be lost together with notp. Therefore we call this kind of forgetting strong forgetting.

With a different way of dealing with negation as failure, we have a weak version of forgetting. We de�ne a program to be the result of weakly forgetting p in Π, denoted as WForgetLP(Π, {p}), exactly in the same way as in De�- nition 2 except that Step 5 is replaced by the following step:

Suppose we have a rule like r : head(r) ← pos(r), notneg(r) where p ∈ neg(r). Instead of viewing neg(r) as part of the support of head(r), we may treat it as a default evidence of head(r), i.e. under the condition of pos(r), if all atoms in neg(r) are not presented, then head(r) can be derived. Therefore, forgetting p will result in the absence of p in any case. So r may be replaced by r ′ : head(r) ← pos(r), not (neg(r) - {p}).

Strong and weak forgettings can be easily extended to the case of a set of atoms:

and WForgetLP(Π, P) is de�ned accordingly. The following proposition ensures that our strong and weak forgettings in logic programs are well de�ned under strong equivalence.

SForgetLP(Π, ∅) = Π, SForgetLP(Π, P ∪ {p}) = SForgetLP (SForgetLP (Π, {p}), P ),

Proposition 1 Let Π be a logic program and p, q two propositional atoms. Then

1. SForgetLP(SForgetLP(Π, {p}), {q}) is strongly equivalent to SForgetLP(SForgetLP(Π, {q}), {p});
2. WForgetLP(WForgetLP(Π, {p}), {q}) is strongly equivalent to WForgetLP(WForgetLP(Π, {q}), {p}).

Example 2 Let Π = {b ← a, c, d ← nota, e ← notf}.

Then we have SForgetLP(Π, {a}) = {e ← notf}, and WForgetLP(Π, {a}) = {d ←, e ← notf}. Now we consider Forget([Π]C , {a}), which is logically equivalent to formula (b ∨ ¬c ∨ d) ∧ (f ∨ e). Then it is clear that |= Forget ([Π]C , {a}) ⊃ [SForgetLP(Π, {a})]C , and |= [WForgetLP(Π, {a})]C ⊃ Forget ([Π]C , {a}). □

The above example motivates us to examine the deeper relationships between strong and weak forgettings in logic programs and forgetting in propositional theories. Let Π be a program and L a clause, i.e. L = l1 ∨ · · · ∨ lk where each li is a propositional literal. We say that L is Πcoherent if there exists a subset Π′ of Π and a set of atoms P ⊆ Atom(Π) (P could be empty) such that L is a subclause of [Reduct(Π′ , P)]C (i.e. [Reduct(Π′ , P)]C is a single clause). The intuition behind this notion is to specify those clauses that are parts of clauses generated from program Π through reduction. Consider program Π = {a ← b, d ← a, notc, e ← notd}. Clause d ∨ b is Π-coherent, where clause ¬d ∨ e is not. Obviously, for each rule r ∈ Π, [{r}]C is Π-coherent. The following proposition provides a semantic account for Π-coherent clauses.

Proposition 2 Let Π be a program and L a Π-coherent clause. Then either |= [Π]C ⊃ L or |= L ⊃ Φ for some clause Φ where |= [Π]C ⊃ Φ.

De�nition 3 Let Π be a logic program, ϕ, ϕ1 and ϕ2 three propositional formulas where ϕ1 and ϕ2 are in conjunctive normal forms.

1. ϕ1 is called a consequence of ϕ with respect to Π if |= ϕ ⊃ ϕ1 and each conjunct of ϕ1 is Π-coherent. ϕ1 is a strongest consequence of ϕ with respect to Π if ϕ1 is a consequence of ϕ with respect to Π and there does not exist another consequence ϕ′1 of ϕ (ϕ′1 ̸≡ ϕ1) with respect to Π such that |= ϕ′1 ⊃ ϕ1.
2. ϕ2 is called a premiss of ϕ with respect to Π if |= ϕ2 ⊃ ϕ and each conjunct of ϕ2 is Π-coherent. ϕ2 is a weakest premiss of ϕ with respect to Π if ϕ2 is a premiss of ϕ with respect to Π and there does not exist another premiss ϕ′2 of ϕ (ϕ′2 ̸≡ ϕ2) with respect to Π such that |= ϕ2 ⊃ ϕ′2.

Example 3 (Example 2 continued) It is easy to verify that [SForgetLP(Π, {a})]C is a strongest consequence of Forget([Π]C , {a}) and [WForgetLP(Π, {a})]C is a weakest premiss of Forget([Π]C , {a}). In fact, the following theorem con�rms that this is always true. □

Theorem 1 Let Π be a logic program and P a set of atoms. Then [SForgetLP(Π, P)]C is a strongest consequence of Forget([Π]C , P) with respect to Π and [WForgetLP(Π, P)]C is a weakest premiss of Forget([Π]C , P) with respect to Π.

Theorem 1 actually provides a precise semantic characterization for strong and weak forgettings in logic programs in terms of the forgetting notion in the corresponding propositional theory.

4 Solving Con�icts in Logic Program Contexts

In this section, we de�ne a general framework called logic program context to represent a knowledge system which consists of multiple agents' knowledge bases. We consider the issue of con�icts occurring in the reasoning within the underlying logic program context. As we will show, the notions of strong and weak forgettings provide an effective way to solve such con�icts.

De�nition 4 (Logic programcontext) A logic programcontext is a n-ary tuple Σ = (Φ1, · · · ,Φn), where each Φi is a triplet (Πi, Ci,Fi) - Πi and Ci are two logic programs, and Fi ⊆ Atom(Πi) is a set of atoms. We also call each Φi the ith component of Σ. Σ is consistent if for each i, Πi ∪ Ci is consistent. Σ is con�ict-free if for any i and j, Πi ∪ Cj is consistent.

In the above de�nition, for a given logic program context Σ, each component Φi represents agent i's local situation, where Πi is agent i's knowledge base, Ci is a set of constraints that agent i should comply and will not change in any case, and Fi is a set of atoms that agent i may forget if necessary. To simplify our following discussion, we assume that for each component Φi, the corresponding agent's knowledge base Πi does not contain constraints (i.e. rules with empty heads). Alternatively such constraints will be contained in the constraint set Ci though Ci may also contain rules with nonempty heads.

Now the problem of con�ict solving under this setting can be stated as follows: given a logic program context Σ = (Φ1, · · · , Φn), which may not be consistent or con�ictfree, how can we �nd an alternative logic program context Σ′ = (Φ′1 , · · · , Φ′n) such that Σ′ is con�ict-free and is closest to the original Σ in some sense?

De�nition 5 (Solution) Let Σ = (Φ1, · · · ,Φn) be a logic program context, where each Φi = (Πi, Ci,Fi). We call a logic program context Σ′ a solution that solves con�icts in Σ, if Σ′ satis�es the following conditions:

1. Σ′ is con�ict-free;
2. Σ′ = (Φ′1 , · · · , Φ′n), where Φ′i = (Π′i , Ci, Fi), and Π′i = SForgetLP(Πi, Pi) or Π′i = WForgetLP(Πi, Pi) for some Pi ⊆ Fi.

We denote the set of all solutions of Σ as Solution(Σ).

De�nition 6 (Ordering on solutions) Let Σ, Σ′ and Σ′′ be three logic program contexts, where Σ′ ,Σ′′ ∈ Solution(Σ). We say that Σ′ is closer or as close to Σ as Σ′′ , denoted as Σ′ ⪯Σ Σ′′ , if for each i, Φ′i = (Π′i , Ci,Fi) ∈ Σ′ and Φ′′ i = (Π′′ i , Ci,Fi) ∈ Σ′′ , where Π′i = SForgetLP(Πi, Pi) or Π′i = WForgetLP(Πi, Pi) for some Pi ⊆ Fi, and Π′′ i = SForgetLP(Πi,Qi) or Π′′ i = WForgetLP(Πi,Qi) for some Qi ⊆ Fi respectively, we have Pi ⊆ Qi ⊆ Fi. We denote Σ′ ≺Σ Σ′′ if Σ′ ⪯Σ Σ′′ and Σ′′ ̸⪯Σ Σ′ .

De�nition 7 (Preferred solution) Let Σ and Σ′ be two logic program contexts. We say that Σ′ is a preferred solution of Σ, if Σ′ ∈ Solution(Σ) and there does not exist another Σ′′ ∈ Solution(Σ) such that Σ′′ ≺Σ Σ′ .

Example 4 Let Σ = (Φ1, Φ2), where

It is easy to see that Σ is consistent but not con�ict-free because neither Π1 ∪ C2 nor Π2 ∪ C1 is consistent. Now consider two logic program contexts Σ1 = (Φ′1,Φ′2) and Σ2 = (Φ′′ 1 , Φ′′ 2 ), where

• Φ′1 = (SForgetLP(Π1, {c}), C1, F1),

Φ′′

1 = (WForgetLP(Π1, {a, c}), C1, F1),

Φ′′ 2 = (WForgetLP(Φ2, {e}, C2, F2).

It can be veri�ed that both Σ1 and Σ2 are solutions of Σ, but only Σ1 is a preferred solution. □

5 Semantic and Computational Properties

In this section, we study some important semantic and computational properties in relation to strong and weak forgettings and con�ict solving.

5.1 Semantic Characterizations

We observe that the consistency of program Π does not necessarily imply a consistent SForgetLP(Π, P) or WForgetLP(Π, P) for some set of atoms P, and vice versa. For example, consider program Π = {a ←, b ← nota, notb}, then weakly forgetting a in Π will result in an inconsistent program {b ← notb}. Similarly, strongly forgetting a from an inconsistent program Π = {b ← nota, c ← b, notc} will get a consistent program {c ← b, notc}.

To understand why this may happen, we �rst introduce some notions. Given program Π and a set of atoms P, we specify two programs X and Y . Program X is a subset of Π containing three types of rules in Π: (1) for each p ∈ P, if p ̸∈ head(Π), then rule r ∈ Π with p ∈ pos(r) is in X; (2) for each p ∈ P, if p ̸∈ pos(Π), then rule r ∈ Π with head(r) = {p} ⊆ X; and (3) rule r ∈ Π with neg(r) ∩ P ̸= ∅ but not of the types (1) and (2) is also in X. Clearly, X contains those rules of Π satisfying Atom(r) ∩ P ̸= ∅ but will not be affected by Reduct(Π, P ). On the other hand, programY is obtained as follows: for each rule r in X of the type (3), a replacement of r of the form: r′ : head(r) ← pos(r), not(neg(r) -P) is in Y . It should be noted that both X and Y can be obtained in linear time in terms of the sizes of Π and P .

Theorem 2 Let Π be a program and P a set of atoms. A subset S of atoms occurring in SForgetLP(Π, P) (or in WForgetLP(Π, P)) is a stable model of SForgetLP(Π, P)

(or WForgetLP(Π, P) resp.) iff program Π -X (or (Π - X) ∪ Y resp.) has a stable model S ′ such that S = S ′ - P .

Theorem 2 presents an interesting result: given program Π and set of atoms P , although computing SForgetLP(Π, P ) or WForgetLP(Π, P) may need exponential time (see Section 5.3), its stable models, however, can be computed through some program that is obtained fromΠ in linear time.

Now we consider the existence of (preferred) solutions for logic program contexts in con�ict solving. It is easy to see that not every logic program context has a preferred solution. For instance, Σ = (({a ← nota}, ∅, ∅)) has no solution, and hence has no preferred solution neither. The following result shows that the existence of a Σ's solution always implies the existence of Σ's preferred solution, and vice versa.

Theorem 3 Let Σ be a logic program context. Σ has a preferred solution iff Solution(Σ) ̸= ∅.

Although deciding whether a Σ has a (preferred) solution is NP-hard (see Theorem 6 in section 5.3), we can identify a useful class of logic program contexts whose solutions always exist (we have showed in our full paper that all major logic program update approaches can be transformed into the following form of con�ict solving context).

Proposition 3 Let Σ = (Φ1, · · · ,Φn) be a logic program context. If for each Φi = (Πi, Ci,Fi), Ci is consistent, and for each r ∈ Πi, Fi ∩Atom(r) ̸= ∅, then Solution(Σ) ̸= ∅.

Proof: We show that Σ′ = (Φ′1, · · · ,Φ′n), where Φ′i = (∅, Ci,Fi) (1 ≤ i ≤ n) is a solution of Σ. Since for each i, Fi ∩ Atom(r) ̸= ∅ for each r ∈ Πi, we have Π′i = SForgetLP(Πi,Fi) = ∅ (note that this is because we already assumed that Πi does not contain any rules with empty heads. Instead, this type of rule is contained in Ci). This follows that Π′i ∪ Cj = Cj for all j = 1, · · · , n are consistent. So ((∅, C1, F1), · · · , (∅, Cn, Fn)) is a solution of Σ. □

5.2 Representing Logic programUpdates

One major advantage of the proposed framework of logic program contexts is that it can represent new con�ict solving scenarios for which the traditional logic program update approaches may not handle properly, like the one discussed in section 1 (or Example 4). In fact, our framework can also represent previous logic program update approaches. To illustrate this, we take Sakama and Inoue's update approach [Sakama and Inoue, 1999] as an example (note that we need to restrict their approach to a normal logic program setting).

De�nition 8 [Sakama and Inoue, 1999] Let Π1 and Π2 be two consistent logic programs. Program Π′ is a SI-result of a theory update of Π1 by Π2 if (1) Π′ is consistent, (2) Π2 ⊆ Π′ ⊆ Π1 ∪ Π2, and (3) there is no other consistent program Π′′ such that Π′ ⊂ Π′′ ⊆ Π1 ∪ Π2.

Now we transform Sakama and Inoue's theory update into a logic program context. First, for each rule r ∈ Π1, we introduce a new atom lr which does not occur in Atom(Π1 ∪Π2). Then we de�ne a program Π′1 : for each r ∈ Π1, rule r′ : head(r) ← pos(r), not(neg(r) ∪ {l r }) is in Π′1 . That is, for each r ∈ Π1, we simply extend its negative body with a unique atom lr . This will make each r′ in Π′1 be removable by strongly forgetting atom l r without in�uencing other rules. Finally, we specify ΣSI = (Φ1,Φ2), where Φ1 = (Π′1, ∅, {lr | r ∈ Π1}) and Φ2 = (∅, Π2, ∅).

For convenience, we also use Π-notP to denote a program obtained from Π by removing all occurrences of atoms in P from the negative bodies of all rules in Π. For instance, if Π = {a ← b, notc, notd}, then Π-not{c} = {a ← b, notd}. Now we have the following characterization result.

Theorem 4 Let Π1 and Π2 be two consistent programs, and ΣSI as speci�ed above. Π′ is a SI-result of updating Π1 by Π2 iff Π′ = Π-not{lr |r∈Π1} ∪ Π2, where Σ′ = ((Π, ∅, {lr | r ∈ Π1}), (∅, Π2, ∅)) is a preferred solution of ΣSI .

In our full paper we have showed that other logic program update approaches such as Eiter et al's causal rejection and Dynamic Logic Programming [Eiter et al., 2002; Leite, 2003] for dealing with sequence of programs can also be embedded into our framework. In this sense, the logic program context provides a uni�ed framework for logic program updates.

5.3 Complexity Results

We assume that readers are familiar with the complexity classes of P, NP, coNP, ΣP2 and ΠP2 = coΣP2 . The class of DP contains all languages L such that L = L1 ∩L2 where L1 is in NP and L2 is in coNP. The class coDP is the complement of class DP (readers refer to [Papadimitriou, 1994] for further details).

We observe that the main computation of strong and weak forgettings relies on the procedure of reduction that further inherits the computation of program unfolding. Hence, in general computing strong and weak forgetting may need exponential steps of rule substitutions in terms of the sizes of the input program and the set of forgotten atoms. However, the following result shows that the inference problem associated to strong and weak forgettings still remains in coNP.

Proposition 4 Let Π be a logic program, P a set of atoms, and a an atom. Then deciding whether SForgetLP(Π, P ) |= a (or WForgetLP(Π, P) |= a) is coNP-complete.

Proof: (Sketch) The hardness is followed by setting P = ∅, and the membership can be proved by using Theorem 2. □

Now we consider the complexity of irrelevance in relation to strong and weak forgettings and con�ict solving. From a semantic viewpoint, the irrelevance tells us whether a strong/weak forgetting or con�ict solving procedure will affect some particular atoms occurring in the underlying programs. Hence, studying its associated computational properties is important.

De�nition 9 (Irrelevance) Let Π be a logic program, P a set of atoms, and a an atom. We say that a is irrelevant to P in Π, if either Π |= a iff SForgetLP(Π, P) |= a, or Π |= a iff WForgetLP(Π, P) |= a.

We generalize the notion of irrelevance to the logic program context. Formally, let Σ be a logic program context and a an atom, we say that a is derivable from Σ's ith component, denoted as Σ |=i a, if Φi = (Πi, Ci, Fi) ∈ Σ and Πi |= a.

De�nition 10 (Irrelevance wrt logic program contexts) Let Σ and Σ′ be two logic program contexts where Σ′ ∈ Solution(Σ), and a an atom. We say that a is irrelevant with respect to Σ and Σ′ on their ith components, or simply say that a is (Σ,Σ′ )i -irrelevant, if Σ |=i a iff Σ′ |=i a.

Theorem 5 Let Π be a logic program, P a set of atoms, a an atom, and Σ and Σ′ two logic program contexts where Σ′ ∈ Solution(Σ). The the following results hold:

1. Deciding whether a is irrelevant to P in Π is coDPcomplete;
2. Deciding whether a is (Σ,Σ′ )i -irrelevant is coDPcomplete.

Proof: (Sketch) We describe the main idea of proving the hardness part of Result 1. a is irrelevant to P in Π if (1) Π |= a iff SForgetLP(Π, P) |= a, or (2) Π |= a iff WForgetLP(Π, P) |= a. Here we consider case (1) and proof for case (2) is the same. Let (Φ1,Φ2) be a pair of CNFs, where Φ1 = {C1, · · · , Cm} and Φ2 = {C ′1, · · · , C ′n}, and each Ci and C ′j (1 ≤ i ≤ n, 1 ≤ j ≤ n) are sets of propositional literals respectively. We also assume Atom(Φ1) ∩ Atom(Φ2) = ∅. We know that deciding whether Φ1 is satis�able or Φ2 is unsatis�able is coDPcomplete [Papadimitriou, 1994]. We construct a program Π polynomially based on set Atom(Φ1) ∪ Atom(Φ2) ∪ ˆX ∪ ˆ Y ∪ {l1, · · · , ln, p, a, satΦ1 , unsatΦ1 , unsatΦ2 }, where any two sets of atoms are disjoint and | ˆX| = |Atom(Φ1)| and | ˆ Y | = |Atom(Φ2)|. Π consists of four groups of rules where atom p only occurs in Π4:

Π1: rules to generate all truth assignments of Φ1 and Φ2;

Π2: rules to derive unsatΦ1 and unsatΦ2 if Φ1 and Φ2 are unsatis�able respectively;

• Π3: rules to force a truth assignment of Φ2 making ¬Φ2 true if unsatΦ2 is derivable fromΠ;

Π4 contains 4 rules: satΦ1 ← notunsatΦ1 , a ← satΦ1 , unsatΦ2 ← nota, p ←.

Then we can prove that Φ1 is satis�able or Φ2 is unsatis�able iff (Π |= a and SForgetLP(Π, {p}) |= a) or (Π ̸|= a and SForgetLP(Π, {p}) ̸|= a). □

Finally, the following theorem summarizes major complexity results of con�ict solving in logic program contexts.

Theorem 6 Let Σ = (Φ1, · · · , Φn) and Σ′ = (Φ′1 , · · · , Φ′n) be two logic program contexts, where for each Φi = (Πi, Ci,Fi) ∈ Σ (1 ≤ i ≤ n), Φ′i ∈ Σ′ is of the form Φ′i = (Π′i , Ci,Fi), where Π′i = SForgetLP(Πi, Pi) or Π′i = WForgetLP(Πi, Pi) for some Pi ⊆ Fi.

1. DecidingwhetherΣhas a preferred solution is NP-hard;
2. Deciding whether Σ′ is a solution of Σ is NP-complete;
3. Deciding whether Σ′ is a preferred solution of Σ is in ΠP2 , if strong and weak forgettings in Σ can be computed in polynomial time 1 ;

1 In our full paper, we have classi�ed certain classes of logic program contexts, where for each Φi = (Πi, Ci,Fi) ∈ Σ and each Pi ⊆ Fi, SForgetLP (Πi, Pi) and WForgetLP (Πi, Pi) can always be computed in polynomial time.

1. For a given atom a, deciding whether for each Σ′′ ∈ Solution(Σ), Σ′′ |=i a is in ΠP2 , if strong and weak forgettings in Σ can be computed in polynomial time.

6 Conclusions

In this paper, we de�ned notions of strong and weak forgettings in logic programs, which may be viewed as an analogy of forgetting in propositional theories. Based on these notions, we developed a general framework of logic program contexts for con�ict solving and studied the related semantic and computational properties.

Our work presented in this paper can be extended in several directions. One interesting topic is to associate dynamic preferences to sets of forgettable atoms and components in logic program contexts, so that the extended framework is more �exible to handle task-dependent con�ict solving.