On the Relation Between Autoepistem ic Logic and Circumscription

1 Introduction

The relations between the major nonmonotonic logic for­ malisms of AI - default logic, autoepistemic logic, and circumscription - is of some importance, since all of these logics have been proposed as formalisms for vari­ ous types of commonsense reasoning. The basic formal equivalence of default and autoepistemic logic has al­ ready been shown (see [Konolige, 1987)), but the relation between circumscription and default or autoepistemic logic remains obscure. Mostly this is a consequence of the different foundations of these logics: circumscription is based on a minimal-model semantics (see [Lifschitz, 1985)) , while the others use more proof-theoretic tech­ niques (default logic [Reiter, 1980]) or an epistemic op­ erator (autoepistemic logic [Moore, 1985)) .

In trying to express autoepistemic or default logic in circumscription, researchers have found the basic prob­ lem to be that a minimal-model or even prefered-model semantics simply does not have the capability of rep­ resenting the requisite proof-theoretic or epistemic con­ cepts (see [Shoham, 1987]). We agree with this assess­ ment, and say nothing further about it here.

*This research was supported by the Office of Naval Research under Contract No. N00014- 85-C-0251, by sub­ contract from Stanford University under the Defense Ad­ vanced Research Projects Administration under Contract No. N00039-84-C-0211, and by a gift from the System De­ velopment Foundation.

On the other hand, there have been several results on expressing circumscription in default logic. These results are summarized in [Etherington, 1986); they apply to the restricted case of predicate circumscription with no fixed predicates and with a finite, fixed domain.

From a model-theoretic point of view, the predicate circumscription Circum( A; P; Z) of a first-order sentence A picks out those models of A in which the extension of the predicate P is minimal. The comparison is across models with the same domain and denotation function, but which might differ in the extensions of the predicates Z. All predicates other than P and Z are fixed, that is, cannot vary in a comparison of models. It was recently shown (see [de Kleer and Konolige, 1989)) that fixed predicates are inessential in predicate circumscription, that is, there is a simple translation from any circum­ scription with fixed predicates to one without. Hence fixed predicates no longer present an obstacle to rep­ resenting circumscriptions in default or autoepistemic logic.

The problem of finite domains remains, however. In this paper we provide a solution to this problem, by first extending autoepistemic logic to a language which al­ lows quantifying into the epistemic operator, and then showing that a certain class of autoepistemic theories, the MIN= theories, express all of the first-order conse­ quences of predicate circumscription.

2 Semantics of Quantifying-in

Autoepistemic (AE) logic was defined by [Moore, 1985) as a formal account of an agent reasoning about her own beliefs. The agent's beliefs are assumed to be a set of sentences in some logical language augmented by a modal operator L. As originally defined, and extended in [Konolige, 1987), its language does not permit vari­ ables quantified outside of a modal operator to appear inside. In this section we further extend AE logic to deal with quantifying-in.

2.1 Logical preliminaries

We begin with a language .C for expressing self-belief, and introduce valuations of .C. The treatment generally follows and extends [Konolige, 1987)

Let £ 0 be a first-order language with equality and functional terms. The normal formation rules for for­ mulas of first-order languages hold. A sentence of £o is a formula with no free variables; an atom is a sentence of the form P(t 1 , · · ·, tn)- We extend Lo by adding a unary modal operator L; the extended language is called £ . £ can be defined recursively as containing all the formation rules of £0 , plus the following :

An expression Lc/J is a modal atom. Sentences and atoms of £0 are called ordinary. Note that nestings such as LLcjJ are not allowed; we consider only a single level of nesting here. Because the argument of a modal operator can contain free variables, there may be quantifying into the scope of a modal atom, e.g., 3xLPx is a sentence. Often we will use a subscript "0" to indicate a subset of ordinary sentences, e.g., fo = r n £o .

Let us restrict ourselves for the moment to modal atoms which do not contain free variables. From the point of view of first-order valuations, the modal atoms Lc/J are simply nilary predicates. Our intended interpre­ tation of these atoms is that cP is an element of the belief set of the agent. So we will consider valuations of £ to be standard first-order valuations, with the addition of a belief set r. The atoms Lc/J are interpreted as true or false depending on whether cP is in r . To distinguish these valuations, we will sometimes call them L valua­ tions.

