An Algebraic Foundation for Truth Maintenance

I. Introduction

:.attice-theoretic truth maintenance is a single theoretical ramework that subsumes various notions of truth main­ ;enance, including the assumption-based justifications re­ )Orted by de Kleer [de Kleer, 1984, de Kleer, 1986a, de {leer, 1986b, de Kleer, 1986c] and the nonmonotonic jus­ .ifications reported by Doyle [Doyle, 1979a, Doyle, 1979b, )oyle, 1978] . and Goodwin [Goodwin, 1982, Goodwin, .985, Goodwin, 1984, Goodwin, 1987]. Our complete body >f work on lattice-theoretic truth maintenance includes

• An analysis of the algebraic structure of truth main­ tenance
• An investigation of the abstract and concrete compu­ tational complexity of truth maintenance
• A formal account of the embedding of other forms of truth maintenance in the lattice-theoretic paradigm

n this note we focus on the first aspect, because of its 1trinsic interest, and because this aspect is a precursor to he others. Our express aim here is to present the lattice­ J.eoretic account of truth maintenance, cite the more important algebraic results vi$ a vi$ this account, and inter­ pret these results so as to cast a qualitative light on various computational considerations of truth maintenance. Read­ ers interested in other aspects of our theoretical work or our practical experience with an implementation embody­ ing this theory are referred to [Benanav et al., 1986].

*This work was parti&lly supported by the Defense Adv&nced Re­ :&reh Projects Agency (DARPA) under USAF/Rome Air Devel­ 'ment Center contr&et F30602-85-C-0033. Views &nd conclusions mh.ined in this p&per &re those of the &uthors &nd should not be terpreted as representing the offici&! opinion or policy of DARPA · of the U.S. government .

The initial motivation for this work was the desire to unify in a single abstraction the truth maintenance paradigm of Doyle and Goodwin, and that of de Kleer. The systems of these investigators can be viewed as con­ straint propagation mechanisms. Given a disjunctive set of sets of premises and a set of (monotonic) deductive con­ straints, de Kleer's ATMS tells a client problem solving system what things it is currently obliged to believe, as­ suming one or another of the sets of premises. Doyle's and Goodwin's TMS's, on the other hand, tell the client prob­ lem solving system what things it is currently obliged to believe, given a single set of premises under deductive con­ straints, some of which may be nonmonotonic in nature.* Our original intuition was that it should be possible to account $imultaneou$ly for multiple sets of premises and nonmonotonic deductive constraints.** · ···

This intuition arose from the striking similarity ob­ served between the computations of truth maintenance systems and the computations of global flow analysis that underly modern optimizing compilers [Aho and Ull­ man, 1977, Hecht, 1977, Schaeffer, 1973, Waite and Goos, 1984). Global flow analysis can be couched in the following terms: Given the constraints imposed by individual pro­ gram statements and their interconnecting topology, what facts is a reasoning agent (in this case concerned with pro­ grams) obliged to believe about the state of computation at various points in the program's control flow? In a sense the information propagation problem solved by global flow analysis can be viewed as the dual of the truth maintenance problem. The former assigns propositions to contexts es­ tablished by various paths through a program. The latter assigns contexts of belief to propositions under various de­ ductive constraints. There are two principal methods of solving information propagation problems. Both hinge on , solving systems of equations whose unknowns range over the domain of an algebraic lattice. The work that we will describe prese11tly retains the idea of equations over a lattice, but for various technical reasons (principally non­ monotonic constraints) the solution methods used in global flow analysis are inappropriate. A rather different solution method has been developed.

· A monotonic deductive constra.int obliges & r&tionaJ &gent to be­ lieve its consequent , given th&t it currently believes a.ll of its &n­ tecedents. A nonmonotonic deductive constra.int obliges & r&tion&l &gent to believe its consequent given th&t it believes aJI of its mono­ tonic &ntecedents &nd none of its nonmonotonic &ntecedents.

· · The intellectuaJ cha.llenge of unifying these two &ppro&ehes to truth m&inten&nce is sufficient motiv&tion for proceeding. Nonethe­ less, we note th&t de Kleer (de Kleer , 1986b), &nd Morris &nd N&do [Morris &nd N&do, 1986) &re pr&ctica.lly motiv&ted to &ugment their assumption-b&Sed truth m&inten&nce systems to support some form of nonmonotonic justific&tion. In our &ppro&eh nonmonotonicity will be "built-in" r&ther th&n "&dded-on". Although we will not do so here, it c&n be shown th&t our conceptua.lly p&rsimonious &ppro&eh is &t & comput&tion&) adv&nt&ge rel&tive to the &ttempts of de Kleer, &nd Morris &nd Nado.

