Abductive Framework for Nonmonotonic Theory Change

1 Introduction

A lot of theories for belief change have been proposed in AI and related fields. At abstract and philosophical lev­ els, the belief dynamics have been studied as rationality postulates to be satisfied by belief sets (e.g., [Alchourfon et al., 1985; Katsuno and Mendelzon, 1991b)). In the field of AI and databases, various researchers have pro­ posed revision, contraction, and update methods of data and knowledge bases. On the AI side, revision and up­ date methods mainly cope with knowledge bases which consist of first-order theories. According to [Winslett, 1990], those methods are classified into formula-based and model-based approaches. In the formula-based up­ date such as [Fagin et al., 1983], the units of change are formulas, and the syntax of formulas in a theory influ­ ences the result of update. In the model-based update, on the other hand, update does not care about formulas in a theory but cares about changes of models during update. In both approaches, however, the underlying language for describing beliefs is a monotonic (mainly propositional) logic. In fact, not much is known about update of nonmonotonic theories. Note that this fact should not be confused with the well-known fact that the process of belief change itself is nonmonotonic even when our beliefs are represented in monotonic logic [Makinson and Gardenfors, 1989].

Using nonmonotonic logics, one expects that some previously derived formulas are automatically retracted when our belief set changes. However, the present non­ monotonic formalisms are not strong enough to revise

Chiaki Sakama

Department of Computer and Communication Science Wakayama University

930 Sakaedani, Wakayama 640, Japan

sakama~center.wakayama-u.ac.jp

even a simple belief set. For instance, let us consider an example (due to [Konolige, 1992)) of autoepistemic logic, where an agent's belief is given by the theory K0 :

The formula in K0 can be read as: if she does not believe that "the repairman has arrived (p)" then "the copier must be OK (q)". Suppose further that she then found that "the copier is broken (·q)". Then her beliefs are revised as

The theory K1 now does not have any stable expansion, because while Bp is derivable p is not. We thus need a revision method for nonmonotonic theories that can retract previously derived formulas automatically.

In the context of databases, on the other side, up­ date of deductive databases is usually captured as the view update problem [Abiteboul, 1988]. Namely, in a deductive database, update on virtual relations in an in­ tensional database has to be translated into update on real facts in an extensional database. It is also known that database update is closely related to abduction in AI. Kakas and Mancarella [1990] present that view up­ date in deductive databases is realized by an abductive procedure of logic programming by considering update requests as observations and extensional relations as ab­ ductive hypotheses. This close relationship between ab­ duction and update, however, need not be limited within the area of deductive databases. We consider that ab­ duction can play a fundamental role in a wide class of AI and database problems. That is, abductive methods would contribute to better understanding of various be­ lief change semantics as well as better implementation of them.

In this paper, we characterize update of nonmonotonic theories through abduction. For this purpose, we first extend the abductive framework to autoepistemic the­ ories. The notions of negative explanations and anti­ explanations are introduced to account for observations in nonmonotonic setting. Then we define autoepistemic update through the extended abductive framework. It is . shown that autoepistemic update can provide a uniform framework for various update semantics. In particular, update of first-order theories, view update of deductive databases, and contradiction removal of nonmonotonic theories are expressed as special cases of the new update semantics.

The rest of this paper is organized as follows. The next section reviews autoepistemic logic. Section 3 defines a new abductive framework for autoepistemic logic. The abductive framework is applied to formalize an update semantics for autoepistemic theories in Section 4. Vari­ ous forms of update semantics are expressed in terms of autoepistemic update. Section 5 discusses related work, and Section 6 concludes the paper.

2 Autoepistemic Theory

We briefly review autoepistemic logic by Moore [1985]. A utoepistemic logic is obtained by extending a first-order language .C0 with the modal operator B. A formula in autoepistemic logic is called objective if it does not con­ tain the modal operator B; otherwise it is subjective. Intuitively, the formula BF is read as "F is believed". By an autoepistemic theory, or simply a theory, we mean a set of formulas in autoepistemic logic. In this paper, we allow open variables, and each formula with variables stands for the set of its ground instances. This means that an autoepistemic theory is essentially equivalent to a set of countably many propositional formulas in au­ toepistemic logic.

