Abstract minimality and circumscription

Research Note

Abstract minimality and

circumscription

Churn Jung Liau and Bertrand I-peng Lin

Department of Computer Science and Information Engineering, National Taiwan University, Taipei, Taiwan

Received May 1990 Revised November 1991

Abstract

Liau, C.J. and B.I. Lin Abstract minimality and circumscription (Research Note), Artificial Intelligence 54 (1992) 381-396.

In this paper, we present an alternative approach to the generalization of circumscription. Traditionally, the generalization of circumscription involves the change of ordering among models, while in the present study we only try to generalize the minimality criteria of models. We define the notion of abstractly minimal (or (P, Z)-minimal) models by iso- morphism. Under this generalization we come up with the fact that some theories which are unsatisfiable in the original circumscription will be satisfiable now. Moreover, we prove that this generalization is completely coincident with the original circumscription in the case of well-founded theories.

I. Introduction

In 1977, McCarthy [12] proposed a circumscription formalism to capture the intuitive idea about the minimality of existing objects (in particular, abnormal ones) in commonsense reasoning. The original form he first proposed is called

domain circumscription.

Then he generalized this form to predicate cir- cumscription in 1980 [13], which, when applied to a sentence A and predicates P, restricts the extensions of P to the minimal ones that satisfy the sentence A. Since then, many different variants of circumscription have been proposed to improve the expressibility of the original circumscription. These include par-

Correspondence to: C.J. Liau, Department of Computer Science and Information Engineering, National Taiwan University, Taipei, Taiwan.

