Relating the TMS to Autoepistemic Logic

1. Introduction

In this paper, we shall give the declarative semantics of Doyle's TMS [6). Our method is based on autoepistemic logic defined by Moore [14] . The main result is that there exists a natural one-to­ one correspondence between states acceptable to the TMS and stable expansions of the set of autoepistemic formulas at.tached to the justifications.

In Doyle's first paper on the TMS, his main intention seemed to be to put nonmonotonic reasoning into practical use. But his description of the TMS was algorithmic and without semantics. To provide the semantics is important not only for a theoretical interest but also for a practical one in improving TMS implementations.

McDermott and Doyle [13) attempted to give a logical background of the TMS. However, their "non-monotonic logic" has several disadvantages. Some attempts to resolve these faults have been made [12,14). Among others, Moore's autoepistemic logic has clear semantics. In addition, it is shown that autoepistemic logic has remarkable relations to the modal logic S5 [15) and Reiter's default logic [10). But these studies of nonmonotonic reasoning seem to have little influence on the work on truth maintenance.

De Kleer [3) presented the ATMS architecture, a variant of Doyle's TMS. It aims at efficient search and can process multiple contexts simultaneously. The ATMS, however, can treat monotonic justifications only. There are proposals of the ATMS architecture which allow

Relating The TMS to Autoepistemic Logic

Yasushi Fujiwara Shinichi Honiden

Systems & Software Engineering Laboratory TIJSHIBA Corporation 70 Yanagicho Kawasaki 210, JAPAN

nonmonotonic justifications [4,5,7), but they also lack the semantics.

In this paper, we shall make the semantics of Doyle's TMS clear by using the technique of nonmonotonic reasoning. The TMS is a theorem prover of autoepistemic logic. OUr result suggests the possibility of implementing better TMS and extended ATMS algorithms.

2. Autoepistemic logic

Moore [14) defined autoepistemic logic as a formal framework of beliefs of the ideally rational agent reasoning about her own beliefs. Moore [15) further obtained alternative semantics, which is based on Kripke semantics of the modal logic SS. In this section, we shall give a brief account of his theory.

2 .1. The formalism of autoepistemic logic

The language of autoepistemic logic is that of propositional logic augmented by a unary connective L. The symbol L is intended to mean "is believed". We suppose that atomic propositions are drawn from a finite set P .

Let T be a set of autoepistemic formulas. For any propositional truth assignment v, we define the autoepistemic interpretation VT to be the truth assignment which extends v by the condition VT (Lp) = 1 <=> pET.

If an autoepistemic interpretation VT satisfies the condition that VT (p) = 1 for all p E T, we shall call VT an autoepistemic model of T.

We define the notions of soundness and completeness relative to this semantics.

Definition 1. Let A be a finite set of autoepistemic formulas. A set of autoepistemic formulas T is sound with respect to a set of premises A if and only if every autoepistemic interpretation of T in which every formula of A is true is also an autoepistemic model of T.

Definition 2. A set of autoepistemic formulas T is semantically complete if and only if every autoepistemic formula which is true in every autoepistemic model of T lies in T.

The set of beliefs that a rational agent might hold, given a set of premises A, would be semantically complete theory that is sound with respect to A.

Definition 3. A set of autoepistemic formulas T is called a stable expansion of a set of premises A if and only if T satisfies the following conditions:

1. T contains A.
2. T is sound with respect to A.
3. T is semantically complete.

2 . 2. The modal logic SS [9,11]

The logic SS is a kind of modal logic of knowledge. Its Kripke semantics is very simple . An SS Kripke model is just a set of truth assignments. These truth assignments can be considered as the worlds which are possible.

Syntax. The language of SS is syntactically identical to that of autoepistemic logic. The symbol -L- is often abbreviated as M.

Semantics. An SS Kripke structure is a set of propositional truth assignments. An SS model is a pair (V,K) consisting of a propositional truth assignment V and an SS Kripke structure K such that V e K. The interpretation of an SS formula p with respect to this model is given by the usual truth recursion augmented by conditions:

1. (V,K) l=p <=> V l=p if p is a propositional formula.
2. (V,K) I=Lp <=> (W,K) l=p for all WeK. We shall denote by VK(P) the truth value of a formula p with respect to an SS model (V,K).

2. 3. Autoepistemic logic and SS semantics

The formulation of autoepistemic logic given above is nonconstructive and makes it difficult to seek stable expansions. In [15], Moore characterized semantically complete autoepistemic theories in terms of SS semantics. This characterization enables us to demonstrate the existence of stable expansions of given set of premises.

Theorem 1. (Moore) The following conditions are equivalent.

1. The autoepistemic theory T is semantically complete.
2. The autoepistemic theory T is given by T= {pI (V,K) l=p for all ve K ), for some SS Kripke structure K.

By the above theorem, we get simple characterization of stable expansions, which we shall use repeatedly.

Proposition 1. Let A be a set of autoepistemic formulas. Then a stable expansion T of a set of premises A corresponds bijectively to an SS Kripke structure K which satisfies the following conditions:

1. T = { p I (V, K) I= p for all V e K ) .
2. For any propositional truth assignment v, V e K <=> VT (p) = 1 for all peA.

Proof . Let T be a stable expansion of a set of premises A and define an SS Kripke structure K by K = { V I VT is an autoepistemic model of T ) . From Moore's proof of the above theorem, we have T = {pI (V,K) l=p for all VeK ). On the other hand, as T contains A and is sound with respect to A, VT is an autoepistemic model of T if and only if VT (p) = 1 for all peA. Thus, K satisfies 1) and 2) .

Suppose that an SS Kripke structure K satisfies 1) and 2) . By 2), if V e K, we have VT (p) = 1 for all peA. Remark that, for V e K, VT (q) = VK (q) for any autoepistemic formula q. Then we have VK(P) =1 for any peA and VeK. By the definition ofT, we see that T=>A. By 2), if a propositional truth assignment v satisfies the condition that VT (p) = 1 for all peA, we get V e K, hence VT is an autoepistemic model of T. Thus, T is sound with respect to A. This shows that T is a stable expansion of a set of premises A. Q.E.D.

Combining Proposition 1 and the decidability of the modal logic SS [9,11], we know that autoepistemic logic is also decidable, i.e. we can obtain all the stable expansions of the given set of premises.

3. The TMS

A TMS is a part of the reasoning system. The reasoning system consists of a problem solver and a TMS. The problem solver transmits every inferences made to the TMS. The TMS manages justifications and answers what data are believed ("in") and disbelieved ("out") when asked.

In this section, after giving a formulation of the TMS, we shall define a translation rule from the TMS theory to autoepistemic logic and show its properties.

3 .1. The formalism of the TMS

Here we give a formulation of Doyle's TMS. For simplicity, we shall only deal with SL­ justifications.

Definition 4. A TMS is a triple D = (N, J, C) such that

1. N is a finite set (The elements of N will be called nodes. ) .
2. J is a subset of Nx2Nx2N, where 2N denotes the power set of N (The elements of J ·t~ill be called justifications.).
3. C is a subset of 2N (The elements of c will be called nogoods . ).

Let j = (n, N1, N2) e J be a justification. Then the node n is called the consequent node of j. The subset N1 (resp. N2) of N is called the inlist (resp . outlist) of the justification j. The justification j is said to be nonmonotonic if the outlist N2 is nonempty.

The f ollowing definition of admissible states is intended to formulate states acceptable to a TMS without "circularity-check".

Definition 5. Let D= (N,J,C) be a TMS and S be a subset of N. We shall say that S is an admissible state of D if S satisfies the following conditions:

1. Let j = (n, N1, N2) E J be a justification with N1 c S and N2 c N\S. Then n lies in S.
2. Conversely, for any n E S, there exists a justification j = (n,N1,N2) E J with N1 c S and N2 c N\S .
3. For any nogood c, c 4 S.