The interaction of the interpretation of L with first­ order valuations is often a delicate matter, and so a per­ spicuous terminology for talking about L valuations is necessary. In particular, it is often useful to decouple the interpretation of modal and ordinary atoms. First­ order valuations are built upon the truthvalues of atoms: for ordinary atoms, truthvalues are given by a structure (U, v, R), where v is a denotational mapping from terms to elements of the universe U, and n is a set of rela­ tions over U, one for each predicate. We will refer to any such structure as an ordinary index, and denote it with the symbol I. Modal atoms are given a truthvalue by a belief set r, which is called a modal index. Note that, because modal operators are not nested, only the ordinary sentences of the modal index r are important.

The truthvalue of any sentence in £ can be determined by the normal rules for first-order valuations, given an ordinary and modal index. We write FI,r cP if a val­ uation (I, r) satisfies c/J. The valuation rule for modal atoms can be written as

A valuation that makes a every member of a set of sentences true is called a model of the set. A sentence that is true in every member of a class of valuations is called valid with respect to the class.

We use Cn(X) to mean the first-order consequences of a first-order set of sentences X.

2.2 Autoepistemic Extensions

In [Konolige, 1987), we informally defined an extension of a set of sentences A as those consequences of A which an agent should believe. The formal counterpart is given by:

DEFINITION 2.1 Any set of sentences T wltzch satisfies the equation

is an autoepistemic extension of A.

This is a fixed-point equation for a belief set T, and is a candidate for the belief set of an ideal introspective agent with premises A. It differs slightly from the origi­ nal definition of [Konolige, 1987) in that the modal index consists of the ordinary part (the kernel ofT); this suf­ fices because the language ofT does not include nested modal operators. _

Note that we are considering all models of A in which the interpretation of Lc/J is the belief set of the agent itself that is the valuations we consider all have a modal in de~ that is,the belief set of the agent. Following Moore, we call such valuations autoepistemic (or A E) valuations.

2.3 Quantifying-in

We would like to extend the language of autoepistemic logic to include variables which are quantified outside the scope of the modal operator, but can appear inside, e.g., 3x.LPx. The problern is that it is not obvious how to extend the semantics of the logic to deal with these "quantified-in" expressions. Recall that the belief set r is a set of sentences that form the beliefs of an agent. To interpret Lc/J, we simply ask whether the expression cP is in r. But with the quantified-in language, we must also be able to interpret LcjJ(x), where c/J(x) is the proposition that the individual x has the property q'J. In order to construct a propositional expression whose meaning is c/J(x), we must have some way of refering to individuals in the domain.

The simplest scheme for reference to domain elements is to use the denotation map v already present in the first-order interpretion I. In place of the valuation rule for modal atoms given above, we use:

That is, we say that c/J( x) is believed if x has a name t such cjJ(t) is believed.

Given this addition to the valuation rule , we can use the definition of autoepistemic extension above for the case in which A contains quantified-in expressions. How­ ever, we will make one technical stipulation that will be useful in later developments, to insure that there are enough "free" names in the language £:

The language £ contains a countably infinite set of constants C which cannot be used in the premise ( 4) set A of an extension.

A given individual x may have none or many names in a model, a circumstance which leads to some inter­ esting behavior of the fixed-point equation of Definition 2.1. To explore some of these, we first make the observa­ tion that the revised definition of satisfiability for modal atoms does not perturb the extensions of any set A that contains no quantified-in expressions.

EXAMPLE 2.1 Let. A= {lJa}. There is a single exten­ sion T of A, with To= C:n(Pa). Therefore, we know that LPa and --.LPb are in T. By the valuation rule for modal atoms (3), 3a:.LPx will be true in (I, To) ifthere is some individual x such that x = v(a.). Ev­ ery interpreta.t.ion I has some such individual, and hence 3x.LPx is true in every (I, To) model of A, and hence in T.

Another interesting sentence contained in T is s : Vx.x=Ja. :J --.LPx. To see why this is so, let x be an individual with x=Jv(a.). Since Pa. is the only ground occurrence of the predicate in T0 , it must be the case that LPx is false in any model (I, T0 ) of A, and hence s is an element ofT.

