Extending AGM Contraction to Arbitrary Logics

1 Introduction

The ability to revise and contract beliefs in a rational manner is essential for an intelligent agent. The area of belief change studies operators such as revision and contraction. The dominant approach in belief change is the well known AGM paradigm [Alchourr´on et al., 1985; G¨ardenfors, 1988] in which the beliefs held by an agent are modelled by a logically closed set of formulas called a belief set. The AGM paradigm has a minimal requirement on the underlying logic, that it subsumes classical propositional logic. This means the underlying logic must fully support all the truth functional logical connectives such as negation and disjunction.

The requirement on expressiveness is clearly a limitation in artificial intelligence. Many artificial intelligence applications are built on logical languages that lack certain logical connectives. For example, ontology-based data access [Poggi et al., 2008] is mostly built on description logics (DLs) [Baader et al., 2003], and some DLs do not fully support negation and disjunction. The AGM paradigm is thus inapplicable in these situations. To remedy this limitation, significant effort has been made on constructing AGM-style contraction and revision functions for such logics.

To date, the focus has been on fragments of propositional logic and DLs, e.g., [Booth et al., 2011; Delgrande and Peppas, 2015; Delgrande and Wassermann, 2013; Creignou et al., 2014; Ribeiro et al., 2013]. The guiding principle is that the newly constructed contraction functions maintain, as well as possible, the AGM approach. So new techniques are developed to address the inexpressiveness of the logic fragment, while attempting to adhere to the AGM approach. What is common about the existing work is that they focus on a particular logic and develop techniques specifically for that logic. Given the vast number of inapplicable logics, it is not practical to deal with all of them individually. Thus an interesting question is whether there are techniques that work for all those logics. In this paper, we will present such a technique for entrenchment-based contraction.

A contraction function .- for a belief set K is a function that takes as input a formula φ to be contracted from K and returns as output another belief set K .-φ. Entrenchmentbased contraction is a classic construction method for AGM contraction functions. Intuitively, an agent's beliefs are going to vary in their epistemic importance and a rational agent will give up a less important belief over a more important one in a contraction. Thus all formulas are ranked by their epistemic importance, where higher-ranked formulas are deemed more important. The outcome of a contraction is then determined by using this ranking on formulas. In particular, to determine whether a formula ψ previously held by the agent is retained after contracting by a formula φ (i.e., to decide if ψ ∈ K .-φ), φ is compared with the disjunction φ∨ψ, and ψ is retained if φ∨ψ is higher in the ranking than φ. So, disjunction plays an essential role, and for this reason entrenchment-based contraction is inapplicable to many useful logics including the major propositional fragments and most DLs.

Our goal is to redefine entrenchment-based contraction so that it applies to as may as possible the inapplicable logics. Our strategy is to first define a logic that is general enough to subsume many of the inapplicable ones; then define a version of entrenchment-based contraction for this general logic. Since any of the subsumed logics can be considered as a refinement of the general logic, this version of entrenchmentbased contraction automatically applies to these logics. As we are aiming at propositional fragments and DLs, we will define a general logic called first-order conjunctive logic (FC logic) that subsumes the majority of DLs and major propositional fragments.

The key in defining a version of entrenchment-based contraction for FC logic is to avoid the reliance on disjunction. In deciding whether to retain ψ in contracting φ, we compare φ with, instead of the disjunction φ ∨ ψ, the FC logic formulas that entail φ∨ψ. We call such formulas critical formulas of ψ with respect to φ and, if any of the critical formulas is higher in the ranking than φ, then ψ is retained. We call the contraction defined via the notion of critical formulas FC contraction. We provide representation theorem for FC contraction which shows that it is a generalisation of entrenchment-based contraction.

2 First-Order Conjunctive Logic

We adopt the Tarskian definition of logic, under which a logic is a pair 〈L,Cn〉 where L is the underlying language and Cn : 2L → 2L is a function that takes each subset of L to another. The intended meaning of Cn is that Cn(X) consists of all logical consequences of X. Under this setting, propositional and first-order logic are denoted 〈LP, CnP〉 and 〈LF,CnF〉 respectively.

