Sometimes Updates Are Circumscription

1 Introduction

There is a good deal of interest in the philosophical, AI, and database communities in the problem of revis­ ing logical theories (e.g., [Dalal 88, Fagin 83, 86, For­ bus 89, Gii.rdenfors 88ab, ·Ginsberg 86, Oddie 78, Reiter 87, Satoh 88, Weber 86, Winslett 88a]). Section 2 of this paper reviews a model-based semantics for revis­ ing such theories [Winslett 88b]. This paper will not dwell on the uses for this semantics; rather, in Section 4 we will show that circumscription, a formal approach to common-sense reasoning, can be used to capture exactly this semantics of theory revision. We conclude with a discussion of the advantages and drawbacks of each ap­ proach.

2 Knowledge Base Updates

This section reviews the model-based method of theory revision presented in [Winslett 88b]. Let T be a theory describing some aspect of the world. Some of the formu­ las in Twill describe data about the current state of the world, data that we will be willing to revise in the face of new information. Other formulas ofT, however, will describe beliefs that we are loathe to retract. For exam­ ple, a formula giving the laws of thermodynamics or the rules of a game is a formula that we will likely be unwill­ ing to retract no matter what new information arrives.

Such formulas are called protected, and the remaining formulas ofT are unprotected.

In applications, even different unprotected beliefs are not held equally strongly. For example, given the infor­ mation that a friend of mine is right now in Alaska, I may be more willing to change my beliefs about her vacation plans in order to explain that fact than to change my belief that she works in Silicon Valley. The predicates of T are assigned an a priori priority ordering, based on our willingness to retract beliefs in atoms over those pred­ icates. More precisely, the predicates of T have been partitioned into nonempty strata numbered 1 through I, such that the priority of minimization of changes in pred­ icates in stratum i is higher than for those in stratum j iff i < j .

Each model M of our theory T is a description of what we believe may be the current state of the world. Given new information about the world in the form of a formula a, we would like to update M by making a true in M, while changing M as little as possible. Fur­ ther, the protected formulas ofT must still be true in the updated version of M. As an additional wrinkle, the priority ordering on predicates means that changes in the truth valuations of atoms over some predicates are considered to be less important than changes in oth­ ers, so that the measure of rninimality of changes must consider exactly which predicates have been changed.

Intuitively, two models with the same universe agree on an formula if they assign it the same truth valuation; otherwise they differ on it. They agree on a predicate P if P has the same extension in both models.

Definition 1. Let a be a formula and M a model. Revise(M, a) is the set of models M' such that

1. M' and M have the same universe and agree on all functions.
2. a and the protected formulas ofT are true in M'.
3. There is no other model M" such that for some 1 ~ i ~ I,
4. M" satisfies (1) and (2);
5. M" and M' agree on all predicates in strata 1 through i- 1; and
6. the differences between M" and M on predi­ cates in stratum i are a proper subset of the differences between M' and M on those pred­ icates .

The models produced by incorporating a formula a into theory T are given by

This definition does not say what formulas should ap­ pear in the revised theory; it simply tells what the mod­ els of that theory should be. A method of computing the result models has been devised and implemented by Forbus for use in reasoning about actions in the domain of qualitative physics [Forbus 89]. His theory revision approach incorporates an additional heuristic to choose between multiple possible result models: comparison of the cardinality of sets of proposed model changes. His implementation is described in [Forbus 89], included in these proceedings.

Example. As a running example, let us build a small description of a room, inspired by Ginsberg (87], and then revise it as we move around the objects in the room. The theory describes a living room containing a clock, a TV, and two air vents in the floor. The clock and TV can be either on the floor or on the vents; only one object fits on a vent at a time. The room is stuffy if both vents are blocked. This scenario is encoded by the formulas below. Protected formulas:

These formulas ensure that (1) an object can only be in one place at a time, (2) only one object can be in a place at a time, (3) if x is on y then x is an object and y is a location, ( 4) the room is stuffy when both vents are blocked, and (5) every object is somewhere. The unprotected formulas ofT:

"On" belongs in priority stratum 1, and "stuffy" in priority stratum 2. Intuitively, this means that whether the room is stuffy should be derived from the locations of objects, rather than the reverse. For simplicity, we will take a Herbrand Universe assumption for this example, so that the only objects are v1, v2, the TV, clock, and floor, and that all these constants are distinct. The only Her brand model ofT, restricted to "on" and "stuffy", is

