Inverse Resolution as Belief Change

1 Background

We consider an underlying classical propositional logic with a propositional language L, over a set of atoms, or propositional letters, P = {a, b, c, . . .}, and truth-functional connectives ¬, ∧, ∨, →, and ↔. L also includes the truth-functional constants ⊤ and ⊥. The closure operator Cn denotes classical propositional consequence. We use the term belief set to refer to a set of formulas closed under Cn (i.e., K = Cn(K)). K represents the set of all belief sets. The distinguished element K⊥ ∈ K denotes the inconsistent belief set.

We shall also adopt the following linguistic conventions to simplify the presentation. Lower case Greek characters φ, ψ, χ, . . . will represent arbitrary logical formulas. Lower case Roman characters k, l, . . . will denote propositional literals. Upper case Roman characters A, B, C, . . . denote propositional Horn clauses (disjunctions of literals containing at most one positive literal).

1.1 Belief Change

The mostly widely accepted approach to belief change is the one proposed by Alchourr ´on, G¨ardenfors and Makinson [Alchourr´on et al., 1985; G¨ardenfors, 1988; Hansson, 1999]. This approach is motivated by the concern to characterise rational belief change operators. That is, operations of belief change that are guided by principles of rationality. The AGM approach introduces three belief change operations: expansion (+), contraction (-), and revision (∗). Expansion deals with the addition of new information without retraction of existing beliefs; contraction takes care of the removal of belief; and, revision deals with the addition of beliefs with the possibility of retracting current beliefs in order to maintain consistency. Each of these operations takes a belief set representing the reasoner's original belief corpus and a sentence representing the new information, returning the modified belief corpus: (+,-, ∗ : K × L → K). The belief change operations are characterised by rationality postulates and various constructions. The interested reader is referred to [G¨ardenfors, 1988; Hansson, 1999] for further details.

In this paper we are concerned with the process of belief expansion as this is the typical setting under which inverse resolution is applied. This should not be seen as a significant restriction because belief revision proper can be obtained by combining contraction and expansion. However, AGM expansion is very limited in scope. It can be shown that AGM expansion corresponds to closure under logical deduction: K+φ = Cn(K∪{φ}). What we require is a form of belief change that elaborates upon the newly acquired information. Such an operation has been introduced by Pagnucco [Pagnucco, 1996] in the form of an operation called abductive expansion (⊕ : K×L → K). This operation looks to amplify the newly acquired information by trying to find an explanation for it (via abduction) and is reminiscent of the way that inverse entailment is defined [Muggleton, 1992]. Formally, abductive expansion may be defined as follows:

Definition 1.1 K ⊕ φ is an abductive expansion of K with respect to φ iff

That is, when confronted with new information φ the reasoner seeks an hypothesis ψ that explains φ with respect to its current beliefs and incorporates this explanation into its corpus.

It can be shown that the operation of abductive expansion satisfies the following rationality postulates:

• (K⊕1) For any sentence φ and any belief set K, K ⊕ φ is a belief set
• (K⊕2) If ¬φ ̸∈ K, then φ ∈ K ⊕φ
• (K⊕3) K ⊆ K ⊕ φ
• (K⊕4) If ¬φ ∈ K, then K ⊕φ =K
• (K⊕5) If ¬φ ̸∈ K, then ¬φ ̸∈ K ⊕φ
• (K⊕6) If K ⊢ φ ↔ψ, thenK ⊕φ =K ⊕ψ
• (K⊕7) K ⊕ φ ⊆ Cn(K ⊕ (φ ∨ ψ) ∪ {φ})
• (K⊕8) If ¬φ ̸∈ K ⊕ (φ ∨ψ), then K ⊕ (φ ∨ψ) ⊆K ⊕φ

