Minimal Change and Maximal Coherence for Epistemic Logic Program Updates

1 Introduction

Logic programming has been proved to be one of the most promising logic based formulations for problem solving, knowledge representation and reasoning, and reasoning about actions and plans. Recent research on logic program updates further shows that logic programming also provides a feasi­ ble framework for modeling agents' activities in dynamic en­ vironments [Alferes and et al, 2000; Eiter and et al, 2002; Sakama and Inoue, 1999; Zhang and Foo, 1998].

While all current approaches for logic program updates fo­ cus on the problem of updating extended logic programs or their variations, updating epistemic logic programs, however, has yet to be explored in the research. By combining knowl­ edge and belief operators into logic rules, epistemic logic programming [Gel fond, 1994] is a powerful representation formalism in logic programming paradigm. It can deal with more difficult problems in reasoning with disjunctive infor­ mation while traditional disjunctive extended logic programs fail to handle. Furthermore, epistemic logic programs seem more feasible for knowledge reasoning than many other au­ toepistemic logics [Gelfond, 1994] and has been used as a formal basis for modeling knowledge in action theories, e.g.

[Lobo et al., 2001]. When we use an epistemic logic pro­ gram to represent an agent's knowledge base, it is a nontrivial question how the agent's knowledge base (an epistemic logic program) can be updated when new information is received.

In this paper, we propose an approach for epistemic logic program updates. Contrary to other logic programs, notions of knowledge and beliefs in epistemic logic programs have strong semantic connections to the standard Kripke structures of modal logics. On the other hand, epistemic logic programs are also sensitive with various syntactic forms. Hence, we be­ lieve that a pure model-based or syntax-based approach will not be appropriate to handle epistemic logic program updates. Instead, we require our update formulation to meet three ma­ jor criteria: (1) an update should be performed on a basis of minimal change semantics to remove contradictory infor­ mation; (2) based on the minimal change semantics, the up­ date result should have a clear syntactic representation and contain maximal consistent information from previous pro­ gram(s); and (3) the underlying update procedure should be consistent, that is, updating a consistent program by another consistent program (or a sequence of consistent programs) should generate a consistent result. Our main idea to accom­ plish these criteria is so called minimal change arid maximal coherence which presents both semantic and syntactic fea­ tures in an update procedure.

The paper is organized as follows. Section 2 presents a brief overview on epistemic logic programs. Section 3 de­ velops a formulation for epistemic logic program updates, while section 4 extends this formulation to handle update se­ quences. Section 5 investigates important semantic properties for our update approach. Finally, section 6 concludes the pa­ per with discussions on related work and future research.

2 Epistemic Logic Programs: An Overview

In this section, we present a general overview on epistemic logic programs. Gelfond extended the syntax and semantics of disjunctive logic programs to allow the correct representa­ tion of incomplete information (knowledge) in the presence of multiple extensions. Consider the following disjunctive program about the policy of offering scholarships in some university [Gelfond, 1994]:

P: r1: eligible(x) ~ highGPA(x), r2: eligible(x) ~ minority(x),fairGPA(x) ,

r3 : · eligible(x) ~ ·fairGPA(x), ·highGPA(x), r 4 : interview( .1: ) ~not eligible(x) , not · eligible(x), r5: fairGPA(mike) or highGPA(mike) ~.

Rule r4 can be viewed as a formalization of the statement: "the sutdents whose eligibility is not decided by rules r1, r2 and r3 should be interviewed by the committee". It is easy to see that P has two answer sets {highGPA(mike), eligible(mike)} and {fairGPA(mike), interview(mike)}. Therefore the answer to query interview( mike) is unknown, which seems too weak from our intuition. Epistemic logic programs will overcome this kind of difficulties in reasoning with incomplete information.

