On Semantics of TMS

1. Introduction

TMS (Truth Maintenance System) is frrst proposed by Doyle in 1979, which is a technique to maintain the consistency of belief and find the source of the contradiction (Dependency-Directed Backtracking ). It is more proper to call TMS by BMS (Belief Maintenance System) or RMS (Reason Maintenance System). Traditionally we still call it TMS in this paper. Because TMS plays an important rule in KB, non­ monotonic reasoning, pattern recognition, and all the other fields in which the knowledge will be adjusted because of the new knowledge's accumulation or introspection, there has been much researches work on TMS in this decade. In this paper we do not intend to introduce the results in this respect What we want to point out is that there has been less research on the TMS's basic theory, especially on its formal semantics. This phenomenon can be explained as the following: In this decade, TMS is always studied as a technique, and it seems to be a practical non-monotonic belief maintenance technique by birth. Since TMS is NP-hard, much attention has been attracted to how to make it more practical. The computation complexity of non-monotonic theory has been known since the beginning of 80's, there is still more researches on the beautiful form of non-monotonic reasoning and on the theoretically formal proofs of non-monotonic theory. Although there are some comparison between TMS and non-monotonic reasoning, the results in this field are few and not deep after all.

When we study how to implement a practical non-monotonic reasoning system, we find that it must contain at least two basic pans: one is the non-monotonic inference mechanism, the other is TMS. This opinion complies with the one in reference [B. Smith and G. Kelleher, 1988]. When the default reasoning based on Hom logic is combined with TMS [Wang Xianchang and Chen Huowang, 1990(a),(c)], we find that the frrst problem we meet is to get the formal semantics of TMS. Only by this way can we ensure the consistency between the non-monotonic inference mechanism and the belief maintenance system. But many of the concepts in TMS are not clear. There are different understandings for these concepts among different people. For example what is the correct meaning of CP justification? What should be a premise node? When we replace a valid CP justification by the so called equally SL justification , is the new TMS theory equal the original theory? We notice that in resent years, there are some researches on the

On Semantics of TMS

Wang Xianchang, Chen Huowang Depanment of Computer Science Changsha Institute of Technology Changsha, Hunan, P.R. CHINA 410073

Telex:98141 NUDTC CN Fax:86-731-48583

formalization of TMS, but what they study is the TMS with no CP justification. For example, Ulrich Junker and Kurt Konolige make comparison between the relations among TMS which have no CP justifiCation with AEL and DL. They discuss how to translate the AEL, DL to TMS [U. Junker and K. Konolige, 1990]. This kind of work is also very important in our research worlc [Wang Xianchang and Chen Huowang, 1990(a), (b), (c)].

In this paper, we flfSt defme the TMS language and the TMS theory. Then we define the formal semantics of TMS. Next we prove the valid transformation of the CP justifteation to SL justifications. Finally we discilss the semantic relation between ours and U .Junker semantics of TMS with no CP justification.

2. TMS Theory

The basic language of TMS is a prepositional language. In TMS a statement with variables is not allowed.

Dtf 1. p,q,pl,ql, ... ,p~qi, ... are propositions.

Der 2. Suppose r is a proposition, then r and (-r) are nodes.

In general, a TMS theory contains fmite nodes. Suppose NS is a set of nodes, here NS is always fmite. Node r, ( -r) have no semantics relation in TMS. They are formally non-related statements , although we always regard them as excluding each other.

Der 3. SL (Support List) justification

The SL justifiCation on node set NS is a formula as following:

p <-- in(I),out(O)

Here pis in NS, I and 0 are subset of NS, I/\0= ().pis called the consequence of above SL justification, (in(l),out(O)) is called one of p's reason. The node in I is called p's premise node, the node in 0 is called p's default premise node.

Def 4. CP(Conditional Proof) justification

The CP justification on node set NS is a formula as following:

p <-- q, in(l),out(O)

Here p,q are inNS, I and 0 are subset of NS, I 1\0=(}.

The informal meaning of above CP justification is:

If there is a non-monotonic proof of q under premise (in(l),out(O)), then p is believable.

Doyle has not discussed the meaning of CP justification in the case 0=1= (}. In this paper we mainly discuss the general case. We ensure that when 0=() the meaning of our definition of CP justification complies with Doyle's original meaning.

Der S. TMS theory.

A TMS theory J on node set NS is based on fmite SL justifications or CP justifications.

ner 6. J(l)

Suppose J is a TMS theory on node set NS, I is a CP justification, I = p <-- q, in(l), out(O), Then we define a TMS theory J(l) as:

J(l)= ( J - (I) + ( p'<-- I for every p' in I) ) - ( II I II is a SL justification of J, and p' is ll's consequence, p' is in 0 )

Example 1. Consider the following five TMS theories. It is not necessary to list the corresponding node sets of each theory.

Jl= ( p<-- in(q), q<-- in(p) )

p, q are the premise of each other.

12= ( p<-- out(q), q<-- out(p) ) p, q are the default premise of each other,. 13= ( p<--q, in(ql), q<--in(ql) ) If ql is a belief of theory 13, then q is also a belief of theory 13; Suppose q I is believable, if we can get that q is also believable, then p is a belief. 14 = ( p2<--in(pl,p4), p3<--in(p2,p5), p4<--, p5<--, p6<--p3, in(pl) ) This theory can be referred to in [1. Doyle, 1979]. 15 = ( p<--ql, ql<-- out(q2),q2<--out(ql) ) If there is a non-monotonic proof of ql then p is believable. 3. The Semantic Study on TMS Theory. 3.1 Definitions. Def 1. Assignment f. Suppose 1 is a TMS theory on node set NS, then an assignment f of 1 is a map, f: NS ---> (in out), such that: For every node d in NS, f(d)=in iff Either 1 has a SL justification, I= d<-- in(D,out(O) such that for every p in I,f(p)=in, and for every node in 0, f(p)=out, I is called a valid SL justification. Or 1 has a CP justification I = d <-- p, in(l),out(O) such that 1(1) has a model f such that f(p )=in, I is called a valid CP justification. Def 2. In assignment f of theory 1,we say node pis an in-node if f(p)=in, else we call it out-node. SuppOse p is an in-node, if it has a valid SL justification p<-- in(l),out(O), then (I + 0) is called p's suppon set, denoted by Sup(1,f,p). Else,p has an valid CP justification l=p<--q,in(l),out(O) then Rant(1(1), r, I + 0, q) is Sup(1, f, p), here f is the theory 1(l)'s model which make q believable. Rant is defined as following. Def 3. Suppose p is an in-node of theory 1 in assignment f. We define p's ancestor set, Ant(1,f,p) which is the minimal set satisfying the following conditions: I. Sup(1,f,p) is a subset of Ant(1,f,p) 2. If in-node q is in Ant(1,f,p), then Sup(1,f,q) is a subset of Ant(1,f,p) Def 4. Repercussions set. Suppose 1 is a TMS theory on node set NS, f is a model of 1, for every p in NS we define p's repercussions set , Rep(J,f,p) : Rep(J,f,p)= (q I q is an in-node and pis in Ant(1,f,q)} Obviously any node whether it is in-node or out-node,can be one of the reason of an another in-node. Def 5. Suppose S is a subset of NS, f is an assignment of theory J on node set NS. Then we define Rep(J,f,S) as I. if S=() then Rep(J,f,S)=(} 2. if S= Sl + (p) then Rep(J,f,S)= Rep(J,f,p) + Rep(J,f,Sl) Def 6. Related-ancestors set Suppose p is an in-node of theory 1 in assignment f, then the related­ ancestors set under premise set S, Rant(J,f,S,p) is the maximal set which satisfies the following conditions: I. Rant(1,f,S,q) is a subset of Ant(J,f,q) 2. Rant(J,f,S,q) J\ S = () 3. Rep(J,f,S) J\ Rant(J,f,S,p) = (} The meaning of Rant(J, f, S,q) would be used to define what the premise argument of an valid CP justification. Suppose CP justification I= p<--q,in(l),out(O) is valid in assignment f of theory 1, and r is a model of theory J(l) such that f(q)= in. q's related­ ancestors set under premise set S= I + 0 is Rant(J(l), f, S, q). Then we defme p's support node set under f is Rant(J(l), f, S, q). The concept of assignment has involved an undefined concept "model", in the following we will defme it recursively. Def 7. An assignment f of TMS theory J is a model iff I. For every in-node p of J, p is not in Ant(J, f, p) 2. For every valid CP justification I, 1' is defined as def 2 in section 3.4, f is an assignment of J'.

Def 8. We call TMS theory J's assignment f is well-defined iff every in­ node p off, p isn't in set Ant(J, f, p). Obviously the defmition of model of TMS theory is very complicated , but it will became very simple and easily understand if the theory has no CP justification. In the following we will discuss the way to translate the CP justification to SL justification, and discuss the correctness of this translation.

3.2 Example 2.

According to the above defmitions, we consider the theories of example I. 11 = ( p<--in(q), q<--in (p)) 11 has only one model: fl= (p-->out, q--->out) 12 = ( p<--out(q), q<--out(p)} 12 has only two models: f2,1 =( p--->out, q--->in ) f2,2 =( p--->in, q--->out) 13 = (p<--q,in(ql), q<--in(ql)} 13 has only one model: f3 = (p--->in, q--->out, ql--->out } 14 = (p2<--in(pl,p4), p3<--in(p2,p5},p4<--, p5<--, p6<--p3, in(pl} } 14 has only one model: f4= (pl--->out,p2--->out, p3--->out, p4---> in, p5--->in, p6--->in) 15 = (p<--ql,ql<--out(q2), q2<--out(ql) ) 15 has two models: f5,1 = (p--->in, ql--->in, q2--->out ) f5,2 = (p--->in, ql--->out, q2--->in ) 3.3 The Semantics Consideration on CP Justification. In section 3.1, the meaning of a CP justification is as following: A theory 1's CP justification I= p<--q,in(I),out(O) is valid in model f iff there is a model r of theory 1(1) such that f(q)=in. Obviously (a) Whether 1's CP justification I is valid in model f has nothing to do with f, its validity only depend upon 1. (b) SuAJOSC 1-- is a relation : 1 1-p iff TMS theory 1 has a model f such that f(p)=in. Suppose 11-- is a relation: 1 11-p iff for every model f of TMS theory 1 f(p}=in. Then TMS has the following properties: I. 1 + (p<--p) 11- p iff 1 1--p 2. SuAJOSC I is a subset of node set NS, then J + (p<-- I p is in I} 1---q iff 1 + ( q<--q,in(l)) 11-q. 3. The validity of CP justification express the "non-monotonic provableness" For example. a CP justification I = p<--q,in(D,out(O) is valid in theory 1 iff 1(1) 1----q. Non-Monotonic properties: From 1 1----q we can not conclude 1 + (p<--p) 1-q For example. 12 1---q, but 12 + (p<--p} 1-\-q. 4. if 1 1---q then we have 1 + ( p<--q ) 11--p. (c) A TMS theory may have no model. Example 3. 16 = (p<--out (p)) 17 = {pl--out(p2}, p2<--out(p3), p3<--out(pl)} The above two theories have no model. This kind of theory is called paradox theory. (d) We can modify the semantics definition of CPjustification. For example we can modify the "1(1) has a model " of def.l in section 3.1 by "for all model of 1(1)". Under this interpretation 15 in example 2 will have other two different models: f5,1 = (p-->out, ql--->in, q2--->out } f5,2 = (p-->out, ql--->out, q2--->in } (e) It may be very difficulty to give a defmition by which the validity of CP justification depends upon both the theory and the present model. The importance to find such defmitions is not clear now, but it can be

studied further.

3.4 Translation ol CP to SL JustifiCation.

In order 10 simplify the complex of TM . processing, Doyle gives a method 10 translate a valid CP justification 10 so called "equally" SL justification, maybe it is this unproved "equality" that makes the foUowed researchers tum 10 the TMS theory with no CP justification. But our research shows that this "equality " is false.

First we defme what is the translated SL justification in theory J under model f through a valid CP justification.

Def 1. Suppose CP justification I= p<--q,in(l),out(O) is valid in model f of theory J, f is a model of theory J(l) such that f(q)= in. Suppose Sup(J,f,p) is Rant(J(I), f, I + 0, q) then we defme the translated SL justification of CP justification under J ,f,f is:

p<-- in(l'),out(O') such that

1. I' + 0' = Ranl(J(I), f, I + 0, q)

2. l'l\0'=(}

3. For every r in I', f(r)=in;

For every r in 0', f(r)=out

Example 4. (Continue example 2)

First we consider B.

J3'=J3(p<--q,in(ql)) = (q<--in(ql), ql<--}, it has only one model f3'= (ql--->in, q--->in}, Ranl(J3', f3', {ql}, q) = (}. So the translated SL justification of p<--q,in(ql) under model f3 is:

p<--

Second we consider J4.

J4'=J4(p6<--p3,in(pl)) has only one model f4'=( pl--->in, p2--->in, p3--->in, p4--->in, p5--->in, p6--->out}. Ranl(J4', f4', {pl}. p3) = (p4,p5}, so the translated SL justifiCation of p6<--p3,in(pl) is:

p6<--in(p4,p5)

J5'= J5(p<--ql)={ql<--oul(q2),q2<--<>ul(ql)}, it has one model f5' = (ql--->in, q2-->out}. Since Rant(J5',f3',{ql}.p) = (q2), the translated SL justifiCation of p<--ql under (f5,l), f5'is: p< --out( q2)

The translated SL justifiCation of p<-ql under (!3,2), f3' is p<- in(q2) Def 2. Suwose f is a model of TMS theory J. CP justification 1 = p<-­ q,in(I),oul(O) is valid in f. Suwose p<--in(I'),oul(O') is the translated SL justification of 1, then theory f= J - ( I } + ( p<--in(I'), out(O') } is caUed one replaced theory of J under model f.

Obviously we have following theorem.

Theorem 1. Suwose f is a model of theory J, J' is one replaced theory of J under model f. Then f is still a model of r .

In general some models of J may be not the models of J', and some models of r may be not rs models.

Example 5. Consider Theory J5 of example 4.

Obviously one replaced theory of J5 under model f3,1 is J'5,1 = ( p<· -<>ut(q2), ql<-oul(q2), q2<--<>ut(ql) }. This theory has two'models: one is f5,1 , the other is f5,2 = (p--->out, ql--->out, q2--->in }. Obviously f5,2 is not J5's model and the model f5,2 of J5 is also not the model of 1'5,1.

Def 3. Suwose J has a valid CP justification 1 = p<--q, in(l), oul(O), we define a translated theory of J as J*(l), which is: J*(l) = J · {l} + ( p<· -in(l'),oul(O') I there is a model f of J such that p<--in(l'),oul(O') is a b'anslated SL justification of I under model f)

It is easy 10 prove

Theorem 2. Suwose I is a valid CP justifiCation in theory J then for every model f of J, f is still a model of J*(l).

Example 6.

Consider TMS theory J4 of example 3. CP justification 14= p6<-­ pl,in(p3) is valid, it is easy 10 get that J4*(14)= ( p2<--in(pl, p4), p3<­ ·in(p2, p5), p4<--, p5<--, p3<--in(p4, p5)) . Obviously every model of 14 is also the model of J4 *(14 ).

Consider TMS theory J5 of example 3. 15= p<--ql is valid in J5,J5*(15)=( ql<--oul(q2), q2<--oul(ql), q<--oul(q2), q<--in(q2) }. Obviously all the models of J5 are also J5*(13)'s models.

Whether the model of J*(l) is the model of J? the answer is not clear now.

From theorem 1 and theorem 2, we can conclude that:

Theorem 3. Suwose J is a TMS theory, then there must be a TMS theory J* such that

1. J* has no CP justifiCations.
2. Every model of J is also the model of J*.

4. Comparison With U. Junker and Kurt Konolige's Work

1. Junker and Kurt Konolige give a Semantics of TMS theory with no CP justification. Here we do not want 10 introduce their wort, the conceptS appeared bellow can be referred in [U. Junker and K. Konolige, 1990]. The following are our main conclusions.

Def 1. Suppose J is a TMS theory on node set NS, f is rs model, then we defme T(l) = (c I c is inNS, and f(c)=in } as an extension of J.

Now is U. Junker's extension the same as ours?

In the following all the TMS theories we consider have no CP justifications.

Lemma 1. f is a model of TMS theory J iff

Proof: We can get it from the defmition of model f and the function apply.

Lemma 2. For any model f of theory J, we have

Proof: Because

So we can get lemma 2 after we prove the following by inductive method:

for every i=O.l, ... , n, ...

Lemma 3. Iff is a model of TMS theory J, then

Proof: we can construct a function t:NS--->{0,1, ... } such that 1. if p is an out-node of f then l(p) is 0.

2. if SL justifiCation p<-in(I),oul(O) is in-node p's valid support justification, then l(p) is defmed as

1 + Max(O, ( l(q) I q is in I}

Because every in-node pis not in Anl(J, f, p), the above function t is weU defmed. It is easy 10 proof that for every in-node p

so T(l) is a subset of apply/.T<o ( (})

From lemma 2 and lemma 3 we can get lemma 4.

Lemma 4. f is a model of TMS theory J iff

Lemma 5. Suppose J is a TMS theory on node set NS. TSNS, if T=apply/r ((})

Then the following three properties hold.

a. T = apply 1 r (f)

b. T = apply;·:r ((})

c. There is no TOG T such that

TO= applyJTO (TO)

Proof: The propeities a,b can be found in [U. Junker and K. Konolige, 1990]] . Now we prove c. Suwose c is not hold then there must be a TO such that

TOcT and

So we have proven the following by inductive method

So TO a T , this is contrary to TO c T.

c is proved. Q.E.D

From above three lemmas, we can get.

Theorem 6. J is a TMS theory with no CP justification, then E is an extension of what U. Junker and K. Konolige define iff E is also an extension of what we define. In other words, J must have a model f such that T{t) = E .

This theorem shows that the extension concept defined by U. Junker and Kurt Konolige is correct in our semantics frame.

5. Conclusion

In this paper we first give a formal semantics of non-monotonic TMS theory with CP justifications. Then we prove that the model of a theory J is also a model of theory J*(l). Next we conclude that for every TMS theory J, there must be a theory J* such that J* has no CP justifications and all the model of J is also J*'s; Finally we prove that the concept of extension defined by U. Junker and Kurt Konolige is the same under our defmition. It is necessary to point out that there are more properties of CP justification left for us to study. From our discussion, it seems that the CP justification has a close relation with "non-monotonic provenance".