Postulate (K⊕1) maintains the expanded belief corpus as a belief set. (K⊕2) states that the new information should be included in the expanded belief state provided that it is consistent with the original corpus while (K⊕3) requires that the expanded corpus be at least as large as the original. When the new information is inconsistent with the corpus, (K⊕4) prevents change. Postulate (K⊕5) ensures that the corpus does not expand into inconsistency. (K⊕6) states that the expansion process is syntax insensitive. These postulates suffice to characterise abductive expansion as defined above. Often postulates (K⊕7) and (K⊕8) are added and restrict the mechanism that selects hypotheses to one that satisfies transitivity.

An elegant way of constructing an abductive expansion operation is by providing an ordering of epistemic entrenchment over the sentences in the language that indicates their plausibility or importance. For AGM operations, entrenchment orders the beliefs while the non-beliefs are relegated together as the least important sentences. For abductive expansion however, we need to be able to discriminate between potential hypotheses and so the traditional epistemic entrenchment ordering is modified so that beliefs are lumped together as the most important while the non-beliefs are ordered by importance in what we term an abductive entrenchment ordering.

Definition 1.2 An ordering ≤ over L is an abductive entrenchment ordering iff it satisfies (SEE1)-(SEE3) and condition (AE4):

• (SEE1) For any φ, ψ, χ ∈ L, if φ ≤ ψ and ψ ≤ χ then φ ≤ χ
• (SEE2) For any φ, ψ ∈ L, if {φ} ⊢ ψ then φ ≤ ψ
• (SEE3) For any φ, ψ ∈ L, φ ≤ φ ∧ψ or ψ ≤ φ ∧ψ
• (AE4) WhenK ̸=K⊥, φ ∈ K iff ψ ≤ φ for all ψ ∈ L

This ordering is a total preorder (SEE1)-(SEE3) in which the beliefs are maximally entrenched (AE4); it effectively ranks the reasoner's non-beliefs.

The following properties of abductive epistemic entrenchment will be useful in proving the results in this paper.

Lemma 1.1 Suppose ≤ satisfies (SEE1)-(SEE3), then 1

1. For all φ ∈ L either φ ≤ ψ or ¬φ ≤ ψ for all ψ ∈ L.
2. For all φ ∈ L, {ψ : φ ≤ ψ} = Cn({ψ : φ ≤ ψ})
3. φ ∧ψ =min(φ, ψ)
4. φ ∨ψ ≥max(φ, ψ)

1 Note that φ < ψ iff φ ≤ ψ and ψ ̸≤ ψ and φ = ψ iff φ ≤ ψ and ψ ≤ ψ.

The first property states that for every sentence φ, either φ or ¬φ (possibly both) is minimally entrenched. The second property notes that taking all sentences more entrenched than a certain rank gives a deductively closed set of sentences. The third property indicates that a conjunction is entrenched at the same level as the minimum of the conjuncts while the fourth property states that a disjunction is at least as entrenched as the maximally entrenched disjunct. These are well known properties of orderings satisfying conditions (SEE1)-(SEE3) which are termed expectation orderings by G¨ardenfors and Makinson [G¨ardenfors and Makinson, 1994].

Pagnucco [Pagnucco, 1996] gives a condition that allows us to determine an abductive expansion function ⊕≤ for a particular epistemic state K given an abductive entrenchment ordering ≤.

We omit the subscript ≤ unless necessary. This condition states that we can accept sentence ψ in the abductively expanded belief state whenever it is believed in the original corpus or when ψ is more plausible given φ than ¬ψ given φ.

1.2 Inverse Resolution

Resolution is a valid inference procedure which deduces a clause C from two clauses C1 and C2. Given a clause C1 containing a literal l and a clause C2 containing the literal ¬l, the resolvent of C1 and C2, denoted C = C1.C2, is

This process may be visualised in the following diagram [Muggleton and Buntine, 1988]: 2

C

