Schlechta K. Nonmonotonic Logics: Basic Concepts, Results, and Techniques

156 CHAPTER 5. THEORY REVISION AND PROBABILITY

of K), the more drastic and coarse a contraction will be; the more fine-grained it

is (in the other extreme K itself), the more we approach the above completeness

result. This is made precise in Proposition 5.23, which, basically, shows that

splitting an axiom r into {~b V 05, ~b V 705} will decide 05, i.e. give completeness

with respect to r

Consider now theories T, T! .... in some finite s C_ s It is natural to define r,(T)

:= E {#(g(t)): dorn(t) : s t

b

r}. (t b T means, of course, t(05) = true for all

05 E T, see Remark 5.20.) In other words, t,(T) is the sum of the probabilities of

all s t that make all 05 E T true. The more specific a theory is, the less

likely it is, too: T C_ T/ ~ u(TI) <_ t,(T), and the empty theory has probability

1. On the other hand, we are interested in "good choices", i.e. we prefer 05 to -~05

if u(05) > u(-~05). So t, will be a good measure only for theories of the same level

of specificity. In other words, K - A (here, K - A means some contraction of K

with respect to A) cannot sensibly be the u-maximal Kt C__ K such that K/~/A,

as this is always the empty theory.

A better choice might be a r-maximal one (if it exists) among KA :: {K/C K

maximal: K/k/A, K/is F-closed}, this is again "maxichoice contraction".

But there is a problem to maxichoice contraction, pointed out in lAMB2]: For