Throughout this paper, propositional atoms are written as a, b, . . . , formulas as φ, ψ, . . ., and sets of formulas as S,X, . . .. The letter K is reserved to represent a belief set in some understood logic. So, for example, in the next section we will have K ⊆ LP and K = CnP(K). We sometimes write X |= φ to denote φ ∈ Cn(X), and |= φ to denote φ ∈ Cn(∅). Also Cn({φ}) is abbreviated as Cn(φ).

A logic 〈L′ ,Cn′ 〉 is a fragment of a logic 〈L,Cn〉 if and only if L′ ⊆ L and Cn′ (X) = Cn(X) ∩ L′ for all X ⊆ L′ . Major fragments of propositional logic include the Horn and Krom fragments. The Horn fragment, denoted 〈LH, CnH〉, allows only clauses with at most one positive atom and conjunctions of these clauses. The Krom fragment, denoted 〈LK,CnK〉, allows only clauses with at most two atoms and conjunction of these clauses. By considering propositional atoms as nullary predicates, propositional logic is a fragment of first-order logic. We noted that the majority of DLs are (decidable) fragments of first-order logic.

A logic is a first-order conjunctive logic (FC logic) if and only if it is a fragment of first-order logic that supports conjunction. 1 Let 〈L, Cn〉 be a FC logic. Then φ, ψ ∈ L implies φ∧ψ ∈ L, and Cn is such that Cn(X) = CnF(X) ∩L for all X ⊆ L. For generality, the class of FC logics is intentionally defined to be vague on the supported logical connectives except conjunction. So a FC logic may or may not support connectives like disjunction or negation but it must support conjunction. Since propositional logic and its usual fragments support conjunction, they are FC logics. Similarly, first-order logic and DLs that are first-order fragments are also FC logics. In particular, since FC logic does not require negation, most members of the EL [Baader et al., 2005] family of DLs are FC logics.

Due to the generality of FC logic, if a construction method is applicable to all FC logics, then it is so to all the aforementioned propositional fragments and DLs. We will provide one such construction method in Section 4.

1 Supporting conjunction is hardly an expressiveness requirement as for any first-order fragment, a set of formulas {φ1, . . . , φn} can be interpreted as the conjunction φ1 ∧ · · · ∧ φn.

3 Entrenchment-Based Contraction

Various (equivalent) construction methods have been proposed for AGM contraction functions. In this section, we review a classic construction called entrenchment-based contraction. As noted, the beliefs held by an agent are not equal in terms of epistemic importance. In [G¨ardenfors, 1988; G¨ardenfors and Makinson, 1988], more important beliefs are said to be more entrenched, and the relative entrenchments between formulas is modelled by a relation called epistemic entrenchment. Given a belief set K, the epistemic entrenchment associated with K is a binary relation ≤ over LP 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 φ ≤ σ
• (EE2) If φ |=P ψ then φ ≤ ψ
• (EE3) φ ≤ φ ∧ψ or ψ ≤ φ ∧ψ
• (EE4) If K is consistent then φ ̸∈ K iff φ ≤ ψ for all ψ
• (EE5) If φ ≤ ψ for every φ then |=P ψ

Thus an epistemic entrenchment is a transitive relation (EE1) such that logically stronger formulas are not more entrenched than weaker ones (EE2), logically equivalent formulas are equally entrenched (EE2), a conjunction is equally entrenched as its least entrenched conjunct (EE2)-(EE3), non-beliefs are least entrenched (EE4), and tautologies are most entrenched (EE5).

The outcome of an entrenchment-based contraction function .- for K is determined by the associated epistemic entrenchment ≤ via the following condition:

Thus ψ is retained after the contraction of K by φ (i.e., ψ ∈ K .-φ) if and only if it was originally believed (i.e., ψ ∈ K) and there is "sufficient evidence" for retaining it (i.e., φ < φ ∨ ψ) or it is not possible to remove φ (i.e., |=P φ).

