Connections Between the ATMS and AGM Belief Revision

1 Introduction

Few would dispute the necessity of having a method of representing justificational information in a nonmonotonic reasoning system, but there is less agreement on what form these justifications should take. There are two distinct philosophical approaches to formalising the requirements for a belief to be justified by another belief or set of beliefs; these are called the foundational and coherence theories of justification [Pappas and Swain, 1978; Gardenfors, 1989].

1.1 The Foundational Theory

Foundational reasoning is based on the concept that each fact or belief is accepted on the grounds of other beliefs which justify it. These beliefs are in tum justified by others, forming a chain of supports for each belief. Infinite chains of supports are disallowed, as are cycles in the chains, so that each chain of inferences starts from a set of premises or assumptions. These are called the foundational beliefs, since they give support to the whole of the belief set, and yet are not supported themselves by any other beliefs.

A number of operational systems based on the foundational model have been developed, the most well-

1. 3 C e N such that C ~ E, (E is inconsistent), or
2. p e E, (p is an assumption), or
3. 3 (A,p) E J such that 'V a E A, E 1:.-nts a, (p has a well-founded justification).

(3) may be reformulated in terms of the A TMS label:

• 3*. 3 L e Label (p) such that L !:;;; E.

3 The AGM Logic

The AGM belief revision logic has been described at length in [Gardenfors, 1988]. It is based on a logically closed set of beliefs, K, with the closure operator denoted Conseq, so that K = Conseq (K) . Three basic operations are central to the system: expansion, contraction and revision, denoted K!. K;. and Ka respectively, where a is the sentence by which the belief set is being expanded, contracted or revised. The inconsistent belief set is denoted K 1.. Expansion involves adding a new belief to the belief set, with all of its consequences. A contraction is the removal of a belief from the belief set, accompanied by the removal of sufficient other beliefs so that the belief set remains consistent and closed under logical consequence. That is, the belief being removed must not be derivable from the remaining belief set. The third operation, revision, comprises the addition of a new belief to the belief set such that any conflicting beliefs are removed from the belief set, maintaining the consistency of the system. Revision can be defined as a contraction of the negation of the belief, followed by an expansion operation; this is called the Levi identity.

The postulates for contraction and revision do not define a unique function for either operation, so it is necessary to add some further constraints, in the form of an epistemic entrenchment relation, which is an ordering on the members of the belief set. Let Ent (p) denote the entrenchment of proposition p, where the entrenchments are ordered by the normal relational operators: <, :5 and =. Entrenchment orderings obey the following five axioms [Gardenfors, 1988]:

• (EEl) If Ent(A) :5 Ent(B) and Ent(B) :5 Ent(C) then Ent (A) :5 Ent (C)

(EE2) If A 1- B then Ent(A) :5 Ent(B)

• (EE3)ForanyA andB,Ent(A) :5Ent(AAB) or Ent(B) :5 Ent(AAB)
• (EE4) When K ;t K 1., A fi K iff Ent (A) :5 Ent (B) for all B

(EE5) If Ent(B) :5 Ent(A) for all B then 1- A

Then the AGM operators may be defined as follows:

Expansion: Kit = Conseq (K u a)

Contraction: K;; = { l3e K I 1-a or Ent(a) < Ent(avj3)}

Revision: K; = (K-:,a) ~

4 Translation Algorithm

4.1 Constructing an Entrenchment Relation

To specify an entrenchment ordering completely requires an ordering on the dual atoms. The number of dual atoms is exponential in the number of atoms in the language, and this gives us reason to look for a partial ordering which contains sufficient information to define the contractions which interest us, and which is consistent with the entrenchment axioms. In doing this, we are not defining an alternative to the AGM entrenchment axioms, but instead we are allowing many of the entrenchment values to be unknown, since we will never need to consult these values to implement the AGM contraction operator. Thus the partial entrenchment relation which we define may be extended to any full entrenchment relation (as long as it is consistent with the AGM entrenchment axioms), without affecting our results.