A theory is stable if it is closed under the logical and introspective consequences. Namely, a stable set T sat­ isfies the conditions: (i) T = cons(T), where cons(T) denotes the set of logical consequences (in the sense of classical first-order logic) ofT; (ii) if cp E T then Bcp E T, and (iii) if cp ¢ T then -,Bcp E T. The meaning of each.autoepistemic theory is usually characterized by the following stable set that is expanded from the theory: Given an autoepistemic theory K, a set T is a stable expansion of K iff it satisfies that

Note that an autoepistemic theory may have none, one, or multiple stable expansions. We say that an autoepis­ temic theory K is consistent if it has a consistent stable expansion; otherwise K is inconsistent.

It is well known that for each set l: of objective formu­ las, there is a unique stable set E(l:) containing l: such that the objective formulas in E(l:) are exactly the same as those in cans(l:). Moreover, if a theory K contains only objective formulas, then E(K) is a unique stable expansion of K [Moore, 1985].

By K f= F, we mean that every stable expansion of an autoepistemic theory K contains a formula F. For exam­ ple, { -,Bp ::> q} f= q and { -,Bp ::> q, -,Bq ::> p} ~ q. Thus K ~ F denotes that there is a stable expansiOn T of K such that T does not include F. This skeptical reading of the entailment relation in autoepistemic logic generalizes the meaning of the classical entailment rela­ tion.1 Namely, for a first-order theory l: and a first-order formula F, it holds that l: f= F iff FE E(l:).

1 We can give an alternative, credulous meaning to K f= F: that is there is a stable expansion of K containing F. Note that ir: this weaker reading, again the notion is a generaliza­ tion of the first-order entailment relation since any first-order theory has the unique stable expansion.

Autoepistemic logic and the notion of stable expan­ sions have a close relationship with the answer set se­ mantics [Gelfand and Lifschitz, 1991] for logic program­ ming with negation as failure and classical negation (see [Lifschitz and Schwarz, 1993; Inoue and Sakama, 1994], for instance). Hence, the theory of belief update devel­ oped in this paper can directly be applied to the update problem for such extended logic programs.

3 New Form of Abduction

Abduction is one of the three fundamental modes of rea­ soning characterized by C. S. Peirce, the others being deduction and induction. The most popular formaliza­ tion of abduction in AI defines an explanation as a set of hypotheses which, together with the background theory, logically entails the given observations. A traditional, logical framework of abduction is defined as follows. Let l: (background theory) and r (hypotheses) be two sets of first-order formulas. Given a formula F (observation), a set E of ground instances of elements from r is an explanation of F with respect to ( l:, r) if

1. l: U E is consistent.

An explanation E is minimal if no E' C E is an expla­ nation of F. Suppose, for example, that we are given the background theory l:l and the hypotheses r 1 as

Here, the hypothesis -,ab( x) means that for any ground term t, -,ab(t) can be hypothesized. In other words, a hypothesis containing variables is shorthand for the set of its ground instances. In this case, a minimal explana­ tion of the observation flies(tweety) is {-,ab(tweety)}. As a result of assimilating the observation flies(tweety), our background theory is changed as

Suppose we later find that tweety lasts his flying abil­ ity for some reasons (e.g., injured, fatted, etc). In this case, -,flies(tweety) should be explained by assuming ab(tweety) instead of -,ab(tweety). Retracting the previ­ ous assumption -,ab(tweety) is vital, since flies(tweety) should not be explained any more. To formalize such a situation, we extend the above abductive framework in the following three respects:

1. The background theory l: and the candidate hy­ potheses r can be autoepistemic theories. Thus, the belief operator B may appear in l: or r.
2. Hypotheses can not only be added to the theory l: but also be discarded from l: to explain obser­ vations. When l: \ E f= F for some set E of hy­ potheses, we call E a negative explanation of F. An ordinary explanation E such that l: U E f= F is now called a positive explanation.

1. The notion of explanation is extended to unexplain observations. When L: U E ~ F (resp. L: \ E ~F) for some set E of hypotheses, we call E a positive (resp. negative) anti-explanation.

