A Functional Approach to Non-Monotonic Logic

1. Introduction and overview.

Non-monotonic logic may be studied either in terms of non-monotonic inference rules (Reiter 1980, Goodwin 1984) or in terms of non -monotonic operators in the language such as the Unler1 operator (Sandewall1972, McDermott and Doyle 1980). In this paper we pursue the former approach.

The concept of fixpoints is central to the study of non-monotonic logic: for a given set 11 of propositions and a given set of rules, we are looking for an extension i.e. a set 11 ' of propositions which contains 11 as a subset, and which is a fixpoint of the set of rules. Fixpoints are also used in the denotational semantics approach to the theory of programming languages (Scott 1970; see also e.g. Manna 1974, Stoy 1977, Blikle 1981). There, tbe recursive definition of a function is viewed as a functional, i.e. an operator on partial functions, and the function is viewed as the fiXpoint of the same functional.

In this paper we propose that the functional approach that is taken in denotational semantics, can be adapted and serve conveniently for the study of non -monotonic logic. This is attractive since logical inference is often viewed as a high-level form of computation, and since computational inference often needs to be non-monotonic. The power of this approach is demonstrated through simple proofs of some of Reiter's (1980) results for normal default theories. Other results in the paper apply to non-monotonic rules in general.

Although several f!Xpoints may exist in the monotonic case, the criterium of being 11 minimlll fixpoint (i.e. all other fixpoints are 'larger') is a sufficient one, and there is only one minimal fixpoint, which is then th.e lealt fixpoint. Other, larger fixpoints contain spurious information which is not warranted by the given facts and

Th.i1 reu11rch. 111111 1pouoretl b11 th.e SUJedi1h. Bo11rd of Tech.niclll Development.

inference rules. In the case of non -monotonic rules, there is of course in general no single least fixpoint, and the criterium of fixpoints being minimal is not sufficient: there may be minimal fixpoints which have the given set of propositions as a subset, but which still can not be reached or approached (in the sense of a limit) by any derivation using the given set of rules. In this paper we define a concept of tlpprotJch.able fiXpoint, which is stronger than the concept of minimal fixpoint, and which is proven to be a sufficient condition for the existence of a derivation that reaches or approaches the fiXpoint.

The following formal machinery is used. We start from two domains, a domain L whose elements are called formu.ltJI, and a domain J of tru.th.-vlllu.e.. V is the domain of vlllu.ation1 i.e. continuous functions from L to J.

A set of axioms is seen as a valuation that maps some formulas (the axioms) to t (for true) and "all" other formulas to a (for undefined). (Exception is made for the top element of the domain L). Derivation of theorems is done by proceeding from the initial valuation to others where some formulas change value from a to tor f (for false). A set of inference rules corresponds therefore to a binary relation on valuations, i.e. a subset of V x V, which we shall call a dedu.ction. A tleri1111tion using a deduction F is a sequence of valuations,

where

