Next Steps in Propositional Horn Contraction

1 Introduction

Belief change is a subarea of knowledge representation concerned with describing how an intelligent agent ought to change its beliefs about the world in the face of new and possibly conflicting information. Arguably the most influential work in this area is the so-called AGM approach [Alchourr´on et al., 1985; G¨ardenfors, 1988] which focuses on two types of belief change: belief revision, in which an agent has to keep

∗This paper is based upon work supported by the National Research Foundation under Grant number 65152.

Ivan Jos´e Varzinczak

Meraka Institute CSIR, South Africa ivan.varzinczak@meraka.org.za

its set of beliefs consistent while incorporating new information into it, and belief contraction, in which an agent has to give up some of its beliefs in order to avoid drawing unwanted conclusions.

Although belief change is relevant to a wide variety of application areas, most approaches, including AGM, assume an underlying logic which includes full propositional logic. In this paper we deviate from this trend and investigate belief contraction for propositional Horn logic. As pointed out by Delgrande [2008] who has also studied contraction for Horn logic recently, and to whom we shall frequently refer in this paper, this is an important topic for a number of reasons: (i) it sheds light on the theoretical underpinnings of belief change, and (ii) Horn logic has found extensive use in AI and database theory. However, our primary reason for focusing on this topic is because of its application to ontologies in description logics (DLs) [Baader et al., 2003]. Horn clauses correspond closely to subsumption statements in DLs (roughly speaking, statements of the form A1 ⊓. . .⊓An ⊑ B where the Ai's and B are concepts), especially in the EL family of DLs [Baader, 2003], since both Horn logic and the EL family lack full negation and disjunction. A typical scenario involves an ontology engineer teaming up with an expert to construct an ontology related to the domain of expertise of the latter with the aid of an ontology engineering tool such as SWOOP [http://code.google.com/p/swoop] or Prot´eg´e [http://protege.stanford.edu]. One of the principal methods for testing the quality of a constructed ontology is for the domain expert to inspect and verify the computed subsumption hierarchy. Correcting such errors involves the expert pointing out that certain subsumptions are missing from the subsumption hierarchy, while others currently occurring in the subsumption hierarchy ought not to be there. A concrete example of this involves the medical ontology SNOMED [Spackman et al., 1997] which classifies the concept Amputation-of-Finger as being subsumed by the concept Amputation-of-Arm. Finding a solution to problems such as these is known as repair in the DL community [Schlobach and Cornet, 2003], but it can also be seen as an instance of contraction, in this case by the statement Amputation-of-Finger ⊑ Amputation-of-Arm.

The scenario also illustrates why we are concerned with belief contraction of belief sets (logically closed theories) and not belief base contraction [Hansson, 1999]. Ontologies are not constructed by writing DL axioms, but rather using ontology editing tools, from which the axioms are generated automatically. Because of this, it is the belief set that is important, not the axioms fromwhich the theory is generated.

2 Logical Background and Belief Contraction

We work in a finitely generated propositional language LP over a set of propositional atoms P, which includes the distinguished atoms ⊤ and ⊥, and with the standard modeltheoretic semantics. Atoms will be denoted by p, q, . . ., possibly with subscripts. We use ϕ, ψ, . . . to denote classical formulas. They are recursively defined in the usual way.

We denote by V the set of all valuations or interpretations v : P -→ {0, 1}, with 0 denoting falsity and 1 truth. Satisfaction of ϕ by v is denoted by v ⊩ ϕ. The set of models of a set of formulas X is [X]. We sometimes represent the valuations of the logic under consideration as sequences of 0s and 1s, and with the obvious implicit ordering of atoms. Thus, for the logic generated from p and q, the valuation in which p is true and q is false will be represented as 10.

Classical logical consequence and logical equivalence are denoted by |= and ≡ respectively. For sets of sentences X and Φ, we understand X |= Φ to mean that X entails every element of Φ. For X ⊆ LP, the set of sentences logically entailed by X is denoted by Cn(X). A belief set is a logically closed set, i.e., for a belief set X, X = Cn(X). P(X) denotes the power set (set of all subsets) of X.

A Horn clause is a sentence of the form p1∧p2∧. . .∧pn → q where n ≥ 0. If n = 0 we write q instead of → q. A Horn theory is a set of Horn clauses. Given a propositional language LP, the Horn language LH generated from LP is simply the Horn clauses occurring in LP. The Horn logic obtained from LH has the same semantics as the propositional logic obtained from LP, but just restricted to Horn clauses. Thus a Horn belief set is a Horn theory closed under logical entailment, but containing only Horn clauses. Hence, |=, ≡, the Cn(.) operator, and all other related notions are defined relative to the logic we are working in (e.g. |=PL for propositional logic and |=HL for Horn logic). Since the context always makes it clear which logic we are dealing with, we shall dispense with such subscripts for the sake of readability.

AGM [Alchourr´on et al., 1985] is the best-known approach to contraction. It gives a set of postulates characterising all rational contraction functions. The aim is to describe belief contraction on the knowledge level independent of how beliefs are represented. Belief states are modelled by belief sets in a logic with a Tarskian consequence relation including classical propositional logic. The expansion of K by ϕ, K +ϕ, is defined as Cn(K ∪ {ϕ}). Contraction is intended to represent situations in which an agent has to give up information from its current beliefs. Formally, belief contraction is a (partial) function fromP(LP)×LP toP(LP): the contraction of a belief set by a sentence yields a new set.

The AGM approach to contraction requires that the following set of postulates characterise basic contraction.

• (K-4) If ̸|= ϕ, then ϕ /∈ K -ϕ

The intuitions behind these postulates have been debated in numerous works [G¨ardenfors, 1988; Hansson, 1999]. We will not do so here, and just note that (K-6), a.k.a. Recovery, is the most controversial.

Full AGM contraction involves two extended postulates in addition to the basic postulates given above, but a discussion on that is beyond the scope of this paper (see Section 7).

Various methods exist for constructing basic AGM contraction. In this paper we focus on the use of remainder sets.

Definition 2.1 For a belief set K, X ∈ K ↓ϕ iff (i) X ⊆ K, (ii) X ̸|= ϕ, and (iii) for every X′ s.t. X ⊂ X′ ⊆ K, X′ |= ϕ. We call the elements of K↓ϕ remainder sets of K w.r.t. ϕ.

It is easy to verify that remainder sets are belief sets, and that remainder sets can be generated semantically by adding precisely one countermodel of ϕ to the models of K (when such countermodels exist). Also, K↓ϕ = ∅ iff |= ϕ.

Since there is no unique method for choosing between possibly different remainder sets, AGM contraction presupposes the existence of a suitable selection function for doing so.

Definition 2.2 A selection function σ is a function from P(P(LP)) to P(P(LP)) such that σ(K ↓ ϕ) = {K}, if K ↓ϕ = ∅, and ∅ ̸= σ(K ↓ϕ) ⊆ K ↓ϕ otherwise.

Selection functions provide a mechanism for identifying the remainder sets judged to be most appropriate, and the resulting contraction is then obtained by taking the intersection of the chosen remainder sets.

Definition 2.3 For σ a selection function, -σ is a partial meet contraction iff K -σ ϕ = ⋂ σ(K ↓ϕ).

One of the fundamental results of AGM contraction is a representation theorem which shows that partial meet contraction corresponds exactly with the six basic AGM postulates.

Theorem 2.1 ([G¨ardenfors, 1988]) Every partial meet contraction satisfies (K-1)-(K-6). Conversely, every contraction function satisfying (K-1)-(K-6) is a partial meet contraction.

Two subclasses of partial meet deserve special mention.

Definition 2.4 Given a selection function σ, -σ is a maxichoice contraction iff σ(K ↓ϕ) is a singleton set. It is a full meet contraction iff σ(K ↓ϕ) = K ↓ϕ whenever K ↓ϕ ̸= ∅.

Clearly full meet contraction is unique, while maxichoice contraction usually is not. Observe also that partial meet contraction satisfies the following convexity principle.

Proposition 2.1 Let K be a belief set, let -mc be a maxichoice contraction, and let -fm be full meet contraction. For every belief set X s.t. (K -fm ϕ) ⊆ X ⊆ K -mc ϕ, there is a partial meet contraction -pm such that K -pm ϕ = X.

That is, every belief set between the results obtained from full meet contraction and some maxichoice contraction is obtained from some partial meet contraction. This result plays an important part in our definition of Horn contraction.

Horn Contraction Horn contraction differs from classical AGM contraction in a number of ways. The most basic differences are the use of Horn logic as the underlying logic and allowing for the contraction of finite sets of sentences Φ.

As recognised by Delgrande [2008], the move to Horn logic admits the possibility of more than one type of contraction. He considers two types: entailment-based contraction (or e-contraction) and inconsistency-based contraction (or i-contraction). In what follows, we recall Delgrande's approach and develop our theory of Horn contraction.

3 Entailment-based contraction

For e-contraction, the goal of contracting with a set of sentences Φ is the removal of at least one of the sentences in Φ. For full propositional logic, contraction with a set of sentences is not particularly interesting since contracting by Φ will be equivalent to contracting by the single sentence ∧ Φ. For Horn logic it is interesting though, since the conjunction of the sentences in Φ is not always expressible as a single sentence. (An alternative, and equivalent approach, would have been to allow for the conjunction of Horn clauses as Delgrande [2008] does, but for reasons that will become clear in Section 5, we have not opted for this choice.) Our starting point for defining Horn e-contraction is in terms of Delgrande's definition of e-remainder sets.

Definition 3.1 (Horn e-Remainder Sets) For a belief set H, X ∈ H ↓e Φ iff (i) X ⊆ H, (ii) X ̸|= Φ, and (iii) for every X′ s.t. X ⊂ X′ ⊆ H, X′ |= Φ. We refer to the elements of H ↓e Φ as the Horn e-remainder sets of H w.r.t. Φ.

It is easy to verify that all Horn e-remainder sets are belief sets. Also, H ↓e Φ = ∅ iff |= Φ.

We now proceed to define selection functions to be used for Horn partial meet e-contraction.

Definition 3.2 (Horn e-Selection Functions) A partial meet Horn e-selection function σ is a function from P(P(LH)) to P(P(LH)) s.t. σ(H ↓e Φ) = {H} if H ↓e Φ = ∅, and ∅ ̸= σ(H ↓e Φ) ⊆ H ↓e Φ otherwise.

Using these, we define partial meet Horn e-contraction.

Definition 3.3 (Partial Meet Horn e-Contraction) Given a partial meet Horn e-selection function σ, -σ is a partial meet Horn e-contraction iff H -σ Φ = ⋂ σ(H ↓e Φ).

We also consider two special cases.

Definition 3.4 (Maxichoice and Full Meet) Given a partial meet Horn e-selection function σ, -σ is a maxichoice Horn e-contraction iff σ(H↓eΦ) is a singleton set. It is a full meet Horn e-contraction iff σ(H ↓e Φ) = H ↓e Φ when H ↓e Φ ̸= ∅.

Example 3.1 Let H = Cn({p → q, q → r}). Then H ↓e {p → r} = {H′ ,H′′ }, where H′ = Cn({p → q}), and H′′ = Cn({q → r, p ∧ r → q}). So contracting with {p → r} yields either H′ , H′′ , or H′ ∩H′′ = Cn({p ∧ r → q}).

3.1 Beyond Partial Meet Contraction

While all partial meet e-contractions (and therefore also maxichoice and full meet e-contractions) are appropriate choices for e-contraction, they do not make up the set of all appropriate Horn e-contractions. This has a number of implications, one of them being that it conflicts with Delgrande's conjecture that orderly maxichoice e-contraction is the appropriate form of e-contraction (see Section 6).

The argument that maxichoice e-contraction is not sufficient is a relatively straightforward one. In full propositional logic the argument against maxichoice contraction relates to the link between AGM revision and contraction via the Levi Identity [Levi, 1977]: K ⋆ ϕ = (K - ¬ϕ) + ϕ. For maxichoice contraction this has the unfortunate consequence that a revision operator obtained via the Levi Identity will satisfy the following "fullness result", i.e., K ⋆ ϕ is a complete theory: If ¬ϕ ∈ K then for all ψ ∈ LP, ψ ∈ K ⋆ ϕ or ¬ψ ∈ K ⋆ ϕ. Semantically, this occurs because the models of any remainder set for ϕ are obtained by adding a single countermodel of ¬ϕ to the models of K. And while it is true that e-remainder sets for Horn logic do not always have this property, the fact is that they still frequently do, which means that maxichoice e-contraction will frequently cause the same problems as in propositional logic. For example, consider the Horn belief set H = Cn({p, q}). It is easy to verify that [H] = {11}, that the e-remainder sets of {p} w.r.t. H are H′ = Cn({p → q, q → p}) and H′′ = Cn({q}), and that [H′ ] = {11, 00} and [H′′ ] = {11, 01}: i.e., the models of H′ and H′′ are obtained by adding to the models of H a single countermodel of p. This is not to say that maxichoice e-contraction is never appropriate. Similar to the case for full propositional logic, we argue that all maxichoice Horn e-contractions ought to be seen as rational ways of contracting. It is just that other possibilities may be more applicable in certain situations. And, just as in the case for full propositional logic, this leads to the conclusion that all partial meet e-contractions ought to be seen as appropriate.

Once partial meet e-contraction has been accepted as necessary for Horn e-contraction, the obvious next question is whether partial meet Horn e-contraction is sufficient, i.e., whether there are any rational e-contractions that are not partial meet Horn e-contractions. For full propositional logic the sufficiency of partial meet contraction can be justified by Proposition 2.1 which, as we have seen, states that every belief set between full meet contraction and some maxichoice contraction is obtained from some partial meet contraction. It turns out that the same result does not hold for Horn logic.

Example 3.2 As we have seen in Example 3.1, for the e-contraction of {p → r} from the Horn belief set Cn({p → q, q → r}), full meet yields Hfm = Cn({p ∧ r → q}) while maxichoice yields either H1mc = Cn({p → q}) or H2mc = Cn({q → r, p ∧ r → q}). Now consider the belief set H′ = Cn({p ∧ q → r, p ∧ r → q}). It is clear that Hfm ⊆ H′ ⊆ H2mc , but there is no partial meet e-contraction yielding H′ .

Our contention is that Horn e-contraction should be extended to include cases such as H′ above. Since full meet Horn econtraction is deemed to be appropriate, it stands to reason that any belief set H′ bigger than it should also be seen as appropriate, provided that H′ does not contain any irrelevant additions. But since H′ is contained in some maxichoice Horn e-contraction, H′ cannot contain any irrelevant additions. After all, the maxichoice Horn e-contraction contains only relevant additions, since it is an appropriate form of contraction. Hence H′ is also an appropriate result of e-contraction.

Definition 3.5 (Infra e-Remainder Sets) For belief sets H and X, X ∈ H ⇓e Φ iff there is some X′ ∈ H ↓e Φ s.t. (⋂ H ↓e Φ) ⊆ X ⊆ X′ . We refer to the elements of H ⇓e Φ as the infra e-remainder sets of H w.r.t. Φ.

Note that all e-remainder sets are also infra e-remainder sets, and so is the intersection of any set of e-remainder sets. Indeed, the intersection of any set of infra e-remainder sets is also an infra e-remainder set. So the set of infra e-remainder sets contain all belief sets between some Horn e-remainder set and the intersection of all Horn e-remainder sets. This explains why Horn e-contraction is not defined as the intersection of infra e-remainder sets (cf. Definition 3.3).

Definition 3.6 (Horn e-Contraction) An infra e-selection function τ is a function from P(P(LH)) to P(LH) s.t. τ(H ⇓e Φ) = H whenever |= Φ, and τ(H ⇓e Φ) ∈ H ⇓e Φ otherwise. A contraction function -τ is a Horn e-contraction iff H -τ Φ = τ (H ⇓e Φ).

3.2 ARepresentation Result

Our representation result makes use of all of the basic AGM postulates, except for the Recovery Postulate (K - 6). It is easy to see that Horn e-contraction does not satisfy Recovery. As an example, take H = Cn({p → r}) and let Φ = {p ∧ q → r}. Then H - Φ = Cn(∅) and so (H -e Φ) + Φ = Cn({p ∧ q → r}) ̸= H. In place of Recovery we have a postulate that closely resembles Hansson's [1999] Relevance Postulate, and a postulate handling the case when trying to contract with a tautology.

Postulates (H-e1)-(H-e5) are analogues of (K-1)-(K-5), while (H -e 6) states that all sentences removed from H during a Φ-contraction must have been removed for a reason: adding them again brings back Φ. (H-e7) simply states that contracting with a (possibly empty) set of tautologies leaves the initial belief set unchanged. We remark that (H -e 3) is actually redundant in the list, since it can be shown to follow mainly from (H -e 6).

Theorem 3.1 Every Horn e-contraction satisfies (H -e 1)- (H -e 7). Conversely, every contraction function satisfying (H -e 1)-(H -e 7) is a Horn e-contraction.

4 Inconsistency-based Contraction

We now turn our attention to Delgrande's second type of contraction for Horn logic: inconsistency-based contraction, or i-contraction. The purpose of this type of contraction by a set Φ is to modify the belief set H in such a way that adding Φ to H does not result in an inconsistent belief set: (H -i Φ) + Φ ̸|= ⊥. Our starting point for defining i-contraction is in terms of Delgrande's definition of iremainder sets with respect to Horn logic.

Definition 4.1 (Horn i-Remainder Sets) For a belief set H, X ∈ H ↓i Φ iff (i) X ⊆ H, (ii) X + Φ ̸|= ⊥, and (iii) for every X′ s.t. X ⊂ X′ ⊆ H, X′ +Φ |= ⊥. We refer to the elements of H ↓i Φ as the Horn i-remainder sets of H w.r.t. Φ.

It is again easy to verify that Horn i-remainder sets are belief sets and that H ↓i Φ = ∅ iff Φ |= ⊥.

The definition of i-remainder sets is similar enough to that of e-remainder sets (Definition 3.1) that we can define partial meet Horn i-selection functions, partial meet Horn icontraction, maxichoice Horn i-contraction, and full meet Horn i-contraction by repeating Definitions 3.2, 3.3, and 3.4, but referring to H↓iΦ rather than H↓eΦ.

4.1 Beyond Partial Meet

As in the case for e-contraction we argue that while partial meet Horn i-contractions are all appropriate forms of i-contraction, they do not represent all rational forms of i-contraction. The argument against maxichoice Horn icontraction is essentially the same one put forward against maxichoice Horn e-contraction. That is, the result H -i Φ of maxichoice Horn i-contraction frequently results in a belief set which differs semantically from H by adding a single valuation to the models of H in order to avoid inconsistency. We can, in fact, use a variant of the same example used against maxichoice Horn e-contraction. Let H = Cn({p, q}) and Φ = {p → ⊥}. Then [H] = {11}, the i-remainder sets of Φ w.r.t. H are H′ = Cn({p → q, q → p}) and H′′ = Cn({q}), and [H′ ] = {11, 00} and [H′′ ] = {11, 01}: i.e., the models of H′ and H′′ are obtained by adding to the models of H a single valuation in order to avoid inconsistency. The case against partial meet Horn i-contraction is again based on the fact that it does not always include all belief sets between some maxichoice Horn i-contraction and full meet Horn i-contraction, leading us to infra i-remainder sets.

Definition 4.2 (Infra i-Remainder Sets) For belief sets H and X, X ∈ H ⇓i Φ iff there is some X′ ∈ H ↓i Φ s.t. (⋂ H ↓i Φ) ⊆ X ⊆ X′ . We refer to the elements of H ⇓i Φ as the infra i-remainder sets of H w.r.t. Φ.

And Horn i-contraction is defined i.t.o. infra i-remainder sets.

Definition 4.3 (Horn i-Contraction) An infra i-selection function τ is a function from P(P(LH)) to P(LH) s.t. τ (H ⇓i Φ) = H whenever Φ |= ⊥, and τ (H ⇓i Φ) ∈ H ⇓i Φ otherwise. A contraction function -τ is a Horn i-contraction iff H -τ Φ = τ (H ⇓i Φ).

4.2 ARepresentation Result

Our representation result for i-contraction is very similar to that for e-contraction and Postulates (H-i1)-(H-i7) below are clearly close analogues of (H-e 1)-(H-e 7).

Analogously with e-contraction, rule (H-i3) can be shown to follow mainly from (H-i6). We show that Horn i-contraction is characterised precisely by these postulates.

Theorem 4.1 Every Horn i-contraction satisfies (H -i 1)- (H -i 7). Conversely, every contraction function satisfying (H-i 1)-(H-i 7) is a Horn i-contraction.

5 Package Horn Contraction

The third and last type of contraction we consider is referred to as package contraction, a type of contraction studied by Fuhrmann and Hansson [1994] for the classical case (i.e., for logics containing full propositional logic). The goal is to remove all sentences of a set Φ from a belief set H. For full propositional logic this is similar to contracting with the disjunction of the sentences in Φ. For Horn logic, which does not have full disjunction, package contraction is more interesting. Our primary interest in package contraction relates to an important version of contraction occurring in ontological reasoning, as we shall see below.

Our starting point is again in terms of remainder sets.

Definition 5.1 (Horn p-Remainder Sets) For a belief set H, X ∈ H ↓p Φ iff (i) X ⊆ H, (ii) Cn(X) ∩ Φ = ∅, and (iii) for all X′ s.t. X ⊂ X′ ⊆ H, Cn(X′ ) ∩ Φ ̸= ∅. The elements of H ↓p Φ are referred to as the Horn p-remainder sets of H w.r.t. Φ.

It is easily verified that Horn p-remainder sets are belief sets. In addition, the following definition will be useful.

Definition 5.2 A set Φ is tautologous iff for every valuation v, there is a ϕ ∈ Φ such that v ⊩ ϕ.

It can be verified that H↓pΦ = ∅ iff Φ is tautologous. (Note that tautologous is not the same as tautological.)

The definition of p-remainder sets is similar enough to that of e-remainder sets (Definition 3.1) that we can define partial meet Horn p-selection functions, partial meet Horn pcontraction, maxichoice Horn p-contraction, and full meet Horn p-contraction by repeating Definitions 3.2, 3.3, and 3.4, but referring to H↓pΦ rather than H↓eΦ.

Since e- and p-contraction coincide for contraction by singleton sets, our argument also holds for p-contraction. Also, Example 3.2 is also applicable to p-contraction, from which it follows that partial meet p-contraction is not sufficient either. Consequently, as we did for e-contraction and i-contraction, we move to infra p-remainder sets.

Definition 5.3 (Infra p-Remainder Sets) For belief sets H and X, X ∈ H ⇓p Φ iff there is some X′ ∈ H ↓p Φ s.t. (⋂ H ↓p Φ) ⊆ X ⊆ X′ . We refer to the elements of H ⇓p Φ as the infra p-remainder sets of H w.r.t. Φ.

Horn p-contraction is then defined in terms of infra premainder sets in the obvious way.

Definition 5.4 (Horn p-contraction) An infra p-selection function τ is a function from P(P(LH)) to P(LH) such that τ(H ⇓p Φ) = H whenever Φ is tautologous, and τ(H ⇓p Φ) ∈ H ⇓p Φ otherwise. A contraction function -τ is a Horn p-contraction iff H -τ Φ = τ(H⇓pΦ).

5.1 ARepresentation Result

The representation result for p-contraction is very similar to that for e-contraction, with Postulates (H -p 1)-(H -p 7) being close analogues of (H-e 1)-(H-e 7).

Observe that the following definition is used in (H-p 5).

Definition 5.5 For sets of sentences Φ and Ψ, Φˆ≡Ψ iff either both are tautologous, or ∀v ∈ V, ∃ϕ ∈ Φ s.t. v ⊩ ϕ iff ∃ψ ∈ Ψ s.t. v ⊩ ψ.

This definition describes a notion of set equivalence which is appropriate to ensure syntax independence.

Once more (H-p3) is actually redundant here. We show that these postulates characterise Horn p-contraction exactly.

Theorem 5.1 Every Horn p-contraction satisfies (H -p 1)- (H -p 7). Conversely, every contraction function satisfying (H -p 1)-(H -p 7) is a Horn p-contraction.

5.2 p-Contraction as i-Contraction

In addition to package contraction being of interest in its own right, we have a specific interest in the case where Φ contains only basic Horn clauses: those with exactly one atom in the head and in the body. Our interest in this case is because of its relation to an important version of contraction for ontological reasoning in the EL family of description logics. Briefly, basic Horn clauses correspond closely to basic subsumption statements in the EL family: statements of the form A ⊑ B where A and B are concept names. Its importance stems from the fact that basic subsumption statements are used to repair the subsumption hierarchy. A detailed investigation of this form of contraction for the EL family is beyond the scope of this paper. Here we just show that Horn p-contraction with basic Horn clauses can be represented as a special case of Horn i-contraction. Define i as a function from sets of basic Horn clauses to sets of Horn clauses, such that for any set Φ = {p1 → q1, . . . , pn → qn} of basic Horn clauses, we have i(Φ) = {p1, . . . , pn, q1 → ⊥, . . . , qn → ⊥}.

Proposition 5.1 Let H be a Horn belief set and let Φ be a set of basic Horn clauses. Then K -p Φ = K -i i(Φ).

It is worth noting that this result does not hold for the case where Φ includes general Horn clauses.

6 RelatedWork

Work on belief change for Horn logics has focused mostly on belief revision [Eiter and Gottlob, 1992; Liberatore, 2000; Langlois et al., 2008]. The only work of importance on Horn contraction, to our knowledge, is that of Delgrande [2008], and this section is mainly devoted to a discussion of his work.

Delgrande defines and characterises a version of econtraction which introduces additional structure in the choice of e-remainder sets by placing a linear order on all e-remainder sets involving a belief set H (i.e., for all possible Φs). When performing contraction by a set Φ, one is obliged to choose the remainder set of H w.r.t. Φ that is minimal w.r.t. the linear order. The additional structure imposed by the use of these linear orders ensures that this kind of e-contraction is actually more restrictive than maxichoice e-contraction, although Delgrande refers to it as maxichoice e-contraction. We shall refer to it as orderly maxichoice e-contraction. Delgrande conjectures that orderly maxichoice e-contraction is the appropriate form of e-contraction for Horn logic. Our work is not directly comparable to that of Delgrande since he works on the level of full AGM contraction, obtained by also considering the extended postulates, whereas we are concerned only with basic contraction, and leave the extension to full contraction for future work. Nevertheless, as spelt out in Section 3, it is clear that an extension to full contraction will involve more than just orderly maxichoice e-contraction.

Delgrande also defines a version of orderly maxichoice icontraction, but his representation result is in terms of maxichoice i-contraction: he refers to it as singleton i-contraction. He takes a fairly dim view of i-contraction, primarily because of the following result: If p → ⊥ ∈ H then either q ∈ H -i {p} or q → ⊥ ∈ H -i {p} for every atom q. His main concern with this is related to the fact that revision defined in terms of the Levi Identity (i-contraction followed by expansion) will yield a result in which all structure of H, given in terms of Horn clauses, is lost. This means that for him a move to partial meet i-contraction is not the solution either, since any prior structure contained in H will still be lost. We view this objection as somewhat surprising in this context, since Horn contraction is intended to operate on the knowledge level in which the structure of the theory from which the belief set is generated is irrelevant. So, while we agree that the formal result on which he bases his objections is a good argument against maxichoice i-contraction (it is closely related to our argument against maxichoice e-contraction in Section 3), it does not provide a persuasive argument against partial meet i-contraction. It is worth noting that he does not consider i-contraction in terms of infra i-remainder sets at all. Finally, Delgrande expresses doubts about i-contraction, but our result in Section 5.2 shows that this might be too pessimistic.

7 Conclusion and FutureWork

We have laid the groundwork for contraction in Horn logic by providing formal accounts of basic versions of three types of contraction: e-contraction and i-contraction, previously studied by Delgrande [2008], and p-contraction. We showed that Delgrande's conjectures about orderly maxichoice contraction being the appropriate version for these two forms of contraction were perhaps a bit premature.

Here we focus only on basic Horn contraction. For future work we plan to investigate Horn contraction for full AGM contraction, obtained by adding the extended postulates. Finally, we plan to extend our results for Horn contraction to DLs, specifically the EL family of DLs. In this context we also plan to investigate a connection between p-contraction and e-contraction, suggested by an anonymous reviewer.