Since we are modelling ATMS environment changes, the only beliefs to be added or contracted are ATMS assumptions, which are atomic. In fact, our algorithm contracts one atom at a time, and for the results we require, the only beliefs we need to check for membership in K are also atomic (ATMS nodes). From the definition of contraction, we only need to know entrenchment relations between each assumption and the disjunction of the same assumption with each other atom. For any atoms a and b, (EE2) constrains this relation to Ent (a) :5 Ent (a v b), which allows two possibilities: Ent (a) < Ent (a v b) or Ent (a) = Ent (a v b) . For this algorithm, it is sufficient to use only 5 distinct entrenchment values, denoted E~o E2, £ 3,£4 and £ 5 , where £ 1 < E2 < £3 < £4 < Es. We denote the entrenchment of a proposition p, when the AGM system represents the A TMS in environment E, by EntE(p). Then by (EE4), Ent (p) = E 1 iff p fi K, for consistent K. By (EE5), Ent (p) = E 5 only if p is a tautology. Since ATMS justifications cannot be altered once they are provided by the problem solver, they are entrenched at the next highest level of entrenchment, £ 4 · The atoms in the current environment have entrenchment E 2 , and all disjunctions of an assumption and any other atom are initially given the entrenchment E 3 .

4.2 Definitions

Let the set of all atoms be denoted r.

From the functional specification of the ATMS, 1t IS possible to work backwards to a definition of the label of a node. Each environment in the label of a node p is a support set for p, so the label is a set of support sets, which we may define as follows:

A e Label (p) if and only if