Deductions in this sense can be used for characterizing both proofs and semantics, provided that there are syntactic functions and predicates on L which characterize the abstract syntax of the language. This includes predicates which indicate whether a formula is a conjunction, a disjunction, an implication, atomic, etc., as well as functions e.g. for composing the conjunction of two other formulas . The conventions for calculating the truth-value of a propositional expression may then be seen as a deduction F where F(v,t') e.g. in the case where:

11(11) = t

v(b} = t

v(11 II b) = a

v'(1111b)=t

11 '(z) = v(z)

for all other formulas z.

Here a II b refers of course to the formula obtained by composing the formula 11, the conjunction operator, and the formula b.

The concepts and results of conventional logic can easily be re-phrased along these lines. In the case of non -monotonic logic, there is however a particular advantage with doing so: a non-monotonic rule 4 A Unle11(b} -+ c can now be seen as a deduction F which allows F{·,·') e.g. in the case where 11{4) = t v(b} =a v(c) =a v'{b) =I ·'(c) = t v'(z) = v(z) otherwise.

In other words, one derivation step using F will change the truth-values of the two formulas b and c at the same time. This is different from the viewpoint in ordinary logic, where the intuition is that each formula or proposition has 'its' truth-value, so that rules of inference may contribute additional information about 'the' truth of a proposition. In non-monotonic logic, we must be prepared to recognize multiple extensions of the given axioms, or multiple fixpoints of what is here called a deduction. It therefore makes sense to correlate assignments of truth-values in the way just described.

Suppose now, in the above example, that b has already been assigned the value t (maybe by an ordinary rule that does not use Unle11), and therefore we have v(b) = t. In order to deal with such cases it is convenient to consider two deductions F and G as follows. For G there is no ti' such that G(11,v'l. This expresses the intended meaning of Unle11. For F we take the view that information has now accumulated both that b is t and that it is/. A new truth-value k is introduced for this purpose, and there is a v' such that v'{b} = k and F{v,11').

We therefore obtain a four-valued logic, with the truth-values t, /, 11, A:. This logic has previously been studied by Belnap (1977). One can think of these truth -values as the ones assigned by committees (cf. Borgida et a!, 1984): if some members of the committee assign the value t to a proposition and the others assign the value a, then the committee assigns t, but if some members assign t and others assign /, then the committee assigns the value k to the the proposition. 'Committees' are a convenient metaphor whenever there are several parallel sources of knowledge, such as when several inference rules are being used.

The deductions G and F are in general related so that G ~ F, and the difference occurs in cases like the one just discussed, where G 'refuses' to use a rule if it means that the non-monotonic antecedent (the formula given as argument to Unle11) then obtains the truth-value lc.

This has been an outline of the key ideas of the paper. We now proceed to the systematic treatment.

2. Monotonlelt:y and ftxpolnt· for relation·.

The domain J contains the elements { a,t,/,k} as already discussed, with the partial order !;;;; described by the following figure:

Thus it is a flat lattice with a as the bottom element and k as the top element.

The flat domain L is called a l·nguge and its elements are called formul··, with lb as the bottom element and It as the top element.

A v41ution is a function "from L to J which satisfies v{lb} = a v(lt} = k which in particular guarantees that valuations are continuous (and therefore monotone) functions. A valuation is con·istent iff no formula other than It is mapped to lc. Valuations form a lattice with the partial order !;;;; defined in the following way:

" !;;;; v' iff (Vz) v(z} !;;;; 11'(z} We say then that "' is an eztennon of 11, and that 11' is abo11e 11 (with respect to !;;;;). A valuation 11 is finite iff 11(l} = a except for a finite number of formulas I.

A dedaction is a binary relation on V, i.e. a subset of V X V. The operation U and the relation ~ is therefore defined on deductions. The partial order !;;;; could also be extended to deductions, but that will not be needed in this paper.

A deduction F is con·er114ti11e iff F{ll,ll'} -+ II!; II' which can now be written F~!;;;

A cll4ill is a sequence of valuations where

11o!;;;; 111!;;;; ... It is well known that each such chain has a l.u.b. in a lattice. A tlerill4tion from · to ·' using a conservative deduction F is a chain where

Notice that we say a derivation -- to ,· -- even in the case of an infinite sequence where 11' is never reached, just approached as a limit.

A deduction F is monotonic iff "!;;;; ,, A F(·,11)-+ (311?(F(v',11') A 11!;;;; 11, It is line4r iff F{11,11) -+ F(11 U z, 11 U z} Clearly every linear deduction is also monotonic.

A valuation 11' is a fizpoint of a deduction F iff F(v',v") --+ w' = o" Thus in particular 'II' is a fixpoint if F does not allow any 'successor' ·"· For a given valuation 17 and deduction F, we shall be interested in fixpoints ofF above 'II, i.e. fixpoints ofF which are ;;;! 17.

A fJxpoint of F above 17 is minim41 iff no 'smaller' (by !; ) fix point exists for the same F and 17.

What has been described so far uses some of the tools of denotational semantics, but in a diffferent fashion than usual. The differences are dictated by our desire to deal with logic using these tools. The reason for that, again being the wish to consider non-monotonic deduction. Anyway, the obvious properties of the monotonic case follow easily, in particular:

Proposition 1. a) A conservative, monotonic deduction has a unique least fixpoin t above each 17.

b) The l.u.b. of any derivation from 17 is!;;;; the least fixpoint.

Proof a) Consider a set { ";} of fixpoints of F above ·· We wish to prove that 11' = n ";is also a fixpoint of F. Suppose

By monotonicity, for each 11 i there exists a valuation zi such that

Since each ";is a fiXpoint, we have

11. = z .

I

I

and therefore

and since F is conservative,

b) Let flO' fl 1 , ... be a derivation using F, and let 11* be the least fixpoint of F above · 0 . By induction, it is easily proven that fl. c ·· .-

for each i. []

The following concept is also of interest in the non-monotonic case:

3. Linearity and compaetneu.

There are two significant properties for deductions formed using a number of rules: linearity and compactness. This section studies consequences of those properties. Linearity was defmed in the previous section

Propolilion t. If F is a conservative, linear deduction, and there exists a derivation from fl to fl' using F, then for every 11 such that

there exists a derivation from 11 to 11' using F.

Proof Let the derivation from fl to fl ' be

where "o = fl. The sequence

is a derivation using F, and by the assumptions we have

and the J.u.b. of the sequence is 11'. []

Propolilion :J. If F is a conservative, linear deduction, and there are derivations from fl to 11' and from 11 to e· using F, then there is a derivation from 11 to e' U fl" using F.

Proof. Let the derivations of fl ' and 11" be:

The proof of proposition 3 generalizes easily:

Propolilion ,1. If F is a conservative, linear deduction, and there are derivations using F from fl to each member of a non -empty (possibly infinite) set W of valuations, then there is a derivation from fl to the J.u.b. of W.

Proof (outline): use the same technique as in the previous proof, but select some ordering of the members of W (presumed denumerable), and construct the new derivation in a triangular fashion, so that it may use the first j terms of the derivation for the f~nt member of W, the first j · 1 terms of the derivation of the second member, etc. [I

The other important property is compactness. A deduction F is compacl iff whenever F(e, fl'} there exist some finite valuations 11, 11' such that

We shall see in a moment that the deductions obtained from 'ordinary' rules of inference are compact, but f~nt let us identify a consequence of compactness:

Propolilion 5. If F is a conservative, linear and compact d.,J u<: tinu, and there are derivations using F from · to e' and from e' to fl", then there is also one from fl to fl " .

Proof Let the derivation from · to ·' be

and let the derivation from fl ' to ·" be

where for each i ~ 0 there are some finite 11, z. such that ··

Construct now a sequence of valuations as follows:

where the n are selected so that

for i ~ 0. By compactness such a sequence must exist, and by the linearity the sequence is a derivation using F, and its l.u.b. is dearly v·. [)

We can now proceed to introducing the counterparts in our system of inference rules.

A kerllel is a pair <r,v'> where 11 and 11' are finite valuations, and 11 ~II'.

Kernels may be used for expressing how the truth-value of a composite expressions follows from the truth -value of its component(s), or vice versa. One such example was given in the introductory section. For another example, the rule that if o is true then -.a is false, is expressed by the kernel <v,11'> where

The direct reolizolioa of a kernel <11,11'> is the deduction formed as

11(11) = v'(o) = t v(-.o) =a · 11'(-.o) =I {<· u 11, ·' u 11> 1 11e V}

In other words, the direct realization of a kernel < e, ''> is the set of all possible pairs <11, 11'> such that 11 ~ 11 and 11' = 11 U 11'. Each such pair characterizes a derivation that is allowed by the kernel, i.e. if the preconditions · are satisfied in 11 then the conclusions 11' may be accumulated to 11 giving 11'·

The direct realization of a set of kernels is defmed to be the union (using u) of the direct realizations of the individual kernels. This has the effect that from each valuation 11 there are several successors, corresponding to the choices of which derivation step to take. From this definition it follows:

Propolitiora 6. The direct realization of a set of kernels is conservative, linear and compact.

4. NM-Rule·.

We shall now characterize those deductions which correspond to (what we intuitively think of as) a set of non-monotonic inference rules.

Following Goodwin (19S.) approximately, an NM-rllle is a triple

<M,N,C> of finite sets of formulas, where M is the moraotollic Glltece4ellfl, N is the raora-ma·oto·ic o.tecetleatl, Cis the coraregaellfl.

The idea is that if each member of M is true, and each member of N is false or undefined, then each member of C can be inferred to be true. At the same time, the assumption is made that all members of N are false.

Each of M, N, and C may be the empty set. If N is empty we have a monotonic rule. If C is empty we have what Reiter (1980) calls a normal default rule.

The kernel that correrpo·tl· to an NM-rule <M, N, C> is the pair

e(m) = e'(m) = t for all min M ·'(·) =I for all · in N ·'(c) = t for all c in C.

<11,11'> where and all other values are a.

Thus non-monotonic rules differ from monotonic ones, partly by causing ·ererol formulas to change their truth -value as one inference step is performed. A possible objection against this way of dealing with non-monotonic antecedents, is that the resulting valuation should differentiate explicitly between that information which has been obtained as a consequent, and that which was 'merely' assumed in order to be able to apply the rule, i.e. the assignment to the non-monotonic antecedent(s). We however view that as a book-keeping issue, which need not concern the formal treatment of the deduction as such.

The direct realization of an NM -rule is the direct realization of its corresponding kernel.

We let H be that deduction which performs the obvious deductions of conventional, propositional logic. Thus if a valuation 11 satisfies

11(11 II b) = t then the valuation e·(11) which is the least fixpoint of H over II (proposition 1), satisfies

e·(11}{o) = e·(11){6) = t (unless a contradiction occurs in which case e·(lj = k for alii). We work presently on a more specific definition and analysis of this deduction H.

We want the direct realization of a set of NM-rules to be the deduction which has as subsets the realizations of each of the rules, but which is also able to do trivial derivations of truth-values. We therefore formally define the direct reolizotio· of a ret of NM -rules as H U (the union using U of the direct realization of each of the rules). Clearly the direct realization of a set of NM-rules is lin t·a.r , conservative, and compact.

The renricte4 reolizotiora of an NM-rule <M,N,C> is a subset of the direct realization of the same rule. It is obtained by excluding all those pairs <v,v'> where v'(·) =A: for some "eN. Notice that pairs <r, ·'> where ·'(c) = k for some c E Care not excluded, unless some ·'(·) is also A:. The restricted realization of a set of NM-rules is obtained as the union (using u) of Hand the restricted realization of each of the NM-rules. The restricted realization is conservative and compact but not monotonic (and therefore not linear).

An example may be useful at this point. For the examples we assume that the language consists of the formulas { o,6,c, ... }. A valuation will be written as ]z,11, ... ] meaning the valuation 11 where 11(11) = z, t{b} = 11, etc. If either of the sets in a rule is a singleton, then the curly brackets around it will be omitted, and the empty set will be written as a dash. Thus <o, -, c> is an example of a rule, meaning the same as <{o}, {}, {c}>.

Eumple 1. Suppose we have the following rules: <-, o, 6> <6, -, c> Informally, this says: 6 holds unless o is known to be true; if 6 then c. The restricted realization G of this set of rules satisfies: G(J a, a, a], [/,t, a]) (this uses the rule "6unless o") G([l,t,a], [l,t,t]) (this uses the rule "if 6 then c") and [l,t,tJ is also a fixpoint for Gover [a,a,.j.

If we ~tart instead from a valuation where o is known to be true, e.g. r = [t,a,a], there is no valuation v' such that G(t,fl'). The direct realization F of the same set of rules holds of course for the same argument pairs as G, but also

F([t,a,a], [k,t,.j) since the direct realization will proceed even if it introduces a contradiction. The valuation [t, a, .j is therefore a fixpoint for G, but not for F. However, it is a maximally consistent extension of [ t, a, a] w.r.t. F.

5. Correct extensions, Approachability.

Throughout this section, we assume that 11 is a valuation, and R is a set of NM -rules whose direct realization is F and whose restricted realization is G.

A valuation 11 ' is termed a correct ezteruion of 11 w.r.t. Riff:

1. 11' is a fixpoint of G above 11 (meaning in particular that II !;;; 11')
2. 11' is consistent
3. there is some derivation from 11 to 11' using G.

(Remember that the phrase /11' is an extension of 11/ means simply that 11' ;;! 11) . The notion of correct extensions expresses stringently what are the desirable fixpoints for given 11 and G. If 11' is not a flxpoint then some additional aer1vauon steps rema.m to l>e performed. If 11 ' is inconsistent it is for either of the following reasons: a) 11 is inconsistent

b) the set of NM-rules implies an inconsistence (e.g. if 11(4) = t and one of the rules is <-, -, ~ll>)

c) some non-monotonic antecedent was assumed to be/ early during the derivation, and later in the derivation we had an NM-rule with the same proposition as a consequent, which invalidated the assumption.

Finally, if there is no derivation from 11 to 11 ' then 11' is 'unfounded', like a non-minimal f!Xpoint in the monotonic case.

The third condition in the definition corresponds to Goodwin's requirement of well-foundedness. The above formulation is however problematic in that it refers to the existence of a derivation. By contrast, the minimality requirement on a fixpoint need not refer to derivations: it just states that no 'smaller' fixpoint exists. We would similarly like to have a static condition, which guarantees the existence of a derivation, instead of having to prove its existence whenever needed. The remainder of this section will give such a result.

Although the definition of correct extensions uses G, the deduction F provides a partial characterization of them, and will be used as a tool:

Propolition 7. Each consistent fixpoint of G above 11 is a maximally consistent extension of 11 w .r.t. F.

Proof. Follows easily from the definition of G from F, since F(11,11'l11 ~�(11,11')

implies that 11' is inconsistent.

The converse does not hold, i.e. there are maximally consistent extensions of 11 w.r.t. F which are not flxpoints of G over 11. This happens in those cases where a truth maintenance system has to shift IN nodes to OUT status. Consider

Eumple t . Suppose we have the following NM-rules:

<-, ll, b>

<·,·,a>

Then I/, t] is a maximally consistent extension of !a, a] w.r.t . F, but G(lf, tJ, !A:, t]).