On the other hand, consider a similar sentence s' : Vx .x = b :J --.LPx. It might be suspected that s' is a member of T, but this is not the case. For although x is the denotation of b, it may also be the denotation of a in some first-order interpretation, and for this interpretation, LPx will be true. So s' will not be true in all (I, To) models of A.

This example highlights a curious situation that oc­ curs when knowledge of properties of individuals hinges on having a name for that individual: the epistemic op­ erator expresses knowledge of the intension of a term. Let us take P to be the property of being rich, a to be the mayor, and b to be the former police chief. We have proof that the mayor is rich (LPa) and no evidence that the former police chief is ( -.LPb ). These are statements about the intension of the terms a and b, that is, the mayor, whoever he is, is rich. On the other hand, the expression LPx when x is a quantified-in variable says that we know Pc to be true for some intensional concept c whose denotation is x. Now if we were to know that a particular individual x is the former police chief, we still cannot say that we have no evidence that x is rich, because x may also be the mayor.

Another consequence of the intensional nature of the epistemic operator is that even though a universal state­ ment may be true in an AE valuation, its substitution instances may not . Consider the valuation (I, r), where FI a=b 1\ Vx.Px :J x=a. and r = Cn(Pa.). We must have FI,r Vx.(LPx V ·Px), because if x = v(a), LPa is true; and if not, --.Px is true . However, the substitution instance LPb V -.Pb is not true in this valuation: LPb is not a member of r, and Pb is true in I because a=b.

Finally, we note that the Barcan formula VxLPx :J LVxPx is tr.ue in every AE valuation, while the converse LVxPx :J VxLPx may be false. The reason for the latter is that even though every individual x has the property P, some individuals may not be given a name in the AE valuation, and so LPx will be false.

This scheme for extending the semantics of L valu­ ations to the quantified-in case is similar to that pro­ posed for the simple epistemic operators in [Konolige, 1984]. It differs from the approach of [Levesque, 1982, Levesque, 1981] in that it is based on the intension of terms rather than their denotation. Nevertheless there are many points of similarity between the two approaches that we have not investigated.

3 MIN Theories

So far we have only looked at extensions of sets of first­ order sentences. The normal definition of extension (2.1) carried over to the extended language, with only a change in the valuation rule for modal atoms, and a slight restriction on the constants appearing in the premise set. VVe now examine a class of first-order sen­ tences that we call MIN theories. Any such theory has the form

where W is a finite set of first-order sentences and the P; are a sequence of predicates. Vole write M(W; P1, ... Pn) to indicate the MIN theory of W over the predicates P;.

The idea behind MIN theories is to select AE valua­ tions in which every individual not known to have the property P; does not have this property, i.e., to minimize the extension of each P; .

EXAMPLE 3.1 Let W {Pa}, and let S Cn(Vx.Px = x=a). Every valuation (I, S) which satisfies M(W; P) makes Px true for x = v(a), and false for every other x . Thus, if we define T by

it is clear that To = S, and hence Tis an extension