Given a contraction function .- for K, we can obtain an epistemic entrenchment ≤ through the following condition:

If .- is an entrenchment-based contraction function then the relation ≤, determined via (C ≤), is the determining epistemic entrenchment for .-. This result is crucial for proving the following representation theorem for entrenchment-based contraction.

Theorem1. [G¨ardenfors andMakinson, 1988] A function .- is an entrenchment-based contraction function iff .- satisfies the following postulates:

• (K .-2) K .-φ ⊆K
• (K .-1) K .-φ = CnP(K .-φ)
• (K .-3) If φ ̸∈ K, then K .-φ =K
• (K .-5) K ⊆ (K .-φ) +φ
• (K .-4) If ̸|=P φ, then φ ̸∈ K .-φ
• (K .-6) If CnP(φ) = CnP(ψ), then K .-φ =K .-ψ
• (K .-8) If φ ̸∈ K .-φ ∧ψ then K .-φ ∧ψ ⊆K .-φ
• (K .-7) K .-φ ∩K .-ψ ⊆K .-φ ∧ψ

Intuitions behind these postulates are well known and thus are omitted. However, it is important to note that (K .-5), called the recovery postulate, is controversial and has been the subject of much discussion [Makinson, 1987; Hansson, 1991; Levi, 1991]. For example Hansson [1991] argues that it is an emergent property rather than a fundamental postulate. Also (K .-7) and (K .-8), which are often referred as the supplementary postulates, capture relations between contraction by a conjunction and contractions by the constituent conjuncts. Seminal results in the AGM paradigm show that (K .-7) and (K .-8) correspond to the existence of a well behaved plausibility ranking such as epistemic entrenchments which governs the changes of belief. Several equivalent postulates of (K .-7) have also been proposed. In particular, in the presence of the other postulates, (K .-7) is equivalent to the postulate of Conjunctive Trisection [Rott, 1992; Hansson, 1993]:

4 Redefining Entrenchment-Based Contraction for FC Logics

Condition (C .-), which is central to entrenchment-based contraction, refers to disjunctions. Since a FC logic does not necessarily support disjunction, entrenchment-based contraction is not in general applicable to FC logics. In this section, we provide a version of entrenchment-based contraction that applies to an arbitrary FC logic 〈LFC,CnFC〉. Unless explicitly stated, 〈LFC,CnFC〉 is the default underlying logic in the remainder of the paper.

FC Contraction

According to (C .-), the disjunction φ ∨ ψ is crucial for deciding whether to retain ψ in the contraction by φ. φ ∨ ψ is a first-order formula but not necessarily a 〈LFC,CnFC〉 one; thus we instead consider the 〈LFC,CnFC〉 formulas that entail φ∨ψ under the consequence operator of first-order logic and we call them the critical formulas of ψ with respect to φ.

Definition 1. Let the underlying logic be 〈LFC, CnFC〉. The set of critical formulas of ψ with respect to φ, denoted C φ (ψ), is given by: σ ∈ C φ (ψ) iff σ ∈ LFC and σ |=F φ ∨ ψ.

For example, if 〈LFC, CnFC〉 is 〈LH, CnH〉, then ¬a, b, c, ¬a∨b, and ¬a ∨ c are critical formulas of c w.r.t. ¬a ∨ b but b ∨ c is not. This is because although b∨c entails ¬a∨b∨c, it is not a 〈LH, CnH〉 formula. Note that critical formulas always exist. Since φ and ψ are both 〈LFC, CnFC〉 formulas and entail φ∨ψ, we at least have φ and ψ as the critical formulas of ψ w.r.t. φ. To fully appreciate the notion, it helps to identify logically the weakest critical formulas, which we call the most critical formulas.

Definition 2. Let the underlying logic be 〈LFC,CnFC〉. A formula σ is a most critical formula of ψ with respect to φ iff σ ∈ C φ (ψ) and for all σ′ ∈ C φ (ψ), σ |=FC σ′ implies σ′ |=FC σ.