Not every set of NM -rules has a correct extension:

Eztlmple 9. Consider the NM-rules

<-,a, b>

<b, -, a>

Then of course

G(l a, a] ,1/,t])

G(!!,t],!A:,t])

and !a, a] does not have any correct extension w.r.t. these NM-rules.

Some of the propositions in earlier sections can now be extended to apply to the realizations of NM -rules. The basic idea is to first use those results for F, and then to transfer the result to G by introducing a consistency requirement.

Propolition tA. If 11' is a correct extension of 11 w.r.t. R, then for every 11 such that

there exists a derivation from 11 to 11' usiug <1.

Proof. According to proposition 2 this holds for F. However, it follows from the defmition of G that if F{z,z') and z'.is consistent , then G{z,z'). Since 11' is consistent, so must all intermediate steps in the derivation from 11 be, because G is conservative. Therefore we have a derivation from 11 to 11' using G. IJ

CoroUar11 ("minimality of extensions· correct extensions of 11 w.r.t R, then Reiter). If 11' and .,· are

Propolition SA. If there are derivations from 11 to 11' and from 11 to 11" using G, and 11' U 11" is consistent, then there is a derivation from 11 to 11' U 11" using G.

Proof follows directly from proposition 3.

CoroUar11. If 11' and 11" are distinct correct extensions of 11 w.r.t . R, then 11' U 11" is inconsistent.

This corollary subsumes Reiter's (1980) ·orthogonality of extension· theorem. - Proposition 4 of course extends similarly.

Let us return now to the issue of the third criterium in the definition of a correct extension. This requirement can not be omitted, since that would allow flXpoints for which there is no support. For example, the valuation !t,a,u] is a consistent fixpoint of Gin example 1 above. In the monotonic case, such flXpoints are eliminated by the requirement to be minimal, but that requirement is not sufficient here since !t,a,a] is indeed a minimal fixpoint in the example (no 'smaller' f!Xpoint exists). However, we can substitute instead of the third requirement another one which is similar in spirit to minimality, as follows.

A fixpoint 11' of Gover 11 is called llpproachable from 11 iff

II!;;; 11-< 11'- (311,(11-< 11' !;;; 11' II G(y,y')) For lack of adequate characters in the font , -< is used for strict !;;; i.e. excluding equality. Intuitively, this says that whenever we are on the path from 11 to 11', there is some step allowed by G that will take us closer to 11 '.