382 ('hurpt ,hm~,, Liau, Bertrand I-peng Lin

allel circumscription, prioritized circumscription [8], pointwise circumscription [10], formula circumscription [14], and equality circumscription [16].

However, because it is possible that there do not exist any minimal models for a given sentence A, circumscription may result in an unsatisfiable theory. Davis [3] and Etherington [4] give such examples. In 1986, Lifschitz [9] provided some sufficient conditions under which predicate circumscription can always preserve satisfiability. Recently, Jager [6[ also defined a class of sentences, called positive disjunctive sentences, and proved that if a theory can be partitioned into two parts, one part being a consistent theory without involving P and the other part equivalent to a positive disjunctive sentence, then the whole theory is consistent under predicate circumscription. However, it still remains open to determine the largest class of theories in which circumscription can preserve consistency. On the other hand, some weaker versions of circumscription have been proposed to guarantee the preservation of consistency for all first-order theories. (E.g. Mott's closed and nonrecursive circumscription [15].) However, some researchers have observed that over- weakening of circumscription may lead to inadequacy in some cases [1].

In this paper, we present an alternative compromised approach to this problem. Wc weaken the original circumscription by taking model iso- morphism into consideration and prove that the new circumscription formulae are strong enough to coincide with the original ones in a large class of theories.

I. 1. Preliminary knowledge

In this subsection we give some preliminary knowledge about circumscrip- tion. In particular, we focus our attention on domain circumscription and parallel circumscription since they possess the most basic features of all circumscription formalisms.

In what follows we assume that the reader is familiar with basic notations of second-order logic. For convenience we use P to denote a tuple of distinct predicates, i.e. P = ( P I , P 2 . . . P,,). Two tuples of predicates, P = (P~, P2 . . . P,,) and (2 = ( Q I , Q2 . . . Qm), are called similar if n = m and the arity of Pi is equal to that of Qi for each i. Following Lifschitz's notation, we write P < (2 to denote (P <~ (2)/x -3((2 ~< P), where P ~< (2 is the abbrevia- tion of A i_~i~,, Vx (Pi x D Qix).

Let A(P, Z ) be a first-order sentence containing predicates P and Z; then we have the following definitions for domain circumscription [4] and predicate circumscription [8, 13].

Definition 1.1.

(1) The domain circumscription of A is DCir(A) = V d . ( 3 x . d x A Axiom(d) A A J D Vx.dx), where A '/is the relativization o f A w.r.t, d and is formed by replacing each universal q u a n t i f e r Vx in A by V x . d x D and

each existential quantifier 3x by 3x.dx A, and Axiom(d) is the conjunc-

tion of sentences V x . ( ( A l~i~, dxi)D df(x)) for each n-ary function

symbol f and n t> 0.

(2) The parallel circumscription of P in A with variables Z is the sentence

A(P, Z) A -a3pz(A(p, Z) A p < P)

and is denoted by Cirw;z)(A ) (or Cir(,4) for convenience).

Note that the definition of domain circumscription is Etherington's improved version which excludes a smaller model with empty domain by conjoining " 3 x . d x " before "Axiom(d)".

Now, let us turn to the model-theoretic counterpart of circumscription. We first give the following definition.

Definition 1.2. Assume that M and N are two first-order structures.

(1) We say that M is a substructure of N if IMI c_ IN[ and M[K] is the

restriction of N[K] to ]M[ for each function or predicate symbol K.

(2) We say that M is (P, Z)-less than N if (i) IMI =

INI;

(ii) M[K] = N[K] for every symbol K not in P U Z;

(iii) M[Pi] C N[Pi] for each Pi in P and there exists at least one, Pi so

that M[P~] ~ N[Pi].

(3) A model M of sentence ,4 is called minimal (resp. (P, Z)-minimal) if there do not exist any models of ,4 which are proper substructures of (resp. (P, Z)-less than) M.

From the two definitions above we have the following simple but important lemma [9, .12]:

Lemma 1.3. The models of DCir(A) (resp. Cir(A)) are exactly the minimal

(resp. (P, z)-minimal) models of A.

Finally, we present some basic model-theoretic definitions for later ref- erence.

Definition 1.4 [11, 16]. Given two first-order structures M and M' and a function h: IMI--~ [M' I,

(1) h is a homomorphism from M to M' if h satisfies the following conditions for all function symbols f and predicate symbols P:

(i) for all a EIM] n, h(M[f](a))=M'[f](h(a)), where h ( a ) =

(h(al) . . . . , h(an) ) and n = arity(f),

384 Churn Jung Liau. Bertrand l-peng Lin

(2) h is an isomorphism between M and M ' if h is 1-1 and onto, and satisfies condition (i) above and the following condition:

(ii') for all a E IM[", a E M[P] iff h(a) ~ M ' [ P ] , where n = arity(P). T h e model M is said to be h o m o m o r p h i c to (resp. isomorphic with) M ' if t h e r e exists a h o m o m o r p h i s m (resp. isomorphism) from M to M'. Moreover, two sets are equinumerous if there exists a 1-1 and onto function between these two sets.

2. Abstract circumscription and minimality

2.1. S o m e motivating examples

In 1980, Davis [3] d i s c o v e r e d a first-order theory without minimal models. His example was presented in the context of domain circumscription and, later on, E t h e r i n g t o n et al. [4] modified it to match the formalism of predicate circumscription. In this section we will present Etherington's example and two further examples from model theory and temporal reasoning literature. The latter two examples are presented in the context of domain circumscription but it is quite easy to find the corresponding examples in predicate circumscription.

Example 1.

T,, : 3 x . N x /x V y . [ N y D x ~ s u c c ( y ) ] , Vx. N x D N s u c c ( x ) ,

V x . V y . ( s u c c ( x ) = succ(y) D x = y ) .

T h e n , in any model of T O the extensions of N contain a sequence of elements isomorphic to the natural numbers. Hence T 0 has no N-minimal models since we can cut a finite initial segment of the sequence to construct a model which is N-less than the original model.

Example 2 [2]. T 1 : V x y z . R x y / x R y z D R x z , V x.-7 R x x , V x y . R x y v R y x v x = y , V x y . R x y ~ 3 z . ( R x z A R z y ) , Vx. 3 y . R x y , V x. 3 y . R y x ,

dense ordering without endpoints. Thus for each model M of T 1, if we remove finite elements from M, it remains to be the model of T I. In other words, T 1 has no minimal models.

Example 3. To model a time structure which is linear, discrete and unbounded in the future direction and has a starting point, Gabbay [5] proposes a fragment of first-order axioms which characterizes the so-called integer-like time. The following axioms are a slightly modified version of his:

T 2 : V t u v . t < u A u < v D t < v (transitivity of < ) , Vt.-7(t < t) (irreflexivity of < ) ,

V t u . t < u v u < t v t = u (linearity),

3 t . V u . ( 7 ( u = t) D t < u) (starting point of time),

V t . 3 u . ( t < u A 7 3 V . ( t < v A V < U)) (immediate successor), V t . [ ( 3 u . u < t) D 3 u . ( u < t ^ - ~ 3 v . ( u < v A V < t))]

(immediate predecessor except the starting point).

As pointed out by Gabbay this is not exactly an axiom system for integer time. Indeed, there exist some odd models for this set of axioms. For example, suppose that (N, < u ) denotes the natural numbers and (Z', < z ' ) denotes a structure isomorphic to integer numbers so that NCq Z ' = fJ, then we can construct a model M for the above axioms as follows:

IMI

= N u

z',

M [ < ] = < N U < z ' U ( N x Z ' ) .

Thus, M has transfinite time

points

(i.e., Z'). Now, if we want to eliminate models with transfinite time points, domain circumscription may be helpful. However, as in the examples we have seen, the axioms have no minimal models since we can always cut initial segments of any models to construct new models.

Some interesting features can be observed from these examples. First, every model of these theories has infinite submodels which form an infinitely descending chain under the orderings of Definition 1.2. Secondly, though these theories have no minimal models, they have some special models so that the infinitely descending chain starting from them consists of a class of isomorphic models.

2.2. A b s t r a c t m i n i m a l i t y

According to Definition 1.2, a model is minimal (resp. (P, Z)-minimal) if we cannot decrease the domain elements (resp. extensions of the predicates in P) properly. From the examples above we find that, in some cases, though a

386 ('hurn Jung Liau, Bertrand I-peng Lin

model can be decreased properly, the decreasing is not substantial in the sense of set equinumerous and algebraic homomorphism. This motivates the follow- ing definition.

For notational convenience, we denote (P, Z)-less than by <(p,z~ (or < when P and Z are clear from the context), and ~<~p.z~ represents (t", Z)-less than or equal to.

Definition 2.1. Let T be a theory. If P, Z are two tuples of predicates in T and M is a model of T, then:

(a) M is an abstractly minimal model of T if all its submodels are isomorphic to it.

(b) M is an abstractly (P,Z)-minimal model of T, if for each model M ' <~ ¢e,z)M, M is isomorphic to M'.

In what follows, the prefix (P, Z) is dropped when distinguishing domain minimality from (t, Z)-minimality is irrelevant.

To see how we generalize the original definition of minimal model, first notice that in the original minimality criterion a model M is minimal if the only model less than M is M itself. Now, contrary to other generalizations of circumscription (e.g. generalized circumscription [7]), we do not change the definition of "less t h a n " into another new pre-order relation but we relax the requirement for ordinary minimality so that a model M is abstractly minimal if all models less than M have the same structure as M. Intuitively, isomorphism of two models guarantees that they are structurally equivalent. Therefore, if M ' is less than but isomorphic to M, then we say M' is not substantially less than M and if the only models less than M are those not substantially less than it, then M can be said to be abstractly minimal.

Obviously, the definition of abstract minimality is compatible with ordinary minimality. This can be seen in the following lemma:

L e m m a 2.2. I f M is an abstractly minimal model o f T, then so are all models M ' <~ ~p.z)M.

2.3. Abstract circumscription

Corresponding to the minimality criteria is Definition 2.1, we have a weaker form of circumscription to express the idea of abstract minimality.

To begin with, we present some notations for brevity. First, let F denote the set of function symbols in a theory T, (P, Z ) = (P~, P2 . . . P,, Z, . . . Z m ) and (p, z) be tuples of predicate symbols and variables respectively and Q be the tuples of predicates in T but not in ( P , Z ) . Secondly, if h is a unary function, we denote ( h ( x l ) , h ( x 2 ) . . . h(xk) ) by h(x). Then, we have the

following abbreviations:

Fun(h) ~f /~ V x . h ( f ( x ) ) : f ( h ( x ) )

f ~ F

(h satisfies Definition 1.4(1)(i)).

1 - 1 ( h ) ~ f V x y . h ( x ) = h(y)=- x = y (h is a 1-1 function). O n t o ( h ) ~ f V x . 3 y . x = h ( y ) (h is an onto function). H o m o ( R , S, h) de=fVx.Rx =- Sh(x)

(h satisfies Definition 1.4(2)(ii')).

Pred(h, p, = H o m o ( P , P, h) /x /~ H o m ° ( P i , Pi, h)

l ~ i ~ n

l ~ i ~ m

We now can define abstract circumscription. Definition 2.3.

(a) Let T be a first-order theory; then we define abstract domain circum- scription of T as follows: A B D C i r ( T ) = T ^ V d [ ( 3 x . d ( x ) ) ^ T d ^ Axiom(d) D 3 h ( F u n ( h ) A 1-1(h)/x V x ( d ( x ) - 3 y . h ( y ) = x) ^ /~ H o m o ( P , P, h))] , P E P _1

where d is a predicate variable, T d and Axiom(d) are the same as in Definition 1.1, and P is the set of all predicates in T.

(b) If T is a theory and (P, Z) is a tuple of predicates in T, we define abstract parallel circumscription of T as follows:

ABCir~p,z)(T)

= T(P, Z ) ^ Vpz. IT(P, z) ^ p < P

D 3 h . ( F u n ( h ) / x 1-1(h) ^ Onto(h) ^ Pred(h, p, z))].

Note that in A B D C i r ( T ) , the requirement of h being onto is expressed by " V x ( d ( x ) = - - 3 y . h ( y ) = x " , since we require the isomorphism of two models with different domains.

The intuitive meanings of the other abbreviations and definition will become clear after the following theorem and its proof are presented.

388 Churn Jung Liau, Bertrand 1-peng Lin

Theorem

2.4.

The models of ABCirw,zl(T ) (resp. ABDCir(T)) are exactly the

abstractly

(P,

Z)-minimal (resp. minimal) models of T.

Proof. We prove that all abstractly (P, Z)-minimal (resp. minimal) models of T are models of

ABCir(e.z)(T )

(resp.

ABDCir(T))

in the following (1) (resp. (2)), and sketch the proof of the other direction in (3).

(1) For abstract parallel circumscription, let M be an abstractly ( P , Z ) - minimal model of T. We want to show that M is a model of

ABCir(e,z)(T ).

Suppose a is an arbitrary variable assignment (including individual, predicate and function variable), then

M, a ~ T(P, Z)

for M is a model of T. Let M ' be another structure, defined as follows:

IM'I=IM[,

M'[Q] = M[Q] for symbols Q not in

(P, z ) ,

M'[P,] = a ( p , ) ,

M'[ZJ = c~(z,) .

If

M, a ~ T(p, z) A p < P,

then M ' will be a (P, Z)-submodel of M for T, so by abstract minimality of M we can find an isomorphism h 0 between M and M'. Since IMI = IM'[, h o is a unary function on IMI, so we can set a ' =

a[h *--ho]

(i.e., a ' is identical to a except that h is assigned the function h0). Then, according to Definition 1.4:

(i) for all a E Inl",

h,,(M[f](a)) = M'[f](h,,(a)) = M[f](ho(a))

(for

M [ f ] = M ' [ f ] )

~ M , a ' ~ h(f(a))=f(h(a)),

for all a ~

IMI"

M, o~' ~ Vx. h(f(x)) : f(h(x)) ,

thus we have

M, a' ~ Fun(h)

since the result holds for all f ; (ii) for all a E ]Mj" and all predicate symbols P,

and a ~ M[P]

iff

ho(a ) ~ M'[P] M, ~' ~ Vx.Qx ~- Qh(x)

M, ~' ~ Vx. Pi x =- pih(x)

if Q not in (P, Z),

for M[Q] = M'[Q'],

if P~ in P, for

M'[P,]

= a ' [ p , ] ,

M, a' ~ Vx.Zix=- zih(x )

if Zi in Z, for

M'[Zi]

= a ' [ z i ] , thus we have

M, a' ~ Pred(h, p,

z);

(iii) h o is 1-1 ==>for all a, b in IMI,

ho(a ) = ho(b )

implies a = b, thus we have

Thus,

h 0 is onto ~ Va E

IM'I

= IMI, 3 b E IMI such that

ho(b ) = a,

thus we have

M, a ' ~ Onto(h).

M, a ~ 3h.(Fun(h)

A 1-1(h) ^

Onto(h) A Pred(h, p, z)) ,

and

M ~ABCir(e,z)(T )

since a is arbitrary.

(2) For abstract domain circumscription let M be an abstractly minimal model and a be a variable assignment such that

M, ~ ~ 3 x . d ( x ) ^ TdA

A x i o m ( d ) . We can construct M ' as follows:

IM'[--c~(d),

and

M'[S]

is

M[S]

restricted to

[M'I

for all symbols S (i.e.,

M'[S] = M[S] "~

[M[).

Obviously, M ' is a submodel of M, and by abstract minimality, we have an isomorphism h 0 from M to M'. Since IM'I is a subset of

IMI, we

can again set a ' =

a[h

~---h0]. Similarly, we can show M, a ' ~ 1-1(h)

A Fun(h).

Moreover,

(i)

ho:[MI--~lM'l~for a

in [MI,

ho(a)

is in

IM'I

= a ( d )

M, a' ~ Vx(3y(h(y) = x) D d(x)),

(ii) h 0 is onto, Va E

IM'I

= ~ ( d ) ,

3b

~ IMI

such

that

ho(b ) = a

M, a' ~ Vx(d(x) D

3 y ( h ( y ) = x)),

(iii) for all a ~

IMP,

a E M[P]

iff

ho(a ) E

M'[PI

= M[P] n ~(d)"

for

all predicate symbols P

l<_i<~n

f f M, ct' ~ Vxex =- eh(x)

(since

M, a' ~ Vx.d(h(x))

by (i))

M, a' ~ A Homo(P, P, h).

P E P Consequently,

M, a ~ 3h(Fun(h)

^ 1-1(h) A

Vx(d(x) =- 3y.h(y) = x)

/

A A Homo(P, P, h)) ,

P ~ P and

M ~ ABDCir(T).

(3) For the converse direction, we comment on the case of abstract parallel circumscription. Suppose M is a model of

ABCir(e,z)(T ),

and M ' is a (P, Z)- submodel of M. Then M, a ~ T(p, z) A p < P with a being a variable assign- ment satisfying

a(p,

z ) =

(M'[P], M'[Z]).

Thus, the existence of h guarantees the existence of an isomorphism between M and M'. This proves M is abstractly (P, Z)-minimal. []

We now go back to the three previous examples to see how abstract circumscription circumvents the unsatisfiability problem of these examples.

3 9 0 Churn Jung Liau, Bertrand l-peng Lin

Example 1 (continued). For T~, we have a model M as follows: [M 1 = { . . . . - 3 , - 2 , - 1 , ( I , 1, 2, 3 . . . . },

i.e. the set of integers.

M[succ]: [M[--+

IMI, x ~ x + 1.

MIN]

= {0, 1, 2, 3 , . . . } ,

i.e. the set of natural numbers.

T h e n , any N-submodels of M must have the same universe and interpreta- tion of "succ" with M and extensions of N must be {n, n + 1, n + 2 . . . . } for some positive integer n. It is easy to construct an isomorphism between M and its respective submodels. In other words, it is an abstractly N-minimal model of T 0 .

Note that M is not a model with minimal domain, i.e., the domain contains many junk elements - 1 , - 2 , - 3 . . . . Thus McCarthy's claim [13] that domain circumscription can be replaced by predicate circumscription fails in the abstract case. This will be discussed further in Section 3.3.

Example 2 (continued). According to the results from model theory [2], all countably infinite models of T~ are isomorphic to each other. Thus, any countable models of T~ are abstractly minimal models. This example is just an instance of T h e o r e m 3.1 below.

Example 3 (continued). It is easy to verify that the natural n u m b e r structure (N, < x ) is an abstractly minimal model of T 2 and any model with transfinite time points contains this model as its p r o p e r submodel. T h e r e f o r e , abstract d o m a i n circumscription has eliminated all odd models successfully since (N, <N) cannot be isomorphic to any transfinite model.

3. Properties and comparisons with related work

3. I. Satisfiability of abstract circumscription

According to Definition 2.1, any minimal model is also abstractly minimal. Thus, any theory which is satisfiable u n d e r the ordinary circumscription must be also satisfiable under abstract circumscription. We provide a natural class of theories which may be unsatisfiable under the ordinary circumscription but is satisfiable u n d e r abstract circumscription.

In classical model theory, a theory T is called K-categorical if all models of T with cardinality K are isomorphic. For a finite theory T, if T is satisfiable, then T has a model M with cardinality w by the L o w e n h e i n - S k o l e m t h e o r e m [11]. Thus, if M has a finite submodel, then T has a minimal model; otherwise, if T is w-categorical, then all infinite submodels of M are isomorphic to M, so M is an abstractly minimal model. It follows that we have the following theorem:

Theorem 3.1. Each to-categorical theory has abstractly minimal models.

A n algebraic characterization of to-categorical theories has been given by the so-called Morley's theorem [2].

3.2. Coincidence with ordinary circumscription

A theory is called suitable for a circumscription formalism if it is satisfiable under the formalism. Though we have a strictly larger class of suitable theories for abstract circumscription than for the ordinary one, there still exist satisfi- able theories which are not suitable for abstract circumscription. This can be seen from the following example:

Example 4. A satisfiable theory which is not suitable for abstract cir- cumscription: 3x.[ Bx ^ Vy.( By D x ~ l( y) ^ x ~ r ( y ) ) ] , Vx. Bx ~ BI(x) ^ Br(x) , V x . V y . l ( x ) = l ( y ) D x = y , V x . V y . r ( x ) = r(y) ~ x = y , V x . V y . l ( x ) ~ r( y) .

Now, if we interpret x = l(y) (resp. x = r(y)) as " x is the left (resp. right) son of y " , then obviously, for each model M of this theory, M[B] must contain an infinite binary complete tree (i.b.c.t.). Thus, we have two cases:

Case 1. M[B] contains infinite i.b.c.t.'s: let M ' be a B-submodel of M with only one i.b.c.t, in M'[B], then M ' is not isomorphic with M.

Case 2. M[B] contains finite (say n) i.b.c.t.'s: let [M' I = IMI, M'[S] = M[S] for all symbols S except B, and M'[B] = M [ B ] / { r o } , where r 0 is the root of one i.b.c.t, in M[B], then M ' is a B-submodel of M and M'[B] contains n + 1 i.b.c.t.'s, so M' is not isomorphic with M.

Consequently, all models of this theory are not abstractly B-minimal, i.e., this theory is not suitable for abstract circumscription on B.

However, abstract circumscription has another advantage, i.e., its coinci- dence with the ordinary circumscription. Recall that a theory T is called well-founded (w.r.t. (P, Z)) if for each model M of T, there exists a minimal (resp. (P, Z)-minimal) model M ' such that M ' is a submodel of M (resp. M ' <~(l,,Z) M ) . Then, we have:

Theorem 3.2. Let T be a well-founded theory, then M is a minimal model o f T iff it is abstractly minimal. Here minimality refers to domain minimality or ( P, Z ) -minimality.

392 Churn Jung Liau, Bertrand 1-peng Lin

ProoL The "only if" part is derived directly from Definition 2.1. To prove the "'if" part, assume M is an abstractly minimal model but not minimal. Since T is well-founded, there is a minimal model M' so that M ' < M , and M' is isomorphic with M by abstract minimality of M. However, since M' is isomorphic with M, and there exists a model less than

M,

there must be also a model less than M'. This contradicts the assumption that M' is minimal. Thus, M must be minimal and the result follows. []

Combining Lemma 1.3, Theorem 2.4 and the above theorem, we have the following corollary:

Corollary 3.3.

If T is a well-founded theory, then ABDCir(T) (respectively

ABCir~e.z)(T)) is equivalent to DCir(T) (respectively Cir~e.z)(T)).

As for non-well-founded theories, we still have some intuitively justifiable ground for the definition of abstract minimality. To explain this, we first partition the class of all models for a theory T into equivalence classes according to the isomorphism relation between them. Let [M] denote the equivalence class containing the model M. Then, define [M] < [M'] iff [M] [M'] and there exist M~ E [M] and M 2 E [M'] so that

M l <~(e.z) M2

(or M~ is a submodel of

M2).

It can be verified that < is a well-defined partial ordering on these equivalence classes. Now, we have the following characterization of abstractly minimal models:

Lemma 3.4.

A model M is abstractly minimal iff

[M]

is a minimal equivalence

class under the partial ordering < defined above.

This lemma, though simple, is important since it guarantees that the abstractly minimal models are also minimal in some good sense. Thus, for well-founded theories, abstract circumscription is completely coincident with ordinary circumscription, and even for non-well-founded theories, the notion of abstract circumscription still matches the basic idea of ordinary cir- cumscription.

Furthermore, Example 4 may motivate the following alternative definition of abstract minimality.

A model M is an abstractly (P, Z)-minimal model of T, if for each model M' ~< ~e, z) M, M' has a (P, Z)-submodel which is isomorphic to M.

Adopting this new definition of abstract minimality, the consistency of that example can be preserved, and Theorems 3.1 and 3.2 are still valid. However, the cost is that the axiomatic formulation in Definition 2.3 of abstract cir- cumscription will become more complicated.

3.3. The importance of domain circumscription

In the above sections, we have treated domain circumscription and parallel circumscription separately. According to [13], where McCarthy claimed do- main circumscription can be replaced by predicate circumscription completely, it seems unnecessary to treat domain circumscription independently. McCar-

thy's approach is as follows. First, he introduces a new predicate

all

and got

T"', the relativization of T w.r.t,

all

(see Definition 1.1). Then

DCir(T)

can be

replaced by

Cir(,u.

)(T air U

Axiom(all)) tO {Vx.all(x)}.

This approach, though

feasible in principle, has some serious defects as pointed out by Etherington

[4]. The main issue is that even

Cir(a,,)(T "tl UAxiom(all) tO {Vx.all(x)})

is

consistent,

Circ,,, )(T "u LJ Axiom(all))

U {Vx.all(x)} may be inconsistent. From

the viewpoint of abstract circumscription, we can reinforce the importance of domain circumscription. Consider the following theory T:

3x.Vy.x ~

succ(y),

Vx.Vy.succ(x)

= succ(y) D x = y .

Then, obviously, T has the abstractly minimal model M with IM[ = {0, 1, 2 , . . . } and M[succ]:x---~ x + 1. However,

T o = T a" tO Axiom(all)

is es- sentially equivalent to our previous Example 1 with some modifications. These modifications do not change an important feature of T 0. This {eature is that in

any abstractly

(all,)-minimal

model of

T~, M, M[all]

must be a proper subset

of [M]. Otherwise, if

M[all]

= [M], then by cutting some initial segment of

M[all],

we can get M' so that IM'[ = [M[, but

M'[all]

is a proper subset of

M[all],

so it is impossible to construct an isomorphism between M' and M.

Thus M is not abstract

(all,)-minimal

if

M[all] = [M I.

Then, by Theorem 2.4,

ABCir(,u, )(T"" U Axiom(all)) U {Vx.all(x)}

will have no models even though

ABDCir(T)

does. This example shows that abstract parallel circumscription cannot replace abstract domain circumscription though the former seems more powerful. Thus, a separate treatment of abstract parallel circumscription and domain circumscription is necessary.

3.4. Comparison with other work

In this subsection, we will compare abstract circumscription with closed and nonrecursive circumscription [15] and equality circumscription [16] according to the following points, (i) preservation of satisfiability, i.e., the suitable classes of theories for these circumscription formalisms, (ii) semantic characterization, i.e., what kind of models these formalisms can capture, and (iii) coincidence with the ordinary circumscription.

First, let us review the basic notions of closed nonrecursive circumscription and equality circumscription.

394 ('hum dung Liau, Bertrand l-peng Lin

Mott [15] adds to a theory

T(P, Z)

the following axiom schema, T(@, qt)/x q~ ~< P D P ~< q~, where q~ and qt are tuples of first-order formulae with the restriction that each q~i has no more free variables than Pi has (i.e., closedness) and all symbols in (P, Z) do not occur in any of q~g (i.e., nonrecursiveness). He proves that all consistent first-order theories are suitable for this form of circumscription. However, its semantic characterization is not clear, as pointed out by Etherington [4]. Furthermore, even in the cases of well-founded theories, it is strictly weaker than ordinary circumscription, For example,

3x.P(x)

is a well-founded theory w.r.t, the predicate

P,

but if we apply closed

and nonrecursive circumscription to this sentence it is impossible to derive the results which ordinary circumscription can derive. This shows that open and recursive circumscription is necessary to derive some useful results in some c a s e s .

Equality circumscription mainly aims at circumscribing equality predicate. Because, in the ordinary minimal model semantics, the ~ relation is defined between two models with the same interpretation of function symbols, it is impossible to circumscribe equality directly in this framework. Thus Rathmann et al. [16] present the equality circumscription formalism in a more general setting, i.e., the preferential model semantics [18]. Let M--* M ' denote that there exists a homomorphism from M to M ' where M and M' are models of some theory T, then M is said to be preferred to M ' iff M---~M' but not M ' - + M. Then, they present the axiomatic formulation of equality circumscrip- tion and show that preferred models are exactly the semantic characterization of it. They also prove that equality circumscription preserves consistency for universal and existential theories. Moreover, if two models are isomorphic, equality circumscription will not prefer one over the other, so the theories in Examples 1 to 3 may have preferred models. However, they also provide an example which is suitable for ordinary circumscription but not for equality circumscription. In fact, equality circumscription is essentially incompatible with the ordinary circumscription. In other words, equality circumscription is neither stronger nor weaker than the ordinary one. This is because the preferred models are not necessarily minimal in the ordinary sense. Therefore, equality circumscription can derive some useful results about equality predi- cates, but it may also lose some information about other predicates.

Now, we can compare the three different circumscription formalisms. First, undoubtedly, closed nonrecursive circumscription is best behaved in preserving the satisfiability of the theories being circumscribed. Moreover, it is well known that universal theories are well-founded under ordinary circumscription and because consistent existential theories have finite models, they must have minimal models in the ordinary sense. Thus, since all minimal models are abstractly minimal, abstract circumscription and equality circumscription ap- pear to be equally well-behaved in the preservation of satisfiability according to the present known results. Secondly, abstract circumscription is more coinci-

dent with ordinary circumscription than the other two formalisms are by Theorem 3.2 and Lemma 3.4. However, unlike closed nonrecursive cir- cumscription, the deviation of equality circumscription from the ordinary one is for deriving new sentences about equality, so, in this case, it is a tradeoff, not a weakness. Finally, abstract circumscription and equality circumscription both have clear semantic characterization, while Mott's formalism does not.

Finally, we would like to mention another application of model isomorphism in the context of the closed world assumption (CWA, [17]). A concept similar to o~-categoricity, called weak categoricity, has been used by Jager [6] to provide a sufficient condition for the consistency of CWA. He defined a class of theories, called inductive databases which are the generalization of Horn sentences, and showed that if all countable models of an inductive database D are isomorphic modulo P (i.e., isomorphic in the sublanguage without involv- ing P), then D is consistent under the P-relativized CWA (i.e., CWA applied only to the ground atoms involving P). This result, though not directly related to our work, also shows the potential interest of the notion of model morphism to nonmonotonic reasoning.

4. Conclusion

We have presented the concept of abstract circumscription and minimality in this paper. Instead of changing the set-inclusion ordering among models, we obtain abstract circumscription by relaxing the minimality criteria. Essentially, we let all isomorphic models be in the same equivalence class, and conse- quently, the model whose submodels (or (P, Z)-submodels) are all in the same class is the abstractly minimal one. The properties in Section 3 show that the idea of abstract circumscription is natural and completely matches the original circumscription in the cases of well-founded theories.

Another point we have to mention is that, as in the original circumscription, a complete syntactic characterization of satisfiability of abstract circumscription remains to be decided. What we have provided is a sufficient condition for the satisfiability of abstract circumscription, i.e. to-categoricity. This, though not a syntactic characterization, has been well studied in classical model theory.

In summary, we have improved the satisfiability of the original circumscrip- tion without deviating too far from the minimal model semantics.

Acknowledgement

We would like to thank three anonymous referees for valuable comments, especially the suggestion to compare our work with that in [6, 15, 16[, and to elaborate the proof of Theorem 2.4.

396 Churn Jung Liau, Bertrand l-peng Lin References

[1] P. Besnard, Y. Moinard and R. E. Mercer, The importance of open and recursive circumscrip- tion, Artif. lntell. 39 (1989) 251-262.

[2] C.C. Chang and H.J. Keisler, Model Theory (North-Holland, Amsterdam, 1973). [3] M. Davis, The mathematics of non-monotonic reasoning, Artif. lntell. 13 (1980) 73-80. [4] D. Etherington, Reasoning with Incomplete Information (Morgan Kaufmann, Los Altos, CA,

1988).

[5] D. Gabbay, Modal and temporal logic programming, in: A. Galton, ed. Temporal Logics and Their Applications (Academic Press, New York, 1987).

[6] G. Jager, Non-monotonic reasoning by axiomatic extensions, in: J.E. Festand et al., eds., Logic, Methodology and Philosophy of Science VIH (Elsevier Science Publishers, Am- sterdam, 1989) 93-110.

[7] V. Lifschitz, Some results on circumscription, Tech. Report, Stanford University (1984). [8] V. Lifschitz, Computing circumscription, in: Proceedings 1JCA1-85, Los Angeles, CA (1985). [9] V. Lifschitz, On the satisfiability of circumscription, Artif. lntell. 28 (1986) 17-27.

[10] V. Lifschitz, Pointwise circumscription: preliminary report, in: Proceedings AAA1-86, Phila- delphia, PA (1986).

[11] J. Malitz, Introduction to Mathematical Logic (Springer, New York, 1979).

[12] J. McCarthy, Epistemological problems of artificial intelligence, in: Proceedin M IJCAI-77, Cambridge, MA (1977).

[13] J. McCarthy, Circumscription--a form of non-monotonic reasoning, Artif. lntell. 13 (1980) 27-39.

[14] J. McCarthy, Application of circumscription to formalizing commonsense knowledge, Artif. lntell. 28 (1986) 89-116.

[15] P.L. Mott, A theorem on the consistency of circumscription, Artif. lntell. 31 (1987) 87-98. [16] P, Rathmann, M. Winslett and M. Manasse, Equality and circumscription, Report No.

UIUCDCS-R-90-1615, University of Illinois at Urbana-Champaign (1990).

[17] R. Reiter, On closed world data bases, in: H. Gallarie and J. Minker, eds., Logic and Database (Plenum, New York, 1978).

[18] Y. Shoham, A semantical approach to nonmonotonic logics, in: Proceedings of Logics in Computer Science, Ithaca, NY (1987) 275-279.