Let S be an admissible state of D. By the above definition, for any node n E S, there exists a justification j = (n, N1, N2) such that N1 c S and N2 c N\S. We shall call such j a supporting justification of n.

Doyle tried to get rid of "in" nodes supported by circular arguments. His TMS singles out one supporting justification to each "in" node and tries to ensure that the set of supporting justifications is without circularity. The following definition of well-founded admissible states is intended to formulate states acceptable to the TMS with "circularity-check" . Although Doyle classified three patterns of circular arguments, we shall consider the first one only. The second type of circularity is an example of multiple-extension problem which are common in nonmonotonic reasoning. The third type of circularity is unsatisfiable one and it has no admissible state in our sense.

Definition 6. Let D and S be as in the above definition. we shall say that S is a minimal admissible state of D if S is an admissible state of D and any proper subset of S is not an admissible state of D.

Definition 7. Let D and S be as in the above definition. An admissible state S of D is said to be a well-founded admissible state if, for any n E S, there exists a supporting justification jn of n such that S is a minimal admissible state of the TMS (N, { jn 1 ne S },0) (Such a set { jn I ne S} is called a set of well-founded supporting justifications.).

The following example shows our definition precludes admissible states which are based on circular arguments.

Example 1. Let J = { (p, {p}, 0), (q, 0, {p})} . Then there are two admissible states, i.e. {p} and {q}, which are both minimal. The supporting justification (p,{p},0) of the node pis circular, hence {p} is not well-founded. On the other hand, the supporting justification of q is (q,0,{p}) and {q} is a minimal admissible state of {(q,0,{p})}. Thus, the state {q} is the unique well-founded admissible state of J.

Remark. In the first version of this paper, we formulated the states acceptable to the TMS with circularity-check to be minimal admissible states .

But as we can see in the above example, it is insufficient. The authors also considered yet another truth maintenance system [8] based on stratified logic programming technique [16], which accepts only the state {q} of the above example. Thus, we felt a need to reformulate states acceptable to the TMS. The definition given here is a natural formalization of Doyle's original one.

A TMS may have no well-founded admissible states and may have more than one. As long as we allow the full use of nonmonotonic justifications, there seems to be little hope to resolve this difficulty. The set of justifications of the following example has two well-founded admissible states, but there seems to be no reasonable way to select one of them as canonical. Later we shall discuss the class of the set of justifications which has one and only one well-founded admissible state.

Example 2. Consider the set of justifications J = {(p,0,{q}), (q,0,{p})} . Then there are two admissible states of J, i.e. {p} and {q}. It is easily checked that both are well-founded.

The following proposition shows that well­ foundedness subsumes minimality.

Proposition 2. Let D and S be as in the above definition. If S is a well-founded admissible state of D, then it is also a minimal admissible state of D.

Proof. Suppose that S is not a minimal admissible state of D. Then there exists a proper subset To of S which is an admissible state of D.