any K1 E Ka, A E K, Th(I(~ u

{~A})

will be a complete theory. (The proof

is very simple: Let B be given. As A E K, AVB and AV-~B are in K.

Suppose A V B r K/, A V -~B r KI. As A V B 6 K/, by maximality there is

Co E Kt such that Co A (A V B) b A, and as A V -~B r Kt, there is C1 E K/with

U1A(AV-,B) t- A. Thus, for C := CoAC~ E Kt, CA(AVB) t- A, CA(AV-,B) F A,

consequently C A B F A, C A -~B b A, and C t- A, contradicting C E K! E KA.

Thus, A V B E Kt or AV-~B E K6 and KIU {-~A} b B, or Kt U {-~A} b -~B. )

We now show that this problem essentially carries over to theory revision based

on axiom sets too.

So far, we have examined theories without any specified axiom system generating

the theory. In the following, we consider pairs < K, X >, where X is an axiom set

for K. Define KA, X := {< Kt, X1 >: X/C X maximal, X/t7' A, K/= Th(Xt)}

and choose K-A as a u-maximal < Kt, XI > from KA, X (if possible). Consider

nOW <~ I(, X 1 >, <~ /(, X 2 ~>, w}lere X l :--- {05, 05 ---+ ~), ~},

and X2 := {05, 05 --* ~b}.

In both cases, we can infer ~b, and the resulting theories are the same. Suppose

we now retract 05 -+ ~b. In case [, it is very sensible to uphold ~b, whereas in case 2,

it will not be a good choice. (This example can be found analogously in [GM88]

and [FUV83].) So we are highly dependant on the syntactic form of the axioms,

and this is certainly not very desirable. As another example, consider revising a

theory which is given by the axiom

sets {al, a~]. or

{a I

/~, a2}.

So revision may

give different results ({al} or {a2} vs. the empty theory), which is a doubtful

outcome. To avoid this influence of the syntactic form, we might split the axioms

as far as possible to obtain optimal results. This procedure, however, approaches

completeness, as the following Proposition will show:

5.3. REMARKS ON DIFFERENT APPROACHES

157

Let Y

:= {yl .-.Ym}

be minimal with Y F- A. Let Y/ := {g2 ...g,~}. Split 91

into {Yl V r yl V -he}. Both gl

U

{Yl V r I- A and Yt U {Yl V 7r I- A can't be,

since otherwise Y/~- A, contradicting minimality of Y. So Y0 := Yt U {yl V ~} or

Y~ := Y/U {y~ V -,~} is a good candidate for Y - A, i.e. for contracting Y with

respect to A. So, let Y - A be Y0 if !/0 ~/A, and Y1 Otherwise.

Proposition 5.23 If Y - A is as just defined, then Y := Y - A U {-~A} decides

Proof We have ylA ... Aym F- .4, thus ~A A y2A ... Ay,= }- ~Yl. Consequently,

Y F- -~yl. If Y - A is Yo, then

(by ~1 V r E Y) Y F qS, if Y - A is I/1, then Y F- -,r

[]

This is further illustrated by the following point of view: We may consider "maxi-

choice contraction" as theory revision with axioms - taking the lull theory as ax-

iom set, and choosing a maximal subset from which A does not follow - resulting

in full completeness.

Chapter 6

Structured reasoning

6.1 Inheritance diagrams

6.1.1

Introduction

We shall limit the discussion to finite acyclic graphs, and mostly to purely de-

feasible ones. Exceptions are in Sections 6.1.2.2 and 6.1.2.4, where we give an

extended treatment of the monotonic case, too. As in all of nonmonotonic rea-

soning, the interesting questions arise in the treatment of contradictions. The

difference in quality of information is expressed by "preclusion" ("preclusion").

Unresolved contradictions give either rise to a branching into different extensions,

which may roughly be seen as maximal consistent subsets, or to mutual cancella-

tion in directly sceptical approaches. The extensions approach can be turned into

an indirectly sceptical one, by forming first all extensions, and then taking the

intersection of either the sets of valid paths, or of valid conclusions, see [MS91]

for a detailed discussion.

We start by giving a detailed account of the theory developed by J.Horty,

R.Thomason, D.S.Touretzky and co-authors, rich in ideas. We take the liberty

to digress somewhat to present also the monotonic case, and several logical and

semantical approaches.

The main part of Section 6.1.2 is 6.1.2.3, the nonmonotonic case, containing

the principal ideas. The - in the present author's opinion - central notion is

that of preclusion or preclusion. It captures the idea that some conflicts (i.e.

contradictory information sets) are resolvable using a specificity criterion: the

more specific intbrmation is considered the more reliable one. The (inductive)

definition of validity of paths in defeasible inheritance networks as presented

below consists of an interplay between plain (unresolvable) contradictions - the

prototypical example being the Nixon Diamond - and preclusion situations as

exemplified by the Tweety diagram. Various properties of the definition are

discussed, and an equivalent, essentially parallel, marker propagation algorithm

is presented in outline.

We then (in Section 6.1.3) proceed to give a concise overview of some other

approaches and problems, and give a sort of resume definition in Section 6.1.4.

160 CHAPTER 6. STRUCTURED REASONING

In Section 6.1.5 we give a formal proof that, under very weak assumptions, the

directly sceptical and the indirectly sceptical (via intersection of extensions) ap-

proach can never give the same results in all cases.

In Section 6.1.6 we give a (tentative) semantics for defensible inheritance by 3/-

systems. This semantics is tentative in the following sense: It is made to fit a

given proof theory, and not vice versa, and so cannot decide between different

formalisms of inheritance, as a good semantics should, see also the discussion in

the Introduction, Chapter 1.

Sometimes, we shall very slightly simplify the papers discussed. Our primary

aim is to develop the central ideas and to help the reader to understand them.

So, we sometimes sacrifice correctness marginally to improve intuition. We have

adopted a unified notation, resulting in some divergence from the originals.

6.1.2 A detailed survey of inheritance theory a la

Thomason (et al.)

Introduction

Preliminary intuition We call a -, p an atomic statement, if a is an object.

Letters from the beginning of the alphabet shall range over objects. We call p --* q

a generic statement, if p is a kind (a set or a class). Letters from the middle of

the alphabet shall range over kinds. Letters from the end of the alphabet will

range over both objects and classes. Of course, the head of an arrow must always

be a kind. It helps intuition to interpret a --* p as a E p, a 74 p as a ~ p, p --~ q

as p C q, p 74 q as p C Cq (the complement of q, where C is formed with respect

to some universe large enough).

From the above diagram, we may conclude set-theoretically e.g.: a E q, a E Cr,

v C Cp, a f[ r, q ~ r, q f3 Cr 7i (~, etc. Our conclusions by inheritance are more

restricted, in two ways. First, the language of admissible inheritance-expressions

is limited. It admits only expressions of the form z --~ p or z 7 4 p. Only if x is an

object, one is the negation of the other, whereas for sets, z C_ Cp is usually much

stronger than x ~ p. Thus, negation is very limited, and expressions like p n q do

not exist at nil. Second, we can form expressions and argue (reason) only Mong

paths, suitable chains of arrows. E.g., in the diagram {p --* q, io 74 q, r'} (i.e.

with isolated node r), q --~ r is neither an expression admitted by the diagram,

nor can we find a line of argument that, takes us from q to r. On the other hand,

our present intuitive interpretation tells us p = ~, thus p C_ r (and p C Or).

These limited reasoning capabilities will contain inconsistencies, however, as seen

in the following example: {a -* p, p~ q, p 74 q, r}.

In our interpretation, this net is inconsistent, as p is not empty. But we cannot

conclude by inheritance a. -* r, in other words, EFQ fails.

Objectives of the papers discussed The central objective is to examine

suitable relations ~ .

6.1. [NHERITANCE DIAGRAMS

161

First, r ~ cr for F an inheritance system (or diagram), a a path, in words, validity

of a in F. Second, c~ ~ A for cr a path, A a formula

xp

or x~. (Note: We digress

here from the notation in the papers discussed, which identify arrows x --* p and

results xp. This identification results in problems with stability - see below.) The

meaning of xp (x~) is roughly (as above): all x's are p's (all x's are not p's). The

identification gets, of course, its justification from the

use

of inheritance systems.

If we use an arrow x --~ p to encode the statement "all x's are p's" then it makes

sense to identify the conclusion "all y's are q's" in the translating diagram again

with an arrow. As long as we work within the machinery of inheritance, it is,

however, clearer to uphold the distinction.

Third, r ~ A defined by r ~ A iff 3~(F ~ cr Acr ~ A),

In other words, our problem is to decide which paths are valid paths in an inher-

itance system, and which conclusions are justified by arguing along valid paths.

Monotonic inheritance [THT86]

We will write monotonic (strict) links with double lines, =~ etc.

The intuition of the monotonic case a ~ p means: there is evidence, that

pa,

a 7~ p means: there is evidence, that

~pa,

p ~ q means: there is evidence, that all p are q,

p 7~ q means: there is evidence, that all p are not q.

In this sense, the famous Nixon Diamond (see Diagram 6.1 below) makes sense

in strict inheritance diagrams too, and, again, EFQ fails.

Different kinds of reasoning We shall examine here 5 different notions of

entailment, and show their equivalence:

- ~ as discussed in the introductory Section 6.1.2.1,

-1~- defined by a kind of transitive closure (which yields immediately logical

monotonicity, and excludes any preclusion),

- t- a sequence calculus very close to I1- ,

- ].~ 4-valued semantics (d. the intuition: "there is evidence ...", so there may

be no evidence, positive e., negative e., or both),

~p a Parallel Marker Propagation Machine Algorithm (PMPM). Roughly

speaking, we simulate the net on a PMPM, have markers run through the net to

obtain the transitive closure.

The definition of

Definition 6.1 a) The inductive definition of valid paths:

If x =~ p E F, then x =~z p is a valid positive path, so P ~ x :=~ p. If x :~ p E F,

then x :2~ p is a valid negative path, so F ~ z 7~ p. These two rules will be called

"Garbage In", reminding "garbage in - garbage out". The intuition is that there

is evidence that x C p or

x C_ p (x r p, x C_ Cp).

162

CHAPTER 6. STRUCTURED REASONING

If x.-. =~ p is a positive path, p =~ q C E, then x... =~ p =~ q is a valid

positive path, thus F ~ z... =~ p => q. The interpretation is clear. If z..- =~ p

is a positive path, p 5r q C F, then z... ::~ p 7b~ q is a valid negative path,

thus r ~ z... ~ p 7~ q. Read

x C ... C_ p C_ Cq

etc. If x..- r p is a

negative path, p r q E F, then z-.. r p <= q is a valid negative path, thus

r ~ x..- r p ~ q. (For the intuition : read x ~ r =~ s r t <= ...p ~ q as:

x C r C s C Ct C_ Cp C Cq.)

b) The definition of valid statements: If ~r = z-.. =~ p is a positive path, then

cr ~ xp.

If ~ = x... ~ r.-. r s r -..p is a negative path, then a ~ zp.

Remark: If 7 C_ ~r a segment of ~r, and r ~ c,, then E ~ r (trivial by definition).

This will no longer be true in the nonmonotonic systems.

The definition of iF- and equivalence with

Definition 6.2 We directly define F if-

xp

(resp. xp). Let FH be the smallest set

of statements such that certain closure properties are satisfied:

0) F C_ Ftl (Garbage In) (more precisely the set of all xy (xg) such that z ~ y

(z ~ y) E F will be in Ffl,

1)

pp

E Fit for all vertices p in F (the definition is obvious),

2) if

xq, qr

r F11, then zr C I?tt (transitivity),

3) if p~ E Ftl, then qp EFt/ (p C Cq iff

q C_ Cp),

4) if