If 〈LFC,CnFC〉 is propositional or first-order logic, then φ∨ψ is the single most critical formula of ψ w.r.t. φ up to logical equivalence. For FC logics that do not fully support disjunction, often there are multiple (non-logical equivalent) most critical formulas. Of the many critical formulas in the 〈LH, CnH〉 example above, both ¬a ∨ b and ¬a ∨ c are most critical ones. ¬a is not a most critical one as ¬a entails ¬a∨b but not vice versa. Similarly, neither b nor c are most critical ones. For the same example, if 〈LFC,CnFC〉 is 〈LK,CnK〉, then since disjunctions with two positive atoms are allowed, other than ¬a ∨ b and ¬a ∨ c, b ∨ c is also a most critical formula. Last, for the limiting case where φ ∨ ψ is a tautology, clearly every most critical formula of ψ w.r.t. φ is a tautology.

Before reformulating (C .-) with the notion of critical formulas, we have to fix the relative entrenchments between 〈LFC,CnFC〉 formulas. The relative entrenchments are represented by a binary relation over LFC that satisfies the 〈LFC,CnFC〉 version of conditions (EE1)-(EE5). 2 Such version can be obtained for (EE1)-(EE4) by assuming 〈LFC,CnFC〉 formulas and consequence operator. As a FC logic may not be able to express tautologies, the version for (EE5) which is shown below states that if the logic is able to express that ψ is a tautology, then ψ is strictly more entrenched than any other non-tautological formulas.

(EE5) If |=FC ψ, then φ < ψ for every φ such that ̸|=FC φ We call such a binary relation a FC epistemic entrenchment.

The reformulated version of (C .-), viz. (CFC .-), which gives the contraction outcome through a FC epistemic entrenchment is as follows.

(CFC .-) ψ ∈ K .-φ iff ψ ∈ K and either there is σ ∈ C φ (ψ) such that φ < σ or |=FC φ.

To decide if ψ ∈ K .-φ, we first check if ψ ∈ K and if so we compare the relative entrenchment between φ and the critical formulas of ψ w.r.t. φ. The existence of a critical formula being strictly more entrenched than φ is a sufficient condition for retaining ψ. Similar to (C .-), another sufficient condition is that φ is a tautology.

Among the critical formulas of ψ w.r.t. φ, the most critical ones are logically the weakest ones thus by (EE2) they are also the most entrenched ones. This means there is a critical formula of ψ w.r.t. φ that is strictly more entrenched than φ if and only if there is a most critical one that is so. Therefore, to decide if ψ ∈ K .-φ, it suffices to compare the relative entrenchment of φ with only the most critical formulas of ψ w.r.t. φ.

Formally, the version of entrenchment-based contraction for 〈LFC, CnFC〉, called FC contraction, is defined as follows.

Definition 3. A function .- is a FC contraction function for K iff the output of .- is determined by the FC epistemic entrenchment associated with K via (CFC .-).

2 (EE4) states properties regarding formulas not in a consistent belief set, it should be noted that our approach works even if with the underlying logic every belief set is consistent.

Figure 1 demonstrates, under 〈LK,CnK〉, the contraction of K = CnK({¬a ∨ b, c}) by b ∨ c when the associated FC epistemic entrenchments are ≤1 and ≤2 respectively. The rectangles illustrate the formulas in K along with their entrenchments. Formulas at the same level of a rectangle are equally entrenched and formulas at a higher level are strictly more entrenched than those in a lower level. 3 The shaded formulas are retained after the contraction. ¬b ∨ c is retained for both ≤1 and ≤2, since the most critical formulas of ¬b ∨ c w.r.t. b ∨ c are tautologies which are strictly more entrenched than b∨c in both cases. The most critical formulas of ¬a∨b w.r.t. b ∨ c are ¬a ∨ b, b ∨ c, and ¬a ∨ c. ¬a ∨ b is retained under ≤1 but not under ≤2, since for ≤1 the most critical formula ¬a∨c is strictly more entrenched than b∨c but none of them is so for ≤2.