In epistemic logic programs, the language of (disjunctive) extended logic programs is expanded with two modal opera­ tors Kand M. KF is read as "F is known to be true" and MF is read as "F may be believed to be true". For our purpose, in this paper we will only consider propositional epistemic logic programs where rules containing variables are viewed as the set of all ground rules by replacing these variables with all constants occurring in the language. The semantics for epistemic logic programs is defined by pairs (A, W), where A is a collection of sets of ground literals called the sets of possible beliefs of certain agent, while W is a set in A called the agent's working set of beliefs. The truth of a formula F in (A, W) is denoted by (A, W) I= F and the falsity by (A, W) =IF, and are defined as follows:

(A, W) I= F iff F E W where F is a ground atom.

(A , W) I= KF iff (A, W;) I= F for all W; EA.

(A, W) I= MF iff (A, W;) I= F for some W; E A.

(A, W) I= F 1\ G iff (A, W) I= F and (A, W) I= G.

(A , W) I= For G iff(A, W) I= ·(·F 1\ ·G).

(A , W) I= ·F iff (A , W) =IF.

(A, W) =IF iff ·F E W where F is a ground atom.

(A , W) =IJ<F iff (A , W) &i= KF.

(A, W) =IMF iff (A, W) &i= MF.

(A, W) =IF 1\ G iff(A, W) =IF or (A, W) =I G.

(A, W) =IF or G iff (A, W) =IF and (A, W) =I G.

It is clear that if a formula G is of the form KF, --,J{F, MF or·MF,thenitstruthvaluein(A, W) willnotdependon W and we call G a subjective formula. On the other hand, if G does not contain I< or M, then its truth value in (A, W) will only depend on W and we call G an objective formula. In the case that G is subjective, we simply write A I= G instead of (A, W) I= G, and W I= G instead of (A, W) I= Gin the case that G is objective.

An epistemic logic program is a finite set of rules of the form:

In (1) F is of the form F1 or · · · or Fk and F1, · · ·, Fk are objective literals, G1, · · ·, Gm are objective or subjective lit­ erals, and Gm+ 1 , · · · , Gn are objective literals. For an epis­ temic logic program P, its semantics is given by its world view which is defined in the following steps:

Step 1. Let P be an epistemic logic program not containing modal operators J( and M and negation as failure not. A set W of ground literals is called a belief set of P iff W

is a minimal set of satisfying conditions: (i) for each rule F ~ G1 , · · ·, Gm from P such that WI= G1 /\ · ··I\ Gm we have W I= F; and (ii) if W contains a pair of complementary literals then W = Lit, i.e. W is an inconsistent belief set.

Step 2. Let P be an epistemic logic program not containing modal operators I< and M and W be a set of ground literals in the language of P. By Pw we denote the result of (i) removing from P all the rules containing formulas of the form notG such that W I= G and (ii) removing from the rules in P all other occurrences of formulas of the form notG.

Step 3. Finally, let P be an arbitrary epistemic logic program anctA a collection of sets of ground literals in its language. By P A we denote the epistemic logic program obtained from P by (i) removing from P all rules containing formulas of the form G such that G is subjective and A &t= G, and (ii) removing from rules in P all other occurrences of subjective formulas.

Now we define that a collection A of sets of ground literals is a world view of P if A is the collection of all belief sets of P A. Consider program P about the eligibility of scholarship discussed earlier, if we replace rule r4 with the following rule:

then the epistemic logic program that consists of rules r1, r2, r3, r,4, and r5 will have a unique world view { {highGPA(mike), eligible( mike), interview( mike)},

{fairGPA( mike), interview( mike)}}, which will result in a yes answer to the query interview (mike).

3 Formalizing Epistemic Logic Program Updates

From this section, we start to develop a formulation for epis­ temic logic program updates. Consider the update of an epis­ temic logic program P 1 by another epistemic logic program P 2. Our approach consists of two stages: firstly, we update each world view ofP1 by P2- this will remove contradictory information between P 1 and P 2 and ensure a minimal change for the underlying update semantics; and secondly, from the first stage result, we will derive a resulting program which re­ tains the maximal consistent information represented by P 1.

3.1 Preliminaries

To begin with, we first introduce some useful notions. Let A be a collection of belief sets (i .e. sets of ground literals) and P an epistemic logic program. We call a pair (A, W) where W E A an epistemic model induced from A . If A is a world view of P, then M = (A, W) is also called an epistemic model of P . We use ind (A) to denote the set of all epistemic models induced from A. Note llind(A)II = I lA II·

Consider a rule r of the form (1). We use H(r) and B ( r) to denote the head and body parts of rule r respec­ tively. For instance, for ruler: a or ·b ~ c, I<d , not · e, wehaveH(r) = {a,--,b},andB(r) = {c,Kd,nobe}. We say H ( r) is satisfied in an epistemic model M, denoted as M I= H(r), iff for some FE H(r) M I= F . We say B(r) is satisfied in M, denoted as M I= B ( r), iff ( 1) for each ob­ jective or subjective literal G E B ( r) M I= G, and (2) for each not G E B ( r) M &i= G. r is satisfied in M, denoted as M f= 1·, if M f= B(r) implies M f= H(r). An epis­ temic logic program P is satisfied in M if each rule of P is satisfied in .M. P is satisfied in a collection of belief sets A if P is satisfied in all epistemic models induced from A. A ground literal Lis derivable from P, denoted asP f= L, if L is true in all world views ofP, i.e. Lis true in all epistemic models induced from each world view of P.

A collection of belief sets is consistent if each of its belief sets is consistent. An epistemic logic program is consistent if it has a world view and all of its world views are consistent. To simplify our presentation, in the rest of this paper, we will simply call an epistemic logic program program. By V(P) we denote the set of all collections of belief sets in which P is satisfied. We also denote the set of all world views of P as A(P). Clearly A(P) <:;:; V(P).

3.2 Minimal Change on World View Updates

Let W and W1 be two belief sets. We define Diff ( W, W1) tobetheseti(W\ W1)U(Wt \ W)l'· Ourmethodofup­ dating world views shares a similar spirit of traditional model based update [Winslett, 1988] by defining a closeness relation between collections of belief sets, and after the update, there­ sulting collection of belief sets should be as close as possible to the original one.

Definition 1 (Closeness) Let A, A1 and A2 be three collec­ tions of belief sets. We say At is as close to A as A 2. denoted as A1 <A A2, ijjfor any W E A and W2 E A2. there exists a wl E Al such that Diff( w) Wt) <:;:; Diff( w) W2)· We denote A1 <A A2 if At :=;A A2 and A2 i:.A A1 .