Inverse resolution (and more recently, inverse entailment), on the other hand, is a machine learning technique based upon the following characterisation of inductive inference [Muggleton, 1987; 1989]. Given a partial domain theory Γ and a positive example E that is not a consequence of the domain theory (Γ ̸⊢ E) we attempt to determine a new domain theory Γ′ , using Γ and E, that will account for the example (Γ′ ⊢ E) and the original domain theory (Γ′ ⊢ Γ). If we think of Γ′ as Γ∪I where I represents the result of inverse resolution, then the relationship with abduction should become much clearer. In practice, the domain theory and example are usually represented as Horn clauses. This technique is based on inverting the resolution process and consists of five operators: two Voperators, two W-operators and the truncation operator.

So as not to countenance invalid inference, the notion of an oracle is adopted. An oracle is an entity that accepts a clause, constructed using one of the inverse resolution operators, if it is valid in the intended model. In our framework abductive entrenchment is used to discriminate between potential hypotheses and takes the place of the oracle.

2 The plus (+) (respectively minus (-)) sign in the diagram denotes that the literal resolved upon appears positive (respectively negative) in that clause.

V-Operators

Previously, a single resolution step was presented in terms of a "V"-shaped diagram. The two V-operators can derive one of the clauses at the top of the V given the other clause at the top of the V and the clause at the bottom of the V. The absorption operator derives C2 given C1 and C while the identification operator derives C1 given C2 and C.

Since the new clause is constructed by finding the inverse of a resolved product, the notion of a resolved quotient 3 of C and C1 is defined [Muggleton and Buntine, 1988] as C2 = C/C1. Rearranging equation (1) for resolution can obtain C2 = (C \ (C1 \{l}))∪{¬l} under the following assumption [Muggleton and Buntine, 1988]:

• Separability Assumption - Clauses C1 \ {l} and C2 \ {¬l} contain no common literals.

This assumption also simplifies the calculation of resolved quotients (i.e., absorptions or identifications).

W-Operators

Joining two resolution "V"s we obtain a form analogous to that for the V-operators [Muggleton and Buntine, 1988]:

In this situation a common literal l, contained in A, resolves with clauses C1 and C2 to produce B1 and B2. Clauses B1 and B2 represent the new information and clauses A, C1 and C2 the constructed clauses. Interestingly, since l is resolved away, the constructed clauses A, C1 and C2 will contain a literal whose propositional symbol does not appear in either B1 or B2. If l occurs negative in A then the operator is referred to as intra-construction and if it occurs positive in A the operator is called inter-construction.

Truncation

The truncation operator results from the special case where the empty clause occurs at the base of a V or W schemata. In a propositional system, this corresponds to dropping negative literals from a clause. In the first-order case Muggleton and Buntine [Muggleton and Buntine, 1988] show that two literals may be truncated by taking their least-generalgeneralisation. Rouveriol and Puget [Rouveirol and Puget, 1990] generalise this to a truncation operator which replaces terms by variables and drops literals from clauses.

In the case of a propositional language, a number of schema may be used to compute the required inverse resolution. These are displayed in Table 1 (see [Muggleton, 1987; 1989]). 4 In each instance, the top line represents the initial clauses and the bottom line represents the constructed clause(s). We shall use these directly in our approach to characterise the inverse resolution operators as belief change operators (abductive belief expansion operators in fact).

3 Absorption is considered here. Identification is similar.

4 We adopt a slight renaming of the terms to those presented in [Muggleton, 1989], having found them more amenable to study. In the case of absorption and identification, the first clause on the top

2 Approach

Our aim here is to render the individual inverse resolution operations as belief change operators. In particular, we shall give conditions on the abductive epistemic entrenchment that will guarantee that the results of an inverse resolution operation are included in the revised (or, more precisely, abductively expanded) belief corpus.

To make this more precise, we take the reasoner's belief corpus K and an example φ as the newly acquired information. We want to construct abductive expansion operations ⊕ for each of the five inverse resolution operations such that K⊕φ represents the result of applying that particular inverse resolution operation on the given example and elements of the current belief corpus. This construction is achieved by specifying a condition(s) on abductive entrenchment that, when added to conditions (SEE1)-(SEE3) and (AE4), guarantees the result of the inverse resolution operation.