Following the AGM tradition, we will make explicit some properties of FC contraction by proving a representation theorem for it. The proof is more involved than that of the representation theorem for entrenchment-based contraction, since we no longer have a functionally complete set of logical connectives at our disposal. As a preparatory result, we can show that any FC contraction function satisfies (C ≤).

Theorem2. If .- is a FC contraction function then it satisfies (C ≤).

Proof sketch: If disjunctions of formulas are allowed then the proof can go through as in the propositional case. The trick is that we can indirectly refer to disjunctions via the link provided in the definition of critical formulas. That is, critical formulas of ψ w.r.t. φ entail φ∨ψ under first-order logic.

Next we present the representation theorem.

Theorem 3. A function .- is a FC contraction function for K iff .- satisfies the following postulates:

• (FC .-2) K .-φ ⊆K
• (FC .-1) K .-φ = CnFC(K .-φ)
• (FC .-3) If φ ̸∈ K, then K .-φ = K
• (FC .-de) If ψ ∈ K \K .-φ, then σ ̸∈ K .-φ for all σ ∈ C φ (ψ)
• (FC .-4) If ̸|=FC φ, then φ ̸∈ K .-φ
• (FC .-6) If CnFC(φ) = CnFC(ψ), then K .-φ = K .-ψ
• (FC .-ct) If φ ∈ K .-φ ∧ψ, then φ ∈ K .-φ ∧ψ ∧ δ
• (FC .-re) If ψ ∈ K .-φ, then there is σ ∈ C φ (ψ) such that σ ∈ K .-φ ∧ σ

Proof sketch: To prove satisfactions of the postulates, again the key is the ability to use disjunctions indirectly. For the other direction, (FC .-ct) and (FC .-8) correspond to (EE1)-(EE5) as in the AGM case. In the principal case, (FC .-re) and (C ≤) correspond to: if ψ ∈ K .-φ then there is σ ∈ C φ (ψ) s.t. φ < σ, and (FC .-de) and (C ≤) correspond to the converse. Thus together they characterise (CFC .-)

(FC .-1)-(FC .-4), (FC .-6), (FC .-ct), and (FC .-8) are the 〈LFC, CnFC〉 version of (K .-1)-(K .-4), (K .-6), (K .-ct), and (K .-8). Although not required for its characterisation, FC contraction also satisfies the 〈LFC,CnFC〉 version of (K .-7).

3 Non-beliefs, tautologies and conjunctions are not shown as their entrenchments are uniquely determined by the formulas shown.

Theorem4. If a function .- is a FC contraction function then .- satisfies the following postulate:

According to Theorem 3 and 4, FC contraction complies with all the AGM contraction postulates except Recovery. Additionally, it complies with (FC .-de), (FC .-re), and (FC .-ct).

Absence of Recovery is not a weakness of FC contraction. Besides its controversy, satisfaction of Recovery is subject to a property (viz, AGM-compliance) 4 of the underlying logic [Ribeiro et al., 2013], and not all FC logics have this property. Alternatively, we rely on (FC .-de) to play the role of Recovery. (FC .-de) originates from the postulate of Disjunctive Elimination [Ferm´e et al., 2008]:

In its contrapositive form

(K .-de) is "a condition for a sentence ψ 'to survive' the contraction process" [Ferm´e et al., 2008](page 745). So essentially (K .-de) specifies what should be retained after the contraction and in turn captures some minimal change properties of a contraction. (K .-de) is equivalent to Recovery under 〈LP,CnP〉 but unlike Recovery it is amenable to 〈LFC,CnFC〉. (K .-de) refers to the disjunction φ ∨ ψ, which is the single most critical formula (up to logical equivalence) for ψ w.r.t. φ under 〈LP, CnP〉. In a more general setting where disjunction is not fully supported and there may be multiple most critical formulas, we have to refer to the critical formulas by the notation C φ (ψ), as in (FC .-de).