Proposition 1 :=;A is a partial ordering.

Definition 2 (Updating world views) Let A be a world view of some program and P a program. A collection of belief sets A' is a possible result of updating A by P, if

1. A' f= P (i.e. A' E V(P)); and

1. there does not exist another collection of belief sets A" satisfying condition 1 and A" <A A'.

We use Res(A, P) to denote the set of all possible collections of belief sets after updating A by P .

Example 1 Consider two epistemic logic programs Pt and P2 where

Pt: a +--, ·b +-- not c, c +-- not ·b, and P2 : b or c +-- K a,

Clearly, P 1 has one world view At = { {a, ·b}, {a, c }}. Updating A1 by P2, according to Definition 2, we obtain a unique result A' = { {a, b} , {a, c}}. Note that neither A"= {{a ,c}} norA* = {{a , ·b,c} , {a,c}}isaresult of updating A by P2. Although A" f= 'P2 and A* f= P2, we have A' <A, A" and A' <A, A* according to Definition I.

'For a set of ground literals W, I WI = {IIIII E W} and here 111 is l's corresponding propositional atom, i.e. 111 = a if 1 is a or ...... a.

·

Proposition 2 Given a collection of belief sets A and a program P. Then Res(A, P) = Min(V(P), :=;A). where Min(V(P) , :=;A) is the subset ofV(P) containing all mini­ mal elements with respect to ordering :=;A.

3.3 Maximal Coherence and Resulting Programs