1. A!:;;; E*
2. A 1:.-nts P
3. ('VA' c A)[A' ~n~s p]
4. (-,3CeN)[C!:;;;A]

The first condition requires that the label contain assumptions only, that is, the foundational beliefs of the node. The second condition ensures soundness, the third minimality, and the fourth consistency. Completeness is achieved when the label contains all sets fulfilling the four conditions.

The above definition uses the A TMS provability relation to extract the internal data structure from the ATMS. However, an explicit definition is necessary to implement the following algorithm. The label update algorithm is performed as follows:

AGM logic is based on the coherence theory of justification, it is possible to use epistemic entrenchment to achieve foundational behaviour. We describe an algorithm for translating the justificational information stored by the A TMS into an entrenchment ordering on the beliefs in the AGM model. This algorithm uses the AGM expansion and contraction operations to perform A TMS context switches. We prove that this algorithm creates a system which is behaviourally equivalent to the ATMS, relative to the specification of the A TMS given in section 2.1.

One motivation for developing this algorithm was to show that by using epistemic entrenchment it is possible for the AGM logic to exhibit foundational behaviour, without the limitations of the ATMS. In the ATMS, the problem solver and the truth maintenance systems are separate, so that the justifications are not part of the logic. Attempts have been made to formalise the logic of the A TMS [Reiter and de Kleer, 1987; Selman and Levesque, 1990]. We do not attempt to formalise the logic of the ATMS in this paper, but we have formalised the functional behaviour of the A TMS in order to prove the correctness of the simulation algorithm. There is no corresponding problem with formalising the AGM logic, since the justifications are part of the logic, so it is possible to reason about the system directly. Also, the ATMS's separation of justifications from the data means that the justifications cannot be altered without restarting the system, whereas the AGM logic allows the justifications to be varied dynamically.

By establishing a constructive connection between the AGM logic and the ATMS, we can use existing relationships between the ATMS and other logics to calculate the epistemic entrenchment relations which correspond to these logics. To date there have been very few constructive definitions of entrenchment relations which achieve the same behaviour as other systems.

In section 2, we describe the ATMS and give a formal specification of its behaviour. The AGM logic is outlined in section 3, followed by the algorithm for simulating the A TMS in the AGM logic in section 4, with the proof of the correctness of the algorithm in section 5. Section 6 summarises the paper, and outlines areas of future research.

2 TheATMS

The A TMS is an implementation of the foundational approach to modelling states of belief. Each belief must be justified by some set of beliefs, and any proposition that does not have such a justification is not accepted as a belief. The exception to this rule is the set of foundational beliefs, which require no justification at all. In the ATMS, these beliefs are called assumptions. For a justification to be valid, the beliefs which justify any proposition must be justified themselves, so that chains of justifications are formed.

The foundational theory places two restrictions on these chains: firstly they must be acyclic, so that no proposition can form part of its own justification, and secondly the chains must be finite, regressing to the beliefs which require no further justification. The A TMS removes the restriction that justifications be acyclic, since the "ATMS mechanism will never mistakenly use it as a basis for support" [de Kleer, 1986, p.155]. Naturally, the ATMS has no way of representing infinite chains of justifications. We place one additional restriction on the ATMS: we do not allow the assumptions to be justified, in keeping with the concept of foundational beliefs. [de Kleer, 1986, p.147] provides a technique which "avoids ever having to justify assumptions", so this restriction does not reduce the power of the A TMS at all.

In the A TMS, each proposition is represented by a node, and is treated as atomic. Any logical relationship between nodes must be provided by the problem solver, in the form of justifications which are passed to the TMS. The justifications represent propositional Horn clauses, with the normal provability relationships, except that inconsistency is avoided by the use of nogoods, which have a separate data structure. Nogoods are sets of assumptions which cannot be held simultaneously, and they are used to reduce the size of the search space, improving the efficiency of the A TMS.

The current set of assumptions is called the environment, and the set of facts derivable from this environment is called the context. An atomic proposition p is held to be true in an environment E if and only if it is a member of the current context. In this work, ATMS provability is denoted E 1-xTMs p.

For a node representing a proposition to be held true in a particular context, it must have a well-founded supporting justification, that is, a chain of justifications starting from a set of assumptions, where each of these assumptions is part of the current environment. The only other conditions under which a node is considered true are when it is an assumption, and therefore requires no justification, and when the current environment is inconsistent, in which case all nodes are accepted as true.

The implementation of the A TMS achieves a high level of efficiency by creating a static data structure in place of a theorem prover to calculate revisions of belief sets. The justifications and nogoods are "pre-compiled" into this data structure initially, and after this they are not consulted again. For each proposition p, the ATMS creates a node representing it, and associates a label with it, which stores the justificational information. The label represents the set of environments in which the proposition p is true. The label must be consistent, sound, complete and minimal. A label is consistent when each of its members is a consistent environment. That is, a label must not contain an environment which is a superset of any nogood set. The label for p is sound when p is derivable from each environment of the label. If every environment from which p can be derived is a superset of some environment of its label, then the label is complete. A label is minimal if no environment of the label is a superset of any other.

2.1 A TMS Functional Specification

Let E · represent the set of all assumptions. As described above, no member of E · may appear as the consequent of any justification. Let a and c represent atoms, and A a set of atoms. The input to the A TMS consists of a set of justifications, 1= {(A,c) I(/\ x) ~c}, a set of nogood xeA environments, N ={A r;;, E* I -, 1\ x}, and the current environment, E ={a E E* I a}. xeA

E 1-xrMs p if and only if

Update_Label (p)

For each justification (B,p) e J

If the label of any member of B is empty

Continue with next justification

For all choices of one environment from each member of B

Let L be the union of these environments

If L subsumes any nogood environment

Continue with next choice

Else if L is subsumed by any environment in Label (p)

Continue with next choice

Else if L subsumes any environments in Label (p)

Remove those environments from Label (p)

Add L to Label (p)

If Label (p) has changed

For each justification (B,q) e J such that p e B

Update_Label (q)

End { Update_Label}

The foundational beliefs of an atom p in the environment E, denoted FB (p,E), is the set of support sets of p which are held to be true in E. If no such set exists, then the atom has no well-founded justification. Formally:

The essential support set, ES (p,E), is defined:

From the functional specification of the A TMS, an atom is considered true if and only if it is an assumption, or the environment is inconsistent, or it has a well-founded justification. In terms of the above definitions:

Using these definitions, we now describe the algorithm which calculates the entrenchments for the AGM logic to simulate the ATMS behaviour.

4.3 Algorithm A TMS_to_AGM

This algorithm calculates the epistemic entrenchments necessary to simulate A TMS environment change in the AGM logic via the AGM belief change operators described in section 3. The belief set K contains all of the current beliefs, and corresponds to the ATMS context. Obviously, since K is logically closed, it is a much larger set than the corresponding A TMS context, but we show that for all p E 'I., E lxTMs p H p E K.

The algorithm encodes the current support relationships in the entrenchment relation. That is, if p is an essential support for q, then the removal of p must force the removal of q, and this, according to the definition of contraction, requires that the entrenchment relation contain Ent (p) = Ent (pvq) . Since Ent (p) = E 2 , this is achieved by setting Ent(pvq) = E2 · Alternatively, if q is not dependent on p, then we have Ent (p) < Ent (pvq), by setting Ent(pvq) = E3.

For each environment change, the translation algorithm computes the corresponding changes in the entrenchment relation from the changes in the essential support sets. For each new assumption A in the essential support of the proposition B, the entrenchment of A v B is set to E2 , so that Ent(A) = Ent(A vB). Conversely, for any A which was a member of the essential support set of B but is no longer in the essential support set, we let Ent(A vB) = £ 3 , so that Ent(A) < Ent(AvB).

Initially, K contains the justifications and nogoods in their logical (Hom clause) form. That is, for each (A,p) e J, ( ( A x) ~ p) e K, and for each C e N, ( -, A x) e K. nA nC Also, for each of these formulas f, Ent (j) = E 4 . The initial

value of Old_Environment is 0.

Algorithm A TMS_to_AGM

For each New_Environment "i/ x e ( Old_Environment -New _Environment) { Remove all assumptions which are no longer true } K := K; { AGM contraction } { Note that AGM logic implies that Ent (x) := E 1 "i/ c such that x e u X X e FB (c,Old_Environment) "i/ y e (ES(c,New_Environment) - ES (c,Old_Environment)) { Entrench new essential supports } Ent (yvc) := E 2 (i.e. Ent (y) = Ent (yvc)) "i/ y e (ES(c,Old_Environment) - ES(c,New_Environment)) { Change entrenchments of old essential supports } Ent (yvc) := E 3 (i.e. Ent (y) < Ent (yvc)) "i/ x e (New_Environment- Old_Environment) { Add all assumptions which have become true } K := K; { AGM expansion } Ent(x) := E 2 "i/ y e 'I., Ent (xvy) := E 3 { Default entrenchment } "i/ c such that x e u X X e Lilbe/(c) "i/ y e (ES(c,New_Environment) - ES (c,Old_Environment)) { Entrench new essential supports } Ent(yvc) := E2 (i.e. Ent(y) = Ent(yvc)) "i/ y e (ES(c,Old_Environment) - ES(c,New_Environment)) { Change entrenchments of old essential supports } Ent(yvc) := E 3 (i.e. Ent(y) < Ent(yvc)) Old_Environment := New_Environment End { A TMS_to_AGM }

Note that the default entrenchment, Ent (x) < Ent (xvy) , for atomic x and y, encodes the fact that x and y are unrelated, since if x is removed from K, y is unaffected. It is the job of the problem solver, not the TMS, to point out any relationships between the various atoms, or if it is considered expedient, to refrain from doing so.

The amount of work performed by the algorithm suggests that simulating the A TMS in AGM logic is not trivial. The reason for this is that foundational reasoning is independent of history - for example the A TMS context depends only on the current environment, and is not affected by any previous environment, whereas the AGM logic relies on a principle of minimal change when moving from one theory to the next. Unfortunately, this minimal change principle cannot also apply to the entrenchment relation, thus extensive revisions of the entrenchment relation are often necessary to keep the system "effectively independent" of its previous state.

4.4 Example

Consider a simple system with just two rules :

A ~D. B A C ~D

Now suppose we want to change environment from Old_Environment = {A,B} to New_Environment = {B,C}. The entrenchment relation in Old_Environment will contain:

Et:C

E2:A, B, D, AvD

E 3 :AvB, BvD

The essential support forD in Old_Environment is {A}, and in New_Environment it is {8, C} . Applying the algorithm above, we first remove A from the environment. Since A features in one of the foundational beliefs of D, the essential supports of D are recalculated, giving Ent (A v D) = E 3 and Ent(BvD) = Ent(CvD) = £ 2 . In the next step, Cis added to the environment with entrenchment £ 2 , and the formulae CvA, CvB, and CvD are entrenched at level £ 3 . Finally, since C appears in the label of D, the essential supports of D are calculated again, giving a relation containing:

E 1: A

£ 2 : B, C, D, BvD, CvD

E 3 :AvB, AvC, AvD, BvC

5 Theorem and Proof of Correctness

The ATMS and AGM systems are equivalent if and only if: Theorem 1: ("tp E L) [ E l:tl'Ms p H p E K]

We will prove this theorem by induction on the number of expansion and contraction operations. Firstly, it is necessary to prove two important lemmas which establish the relationship between entrenchment and the notion of essential support, and that between essential support and ATMS provability.

5.1 Lemma 1

For all ae E, and for all beL,

EntE(a) = EntE(a v b) H a E ES(b,E)

5.2 Lemma2

If E is a consistent environment and a -:t b then

aeES(b,E) H (EI:tl'Ms b)A((E-{a})~l'Ms b)

Lemmas 1 and 2 are proved in [Dixon and Foo, 1992a].

5.3 Proof of Theorem 1

Initial case

Before any operations are performed, E = 0. In this case, E l:tl'Ms a H 3 (B,a) E J such that (\;/bE B) [E l:tl'Ms b]. Since no assumptions are true, the chains of justifications must end in formulae of the form (0,x) , which are called premises.

Part (1): Suppose E l:tl'Ms a. We show by induction on the length (n) of the longest chain of justifications that a E K.

When n = 1, we have (0,a) E J, which in Hom clause form is the formula a, and hence a E K.

Inductive hypothesis: assume that if E l:tl'Ms a then a E K for all n ~ k.

Consider a proof of a with maximum length k+1 justifications. Then 3 (B,a) E J such that "t b E B, E l:tl'Ms b in at most k steps. Then by the inductive hypothesis, each b is in K. Since K is logically closed, we also have

( 1\ x) E K. Combining this with ( 1\ x) ~ a, which is HB HB also in K, since (B,a) E J, we can conclude by modus ponensthata E K.

We conclude by induction that for all n, a E K.

Part (2): Conversely, suppose a E K. Then there exists a sequence of resolutions of clauses in K from J u N such that the final step produces the clause a. We know that no clauses from N are used in the resolution, because when one of the resolving clauses has no positive literals, the resulting clause will have no positive literals. Therefore no such clause can be involved in a sequence of resolutions which produces a positive literal. We now show by induction on the number (n) of resolution steps that E l:tl'Ms a.

Initial case: when n=O, then (0,a) E J. Hence E l:tl'Ms a. Inductive step: assume for all n ~ k that E 1:.ms a.

Consider a sequence of k + 1 resolution steps ending with the clause a. Then there exists in this sequence a clause containing the positive literal a, corresponding to some justification (B,a) E J. Let this clause be -.bt v ··· v-,bmva. (i.e. B={b1, ··· , bm}). Then for 1 ~ i ~ m, b; E K, and the resolution proof for each b; takes ~ k steps, so by the inductive hypothesis E l:tms b;. But ({bt, . .. ,bm},a) E J, so by the definition of the ATMS, E l:tl'Ms a.

By induction, we have shown that for all n, if a e K then E l:tl'Ms a. This completes the initial case of the proof of the theorem.

Inductive step

Assume that after m expansions and contractions that p E K H E l:tl'Ms p, for all p E L. Consider the (m + l)st operation.

Case (1): Expansion by a

LetE'=E u {a} .

Suppose E' l:tl'Ms b. Then one of the following 4 cases must hold:

(a) E l:tl'Ms b

(b) E ~l'Ms band 3 C E N such that C!:: E'

(c) E ~l'Ms band a = b

(d) E ~l'Ms b and 3 (A,b) E J such that "t X E A, E' l:tms X

Case (a): By the inductive hypothesis, b E K. Using AGM axiom (K+3), K s;;; K;, we have b E K:.

Case (b): E!:: K, from the inductive hypothesis, since "t x E E, E l:tl'Ms x. Also a E K;, by AGM axiom (K+ 1) . Since K !:: K: (AGM axiom (K+3)) and C ~ E', we have C s;;; K;. But since

C E N, (-, 1\ x) e K s;;; K;, and by logical closure xeC K: = K1. . Thus bE K";.

Case (c): By AGM axiom (K+ 1) , b E Kb.

Case (d): We show that be K; by induction on the number (n) of justifications used in proving E' l:tl'Ms b.

Initial case: when n = 0, by Cases (a)-( c), we have bE K:.

Inductive step: assume that for all n ~ k we have b E K: . Consider a proof using k + 1 justifications, including a justification for b, (A,b) E J. Then for all x E A, E' l:tl'Ms x. Now if Case (a), (b) or (c) applies, we have shown x E K; . Alternatively, if Case (d) applies, the proof of x contains ~ k justifications, and hence by the inductive hypothesis x e K;. Also, since (A,b) e J, [(/\ x) ~b]e K,;;;,K;, so by closure we .teA have be K;.

Hence, by induction b e K; for all n.

Conversely, assume that be K;. That is, b e Conseq (K v {a}) .

We show by induction on the number (n) of resolutions involved in proving b from K v {a} that E' l:r7Jis b.

Initial case: when n = 0, either b e K or b = a. If b e K, then by the inductive hypothesis of the main proof, E l:r7Jis b, and hence since E ~ E', we have E' l:r7Jis b. Otherwise, if b =a, then b e E' and thus E' l:r7Jis b.

Inductive step: assume for all n :s; k that E' l:r7Jis b. Now consider a resolution proof of b requiring k + 1 steps. This procedure uses a formula from J of the form -,rl v · · · v -,rm v b, where r; e K!, 1 :5; i :5; m. For this to resolve to b, there are resolution proofs for all r;, 1 :5; i :5; m, with each of these procedures requiring :5; k steps. Hence by the inductive hypothesis E' l:r7Jis r;, 1 :5; i :5; m. Also ( { r I> ... , r m}, b) e J, so by the definition of the A TMS, E' l:r7Jis b.

Hence for all n, E' l:r7Jis b, and thus we have shown that E' J:r7Jts b H b e K;.

Case (2): Contraction by a

Let E' = E - {a}.

Suppose E' l:r7Jis b. Then E l:r7Jis b, since E',;;;, E, and hence by the inductive hypothesis, be K. Then by Lemma 2, a fi ES (b,E). From (EE2) we have EntE(a) :5; EntE(a v b), and using Lemma 1, this result strengthens to EntE(a) < EntE(a v b). Finally, from the definition of contraction, we have b e K~.

Conversely, suppose that b e ~. Then by the definition of contraction, EntE(a) < EntE(a v b), and by Lemma 1, a fi ES(b,E). We also know that be K, since ~ ,;;;, K. So E l:r7Jis b, by the inductive hypothesis, and then by Lemma 2 we conclude that E' l:r7Jis b.

Thus we have shown that Vbe r., E' l:r7Jis b H b e ~, after the (m + l)st operation.

Therefore, we have shown by induction that, p e K H E l:r7Jis p, Vpe r., and the algorithm correctly chooses an entrenchment so that the behaviour of the AGM system is equivalent to that of the ATMS.

6 Conclusions and Further Research

We have shown that the A TMS can be simulated in the AGM logic by using a suitable epistemic entrenchment relation to encode the foundational justifications of the beliefs, and using contraction and expansion operations to perform context changes. The A TMS encoding does not specify a complete entrenchment relation, but calculates the class of entrenchments for which the AGM's behaviour with respect to atoms is equivalent to the ATMS. Thus the coherence-based AGM logic is able to mimic the behaviour of a foundational system, the ATMS. This illustrates an advantage of the AGM logic with entrenchment over the many purely foundational systems: it is possibl~ to express all types of justificational information using epistemic entrenchment. Current research involves using epistemic entrenchment to model non-foundational justifications [Dixon and Foo, 1992b], such as a coherence-based truth maintenance system. Another advantage is that the AGM logic is a formal system, so it is possible to reason directly about the system, which is not true of the A TMS.

Other extensions of this work are rule revision, which is not allowed by the A TMS, but could be easily implemented in the AGM logic by decreasing the entrenchment of the justifications. One application of rule revision would be to model default rules and exceptions, by creating a stratified rule base, with various sets of rules being placed at different levels of entrenchment. Current research also includes extending the implementation in [Dixon, 1993] to a belief revision system which satisfies all of the AGM postulates.