As with (FC .-de), (FC .-re) is neither a generalisation of an AGM contraction postulate nor a completely new postulate. Actually, it originates from a property of entrenchmentbased contraction. For entrenchment-based contraction, the rule for retaining a formula is specified by (C .-). Due to (C ≤), (C .-) implies the following property regarding retained formulas:

This property however does not have to be postulated explicitly, as it can be deduced from (K .-6) and (K .-1) (under 〈LP,CnP〉). For FC contraction, the rule for retaining formulas is specified by (CFC .-), which requires that, when deciding the retainment of ψ in the contraction by φ, ψ is retained if a critical formula of ψ w.r.t. φ is strictly more entrenched than φ. Due to (C ≤), this rule is captured exactly by (FC .-re). And this time the postulate is not deducible from the others. Note that (FC .-re) generalises (K .-re) in the same way as (FC .-de) generalises (K .-de).

In summary, FC contraction complies with the set of postulates that are sufficient to characterise entrenchment-based contraction 5 and all the characterising postulates for FC contraction originate from those that characterise entrenchmentbased contraction. This suggests that FC contraction is no different from entrenchment-based contraction, only that the former is applicable to a much wider class of logics, and thus is a generalisation of the latter. The next subsection will further elaborate this point.

4 A logic 〈L, Cn〉 is AGM-compliant iff for all K, A ⊆ L, where A is finitely representable and Cn(∅) ⊂ Cn(A) ⊂ Cn(K), there is a K′ ⊆ L s.t. Cn(K′ ) ⊂ Cn(K) and K′ ∪ A = K.

Application to 〈LP, CnP〉 and 〈LH, CnH〉

Theorems 2, 3, and 4 have shown the rationality of FC contraction in the traditional way. To further evaluate this construction method, we apply it to propositional logic and its Horn fragment respectively.

We have noted that, under 〈LP, CnP〉, the single most critical formula of ψ w.r.t. φ is the disjunction φ ∨ ψ. So according to (C .-) and (C .-FC), once the same epistemic entrenchment is used for determining the contraction outcome, a FC contraction function and an entrenchment-based contraction function produce identical outcomes.

Theorem 5. If the underlying logic is 〈LP,CnP〉 then a function is a FC contraction function iff it is an entrenchmentbased contraction function.

Next we consider the Horn fragment. Entrenchment-based contraction has been adapted for 〈LH,CnH〉 in [Zhuang and Pagnucco, 2014], where their version is called entrenchmentbased Horn contraction. Entrenchment-based Horn contraction is based on the notion of Horn strengthenings [Kautz and Selman, 1996]. For any non-Horn disjunction φ, its set of Horn strengthenings, denoted HS(φ), consists of the logically weakest Horn formulas that entail φ. The contraction outcome is determined by condition (HC .-), which reformulates (C .-) with the notion of Horn strengthenings.

(HC .-) ψ ∈ K .-φ iff ψ ∈ K and either there is σ ∈ HS(φ ∨ ψ) such that φ < σ or |=H φ.

In (HC .-), ≤ is a binary relation over LH that satisfies the 〈LH,CnH〉 version of (EE1)-(EE5); it is called Horn epistemic entrenchment. Clearly, a FC epistemic entrenchment is a Horn epistemic entrenchment under 〈LH,CnH〉. To decide whether to retain ψ when contracting K by φ, (HC .-) compares φ with the Horn strengthenings of φ∨ψ. As a consequence of Definition 2, the set of Horn strengthenings of φ∨ψ is exactly the set of most critical formulas of ψ w.r.t. φ.

Lemma 1. If the underlying logic is 〈LH,CnH〉 then HS(φ∨ ψ) is the set of most critical formulas of ψ with respect to φ.

So according to (HC .-) and (C .-FC) once the same Horn epistemic entrenchment is used for determining the contraction outcome, a FC contraction function and an entrenchment-based Horn contraction function produce identical outcomes.

Theorem 6. If the underlying logic is 〈LH,CnH〉 then a function is a FC contraction function iff it is an entrenchmentbased Horn contraction function.