From this assumption, we shall construct an admissible state T of the TMS (N, { jn I n E S}, 0). Denote by Jo = { jn 1 n E S } the set of well-founded supporting justifications. Let J1 be the set consisting of justifications jn = (n, N1, N2l E Jo with N1 c To and T1 be the union of To and the set of consequent nodes of J1

T1=Tou{ n I jn= (n,N1,N2l EJO with N1cTo }. Let J2 be the set consisting of justifications jn = (n, N1, N2) E Jo with N1 c T1 and T2 be the union of To and the set of consequent nodes of J2

T2=Tou{ n I jn= (n,N1,N2) eJo with N2cT1 }. As J2 contains J1, T2 contains T1. By repeating this argument, we get a chain of sets

TO c T1 c ... CTi c .. ..

Denote by T the union of all the sets Ti (i ~ 0) . Then it is easily checked that T is an admissible state of the TMS (N,J0,0).

On the other hand, as TO is an admissible state of D, we see that the set of consequent nodes of J1 is a subset of To. Hence we get To= T1 = T2 = .. . =T. Thus, we obtain an admissible state To of the TMS (N,J0,0), which is a proper subset of S. This contradicts the assumption that S is a wellfounded admissible state of D. Q.E .D.

3. 2. The TMS and autoepistemic logic

If I is a finite set of formulas, we shall denote by AI (resp. VI) the conjunction (resp. disjunction) of the formulas in I.

Let D = (N,J,C) be a TMS. By considering N as a set of atomic propositions, we associate to any justification j = (n,N1,N2) an autoepistemic formula F(j) defined by

A{ Lk. I k E N1 }A A{ -Ll I l E N2 } :::J n.

Put F (D) = { F (j) 1 j E J}. For any subset S of N, we define an S5 Kripke structure k(S) by

k(S) = {VIV(s) = 1 for all SES} and an autoepistemic theory t(S) by

t(S) ={pi (V,k(S))I=p for all VEk(S) }.

Remark. The above translation rule has a natural interpretation. The node is "in" if and only if the corresponding atomic proposition lies in the autoepistemic theory (the set of "beliefs"). It is interesting that the above rule is very similar to the rule used in Konolige's proof [10] of the "equivalence" of default logic [19] and autoepistemic logic.

We can now state our main result.

Theorem 2 . The mappingS-> t(S) gives a

2) The set of stable expansions T of F(D) with

bijection between the following sets. 1) The set of admissible states of D. Ac~T for all CEC.

Proof. For any autoepistemic theory T, define a subset s (T) of N by s (T) = { n EN I n E T } .

It suffices to show the theorem for the case that C = 0. We shall proceed in three steps:

Step 1. If Sis an admissible state of D, t(S) is a stable expansion of F(D).

Step 2. If Tis a stable expansion of F(D), s(T) is an admissible state of D.

Step 3. s(t(S)) = S for any subsetS of Nand t(s(T)) = T for any stable expansion T of F(D).

Proof of Step 1. Let S be an admissible state of D. By Proposition l, to prove our claim, it suffices to show that

VEk(S) <=> Vt(S) (F(j)) =l for all jEJ. We first show the implication => . Let V be an element of k(S). By the fact that Sis an admissible state of D, we have Vt(S) (F(j)) = 1.

For the other implication, suppose that a propositional truth assignment V satisfies the RHS. By the definition of k(S), it suffices to show that V (s) = l for all s E S. Let s be any element of S. As S is an admissible state of D, there exists a supporting justification j of s. Thus, Vt(S) (F(j)) = Vt(S) (s) = V(s) = l. This shows the other implication.

Proof of Step 2. Let T be a stable expansion of F(D) and K be the corresponding S5 Kripke structure as in Theorem l. Let us show that s(T) satisfies l) and 2) of Definition 5. To show 1), let j = (n,Nl,N2) be an element of J such that N1 c s (T) and N2 c N\s (T) . Since T is a stable expansion of F(D), any V of K satisfies the condition VT (F ( j)) = l for all j E J. Thus, we have v (n) = 1 for v E K. This implies that nET. Now we show that s(T) satisfies 2) of Definition 5. Let s be an element of s(T). Suppose that there exists no justification j = (S,N1,N2) with N1 c s (T) and N2 c N\s (T) . Let V be any element of K and w be a propositional truth assignment such that W(n) = V(n) (n * s) and W(s) = 0 . Then it is easily observed that WT (F ( j) ) = 1 for all j E J. As T is a stable expansion of F (D), we have WE K by Proposition l. Since s belongs to the set s(T) = {pEN 1 V(p) =1 for all VEK},

we have W(s) = l, a contradiction.

Proof of Step 3. The equality s(t(S)) =Sis trivial. Let T be a stable expansion of F(D) and K be the corresponding S5 Kripke structure. To prove the equality t(s(T)). = T, it suffices to show that k(s(T)) = K. Note that

k(s(T)) = {VIV(s) = l for all SES(T)}

= { V I V (s) = l for all node sET } .