···we h&ve recently been m&de ·&w&re of the work of McDermott [McDermott, 1983) whose perspective on truth ma.inten&nce hu much in common with our own. Indeed, his concrete solution to wh&t we will eventua.lly define &S even equational !y!tem. &ppe&rs to be identic&) to ours, though &rrived &t from & quite different point of de­ p&rture. Our investig&tion is bro&der in both the scope of equ&tion&l systems investig&ted, &nd in the ch&r&cteriz&tion of those systems' structures &nd solution sp&ees.

II. Lattice Equational Systems

Let 8 be a Boolean lattice equipped with the usual meet, join, and complementation operators; a partial or­ der, <; and maximum and minimum elements, T and 1., respectively.* A complete account of such structures can be found in any of [Balbes and Dwinger, 1974, Birkhoff, 1967, Skornjakov, 1977). Elements of 8 will be called situa­ tions, and will be denoted by A and B. A and B (possibly subscripted) are lattice expressions in 8. Moreover, if A and B are expressions in 8 then so are A V B, A A B, A and B. Especially important to us will be the existence of the partial order, the complement, maximum and mini­ mum elements, and the mutual distributivity of meet and join.

A lattice unknown is a super- and/or subscripted s. Each lattice expression in 8 and unknown is a lattice form in 8. Moreover, if X and Y are forms in 8 then so are XV Y, X A Y, X and Y . Individual (fixed) lattice forms in 8 will be denoted by X and Y, possibly subscripted. Every fact or proposition has an associated unknown. Note that a proposition and its negation have distinct associated unknowns. Indeed, an unknown corresponds exactly to a node as that term is used by Doyle, Goodwin, and de Kleer. A lattice equation over 8 is a relation of the form X = Y where X is a lattice unknown and Y is a lattice form. A lattice equational system over 8, E, is any collection of lattice equations over 8 such that the total number of lattice unknowns occurring on the right-hand sides of the equations is finite and any lattice unknown occurs at most once on the left-hand side of an equation. The equation on whose left-hand sides appears will be called the s equation.

*In this report we assume B to be a recursive set, its operators to be total recursive functions, and its partial order to be a recursive relation.

E will be sub- or superscripted when it is useful to distinguish among various equational systems. Unless the context is ambiguous, we will freely say 'system' without modifiers. A lattice equational system should be inter­ preted as encoding the way a reasoning agent's belief (or disbelief) in a collection of propositions entails belief in others. If E is a lattice equational system such that the right-hand side of each equality is of the form V; /\(· X;i where each X;j is an element of 8 or an unknown pos­ sibly complemented), then E is said to be in disj~ctive normal form.* Since we can transform any form il.to dis­ junctive normal form, we will usually treat forms over 8 and lattice equational systems as if they were in disjunctive normal form.

A solution to a lattice equational system, E, is a func­ tion, r, from the lattice unknowns into 8 such that if for each equation in the system, each unknown s in the equa­ tion is replaced by r(s) the equation holds in 8. Moreover, r takes any unknown, s, not on the left-hand-side of some equation in E into 1., and in that regard the system E im­ plicitly has the equation s = .l. We will interpret lattice equations as constraints. A solution, then, is a labeling of propositions with situatiom. In particular, the situations are those in which a rewoning agent is obliged to believe the correspondingly labeted proposition given acceptance of the constraints imp()sed by the system. We will often subscript 'r' with the name of the system of which it is a solution. A justification of a disjunctive normal form lat­ tice equational system, E, is an ordered pair, d = (s, X}, where s appears on the left-hand side of some equation in E and X is a d: .. ,junct on the right-hand side of that same equation. AlE:o, s is called the consequent of the jus­ tification d and each conjunct of the disjunct X is called a nonmonotonic or monotonic antecedent of d depending on whether or not it is complemented. The sets of mono­ tonic and· nonmonotonic antecedents of d are respectively denoted a( d) and a( d). A justification, d, is valid with re­ spect to a situation, A, and a solution, r, of an equational system E if and only if,