This concept is a strengthening of the concept of least f!Xpoint, since the definition directly implies:

Propolition 8. If 11' is an approachable flXpoint of Gover 11, then it is minimal.

It is easily seen that the least fixpoint !t,a,a] in example 1 is not approachable. This approachability condition can replace the third condition in the definition of the correct extension, since:

Propolition 9. If 11' is a consistent f!Xpoint of G over 11, and 11 ' is approachable from 11, then it is a correct extension of 11 w.r.t. R.

Proof. 11 ' immediately satisfies the first two conditions for being a correct extension. It remains to show that there is a derivation from 11 to 11' using G.

Suppose this were not the case, i.e. every chain from 11 whose members are !;;; 11 ' (the existence of at least one such chain is guaranteed by the definition of 'approachable') has a l.u.b. 11 -< v'. Let v· be the l.u.b. of all such II· By proposition 4 there is a derivation from II to 11". If DOW v· -< 11', consider the 11' whose existence is guaranteed by the approachability, such that

The derivation step from v· to 11' must have been obtained using the extension of a kernel <z, z'> such that z !; 11", and z' is not !; 11". By compactness, in any derivation,

of 11" there must be some element z such that z C z . But then n - n there is also a derivation of z U z', which is not !; 11". This is a .. contradiction. (]