of M(W; P). In fact it is the only extension. Let W = {Pa V Pb}, and as before let S = Cn(Vx.Px = x=a) . Again we can show that ev­ ery valuation (I, S) satisfying M(W; P) satisfies Vx.Px = x=a, and so S is the kernel of an AE extension of !VI ( T,'lf; P). In this case the extension is not unique; there is another one whose kernel is Cn(Vx.Px = x=b) . The sentences which these two extension have in common are all first-order conse­ quences of (Vx.Px = x =a.) V (Vx.Px = x =b). Let W = {3xPx}, and let S = Cn(Vx.Px = x=a) . Again we can show that every valuation (I, S) sat­ isfying M(vV; P) satisfies Vx .Px = x=a, and so S generates an AE extension T . But the choice of the constant a. was arbitrary, and we can use any other constant in defining S. Hence there are an infinite number of extensions of M(W; P); the sen­ tences they have in common are the first-order con­ sequences of 3!xPx .

These examples are very suggestive of a correspon­ dence between MIN theories and the minimal models of W. However, there is one essential point of difference. A· model I of W is minimal in P; if there is no other model with the same universe and denotation function whose extensions of P; are properly included in those of I. (Note that we are assuming here that the exten­ sions of all predicates other than the P; can vary across compared models . In the next subsection we consider the case of fixed predicates.) Comparisons are not made between models with different domains and different de­ notation functions, and hence choosing only the minimal models of W will not lead to any conclusions about the equality relation or the size of the domain not already apparent in W (this point has been noted in [Etherington and Reiter, 1984]). On the other hand, this is not true of (.he extensions of MIN theories: an extension c<:1n con­ tain conclusions not present in W about equa li ty among terms . For example, the set W = { ·Pa :) a = b} docs not have a = b among its first-order consequences, yet. the single extension of M(VV, P) does . To get the cor­ respondence between MIN theories and minimal model;; correct, we need to fix the interpretation of equality 111 the former .

3.1 Fixing predicates

We extend rviiN theories by adding a set of predi cates, the fixed predicates, to the original definition . A Ml N theory now has the form

where the Qi are a sequence of predicates . 'Ve write M(W; P1, . .. Pn; Q1, ... Qm) to indicate the MIN theory of W over the predicates P; with Qi fixed.

Note that, to fix Q, both Q and its negation ·Q are minimized . In general this will lead to multiple exten­ sions in which various combinations of Qx and ·Qx hold for each individual x .

EXAMPLE 3.2 Let W = {·Pa:) Qa} . The MIN the­ ory M(W; P; Q) has two classes of extensions: one class contains { ·Pa, Qa}, while the other contains { ·Qa, Pa.}. Thus the minimization of P does not force the acceptance of Qa in every extension .