We will write Valid(A,d,r) to indicate that dis valid with respe~t to A and solution r. A solution, r, is well­ founded with respect to a lattice equational system, E, at lattice unknown, s, if and only if either r( s) = l., orr( s) = V; A;, and for each A;, there is a partially ordered set, (P A;, -<A,}, such that P A; is a set of justifications from E and

1. There is a justification, d in PA, , whose consequent is s

*We use disjunctive normal form for notational convenience. While its existence is required in establishing some of the formal re­ sults that we cite, it plays no essential role in lattice-theoretic truth maintenance computations.

1. For every justification d, in 'PAn Valid(A;,d,r)
2. Every unknown, 8 1 , that is a monotonic antecedent of some d in P A; is also the consequent of some justifi­ cation d' in P A; and d' -(A, d

A solution to a lattice equational system is well-founded if and only if it is well-founded with respect to the system at every lattice unknown mentioned in the system.

We interpret justifications, validity and well-founded­ ness in the following way: Validity describes the circum­ stances under which the consequents of a justification are to be believed given the belief status of the antecedents. A justification therefore constitutes an independent source of support justifying belief in a consequent. Chaining justifi­ cations together constitutes a supporting argument . Since we wish our arguments to be noncircular, we impose an additional condition, well-foundedness, to guarantee that state of affairs.

Let us first consider some uninterpreted equational systems, all taken to be over the Boolean lattice, 8, having at least two distinct elements: The system E1

has one well-founded solution, { 8 = ..l}. On the other hand, any of { { 8 = A} lA "# ..l and A E 8} are also solu­ tions, though not well-founded. The system E2

the classical "odd loop" of Doyle's TMS, has no solutions, well-founded or otherwise. The system E3

has one well-founded solution, { 81 = ..l, 82 system E4 ..l}. The

has well-founded solutions {{ 81 = A, 82 The system Es A}IA E 8}.

has a single solution {81 = T,82 = T}, and it is not well­ founded. Finally, E6

has well-founded solutions {{ 8 1 = ..l, 82 = A, 83 =A} lA E 8} u {{81 = A,82 = ..l,83 = A}IA e 8} u {{81 = A,82 =

A,83 = ..i}IA E 8}. If 8 = {T,..l} and interpreting T as

"IN" and ..l as "OUT", it should be apparent to readers familiar with the TMS's of Doyle and Goodwin how lattice equational systems correspond to their TMS nodes and justifications.

The correspondence with de Kleer's ATMS is a little harder to convey, and we shall attempt only an approx­ imation here.* We shall do this by actually interpreting a lattice equational system with respect to a toy applica­ tion. Imagine a simple series-connected circuit consisting of a voltage source, V, of 5 volts connected to resistor R1 at node n~, which in turn is connected to resistor R2 at node n2 , which is connected to ground. The application is a pro­ gram that diagnoses ground faults in electrical circuits. In its truth maintenance database it has the following system of equations, E1:

The situations A, E 1 , and E2 respectively correspond to the assumption that the voltage source, V, and resistors, R1 and R2 , are working. 81 corresponds to the proposition that voltage at node n1 is held at 5 volts. 82 corresponds to the conjunctive proposition that the current into the resistor and node n1 is the same as the current out of the resistor R1 at node n2 and that the voltage drop across the resistor is the product of its resistance and the cur­ rent through. 8 3 corresponds to the conjunctive proposi­ tion that the current into the resistor R2 at node n2 is the same as the current out of the resistor at ground and that the voltage drop across the resistor is the product of its resistance and the current through. Finally, 84 corre­ sponds to the proposition that the voltage at node n2 is the product of 5 volts and the resistance of R2 divided by the sum of the resistances of R1 and R2 · The equations can now be interpreted as saying that the propositions associ­ ated with 81, 82, and 8 3 hold whenever the corresponding assumptions can be believed. The proposition associated with 8 4 is believed whenever the propositions associated with 81, 82, and 8 3 are believed. A solution to this sys­ tem will tell us the circumstances under which the various propositions are to be believed. Since the well-founded so­ lution is {81 = A ,82 = E1,83 = E2,84 =A 1\ E11\ E2}, a reasoning agent believes the propositions associated with 8 1 ,82 ,83,and 84 in situations whose meets with (respec­

tively) A,E1,E2, and A 1\ E 1 1\ E2 are not ..l.

In the foregoing exa~ples we have made implicit use

of the fact that any set of TMS or ATMS justifications has equivalent renderings in the lattice-based formaliza­ tion. For our last example we consider the classical prob­ lem of adding facts to or deleting facts from worlds or states. To begin with, we interpret situations as worlds or states. We have already asserted that every fact or propo­ sition, p, has an associated unknown, say 8p· We will also posit additional unknowns, 8 11 and 8 4 , corresponding to the beliefs (respectively) that p has been added and that p has been deleted. Consider now the system of equations

*Readers interested in the precise details of encoding these other truth maintenance systems in the lattice-theoretic paradigm should consult [Benanav et al., 1986] .

The well-fo~ded solution of this system is { 8 11 = A, 8<1 = B, 8p =A /1. B}. Our interpretation of this solution is that a reasoning agent believes p just in case he believes himself to be in a world or state whose meet with A /1. B is not . .1.. In addition, we can use the lattice partial order to encode inheritance among worlds. Notice that the fact p will be added to any world, A', such that A' < A /1. B and deleted from any world, B', such that B' ~ ii. '

III. The Existence of Solutions

We have seen how lattice-theoretic truth maintenance is connected to some well known models of truth mainte­ nance; we now turn to the challenge of actually solving truth maintenance problems is this new paradigm. We have already seen in r:2 that solutions need not exist, but even if they do (as in r:5), there may not be well­ founded ones. It is well known that general polynomial equations in rational coefficients cannot be solved by ap­ plying the operations of addition, multiplication, and ra­ tional root extraction to their coefficients (Birkhoff and MacLane, 1965, van der Waerden, 1953). By analogy we might ask about the solvability of lattice-equational sys­ tems by taking meets, joins, and complements of lattice expressions appearing in the equations. Put another way, could it be the case that the equations are not solvable by applying the obvious operations to the available data? To answer this question we must first formalize our notion of the 'available data'.

A 3urface element of a lattice equational system r: is an element of 8 that actually appears in r:. The Boolean lattice generated by meets, joins, and complements over the surface elements is called the 3urface lattice. An atom of the Boolean lattice, 8, is any element, A E 8, A :f .l, such that there is no B E 8 satisfying A > B > .l. A lattice is atomic if each of its elements is the join of atoms. If r: contains only a finite number of equations, the number of surface elements is finite and thus the surface lattice is atomic. The atoms of this lattice will be called 3urface atom3. A 3urface 3olution is one such that for every lattice unknown, 8, that appears in r:, r( 8) is in the surface lattice. Consider again the system, r:4 · Note that it has many possible well-founded solutions (depending on the Boolean lattice with respect to which the system is being interpreted) of which only two, {81 = T,82 = .l} and { 81 = .l, 82 = T} are surface. Our question posed in the last paragraph is answered by the following:

Theorem 111.1 If a finite lattice equational 3y3tem r: over 8 ha3 a well-founded 3olution, then, it ha3 a well­ founded 3urface 3olution.

Thus we see that if there are any well-founded solutions at all, we are guaranteed that'some of them can be computed by taking meets, joins, and complements over the available data.

Thus far we have established a framework within which we can formally describe truth maintenance prob­ lems and within which solutions can be connected with the available data in the equations. For this framework to be truly useful we must provide a way of finding solutions other than by blindly enumerating candidates and testing them. Suppose we could obtain a solution. How do we ~now that this is the only solution? Or even the only 3Ur­ face solution? To convey some idea of the challenge of this problem consider the system r;8

This system has 2n well-founded surface solutions. 8 is always .l and we are free to choose .l or T as the value of each of the odd-indexed unknowns. The usual method of solving algebraic equational systems is by using sub­ stitution together with other "legal" (with respect to the algebraic system in question) transformations to produce a new lattice equational system whose solutions are also solutions of the original. Because of the algebraic nature of the meet and join operators there is no obvious way of effecting such a transformation. Before introducing the more novel transformation that we will need, let us first formalize the notion of substitution that we will be using.

Let r;_. be r: less its 8 equation. Systems will be pre­ sented always according to some fixed lexical order. This is possible since each system is obviously a recursive set . Hence it is reasonable to speak of the nth occurrence of the unknown, 8, on the right-hand side of an equation in r:. We define a local3ub3titution, O'·,n, as follows: If the 3 1 equation is the locus of the nth occurrence then q (r:) ' .s ,n is r:_., together with a new 8 1 equation wherein the nth occurrence of 8 is replaced by the right-hand side of the 8 equation in r:. If there is no nth then q ·,n(r:) = r:. Suppose there are k 8's in r: before the s equation, min the 8 equation, and n after the 8 equation. The (global) 3Ub3titution tran3formation of r: under 8, q .(r:), is

This transformation has the effect of replacing every right­ hand side occurrence of 8 (except those in the 8 equation)

with the right-hand side of the s equation. The follow­ ing lemma suggests the other transformation necessary for computing solutions.

Lemma III.l Let X1, X2 and X3 be expre!!ion! having no occurrence of s, then

where r is a solution of a sy!tem including the s equation.

Let the s equation be rearranged to have the form: s = X1 V (X2 As) V (Xa V s). The distributive nature of the Boolean lattice guarantees that we can always do this. The minimization tran!formation of ~ under s, J.lo(~), is ~-· together with the equations= X1 V X3. This transforma­ tion is semantically equivalent to having substituted .l for every occurrence of s on the right-hand side of the s equa­ tion. Or put another way, we are taking the lower bound of the solution interval defined in the previous lemma.

We ask then whether or not minimization and sub­ stitution can be used to produce a solution. The answer will always be in the affirmative for an important class· of equational systems. We may apply these transformations to the original system of equations in such a way as to yield a new system free of unknowns on the right-hand side. The resulting system constitutes a solution for the original sys­ tem of equations. Before discussing the exact method of applying these transformations, however, we offer the fol­ lowing apparently technical but actually qualitatively im­ portant result about minimization and substitution.

Lemma III.2 A well-founded solution, r, of a lattice equational !ystem, ~' is a well-founded !olution of 0' .(~) unless 0' · involve! a local sub!titution for a complemented occurrence of s. If J.l·(~) = ~ 1 , then a well-founded !olu­ tion f 1 of ~I is a Well-founded !Olution of~.

A close examination of the proof would reveal that the substitution operation has the property that it preserves "solution-ness" but may lose · well-foundedness. On the other hand, minimization preserves well-foundedness, in the sense that any well-founded solution to the original system that per!i!t! in being a solution to the transformed system is still well-founded. Consider first the system ~4 · Applying the transformation u ., yields the system ~~

which has the same surface solutions as ~., but only the second of them is well-founded. Applying ~'·· to~~ yields

·The well-known truth maintenance systems in the literature only guarantee well-founded solutions for even equational systems.

which has only one solution, { s1 = .l, s2 = T}.

A proce!! for ~ is any functional composition of min­ imizations and substitutions. ~'·· 0' ·,n and 0' · are all pro­ cesses for any lattice unknown, s . If 1r is a process, so are J.l· o 1r, 0' ·,n o 1r and u · o 'Tr. A terminal process for ~. denoted T, is a process such that for every process 1r, T 0 1r(~) = T(~).

A path of length n from so to s n is a sequence of triples of the form

where Xi E {si-J,Si-1}, Xi is an antecedent of theY; dis­ junct of the Si equation in ~' and 1 ~ i ~ n. Xi is a complemented (uncomplemented) unknown if it is a com­ plemented (uncomplemented) conjunct of Y; . Unknowns is connected to unknown s 1 if there is a path of any length from s to s 1 · A path is odd if it has an odd number of complemented unknowns and even otherwise. A system is odd (and even otherwise) if it has an unknown, s, and an odd path from s to s.

Theorem III.2 Every even lattice equational !ystem, ~' ha! a terminal proce!!, T, such that f r(E) is a well-founded solution of~-

An immediate consequence of the previous theorem is an algorithm that is analogous to Gaussian elimination [Birkhoff and MacLane, 1965, Gantmacher, 1959] that will always produce a well-founded solution for an even lattice equational system:

1. Let x be a LIFO queue of the equations in ~; let y be an empty LIFO queue of equations in ~; let z be an equation in ~
2. Until xis empty, x becomes u.(J.I.(x)) (the order of equations remaining invariant with respect to their left-hand sides) where s is the unknown on the left­ hand side of the first equation in the queue, dequeue x to z, enqueue z toy
3. Until y is empty, y becomes 0' .(y) (the order of equa­ tions remaining invariant with respect to their left­ hand sides) where s is the unknown on the left-hand side of the first equation in the queue, dequeue y to z, enqueue z to x

4. End

This algorithm terminates with x being a queue of equa­ tions with constant right-hand sides (a solution). Step 2 is tlie analogue of forward elimination; step 3 corresponds to back substitution. Each (unspecified) order in which un­ knowns are removed from the queue, x, is an elimination sequence. Every such sequence produces a well-founded so­ lution (for an even system) and it may be the only sequence that produces that particular solution. In re-examining ~4 above we implicitly applied this algorithm, first eliminating s1 and thereby generating the first of the two well-founded surface solutions. Had we done the other elimination first, we would have obtained the second well-founded surface solution. Can we generate all of the surface solutions by varying the order of elimination? Unfortunately the an­ swer is no as can be seen by examining the following sys­ tem, E9 :

only three of whose four well-founded solutions can be pro­ duced by varying the order of elimination. As suggested by the statement of the theorem, there are odd lattice equa­ tional systems some of whose elimination sequences do not produce solutions. Such a system is E10 :

Addressing either of the aforementioned deficiencies re­ quires the separability results of the next section.

IV. The Structure of Systems and Solutions

In this section we discuss some separability results for lat­ tice equational systems. These results are of two classes: topological and algebraic. They are important because

• They provide the machinery from which all surface solutions to all equational systems may be generated
• They provide the basic perspective for analyzing the abstract complexity of the truth maintenance problem
• They s~ggest concrete "divide and conquer" algo­ rithms for solving the truth maintenance problem by
• supporting "lazy evaluation" of the solution vis a vis any given unknown
• supporting incremental update of solutions as jus­ tifications are added or removed
• enabling parallel solution methods

Let the equations of E be partitioned into equivalence classes in such a way that the s1 and s2 equations of E will be in the same equivalence class E', a subsystem of E, just in case St is connected to s2 in E and s2 is connected to s1 in E. Each equivalence class E' is a lltrongly connected subsystem of E. A partial order, ~E, can be defined on the strongly connected subsystems of an equational sys­ tem such that for subsystems E' and E", E' ~E E" if and only if there is an s' equation of E' and an s" equation of E" such that s' is connected to s". E" is minimal, if and only if there exists no E' such that E' ~E E". Given a partitioning of a lattice equational system E into strongly connected subsystems, there always exists at least one min­ imal strongly connected subsystem of E.

Proposition IV .1 Every lattice equational sy.stem can be partitioned into a partial order of strongly connected sub­ systems. Moreover, each of the.se subsystems can be treated as if the unknowns whose corresponding equations are in other strongly connected subsystems were lattice elements (i.e., constants).

Since we can solve each of the partitions separately, treating the unknowns whose corresponding equations are not in the strongly connected subsystem being solved as if they were expressions from the surface lattice (i.e., con­ stants), we can pursue a strategy of lazy evaluation and in­ cremental update. Not only can the system be partitioned very efficiently (Aho et al., 1974), but there are also effi­ cient methods of updating this partially ordered partition as justifications are added (and deleted). As things change in the truth maintenance database, we compute new parti­ tions and only re-solve for unknowns whose equations are in the same strongly connected subsystem as the changed equation, and (optionally) for unknowns in greater subsys­ tems. For example, consider E10 · This system partitions into two strongly connected subsystems. The s1 and s2 equations form the first and lesser (in ~E10 ) subsystem; the second strongly connected subsystem consists of the sa equation. We can solve the second subsystem, treating it as if s 1 were a constant. Note that the sa equation has a solution only in the case that s1 = sa = .l. This "forces" the solution of the first subsystem to be {s1 = .l, s2 = T}.

A lattice equational system, E, is reduced if and only if for every pair of unknowns s and s' whose equations are in the same strongly connected subsystem of E such that s is an antecedent of s' in E, s is a nonmonotonic antecedent of s'.

Theorem IV.l For every lattice equational system, E, there is a process, 1r, such that E' = 1r(E) is reduced, and r is a well-founded solution of E if and only if it is a well­ founded solution of E'.

The utility of the previous theorem becomes clearer when we combine the computation of strongly connected subsys­ tems of a system with reduction and minimization. Since we need to do only substitutions through uncomplemented occurrences of unknowns in the original system in order to reduce it, the resulting system has exactly the same well­ founded solutions as the original. Reconsider now E8 . If we minimize with respect to s and reduce again we get the reduced system:

The system has now been separated into n + 1 strongly connected subsystems, each of which is disconnected from the others, hence independently solvable. We see now how the 2n solutions arise, since we have n repetitions of the system :E4.

If we combine the previous two results, and manipu­ late the proof of theorem 111.2 we obtain

Theorem IV.2 Let :E be a lattice equational -'Y"tem who"e "urface lattice ~ {T, .l}. Every well-founded "urface "olution of :E i" produced by some "equence of minimiza­ tion" and global "ub,titution,.

Thus if we restrict the lattice over which the equations are taken to correspond exactly to the TMS's of Doyle and Goodwin, each well-founded solution will be produced by some elimination sequence. Unfortunately, among the large number of elimination sequences, many (in the case of odd systems) do not produce solutions. Since we and others [McAllester] have independently shown the NP­ completeness (in the size of the equational system) of solv­ ing this restricted class of lattice equational systems, there can be no "easy" characterization of the circumstances un­ der which a particular elimination sequence will produce a well-founded solution.

We turn now to the question of how to find all the well-founded surface solutions for arbitrary systems. Let r, V r2, r, A r2, and A A r denote functions such that (r, V r2)(s) = r,(s) V r2(s), (r, A r2)(s) = r,(s) A r2(s), and (AAr)(s) = AAr(s). A Goodwin projectionofalattice element B with respect to an atom A, denoted 'YA(B), is defined by

We extend the notion of a Goodwin projection to expres­ sions over lattice elements by

and to lattice equations by applying the projection to each constant term in each eqU:atio~.

Theorem IV.3 rE ~ a well-founded ,urface $Olution of :E if and only if there exid" a "ub,et, {Ail1 :$; i :$; N}, of the atom" of the "urface lattice of :E, and corre,ponding Goodwin projection,, bA, 11 :$; i :$; N}, "uch that

where the r "'A; (E) are Well-founded $Urface $Olutio~.

This theorem guarantees a unique prime (where the primes are the surface atoms) factorization of lattice equa­ tional systems and their solutions. Notice that each Good­ win projection of a system :E results in a system whose surface lattice is {T, .l}. We "know" how to solve these by theorem IV.2. Hence factoring followed by finding all of the (successful) elimination sequences produces all of the surface solutions. In particular, all four of the well­ founded surface solutions of :E9 can be produced by tak­ ing the Goodwin projections with respect to the surface atoms, A and A, solving the two resulting systems, "mul­ tiplying" the resulting solutions by A and A respectively, and "adding" the results. Since each projected system has two solutions, the overall system has four. Elsewhere [Be­ nanav et al. J we have shown the problem of solving gen­ eral lattice equational systems to be NP-hard in the size of the system. We see now how this might arise: Using the algebraic results that we have cited can produce solu­ tions at the cost of composing two potentially exponential processes, the projection by surface atoms and the finding of minimization and substitution sequences that actually produce a well-founded solution.

V. Conclusions

In the foregoing we have introduced a general model of truth maintenance couched in a lattice-theoretic frame­ work. All of the truth maintenance systems familiar to us in the literature can be construed as solving systems of lattice equations. Indeed, those systems can be properly embedded in our lattice-theoretic formalism. We intro­ duced the fundamental transformations of substitution and minimization and showed how they could be used to pro­ duce solutions of even lattice equational systems. We have cited a number of theoretical results about the algebraic structure of truth maintenance systems and interpreted these results in terms of concrete examples. We have used these examples to illustrate how a given formal algebraic result either reveals some intrinsic difficulty, or how it can be used to computational advantage. Finally, we sketched how our separation results can be used to generate all of the surface solutions of an arbitrary lattice equational sys­ tem. The principal technical contributions of those aspects of our work on lattice-theoretic truth maintenance that we have presented in this paper are:

• The formalization of truth maintenance in a way that properly includes nonmonotonic justifications and assumption-based justifications
• The presentation of a point of view from which one can algebraically analyze the structure of truth main­ tenance problems and the construction of solutions to those problems
• The motivation of the algebraic results with computational and phenomenological interpretations

Though not the topic of this paper, it is also from this same lattice-theoretic point of view that we have carried out the analysis of the abstract and computational complexity of truth maintenance.