In this way we have obtained the desired counterpart of the fixpoiut criterium of the monotonic case.

6. Normal default rules.

Reiter (1980) introduces the concept of n.ornull tlefnlt rale·. He shows that every normal theory has an extension (in our terms: a correct extension), and proves semi-mouotouicity, i.e. a larger set of normal default rules has a larger extension. His results, which are given with fai.rly complicated proofs, can now be obtained more easily from the material presented above.

A n.ormlll defa.Zt rale is au NM-rule of the form <M, { n.}, {}>.

If vis a valuation then 11· is the (obviously unique) least fixpoiut of H over v. Clearly the · operation is monotonic. The valuation v is fallll con..i.ten.t iff 11· is consistent.

A valuation 11 is ·aturatetl w.r.t. a formula a iff 11(a) = v·(a).

Let G be the restricted realization of a set of normal default rules. A derivation using G is cntiou iff in each derivation step < v, 11 '> that uses a rule <M, { n.} , {}>, vis saturated w.r.t . 11. The idea is that in a cautious derivation it is n.ot possible to have the following scenario. Let the formula c be -.a. Start from the valuation [a, a, ~ . i.e. -.a is false but the conclusion that a is true has not been drawn. Use the extension of the NM-rule <·, a, b> to derive [/, t, k After that, use the deduction H which administrates simple truth-value calculations, to derive [.1:, t, k The cases that we exclude by being cautious in this sense are the ones where au implementation would have to backtrack, or (in a truth-maintenance system) shift propositions from IN to OUT status, because a non-monotonic antecedent which was temporarily accepted because no proof had been bound so far, later had to be retracted when a proof was found.