The inclusion k (s (T)) :::J K is clear. Suppose that V E k (s (T)) . By using the fact that s (T) is an admissible state of D, we easily see that VT(F(j)) = l for all jEJ. As Tis a stable expansion of F (D), we have v E K by Proposition l. This shows the other inclusion. Q. E.D.

In the original definition of autoepistemic logic, all the stable expansions are considered t o be of the same rank. For example, let A = {Lp :::J p} . Then there are two stable expansions of A, one has p as a belief and one has not. But in the former, p is believed on tenuous bases. The proposition p is derived because Lp is derived. This is a circular argument. The latter seems more appropriate for the belief set of the rational agent. This problem is similar to the circularity-check problem of the TMS.

Konolige [10] introduced strongly grounded stable expansions to get rid of stable expansions based on circular arguments. By using his idea, we can extend the correspondence given above to the TMS with circularity- check.

To introduce the notion of strongly grounded stable expansions, we first give the definition of minimal stable expansions.

Definition 8. Let A be a finite set of autoepistemic formulas. A set of autoepistemic formulas T is called a minimal stable expansion of A if T is a stable expansion of A and the corresponding S5 Kripke structure is maximal among all the S5 Kripke structures corresponding to stable expansions of A.

Then the following characterization of minimal admissible states is a direct consequence of Theorem 2.

Theorem 3. The mappingS-> t(S) gives a

bijection between the following sets.

1) The set of minimal admissible states of D.

2) The set of minimal stable expansions T of F (D) with /\c ~ T for all c E C.

Proof. It is sufficient to show that, for a minimal admissible state S of D, the stable expansion t(S) of F(D) is minimal. Let K denote the SS Kripke structure which corresponds to t(S) . Suppose that t(S) is not minimal. Then there exists a stable expansion T' such that the corresponding SS Kripke structure K' includes K properly. Since 1\c f t (S), we immediately have 1\c ~ T'. Thus, T' also corresponds to an arunissible state of D, a contradiction. Q.E.D.

An autoepistemic formula is said to be normal if it is of the form

L0.1A ... AL<XmA-L~p .. . A-L~n -:)'Y (i, j ~ 0), where ui, ~j andy are propositional formulas. The autoepistemic formula F(j) attached to the justification j is normal. Konolige [10] defined the notion of strongly grounded stable expansions for the set of normal autoepistemic formulas. Notice that the strongly grounded stable expansions of the given set of premises is dependent on the presentation of the formulas.

Definition 9. Let A be a finite set of normal autoepistemic formulas and T be a stable expansion of A. The set T i s said to be a strongly grounded stable expansion of A if T is a minimal stable expansion of A', where A' is the subset of A defined as follows:

The following theorem shows that states acceptable to the TMS (with "circularity-check") are completely characterized as strongly grounded stable expansions of the normal autoepistemic formulas attached to justifications.

Theorem 4. The mappingS-> t(S) gives a bijection between the following sets.

1) The set of well-founded admissible states of D.

2) The set of strongly grounded stable expansions T of F (D) with /\c ~ T for all c E C.

Proof. Suppose that S is a well-founded admissible state of D. By the definition, there exists a set of well-founded supporting justifications { jn I n e S } . Denote by Jo the subset of J such that

Jo={j=(n,Nl,N2)EJinES, N2cN\S}. Remark that jn E JQ for all n E S and that S is also a well-founded admissible state of (N,Jo,C). To show that the stable expansion t(S) of F(D) is strongly grounded, it is sufficient to show that t(S) is a minimal stable expansion of F(JO). By Proposition 2 and the above remark, we see that S is a minimal admissible state of (N,Jo,C). By Theorem 3, we conclude that t(S) is a minimal stable expansion of F(Jo) .