Suppose the clock is now moved from the floor to v2. If we update T by inserting on( clock, v2), then the follow­ ing result model is produced under Definition 1:

If "stuffy" were also in priority stratum 1, then a model where the TV moved to the floor and the room remained unstuffy would also be admitted. If "stuffy" were in stratum 1 and "on" were in stratum 2, then only this latter model would be produced.

3 Review of Prioritized Circumscription

The goal of circumscription [Etherington 88, McCarthy 87ab, Shoham 87] is to pick out the models of a theory T that are minimal with respect to a particular partial or­ dering. Models are ordered on the basis of the extents of certain of their predicates; in the ordering, models with smaller extents precede models with larger extents. We begin this section with the model-theoretic characteriza­ tion of this intuition, and then present the second-order axiom that also captures the intuition.

Let S be the set of predicates whose extents are to be minimized. Assume that the predicates of S are parti­ tioned into nonempty strata S1, ... , Sz, such that min­ imizing the extents of the predicates in S; is of higher priority than minimizing those in sj whenever i < j. A convenient notation for S is S1 < · · · < S1, as in P1, P2 < P3 < P4, Ps.

Recall that when comparing two models M1 and M2 on the extent of the predicates of stratum S;, we may not care whether M 1 and M 2 agree on a set V; of other predicates, in which case the predicates of V; are said to be "allowed to vary." If s = sl < 0 0 0 < sl gives the predicates to be minimized, then we will assume that when minimizing at stratumS;, predicates of Sj areal­ lowed to vary, for all j > i . Additional predicates not in S may also be allowed to vary when minimizing at S;; V = V; < · · · < Vi is a convenient notation for recording the identity of these additional predicates. Under this notation, every predicate in Vj, for j 2:: i, is allowed to vary when minimizing the predicates of S;. The equality predicate cannot appear in either S or V.

Definition 2 presents the partial order on models that is introduced by this variant of circumscription. (Throughout this paper, "X will be a tuple of terms, of the appropriate arity for the function or predicate taking "X as an argument.)

Definition 2. A model M 1 is preferred to model M2 at the ith stratum (written M 1 <; M2) iff

1. M 1 and M 2 have identical universes;
2. M 1 and M 2 agree on all predicates and functions, except possibly those of S; and V;;
3. For all predicates Pin stratum S;, and for all "X such that P(x) is true in M 1, P(x) is true in M2; and
4. For some predicate P in stratum S; and some "X, P(x) is false in M 1 and true in M 2.

Intuitively, circumscription picks out those models that are minimal with respect to <. M1 is preferred to M2 (written M1 < M2) iff