xp,

p~ E Fir, then x~ E FH,

5) if

pq,

xg r Eli, then xp E Ptl.

The meaning of the last two conditions will be obvious, when thinking in terms

of set-inclusion.

We write F [k- A iff A E Fir.

We then have

Lemma 6.3 Let F! be the obvious translation of the net F into statements, then

A ifr r A.

Lemma

6.4 ['1t- A implies FUAI~- 'A ~-, and, thus ~ are monotone). (Trivial

by definition of Ik- as closure.)

Lemma 6.5 Let F tt- A, F, AII~- B, then F [k B (stability, usually called Cut),

again trivial by closure. AI is the arrow corresponding to A.

Lemma

6.6 If A consists only of arrows of the type a =~ p or a ~ p, then

r U A ~ qr implies F ~ qr and F U A ~ qT implies F ~ qg.

Lemma

6.7 If F a is a net not containing a, then 12' ~ ~

pq

iff

F ~, a => p ~ pq

and

F ~ ~ p~ iff F% a =~ p ~ p~. (Use the definition Of ~ for the proof.)

6.1. INHERITANCE DIAGRAMS

163

The sequent calculus F- A sequent calculus consists of axioms and rules.

Axioms have the form F F- A, e.g. we may have F F- A for all A E r. The

formulae on the left hand side should be read as a conjunction. Rules will have

the form

PF-A, F/P B =~ DtF- C

which should be read as: If the top sequences are provable, then so is the bottom

formula.

The following definition gives the sequent calculus (modified a bit, to point out

the parallels to IF- defined above):

Definition 6.8 l) Axioms (Garbage In) If A E F, then P F- A.

2) Rules (simplified)