As noted above, abductive entrenchment encodes the 'choices' that are made by the oracle. In other words, entrenchment will be used to determine which potential hypotheses are accepted and which are rejected. Furthermore, it may be the case that in expanding the reasoner's belief corpus in this way, more than one potential hypothesis is accepted for a given example φ. This could be easily restricted to one hypothesis by imposing additional restrictions on the entrenchment ordering however, intuitively, this seems procrustean. Multiple generalisations allow for a more flexible characterisation of the inverse resolution process. Finally note that we will only be concerned with examples (new information) that are presented as Horn clauses in keeping with the way in which inverse resolution is traditionally realised.

2.1 Absorption

The typical case for Absorption occurs when A → k is believed and A ∧ B → j is presented as an example (newly acquired information). The Absorption operator looks for a sentence B ∧ k → j to add to the current theory in this case. By (C⊕), the condition we need to guarantee is therefore:

line of the schemata is taken from the domain theory while the second represents the new data.

5 Here A, B, C represent conjunctions of atoms while j, k, l represent atoms.

What we require here is a restriction on abductive entrenchment that, given A → k ∈ K, guarantees this condition. Consider the following restriction:

It states that the sentence B ∧ k → j is not minimally entrenched (by Lemma 1.1(1), ⊥ is minimally entrenched). In other words, when an example A ∧ B → j is presented, any hypothesis of the form B ∧ k → j that is not minimally entrenched and where A → k is believed, will be accepted. Now, by Lemma 1.1, condition (Abs) is equivalent to ¬(B ∧ k → j) < B ∧ k → j which says that this hypothesis is preferred to its negation. The following theorem indicates the appropriateness of this condition.

Theorem 2.1 Given a belief set K ̸= K⊥, a sentence A → k ∈ K and an abductive epistemic entrenchment relation ≤ satisfying (Abs), the abductive expansion operator ⊕≤ obtained from ≤ via condition (C⊕) gives the same result as Absorption (i.e., B ∧ k → j ∈ K ⊕ (A ∧ B → j)).

Proof: Now (A → k) ∧ (B ∧ k → j) ⊢ A ∧ B → j so (A → k) ∧ (B ∧ k → j) ≤ A ∧ B → j by (SEE2). But B ∧ k → j ≤ A → k by (AE4). It follows by Lemma 1.1(3) that B ∧ k → j = A ∧ B → j. Furthermore (B ∧ k → j)∧(A∧B → j) = B∧k → j. But by (Abs) ⊥ < (B∧k → j) ∧ (A ∧ B → j). Therefore ¬((B ∧ k → j) ∧ (A ∧ B → j)) = ⊥ by Lemma 1.1(1) and so ¬((B∧k → j)∧(A∧B → j)) < B ∧ k → j. It follows by Lemma 1.1(4) ¬((B ∧ k → j) ∧ (A∧B → j)) < ¬(A∧B → j) ∨ (B ∧K → j). Hence by logical equivalence (A ∧ B → j) → ¬(B ∧ k → j) < (A ∧ B → j) → (B ∧ k → j) as required. ✷

Now it may seem strange that condition (Abs) does not mention the new example A ∧ B → j. By Lemma 1.1(2) it can be shown that whenever A → k ∈ K, it is always the case that B∧k → j ≤ A∧B → j. That is, the new example cannot be less entrenched than any potential hypothesis.

However, we might re-consider the typical Absorption case and look at what happens when we assume that A∧B → j ∈ K and A → k is the new example. In this case we require condition (Abs) together with the following condition:

The following result indicates this formally:

Theorem 2.2 Given a belief set K ̸= K⊥, a sentence A ∧ B → j ∈ K and an abductive epistemic entrenchment relation ≤ satisfying (Abs) and (Abs′ ), the abductive expansion operator ⊕≤ obtained from ≤ via condition (C⊕) gives the same result as Absorption (i.e., B ∧ k → j ∈ K ⊕ (A → k)).

2.2 Identification

The typical case for Identification occurs when B ∧ k → j is believed and A ∧ B → j is presented as the new example. Identification returns A → k to be added to the belief corpus. The condition that we need to guarantee is, by (C⊕):

Analogously to Absorption we require the following restriction on entrenchment to guarantee this condition.

It states that any potential hypothesis A → k is not minimally entrenched and by Lemma 1.1 is equivalent to saying that any potential hypothesis be preferred to its negation. This result is stated formally in the following theorem:

Theorem 2.3 Given a belief set K ̸= K⊥, a sentence B ∧ k → j ∈ K and an abductive epistemic entrenchment relation ≤ satisfying (Ident), the abductive expansion operator ⊕≤ obtained from ≤ via condition (C⊕) gives the same result as Identification (i.e., A → k ∈ K ⊕ (A ∧ B → j)).

The proof follows a similar idea to that for Absorption and so, due to lack of space, we omit it here.

Again, if we re-consider Identification and suppose that A∧B → j ∈ K while B ∧ k → j is the new example, then we also require the following condition on entrenchment:

2.3 Inter-Construction

In the case of Inter-Construction there is only ever one case to consider because, without loss of generality, we may assume that sentence A ∧ B → j is believed and A ∧ C → k is presented as the new example. In this case three new clauses are derived (B ∧ l → j, C ∧ l → k, and A → l) and we need to guarantee three conditions which are, by (C⊕):

This condition can be read in a number of ways. Literally it says, in analogy to (Abs) and (Ident), that the conjunction of the potential hypotheses is not minimally entrenched. However, by Lemma 1.1(3), this also means that each of the individual hypotheses themselves is not minimally entrenched and so by Lemma 1.1(1) that they are each preferred to their negations. We now obtain the following result.

Theorem 2.4 Given a belief set K ̸= K⊥, a sentence A ∧ B → j ∈ K and an abductive epistemic entrenchment relation ≤ satisfying (Inter), the abductive expansion operator ⊕≤ obtained from ≤ via condition (C⊕) gives the same result as Inter-construction (i.e., B∧l → j, C∧l → k, A → l ∈ K ⊕ (A ∧ C → k)).

In inverse resolution, the literal l in the sentences above is newly introduced. It represents a concept that was not present in the original theory. The terms 'predicate invention' or 'constructive induction' are often used to describe what the W-operators are achieving by introducing a new element into the object language. Current theories of belief change do not allow for the expansion of the object language so we assume that the language is suitably equipped with a supply of propositions that can be used to create literals like l here. Of course, l will be present in any belief set; tautologies like l → l are present in every belief set. However, we can require additional conditions like l ̸∈ K if we want to ensure that l is newly generated. This is not an ideal solution as one is difficult to derive using belief sets but should go some way to achieving the desired results.

2.4 Intra-Construction

In Intra-construction, again without loss of generality, we may assume that A ∧ B → j ∈ K and A ∧ C → j is the new example. In this case, by (C⊕), we need to guarantee the following three conditions:

Again, the desired result is achieved by ensuring that none of the potential hypotheses is minimally entrenched.

The following theorem shows that this condition is correct.

Theorem 2.5 Given a belief set K ̸= K⊥, a sentence A ∧ B → j ∈ K and an abductive epistemic entrenchment relation ≤ satisfying (Intra), the abductive expansion operator ⊕≤ obtained from ≤ via condition (C⊕) gives the same result as Intra-construction (i.e., A ∧ l → j, B → l, C → l ∈ K ⊕ (A ∧ C → j)).

2.5 Truncation