1. For some 1 :=:; i :=:; l, M 1 <; M 2; and
2. For all1 :=:; j < i, M2 {j M1.

Finally, a model M of T is preferred if no model of T is preferred toM.

The second-order characterization of circumscription says, intuitively speaking, that the predicates of S can­ not be replaced by other predicates such that T is still true and the resulting models are "smaller". For a theory T, Circ(T; S; V) is defined to be the theory

In formula (1), T(S; V) is just T, and T(S'; V') is the theory obtained by replacing all occurrences of the predicates of S and V by their counterparts in S' and V', throughout T . The second-order construct S' is ob­ tained from S by replacing each predicate P that appears in S by a predicate variable P' with the same arity as P. V' is constructed from V in the same manner.

In formula (1), the formulaS'< Sis shorthand for

a proof-theoretic counterpart of our usual minimality cri­ terion.

4 Relation of Updates to Circumscription

This section shows that the model-based semantics of Section 2 for updating logical theories can be expressed using prioritized circumscription.

In recent work, Satoh has (Satoh 88) independently proposed a model-based semantics for theory revision that is similar to ours 1 ; interestingly, Satoh uses second­ order logic to define his semantics. Though he does not present his semantics as a type of circumscription, the form of his definition makes the close ties of his update semantics to circumscription readily apparent.

This paper only considers the case of a single update; the general case, where n updates are applied in suc­ cession to T, uses a different, more complex type of circumscription, and is described in detail in [Winslett 88c). Intuitively, the goal of the circumscription is to minimize the differences between each model M of T and the models in Revise(M, a). The transformation of updates into circumscription is realized by first slightly rewriting the theory to be revised, then defining within the rewritten theory the update to be performed, and finally circumscribing· the changes wrought by that up­ date. These three phases are described below, followed by a proof of correctness for the transformations.

Before rewriting T, we must change the language C underlying T to contain a different set of predicates. The new language £' contains three predicates in place of every non-equality predicate P of the old language: oldP, newP, and changedP, all with the same arity as P . Intuitively, this new language will be used to talk about what was true before and after the update, and also about what changed when the update occurred.

We next create the theory rewrite(T, a) by applying the following four steps to T.

1. Replace all occurrences of non-equality predicates P by oldP, throughout T.

1 The distinction is that Satoh judges the minimality of a set of changes in a model M of T by a global comparison with all other sets of changes in models of T (sharing the same universe and function interpretations) that make the inserted formula true. We judge the minimality of a set of changes by comparison only with other sets of changes in M.

1. Add additional protected formulas: make a second copy of the protected formulas, replacing each oc­ currence of a non-equality predicate oldP by newP. Intuitively, the new protected formulas require that both the old and new states of the world satisfy the protected formulas.
2. Suppose that the update to be performed is the in­ sertion of a formula a. Represent this information by the unprotected formula new( a), which is a with each occurrence of a non-equality predicate P re­ placed by newP.
3. The new predicates changedP are to be true exactly when the truth of an atom of a non-equality predi­ cate Palters in a model when Ct is inserted. In other words, add the new protected formulas

The logical connective ";t" is exclusive or, and is not related to the equality predicate.

Rewrite(T, a) is the theory to be circumscribed. The circumscription policy is to circumscribe the changedP predicates in update stratum order. When minimizing the predicates of a particular stratum, the changedP and newP predicates of equal or higher strata are irrelevant, and therefore should be allowed to vary. More precisely, if the predicates of T are partitioned into l nonempty strata for update purposes, then S = S1 < · · · < Sz, where si = { changedP I p is in stratum i}. Similarly, v = vl < ... <Vi, where Vi = {newP I pis in stratum i}. The circumscription to be performed is given by Circ(rewrite(T, a); S; V) .

Example, continued. Rewrite(T, on( clock, v2)) is the theory

Vxyz. [oldOn(x, y) 1\ oldOn(x, z)] ---+ y = z Vxyz. [oldOn(x, y) 1\ oldOn(z, y))---+ [x = z V y =floor) Vxy. oldOn(x, y) ---+ [(y = v1 V y = v2 V y =floor) 1\ (x = TV V x =clock)) oldStuffy ..-.. 3 xy. oldOn(x, v1) 1\ oldOn(y, v2) Vx3y. oldOn(x, y) V (x =floor) V (x = v1) V (x = v2) Vxyz. [newOn(x, y) 1\ newOn(x, z)] ---+ y = z Vxyz. [newOn(x, y) 1\ newOn(z, y)] --+ [x = z V y =floor) Vxy. newOn(x, y) ---+ [(y = vl V y = v2 V y =floor) 1\ (x = TV V x =clock)] newStuffy ..-.. 3 xy. newOn(x, vl) 1\ newOn(y, v2) Vx3y. newOn(x, y) V (x =floor) V (x = vl) V (x = v2) oldOn(TV, vl) old On( clock, floor) newOn(clock, v2) VxVy. changedOn(x, y) ..-.. [oldOn(x, y) ;t newOn(x, y)) changedStuffy ..-.. [oldStuffy ;t newStuffy) In this example, S = changedOn < changedStuffy, and V = newOn < newStuffy.

The two Herbrand models of rewrite(T, a) are

According to the semantics for theory revision, the re­ sult of moving the TV to v1 should be model 1. Using the model-theoretic definition of circumscription, model 1 is preferred to model 2 at stratum 1 because change­ dOn(TV, v1) is true in model2 and false in model1, and there is no atom of "changed On" that is true in model 1 and false in model 2. Therefore model 1 is the preferred model.

Theorem 1 describes the relationship between Circ(rewrite(T, a); S; V) and Revise(T, a):

Theorem 1. Let T be a theory, and let a and¢> be formulas. Then

Proof. We sketch the proof in both directions. For the forward implication, let M be a model ofT, and let M' be a model in Revise(M, a). We will now construct a model of CR(T) (shorthand for Circ(rewrite(T); S; V)) that corresponds to the pair M, M'.

Let .N be a structure with the same universe and func­ tion interpretations as M and M', but over the language of CR(T). For each nonequality predicate P, let oldP(x) be true in .N iff P(x) is true in M. For each nonequality predicate P, let newP(x) be true in .N iff P(x) is true in M'. Let changedP(x) be true in .N exactly when the truth valuations of oldP(x) and newP(x) differ in .N. Then for any formula¢>, by construction ¢> is true in M' iff new(¢>) is true in .N. Further, .N satisfies all the formulas of rewrite(T).

It remains to show that .N is a preferred model of rewrite(T) . Suppose not. Then there is a model M' of rewrite(T) that is preferred to .N . .Nand M' must agree on all "old" predicates, and there must exist a priority level i such that .N and M' agree on all predicates of strata below i. In addition, the cases where changedP(x) is true in M', over all choices of P at priority stratum i, must be a proper subset of the cases in which changedP is true in .Nat that stratum. But then one can construct a model 0 with the same universe and function interpre­ tations as M, and where P(x) is true in 0 iff new P(x) is true in M'. The relationship between M and 0 shows that M' must not have been a member of Revise(M, a) after all, as the differences between 0 and M at priority stratum i are a proper subset of the differences between M' and M at that stratum, and the differences at lower strata are identical. As this contradicts the assumption that M' was a member of Revise(M, a), we conclude that the theorem holds in the forward direction.

For the reverse direction, suppose that .N is a model of CR(T), and new(¢>) is true in .N. Let M be a model with the same universe and function interpretations as .N but over the language ofT, and in which P(x) is true iff oldP(x) is true in .N, for all nonequality predicates P. Let M' be a model with the same universe and function interpretations as M, differing from M only in that if changedP(x) is true in .N, then M and M' differ on the truth valuation of P(x). By construction, M satisfies all the formulas ofT. If M' is not a member of Revise(M, a), then there must be a model 0 in Revise(M, a) such that 0 and M' agree on all predicates below some pri­ ority stratum i, and at priority stratum i the the points at which 0 and M differ on truth valuation are a proper subset of the points at which M' and M differ. But then one can construct a model M' of CR(T), corresponding to the pair M, 0, such that M' is preferred to .N. We conclude that in fact M' is in Revise(M, a). Finally, since new(¢>) is true in .N, by construction ¢> is true in M'. 0

A variant of Theorem 1 was shown in [Winslett 88c] for the case where a series of updates is applied to T.

5 Comparison of the Two Approaches

Given that model-based theory revisions can be ex­ pressed in circumscription, how should one choose be­ tween the two formalisms? In general, circumscription is more expressive, but also more complex.

Operator semantics. The semantics of operators in a reasoning-about-action application can be directly rep­ resented in a circumscriptive theory; under the theory revision approach, operator semantics is external to the theory.

Minimization policy. Priorities for minimization of dif­ ferent predicates can be directly represented in a circum­ scriptive theory; under the theory revision approach, any priorities were specified external to the theory.

Complexity. I feel that model-based theory revision is much simpler than circumscription for a human to understand, especially when one moves to a variant of circumscription that is sufficiently powerful to represent a series of updates.

Algorithms. The theory revision approach should en­ joy computational advantages over circumscription, be­ cause the theory revision approach does not retain any information about previous states of the world. Circum­ scription based on situation calculus remembers all facts about every state of the world encountered. A hybrid ar­ chitecture (retaining only those bits. of information about prior situations that have an impact on the current situ­ ation) should perform better than either approach alone; see [Forbus 89] for a description of such an implementa­ tion.

6 Conclusions

We have shown how a model-based semantics for the­ ory revision can be captured exactly using circumscrip­ tion. This paper has shown how to translate a single update into circumscription; a series of updates can also be expressed using an appropriate type of circumscrip­ tion [Winslett 88c].

This result captures an interesting connection between work on updates and circumscription. Now that the connection has been established, future work on methods of computing circumscription and updates can be shared between the two disciplines. In addition, for a particu­ lar application, researchers can choose between the two paradigms based on considerations of expressiveness ( cir­ cumscription is more expressive) and simplicity (model­ based theory updates are conceptually simpler) .

7 Acknowledgments

I would like to thank Moshe Vardi, Hirofumi Kat­ suno, and Peter Rathmann for their helpful comments. Vladimir Lifschitz suggested the simplified presentation of these results that I have used here.

8 References

• [Dalal 88] M. Dalal, "Investigations into a Theory of Knowledge Base Revision: Preliminary Report ," AAAI-88, Minneapolis, August 1988.
• [Etherington 88] D. W. Etherington, Reasoning With In­ complete Information, Morgan Kaufmann, Los Al­ tos, 1988.
• [Fagin 83] R. Fagin, J . D. Ullman, and M. Y. Vardi, "On the Semantics of Updates in Databases," ACM Symposium on Principles of Database Systems, April 1983.
• [Fagin 86] R. Fagin, G. M. Kuper, J . D. Ullman, and M. Y. Vardi , "Updating Logical Databases," in Ad­ vances in Computing Research, 3, 1986.
• [Forbus 89] K. D. Forbus, "Introducing Actions into Qualitative Simulation," Proceedings of the Inter­ national Joint Conference on Artificial Intelligence, Detroit , August 1989.
• [Gardenfors 88a] P. Gardenfors and D. Makinson, "Re­ visions of Knowledge Systems Using Epistemic En­ trenchment," Proc. Conf. on Theoretical Aspects of Reasoning About Knowledge, Asilomar, March 1988.
• [Gardenfors 88b] P. Gardenfors , Knowledge in Flux: Modeling the Dynamics of Epistemic States, Brad­ ford Books, MIT Press, 1988.
• [Ginsberg 86] M. L. Ginsberg, "Counterfactuals," Art. Intelligence, 30:1, 1986.
• [Ginsberg 87] M. L. Ginsberg and D. E. Smith, "Reason­ ing About Action I: A Possible Worlds Approach," in Readings in Nonmonotonic Reasoning, M. L. Ginsberg, ed., Morgan Kaufmann, Los Altos, 1987.
• [McCarthy 87a] J. McCarthy, "Circumscription-A Form of Non-Monotonic Reasoning," in Readings in Nonmonotonic Reasoning, M. L. Ginsberg, ed., Morgan Kaufmann, Los Altos, 1987.
• [McCarthy 87b] J. McCarthy, "Applications of Cir­ cumscription to Formalizing Common-Sense Knowl­ edge," in Readings in Nonmonotonic Reasoning, M. L. Ginsberg, ed., Morgan Kaufmann, Los Altos, 1987.
• [Oddie 78] G. Oddie, "Verisimilitude," from The Logic and Philosophy of Scientific Change, in Acta Philo­ sophica Fennica, 30:2-4, 1978.
• [Pollack 76] N. Pollack, Subjunctive Reasoning, Reidel, Dordrecht, 1976.
• [Reiter 87] R. Reiter, "A Theory of Diagnosis from First Principles," Artificial Intelligence, April 1987.
• [Satoh 88] K. Satoh, "Nonmonotonic Reasoning by Min­ imal Belief Revision," Proceedings of the Interna­ tional Conference on Fifth Generation Computer Systems 1988, ICOT, December 1988.
• [Shoham 87] Y. Shoham, "A Semantical Approach to Nonmonotonic Logics," in Readings in Nonmono­ tonic Reasoning, M. L. Ginsberg, ed., Morgan Kauf­ mann, Los Altos, 1987.
• [Weber 86] A. Weber, "Updating Propositional Formu­ las," Proc. of the Expert Database Systems Confer­ ence, Charleston SC, April 1986.
• [Winslett 88a] M. Winslett, "A Framework for Compar­ ison of Update Semantics," ACM Symposium on Principles of Database Systems, March 1988.
• [Winslett 88b] M. Winslett, "Reasoning About Action with a Possible Models Approach," AAAI-88, Min­ neapolis, August 1988. A full version appears as TR UIUCDCS-R-88-1428, Department of Com­ puter Science, Univ. of Illinois-Urbana, May 1988.
• [Winslett 88c] M. Winslett, "Setwise Circumscription," unpublished manuscript, 27 pp., May 1988.