F- =~: ra, ap P aq

=~ ra F- pq (see Lemma 6.7),

F- r similarly,

F-: P F- zp ~ P,pq F- xq

(Definition 6.2, 2),

F- t: r F- xF =:> F, qp F- :c-q

(Definition 6.2, 5),

F-: F F- zp ~ F,p-q F- z~

(Definition 6.2, 4),

r b: P b zq =:~ F,p~ F- zF (Definition 6.2, 3) and Definition 6.2, 4).

Lemma 6.9 The rule r F- A =:> F, A F- A is admissible, i.e., if we have a proof of

the top line, then we can, using the above rules, find a proof of the bottom line,

too. (The proof is easy.)

Theorem 6.10 IF- and F- are equivalent.

This follows from

Theorem 6.11 If r b A is provable, then P It- A. (The proof of this theorem is

by induction on the complexity of the proof of F F- A, and uses Lemma 6.3.)

and

Theorem 6.12 If F ~ A, then Fr F- A is provable, where FI is the translation of

F. (The proof is rather tedious, and by cases. A suitable path proving A will be

transformed into a sequent proof.)

4-valued models, the relation i~ We use a 4-valued logic to express simul-

taneously '~There is evidence

that a

is p" and "There is evidence, that a is not

p" etc. The construction is more or less evident. Fix a universe U, and let p

be given. We associate with p two subsets of U, one for the elements, for which

there is evidence that they are p, the. other for those for which there is evidence

that they are not p. More formally,

