On the Relation Between Truth Maintenance and Autoepistemic Logic

1 Introduction

1.1 The Problem

Despite their importance in AI problem solving, non-monotonic truth maintenance systems still lack sufficiently well-understood logical foundations. Existing logical characterizations of truth maintenance suffer from one or several of the following problems:

• they do not correspond exactly to what a TMS actually does, as for example :\ML-1 [McDermott, 1980).
• they only consider the "easy" monotonic case, as for example Reiter and de Kleer's prime implicant theory for assumption-based truth

maintenance (ATMS) [Reiter and de Kleer, 1987). Recent work on non-monotonic justifications for the ATMS, [de Kleer, 1986b) and [Dressler, 1988), underlines the need for non-monotonicity in truth maintenance.

• they are based on new, specialized non ­ monotonic logics whose sole purpose is to characterize a TMS, as for example Brown's logic of justified belief [Brown, 1988). This is an interesting path to pursue, but it yields no insights into the relation between truth maintenance and the existing families of non­ monotonic logics.

The problem addressed in the present paper is to establish a link between non-monotonic truth maintenance and autoepistemic logic, that is, a "standard" non-monotonic logic.

1.2 Analysis of the Problem

An analysis of the problem shows that a logical theory of non-monotonic truth maintenance is hard to design because of the following characteristics of aTMS:

• it is finite and logically incomplete
• it is "brave" in the sense that it may adopt one of multiple, mutually incompatible belief states.
• it has a very strong and, in particular, inherently global notion of a belief state being grounded.
• non-monotonic justifications are asymmetric: disbelief in the non-monotonic antecedents can justify belief in the consequent, but disbelief in the consequent cannot justify belief in the non­ monotonic antecedents.

l.3 The Approach

We pursue a two-step bottom-up approach. First, we specify non-monotonic truth maintenance in a direct, non-logical theory. Then, the specification, together with the corresponding formal framework, is used to draw a connection to autoepistemic logic. The theory is a derivative of Jon Doyle's reasoned assumptions (Doyle, 1983], and is di scussed in (Reinfrank and Freitag, 1988] . It is built on the concept of a non-circular proof being valid relative to a current coherent belief state. To this end, a justification is considered as a rule of the form < alb~c > , where a is a monotonic antecedent and b a non-monotonic antecedent for the conclusion c (In general, we consider sets of antecedents). A justification is valid in a given setS if aES and beS. A set of such justifications is called a non-monotonic formal system (NMFS) . An extension of an NMFS is a set S such that every element of S has a non­ circular proof using only valid justifications, and where the conclusion of every valid justification belongs to S.

One can easily verify that extensions correspond exactly to the IN/OUT labellings of a non-monotonic justification-based TMS [Doyle , 1979, Goodwin , 1987]. With some minor extensions, NMFS-theory is also sufficient to describe an assumption-based TMS (de Kleer, 1986a].

1.4 The Solution

The key to a logical theory of truth maintenance now is to relate a justification < alb~c > to a self­ referential formula in autoepistemic logic CAEL), La/\-, Lb:::Jc, where L is an introspective modal operator, and La reads as "a is believed". This formula is essentially in AEL normal form (Konolige, 1988a], and therefore the AEL-transform of a set of justifications can be used as a basis for so­ called strongly grounded AEL-extensions. Notice that the scope of modal operators and the right-hand side of the implication are restricted to non-modal atoms. Given an NMFS J, the strongly grounded AEL-extensions of its transform JAEL correspond to the extensions of J, and hence to TMS-labellings, in the sense that a TMS labels exactly the non-modal atoms of a strongly grounded AEL-extension IN.

We show that a variant of Dressler's encoding of non-monotonic justifications in an ATMS [Dressler, 1988] is correct. Therefore it also inherits the AEL semantics. Dependency-directed backtracking and so-called nogood inferences are identified as a source of ungrounded conclusions.

2 A Direct Theory of Truth Maintenance

We consider a countable set V of propositional atoms. A TMS works with finite subsets of V. A

justification is a rule p = < AIB~c >, where A and B are finite sets of atoms, and cis a single atom. (We usually omit the set parentheses when enumerating the members of A and B.) pis valid in a set S~V (or S-val id ) iff A~S and BnS=0 . Note that a justification of the form < 010~c > is valid in every setS. It is called a premise justification, and c a premise. A non-monotonic formal system (NMFS) is a finite set of justifications.