5 Since (K .-de) and (K .-ct) are equivalent to (K .-5) and (K .-7) respectively, (K .-1)-(K .-4), (K .-de), (K .-6), (K .-ct), and (K .-8) are sufficient to characterise entrenchment-based contraction.

5 ComputingMost Critical Formulas

We next investigate the computation of most critical formulas. For practical applications, it is natural to assume that the language LF is over a finite set of predicates, constants, and functions. For any FC logic 〈LFC, CnFC〉, since LFC is a subset of LF, it consists of a finite number of formulas.

For all FC logics, the computational procedures for FC contraction (which basically implement condition (CFC .-)) are identical except for the computation of most critical formulas. Due to the diversity of FC logics, procedures for computing most critical formulas for one FC logic can be quite different from that for another. The procedures for propositional and first-order logic are the simplest, as for these logics the only most critical formula of ψ w.r.t. φ is φ∨ψ (up to logical equivalence). Clearly, procedures for FC logics that do not fully support disjunction are more involved. By Lemma 1, a procedure for the Horn fragment can be inherited from that for computing Horn strengthenings. In contrast to propositional fragments, DLs are fragments of a higher order logic with more complicated semantics and syntax; however, as we will show, procedures for computing most critical formulas for DLs are not necessarily more complicated than that for propositional fragments.

If a FC logic satisfies the following variant of the disjunction property 6 then the most critical formulas can be obtained without any computation.

(DP) γ |=F φ∨ψ iff γ |=FC φ or γ |=FC ψ for γ, φ, ψ ∈ LFC The reason is that (DP) assures that if there is no entailment between φ and ψ, then the most critical formulas of ψ w.r.t. φ can only be ψ and φ (up to logical equivalence). In the case that there is an entailment between φ and ψ, say φ entails ψ, then φ ∨ ψ is equivalent to ψ and so the single most critical formula is ψ itself (up to logical equivalence).

Lemma 2. If 〈LFC,CnFC〉 satisfies (DP), and φ, ψ ∈ LFC are such that φ ̸|=FC ψ and ψ ̸|=FC φ, then the most critical formulas of ψ with respect to φ are φ and ψ.

Of the DLs that can be classified as FC logics, SRIQ [Horrocks et al., 2005] is a very expressive one. 7 SRIQ subsumes many common DLs like SHIQ and ALC, and the Horn fragment of SRIQ (viz., Horn-SRIQ) [Ortiz et al., 2010] covers a majority of the EL and DL-Lite families.

We can show that any fragment of Horn-SRIQ has the disjunction property, which means that for these DLs, most critical formulas can be obtained without any computation.

Theorem 7. If 〈LFC,CnFC〉 is a DL that is a fragment of Horn-SRIQ then it satisfies (DP).

Proof Sketch. We show that for Horn-SRIQ formulas γ, φ and ψ, γ ̸|=FC φ and γ ̸|=FC ψ imply γ ̸|=F φ ∨ ψ. We show this using tableau. Suppose γ ̸|=FC φ; then a conflictfree tableau can be constructed from ¬φ w.r.t. γ, which is essentially a model of γ and ¬φ. Similarly, suppose γ ̸|=FC ψ; a conflict-free tableau of ¬ψ can be constructed w.r.t. γ. If these two tableaux share no constants, a conflict-free tableau of ¬φ ∧ ¬ψ can be constructed from the tableaux of ¬φ and ¬ψ w.r.t. γ, which is a model of γ and ¬φ ∧ ¬ψ; and the statement is proven. If the tableaux of ¬φ and ¬ψ share a constant then that is when φ and ψ are both ground atoms (i.e., ABox axioms), and we prove the statement using the canonical model property of Horn-SRIQ, that is, γ ̸|=FC φ and γ ̸|=FC ψ imply that the canonical model of γ satisfies ¬φ and ¬ψ, and hence γ ̸|=F φ ∨ ψ.

6 |= φ ∨ ψ iff |= φ or |= ψ.

7 Its extension SROIQ underlies the OWL 2 standard for Web ontology languages.