For truncation, there are no requirements on the original belief corpus and all we assume is that A ∧B → j is the new information. Truncation generalises this by adding A → j to the belief corpus. The condition we need guarantee is:

This can be achieved by the following condition stating that A → j is not minimally entrenched.

The following theorem indicates that this is correct.

Theorem 2.6 Given a belief set K ̸= K⊥ and an abductive epistemic entrenchment relation ≤ satisfying (Trunc), the abductive expansion operator ⊕≤ obtained from ≤ via condition (C⊕) gives the same result as Truncation (i.e., A → j ∈ K ⊕ (A ∧ B → j)).

3 Discussion

The idea of using a form of belief expansion capable of introducing new hypotheses has also been suggested by Levi [Levi, 1991] who introduces an operation known as deliberate expansion. While his method of determining and selecting hypotheses differs from ours, the notion that belief expansion should allow for the addition of sentences that do not necessarily follow from the new information and the belief corpus is the same. The level to which the reasoner wishes to accept such hypotheses will be determined by their aversion to courting erroneous beliefs and this is reflected in the abductive entrenchment ordering in our framework. Such errors, when realised later, may of course be fixed by subsequent revision. We follow Levi's commensurability thesis in maintaining that any form of belief revision can be obtained via a sequence of (abductive) expansions and contractions.

Forms of symbolic machine learning such as inverse resolution are often equated with inductive inference (or what might be termed 'enumerative induction' [Harman, 1968]). However, here we have preferred the notion of abductive inference. There has been a substantial amount of debate in the artificial intelligence community as to what constitutes induction and abduction and whether they are essentially the same form of inference. We do not address this at any great length here. Levi [Levi, 1991] adopts Peirce's later ideas on this subject where abduction is concerned with formulating potential hypotheses and induction selects the best of these. Abductive entrenchment to a large extent serves both purposes here.

One issue that is not strictly addressed by the inverse resolution operators but is important in the wider literature on symbolic machine learning is that of positive and negative examples. Clearly our framework and the inverse resolution operators deal quite well with positive examples. When it comes to negative examples this issue is not so clear. On the one hand new information like ¬φ can be dealt with quite easily. However, negative information of the form φ ̸∈ K, cannot be dealt with adequately here. It is possible to place restrictions on the entrenchment relation that will not permit φ to be believed but it is not clear how this information should be presented. On first sight it would appear that this is more an issue for iterated revision.

4 Conclusions and Future Work

In this paper we have developed an account of how the machine learning technique of inverse resolution, can be viewed as a form of belief change. In particular, we have given restrictions on epistemic entrenchment that will guarantee that the resulting belief change operations behave exactly in the manner of the inverse resolution operations. This is the first step in unifying the study of machine learning and belief change and has important repercussions for the links between machine learning and nonmonotonic reasoning.

This paper opens many avenues for future research in a number of interesting directions. Firstly, the development of belief change postulates that characterise the various inverse resolution operators. Such rationality conditions would allow another way of comparing these operations with belief revision. Perhaps more importantly, at this point it would be relatively straightforward to characterise each of the inverse resolution operators as a nonmonotonic consequence relation in the way of Kraus, Lehman and Magidor [Kraus et al., 1990] allowing comparison with another large body of research.

In this work we have been able to capture each of the inverse resolution operators as a belief change operation. Given an example, we need to state which operation to apply in order to generalise the reasoner's beliefs. A more general form of this theory would not require that the operation be stated but that a single belief change operation represent all inverse resolution operations and that it determine which are applied when new information is given. It is not clear however, how feasible such a super-selecting belief change operation is.

One important principle that guides belief change is that of minimal change; the reasoner's belief corpus should be modified minimally to accept the new information. It would be interesting to see how this notion in belief change is manifested in work on inverse resolution and symbolic machine learning and the heuristics and metrics applied there to select hypotheses for generalisation. Extending this work to the first-order case and investigating forms of iterated (abductive) belief change are also interesting and important possibilities.