Def. 2.1: Let J be an NMFS, S~V, and qEV. A J ­ proof for q valid in S is a sequence (ql>q2,· .. ,q 0 ) with the following properties:

1. qn =q (2) Vqi : qiES (3) Vqi: 3 <AIB~qi> EJ: A~{ql , ... qj.d 1\ BnS=0

In other words, a J-proof is a non-circular sequence of applications of S-valid justifications to intermediate conclusions.

De f. 2.2: Let J be an NMFS, S~ V. S is J -closed iff V<AIB~c> EJ: A~S 1\ BnS= 0 ~ cES.

Def. 2.3: Let ,J be an NMFS, S~V. Sis J-grounded iff every q E S has a J -proof valid inS.

Sometimes we need to consider sets that are only grounded in a substantially weaker sense.

Def 2.4: Let .J be an NMFS, S~V . S is locally J­ grounded iff every qE S has an S-validjustification.

Def. 2.5: Let J be an NMFS, S~V . Sis a J -extension iff

1. S is J -grounded and
2. Sis J-closed.

An extension thus has the property that it contains an atom if and only if a proof - valid in that extension - can be found for the atom. As we have shown in [Reinfrank, 1987], a justification-based TMS computes exactly the extensions. of its justifications. We can easily verify that NMFS have the following properties:

• finiteness : given that J is finite, so are its extensions.
• logical incompleteness : consider a propositional language L rather than a set V of constants as the domain from which just i fica t ions are form u 1 ate d . {<plpvq~r>,<010~p>} has the extension {p,r}, since a TMS fails to make the logically valid inference pVq from p.

• braveness: {<0jp-+q>,<0lq-+p>} has two extensions: {p}, {q}.
• strong, global notion of groundedness : {<pl0-+p>, <0lp-+q>} has exactly one extension {q}. ~otice that {p} is closed, locally grounded, that is, p is the consequence of a {p}­ valid justification, and it is minimal in that respect. But it is not grounded.
• asymmetry of justifications : the only admissible extension of { < 0jq-+p >} is {p}. It does not yield an extension {q}, where p is disbelieved and q believed, "backward" justified by disbelief in p.

The usual approach to achieving a higher degree of logical completeness, unless full responsibility for logical inferences is left to the problem solver, is to use sets of justifications to partially encode the meaning of connectives, as, e.g., in [McAllester 1980, de Kleer 1986b, Dressler 1988]. We do not consider such techniques in the present paper.

NMFS theory provides a direct yet implementation independent specification of justification-based truth-maintenance. It can be easily extended to non­ monotonic rules with variables [Reinfrank and Freitag, 1988]. The following results on NMFS are needed in order to formally prove their equivalence to the particular subclass of autoepistemic theories to be introduced later.

Lemma 2.6: Let J be an NMFS, E be a J-extension, J*kJ be the set of all E-valid justifications. Then E={c: <AIB-+c>EJ*}.

Lemma 2.7: Let J be an ~MFS, E a J-extension. There is no proper subset E'~E such that E' is a J ­ extension.

3 Autoepistemic Logic and Truth Maintenance

3.1 Strongly Grounded AEL·Extensions

AEL [Moore, 1985) is a cleaned-up version of McDermott and Doyle's first shot at a modal non­ monotonic logic [McDermott and Doyle, 1980]. In this section, we consider an AEL language based on a propositional logic. In [1988a], Konolige develops the concept of a strongly grounded AEL-extension of a given base set. It is meant to formalize AEL­ extensions in which a formula p always has a derivation independent of Lp. That is, Lp itself can only be derived from p, and hence strongly grounded AEL-extensions are a candidate for a logic of justified as opposed to simple belief. The definition of strong groundedness is partly syntactical, since the base set is assumed to be in a particular normal form.

Def. 3.1 (Konolige): An AEL formula pis in normal form iff p=..., LavL~tv .. .vL~nVY, where all of a, ~i. and y are non-modal formulae . Any of the disjuncts, except for y, may be absent.

For a set S of formulae, let LS = {Lp : pES}, ...,LS'={...,Lp: peS}, and So be the set of non-modal formulae contained inS.

Def. 3.2 (Konolige): Tis an AEL-extension of A iff

Def. 3.3 (Konolige) : Let A be in normal form, T an AEL-extension of A. Let A* be those formulae in A for which ~ieT, for all L~i · Tis strongly grounded iff

The sign F=ss here means that the modal index of autoepistemic valuations, which consist of an ordinary propositional interpretation and a set of beliefs, is restricted to stable sets. For details, see [Konolige, 1988a]. We use a slightly different definition of strong groundedness as the one given there . This modification is necessary both for Konolige's results on the relation between strongly grounded AEL-extensions and default logic, and for our purposes here. It is due to Konolige [1988b] .

A weaker notion of groundedness only requires minimality w.r.t. non-modal formulae . It is equivalent to:

Def. 3.4 (Konolige): LetT be an AEL-extension of A, which is not necessarily in normal form . T is moderately grounded in A iff

Simple AEL-extensions are called weakly grounded. AEL-extensions, and hence also strongly grounded extensions, are uniquely determined by the set of non-modal formulae contained in them, their so­ called kernel .

Lemma 3.5 (Konolige) : If two AEL-extensions agree on their non-modal formulae, they are the same.

3.2 The Translation from NMFS to AEL

We transform justifications into AEL-formulae as follows.

Def. 3.6: Let <al, . .. ,amlbl, ... ,bn~c> be a justification . Its AEL-transform is ..., L(a1/\. .. AamlVLb1 v .. .vLbnvc.

Since, in AEL, La1A ... ALam is equivalent to L(alA ... Aam), and using the definition of :J, the AEL-transform of a justification can be rewritten as

where all of ai, bj, and care non-modal atoms from V. For a premise < 010~c >,we get the atom c. Let J AEL be the set of transformed justifications of an ~MFS J . Given this particular form of a base set, and by view of Lemma 3. 5, the corresponding strongly grounded AEL-extensions are uniquely determined by the set of non-modal atoms contained in them. It is exactly this atomic kernel that is computed by a TMS.

For a set S of formulae, let At(S) be the set of propositional atoms in S, and Th(S) be the set of propositional logic consequences ofS.

Theorem 3. 7: Let J be an .:--J"MFS with AEL-­ transform J AEL·

1. Suppose T is a strongly grounded AEL­ extension of J AEL · Then At(To) is a J · extension.
2. Conversely, let E be a J -extension. Then Th(E) is the kernel of a strongly grounded AEL-extension T of J AEL·

3.3 Discussion

It is important to note that the theorem no longer holds if the justifications are formed from a full­ fledged propositional language rather than from a set of propositional atoms . The AEL base set {p, LpA..., L(pVq):Jr} has obviously no extension that contains r, since from p we get pVq, and hence ..., L(pVq) cannot be assumed. But {p,r} is a { < PICpVq)~r >, < 0l0~p >}-extension.

Also, the condition of strong groundedness is necessary~ since {Lp:Jp, ..., Lp:Jq} has a moderately grounded AEL-extension containing p, which is not strongly grounded. The corresponding NMFS has only {q} as an extension.

This poses the question as to ~MFS-counterparts to weakly or moderately grounded AEL-extensions. In some independent piece of work and cast in a quite different formalism, Fujiwara and Honiden [1989] show that weakly grounded AEL-extensions correspond to closed and locally grounded J · extensions, in the same sense as in theorem 3.7. In .:--J"MFS-theory, it is easy to show that in the monotonic case minimality of closed sets is sufficient to guarantee global groundedness . For a non­ monotonic ~MFS, however, even minimality of locally grounded sets is insufficient, as the example above shows. Similarly, the minimization involved in the definition of moderately grounded AEL­ extensions is too weak to capture the notion of grounded belief used in the TMS-world.

An additional filter is required for moderately grounded extensions . The definition of strong groundedness provides exactly that filter. (Note that it is related to a property of I\OMFS extensions given in Lemma 2.6.) As we elaborate in the long paper, this extra condition is similar in spirit to stability conditions in model-preference theories for default logic [Etherington, 1988] and logic programming [Elkan, 1989].

To our opinion, all of this may eventually shed some new light on the relation between proof theory and model theory in non-monotonic reasoning. The concept of a finite, non-circular proof which is valid relative to an overall coherent state of belief simply has some proof theoretic flavor which is hard to represent independently in the model theory.

3.4 Seman tical Considerations

Suppose we are given two justifications <alb~c> and <010~a>. The corresponding AEL-base set is {a, La/\..., Lb:Jc }. Figure 1 shows the usual graphical representation of justifications. A TMS­ labelling procedure proceeds as follows : a is a premise, so it is necessarily believed and labelled IN. In AEL, this corresponds to the K45 [Konolige, 1988a] inference step a/La. Since there is no valid justification forb, b is labelled OUT, which reflects the AEL-assumption ..., Lb. Now the justification for c has become valid, so it must be the case that c holds, and hence it is also labelled IN.That is, a

justification gets the following semantic interpretation: if a is believed (IN the database) and b is not believed (OUT of the database) then it must be the case that c is true and, consequently, must also be believed (IN). Note that this interpretation is different from the usual reading for a justification, where the direct and only conclusion is the self­ belief that c must be IN the database, without referring to the world in consideration.

A proper distinction between ...., La and ...., a is crucial to an understanding of truth maintenance. While there is no a priori preference for either of a and ...., a, and hence it might be the case than none of them is believed, ...., La is always preferred to La. I.e., a TMS only adopts the self-belief La if it is forced to do so because it follows from a itself. Otherwise it jumps to the assumption ...., La. As we will see in chapter 5, a confusion of a proposition being OUT and its negation being IN may lead to peculiar consequences.

3.5 Default Logic

AEL and default logic [Reiter, 1980] are essentially equivalent [Konolige, 1988a], in that the kernels of strongly grounded AEL-extensions correspond to extensions of default theories, where an AEL­ formula La/\ ...., Lb:Jc is translated to a default a:M...., b/c. (Since default logic does not preview an empty M-part, dummy conditions are introduced if needed) . Theorem 3.7 thus yields a relationship between NMFS and default logic as a corollary.

Corollary 3.8: Let J be an NMFS and ~.J be the default theory constructed from J AEL .

1. Suppose T is a default logic extension of ~J . Then At(T) is a J -extension.
2. Conversely, let E be a J -extension. Then Th(E) is a default logic extension of ~J -

This relationship is of some interest in its own right, because default logic has been given a semantics [Etherington, 1988] in terms of stable, maximally preferred sets of models. We show in the long paper [Reinfrank and Dressler, 1988] that the computations performed by a TMS can be regarded as operations on a condensed representation of such model sets.

4 Assumption-Based Systems

Theorem 3.7 begs the question as to a related theorem for a non-monotonic ATMS [Dressler, 1988]. A minor extension to NMFS-theory is sufficient to model an ATMS. We must allow for assumptions from a given set a<;;;;V to be used in J­ proofs.

Def. 4.1: Same conditions as in Def. 2.1, and a<;;;;V. A J-proof relative to a is a J-proof as in Def 2.1., condition (3) replaced by:

The definitions of J -grounded relative to a and J­ extension of a then are straightforward generalizations of Def. 2.3 and 2.5. An ATMS works with monotonic justifications of the form< Al0-+c > . J -extensions for a monotonic NMFS always exist and are unique.

Lemma 4.2: Let J be a monotonic NMFS, a<;;;; V. There is one and only one J-extension of a . We write Jext(a).

Given a distinguished set Ass<;;;; V, an ATMS simultaneously computes all J ext(a), aE 2Ass. To integrate non-monotonic justifications into the essentially monotonic ATMS-world, explicit Out­ atoms are introduced. For a given V, let OutV ={Out x: xE V}. Out-atoms may not occur as the consequent of a justification.

Def. 4.3: Let < alb-+c > be a non-monotonic justification. Its (monotonic) AT:vlS-transform is <a, Out bl0-+c> .

Obviously, there is a one-to-one correspondence between non-monotonic formal systems over V and those monotonic formal systems over VUOutV that do not permit Out-atoms as consequents. Non­ monotonicity in an ATMS then is achieved by manipulating assumption sets. A J-11-extension E of an assumption set a is an ordinary extension of a maximal augmentation of a with a set ~ of Out­ atoms. Out x is added to the basis aU~ if and only if x~E .

Def. 4.4: Let J be a monotonic N:vtFS over VUOutV, a<;;;;V. E is a J-11-extension of a iff 3~<;;;;0utV : E =Jext(aU~) 1\ (VxE V: Out xE ~ ¢::> x~E).

It is important to note that, unlike in [Dressler, 1988], J-11-extensions do not involve any so-called nogood inferences . It is exactly these nogood inferences that lead to problems of ungroundedness in an NMA TMS, cf. next section.

Lemma 4.5: Let J be a non-monotonic ~MFS over V, JATMS its ATMS-transform over VUOutV. Let a<;;;;V be an assumption set.

1. Suppose E is a J-extension of a and let ~={Out x: x~E}. Then EU~ is a JATMs-ll­ extension of a, with basis aU~-

1. Conversely, letS be a JATMS-j.l-extension of a. Then Sn V is a J -extension of a .

It is easy to see that every J-proof relative to a can be simulated with a JATMs-proof relative to aU{Out x: xfE}. Conversely, we can construct a J-proof for every ordinary atom in a JATMS-j.l-extension. Since the transform is bidirectional, Lemma 4.2 also works in the opposite direction (i.e. starting from a monotonic NMFS over VUOutV) and yields a one­ to-one correspondence between j.l-extensions for the NMATMS and strongly grounded AEL-extensions in the sense of Theorem 3.7 as a corollary.

5 Backtracking and Nogood Inferences

Consider an extended language including justifications of the form < aJb~ l. >, where l. stands for falsity. Let a be a premise. Since there is no way to derive bin the basic TMS-machinery, we get an inconsistent extension {a,l.}. A dependency­ directed backtracking routine, which is triggered whenever l. becomes IN, would in this case introduce an additional justification <al0~b> . Similarly, a nogood inference rule in the NMAT~S would infer <aJ0~b> from <a, Out bl0~1.> . This yields {a,b} as the atomic kernel of an AEL­ extension. It is strongly grounded in the extended base set. However, from the original base set {a, La/\ · Lb:Jl.}, we can only infer La and · LavLb, and hence get the ungrounded assumption Lb, independently of b.

In general, dependency-directed backtracking in a TMS and nogood inference rules in an ATMS can be considered as justification-generating rules of the form

with approriate control restrictions . This leads to modified base sets with new conclusions that are possibly not strongly grounded w.r .t . the original base set. A peculiar problem arises in an NMATMS due to justifications of the form < x, Out xl 0~ l. >, which are used to prevent x and Out x from being assumed simultaneously. This technique appears to be reasonable for de Kleer's negated assumptions [de Kleer, 1988]. However, in the case of genuinely non-monotonic Out-assumptions, together with nogood inferences, it leads to a confusion of inconsistency and incoherence, that is, non­ existence of any extension. This difference also suggests to use negated assumptions rather than Out-assumptions to encode logical connectives with sets of justifications.

Applied to the incoherent set {<Out pJ0~p> }, for example, a simple nogood inference step yields {p} as an extension. The corresponding AEL-base set has no extension at all, neither consistent nor inconsistent. More work is needed to come to a better understanding of the properties of backtracking and nogood inferences. [Morris, 1988] seems to be a first step in the right direction.

6 Related Work

Using the same translation as we do, but described in a quite different formalism, Fujiwara and Honiden [1989] prove a relation, similar to the one presented in theorem 3.7, between weakly grounded AEL-extensions and what we call closed and locally grounded NMFS-extensions.

Elkan [1989] has recently proposed a different translation, a/\ · Lb:Jc (a instead of La) . For the simple form of an AEL-language in consideration, it turns out that the weakly grounded extensions of the resulting AEL base sets correspond to the strongly grounded extensions using our translation.

I.e., three groups of researchers have come up independently of each other with related ideas and results, though formulated in superficially quite different formalisms . We consider this as evidence that we are on the right track, and that it was getting to be time to put non-monotonic truth maintenance on a sound logical basis . What is unique to our approach, compared to [Fujiwara and Honiden, 1989] and [Elkan, 1989), is the development of NMFS as a direct theory of truth maintenance, as well as the treatment of ATMSs.

Our research is similar in spirit to the work by Horty, Thomason, and Touretzky on logical theories of inheritance, cf. [Thomason and Horty, 1988) . They also pursue a bottom-up approach using intermediate direct formalizations. The situation in inheritance theory is comparable to the one in truth maintenance in that, in both fields, procedural realizations and network-based concepts were the starting point. We are currently working on a characterization of truth maintenance in a four­ valued logic, which is related to Thomason's approach.

7 Conclusions

We have established a relationship between non­ monotonic truth maintenance and non-monotonic logics. This provides the technical fundament for an alternative view of truth maintenance as inference in a non-monotonic calculus, in addition to the traditional view as an efficient mechanism for search and caching. We also have developed a direct theory of truth maintenance and presented a correct encoding of non-monotonic justifications in an assumption-based TMS. Our results contribute to closing an important theory-implementation gap, after TMSs and non-monotonic logics have been coexisting for more than a decade. They open the way for further research into the foundations of truth maintenance.

8 Proofs

Complete proofs, including an independent proof for Corollary 3.8, for the claims made in this paper are contained in [Reinfrank and Dressler, 1988].

Acknowledgements

Our work benefited from discussions with Frank Zetsche and the members of the Advanced Reasoning Methods Group.