The presence of a fixed Q actually creates an infi­ nite number of extensions because of the presence of the countable set C of constants in [ . '"'e will consider extensions to be equivalent if they differ only in sentences containing these constants; in this case, there are just two nonequivalent extensions.

The equality predicate can be fixed, just a<; any other predicate, and it is the class of MIN theories M(W; P; =) that we consider in relating extensions to minimal mod­ els: call these MIN= theories. We now develop the re­ sult that a first-order sentence is true in the ?-minimal models of W just in case it is true in every extension of M(W;P;=).

3.2 Parameter models

A first-order interpretation in which every individual x is denoted by some term is called a parameter interpreta­ tion. Her brand interpretations are one type of parameter interpretation, in which every term denotes itself. Pa­ rameter interpretations are more general than Herbrand interpretations, since in the former two terms can refer to the same individual.

Just as Herbrand interpretations are a sufficient se­ mantics for universal prenex sentences, so too parame­ ter interpretations suffice for sets of first-order sentences. By "suffice" we mean that any such set W has a model if and only if it has a parameter model. Note that this statement is not true in general if W can contain mem­ bers of C: for example the set {3x-.Px,Pc1 ,Pc2,···}, in which Pc; is asserted for every constant c; E C, has a model but no C-parameter model.

A second interesting property of parameter models is that the ? -minimal parameter models of a finite set W are sufricient for minimal entailment , as we now showl

PROPOSIT ION 3. 1 Let ¢ be a sent ence of [ o - C (the base la.ng·uage without the constants C), and 11\l a set of sent ences of the same lang1wge. Then ¢ E [ a is t rue in all P -minimal countable models of W if and only if it is true in all ?-minimal parameter models.

Proof. Suppose W +1/J ha<; a ?-minimal count­ able model I. Let the constants C' be those members of C not mentioned by ¢. 'iVe are free to construct a model I' that is the same as I , but in which all elements of I are clenoted by one of C'. I' must be minimal; if it were not , then there is another model I" with the same denotation function and universe as I', but with a smaller extension of P. We can con­ vert I" into a model with the same denotation function as I, which must then be less than I , a contradiction.

In the converse direction, if W + ¢ has a minimal parameter model, it obviously has a minimal countable model.

Finally, as the next proposition shows , parameter models are the only ones we need consider in forming extensions of MIN= theories.

PROPOSITION 3.2 Any interpretation (I, r) is a model of a MIN= theory M(W;P;=) only if I is a param­ eter model.

Proof. Suppose I isn't a parameter model. Then there is some element e of the universe of I such that e is not denoted by any term. Thus both ·Lx=y and ·Lx::j:.y are true for x=e, and this leads to a contradiction in M(W;P;=).

3.3 The main theorem

For any ?-minimal parameter model I of W, we call the ?-diagram of I the set of ground literals in P and= that are true in I. We first show that the diagram of I picks out a unique extension of M(W;P;=), for which I is a model.

PROPOSITION 3.3 Let D be the diagram of a ?­ minimal parameter model I of W. Then (I, D) zs a model of some extension of M(W; P; =) .

Proof. This is a sketch of the proof. Let

We first show that the restriction of S to ground P and equality literals is exactly the set D. Note that D is complete with respect to equal­ ity literals: for all terms a and b, either a=b or a::j:.b is in D, but not both. From the fixing of equality in M(W;P;=), all of these are also contained in S. D is also complete with respect to ?-literals. From the sentence V:r .·LP:r :J ·Px, S contains all negative in­ stances of the ?-literals of D. It also must contain al l positive instances; if it did not., we cou ld construct a parameter model of {;V whose P-ex tension is less than that of I, a contradic­ tion. Fi naJJy, S is consistent because (I, D) is a. model of M(HI ; P; =).

1 Note: we will often use a single minimized predicate P in propositions in the rest of this paper; the extensions to multiple predicates is obvious.

Consider the equation

Since Sand D agree on P and=, the To must be eq ual to S. Hence T is an extension of M( W; P; =),and (I, D) is a model of it.

EXAMPLE: 3.:3 This example is from David Kueker (as reproduced in [Perlis, 1986)) . Let W be the set {Pa, V:r.Px ::;:::: Ps(x), Yx.a#s(x), s(x)=s(y) :J :r=y}. A ?-minimal parameter model I satisfying this is the Herbrand model with Px true for a and all terms of the forms( s( s( . .. s( a) . . . ) ) , and false for all other terms. I is isomorphic to the natural numbers, hence the sentence Vx.Px :J ((·3y.x=sy) :J x=a)) is satisfied by I. In fact, this sentence is in every extension of the MIN= theory of W.

We now prove a suitable converse of the above propo­ sition, namely, that the models of every extension of l\ti(l·V; P; =) are minimal in P.

PROPOSITION :3 .4 Let T be an extension of the theory lvl(W; P; =). If (I, T0 ) is a model of M(W; P; =), then I is a ?-minimal parameter model of W .

Proof. This is a proof sketch. First we show that To is complete with respect to equality and ?-literals. For equality, if T0 doesn't contain a=b, then it must contain a#b by the equality­ fixing sentence of M(W;P;=) . For ?-literals, if To doesn't contain Pa, it must contain -.Pa by the ?-minimizing sentence of M(W; P; =).

From Proposition 3.2 we know that I must be a parameter model. Suppose I is not P­ rninimal, and I' is a similar parameter model of W less than I . Then (I', T0 ) is a model of M(W; P; =),because the equality sentences are satisfied, and the ?-minimizing sentence also is. But then the fixed-point equation for T does not hold, since To is complete with respect to P-lit.erals, and I' does not satisfy T0 .

By Proposition 3.3 above, every ?-minimal parame­ ter model of W satisfies the kernel of some extension of M(W; P; =). Conversely, by Proposition 3.4 above, the kernel of every extension ofM(W;P;=) are the sen­ tences true of some class of ?-minimal parameter models of W. Given the sufficiency of parameter models for min­ imal entailment (Proposition 3.1), we have the following theorem.

THEOREM 3.5

The first-order sentences S true in every extension of M(W; P; =) are exactly those sentence true in the ?-minimal models of W .

R.emarks. From the above theorem we can clarify t.he relationship between predicate circumscription and au­ toepistemic logic. The semantics of the second-order cir­ cumscript.ion schema Circum(A; P; Z), with every pred­ icate other than P in the tuple of varying predicates Z, is given by the P-minimal models of A. Thus, the first-order conseq11 ences of a predicate circumscription of this form are exactly the sentences common to all ex­ tensions of a corresponding MIN= theory M(W; P; =), holding equality fixed. This result could be extended to the parallel circumscription of a tuple of predicates in an obvious way.

From the result.s of [de Kleer and Konolige, 1989], we know that fixed predicates are inessential, and that any circumscription involving fixed predicates can al­ ways be reduced t.o one without . For example, the cir­ cumscription Circum( A; P; Z) with Q f. Z is equiva­ lent to Circum(A 1\ Q'=·Q;P,Q,Q';Z), where Q' is a new predicate constant. The corresponding construct for MIN= theories is to fix Q using M(W; P; =, Q) (note that there is no need to introduce a new predicate con­ stant for ·Q). Hence the first-order consequences of par­ allel predicate circumscription with fixed predicates a.re given by the corresponding MIN= theory.

On the other hand, there is no way to translate in gen­ eral from autoepistemic theories to circumscription. The basic problem (noted in [Imielinski, 1987]) is that cir­ cumscription cannot distinguish between the epistemic idea of knowing Px, and the simple truth of Px. Thus, even without the complications of quantifying-in, there is no adequate circumscriptive translation for sentences such as LPa 1\ -.L-.Qa :J Qa. Further, even in the re­ stricted :MIN= theories which have a natural correspon­ dence to circumscription, AE logic is finer-grained than circumscription. Each extension of a MIN= theory yields a set of sentences true in an equivalence class of some minimal model of A, not all of them.

In the next section we use Theorem 3.5 to explore some issues of reasoning about equality in circumscription.

4 Reasoning about Equality

In defining P-minima.l interpretations, we have specified that two interpretations must have the same domain and denotation function in order to be comparable. This cor­ responds to predicate circumscription with a fixed inter­ pretation of terms.

EXAMPLE 4.1 Consider a simple abnormality theory (see [McCarthy, 1986]), with W = {Vx.Px 1\ ·ab(x) :J Qx, Pa, ·Qb} (this is a variation of an example in [Perlis, 1986]). We would expect Qa to be a consequence of Circum(W; ab; Q), but it is not. The reason is that there are ab-minimal models of W in which b and a refer to the same individual, and ·Qa is true.

This example is typical of the way in which circum­ scription handles equality: it does not allow any new conclusions about equality, because the denotations of terms are fixed across comparable models. However, it is also possible to compare models with different denota­ tion functions; the corresponding predicate circumscription allows functions to vary, as well as predicates (see [Lifschitz, 1984]).

• EXAMPLE 4.2 Consider a simple abnormality theory with W = {'v'x.Px 1\ ·ab(x) :::::J Q.'t, ab(a), ab(b)} In this case, a=b is a consequence of Circum(W;ab;Q,a,b) . The reason is thal, if we al­ low interpretations with different denotations for a and b to be comparable, the interpretations in whi ch a and b are identical are obviously minimal in ilb.

From the above example, it seems that allowing terms to vary leads to the danger of unexpect.ed identifi cat ion of terms, at least if we do not have axioms that explicitly say that differing terms refer to different. individuals. We would like to treat equality among terms somewhat in between the two extremes of fixed and varying denota­ tions: to remain agnostic about the equivalence of terms, but still be able to draw basic default conclusions.

The MIN= theories, because of their relation to ?­ minimal models, always leave the denotations of terms fixed, and so fall prey to the same problems with equal­ ity as circumscription with fixed terms . However , we can relax the restriction on denotations by using MIN theories, without the sentences fixing equality.

• EXAMPLE 4.3 Redoing the previous examples, let W = {'v'x.Px 1\ ·ab(x) :::::J Qx, Pa , ·Qb}. There is one extension of M(W; ab) , whose kernel is Cn(W, Ax.Px :::::J x=a, afb}. Here the lack of equality fixation leads to the. conclusion that a and

b are different individuals. For the abnormality theory W = {'v':z:. Px/\·ab(x) :::::J Qx, ab(a), ab(b)}, on the other hand, the exten­ sions of M(W; ab; =) and M(W; ab) are the same: getting rid of the equality-fixing sentences does not lead to the identification of a and b.

MIN theories without equality fixation are thus inter­ mediate between a fixed and varying interpretation of equality, and seem to be the right level of variation for commonsense reasoning in abnormality theories.

5 Conclusion

We have extended the language and semantics of au­ toepistemic logic in a natural way to the case of quantified-in variables. By looking at a class of AE the­ ories, the MIN= theories, we showed that all of the first­ order consequences of predicate circumscription could be expressed in a simple way in autoepistemic logic. This is the first result on the relationship of these two logics for the case of nonfinite domains. The results have been used to shed some light on the treatment of equality in commonsense reasomng.