# entrenchmentbased_horn_contraction__cbd26a0d.pdf Journal of Artificial Intelligence Research 51 (2014) 227-254 Submitted 04/14; published 09/14 Entrenchment-Based Horn Contraction Zhiqiang Zhuang z.zhuang@griffith.edu.au Institute for Integrated and Intelligent Systems Griffith University, QLD 4111, Australia Maurice Pagnucco morri@cse.unsw.edu.au School of Computer Science and Engineering The University of New South Wales, NSW 2052, Australia The AGM framework is the benchmark approach in belief change. Since the framework assumes an underlying logic containing classical Propositional Logic, it can not be applied to systems with a logic weaker than Propositional Logic. To remedy this limitation, several researchers have studied AGM-style contraction and revision under the Horn fragment of Propositional Logic (i.e., Horn logic). In this paper, we contribute to this line of research by investigating the Horn version of the AGM entrenchment-based contraction. The study is challenging as the construction of entrenchment-based contraction refers to arbitrary disjunctions which are not expressible under Horn logic. In order to adapt the construction to Horn logic, we make use of a Horn approximation technique called Horn strengthening. We provide a representation theorem for the newly constructed contraction which we refer to as entrenchment-based Horn contraction. Ideally, contractions defined under Horn logic (i.e., Horn contractions) should be as rational as AGM contraction. We propose the notion of Horn equivalence which intuitively captures the equivalence between Horn contraction and AGM contraction. We show that, under this notion, entrenchment-based Horn contraction is equivalent to a restricted form of entrenchment-based contraction. 1. Introduction Given an agent with a set of beliefs, the theory of belief change deals with how the agent changes its beliefs in a rational manner when it is confronted with new information. Two kinds of changes are mainly studied, namely contraction and revision, for removing old beliefs and for incorporating new beliefs respectively. The main strategies for studying belief change are to articulate principles called rationality postulates that rational agents should obey when contracting or revising their sets of beliefs and to specify explicit change mechanisms called construction methods for the contraction and revision operation. The dominant theory of belief change is the so called AGM framework (Alchourr on, G ardenfors, & Makinson, 1985; G ardenfors, 1988). The framework does not specify a specific underlying logic, however, it assumes that the logic contains classical Propositional Logic. It is commonly accepted that the AGM framework provides the best set of rationality postulates for capturing the intuitions behind rational belief change along with well motivated construction methods that can be characterised by the rationality postulates. Regardless of its desirable properties, this assumption on the underlying logic is a severe limitation. Tractable fragments of Propositional Logic and some non-classic logics such as Description Logics (Baader, Calvanese, Mc Guinness, Nardi, & Patel-Schneider, 2003) are particu- c 2014 AI Access Foundation. All rights reserved. Zhuang & Pagnucco larly useful in artificial intelligence applications as they allow for efficient reasoning methods. Since knowledge evolves, systems based on these logics are subject to change. However, fragments of Propositional Logic and Description Logics do not subsume Propositional Logic, thus the AGM framework can not be applied to these systems. Consequently, extensive attention has been paid to the problem of belief change under fragments of Propositional Logic and Description Logics. A recent trend focuses on the Horn fragment of Propositional Logic (i.e., Horn Logic) which has found extensive usage in artificial intelligence and database systems. In this paper we contribute to Horn belief change by thoroughly investigating the Horn version of entrenchment-based contraction (G ardenfors & Makinson, 1988; G ardenfors, 1988) which we refer to as entrenchment-based Horn contraction. Entrenchment-based contraction is based on rankings of formulas called epistemic entrenchments. The general idea is that formulas more entrenched in the ranking are more preferred to those less entrenched and, when deciding which formulas to give up in a contraction; it is intuitive to give up the less preferred beliefs. An obvious obstacle in adapting the entrenchment-based contraction to Horn logic is that the standard construction refers to disjunctions which may be non-Horn formulas. Therefore, we can not apply the construction method directly under Horn logic. To get around this expressiveness problem we propose to replace the non-Horn formulas with their Horn approximations (Kautz & Selman, 1996). The contraction thus constructed satisfies Horn versions of all the characterising postulates for entrenchment-based contraction, except the Recovery postulate (Alchourr on et al., 1985). Due to the limited expressiveness of Horn logic, entrenchment-based Horn contraction is not as comprehensive as entrenchment-based contraction. Therefore, in characterising entrenchment-based Horn contraction, an extra postulate is needed to capture how restricted it is (compared to entrenchment-based contraction). Ideally, Horn contraction should perform as rationally as AGM contraction. To evaluate the rationality of Horn contractions against AGM contraction, we propose the notion of Horn equivalence which formalises the equivalence between Horn contraction functions and AGM contraction functions from a constructive point of view. Horn contractions are restricted to Horn formulas, thus it is fair to say a Horn contraction function performs as rationally as an AGM one if the change over Horn formulas as a result of the AGM contraction function is identical to that incurred by the Horn contraction function. Put simply, a Horn contraction function is Horn equivalent to its AGM counterpart if they behave identically in terms of Horn formulas. In other words, Horn equivalence implies that the change mechanism of the AGM contraction function is exactly the same as that of the Horn contraction function, thus the latter preserves every property of the former. We are able to identify a restricted form of entrenchment-based contraction that has a one-to-one correspondence with entrenchment-based Horn contraction by means of Horn equivalence. Due to the contention over the Recovery postulate, Makinson introduced the idea of a Withdrawal function which encompasses a broader class of belief contraction functions. In the AGM setting, Rott and Pagnucco (1999) explored severe withdrawal, an operation similar to contraction but defined intentionally to violate the Recovery postulate. They propose a construction for severe withdrawal that is based on epistemic entrenchment which we refer to as entrenchment-based withdrawal. Different from entrenchment-based contraction, the construction does not refer to arbitrary disjunctions. Moreover, as we will see, Horn contractions are intrinsically incompatible with Recovery, thus it is curious to see Entrenchment-Based Horn Contraction if entrenchment-based withdrawal is seamlessly transferable to Horn logic. Through investigating the Horn version of entrenchment-based withdrawal we can give an affirmative answer. The rest of this paper is organised as follows. We first give the technical preliminaries in Section 2, then in Section 3 we recall the details of entrenchment-based contraction. In Section 4, we introduce entrenchment-based Horn contraction and present its representation theorem. In Section 5, we compare entrenchment-based Horn contraction and entrenchment-based contraction through the notion of Horn equivalence. In Section 6 we introduce entrenchment-based Horn withdrawal and demonstrate its close connection with entrenchment-based withdrawal. Finally, the related work and conclusions are given in Section 7 and Section 8 respectively. Proofs are given in the appendix. This paper is a revised and extended version of (Zhuang & Pagnucco, 2010). 2. Technical Preliminaries We assume a propositional language L over a finite set of atoms P which is closed under the usual truth-functional connectives and contains the propositional constants (truth) and (falsum). Atoms are denoted by lower case Roman letters (p, q, . . .). Formulas are denoted by lower case Greek letters (φ, ψ, . . .). Sets of formulas are denoted by upper case Roman letters (V, X, . . .). The logic generated from L is specified by the standard Tarskian consequence operator Cn. For any set of formulas X, Cn(X) denotes the set of formulas following logically from X. For any formula φ, Cn(φ) abbreviates Cn({φ}). We sometimes write X φ to denote φ Cn(X), φ ψ to denote Cn(φ) = Cn(ψ), and φ to denote φ Cn( ). The letter K is reserved to represent a theory or a belief set which is a set of formulas such that K = Cn(K). Standard propositional semantics is assumed. An interpretation µ is a model of a formula φ if φ is true in µ. For any set of formulas X, |X| denotes the set of models of X. For any formula φ, |φ| abbreviates |{φ}|. A clause is a disjunction of positive and negative atoms. A Horn clause is a clause that contains at most one positive atom, e.g. a b c. A Horn formula is a conjunction of Horn clauses. The Horn language LH is the maximal subset of L containing only Horn formulas. The Horn logic generated from LH is specified by the consequence operator Cn H such that, for any set of Horn formulas X, Cn H(X) = Cn(X) LH. The letter H is reserved to represent a Horn theory or a Horn belief set which is a set of Horn formulas such that H = Cn H(H). The Horn subset function H : 2L 2LH is such that given a set of formulas X, H(X) is the set of Horn formulas in X. Formally, H(X) = LH X. 3. Entrenchment-Based Contraction An AGM contraction function . takes as input a belief set K and a formula φ and returns another belief set K . φ. We refer to K as the original belief set, φ as the contracting formula, and K . φ as the resulting belief set. Various constructions have been proposed for contraction in the AGM framework. In this section, we review a classical one called entrenchment-based contraction (G ardenfors, 1988; G ardenfors & Makinson, 1988). Zhuang & Pagnucco The beliefs held by an agent are not equal in terms of epistemological importance. In the work of G ardenfors (1988) and G ardenfors and Makinson (1988), the more important beliefs are said to be more entrenched than the others. The idea behind entrenchmentbased contraction is that, in a contraction, we should give up the less entrenched formulas whenever possible. The relative entrenchments between formulas are modeled by epistemic entrenchments. Given a belief set K, the epistemic entrenchment associated with K is a binary relation over L such that φ ψ means ψ is at least as entrenched as φ. The strict relation φ < ψ is defined as φ ψ and ψ φ. Importantly, satisfies the following conditions: (EE1) If φ ψ and ψ χ, then φ χ (Transitivity) (EE2) If φ ψ, then φ ψ (Dominance) (EE3) φ φ ψ or ψ φ ψ (Conjunctiveness) (EE4) If K , then φ K iffφ ψ for every ψ (Minimality) (EE5) If φ ψ for every φ, then ψ (Maximality) Thus an epistemic entrenchment is a transitive relation (EE1) such that logically stronger formulas are not more entrenched than weaker ones (EE2), a conjunction is equally or more entrenched than one of its conjuncts (EE3), non-beliefs are least entrenched (EE4), and tautologies are most entrenched (EE5). Entrenchment-based contraction is defined through two conditions which establish the connections between epistemic entrenchments and contraction functions. Condition (C ) generates an epistemic entrenchment from a contraction function. The motivation is that, in the contraction of K by φ ψ, we have to give up either φ or ψ (or both), however, it is more intuitive to give up the epistemically less important one. Thus, if φ is retracted, then it must be the case that ψ is at least as entrenched as φ. In the limiting case that φ and ψ are both tautologies, they are equally important and, by (EE5), required to be maximally entrenched. (C ) : φ ψ iffφ K . φ ψ or φ ψ. Condition (C . ) derives a contraction function from an epistemic entrenchment. According to (C . ), ψ is retained in the contraction by φ if and only if it was originally believed (i.e., ψ K) and either there is sufficient evidence for retaining it (i.e., φ < φ ψ) or it is not possible to remove φ (i.e., φ). (C . ) : ψ K . φ iffψ K and either φ < φ ψ or φ. The contraction function generated via (C . ) is referred to as an entrenchment-based contraction function. Definition 1 (G ardenfors & Makinson, 1988) A function . is an entrenchment-based contraction function for K iffits outcome is determined by the epistemic entrenchment for K via (C . ). As pointed out in the work of G ardenfors and Makinson (1988), it is rather difficult to motivate (C . ), however, its appropriateness can be justified by the representation theorem for entrenchment-based contraction. Entrenchment-Based Horn Contraction Theorem 1 (G ardenfors & Makinson, 1988) A function . is an entrenchment-based contraction function iff. satisfies the following postulates: (K . 1) K . φ = Cn(K . φ) (Closure) (K . 2) K . φ K (Inclusion) (K . 3) If φ K, then K . φ = K (Vacuity) (K . 4) If φ, then φ K . φ (Success) (K . 5) K (K . φ) + φ (Recovery) (K . 6) If φ ψ, then K . φ = K . ψ (Extensionality) (K . 7) K . φ K . ψ K . φ ψ (Conjunctive Overlap) (K . 8) If φ K . φ ψ then K . φ ψ K . φ (Conjunctive Inclusion) By Theorem 1, entrenchment-based contraction functions are characterised by the full set of AGM postulates for contraction (K . 1) (K . 8). In the AGM tradition, (K . 1) (K . 6) are referred to as the basic postulates and (K . 7) and (K . 8) are referred to as the supplementary postulates. According to the basic postulates, a contraction produces a belief set (K . 1) which does not contain the contracting formula unless it is a tautology (K . 4). The produced belief set is not larger than the original one (K . 2). If the contracting formula is not believed, then nothing has to be done (K . 3). The contraction is syntax-insensitive (K . 6) and when the contracted formula is added back to the contracted belief set, the result entails every formula in the original belief set (K . 5). (K . 5), which is often called Recovery, is controversial and has been the subject of much discussion (e.g., Makinson, 1987; Hansson, 1991; Levi, 1991). For example in the work of Hansson (1991), it is argued as an emerging property rather than a fundamental postulate for contraction. The supplementary postulates concern relations between contraction by a conjunction and contractions by the constituent conjuncts. Formulas surviving the contraction of each conjunct also survive the contraction by the conjunction (K . 7). If a conjunct is removed in the contraction by the conjunction, then formulas surviving the contraction by the conjunction also survive the contraction by the removed conjunct (K . 8). Some postulates equivalent to (K . 7) have been proposed which are essential for proving the representation theorems for AGM contractions. In the presence of the basic postulates, (K . 7) is equivalent to the postulate of Partial Antitony (Alchourr on et al., 1985) (K . pa) K . φ Cn(φ) K . (φ ψ) and the postulate of Conjunctive Trisection (Rott, 1992; Hansson, 1993). (K . ct) If φ K . (φ ψ) then φ K . (φ ψ δ) (K . pa) has a rather technical nature, however, (K . ct) is well motivated. Informally speaking, it says the preferred belief (i.e., φ) of a pair (i.e., φ, ψ) is not the least preferred when a third belief (i.e., δ) is added to the pair. In a contraction, it is rational to discard the less entrenched formulas whenever possible, thus φ being retained in contracting by φ ψ means φ is more entrenched than ψ. Since φ is more entrenched than ψ, it is not the least entrenched one among φ, ψ, and δ. Therefore, φ should be retained in contracting by φ ψ δ. In other words, preferences cannot be changed when other beliefs are considered. Zhuang & Pagnucco 4. Entrenchment-Based Horn Contraction Although entrenchment-based contraction is defined while assuming Propositional Logic, the intuition behind the construction is universal and can be applied to fragments of Propositional Logic. In this section, we apply the intuition to the Horn fragment. 4.1 Horn Strengthening Standard entrenchment-based contraction makes use of a disjunctive formula in the condition (C . ). In adapting the construction method to Horn logic, an immediate problem is that the disjunctive formula may be non-Horn. In such cases, we propose to replace the non-Horn formula with its Horn approximations, more precisely, its Horn strengthenings (Kautz & Selman, 1996). The notion of Horn strengthening is proposed by Kautz and Selman in the context of knowledge compilation. Their original definition is for clauses and sets of clauses such that a Horn strengthening for a clause C is logically the weakest Horn clause that entails C and a Horn strengthening for a set of clauses {C1, . . . , Cn} is any set of Horn clauses {C 1, . . . , C n} where C i is the Horn strengthening of Ci. Here we reformulate their definition to cover arbitrary formulas such that, for a formula φ, a Horn strengthening is logically the weakest Horn formula that entails φ. Definition 2 Let φ be a formula. The set of Horn strengthenings of φ, denoted by HS(φ), is such that χ HS(φ) iff 2. |χ| |φ|; and, 3. there is no χ LH such that |χ| |χ | |φ|. According to Definition 2, a Horn formula has one Horn strengthening, namely itself. In the limiting case of φ being a tautology, we assume that its single Horn strengthening is itself. The following results provide new properties of Horn strengthenings that will be helpful in this paper. Firstly, since Definition 2 is model-theoretic, the set of Horn strengthenings for logically equivalent formulas are identical. Lemma 1 If φ ψ, then HS(φ) = HS(ψ). If a Horn formula ψ entails another formula φ which is not necessarily Horn, then ψ must also entail a Horn strengthening of φ. Lemma 2 If ψ is a Horn formula such that ψ φ, then there is χ HS(φ) such that ψ χ. Any Horn strengthening of a conjunction can be formed by conjoining some Horn strengthenings for each conjunct. Lemma 3 If χ HS(φ ψ), then there is χ1 HS(φ) and χ2 HS(ψ) such that χ χ1 χ2. Entrenchment-Based Horn Contraction If χ is a Horn strengthening of φ ψ such that φ and ψ are Horn formulas, then every Horn strengthening of φ χ is a Horn strengthening of φ ψ. Lemma 4 Let ψ and φ be Horn formulas. If χ HS(φ ψ), then HS(φ χ) HS(φ ψ). 4.2 Construction In constructing the Horn version of an entrenchment-based contraction function, we also need a relation that captures the relative importance between formulas. Since, in Horn belief change, formulas are restricted to the Horn fragment of Propositional Logic, the relation is over Horn formulas. We define a Horn epistemic entrenchment as a binary relation over LH that satisfies (HEE1) (HEE5): (HEE1) If φ ψ and ψ χ, then φ χ (HEE2) If φ ψ, then φ ψ (HEE3) φ φ ψ or ψ φ ψ (HEE4) If H , then φ H iffφ ψ for every ψ (HEE5) If φ ψ for every φ, then ψ (HEE1) (HEE5) are simply (EE1) (EE5) restricted to Horn formulas and Horn belief sets. We can derive the following properties for Horn epistemic entrenchment. Lemma 5 Let be a Horn epistemic entrenchment. Then satisfies (cf. (Foo, 1990)): 1. φ ψ or ψ φ 2. If ψ χ φ, then ψ φ or χ φ 3. φ < ψ iffφ ψ < ψ 4. If χ φ and χ ψ, then χ φ ψ 5. If χ < φ and χ < ψ, then χ < φ ψ 6. If φ ψ, then φ φ ψ 7. If φ ψ then φ ψ and ψ φ Particularly, Horn epistemic entrenchment is connected (Item 1) and is such that logically equivalent formulas are equally entrenched (Item 7). Clearly, we can obtain a Horn epistemic entrenchment from an epistemic entrenchment by simply removing the entrenchment relations involving non-Horn formulas. The obtained Horn epistemic entrenchment is called the Horn subset of the epistemic entrenchment. Definition 3 Let H be a Horn epistemic entrenchment and P an epistemic entrenchment. Then H is the Horn subset of P iff φ P ψ iffφ H ψ for all φ, ψ LH. Zhuang & Pagnucco Notice that each epistemic entrenchment has one Horn subset but different epistemic entrenchments may have the same Horn subset. In the latter case, the epistemic entrenchments are identical with respect to the entrenchments between Horn formulas but different with respect to those involving non-Horn formulas. Condition (C . ) is central in determining the outcome of entrenchment-based contraction functions. According to (C . ), in the contraction of K by φ, if ψ is in K, then the disjunction φ ψ being strictly more entrenched than φ is a sufficient condition for retaining ψ. Since φ ψ is an arbitrary disjunction, it may not be a Horn formula. Therefore, (C . ) is not applicable in Horn logic. In forming a similar condition for Horn contraction, we replace the non-Horn disjunctions by their Horn strengthenings which results in the following condition: (HC . ): ψ H . φ iffψ H and either φ or there is χ HS(φ ψ) such that φ < χ. According to (HC . ), in the contraction of H by φ, if ψ is in H, then the existence of one Horn strengthening of φ ψ being strictly more entrenched than φ is a sufficient condition for retaining ψ. Similar to (C . ), another sufficient condition is φ being a tautology. Since φ ψ is logically weaker than its Horn strengthenings, for any epistemic entrenchment (EE2) implies that φ ψ is equal or more entrenched than its Horn strengthenings. Thus by (EE1) if any Horn strengthening of φ ψ is strictly more entrenched than φ, then so is φ ψ. The converse, however, does not hold in general. So, informally speaking, (HC . ) is a stricter condition than (C . ) for retaining formulas in a contraction. We refer to the Horn contraction function generated via (HC . ) as an entrenchment-based Horn contraction function. Definition 4 A function . is an entrenchment-based Horn contraction function for H iff its outcome is determined by the Horn epistemic entrenchment for H via (HC . ). p q p r q q r p r p q r p q r p q p r q q p r q r p q p r q q p r q r Figure 1: Entrenchment based Horn contraction function and entrenchment based contraction functions that are determined respectively by H, p1 and P2 such that H is the Horn subset of P1 and P2. Figure 1 demonstrates the contraction of H = Cn H({ p q, q r}) by p r such that the contraction is determined by the Horn epistemic entrenchment H via (HC . ) and the contraction of K = Cn(H) by p r such that the contraction is determined respectively by P1 and P2 via (C . ). Notice that H is the Horn subset of both P1 and P2. The Entrenchment-Based Horn Contraction rectangles illustrate the formulas in the Horn belief set H and the belief set K along with their entrenchments. Formulas at the same level of a rectangle are equally entrenched. Formulas at a level higher are strictly more entrenched than those in a level lower. Nonbeliefs, tautologies and conjunctions are not shown as their entrenchments are uniquely determined by the formulas shown. The shaded formulas are retained after the contraction. Let s examine the fate of p q in the Horn contraction determined by H via (HC . ). The disjunction of p q and p r (i.e., p q r) has two Horn strengthenings p r and p q. Since the Horn strengthenings are equally or less entrenched than p r, then p q is discarded. In the contractions determined by P1 and P2 via (C . ), since p q r is allowed in the epistemic entrenchments the retention of p q is then determined by the entrenchment of p q r compared to that of p r. Observe that the contraction determined by P1 retains the same Horn formulas as the Horn contraction but that determined by P2 retains more. In Section 5, we identify the entrenchmentbased contraction functions that always retain the same Horn formulas as the corresponding entrenchment-based Horn contraction function. Condition (C ) concerns the generation of an epistemic entrenchment from a contraction function. Its Horn version is used for generating a Horn epistemic entrenchment from a Horn contraction function. It is identical to the (C ) condition but restricted to Horn formulas. (HC ): φ ψ iffφ H . φ ψ or φ ψ. 4.3 Characterisation Before giving the representation theorem for entrenchment-based Horn contraction, let us consider the following postulates. (H . 1) H . φ = Cn H(H . φ) (H . 2) H . φ H (H . 3) If φ H, then H . φ = H (H . 4) If φ, then φ H . φ (H . de) If ψ H and ψ H . φ, then for all χ HS(φ ψ), χ H . φ (H . wr) If ψ H and ψ H . φ, then there is some H such that H . φ H , φ Cn H(H ) and φ Cn H(H {ψ}) (H . 6) If φ ψ, then H . φ = H . ψ (H . f) If φ, then H . φ = H (H . hs) If ψ H . φ, then there is χ HS(φ ψ) such that χ H . φ χ (H . pa) (H . φ) Cn H(φ) H . φ ψ (H . ct) If φ H . φ ψ, then φ H . φ ψ δ Zhuang & Pagnucco (H . 7) H . φ H . ψ H . φ ψ (H . 8) If φ H . φ ψ, then H . φ ψ H . φ Most of these postulates are well known in the belief change literature. (H . 1) (H . 4) and (H . 6) (H . 8) are Horn versions of the AGM postulates Closure, Inclusion, Vacuity, Success, Extensionality, Conjunctive Overlap and Conjunctive Inclusion respectively. (H . f) is the Horn version of the Failure postulate (Fuhrmann & Hansson, 1994). (H . de) is the Horn version of the Disjunctive Elimination postulate (Ferm e, Krevneris, & Reis, 2008):1 (K . de) If ψ K and ψ K . φ, then φ ψ K . φ (K . de) captures the minimal change properties of a contraction; in its contrapositive form If ψ K and φ ψ K . φ, then ψ K . φ the postulate is a condition for a sentence ψ to survive the contraction process (Ferm e et al., 2008, p. 745). Combining some existing results (Ferm e et al., 2008; Hansson, 1991), we get that (K . de) implies (K . 5) in the presence of (K . 2) and (K . 3). The reverse is also true as we can show that the contrapositive of (K . de) follows from Recovery.2 Thus (K . de) is equivalent to (K . 5). (H . de) is obtained from (K . de) by replacing the possibly non-Horn disjunction φ ψ with its Horn strengthenings. It deals with the removal of formulas in regard to the related Horn strengthenings such that, if ψ is removed in contracting φ, then so are all the Horn strengthenings of φ ψ. Interestingly, (H . wr) that is proposed in the work of Delgrande and Wassermann (2010) for characterising partial meet Horn contraction is equivalent to (H . de) in the presence of (H . 2). Also, in the presence of (H . 2), (H . f) follows from (H . de). The Horn Strengthening postulate (H . hs) has no counterpart in classic belief change. For entrenchment-based contraction, if a formula ψ is retained in contracting φ, then ψ φ is strictly more entrenched than φ which means, in accordance with (C ), that φ ψ K . φ (φ ψ). Thus the property can be expressed as: If ψ K . φ, then φ ψ K . φ (φ ψ). The property however does not have to be postulated explicitly as it is deducible from (K . 6) and (K . 1). Since φ (φ ψ) is logically equivalent to φ, by (K . 6) we have K . φ (φ ψ) = K . φ. Then φ ψ K . φ (φ ψ) follows from the fact that ψ K . φ and K . φ is logically closed. For entrenchment-based Horn contraction, if a Horn formula ψ is retained in contracting a Horn formula φ, then there must be a Horn strengthening χ of φ ψ that is strictly more entrenched than φ which means, in accordance with (HC ), that χ H . φ χ. Such property is captured exactly by (H . hs). This time the property is not deducible from other postulates thus we postulate it explicitly. Notice that (H . hs) is in fact the Horn adaptation of the above retention property for the classic case by replacing the disjunction φ ψ with its Horn strengthenings. 1. Disjunctive Elimination was originally proposed in the context of belief base change. It is adapted to belief set change here. 2. If ψ is in K, then Recovery ensures that φ ψ is in K . φ. Hence if φ ψ is also in K . φ, we have ψ K . φ. Entrenchment-Based Horn Contraction (H . ct) and (H . pa) are Horn versions of Conjunctive Trisection and Partial Antitony. As in the classical case, (H . pa) and (H . ct) are equivalent in the presence of (H . 6). (K . pa) and (K . 7) are equivalent. Since the proof relies on Recovery which is not available for Horn logic, we can not establish equivalence between their Horn analogues (H . pa) and (H . 7). Proposition 1 summarises some connections between the postulates. Proposition 1 Let . be a contraction function. Then: 1. if . satisfies (H . 1) and (H . de), then it satisfies (H . f); 2. if . satisfies (H . 2) and (H . de), then it satisfies (H . wr); 3. if . satisfies (H . wr), then it satisfies (H . de); 4. if . satisfies (H . pa), then it satisfies (H . ct); and, 5. if . satisfies (H . 6) and (H . ct), then it satisfies (H . pa). Now, we give the representation theorem for entrenchment-based Horn contraction. Theorem 2 A function . is an entrenchment-based Horn contraction function iffit satisfies (H . 1) (H . 4), (H . de), (H . 6), (H . hs), (H . ct), and (H . 8). Comparing with the characterisation for entrenchment-based contraction, Recovery and Conjunctive Overlap do not appear and instead (H . de), (H . hs), and (H . ct) are used. Let s go through the new postulates. The condition of decomposability that is proposed in the work of Flouris, Plexousakis, and Antoniou (2004) characterises the logics that admit contraction functions that satisfy Recovery. Langlois, Sloan, Sz or enyi, and Tur an (2008) verified that Horn logic is not decomposable, thus there is no Horn contraction function that satisfies Recovery. Here, (H . de) plays a similar role to Recovery for capturing the minimal change property of entrenchment-based Horn contraction. As just mentioned, (H . 7) and (H . ct) are not equivalent in the Horn case. It turns out that instead of (H . 7), it is the property (H . ct) that is needed for characterising entrenchment-based Horn contraction. Since (HC . ) is, in a sense, stricter than (C . ), we need (H . hs) to capture this extra strictness of entrenchment-based Horn contraction. Besides the characterising postulates, we can show that entrenchment-based Horn contraction functions satisfy (H . 7). Proposition 2 If . is an entrenchment-based Horn contraction function, then it satisfies (H . 7). By Theorem 2, (H . 1) (H . 4), (H . de), (H . 6), (H . hs), (H . ct), and (H . 8) characterise entrenchment-based Horn contraction functions. Thus it follows immediately from Proposition 2 that (H . 7) follows from these postulates. Corollary 1 Let . be a Horn contraction function. If . satisfies (H . 1) (H . 4), (H . de), (H . 6), (H . hs), (H . ct), and (H . 8), then it satisfies (H . 7). Zhuang & Pagnucco Besides the representation results, another property of entrenchment-based Horn contraction that deserves mentioning is its uniqueness . Each Horn epistemic entrenchment determines a unique entrenchment-based Horn contraction function. Specifically, given any two distinct Horn epistemic entrenchments 1 and 2 for H and the two entrenchmentbased Horn contraction functions they determine . 1 and . 2, there is a formula φ such that H . 1φ = H . 2φ. Theorem 3 Let 1 and 2 be two different Horn epistemic entrenchments and let . 1 and . 2 be entrenchment-based Horn contraction functions that are determined by 1 and 2 respectively via condition (HC . ). Then . 1 and . 2 are not identical. Uniqueness is a property of AGM contraction. It is shown in (Alchourr on et al., 1985) that, in the finite case, each selection function determines a unique partial meet contraction function (OBSERVATION 4.6). This is a desirable property which captures the intuition that two agents with different preferences over a certain domain will have different contraction outcomes. Notice that uniqueness is not an immediate property of Horn contraction and revision. In fact, most of the existing Horn contractions and Horn revisions do not enjoy the property, for instance the transitively relational partial meet Horn contraction (Zhuang & Pagnucco, 2011), the model-based Horn contraction (Zhuang & Pagnucco, 2012), and the model-based Horn revision (Delgrande & Peppas, 2011). 5. Connections with Entrenchment-Based Contraction We have seen how entrenchment-based contraction is adapted naturally to Horn logic, which results in entrenchment-based Horn contraction. But how well does entrenchment-based Horn contraction perform in comparison to its classic counterpart? In this section, we introduce the notion of Horn equivalence through which Horn contraction can be compared with AGM contraction. A properly defined Horn contraction should be as rational as AGM contraction. Horn contraction is more restrictive than AGM contraction as it deals only with Horn formulas. It is then reasonable to consider only Horn formulas in comparing Horn contraction with AGM contraction. And we claim that a Horn contraction is as rational as an AGM one if they perform identically in terms of Horn formulas. This forms the intuition behind Horn equivalence. In evaluating the possible equivalence between two contraction functions, it makes sense to start with an identical belief set and check the effect of the two functions in contracting the same formula. With this intuition and the fact that a Horn contraction function only permits Horn formulas, Horn equivalence is defined for pairs of AGM contraction function . for a belief set K and Horn contraction function . H for a Horn belief set H such that H is the Horn subset of K. Consider the set of Horn formulas in the resulting belief set of . in contracting a Horn formula, if the same set can be returned by the Horn contraction function . H in contracting the same Horn formula, then we say . H and . are Horn equivalent. Definition 5 Let K be a belief set and H a Horn belief set such that H = H(K). Let . be an AGM contraction function for K and . H a Horn contraction function for H. Then Entrenchment-Based Horn Contraction . H and . are Horn equivalent iff H(K . φ) = H . Hφ for all φ LH. As depicted in Figure 2, the Horn equivalence between . and . H stems from the fact that, in contracting any Horn formula φ, the Horn belief set H . Hφ returned by . H is the Horn subset of the belief set K . φ returned by . . H(K) H(K . φ) Figure 2: Horn equivalence between the AGM contraction function . and the Horn contraction function . H. Obviously, for an entrenchment-based Horn contraction function to be Horn equivalent to an entrenchment-based contraction function, the determining Horn epistemic entrenchment must be the Horn subset of the determining epistemic entrenchment. However, this is not sufficient to guarantee Horn equivalence. As shown in Figure 1, although the Horn epistemic entrenchment H is the Horn subset of the epistemic entrenchment P2, the entrenchment-based contraction function determined by P2 retains more Horn formulas than the entrenchment-based Horn contraction function determined by H. In Figure 1, Horn formulas are equally entrenched in H, P1 and P2. However, the non-Horn formula p q r, which is not allowed in H, is entrenched differently in P1 and P2. With the extra preference information on the non-Horn formula, P1 and P2 give rise to two different entrenchment-based contraction functions. The point is that a Horn epistemic entrenchment is consistent with several epistemic entrenchments (i.e., being their Horn subset), thus an entrenchment-based Horn contraction function corresponds to several entrenchment-based contraction functions. But which entrenchment-based contraction functions are Horn equivalent to the entrenchment-based Horn contraction function? Essentially, this requires us to identify the epistemic entrenchments that will determine the Horn equivalent entrenchment-based contraction functions. As we will show, the following is a necessary and sufficient condition for this purpose: (EE6) For φ, ψ LH if φ, ψ K and φ < φ ψ then there is χ HS(φ ψ) such that φ < χ. The condition requires that, for all pairs of Horn formulas φ, ψ in K, if φ is strictly less entrenched than φ ψ, then it is also strictly less entrenched than a Horn strengthening Zhuang & Pagnucco of φ ψ. Since a formula is entailed by any of its Horn strengthenings, it can be verified through (EE1) and (EE2) that the converse is also true. Thus φ is strictly less entrenched than φ ψ if and only if φ is strictly less entrenched than a Horn strengthening of φ ψ. In the principal cases, to decide whether to retain ψ in the contraction by φ, (C . ) compares the entrenchment between φ ψ and φ whereas (HC . ) compares the entrenchment between the Horn strengthenings of φ ψ and φ. (EE6) assures that comparing φ ψ and φ is the same as comparing Horn strengthenings of φ ψ and φ. This means, if the entrenchment satisfies (EE6), then the mechanism for retaining formulas for (C . ) is essentially the same as that for (HC . ). We call entrenchment-based contraction functions whose determining epistemic entrenchments satisfy (EE6) strict entrenchment-based contraction functions. Definition 6 A function . is a strict entrenchment-based contraction function if it is an entrenchment-based contraction function whose determining epistemic entrenchment satisfies (EE6). To characterise strict entrenchment-based contraction functions we need, in addition to (K . 1) (K . 8), the classic case of (H . hs): (K . hs) For φ, ψ LH, if ψ K . φ then there is χ HS(φ ψ) such that χ K . φ χ. In fact, (EE6) corresponds exactly to (K . hs). Theorem 4 A function . is a strict entrenchment-based contraction function iff. satisfies (K . 1) (K . 8) and (K . hs). As the main result of this section, each entrenchment-based Horn contraction function is Horn equivalent to a strict entrenchment-based contraction function and vice versa. Theorem 5 If . H is an entrenchment-based Horn contraction function, then there is a strict entrenchment-based contraction function . such that . H and . are Horn equivalent. If . is a strict entrenchment-based contraction function, then there is an entrenchmentbased Horn contraction function . H such that . H and . are Horn equivalent. Moreover, any entrenchment-based contraction function that is Horn equivalent to an entrenchment-based Horn contraction function is a strict entrenchment-based contraction function. Theorem 6 Let . H be an entrenchment-based Horn contraction function. If . is an entrenchment-based contraction function such that . H and . are Horn equivalent, then . is a strict entrenchment-based contraction function. Horn equivalence is a local feature which deals with the equivalence between specific contraction functions. A number of functions can be constructed according to a particular construction method and each contraction function represents a possible way of contracting a formula. Thus we can also compare Horn contraction with AGM contraction in terms of the possible ways of contracting a formula. A Horn contraction is as comprehensive as AGM contraction if the Horn contraction permits all possible ways of contracting a Horn Entrenchment-Based Horn Contraction formula as the AGM does. Due to the allowance of non-Horn formulas, there are more ways of forming epistemic entrenchments than Horn epistemic entrenchment; thus more ways of generating entrenchment-based contraction functions. In Figure 1 there is no entrenchmentbased Horn contraction function that corresponds to (i.e., being Horn equivalent to) the entrenchment-based contraction function determined by P2. Entrenchment-based Horn contraction is therefore not as comprehensive as entrenchment-based contraction. However, this is not due to how the Horn contraction is defined but due to the limited expressiveness of Horn logic compared to that of Propositional Logic. Entrenchment-based Horn contraction is equally comprehensive to strict entrenchment-based contraction. 6. Entrenchment-Based Horn Withdrawal Due to the controversy over the Recovery postulate in the AGM setting, Makinson (1987) proposed an operation called withdrawal that satisfies five of the basic AGM contraction postulates but not necessarily Recovery. Since Horn contraction is intrinsically incompatible with Recovery, it makes sense to explore the Horn version of withdrawal. Since our Horn contraction originates from entrenchment-based contraction, we focus on the withdrawal version of entrenchment-based contraction. Such withdrawal has been characterised by Rott and Pagnucco (1999) and referred to as severe withdrawal. For uniformity, we call it entrenchment-based withdrawal. An epistemic entrenchment is also assumed for entrenchment-based withdrawal and the withdrawal outcome is determined by the following condition: (W . ) : ψ K . φ iffψ K and either φ < ψ or φ. Definition 7 (Rott & Pagnucco, 1999) A function . is an entrenchment-based withdrawal function for K iffits outcome is determined by the epistemic entrenchment for K via (W . ). Notice that (W . ) can also be used to generate an epistemic entrenchment from a withdrawal function as, on the reverse reading, ψ is strictly more entrenched than φ whenever ψ is retained in the withdrawal by φ. Rott and Pagnucco (1999) showed that to characterise entrenchment-based withdrawal we need the full set of AGM contraction postulates except Recovery and we also need to replace Conjunctive Overlap with the much stronger Antitony Condition. Theorem 7 (Rott & Pagnucco, 1999) A function . is an entrenchment-based withdrawal function iff. satisfies the following postulates: (K . 1) (K . 4), (K . 6), (K . 8), and (K . 7a) If φ, then K . φ K . φ ψ (Antitony Condition) Adapting entrenchment-based withdrawal to Horn logic is straightforward as everything is Horn expressible. We obviously need a Horn epistemic entrenchment. By restricting to Horn belief sets and Horn formulas (W . ) is recast as follows: (HW . ) : ψ H . φ iffψ H and either φ < ψ or φ. The Horn withdrawal function generated via (HW . ) is referred to as an entrenchment-based Horn withdrawal function. Zhuang & Pagnucco Definition 8 A function . is an entrenchment-based Horn withdrawal function for H iff its outcome is determined by the Horn epistemic entrenchment for H via (HW . ). It is obvious from the constructions that, unlike entrenchment-based Horn contraction, entrenchment-based Horn withdrawal has the same change mechanism as that of its origin. Therefore, entrenchment-based Horn withdrawal is characterised by exactly Horn versions of the characterising postulates for entrenchment-based withdrawal. Theorem 8 A function . is an entrenchment-based Horn withdrawal function iff. satisfies the following postulates: (H . 1) (H . 4), (H . 6), (H . 8), and (H . 7a) If φ then H . φ H . φ ψ. We can show that entrenchment-based Horn withdrawal and entrenchment-based withdrawal have a one-to-one correspondence under the notion of Horn equivalence. Theorem 9 If . H is an entrenchment-based Horn withdrawal function, then there is an entrenchment-based withdrawal function . such that . H and . are Horn equivalent. If . is an entrenchment-based withdrawal function, then there is an entrenchment-based Horn withdrawal function . H such that . H and . are Horn equivalent. 7. Related Work Most of the existing approaches to Horn contraction are different Horn variants of partial meet contraction (Alchourr on et al., 1985). The notion of remainder sets is central to the construction of partial meet contraction where the outcome of the contraction is the intersection of some candidate remainder sets chosen by a selection function. In the standard definition, a remainder set of K with respect to φ is a maximal subset of K that fails to imply φ. The maximal nature implies the following model-theoretic behaviour of remainder sets (e.g., see G ardenfors 1998, p. 86). The set of models of each remainder set for φ is the union of the set of models of K and a model of φ. Furthermore, there is a bijection between the remainder sets for φ and the models of φ. Another property which is often referred to as the convexity property states that any belief set that is a subset of the outcome of a maxichoice contraction and a superset of the outcome of full meet contraction is the outcome of some partial meet contraction. The above properties and behaviours are however mutually exclusive for remainder sets under Horn logic, which gives rise to three Horn variants of remainder sets thus three Horn variants of partial meet contraction. To avoid confusion, remainder sets under Propositional Logic will be referred to as classic remainder sets. The first work on Horn contraction is by Delgrande (2008). In his seminal paper, Delgrande studied the Horn analogue of orderly maxichoice contraction (G ardenfors, 1988) which we term as orderly maxichoice Horn contraction. Here the remainder sets are defined as in the standard definition which means they are maximal, thus we call it a maximal remainder set. As in orderly maxichoice contraction, a transitive and antisymmetric relation over maximal remainder sets is assumed for selecting the single best remainder set as the contraction outcome. Entrenchment-Based Horn Contraction Booth, Meyer, and Varzinczak (2009) suggested that, while orderly maxichoice Horn contractions are appropriate choices for Horn contraction, they do not constitute all the appropriate forms of Horn contraction. The authors argued that a Horn contraction should satisfy the convexity property. As they demonstrated, this is not the case for Horn contractions based on maximal remainder sets. They proposed infra Horn contraction (Booth, Meyer, Varzinczak, & Wassermann, 2010, 2011). Infra Horn contraction is based on the notion of infra remainder set. The set of infra remainder sets of H with respect to a Horn formula φ consist of any Horn belief set that is the subset of a maximal remainder set for φ and the superset of the intersection of all maximal remainder sets for φ. The notion of infra remainder set subsumes that of maximal remainder set as each maximal remainder set is an infra one but not vice versa. As noticed by Delgrande and Wassermann (2010, 2013), both maximal and infra remainder sets do not exhibit the model-theoretic behaviour of classic remainder sets. They therefore give another Horn variant called partial meet Horn contraction. It is based on the notion of a weak remainder set which is defined to behave as classic remainder sets model-theoretically. They show that weak remainder sets subsume maximal remainder sets but weak remainder sets and infra remainder sets do not subsume one another. Thus partial meet Horn contraction and infra Horn contraction are not more comprehensive than one another. The nice thing about weak remainder sets is that they have a one-to-one correspondence with classic remainder sets which implies a one-to-one correspondence between partial meet Horn contraction and partial meet contraction. This means the contractions permitted by partial meet Horn contraction correspond exactly to those permitted by partial meet contraction. Zhuang and Pagnucco (2011) further studied partial meet Horn contraction by assuming a preorder over weak remainder sets. This results in the construction of transitively relational partial meet Horn contraction which is the Horn analogue of transitively relational partial meet contraction (Alchourr on et al., 1985). Apart from partial meet contraction, Zhuang and Pagnucco (2012) studied the Horn analogue of model-based contraction (Katsuno & Mendelzon, 1992) which is called modelbased Horn contraction. As in the classic case (Katsuno & Mendelzon, 1992), a pre-order over interpretations is assumed. It is shown that model-based Horn contraction is identical to transitively relational partial meet contraction. Partial meet Horn contraction and infra Horn contraction differ from entrenchmentbased Horn contraction in that they do not assume any explicit preference information. Zhuang and Pagnucco (2012) showed that entrenchment-based Horn contraction is a restricted form of model-based Horn contraction thus a restricted form of transitively relational partial meet Horn contraction and partial meet Horn contraction. No exact relationship can be established between entrenchment-based Horn contraction and infra Horn contraction as (H . hs) is incompatible with infra Horn contraction and one of the characterising postulate of infra Horn contraction (i.e., Core-Retainment) is incompatible with entrenchment-based Horn contraction. For similar reasons no exact relationship can be established between entrenchment-based Horn contraction and orderly maxichoice Horn contraction. As shown in Section 5, entrenchment-based Horn contraction is not as comprehensive as entrenchment-based contraction. In this respect, partial meet Horn contraction and transitively relational partial meet Horn contraction outperform entrenchment-based Horn Zhuang & Pagnucco contraction as bijections exist between partial meet Horn contractions and partial meet contractions and between transitively relational partial meet Horn contraction and transitively relational partial meet contraction. However, the bijection comes at a price. Zhuang and Pagnucco (2011) showed that Horn logic is not expressive enough for Horn contraction to distinguish some different pre-orders of weak remainder sets. These different pre-orders may generate identical transitively relational partial meet Horn contraction functions. The observation which is termed loss of uniqueness is counterintuitive as it means that although two agents who have different preferences over a certain domain, they always end up with identical contraction outcomes. Entrenchment-based Horn contraction does not suffer from this problem. Each Horn epistemic entrenchment determines a unique entrenchment-based Horn contraction. Beside the aforementioned works on Horn contractions, Delgrande and Peppas (2011) studied model-based Horn revision in the manner of the classic model-based revision (Katsuno & Mendelzon, 1992). In the AGM setting, revision can be defined from contraction via the so called Levi identity (Levi, 1991). Zhuang, Pagnucco, and Zhang (2013) explored this connection in the Horn setting and showed that, under proper restrictions, Horn revision can be defined from Horn contraction via a variant of the Levi identity. They also showed that the Horn revision functions generated from transitively relational partial meet Horn contraction functions and from model-based Horn contraction functions suffer from counter-intuitive results whereas the one generated from entrenchment-based Horn contraction functions are guaranteed to be meaningful (i.e., satisfies all the revision postulates proposed in Delgrande & Peppas, 2011). Finally, Adaricheva, Sloan, and Sz or enyi (2012) provided some complexity results regarding Horn contractions. By now all the major construction methods of AGM contraction have been adapted to Horn logic. The principle of such adaptations is to make the adapted contraction as close as possible to AGM contraction (i.e., equally rational in all aspects). As we explained above, due to the limited expressiveness of Horn logic, none of the adapted contractions is identical to its AGM origin in all aspects. However, this is by no means declaring failure on the adaptations for we have emphasised in Section 5 that it is fair to expect the rationality of Horn contractions only to the extent the expressiveness of Horn logic permits. Since the adaptations focus on different aspects of AGM contraction and they often exhibit both desirable and undesirable properties, it is not convincing to argue that one outperforms the other. The best choice of Horn contraction then depends on the actual application. If explicit preference is expected and loss of uniqueness is to be avoided then entrenchmentbased Horn contraction is a better choice. 8. Conclusion In this paper, we defined entrenchment-based Horn contraction which is the Horn analogue of entrenchment-based contraction. The outcome of the Horn contraction is determined by epistemic entrenchments over Horn formulas via a refinement of the condition (C . ) proposed by G ardenfors and Makinson (1988). Since condition (C . ) involves arbitrary disjunctions which may not be Horn formulas, the refined condition (HC . ) considers the Horn strengthenings of the disjunctions. (HC . ) closely resembles (C . ), as each entrenchment-based Horn contraction function performs identically to its classic coun- Entrenchment-Based Horn Contraction terpart (i.e., strict entrenchment-based contraction function) if only Horn formulas are counted. Since non-Horn formulas are disallowed, the set of epistemic entrenchments for determining entrenchment-based Horn contraction is a proper subset of those for determining entrenchment-based contraction. Entrenchment-based Horn contraction is therefore not as comprehensive as entrenchment-based contraction. We are able to identify a restricted form of entrenchment-based contraction called strict entrenchment-based contraction which has a one-to-one correspondence with entrenchment-based Horn contraction. Recently, Creignou, Papini, Pichler, and Woltran (2014) investigated revision operators for fragments of Propositional Logic not limited to Horn. Their work promotes a new direction for furthering the study on Horn belief change. Of the many Horn contractions and revisions, it is important to find out if their adaptation strategies are generalisable to fragments of Propositional Logic other than Horn. Thus for future work, we aim to develop a generalised entrenchment-based contraction that can be applied to arbitrary fragments of Propositional Logic. Appendix A. Proofs of Results We first present some notions and properties of Horn logic that will be used in the proofs. The intersection of two interpretations is the interpretation that assigns true to those atoms that are assigned true by both interpretations. We denote the intersection of interpretations µ and ν by µ ν. Given a set of interpretations M, the closure of M under intersection is denoted by Cl (M). Formally, Cl (M) = {ω | ω M or there is µ, ν M such that µ ν = ω}. For any Horn formula, its set of models is closed under Cl and called Horn closed. Conversely, any Horn closed set of models corresponds to an unique Horn formula (modulo logical equivalence). Moreover, intersections of Horn closed sets of models are also Horn closed. Lemma 1 If φ ψ, then HS(φ) = HS(ψ). Proof: The result is immediate as the definition of Horn strengthening is syntax insensitive. Lemma 2 If ψ is a Horn formula such that ψ φ, then there is χ HS(φ) such that ψ χ. Proof: If ψ HS(φ), then the result trivially holds. Suppose ψ HS(φ), then by the definition of Horn strengthening there is χ1 LH such that |ψ| |χ1| |φ|. Again, if χ1 HS(φ), then there must be χ2 LH such that |χ1| |χ2| |φ|. Since |φ| is finite, eventually we will find a χn which is a Horn strengthening of φ. Since |ψ| |χn|, ψ χn. Lemma 3 If χ HS(φ ψ), then there is χ1 HS(φ) and χ2 HS(ψ) such that χ χ1 χ2. Proof: Suppose χ HS(φ ψ), then by the definition of Horn strengthening |χ| |φ| |ψ| which implies |χ| |φ| and |χ| |ψ|. Then it follows from Lemma 2 that there are χ1 HS(φ) and χ2 HS(ψ) such that |χ| |χ1| and |χ| |χ2|, thus |χ| |χ1| |χ2|. Zhuang & Pagnucco Assume there is µ |χ1| |χ2| such that µ |χ|. Then since |χ1| |χ2| |φ| |ψ| we have µ |φ| |ψ|. It then follows from χ HS(φ ψ), µ |φ| |ψ|, and µ |χ| that there is ν |χ| such that µ ν |φ| |ψ|. Now since µ, ν |χ1| |χ2| we have µ ν |χ1| |χ2| which implies µ ν |φ| |ψ|, a contradiction! Therefore, there is no µ |χ1| |χ2| such that µ |χ| which implies |χ1| |χ2| |χ|. Lemma 4 Let ψ and φ be Horn formulas. If χ HS(φ ψ), then HS(φ χ) HS(φ ψ). Proof: Suppose χ HS(φ ψ) and χ HS(φ χ), we need to show χ HS(φ ψ). By the definition of Horn strengthening, χ HS(φ ψ) implies |χ| |φ ψ|, and χ HS(φ χ) implies |χ | |φ χ|. It then follows from |φ| |φ ψ| and |χ| |φ ψ| that |φ χ| |φ ψ| which implies |χ | |φ ψ|. It remains to show there is no Horn formula χ such that |χ | |χ | |φ ψ|. Assume to the contrary that there is Horn formula χ such that |χ | |χ | |φ ψ|. It follows from |χ | |χ |, χ HS(φ χ), and the definition of Horn strengthening that |χ | |φ χ|. By set theory there is ν |χ |\|χ | such that ν |ψ|\|φ χ|. It then follows from ν |χ| and χ HS(φ ψ) that there is µ |χ| such that µ ν = ω and ω |φ ψ|. We also have µ |ψ| for otherwise |ψ| = Cl (|ψ|) and this implies µ |φ|. Assume µ |χ | then there is x |φ χ| such that µ x = y and y |φ χ|. If x |φ| then |φ| = Cl (|φ|), a contradiction! If x |χ|, then |χ| = Cl (|χ|), again a contradiction! Thus we conclude µ |χ | which implies µ |χ |. It then follows from ν |χ |, µ ν = ω and ω |φ ψ| that |χ | = Cl (|χ |), a contradiction! Thus there is no χ such that |χ | |χ | |φ ψ|. Lemma 5 Let be a Horn epistemic entrenchment. Then satisfies: 1. φ ψ or ψ φ 2. If ψ χ φ, then ψ φ or χ φ 3. φ < ψ iffφ ψ < ψ. 4. If χ φ and χ ψ, then χ φ ψ 5. If χ < φ and χ < ψ, then χ < φ ψ 6. If φ ψ, then φ φ ψ 7. If φ ψ then φ ψ and ψ φ Proof: The proofs are identical to the propositional case. Proposition 1 Let . be a Horn contraction function. Then 1. if . satisfies (H . 1) and (H . de), then it satisfies (H . f) 2. if . satisfies (H . 2) and (H . de), then it satisfies (H . wr) 3. if . satisfies (H . wr), then it satisfies (H . de) 4. if . satisfies (H . pa), then it satisfies (H . ct) Entrenchment-Based Horn Contraction 5. if . satisfies (H . 6) and (H . ct), then it satisfies (H . pa) Proof: 1. Suppose φ. For each ψ H, we have φ ψ which implies HS(φ ψ) = φ ψ. Since H . φ = Cn H(H . φ), all tautologies are in H . φ. Thus φ ψ H . φ. It then follows from the contrapositive of (H . de), ψ H, and φ ψ H . φ that ψ H . φ. Thus H . φ = H. 2. & 3. We will show that (H . wr) and (H . de) are equivalent to the following postulate: (H . mc) If ψ H \ H . φ then |H . φ| |φ ψ|. We first show that . satisfies (H . de) iffit satisfies (H . mc). For one direction, suppose . satisfies (H . de). Let ψ H \ H . φ. We have two cases: Case 1, φ ψ LH: Then HS(φ ψ) = {φ ψ}. By (H . de) we have H . φ φ ψ which implies |H . φ| |φ ψ|. Case 2, φ ψ LH: Assume |H . φ| |φ ψ|. By Lemma 2, there is a χ HS(φ ψ) such that H . φ χ. However, it follows from (H . de) that H . φ χ for all χ HS(φ ψ), a contradiction! For the other direction, suppose . satisfies (H . mc). Since |H . φ| |φ ψ|, there is µ |H . φ| such that µ |φ ψ|. Since |χ| |φ ψ| for all χ HS(φ ψ), µ |χ| for all χ HS(φ ψ). Then by model theory, it follows from µ |H . φ| that H . φ χ for all χ HS(φ ψ). Now we show that . satisfies (H . wr) iffit satisfies (H . mc). For one direction, suppose . satisfies (H . wr). Let ψ H \ H . φ. Assume |H . φ| |φ ψ| then by set theory |H . φ| | φ| |ψ|. Again by set theory, for all H such that |H | |H . φ| and |H | | φ| = , it follows from |H . φ| | φ| |ψ| that there is µ |H | |ψ| such that µ | φ| which implies H {ψ} φ. However, by (H . wr) there is one such H that H {ψ} φ, a contradiction! For the other direction, suppose . satisfies (H . mc). Let ψ H \ H . φ. Then by (H . mc) there is µ |H . φ| | φ| such that µ |ψ|. Let a Horn belief set H be such that |H | = {µ}. Then µ |H . φ| implies |H | |H . φ| and µ | φ| implies |H | | φ|. It follows from |H | |H . φ| and |H | | φ| that H . φ H and H φ. It follows from |H | = {µ} and µ |ψ| that |H | |ψ| = . Thus H {ψ} is inconsistent. All formulas follow from an inconsistent set so does φ. 4. & 5. The proofs are identical to the propositional case which can be found on Page 117 of (Hansson, 1999) (OBSERVATION 2.59). Theorem 2 A function . is an entrenchment-based Horn contraction function iffit satisfies (H . 1) (H . 4), (H . de), (H . 6), (H . hs), (H . ct), and (H . 8). Proof: For one direction, let H be a Horn belief set, a Horn epistemic entrenchment for H, and . be the entrenchment-based Horn contraction function for H that is determined by . We need to show . satisfies (H . 1) (H . 4), (H . de), (H . hs), (H . ct), and (H . 8). (H . 2): Follows directly from (HC . ). (H . 1): If φ, then it follows from (HC . ) that H . φ = H. It then follows from H = Cn H(H) that H . φ = Cn H(H . φ). Suppose φ and ψ Cn H(H . φ), we need to show ψ (H . φ). By (HC . ), it suffices to show ψ H and there is χ HS(φ ψ) such that φ < χ. We have two cases: Zhuang & Pagnucco Case 1, ψ: Since ψ Cn H(H . φ), by compactness of Horn logic, there is a finite subset {δ1, . . . , δn} of H . φ such that δ1 δn ψ. Since {δ1, . . . , δn} H . φ, it follows from (H . 2) that {δ1, . . . , δn} H. It follows from {δ1, . . . , δn} H and δ1 δn ψ that H φ. It follows from H φ and H = Cn H(H) that ψ H. It follows from (HC . ) that there is χi HS(φ δi) such that φ < χi for each δi. It then follows from Lemma 5 (Part 5) that φ < χ1 χn. Since χ1 χn (φ δ1) (φ δn) we have by Lemma 2 that there is χ HS((φ δ1) (φ δn)) such that χ1 χn χ. Thus φ < χ. Since (φ δ1) (φ δn) φ (δ1 δn), we have by Lemma 1, that HS((φ δ1) (φ δn)) = HS(φ (δ1 δn)). Thus χ HS(φ (δ1 δn)). Since φ (δ1 δn) φ ψ, we have χ φ ψ which implies by Lemma 2 that there is χ HS(φ ψ) such that χ χ which implies χ χ . Since φ < χ it follows from (HEE1) that φ < χ . By (HC . ), it follows from ψ H, and φ < χ that ψ H . φ. Case 2, ψ: Then it follows from H = Cn H(H) that ψ H. Also ψ implies φ ψ. Thus by (HEE2) and (HEE5), δ φ ψ for all δ. Since φ, it follows from Lemma 5 (Part 1) and (HEE5) that there is a δ such that φ < δ. Then by (HEE1), it follows from δ φ ψ and φ < δ that φ < φ ψ. By the definition of Horn strengthening, φ ψ implies HS(φ ψ) = {φ ψ}. By (HC . ), it then follows from ψ H and φ < φ ψ that ψ H . φ. (H . 3): Suppose φ H, we need to show H . φ = H. H . φ H follows from (H . 2). Let ψ H. It suffices to show ψ H . φ. By (HEE4) and Lemma 5 (Part 1), it follows from ψ H that there is some δ LH such that δ < ψ. Since ψ φ ψ we have by Lemma 2 that there is χ HS(φ ψ) such that ψ χ. It follows from ψ χ, by (HEE2), that ψ χ. Since φ H, it follows from (HEE4) that φ δ. We can now apply (HEE1) to φ δ, δ < ψ, ψ χ, and obtain φ < χ. By (HC . ), it follows from ψ H and φ < χ that ψ H . φ. (H . 4): Suppose φ. We need to show φ H . φ. By (HEE2), φ φ implies φ φ. By Lemma 5 (Part 1), φ φ implies φ < φ. Since HS(φ φ) = HS(φ) = {φ}, it follows from φ < φ and φ, by (HC . ), that φ H . φ. (H . 6): Suppose φ ψ. We first show H . φ H . ψ. Let δ H . φ. It then follows from (HC . ) that δ H and either φ or there is χ HS(φ δ) such that φ < χ. Case 1, φ: Since φ ψ, φ implies ψ. It follows from ψ and δ H, by (HC . ), that δ H . ψ. Case 2, φ: Then there is χ HS(φ δ) such that φ < χ. Since φ ψ, we have φ δ ψ δ. By Lemma 1, φ δ ψ δ implies HS(φ δ) = HS(ψ δ). Thus χ HS(ψ δ) follows from χ HS(φ δ). By intersubstitutativity of , ψ < χ follows from φ ψ and φ < χ. It then follows from δ H and ψ < χ, by (HC . ), that δ H . ψ. Thus H . φ H . ψ. We can show H . ψ H . φ in the same way. (H . de): Suppose ψ H \ H . φ. We need to show for all χ HS(φ ψ), χ H . φ. It follows from (HC . ) and ψ H . φ that for all χ HS(φ ψ), φ < χ. By Lemma 4, we have for all χ HS(φ ψ), HS(φ χ) HS(φ ψ). Thus we have for all χ HS(φ χ), φ < χ . It then follows from (HC . ) that for all χ HS(φ ψ), χ H . φ. (HC ): For one direction, suppose φ ψ and φ H . φ ψ. We need to show φ ψ. Since φ H . φ ψ we have by (HC . ) that φ H and either φ ψ or there is χ HS((φ ψ) φ) such that φ ψ < χ. Since (φ ψ) φ φ, we have by Lemma 1 Entrenchment-Based Horn Contraction that HS((φ ψ) φ) = HS(φ) = {φ}. By Lemma 5 (Part 6), φ ψ implies φ φ ψ. By connectivity of , φ φ ψ implies φ ψ < φ. Thus it must be the case that φ ψ. For the other direction, suppose either φ H . φ ψ or φ ψ, we need to show φ ψ. If φ ψ, then we have ψ and it follows from (HEE2) and φ ψ that φ ψ. So suppose φ ψ and φ H . φ ψ. It then follows from (HC . ) that either φ H or for all χ HS((φ ψ) φ), φ ψ < χ. In the former case, φ H gives us φ ψ as required by (HEE4). In the latter case, since (φ ψ) φ φ, we have by Lemma 1, that HS((φ ψ) φ) = HS(φ) = {φ}. Thus φ ψ < φ. By the connectivity of , φ ψ < φ implies φ φ ψ. It follows from (HEE2) and φ ψ ψ that φ ψ ψ. It follows from φ φ ψ, φ ψ ψ and (HEE1) that φ ψ. (H . hs): Suppose ψ H . φ. We need to show there is χ HS(φ ψ) such that χ H . φ χ. It follows from ψ H . φ and (HC . ) that there is χ HS(φ ψ) such that φ < χ. Since . satisfies (HC ), it then follows from φ < χ that χ H . φ χ. (H . ct): Suppose ψ H . φ ψ, we need to show ψ H . φ ψ δ. By (HC ), ψ H . φ ψ implies φ < ψ. It follows from (HEE2) and φ δ φ that φ δ φ. It follows from (HEE1), φ δ φ, and φ < ψ that φ δ < ψ. By (HC ), φ δ < ψ implies ψ H . φ ψ δ. (H . 8): Suppose φ H . φ ψ. We need to show H . φ ψ H . φ. If φ H then we have by (H . 3) that H . φ = H. H . φ ψ H . φ then follows from (H . 2). So suppose φ H. By (HC ), φ H . φ ψ implies φ ψ. By Lemma 5 (Part 6), φ ψ implies φ φ ψ. Let δ H . φ ψ, it suffices to show δ H . φ. It follows from δ H . φ ψ and (HC . ) that there is χ HS((φ ψ) δ) such that φ ψ < χ. By Lemma 1, (φ ψ) δ (φ δ) (ψ δ) implies HS((φ ψ) δ) = HS((φ δ) (ψ δ)). Thus by Lemma 3, there are χ1 HS(φ δ) and χ2 HS(ψ δ) such that χ1 χ2 χ. Then by Lemma 5 (Part 7), φ ψ < χ1 χ2. It follows from (HEE2) and χ1 χ2 χ1 that χ1 χ2 χ1. It follows from (HEE1), φ φ ψ, φ ψ < χ1 χ2, and χ1 χ2 χ1 that φ < χ1. It follows from χ1 HS(φ δ) and φ < χ1, by (HC . ), that δ H . φ. For the other direction, let H be a Horn belief set and . a Horn contraction function for H that satisfies (H . 1) (H . 4), (H . de), (H . hs), (H . ct), and (H . 8). It suffices to show the Horn epistemic entrenchment determined by (HC ) satisfies (HEE1) (HEE5) and (HC . ). By replacing the AGM contraction postulates with their corresponding Horn analogues, the proof for satisfaction of (HEE1) (HEE5) is the same as that of Theorem 2.50 in (Hansson, 1999). We therefore only give the proof for (HC . ). (HC . ): For one direction, suppose ψ H . φ. We need to show ψ H and either φ or there is χ HS(φ ψ) such that φ < χ. Since ψ H . φ, we have by (H . hs) that there is χ HS(φ ψ) such that χ H . φ χ. By (HC ), χ H . φ χ implies φ < χ. By (H . 2), ψ H . φ implies ψ H. For the other direction, suppose ψ H and either φ or there is χ HS(φ ψ) such that φ < χ. We need to show ψ H . φ. If φ then H . φ = H. Thus ψ H implies ψ H . φ. So suppose φ. It suffices to show if ψ H \ H . φ then for all χ HS(φ ψ), χ φ. By (H . de), ψ H \ H . φ implies for all χ HS(φ ψ), χ H . φ. Assume χ H . φ χ. By (H . 2), χ H . φ χ implies φ H . φ χ. It follows from (H . 8) and φ H . φ χ that H . φ χ H . φ. It follows from χ H . φ and H . φ χ H . φ that χ H . φ χ, which is a contradiction. Thus χ H . φ χ. By (HC ), χ H . φ χ implies χ φ. Zhuang & Pagnucco Proposition 2 If . is an entrenchment-based Horn contraction function, then it satisfies (H . 7). Proof: Let . be an entrenchment-based Horn contraction function for H with an associated Horn epistemic entrenchment . We have by Theorem 2 that . satisfies (H . 1) (H . 4), (H . de), (H . hs), (H . ct), and (H . 8). Suppose σ (H . φ) (H . ψ). We need to show σ H . φ ψ. Case 1, φ: Then ψ φ ψ. It follows from (H . 6) that H . φ ψ = H . ψ, and thus σ H . φ ψ. Case 2, ψ: The proof is similar to that of Case 1. Case 3, φ and ψ: It follows from (HEE2) that φ ψ φ. It follows from σ H . φ and (HC . ) that there is χ1 HS(φ σ) such that φ < χ1. We then conclude from (HEE1) that φ ψ < χ1. Similarly, it follows from (HEE2) that φ ψ ψ and from σ H . ψ and (HC . ) that there is χ2 HS(ψ σ) such that ψ < χ2, and thus φ ψ < χ2. By Lemma 5 (Part 5), we can deduce from φ ψ < χ1 and φ ψ < χ2, that φ ψ < χ1 χ2. By the definition of Horn strengthening we have χ1 |φ σ and χ2 ψ σ which implies χ1 χ2 (φ σ) (ψ σ). Since (φ σ) (ψ σ) (φ ψ) σ, we have χ1 χ2 (φ ψ) σ. It then follows from Lemma 2 that there is χ HS((φ ψ) σ) such that χ1 χ2 χ. By (HEE2), χ1 χ2 χ implies χ1 χ2 χ. We then have by (HEE1), that φ ψ < χ. Finally, it follows from φ ψ < χ and (HC . ), that σ H . φ ψ. Theorem 4 A function . is a strict entrenchment-based contraction function iff. satisfies (K . 1) (K . 8) and (K . hs). Proof: For one direction, suppose . is a strict entrenchment-based contraction function for K with an associated epistemic entrenchment . Then satieties (EE6). Since a strict entrenchment-based contraction function is an entrenchment-based contraction function, we have by Theorem 1 that . satisfies (K . 1) (K . 8) and (C ). It remains to show . satisfies (K . hs). Suppose φ, ψ LH and ψ K . φ. We need to show there is χ HS(φ ψ) such that χ K . φ χ. If φ then by the definition of Horn strengthening we have χ thus the result trivially holds. So suppose φ. It then follows from ψ K . φ and (C . ) that φ < φ ψ. Since satisfies (EE6), there is χ HS(φ ψ) such that φ < χ. Since . satisfies (C ), φ < χ implies χ K . φ χ. For the other direction, suppose a function . satisfies (K . 1) (K . 8) and (K . hs) we need to show . is a strict entrenchment-based contraction function. It follows from Theorem 1 that . is an entrenchment-based contraction function. It remains to show the epistemic entrenchment generated from . via (C ) satisfies (EE6). Suppose φ, ψ LH and φ < φ ψ. We need to show there is χ HS(φ ψ) such that φ < χ. By (C . ), φ < φ ψ implies ψ K . φ. Then it follows from (K . hs) that there is χ HS(φ ψ) such that χ K . φ χ which implies by (C ) that φ < χ. Theorem 5 If . H is an entrenchment-based Horn contraction function, then there is a strict entrenchment-based contraction function . such that . H and . are Horn equivalent. If . is a strict entrenchment-based contraction function, then there is an entrenchment-based Horn contraction function . H such that . H and . are Horn equivalent. Proof: Part 1: Let K be a belief set and H a Horn belief set such that H = H(K). Suppose . H is an entrenchment-based Horn contraction function for H and it is determined Entrenchment-Based Horn Contraction by the Horn epistemic entrenchment H for H. Let a binary relation over L be such that for φ, ψ LH (1) φ ψ iffφ H ψ, and (2) φ < φ ψ iffthere is χ HS(φ ψ) such that φ