Since H does derivation steps according to propositional logic, one can derive a valuation that is saturated w .r.t. n. in a finite number of steps. It follows:

Propontion. 10. Let 11 be a consistent valuation, and let G be the restricted realization of a set of normal default rules. Each step in a cautious derivation from v using G, is fully consistent.

Proof We first prove that any step is consistent. By the definition of restricted realizations, a derivation step using a normal default rule can not introduce .1: into the valuation. Suppose a derivation step according to H in a cautious derivation does go from a consistent to an inconsistent valuation. Let n. be the non-monotonic antecedent of the most recent derivation step, v' to 11", that uses au NM-rule. We must have 11'(n.} = 11, 11" {n.} = /, and 11'{1) = v· {1} for all other formulas L (By the definition of restricted realizations, we could not have had v'(n.) = t, 11" (n.) = .1:}). But by a familiar result of propositional logic, if there was a derivation using H from 11" to a contradiction, there must have been a derivation using H from 11 ' to a valuation 11 where 11(n.} = t, which means 11' was not properly saturated. Contradiction.

The full consistency follows easily, which completes the proof. []

CoroUar11. If there is a cautious derivation from 11 to 11' using G, then v' is fully consistent.

Propontion. 11. If G is the restricted realization of a set of normal default rules, and there is a derivation from a valuation 11 to a fully consistent valuation 11 using G, then there is a cautious derivation using G from 11 to some 11' such that 11 !; 11' !; y·.