The first extension comes from a demand of common­ sense reasoning that we want to treat a nonmonotonic theory as a background belief theory. An example of such an extension in the literature can be seen in In­ oue's abductive framework [Inoue, 1994] where both L: and r are extended logic programs. Then, it is natural to consider the second extension. This is because the background theory is nonmonotonic, so that contraction of some hypotheses may "revive" the previously derived conclusions. Although it is very natural, as far as the au­ thors know, the notion of negative explanation has never been proposed in the literature. The third extension is useful to talk about unexplained formulas that had been explained before hypotheses changed positively or nega­ tively.

Positive and negative (anti-)explanations are often combined to (un)explain observations. We thus formally define an explanation for our abductive framework by means of a pair of positive and negative explanations.

Definition 3.1 An abductive framework is a pair ( K, r) in which both K and r are autoepistemic theo­ ries. Let F be a formula. A pair (I, 0) is an explanation (resp. anti-explanation) ofF (with respect to (K,r)) if

1. (K U I)\ 0 f= F (resp. (K U I)\ 0 ~F),
2. (K U I)\ 0 is consistent, and
3. both I and 0 consist of instances of elements from r.

An (anti-)explanation (I, 0) of F is minimal if for any explanation (I', 0') ofF, I' ~ I and 0' ~ 0 imply that I' = I and 0' = 0.

Intuitively, a minimal (anti-)explanation (I, 0) offers a tradeoff between minimal reduction 0 of the background theory K and minimal augmentation with the newly added hypotheses I from r. In this sense, each mini­ mal (anti-)explanation accomplishes a minimal change of the theory K with respect to r. Obviously, this def­ inition of (minimal) explanations reduces to the tradi­ tional one when K is a first-order theory and 0 for each explanation (I, 0) is empty. For the bird ex­ ample above, a minimal explanation of flies(tweety) with respect to (L:1,rl) is ({...,ab(tweety)},0). Also, a minimal anti-explanation of flies(tweety) with respect to ( L:2' r 1 ) is ( 0, { -,ab( tweety)}), and a minimal ex­ planation of -,flies(tweety) with respect to ( L:2, rl) is ({ab(tweety)},{-,ab(tweety)}). Notice that an anti­ explanation ofF is not an explanation of ...,F, and that anti-explanations cannot be represented by explanations in general.

Example 3.2 Let us consider the autoepistemic theo­ ries introduced in Section 1:

with the hypotheses ro = {p}. The (minimal) anti­ explanation of q with respect to (K0,r0 ) is ({p},0), which is also the (minimal) explanation of -,q with re­ spect to (K1, ro).

In the next section, we define an update semantics of autoepistemic theories in terms of the extended abduc­ tive framework.

4 Autoepistemic Update

A formula in autoepistemic logic is called a dynamic be­ lief if it is subject to change in an autoepistemic theory. We denote as r the set of all dynamic beliefs in the language. In this setting, an autoepistemic theory K is divided into two parts based on this meta-theoretical partition of beliefs: (i) the invariant beliefs Kr and (ii) the dynamic beliefs KD. Namely, K can be written as

The notion of such a partition (with possibly more than two levels) of beliefs is commonly used for update se­ mantics in the literature: for example, tagged sentences [Fagin et al., 1983], the notion of (un}protected formu­ las [Winslett, 1988], integrity constraints [Katsuno and Mendelzon, 1991a], and priority classes [Nebel, 1991]. Thus update to a theory should be translated into up­ date on dynamic beliefs that an agent can actually change.

We define update as a function u between autoepis­ temic theories. 2 Given an initial theory K, we call K' = u(K) an updated theory. Each update considered in this paper is either an insertion or a deletion of a for­ mula in autoepistemic logic. Now, autoepistemic update is defined as follows.

Definition 4.1 Given a theory K, the autoepistemic update is defined in terms of the abductive framework as follows.

1. If update is an insertion of a formula F into K, then u(K) = (K U I)\ 0 where (I, 0) is a minimal explanation ofF with respect to ( K, r ).
2. If update is a deletion of a formula F from K, then u(K) = (K U I) \ 0 where (I, 0) is a minimal anti­ explanation ofF with respect to ( K, r ).

If there is no such (anti-)explanation, update is impossi­ ble.

Example 4.2 (cont. from Example 3.2) The deletion of q from the theory Ko = { -,Bp :::) q} whose dy­ namic beliefs are ro = {p} is accomplished by the anti­ explanation ({p},0) of q with respect to (K0 ,r0 ).

