Two Results on Default Logic

ABSTRACT

We focus on default logic, a formal­ ism introduced by Reiter to model default reasoning. The paper consists of two parts. In the first one a translation method of non-normal defaults into the normal ones is given. Although not gener­ ally valid, this translation seems to work for a wide class of defaults. In the second part a semantics for normal default theories is given and the completeness theorem is proved.

INTRODUCTION

[Reiter, 1980] introduces a formalism modelling default reasoning. An example of such a reasoning is the inference rule stating "Typically children have parents". In default logic this rule is represented as the following default

child(x): M has-parents(x)/has-parents(x)

Formally, a default is any expression of the form ~(x): M~(x>/w(i), where ~x), ~(i),w(i) are all first-order formulas whose free variables are among those of i=(x1, ··· ,xn). ~(i) is called the prereq­ uisite, ~(i> the justification, and w(xJ the consequent of the default. This de­ fault is interpreted as "for all individ­ uals x1, ··· ,xn, if ~Cx> is believed and ~(x) is consistent with our beliefs, then w(i) can be believed. If OC(i), ~(i) and w<i> are all closed formulas, the default is said to be closed, otherwise it is open.

In default logic the knowledge about a world is represented as a default ~­ ~. i.e., a pair (W,D), where W is a set of first-order axioms and D is a set of defaults. Defaults extend the knowledge contained in axioms. Such an extension provides an acceptable set of beliefs about a world being modelled (see [Reiter, 1980] for details).

To assure the existence of extensions Reiter limits himself to normal theories, i.e., theories all of whose defaults are of the form o(.(i): Mf!(x> /f><x>. Because the class of normal theories has turned out to be insufficient for practical applica­ tions, in [Reiter, Criscuolo, i98iJ the

TWO RESULTS ON DEFAULT LOGIC

WITOLD LUKASZEWICZ

INSTITUTE OF INFORMATICS UNIVERSITY OF WARSAW P.O. BOX 1210 00-901 WARSZAWA, POLAND

more general class of semi-normal theo­ ries, i.e., theories all of whose defaults are of the form cc..Ci>: M(~Cill\w<i>)/w(i), has been introduced. Although these theo­ ries seem to cover all practical applica­ tions, they need not have extensions.

In [Lukaszewicz, i98'J an alternative default logic, coinciding with that of Reiter for normal theories, has been spec­ ified. Although each theory has an exten­ sion in our approach, non-normal theories should be avoided if possible. The reason is that they are computationally more complex than the normal ones.

This paper consists of two parts. In the first one we give a translation of non-normal defaults into the normal ones. Although not generally valid, this trans­ lation seems to work for a wide class of d.etaul ts. In the second part a semantics tor normal default theories is given.

TRANSLATION

The translation we propose is very simple. The first step is to replace any default d=~:Mj!/w by the semi-normal de­ fault d1=~:M$"'w.Vw. Intuitively, this transformation seems to be incontrover­ sial. The only distinction between d and d1 arises from the different applicability criteria for them. Because the criterion of applying d.1 is stronger than that of d, any agent including d into his know­ ledge base, who does not accept to re­ place it by di, considers the applica­ bility criterion for di too strong. Thus he is prepared to apply d when the appli­ cation of di is explicitely blocked. In other words, he considers as possible to apply d when the formula ~ is consistent with his beliefs, while the formula WAr> is not. But in such a case, applying d contradicts its justification. This means that the agent is irrational . Thus any reasonable agent including d into his knowledge base should accept to replace it by di.

The second step of our translation is to replace the semi-normal default di=ot:M(!3-'w)/w by the normal default d2=ot:M(~"wJ/~"w. This transformation is more controversial. Before giving its ap­ plicability criteria let us start by ob­ serving that it is often the case of "Typically if oc. then~"· This observation underlay the method of replacing semi­ normal theories by the normal ones in [Reiter, Criscuolo, 1981]. Consider for example the default stating "Typically ad.ul ts are employed, except when they are high-school dropouts". Formally d i=adul t ( x) : M(-, dropout ( x) 1\ employed (x))l employed{x)

Because "Typically adults are not high­ school dropouts", we clearly can replace di by the normal default

d2=adul t(x): M(..,dropout(x)A employed(x))l -.,dropout (X)t\ employed( x)

In [Reiter, CriScuolo, 1981] di is re­ placed by the pair of normal defaults

adul t(x) : M _, dropout(x) I.., dropout( x)

adult(x)"-.dropout(x): M employed(x) I employed(x)

If all we know about John is that he is an adult, both normal representations of di lead to the conclusion that John is employed not high-school dropout. The difference arises when we additionally know that John is unemployed. The repre­ sentation of Reiter and Criscuolo forces John not to be a high-school dropout, while ours remains agnostic on this point.

Even if "Typically if ct then~" does not hold, our normal representation works if the following weaker condition is sat­ isfied. : "Typically if « and w then~ "· To illustrate this point let us consider the default stating "Typically adults are married, except when they are 21 year olds". Formally

di=adul t (x) : :t.I(married (x)"' 21-old (x) I married(x)

If all we believe about John is that he is an adult, we do not assume that he is not 21 years old. But if we additionally believe him to be married, the conclusion that John is not 21 years old seems to be plausible. In other words, we accept the statement "Typically married adults are not 21 year olds". Note that applying di for John we start to believe that he is married. Thus we can plausibly conclude that John is not 21 years old. Exactly the same effect is achieved when we re­ place di by the normal default

d2=adult (x) : M(married (x)A-,21-old (x)JI married( x)A -,21-old (x)

All the above discussion can be sum­ marized as follows. If d= <:(.. :M ~ lw is any default, then it is always reasonable to replace it by the semi-normal default di=« :M(j3AwJiw. If it is the case that "Typically if ~ and w then f5 ", di can be further replaced by the normal default d2= o( : M(/3Aw)l~ /IW.

SEMANTICS FOR NORMAL DEFAULT THEORIES

We limit ourselves to closed theories, i.e., theories all of whose defaults are closed. Using a technique given in (Reiter, 1980] a generalization to open theories is straightforward.

The id.ea is to view defaults of a theory (W,D) as restricting the models for W in such a way that ·

1. Any restricted set of models for W is the set of all models for some extension for (W,D).
2. If E is any extension for (W,D) then there is some such restricted set of models for W which is the set of all models for E.

Some preliminary termtnology. Let X be a set of first-order models. We sa1 that a formula ol. is X-valid (X-satis·.tl6ble) iff~ is true in all models (in some mod­ el) of X. We say that a closed normal de­ fault ~ :Mwlw is X-applicable iff ex. is X-valid and w is X-satisfiable.

We begin by observing that each closed normal default can naturally be regarded as a mapping from sets of models into sets of models. Formally, if X is a set of models and d= o(. :Mwlw is a closed nor­ mal default, then the set d(X) is given by

Intuitively, X-valid and d(X)-valid for­ mulas can be interpreted as sets of be­ liefs before and after the application of the default d, respectively.

Imagine an agent reasoning on the ba­ sis of some closed normal default theory A=<W,D). His initial set of beliefs should be identified with Th(W) or, from the semantic perspective, with the set of all models ror W. At each step he chooses a default and tries to apply it to the current set of his models X. The new set of the agent's models is d(X). The new set of his beliefs is the set of all X­ valid formulas. Assume that the agent is able to repeat this process infinitely. It can happen, perhaps after applying in­ finitely ~any defaults, that the set of the agent s current models is stable, i . e . , tor each dED, d(X) aX, As we shall see, each stable set of models resulting from such a process characterizes some extension for A. Moreover, each extension for A is characterized by some such sta­ ble set of models.

!he formal details are these. Let (di) be a sequence of defaults, and sup­ poBe that X is a set of models . By (di>X

we denote the set of models given by

Note that if (di) = d 1 , ··· ,dn, then <di)X = dn(d 0 _ 1 ( .· (d 1 (X)) · · ).

Let A=(W,D) be a closed normal theory, Let X be the set of all models for W. We say that a set of models Y is stable with respect to A iff

• ( Si) Y=(di) X for some sequence ( di) such that each dieD.
• ( S2) For each dED, d(Y)= Y,

Theorem 1: Let A be a closed normal de­ fault theory, and suppose that a set of models Y is stable with respect to A. Then Y is the set of all models for some

extension for A.

f!.Q.Q.!.(outline) : Y=(di)X for some ( di), where X is the set of all models for W. We can assume that (d 1 ) is infin­ ite (otherwise, i.e., if (di)=d 1 , .. ,d, define the infinite (d{) by n di=di for i=1, ·· ,n, di=d 1 for i~n),

It follows that Y=n~x , where the sets Xj were d.efined earl~e~. Let F 1 ( i ~0) be tne set of all Xi-valid formulas . Assume t hat di=~i:1mi/wi. It is easily verified that

• ( 1) F 0 =Th(W}.

• ( 3) E= \fo'F i .

It is easily checked that Y is the set of all models for E. Thus it remains to prove that E is an extension for A.

Define

In view of Theorem 2.1 [Reiter, 1980] it is sufficient to show that E=\JEi . By induction on i, it is easily proved that for each i~O we have

• ( 4) Eir; E and (5) F i<; \)Ei From (3), (4), (5) we immediately have E=\JEi what completes the proof of the
• theorem.

Theorem 2: Let E be an extension for a closed normal default theory A=(W,D), and suppose that X is the set of all models for W, Y is the set of all models for E. Then Y is stable with respect to A.

.f!:.2.2! (outline) : Define

GD={.(«.zMw/w)E;D: oe.EE, -.w~E}, CONSEQUENTS(D) = { w: ( ouMw/w)ED}.

In view of Theorem 2 . 5 [Reiter,1980) we have E=Th(Wv CONSEQUENTS(GD)). Consider two oases .

1. GD-{}. ~ke the empty sequence of de­ faults. It is clear that <.)X·Y, and
2. d(Y)=Y for each d€D. Thus Y is stable.
3. GD:#:{J. Let d1, ..· ,dn (d1,d2, ··· ) be any sequence of all elements of GD. Define d'i., . ·· ,dh (d'i,d'2, .·· ) by

I d1 ·dj where j is the smallest integer such that dj is X-applioable

Given dl, .·· , d'i

di+1 =dj where j is the smallest integer such that

• I I (il dj is (d1, ·.· ,di)X-applicable (ii) for each 1~k~i, dj;.dk 1

It is readily verified that (di 1 ) is well defined, and that the elements of (di') are those of (di). Because for each dED we clearly have d(Y)=Y, to complete the proof of the theorem it remains to show that (df)X=Y. It is easily proved that (d1~ ·· d1)X is the set of all models for Th(Wv{w1 1 , ... ,wi 1 }) where wl is the consequent of dj~ It follows there­ fore that (dt>x is the set of all models for Th(Wv CONSEQUENTS (GD)). Thus ( di'~X=Y.

This completes the proof of Theorem 2.

ACKNOWLEDGMENTS

I acknowledge many discussions with Barbara Dunin-K~plicz regarding this work.