A non-Horn fragment of SRIQ (such as ALC) does not necessarily have the disjunction property. For example (we use DL syntax here), (A⊔B)(a) entails A(a)∨B(a), but neither disjunct is entailed. For a more involved example, R(a, b) together with (A ⊔ ∀R.B)(a) entail A(a) ∨ B(b), but again neither disjunct is entailed.

The hybrid nature of DL knowledge bases gives rise to some subtle issues for contraction. A DL knowledge base consists of a TBox and an ABox where the formulas in a TBox, the TBox axioms, are disjoint from those in an ABox, the ABox axioms. For certain applications, it is useful to perform contraction to the TBox without considering the ABox. Note that in these applications, the underlying logic is not a DL but its TBox fragment. Formally, if 〈L,Cn〉 is a DL then its TBox fragment 〈LT,CnT〉 is such that LT consists of the TBox axioms of L and CnT(S) = Cn(S) ∩ LT. If a DL is a FC logic then its TBox fragment is obviously so. Thus such a contraction scenario can be handled by FC contraction. Fortunately, we can show in the same manner as Theorem 7 that for DLs that are fragments of SRIQ, their TBox fragments have the disjunction property.

Theorem 8. If 〈LFC,CnFC〉 is a DL that is a fragment of SRIQ then its TBox fragment satisfies (DP).

6 RelatedWork

Most work on defining AGM-style contraction in a nonclassical logic has focussed on the Horn fragment of propositional logic and DLs. We have shown that FC contraction when applied to the Horn fragment is equivalent to entrenchment-based Horn contraction. Several [Delgrande and Wassermann, 2013; Booth et al., 2011] have adapted partial meet contraction [Alchourr´on et al., 1985] to the Horn fragment. Unlike FC contraction and entrenchment-based Horn contraction, the contractions defined in [Delgrande and Wassermann, 2013; Booth et al., 2011] do not assume explicit preference relations such as epistemic entrenchments.

There has been much work on defining revision for DLs [Qi et al., 2006; Qi and Du, 2009; Wang et al., 2010], while there has been little work addressing contraction. [Qi et al., 2008] and [Ribeiro and Wassermann, 2009] defined contraction for DLs, but they focus on belief base contraction. The only AGM-style contraction defined for DLs, more specifically DL-Lite, is the model-based contraction in [Zhuang et al., 2014]. FC contraction when applied to DL-Lite satisfies all characterising postulates of the model-based contraction except a variant of (K .-de) that is local to the contraction.

The only work on extending the AGM paradigm that aims at both propositional fragments and DLs is [Ribeiro et al., 2013]. Instead of providing a construction, this work identifies some sufficient conditions for the possibility of defining a contraction function that satisfies the postulates of Recovery and of Relevance [Hansson, 1991].

7 Conclusion and FutureWork

In this paper, the AGM approach is strictly generalised to arguable all the reasonable fragments of first-order logic in that when the underlying logic is propositional logic, the postulate set is equivalent to the standard AGM contraction postulates (with Recovery replaced by Disjunctive Elimination). Specifically, the generalisation is carried out for entrenchmentbased contraction with the generalised version called FC contraction. The generality is achieved by basing FC contraction on the notion of critical formulas which imposes no requirement on the expressiveness of the underlying logic.

Given its wide applicability, FC contraction can be used as the foundation for many practical applications. A mandatory task of managing knowledge bases is the elimination of problematic or outdated formulas. Since FC contraction is applicable to for instance most DLs and propositional fragments, it can be used to guide such elimination for knowledge bases based on these logics. Fortunately most DLs satisfy the disjunction property, which means that computing most critical formulas - the core computation task for FC contraction - can be done in constant time.

There are several aspects of FC contraction that merit further exploration. First, we will devise procedures for computing most critical formulas when the underlying logic does not satisfy condition (DP). Second, we will adapt FC contraction to a common contraction scenario for DLs where only the ABox is to be modified. One way this can be done is to restrict FC epistemic entrenchments so that TBox axioms are always more strongly entrenched than ABox axioms.