Example 4.3 Consider the theory

In this theory, the insertion of p is impossible. In fact, there is no pair (I, 0) that accomplishes the insertion.

The proposed autoepistemic update is general enough to provide a unified framework for various update se­ mantics. In the following, we present the relationships between autoepistemic update and those other seman­ tics.

2 According to [del Val and Shoham, 1994], revision is con­ sidered as update of mental states. With this regard, update of autoepistemic theories is also considered as revision of be­ lief states. So we do not distinguish revision and update unlike [Katsuno and Mendelzon, 1991b], and use the terms interchangeably.

4.1 First-Order Update

First-order theory update is a special case of autoepis­ temic update when K and F are first-order theories in Definition 4.1. Some work have been done for updatin& first-order theories. Among them, Fagin et al.'s [1983] semantics for updating first-order theories is one of the best-known frameworks in the field. In this subsection, we address a method of realizing their update semantics in our abductive framework.

Definition 4.4 Let E be a first-order theory and u a formula. A theory up(E) accomplishes a FUV insertion of u into E if

1. {u} ~ up(E) ~ E U {u},
2. up(E) is consistent, and
3. there is no set uj;.(E) satisfyip.g the above two and up(E) C uj;.(E).

Note that in a FUV insertion an inserted formula u is always included in the updated theory up(E), 3 and any formula in E is considered as a retractable formula. Thus the updated theory is defined as a union of the inserted formula u and a maximal subset of the original formulas E that is consistent with u. This situation is realized in our abductive framework by inserting u to the original theory and changing any formula other than u minimally to make the updated theory consistent.

Theorem 4.5 Given a first-order theory E and a for­ mula u, up(E) accomplishes a FUV insertion of u into E iff up(E) = (E U { u}) \ 0 where (0, 0) is a minimal explanation of u with respect to ( E U { u}, E \ { u} ) .

Proof: Suppose that up(E) accomplishes a FUV inser­ tion of u into E. up(E) can be written as (E U { u}) \0, where u ¢ 0, because u E up(E). Then, (Eu {u}) \0 f= u and (E U { u}) \0 is consistent. Therefore, 0 is a nega­ tive explanation of u with respect to ( E U { u}, E \ { u} ) . Suppose to the contrary that (0, 0) is not a minimal ex­ planation of u. Then, there exists an explanation (I', 0') of u such that I'~ 0 and O' ~ 0, but I' :f:. 0 or 0' :f:. 0. The last condition implies that O' C 0. In this case, (E U { u}) \ O' f= u because of the monotonicity and O' C 0. Likewise, (E U { u}) \ 0' is consistent. Then, uj;.(E) = (E U { u}) \ O' satisfies the condition 1 and 2 of Definition 4.4, and up(E) C uj;.(E) holds. This contra­ dicts the fact that up(E) accomplishes a FUV insertion of u into E. Hence, (0, 0) is a minimal explanation of u.