Let T be a strongly grounded stable expansion of F(D). Then Tis a minimal stable expansion of F(J'), where J' is the set of justifications given by J'={j=(n,Nl,N2)EJinET, N2nT=0}. Thus, s (T) = { n EN 1 nET } is a minimal admissible state of J' by Theorem 3. Let J1 be the set of justifications j= (n,N1,N2l EJ' with N1=0 and S1 be the set of consequent nodes of J1

S1 = { n I j = (n, 0, N2) E J'}.

Let J2 be a set of justifications j = (n, N1, N2l E J' with N1 c s1 and S2 be the set of consequent nodes of J2

S2 = { n I j = (n,N1,N2) E J' with N1 c S1l. As J2 contains J1, S2 contains S1. By repeating this argument, we obtain a chain of sets

S1 c S2 c ... c Si c .. . c s (T) . Denote by S the union of all Si (i~O). Then it is easily checked that the subset S of s(T) is an admissible state of J'. By the minimality assumption of s (T), we get S = s (T) . Let n be an element of s(T) and i be the least integer such that n e Si. We define the supporting justification jn of the node n to be the justification j = (n, N1, N2) E J' such that N1 c Si-1 (In the case that i = 0, we let S-1 = 0.). It is easy to see that the set { jn 1 ne S) is a set of well-founded supporting justifications of S. Q.E.D.

4. Stratified case

In general, a TMS may have no well-founded admissible state and may have more than one. But if we impose suitable restrictions on the use of outlists, we can guarantee that the TMS has a unique well-founded admissible state. In the rest of this paper, we shall discuss such a class.

The problem of nonmonotonic justifications in truth maintenance has a strong similarity to that of negation in logic programming. In the field of logic programming, there are also many attempts to extend logic programming incorporating the full use of negation [2,18] . However, all of them have several difficulties. Especially, any positive use of negation in the presence of recursion has not been obtained [20) .

Apt, Blair, Walker and Van Gelder [1,21) introduced a class of sets of clauses which prohibit recursion "through negation". From the semantic viewpoint, in such a set of clauses, we only negate propositions whose meanings are fixed beforehand. Then a "canonical" model is assigned to such a set of clauses.

We here adopt their idea. We shall consider the set of justifications which is "stratified". Our result says that a stratified set of justifications has a unique well-founded admissible state. We suppose that this result is of practical importance in the use of the TMS.

Definition 10. A partition

J = J1 u ... u Jn (dis joint union)

is called a stratification of J if the following two conditions hold:

1) If a node n occurs in a justification in Ji, its definition is contained within Uk{iJk.

2) If a node n occurs in the outlist of a justification in Ji, its definition is contained within Uk<iJk. (The definition of n is the subset of J consisting of all the justifications whose consequent nodes are n.)

Then J is said to be stratified by J1u ... uJn and each Ji is called a stratum of J.

Example 3 . Let J1={(p,0,{q}),(q,0,{p})}. Then there exists no stratification of J1.

Let J2=! (p,{p},0), (q,0,{p}) }. Then the partition J2 = {(p,{p},0)}u{(q,0,{p})} is the stratification of J2.

Let D=(N,J,C) be a TMS. We shall say that Dis stratified if J is stratified. Our result is

Theorem 5. Let D = (N, J, 0) be a stratified TMS. Then D has one and only one well-founded admissible state.

Proof. Let the partition J = J1 u ... u Jn be the stratification of J. We first construct a well­ founded state s by using this stratification.

Put So = ". For an integer i such that 1 { i { n, we shall define sets of nodes Si. Suppose that Si-1 is already defined. Define the set of justifications Ji(1) by

and define the set of nodes Si (1) by

Si < 1 > = Si-1 u{ n I j = (n,Nl,N2) E Ji (1)}. Define the set of justifications Ji(2) by

and define the set of nodes Si(2) by

Si<2l =Si-1u{ n I j= (n,N1,N2) EJi(2l}. As Ji<2l contains Ji(1J, Si(2) contains Si(1). Define Ji(3) by

Ji(3J =( j= (n,Nl,N2) EJil N!CSi(2J, N2nSi-1=0}

and define the Set of nodes Si (3) by

Si (3) = Si-1 u{ n I j = (n, N1, N2} E Ji (3} } . By repeating this construction, we obtain a chain of sets of nodes

Si (1) c Si !2l c. .. c Si (m) c ....

Denote by Si the union of all Si (m) (m ~ 0). Thus, we obtain Si for all 1 { i { n. We put S = Sn .

We now prove that S constructed above is a well­ founded admissible state of D. First we show that S is admissible. Let j = (n,N1,N2) be a justification such that N1 c s and N2 n S = ". Let us show that n E S. Suppose that j E Ji. Then we have N1 c Si, hence N1 c Si (k) for some positive integer k. Because Si-1 c S, we see that j belongs to the set Ji (k+1) , hence n E Si (k+l} c Si.

On the other hand, suppose that n E S. Then there exists an integer i such that j= (n,N1,N2) EJi with N1CSi and N2nSi-1=0. By the construction of S, we see that N2 n S = "· Thus, j is a supporting justification of s.

We now prove that S is well-founded. We associate a node n E S with its supporting justification jn as follows: Let i be the least integer such that n E Si. Then there exists an integer k such that n E Si (k) \Si (k-l) . By the construction, there exists a justification jn = (n,N1,N2) such that N1 c Si (k-1) and N2nSi-1=0. It is easy to check that (jn 1 n E S) is the set of well-founded supporting justifications of S.

Conversely, let T be a well-founded admissible state of D. Denote by Ni the set of nodes whose definitions are contained within Uk{iJk. To show that S and T coincide, it is sufficient to prove that Si = S nNi = TnNi for all i by using induction on i. Notice that, by the stratifiability of J, Si and TnNi are well­ founded admissible states of the TMS (Ni,ukiiJk,0) for all i.

For i = 0, both sides are empty. Let us assume that Si = TnNi. We first show that Si+1 c TnNi+1. It suffices to prove that Si+1 (k) c T for all k by induction on k. Let n E Si+1 (l). By the construction of S, the-re exists a justification j= (n,N1,N2) such that N1 c Si and N2 n Si = " . By the assumption, we have N1 c T and N2 n T = ". Thus, nET . Suppose that Si+1 (k) c T for an integer k. Let n E Si+l (k+1). Then there exists a justification j = (n, N1, N2) with N1CSi+1(k) and N2nSi=0. By the assumption, we have N1 c T and N2 n T = 0, hence nET. Thus, we get Si+1 (k+l) cT. Hence we know that Si+1CTnNi+1. But Si+1 and TnNi+1 are both well-founded admissible states of (Ni+l,Ukii+1Jk,0), hence minimal admissible states of (Ni+l,uk{i+1Jk,0) by Proposition 2. Thus, we obtain Si+l = TnNi+1. This establishes our induction step. Q.E.D.

Remark. Theorem 5 suggests a relationship between the semantics of the TMS and that of logic programming . In fact, the fixpoint semantics can serve as yet another semantics of the TMS. In [8], the authors clarified the semantics of the basic ATMS in terms of propositional Horn logic. The correctness of the label update algorithm follows from the least fixpoint semantics. We also proposed an extended ATMS architecture based on the iterated fixpoint semantics of stratified logic programming. We hope to discuss the relationships among these results in the subsequent paper.

5. Comparison with related work

Reinfrank and Dressler [17) independently have established the relationship between the TMS and autoepistemic logic. Their result and ours are essentially equivalent. The differences between them lie mainly in technical subtleties: Our method is based on Moore's possible world formulation and theirs is based on Konolige [10) . Our definition of states acceptable to the TMS with circularity-check seems to be nearer to Doyle's original one than theirs, but they turn out to be the same.

We suppose that the uniqueness of the well­ founded admissible state of the stratified TMS is suggestive to proposals of extended ATMS architectures.

Conclusion

To make nonmonotonic inference a practical technique, we must fully understand the semantics of Doyle's TMS. In this paper, we have shown that its semantics is completely described in terms of autoepistemic logic. States acceptable to a TMS correspond bijectively to stable expansions of a set of autoepistemic formulas attached to justifications. The implementation of the new TMS algorithm based on autoepistemic logic is to be explored.