v(pa) = [[a =ez p~ = X,

where X _C {T, F},

and T C X iff there is evidence that

pa, F E X

iff there is evidence that ~pa.

We have to choose the universe large enough so we can distinguish all %ets" p

(just think of the possibility that there are no constants a, then we could always

choose 0).

This is made formal in

164

CHAPTER 6. STRUCTURED REASONING

Definition 6.13 A model (a valuation) v is a pair (D,v'), D a set, vt

= (Vl,y2) ,

a pair of functions

vl: Indivual Terms --* Elements in D, a ~

vl(a)

v2: Generic Terms ---* Functions: D --+ T = {T, F}, p ~ v~(p): D --~ T.

We further define

v(pa) :=-

v2(p)(vl(a)),

v(-~pa)

:=

not(v(pa)),

where

not({T})

:= {F},

not({F})

:= {T},

not(O)

:= 0,

not({T,F})

:= {T,F}.

v(p ~ q):=

{T} if[Yd E D ( T E

v(pd) ~ T E v(qd)

and F E

v(qd) --+ F E v(pd)

), and

v(p ~ q)

:= 0 otherwise. (The second condition is motivated by p C q

cq c_ cv.)

Likewise:

v(p 75 q)

:= {T} iff Vd E D ( T E

v(pd) --~ F E v(qd)

and T E

v(qd)

-+ F E v(pd) ),

and

v(p 75 q)

:= 0 otherwise.

Ifvis avaluation, set v]~ AiffT

E v(A),

and Pl~ Aifffor all valuations v

(VB E P(v IF B)

--* v I~ A), and call r equivalent to v iff VA(P ~ A iff v 1~ A).

We can now show

Theorem 6.14 ~ and I~ are equivalent, i.e.

translation of F.)

In the proof, we use

Lemrna 6.15

Vv3F,(v

and P. are equivalent).

and

r A iff r, IF

A. (rr again the

Lemma 6.16 VF3vr (vp and P are equivalent).

A PMPM-algorithm (outline) We can simulate the net on a PMPM, push-

ing markers in parallel through the net. Thus, all paths leading from x to y can

be considered simultaneously. (Note that if we have found a path, we are not yet

finished, as there might be another one of opposite polarity.) Running time is

roughly determined by the length of the longest path from x to y. The algorithm

and the result are essentially trivial, we shortly discuss the situation as a toy sce-

nario to help the reader get familiar with the notions, and thus prepare ourselves

for the more complicated situation in the nonmonotonic case.

In a PMPM, the vertices may have different markers (colours). An unconditional

command like

clear[T]

means: cancel the marker T everywhere. A conditional

command like

link - type[O], on - tail[T] --~ set - head[T]

will pass the marker

T along all arrows of type ~ .

A loop

loop

body

endloop

6.1. INHERITANCE DIAGRAMS

165

will be executed as long as there is a conditional command in body, whose pre-

conditions are satisfied.

E.g.

Procedure

begin

clear[T]

--* set[T]

(only the vertix x is called)

loop

link - type[o], on - tail[T], off - head[T] --* set - head[T]

(see above, the condition

off - head[T]

guaranties that the loop

will be left sometime)

endloop

end

will propagate the marker T upward from x, i.e., in our interpretation, all super-

sets of x (if x is a kind) will have the marker T, when the algorithm is finished.

We then have the following

Theorem 6.17 Let F be simulated on a PMPM, Cy _c T. Then there is an

algorithm for the PMPM, which computes for a given z for alt

y Cy,

such that

F ~ xy iff T E Cy,

P ~ x~ iff" F E C v.

Nonmonotonic inheritance [HTT87]

The intuition Nonmonotonic Inheritance Systems describe situations like

"normally, birds fly", written bird --+ fly. Exceptions are permitted. To sim-

plify matters, and contrary to the monotonic case, we do not understand these

assertions to mean "there is evidence .... ".

Thus, we have changed intuition in two ways:

- assertions will be understood to mean "the normal case"

- assertions will be understood as valid, not as some information, which may be

wrong,

(As already done, we shall use now simple arrows, instead of the double ones of

the monotonic case.)

An immediate consequence of the changed intuition is, that contradictions have

a different meaning now. Thus, the diagram

{Penguins ~ Birds, Birds ~ Fly,

Penguins 74 Fly}

will mean that, penguins are exceptions.

166

CHAPTER 6. STRUCTURED REASONING

Diagram 6.1

8

q r

P

Preclusion In the above example, our intuition tells us, that it is not admis-

sible to conclude from the fact, that most penguins are birds, and most birds

fly, that most penguins fly. The lower arrow barrs this conclusion, it is the more

specific information. Thus, not everything, which would have been a valid path

in the monotonic case, is one now. Consequently, we have to define the condi-

tions under which two potential paths neutralize each other, and when one is

victorious. The idea is as follows:

1) We want to be sceptical, in the sense that we do not believe every potential

path. We will not arbitrarily chose one either.

2) Our scepticism will be restricted, in the sense that we will often make well

defined choices for one path in the case of conflict:

a) If both p --* q, p 74 q C F (as direct links), then F ~ p ~ q, F ~ p 7# q

(Garbage In) This rule, which - in the possibility that both P ~ p --, q, P ~ p 7/~ q

-

is not found elsewhere in the literature, suggests a reinterpretation, as above

for monotonic sets: "There is evidence, that .... ". As this aspects seems only

to complicate matters, it is neglected here, and we continue to read arrows as

"normally .... ".

b) If a compound potential path is in conflict with a direct link, the direct link

wins.

c) Two conflicting paths of the same type neutralize each other, as seen in Dia-

gram 6.1.

d) More specific information will win over less specific one.

Schlechta K. Nonmonotonic Logics: Basic Concepts, Results, and Techniques

Подождите немного. Документ загружается.