Conversely, suppose that (0, 0) is a minimal explana­ tion of u with respect to ( E U { u }, E \ { u} ). Obviously, {u} ~ [(E u {u}) \OJ ~ E U {u}, and (E U {u}) \0 is consistent. Since (0, 0) is a minimal explanation of u, no (0, O') such that 0' C 0 is an explanation of u. Therefore, up(E) = (E U {u}) \0 accomplishes a FUV insertion of u into E. D

Fagin et al. 's deletion is not defined as the counterpart of their insertion, because formulas to be deleted may be logical consequences of the theory.

3 As discussed in[Winslett, 1990, Section 2.1.2), adding an insertion formula a to E is not always desirable. With this regard, our update method by Definition 4.1 can accomplish an insertion in a more flexible manner.

Definition 4.6 Let E be a first-order theory and u a non-tautological formula. A theory up(E) accomplishes a FUV deletion of u from E if

1. up(E) ~ E,
2. up(E) ~ u, and
3. there is no set uj;.(E) satisfying the above two and up(E) C uj;.(E).

In the above definition an updated theory is defined as a maximal subset S of the theory E such that u does not follow from S. This situation is also expressed in our abductive framework by minimizing a set of discarded hypotheses from E to unexplain u .

Theorem 4.7 A theory up(E) accomplishes a FUV deletion of a formula u from the theory E iff up(E) = E \ 0 where (0, 0) is a minimal anti-explanation of u with respect to ( E, E).

Proof: Suppose that up(E) accomplishes a FUV dele­ tion of u from E. up(E) can be written as E \ 0 where 0 ~ E. By definition, E \ 0 ~ u, and hence E \ 0 is consistent. Therefore, 0 is a negative anti-explanation of u with respect to ( E, E). Suppose to the contrary that (0, 0) is not a minimal anti-explanation of a. Then, there exists an anti-explanation (I', 0') of u such that 0' C 0. Put uj;.(E) = E\0'. By definition, uj;.(E) ~ u . Obviously, uj;.(E) ~ E, but up(E) C uj;.(E). This con­ tradicts the fact that up(E) accomplishes a FUV dele­ tion of u from E.

Conversely, suppose that (0, 0) is a minimal anti­ explanation of u with respect to ( E, E). Obviously, (E \ 0) ~ E. By definition, E \ 0 ~ a. Since (0, 0) is a minimal anti-explanation of a, no (0, 0') such that O' C 0 is an anti-explanation of u. Therefore, up(E) = E \ 0 accomplishes a FUV deletion of u from E. D

4.2 View Update of Databases

In the context of databases, update is usually captured as the view update problem, in which update on intensional facts is translated into update on extensional facts in a database. Here, we characterize view update in our abductive framework.

A database D is a finite set of rules of the form:

where A and Ai's are atoms (A is possibly empty) and not denotes the negation-as-failure operator in logic pro­ gramming. When n = 0, the rule is also written just as A by omiting t-. Each rule of the above form is regarded as the autoepistemic formula

where A = false when A is empty in the rule.

Given a database D, £8 is the pre-specified set of atoms from the language of D called the extensional base. Then view update of a database is defined as follows.

Definition 4.8 Let D be a database and A a ground atom. An insertion of A into D (resp. deletion of A from D) is accomplished by an updated database u(D) = (D U I)\ 0, where I, 0 ~ £8, if

1. u(D) f= A (resp. u(D) ~ A),
2. u(D) is consistent,
3. there is no u'(D) = (Dui') \ 0', where I', 0' ~ £8, satisfying the above two and LlD,u'(D) C Lln,u(D)· where Lln1 ,D2 = (D1 \ D2) U (D2 \ D1).

Note that the condition 3 in the above definition says that update of D is performed minimally on £B. The view update problem of deductive databases is charac­ terized by abduction as follows.

Lemma 4.9 Let u(D) = (D U I) \ 0 be an updated database that accomplishes an insertion/deletion of an atom A into/from D as in Definition 4.8. Then,

1. In o = 0,

2. In D = 0, and

3. O~D.

Theorem 4.10 Given a database D and a ground atom A, a database u(D) accomplishes an insertion (resp. deletion} of A into/from D iff A has a minimal expla­ nation (resp. anti-explanation} (I, 0) of A with respect to (D,£8).

Proof: We consider the insertion of A since the case of the deletion is similar. Suppose that u(D) = (D UI) \0, where I, 0 ~ £8, accomplishes an insertion of A into D. By definition, (i) (D U I) \ 0 f= A, (ii) (D U I) \ 0 is consistent, and (iii) no other (I', 0') satisfies (i), (ii) and

By (i) and (ii), (I, 0) is an explanation of A with respect to (D,£8). The last relation in the condition (iii) is equivalent to

Here, D n 0 = 0, D u 0 = D, and I \ D = I by Lemma 4.9. Now, suppose to the contrary that (I, 0) is not a minimal explanation of A. Then there is an explanation (J,P) of A such that J ~I and P ~ 0 but that J f:. I or P f:. 0. Similar to the case of (I, 0), D n P = P, D UP = D, and J \ D = J . On the other hand, J UP C I U 0 . Using these relations, we have the relation that

This contradicts the fact (iii). Therefore, (I, 0) is a min­ imal explanation of A.

The converse direction can also be shown in the same manner. D

The above characterization extends Kakas and Man­ carella's [1990] abductive framework of view update. Moreover, our framework provides a mechanism of view update in a flexible manner. This is because we can freely specify dynamic beliefs r so that atoms from the extensional base are chosen to prefer some intended up­ date and reduce the non-determinism.

Example 4.11 [Manchandra and Warren, 1988) Let D be a database containing the rules:

The first rule says that an employee x has a manager z if x belongs to a department y and the manager of y is z. Suppose that £B is the set of all extensional atoms having the predicate ed or dm. To insert the view em(sam,john), there are two possible ways to accom­ plish the update: to insert dm(publicity,john), or to insert ed(sam, sales). If the company allows to make an employee work in two departments but disallows to let a manager supervise two departments, only the sec­ ond update is permitted. Such a situation is specified in our abductive framework as (D, {ed(x,y)} ). Note that the same effect is achieved in [Manchandra and Warren, 1988) using a framework of dynamic logic programming.

In Definition 4.8, we have assumed that the hypotheses rare £B, while, when needed, we can even change some rules in D by putting them into r.

4.3 Contradiction Removal

An autoepistemic theory often fails to have a consis­ tent stable expansion. For example, the theory K3 = { Bp V p} has no stable expansion, while K4 = { -.p, p} has no consistent stable expansion. Here, we address an application of autoepistemic update to resolve contra­ diction in such theories.

Definition 4.12 Let K be an autoepistemic theory, and C0 the set of objective formulas in the language. The theory r(K) = (K U I)\ 0, where I, 0 ~Co, is called a CR-theory of K if

1. r(K) is consistent, and
2. for any pair (I', 0') such that (K U I') \ O' is con­ sistent, I' ~ I and O' ~ 0 imply that I' = I and 0'=0.

Notice that r(K) =Kif K is consistent.

By definition, the CR-theory r(K) resolves inconsis­ tency in K by minimally introducing or removing appro­ priate objective formulas in the language. In the follow­ ing, we formalize the CR-theory in our abductive frame­ work.

Definition 4.13 Let K and r be autoepistemic theo­ ries. A theory K' = (K u I)\ 0, where I, 0 ~ r, is a most coherent extension of K (with respect tor) if K' is consistent and for any pair (I', O') such that (KUI') \ O' is consistent, I' ~ I and O' ~ 0 imply that I' = I and 0'=0.

It is easy to see that most coherent extensions in Def­ inition 4.13 generalize CR-theories. That is,

Proposition 4.14 Let K and C0 be the same as in Def­ inition 4.12. r(K) is a CR-theory of K iffr(K) is a most coherent extension of K with respect to C0 ·

Note that K is the unique most coherent extension of K iff K is consistent. The next theorem shows that most coherent extensions of K with respect to r in gen­ eral (including CR-theories) can be characterized in the abductive framework ( K, r ).

Theorem 4.15 Let ( K, r ) be any abductive framework. K' = (K u I)\ 0, where I,O ~ r, is a most coherent extension of K with respect tor iff (I, 0) is a minimal anti-explanation of -.F 1\ F with respect to ( K, r), where F is any objective formula.

For the introductory examples, r(K3 ) = { Bp v p, p} with (I, 0) = ( {p}, 0), and r(K4 ) = {p} with (I, 0) = (0, { -.p}) or { -.p} with (I, 0) = (0, {p} ), resolve incon­ sistency of K3 and K4 , respectively. Note that there are some autoepistemic theories that have no CR-theories but have most coherent extensions. For example, the theory

has no CR-theory but has a most coherent extension K 5 ' with (I, 0) = (0, {Bp:::) q} ). However, the restriction on inserted formulas to £ 0 is reasonable. For example, K3 could become consistent by inserting any of p, Bq V p, Br V p, Bq V Br V p, and so on, but in any case the objective formulas of the stable expansion are identical to cons( {p} ).

Morris [1989] provides a method of revising autoepis­ temic theories having no stable expansion. Given an autoepistemic theory K, he defines a stable closure of K as a stable expansion of a minimal augmented the­ ory G = cons(K U I), where I is some set of objective formulas such that K u I has a stable expansion. Note that every autoepistemic theory has a stable closure. In contrast to ours, objective formulas can only be added to resolve inconsistency in his setting. In fact, Mor­ ris's proposal is motivated by dependency-directed back­ tracking in Doyle's truth maintenance system, which re­ solves inconsistency by making some disbelieved propo­ sitions true. Due to this restriction, an autoepistemic theory may have no consistent · stable closure. For ex­ ample, consider the theory K 6 = { -.p, Bp V p} having no stable expansion. The only stable closure of K6 is E(£0 ). On the other hand, our contradiction removal method provides a CR-theory r(K6 ) = { Bp V p, p} with (I ,O) = ({p},{-.p}) where r(K6 ) has the consis­ tent stable expansion E( {p}).

5 Related Work

It is recognized that nonmonotonic theory update is an important future topic in AI and nonmonotonic reason­ ing. However, not much work exist on this topic.

There are some work which relate update semantics to abduction. Boutilier [1994] relates abduction to Kat­ suno and Mendelzon's [1991b] propositional update se­ mantics, but does not consider nonmonotonic theories as background theories. Kakas and Mancarella [1990] characterize update semantics through abduction, while their concern is limited to view update in databases.

Marcus and Subrahmanian [1994] recentl:y established the relationship between Fagin et al.'s [1983] update and default/autoepistemic logic, but they do not discuss the issue of updating nonmonotonic theories. There are some proposals for removing inconsistency from logic programs with negation as failure. Those approaches in [Pereira et al., 1991; Giordano and Martelli, 1990; Witteveen et al., 1994] recover consistency by adding some new formulas, while [Inoue, 1994] discards some beliefs to this effect. In contrast to them, our framework performs update by both inserting and deleting hypothe­ ses based on the extended abductive mechanism.

In the field of theory revision, the AGM-postulates [Al­ chourfon et al., 1985] and their applications to various revision/update systems are thoroug~ly studied by Kat­ suno and Mendelzon [1991a; 1991b]. However, those pos­ tulates are defined for monotonic propositional theories, and not applicable to our nonmonotonic autoepistemic theory in their present forms. Moreover, many of the revision systems are model-based and deal with belief sets, which are closed under logical consequences. By contrast, our approach is formula-based and deals with belief bases, which are not necessarily closed under logical consequences, and is syntax-dependent in its nature. In logic programming and deductive databases, formulas in­ cluded in a theory have their own intended meaning and syntax plays an important role to represent common­ sense knowledge. Nebel [1991] proposes a syntax-based revision system and relates it to some default reason­ ing systems, but he considers only propositional theories and its applications to logic programming and deductive databases are not addressed.

6 Conclusion

We have proposed a new framework for nonmonotonic theory change. This framework is based on a new form of nonmonotonic abduction, which can explain observa­ tions not only by adding some hypotheses to the theory but by retracting some previous hypotheses. With this abductive framework, autoepistemic update was defined for nonmonotonic theory revision and contraction, and then applied to account for view update of deductive databases, first-order theory revision, and contradiction removal for autoepistemic theories. Future work includes devising postulates for nonmonotonic theory change like [Alchourfon et al., 1985; Katsuno and Mendelzon, 1991a; 1991b], developing an efficient mechanism for computing negative and anti- explanations, and investigating con­ nections to update specification languages like [Marek and Truszczynski, 1994] .

Our abductive framework is fairly general and can deal with nonmonotonic theories as background theories. The notions of explanations are extended to allow positive and negative explanans and anti-explanans. An inserted formula that changes the world is an explanandum sen­ tence, and a contracted formula is an anti-explanandum sentence. This extended framework is, we believe, much closer to Peirce's theory of abduction, in which a series of explanatory hypotheses accounting for observations must be revised by experimental testing. The theory of abduction thus relies on the continuous cycle of exper­ iments, observations, hypothesis generation, hypothesis verification, and hypothesis revision.