As discussed earlier, during the second stage of an update procedure, we need to derive a resulting program which should contain the maximal consistent information repre­ sented by the initial program in syntactic forms. This is achieved by introducing the concept of coherence. Let M = (A, W) be an epistemic model and r a rule of the form (1) and M f= r. We define S(M , H(r)) = {l I l E H(r) n W and M F= B(r)}. Intuitively, if M f= B(r), then S(M, H(r)) presents all literals occur­ ring in H ( r) that are true in W. For example, let M = ( {{a , b}, {a, c}, {a, b, c}}, {a, b, c}) and r : b or c +-- J( a, then S ( M, H ( r)) = { b, c}. In the case M ~ B ( r), we have S(M, H(r)) = 0.

Definition 3 (Subsumption) Given two collections of belief sets At and A2 and a program P where A1 E V(P). A2 is subsumed by A1 with respect toP, denoted as A 2 <:;:;p A 1, iff A2 E V(P) and for each M2 E ind(A2) there exists a M 1 E ind(A1 ) such that for each r E 'P. S(M2, H(r)) <:;:; S(M1, H(r2)) .

Given At f= P, if A 2 is subsumed by A1 with respect to P, then each rule r in P is also satisfied in A2 without increasing the satisfied literals of H ( r) in epistemic models induced from A 2 . For instance, let P = { r : a or b +-- K c}, A1 = {{a,b,c,},{b,c, d}}andA2 = {{a,c},{b,c,e}}, then A2 <:;:;p A1. Note that belief set {a , c} in A 2 only con­ tains one literal of H ( r) where belief set {a, b, c} in A 1 con­ tains both literals of H ( r).

Definition 4 (Coherence) Let P and P' be two programs and A E V('P). P' is coherent with P with respect to A if for each A' E Res (A, P'), A' is consistent and A' <:;:;p A .

The intuitive meaning of coherence is explained as follows. Given a collection of belief sets A and programs P and P' where A f= P. Updating A by P' will change A to other collections of belief sets that satisfy P'. Coherence ensures that such changes do not violate the satisfaction of P, i.e. for each A' E Res (A , P') A' f= P. Furthermore, it also ensures that the result A' is not larger than A in terms of P's satisfaction. Note that coherence only associates with consistent programs.

Proposition 3 Let P and P' be two programs and A E V ('P). IfP' is coherent with P with respect to A, then PUP' is a consistent program.

Proof: Since P' is coherent with P with respect to A, it means that for each A' E Res(A, P') A' is consistent, A' F= P' and A' f= P. It also follows A' E V(P UP'). From Lemma 1 in section 5, we know that P U P' is a consistent program. ·

Now the resulting program can be specified by the follow­ ing definition .

Definition 5 (Resulting programs) Let P1 and P2 be two programs and A1 E A(P!). A program P' is a possible resulting program after updating P1 by P 2, ijfP' =Pi UP2, where Pi is a maximal subset ofP1 such that for each A' E Res(A 1, P 2) Pi is coherent with P 2 with respect to A'.

Example 2 Example 1 continued. Note that A1 {{a, -.b} , {a, c}} is the unique world view of P 1. After up­ datingA1 byP2, we have Res (A1 , P 2) = { {{a, b }, {a , c}}} as shown in Example 1. Then it can be verified that {a t-} is the only maximal subset of P 1 that is coherent with P 2 with respect to { {a , b}, {a, c}}. Therefore, from Definition 5, we have

from which, we conclude that P' has a unique world view {{a, b} , {a ,c}}. ·

4 Handling Update Sequences

In this section, we extend our previous formulation to han­ dle update sequences where more than two programs are involved. Let P 1 , · · ·, Pk be consistent programs. P = (P1 , · · ·, Pk) is called an update sequence. Informally per­ forming this update sequence means that program P 1 is se­ quentially updated by P2, · · ·, by Pk. From our intuition, during this process we would like to assign Pj a higher prior­ ity of persistence than P; where j > i since Pj represents the agent's newly received knowledge comparing toP;. There­ fore, after the performance of this update sequence, it is de­ sirable to achieve a result which maximally contains infor­ mation represented by Pk, Pk-l, · · ·, P 1 with progressively decreasing priorities. Similarly to our previous update for­ mulation, we will formalize this principle from both seman­ tic and syntactic considerations. We first illustrate our idea by the following example.

Example 3 Consider an update sequence P = (P1, P 2, P3), where

To perform update sequence P, we first update P 1 by P 2, which, according to the approach developed earlier, will gen­ erate two resulting programs: P' = { r1, r3} and P" = { r2 , r3}. Now we consider to update P' and P" by P3 re­ spectively. However, this time, we cannot simply apply our previous update approach because both P' and P" contain rules from P1 and P 2 where rules from P 2 should have a higher priority to be maintained during the change. For in­ stance, consider the update of P' by P3 . P' has one world view A' = { {a , b}} . Then updating A' by P3 will generate a result A" = { {-.a , b} , {a, -.b}} . Clearly, both { r1} and { r3 } are the maximal subsets of P' that are coherent with P3 with respect to A". However, as we discussed above, we should only have a final resulting program { r3} U P3 because r3 has a higher priority than r1 to be persistent during the update. Updating P" by P3 , on the other hand, will result in a result­ ing program P" U P3 as there is no any contradiction between P" and P3 . ·

Let P = (P1, · · ·, Pk) be an update sequence and P' a subsetofP1 U ···UPk. WedenoteP'[P,i] = {r I r E P; n P'} (1 :S i :S k) . Note that P'[P, i] ~ P ;. Now the following two definitions formalize our idea of performing update sequences as discussed above.

Definition 6 (Preferred subsets) Let P = (P1 , · · ·, Pk) be an update sequence and P' and P" two subsets ofP1 U · · · U Pk. We say that P' is more preferred than P" with respect toP, denoted asP' « P P", iff(i)P" C P'; or(ii)there exist some i and j where 1 ::; i < j ::; k such that for all[ (j ::; I ::; k), P"[P, l] ~ P'[P, l],for some l' (j ::; l' ::; k) P"[P , /'] c P'[P, /'], andP'[P, i] c P"[P , i].

Definition 7 (Update selection functions) Let lP' be the col­ lection of all epistemic logic programs. For each i 2: 1, we define IT; to be a i-ary update selection function ifii ; is a mapping:

where the following conditions hold:

1. if i = 1, then for any update sequence P = (P!), II1(P) ={PI};
2. if i = 2, then for any update sequence P = (P1 , P2), TI2(P) = {P' I where P' is a resulting program as de­ scribed in Definition 5};
3. if i = k and k > 2, then for any update sequence P = (P1 , · · ·, Pk), P E Ilk(P) iffP = P* U Pk , where P* is obtained as follows:
4. (a) let P1 = (P1, · · ·, Pk-1) andP' E Ilk_l(Pl) ;
5. (b) let A be a world view ofP', and P* is a maximal subset ofP' such that for all A' E Res(A, Pk) P* is coherent with Pk with respect to A';
6. (c) there does not exist another maximal subset pt of P' that satisfies condition (b) andPt « P, P* 2 .

Example 4 Consider an irrigation system which has the fol­ lowing general rules to decide whether the plants should be watered:

If there is no evidence showing that it will not be raining next day, then we do not need to water the plants; and

If there is no evidence showing that the soil is dry, then we do not need to water the plants.

It is also assumed that the soil is dry or it will not be raining next day. This scenario can be represented by the following program P1:

2 Note that here we refer to the same world view A of P' as in (b) when we say pt is coherent with Pk with respect to all A' in Res(A, Pk).

P1: r1: ·watering f- not ·to_be_raining, r2: ·watering f- not dry, r3 : dry or ·to_be_raining f- .

P1 has one world view:

from which it is concluded that we do not need to water the plants. However, from a conservative viewpoint for plants' growth, this result is rather optimistic because r3 does not represent an exclusive disjunctive information. Therefore, we consider to update P1 by P2:

P2: r 4 : watering f- -,J<:-,dry, M·to_be_raining, r 5 : ·watering f- ·dry,

r6: -,watering f- to_be_raining,

which says that if it is not known that the soil is dry and it may be believed that it will not be raining next day, then we water the plants; and we do not need to water the plants if the soil is not dry or it will be raining next day. After a period of time, suppose new information is further received that is represented by P3 as follows :

P3:

r7: -,dry or to_be_raining f-.

Now we consider the update sequence P = (P1 , P2, P3). Let P 1 (P1 , P2). Then according to Definition 7, We have I12 (Pl) {P'}, where P' { r3 , r4 , r 5 , r6} (note that rules r 1 and r2 are removed from the initial program P 1). P' has one world view { {dry, watering}, { -,to_be_raining, watering}}, from which it is concluded that we need to water the plants. Finally, we have a unique resulting program I13 (P) = {P"} where P" = { r4 , r5 , r6 , 1"7}, from which it is concluded that we no longer need to water the plants, i.e. P" f= ·watering. ·

5 Semantic Characterizations

In this section, we study important semantic properties of our approach for epistemic logic program updates. Let P = (P1 , · · · , Pk) be an update sequence and P a program, by (P, P) we denote the update sequence (P1 , · · ·, Pk, P). By Body(P) and Head(P) we denote the sets of all objective literals occurring in the bodies and heads of rules in P re­ spectively3. To simplify our presentation, we also use no­ tion 7rk (P) to denote an arbitrary resulting program in ilk (P) whenever there is no confusion in the context. For instance, by 1rk(P) F= L, we mean that for any P E llk(P), P F= L; and by 7rk(P) = 7rk+1(P, P), we mean that any resulting program in ilk (P) is also a resulting program in llk+l (P, P), and vice versa, etc ..

Lemma 1 A program P is consistent iffV (P) # 0 and there is a consistent collection of belief sets in V(P).

Theorem 1 Let P be an update sequence with a length of k and P a program. Then the following properties hold:

3 Note that Body(P) is different from B(r) while Head(P) = u,·EP H( r ). See section 3.1 for definitions on B( r) and H ( r ) .

1. 7rk(P) is a consistent program (consistency property);

The following theorem provides a sufficient condition under which the computation of a (k + I)-length update se­ quence can be reduced to the computation on a k-length up­ date sequence.

Theorem 2 (Reduction property) Let P be an update se­ quence with a length of k, and P and P' two programs. /fV(7rk(P)) ~ V(P) ~ V(P'), then 7rk+2(P, P, P') = 7rk+l (P, PUP').

Now we investigate two specific properties called persis­ tence and preservation for epistemic logic program updates. Informally, the persistence property ensures that if a literal is derivable from a program, then after updating this program, this literal is still derivable from the resulting program. The preservation property, on the other hand, says that if a literal is derivable from a program, then updating other program by this program will still preserve this literal's derivability from the resulting program. While the persistence property is usu­ ally not valid for classical belief revision and update due to their nonmonotonicity, the preservation property, neverthe­ less, indeed holds for classical belief revision and update. It is not difficult to observe that generally none of these two prop­ erties holds for extended logic program updates or epistemic logic program updates. However, it is always worthwhile to explore their restricted forms because under certain con­ ditions, these properties may significantly simplify the com­ putation of a query to the update result. We first present the following lemma.

Lemma 2 Let P be a program and La ground literal. Sup­ pose P' is a subset ofP such that P' f= Land Body(P') n Head(P \ P') = 0. Then P F= L.

Proof: (Proof Sketch) The proof for this lemma is rather technical and involves the proof of a result so called splitting theorem for epistemic logic programs which inherits a similar feature of the splitting theorem for extended logic programs [Lifschitz and Turner, 1994]. Basically, the splitting theorem for epistemic logic programs states that if Body(P') n Head(P \ P') = 0 (here P is a consistent program), then for any world view A of P and every belief set W in A, there exists a belief set W' that is in some world view of P' such that W' ~ W. Due to a space limit, here we have to omit the formal proof of the splitting theorem of epistemic logic programs [Zhang, 2003] 4 . Based on the splitting theorem, this lemma is proved as follows. Consider program P'. Since P' F= L, for each world view A' of P', A' F= L. That is, for each W' E A', L E W'. Suppose P ~ L. Then there exists a world view A of P such that A ~ L. Then there must be some belief set W E A such that L rf. W. However, since Body(P') n Head(P \ P') = 0, from the splitting theorem, there exists a world view A · of P' such that for some w· E A· we have w· c W. Since A* ~ L, it follows L E W* and then L E w-:- Obviously this contradicts the fact L tf. W. So we have P ~ L. ·

4 0ne referee pointed that as a general extension of Lifschitz and Turner's result, Watson also proposed a splitting set theorem for epistemic logic programs [Watson, 2000]. It appears that our split­ ting theorem has a different feature from Watson's though the later may be also used for this proof.

From Lemma 2, we can prove the following two properties.

Theorem 3 (Persistence property) Let P be an update se­ quence with a length of k, P a program, and L a ground literal. Suppose 1I'k(P) ~ L. Then 1rk+!(P, P) ~ L if V(1rk(P)) ~ V(P) and Body(1rk(P)) n Head(P) = 0.

Proof: Since V(1rk(P)) ~ V(P), from Theorem 1, we have 1I'k+l(P,P) = 1I'k(P) UP. On the other hand, from condition Body(1rk(P)) n Head(P) = 0 and Lemma 2, it follows 1I'k+l (P, P) ~ L. ·

Theorem 4 (Preservation property) Let P = (P1 , · · ·, Pk) be an update sequence with a length of k, P a program, and La ground literal. Suppose P ~ L. Then 1rk+1 (P, P) ~ L if Head(U7=1 Pi) n Body(P) = 0.

Proof: Clearly P ~ 1I'k+J (P, P). On the other hand, we have 1I'k+l (P, P) = p· u P, where p· ~ U7= 1 P; and satisfies conditions (b) and (c) in Definition 7. So we have Head(P·) n Body(P) = 0. Then directly from Lemma 2, we have 1I'k+l (P, P) ~ L. ·

6 Concluding Remarks

In this paper, we proposed a formulation for epistemic logic program updates. Our update approach was developed based on the principle of minimal change and maximal coherence. By using our approach, not only a minimal change semantics is embedded into the underlying update procedure, but also a maximal syntactic coherence is achieved after the update. We also investigated important semantic properties of our update approach. This work can be viewed as a further development on knowledge update [Baral and Zhang, 2001]. Although all current approaches of logic program updates have their own features, it is not clear yet whether they are suitable to handle epistemic logic program updates. For instance, in [Zhang, 2003] we demonstrated that a straightforward extension of Alferes et al's approach [Alferes and et al, 2000] or Eiter et aJ.'s approach [Eiter and et al, 2002] to epistemic logic pro­ gram updates may generate incorrect solutions, while the pro­ posed generic framework in [Eiter and et al, 2001] seems not applicable to our case either. On the other hand, a syntax­ based approach, e.g. [Sakama and Inoue, 1999], cannot char­ acterize the semantics of epistemic logic program updates, and some approaches, e.g. [Eiter and eta!, 2002], do not obey the consistency requirement that is believed to be one of the essential requirements for any revision and update systems [Katsuno and Mendelzon, 1991].

Several issues remain open for our future research. First, in our update approach, we did not consider the issue of prefer­ ence over different resulting programs. In practice, it is possi­ ble that one resulting program is more preferred than the other in terms of the domain semantics. This problem involves con­ flict resolution which is a difficult issue in logic program up­ dates [Zhang and Foo, 1998]. Second, as world view semantics can be viewed as a generalization of answer set se­ mantics, our update approach is also applicable for extended logic program updates. Therefore, it is important to charac­ terize similarities and differences between our approach and other logic program update approaches from a semantic view­ point. Finally, since epistemic logic programs have been used as a main component in knowledge based action theories, e.g. [Lobo et al., 2001 ], we expect that these theories may be sig­ nificantly enhanced for representing interactions between ac­ tions and knowledge by applying our update approach.