Proof We prove by induction on the derivation of 11, using the monotonicity of F, that there is a derivation using F from 11 to some such II '· (Just saturate sufficiently before applying each rule). But since 11· is consistent, so is 11', and the derivation using F is also a derivation using G. (]

The main result is now:

Propontion. lt. If 11 is a fully consistent valuation, and G is the restricted realization of a set of normal default rules, then 11 has a correct extension w.r.t. G.

Proof Let W be the set of l.u.b. of cautious derivations from v using G. By the corollary of proposition 10, each member of W is fully consistent. A subset Y ~ W is called mazimall11 con.·i.ten.t iff the l.u.b. of its members is fully consistent, but the l.u.b. of every strict superset of Y which is still a subset of W, isu 't fully consistent . Consider some maximally consistent Y (it is clear that some exist, although maybe Y = W) . Let 11 be the l.u.b. of Y. Clearly 11 is a fJXpoiut of H, i.e. 11 = 11·. According to proposition 4, there is a derivation from fl to y, and by proposition 11 there is then a cautious derivation from v to some 11' which is between 11 and y·, so 11' = II· There can however not be any derivation from 11 using G, except the trivial derivation consisting only of y, since otherwise Y would not be maximal. Therefore 11 is a fixpoiut for G and a correct extension. []

Propontion. U (semi-mouotouicity): Let 11 be a fully consistent valuation; let R' ~ R" be two sets of normal default rules; and let G' ~ G · be the restricted realizations of R' and R ·. If 11 ' is a correct extension of v w.r.t. G', then there exists some correct extension v· of 11 w.r.t . G" for which 11' !; 11".

Proof. let 11 be a correct extension of 11 ' w.r.t . G". Since using G" there is a derivation from v to v ', and a derivation from v' to 11. there is also a derivation from v to 11 (proposition 5). Let W be the set of l.u.b. of cautious derivations using G" from v to, or passing through II· Proceed as in the previous proof. [] .

Reiter's proofs for the last two results are considerably more involved. The functional approach taken in this paper makes it possible to reason more abstractly, and therefore more concisely.

7. Conclusion.

The functional view, starting with the lattice of four truth-values (including .1: for contradiction) makes it possible to deal with non-monotonic logic on a high level of abstraction, avoiding tedious proofs, and at the same time offers the strong intuitions of partial orders, lattices, and fJXpoiuts.

Aeknowledgementa.

I wish to thank Jacek Leszczylowski for his constructive comments on an earlier version of this paper, and Brian Mayoh who brought Belnap's paper to my attention. The term 'conservative' was chosen to conform to the terminology in a manuscript for a paper by Allen Brown, who discussed 'belief conserving' rules of inference.

References.

Belnap, Nuel D.: "A Useful Four-Valued Logic". In: Dunn and Epstein, "Modern Uses of Multiple-Valued Logic", Dordrecht, 1977.

Blikle, A. (1981): "Notes on the Mathematical Semantics of Programming Languages·. Report LiTH-MA T·R-81-19, Mathematics Department, Link!Sping University, 1981.

Borgida, A. and T. lmielinski (1984): "Decision Making in Committees-- A Framework for Dealing with Inconsistency and Non-Monotonicity·, Proceeding· of AAAI Non-Monotonic Retnoning Worbhop.

Goodwin, J . (1984): "WATSON: A Dependency Directed Inference System·. Proceeding· of AAAI Non-Monotonic Re4·oning Worbhop.

Manna, Z. (1974): "Mathematical Theory of Computation·, McGraw-Hill Book Company.

McDermott, Drew, and J. Doyle (1980) : "Non-Monotonic Logic I", Artifici41 Intelligence, Vol. 13:1, pp. 41- 72.

Reiter, R. (1980): "A Logic for Default Reasoning", Artijici41 Intelligence, Vol. 13:1, pp. 81-132.

Sandewall, E. (1972) : "An Approach to the Frame Problem, and its Implementation". In: Meltzer, B. and Michie, D. (Eds), M4clt.ine Intelligence 7 (Wiley, New York, 1972), pp. 195-204.

Scott, D. (1970): "Outline of a Mathematical Theory of Computation", .ltlt. Anna41 Princeton Conf. on Inform4tion Science· 4nd Su.tem., pp. 169-176.

Stoy, J. (1977): "Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory", The MIT Press.