Towards a Principle-based Framework for Assessing the Contribution of Formulas on the Conflicts of Knowledge Bases

1 Introduction

Inconsistency is often a prominent issue in AI-based systems, and knowledge about real-world domains is essentially inconsistent. It is a common idea that some sets of information are more inconsistent than others, or that some pieces of information are to be considered responsible for logical conflicts while others are not. In order to gain a better understanding of such scenarios we need to develop formal methods: namely inconsistency measures. A relevant way of doing that is by evaluating the amount of conflicts in knowledge-based systems. In recent years, inconsistency measurement has become a vibrant trend of research in AI [Hunter and Konieczny, 2010; Ammoura et al., 2017; Jabbour et al., 2016; Jabbour et al., 2017; Bona et al., 2019; Besnard and Grant, 2020; Grant and Hunter, 2023] and Databases [Livshits et al., 2021; Grant et al., 2021; Parisi and Grant, 2023]. Numerous existing proposals have been devoted to evaluate at what point a knowledge base is contradictory by means of minimal inconsistent sets of that base (see [Thimm and Wallner, 2019] for a survey).

In contrast, we see comparatively little effort to investigate the quantification of the contribution of individual formulas to the inconsistency of knowledge bases. In this setting, minimal inconsistent sets play a crucial role to evaluate the amount of conflicts of formulas in knowledge bases. For a broad range of practical applications, it is becoming crucial to evaluate the responsibility of individual information of a given knowledge base for the inconsistency of that base. Notably, applications include progress indication in consistency recovering of inconsistent knowledge bases or ranking information for belief revision (e.g., [Ribeiro and Thimm, 2021; Raddaoui et al., 2023]. Moreover, quantifying the contribution of a formula to conflicts is desirable in databases to ranking user query explanations as discussed in [Livshits and Kimelfeld, 2021], and also to improving formulas clustering [Salhi, 2020]. Another concrete example includes modelbased diagnosis where filtering out the most faulty components of a system can be done by prioritizing the formulas modeling such components [Konieczny et al., 2003].

In the present paper, we focus exclusively on the measures that evaluate quantitatively the involvement of individual formulas in making a knowledge base inconsistent. These measures can take different forms. Existing proposals are mainly defined through the notion of minimal conflicts (usually called minimal inconsistent sets). A basic measure assigns the number of minimal conflicts the formula belongs to, while another metric takes also the size of these minimal conflicts into account [Hunter and Konieczny, 2010]. A more recent inconsistency measure employs a dual notion of minimal conflicts, called minimal correction set, to quantify how inconsistency arises in particular formulas within a knowledge base [Mu, 2015]. Despite their potentially fruitful success, these basic measures violate some intuitive properties (e.g., monotonicity, maximality). Similarly, one may use inconsistency measures from the literature (e.g., [Thimm and Wallner, 2019]) to determine the marginal contribution a formula makes to the inconsistency of the whole base. For instance, the participation of a formula α to the conflict could be computed by simply considering the value I(K)-I(K⊖α), where I is a measure that quantifies the contradiction of the entire base K. However, we will show in the sequel that this kind of measures violate some intuitive properties (e.g., monotonicity) for many existing global measures I.

In the rest of the paper, we first propose a set of postulates to systematise our comparative study. We then study several variants of inconsistency measures based on problematic and free formulas, some proposed in the literature and some new ones, ultimately introducing a new one that satisfies all proposed criteria. Finally, we conclude the paper and present some directions for future work.

2 Technical Background

We consider a finite set of propositional atoms or variables denoted by V. This set, along with the standard connectives (¬, ∨, ∧, →) and the Boolean constants (⊤ or true and ⊥ or false) is used in the usual way to build the propositional language L(V). Greek letters α, β, γ, . . . will be used to denote well-formed formulas from L(V). A literal is a propositional variable or its negation. A clause is a disjunction of literals C = ∨1≤i≤n ai. From now on, we denote by ⊢ the classical consequence relation. Two formulas α, β ∈ L(V) are said to be logically equivalent, written as α ≡ β, if {α} ⊢ β and {β} ⊢ α. A clause C is a prime implicate of a formula α iff α ⊢ C and for every clause C ′ , if α ⊢ C ′ and C ′ ⊢ C, then C ≡ C ′ holds. We denote by PI(α) the set of all prime implicates (i.e., set of clauses) of α. In this paper, a knowledge base is a finite set of propositional formulas from L(V). We use K to represent the set of all knowledge bases built over V. For a given knowledge base K, we write Atoms(K) ⊆ V for the set of atoms present in K. Given Atoms(K) = {p1, . . . , pn} and let {q1, . . . , qn} ⊆ V be a set of atoms not occurring in Atoms(K), the notation K[q1, . . . , qn] represents the syntactic substitution of each occurrence p1≤i≤n by q1≤i≤n in K. Additionally, K is inconsistent if there exists a formula α s.t. K ⊢ α and K ⊢ ¬α. Otherwise, K is consistent. In what follows, we use K ⊕ α (resp. K ⊖ α) as a shorthand for K ∪ {α} (resp. K \ {α}). We recall below three notions employed for reasoning under inconsistency

Definition 1. Let K ∈ K be a knowledge base. Then, a subset of formulas M ⊆ K is a:

• minimal inconsistent subset of K iff M ⊢ ⊥ and ∀α ∈ M, M ⊖ α ̸⊢ ⊥.
• maximal consistent subset of K iff M ̸⊢ ⊥ and ∀α ∈ K \ M, M ⊕ α ⊢ ⊥.
• minimal correction subset of K iff K \ M ̸⊢ ⊥, and ∀α ∈ M, (K \ M) ⊕ α ⊢ ⊥.

For convenience, we write ms(K), mc(K) and mi(K) for the set of maximal consistent subsets, minimal correction subsets and minimal inconsistent subsets of K, respectively. Let define mi(α,K) = {M ∈ mi(K) | α ∈ M}, ms(α,K) = {M ∈ ms(K) | α ∈ M}, and mc(α,K) = {M ∈ mc(K) | α ∈ M}. It is straightforward to see that mc(α,K) = {K \ M | M ∈ ms(K), α ̸∈ M}. A formula α that is not part of any minimal inconsistent set of K (i.e., mi(α,K) = ∅) is referred to as a free formula. We denote the set of free formulas in K as free(K), in symbols free(K) = K \ ⋃ mi(K) = ⋂ ms(K). When a formula α ∈ K is individually inconsistent, α is self-contradictory. We denote the set of self-contradictory formulas in K as ⊥(K) = {α ∈ K | α ⊢ ⊥}. We also write prob(K) for the set of problematic formulas (i.e., that are involved in at least one conflict), prob(K) = ⋃ mi(K).

When a knowledge base is inconsistent, one can evaluate quantitatively the amount of contradiction. Indeed, the field of inconsistency measurement captures this principle through the notion of inconsistency measure. The inconsistency measures studied so far in the literature can be roughly split in two classes. The first class, which we call here global inconsistency measure 1 , allows for a quantification of the degree of conflicts of the whole knowledge base. Whereas, the second class, which we refer to as local inconsistency measure 2 , evaluates the level of responsibility of every individual formula in producing inconsistencies in the knowledge base. In this paper, we are interested in the second class of measures, namely designing new local inconsistency measures to evaluate the inconsistency in propositional knowledge bases. In the sequel, we will refer to the notion of local/global inconsistency measure simply as local/global measure.

3 A Formal Framework for Local Inconsistency Measures

We now present a general framework for ascribing the degree of responsibility of formulas for the whole conflict of the knowledge base. Let us first introduce formally the notion of local inconsistency measure. Let for this K = {(ϕ,K) | K ∈ K, ϕ ∈ K}.

Definition 2. A local inconsistency measure is a function I on K that associates a real value to each formula α in a given knowledge base K, i.e., I : K→R+0 ∪ {∞}.

In informal terms, every formula α is associated with a non-negative real including ∞. Intuitively, these values represent degrees of responsibility of individual formulas to the overall conflicts, with 0 for free formulas, and so on. Briefly put, the intuition behind a local measure I is that the stronger the involvement of a formula α in the production of inconsistencies in K, the higher the value I(α,K).

3.1 Rationality Postulates

We begin this subsection by providing a set of meaningful properties a reasonable local measure should have. As is often the case with sets of formal postulates, they are hard to ultimately justify, they largely rely on pre-theoretic intuitions, and exhaustiveness is hard to reach, which is why we consider our set as merely providing a prima facie normative framework. Sometimes, a set of intuitive principles turns out as not being mutually satisfiable: as we will see, while most proposed measures sub-perform, we ultimately identify a candidate that satisfies them all (see Table 1 for an overview). Besides providing normative guidance, postulates help to comparatively study and systematize measures (see also [Hunter and Konieczny, 2010; Besnard, 2014] in the context of global measures). Since intuitive appeal behind the postulates should be largely self-explanatory we just list them without much commentary:

1 A global measure is formally defined as a function I : K → R+0 ∪ {∞} that maps every knowledge base K to a non-negative real value such that I(K) = 0 if prob(K) = ∅.

2 Local inconsistency measures are also called inconsistency values in [Hunter and Konieczny, 2010] and culpability measures in [Ribeiro and Thimm, 2021].

The Syntax-Independence states that the variables' names do not play any role in quantifying inconsistency.

• Logical Invariance. If α ≡ β, then I(α,K) = I(β,K)
• for every α, β ∈ K.

This principle stipulates that logical equivalent formulas contribute equally to the inconsistency of K.

• Blameless. 3 If prob(K) = ∅, then I(α,K) = 0 for all α ∈ K. This basic postulate states that the degree of inconsis-

tency of formulas in a consistent knowledge base is 0.

• Guiltless. For every α ∈ prob(K), I(α, K) > 0. This requirement ensures that problematic formulas contribute always in the inconsistency of K.
• Monotonicity. For every α ∈ K, I(α,K) ≤ I(α,K⊕ β).
• Strict Monotonicity. For every α ∈ K, if mi(α,K) ⊂
• mi(α,K⊕β), then I(α,K) < I(α,K⊕β).

The (strict) monotonicity property says that the amount of conflict of an individual formula can only grow when expanding the knowledge base by new information.

• Free Formula Independence. For every α ∈ K, if β ∈ free(K⊕β), then I(α,K) = I(α,K⊕β). This property expresses that adding a formula not causing any contradiction cannot change the inconsistency value of formulas in K.
• Minimality. (see [Hunter and Konieczny, 2010]) If α ∈ free(K), then I(α, K) = 0. This property states that non problematic formulas are free from inconsistency.
• Maximality. 4 If α ∈ ⊥(K), then I(α,K) ≥ I(β,K) for all β ∈ K.

This property ensures that self-contradictory formulas are crucially regarded as the most conflicting pieces of information.

• Centrality Conflict. 5 For all α, β ∈ K, if K ⊖ α ̸⊢ ⊥ and K ⊖ β ⊢ ⊥, then I(α, K) > I(β, K). This postulate states that a formula belonging to all minimal inconsistent sets involves a higher degree of incon-

sistency than any formulas in K.

• Dominance. 6 If α ⊢ β with α ∈ K \ ⊥(K), then I(α, K) ≥ I(β, K ⊖ α ⊕ β).
• Conjunctive Dominance. If α ∧ β /∈ K and α ∈ K, then I(α, K) ≤ I(α ∧ β, K ⊖ α ⊕ α ∧ β).

3 This property is called Consistency in [Hunter and Konieczny, 2010].

4 A similar property, named Maximal Contradiction, is studied in [Grant and Hunter, 2017] for global inconsistency measures. Another similar property, coined self-contradiction [Matt and Toni, 2008], used in argumentation to ranking self-attacking arguments lower than any other arguments.

5 A similar property has been pointed out in [Raddaoui et al., 2023] to rank formulas.

6 The original version of Dominance property is defined by [Hunter and Konieczny, 2008].

• Weak Dominance. If PI(β) ⊆ PI(α) and α ∈ K \ ⊥(K), then I(β,K⊖α⊕β) ≤ I(α,K). The last three properties ensure, under various conditions, that the substitution of consistent formulas with weaker ones does not lead to an increase in conflict.

Note that these postulates are intended to offer guidance for a better understanding of local measures by facilitating a comparison between them based on precise formal properties (see Table 1). Additionally, these postulates specify intuitive desiderata and potentially help devising new measures that satisfy sets of principles for which no previous measures are known to jointly satisfy them as shown in the subsequent sections.

The following proposition shows that Weak Dominance ensues from the Dominance property.

Proposition 1. Given a local measure I, if I satisfies Dominance, then I satisfies Weak Dominance. However, the converses is not true.

The next result ensures that the previous postulates can be satisfied all together by a local inconsistency measure.

Proposition 2. The properties Syntax Independence, Blameless, Guiltless, Logical Invariance, Monotonicity, Strict Monotonicity, Free Formula Independence, Minimality, Maximality, Dominance, Conjunctive and Weak Dominance are compatible.

3.2 ACloser Look at Existing Local Measures

Minimal inconsistent sets typically serve as the cornerstone to quantify conflicts in knowledge bases, and numerous global measures are very much tied to this notion. To date, relatively few methods have been introduced in the literature to evaluate the degree of inconsistency of formulas and no measure has a canonical status 7 . We next recall from [Hunter and Konieczny, 2010; Mu, 2015] the three local measures Id, Imi and I# mainly relying on minimal inconsistent sets, and the last one, Idr, based on minimal correction sets (see Figure 1).

The drastic measure Id discriminates only between free (with degree 0) and problematic (with degree 1) formulas. The local measure I# counts the number of minimal inconsistent sets the formula α occurs in, while Imi considers in addition the size of each of these minimal inconsistent sets [Hunter and Konieczny, 2010].

Now, we make some observations about these aforementioned local measures. We start by noticing that the measures Id, I# and Imi are the most popular and mainly built upon the notion of minimal conflicts to quantify the contribution of each formula to the whole inconsistency. In contrast, it turns out that I# and Imi violate the maximality postulate, which is a shortcoming. What we are aiming here for a new class of local measures that consider self-contradictory formulas the most conflictual ones. Our central aim in this paper is also to investigate local measures that take into account all possible

7 Some local measures have been studied for prioritized knowledge bases by [Mu et al., 2012] and are out of the scope of this paper.

Figure 1: Existing local inconsistency measures

participation of individual formulas in generating conflicts in the knowledge base.

The fourth local measure Idr [Mu, 2015], as depicted in Figure 1, is defined based on the concept of minimal correction sets. Again, it is worth mentioning that this measure can exhibit unintuitive results. We use the next examples to illustrate this issue.

Example 1. K = {p, ¬p, ¬q, p ∧ q} has three minimal correction sets: {p, p ∧ q}, {¬p, p ∧ q}, and {¬p, ¬q}. p and ¬p are equally responsible for the conflict: Idr(p,K) = Idr(¬p,K) = 1/2. However, one may find this unsatisfactory because ¬p conflicts with p and p ∧ q. While, p occurs in only one minimal inconsistent set, i.e., {p, ¬p}.

Example 2. Let K = {p, ¬p, q}. Then, we have Idr(p,K) = 1. Consider the base K′ = K ∪ {¬q}, we have Idr(p, K) = 1 ̸≤ Idr(p, K′ ) = 1/2, in violation of monotonicity.

Example 3. Let K = {p, ¬p}, α = p, and β = ¬p∧q. Then, Idr(α, K) = Idr(α, K ⊕ β) = 1. Thus, Idr violates the strict monotonicity.

Another approach to estimate the conflict of formulas is defined on the basis of global measures. Basically, a first local measure following this idea is the one based on the Shapley value [Hunter and Konieczny, 2010], and it is defined as follows.

Definition 3. Let K ∈ K s.t. |K| = n, α ∈ K and let I be a global measure. The Shapley inconsistency value w.r.t. I, denoted by SIK, is defined as:

What is remarkable with the measure I(K) = |mi(K)| is that the induced Shapley value SIK coincides with the local measure Imi [Hunter and Konieczny, 2010]. The next example shows that the (weak) dominance postulate is unsatisfiable for the Shapley inconsistency value SIK.

Example 4. Let K = {p∧q∧r∧s∧t, ¬p, p∨¬q, p∨¬r, p∨ ¬s, p∨¬t}. Let α = p∧q∧r∧s∧t and β = q∧r∧s∧t. We have α ⊢ β, I#(α, K) = 1 ̸≥ I#(β, K ⊖ α ⊕ β) = 4. In the same way, SIK(α, K) = 1/2 ̸≥ SIK(β, K⊖α⊕β) = 4×1/3 = 4/3. This is an example of the violation of dominance and weak dominance for I# and SIK.

The second idea for measuring inconsistency is based on the marginal contribution a formula makes to the inconsistency of K. Generally speaking, the degree of conflict of a formula α is the global measure of the base minus the global measure of that base when removing α, i.e., I(α, K) =

I(K) - I(K ⊖ α). A significant research effort so far has been devoted to quantify the conflict of knowledge bases (see [Thimm and Wallner, 2019; Bona et al., 2019] for an overview). Note that despite this plethora of global inconsistency measures, it is still not fully understood how these measures could be used to efficiently attribute the level of inconsistency to individual formulas. Specifically, applying an arbitrary global measure to define a local measure could lead to unintuitive results as shown in Section 4.

Additionally, while all of the above local measures have potentially fruitful success, none of them can be considered as appropriate for quantifying the amount of contradiction brought by individual formulas in all scenarios. This is why it is necessary to continue investigation of more elaborate local measures. We propose in the next section new local measures to pave the way towards a robust quantification of the participation of formulas to the overall inconsistency.

4 Towards NewClasses of Local Measures

As argued in the introduction, there is a need for a quantitative consistency metric that discriminates amongst individual formulas in knowledge bases. Unlike previous efforts on local measures, we strive in this section to devise more satisfactory measures to estimate the level of responsibility of each formula to the overall inconsistency, evaluated in terms of the postulates defined in Subsection 3.1.

4.1 Problematic-based Local Measures

As mentioned earlier, we can use a global measure from the literature to quantify the marginal contribution an individual formula makes to the inconsistency of a knowledge base. In this subsection, we use the global measure Iprob, defined in [Grant and Hunter, 2011] as the number of formulas in minimal inconsistent sets of the knowledge base (i.e., I(K) = |prob(K)|). Then, the induced local measure can be defined as follows.

Definition 4. Where α ∈ K let define the problematic-based local measure of α, denoted Iprob, as follows:

Intuitively, the Iprob measure counts the number of problematic formulas that become free when removing the formula α from K, by including α itself. In other words, Iprob considers the formulas that are problematic solely due to α (in signs, |prob(K)| - |prob(K ⊖ α)|). The trade-off is the greater this number of formulas, the higher is the participation of the formula α to make the base K inconsistent. At this point, Proposition 3 states that Iprob can be characterized directly in terms of minimal inconsistent sets.

Proposition 3. Given a knowledge base K s.t. α ∈ K\⊥(K), the following result holds:

The local measure Iprob satisfies the following logical properties.

Proposition 4. Iprob satisfies Syntax-Independence, Blameless, Guiltless, Logical Invariance, Free Formula Independence, Centrality Conflict, and Minimality.

Example 5. Let K = {p, ¬p ∧ q}, α = p and β = ¬q. We have Iprob(α, K) = 2. Now in K ⊕ β, we have Iprob(α, K ⊕ β) = 1 < Iprob(α,K). This example shows that Iprob does not satisfy monotonicity and strict monotonicity.

Example 6. Let K = {p ∧ q ∧ r, ¬p, ¬p ∨¬q, p ∨¬r}, α = p∧q∧r and β = q∧r. Obviously, α ⊢ β and PI(β) ⊆ PI(α). We have Iprob(α, K) = 2 - 0 = 2, while Iprob(α, K ⊖ α ⊕ β) = 4 - 0 = 4, here a violation of dominance and weak dominance.

Noticeably, the two local measures Imi and Iprob look like reproducing, at a first glance, the same behavior in the sense that for α, β ∈ K, Iprob(α, K) ≤ Iprob(β, K) iff Imi(α, K) ≤ Imi(β, K). However, this property does not hold in general as shown in the following example.

Example 7. Consider K = {p, ¬p, q, ¬q ∨ r, ¬r}. Clearly, K has two minimal inconsistent sets, namely {p, ¬p} and {q, ¬q ∨ r, ¬r}. Then, we have Iprob(p,K) = 2 < Iprob(q, K) = 3, but Imi(p, K) = 1/2 > Imi(q, K) = 1/3.

Recall that the local measure Iprob is too restrictive since it considers only the formulas of the minimal conflicts of α that do not appear in any other minimal inconsistent sets of K. To make a more generalized version of this problematic-based measure, we present below a second more accurate variant of Iprob.

Definition 5. Where α ∈ K let define the extended problematic-based local measure of α, denoted I + prob , is defined as:

Intuitively, the local measure I + prob computes all formulas contained in any minimal inconsistent set that also involves α. Note that in contrast to Iprob, this measure satisfies (strict) monotonicity and centrality conflict. Nevertheless, the dominance postulate remains unsatisfiable.

Example 8. Consider K = {p, ¬q, ¬p ∧ q}. Clearly, K has two minimal inconsistent sets: {p, ¬p ∧ q} and {¬q, ¬p ∧ q}. Then, Iprob(p, K) = 3 - 2 = 1, however I + prob (p, K) = 2.

Example 8 shows that, unlike Iprob, I + prob only considers those problematic formulas which are relevantly conflicting relative to p: ¬q does not matter in the computation of I + prob . Note that, differently from Iprob, the (strict) monotonicity property holds for the I + prob local measure.

Proposition 5. The local measure I + prob satisfies SyntaxIndependence, Blameless, Guiltless, Logical Invariance, Monotonicity, Strict Monotonicity, Free Formula Independence, Centrality Conflict, Minimality and Maximality.

Proof excerpt. Monotonicity. Since mi(α,K) ⊆ mi(α,K ⊕ β), ⋃M∈mi(α,K) M ⊆ ⋃M∈mi(α,K⊕β) M. Then, I + prob (α, K) ≤ I + prob (α, K ⊕ β).

Strict Monotonicity. If mi(α,K) ⊂ mi(α,K ⊕ β), then β ̸∈ ⋃M∈mi(α,K) M and β ∈ ⋃M∈mi(α,K⊕β) M. Moreover, since ⋃M∈mi(α,K) M ⊆ ⋃M∈mi(α,K⊕β) M, we conclude that I + prob (α, K) < I + prob (α, K ⊕ β).

Nevertheless, the I + prob measure violates the dominance property. In fact, weakening a formula can give rise to the appearance of new conflicts in a knowledge base. This is a trivial reason behind the violation of the (conjunctive/weak) dominance property.

Example 9. Let K = {p ∧ q ∧ r, ¬p, p, ¬q, p ∨ ¬r}, α = p ∧ q ∧ r and β = q ∧ r. We have α ⊢ β, PI(β) ⊆ PI(α), I + prob (α, K) = 3 and I + prob (β, K⊖α⊕β) = 4. Consequently, I + prob (α,K) < I + prob (β,K). This shows that dominance and weak dominance are violated for I + prob .

Example 10. Let K = {q∧r, ¬p, p¬q, p∨¬r} and α = q∧r. We have I + prob (α, K) = 4. Let β = p. Then, I + prob (α ∧ β, K ⊖ α⊕α∧β) = 3, illustrating a failure of conjunctive dominance for I + prob .

To overcome issues with weak and conjunctive dominance, we propose to extend the I + prob measure by considering the formulas that conflict with α both directly and indirectly. More specifically, the new local measure IPI introduced below considers all the formulas that participate explicitly and implicitly to create conflicts in the knowledge base. This can be achieved under special consideration of prime implicates.

Definition 6. Where α ∈ K we define the prime implicate based conflict set of α in K as: ConfPI(α,K) = ⋃{M ⊆ K ⊖ β | PI(β) ⊆ PI(α),M ⊕ β ∈ mi(β,K ⊕ β)}. Then, the prime implicate-based local measure of α, denoted IPI, is defined as:

Let us note that requiring that PI(β) ⊆ PI(α) allows us to avoid blaming innocent formulas. In fact, we cannot consider the condition α ⊢ β instead of PI(β) ⊆ PI(α). For instance, if we consider K = {p, ¬p, q}, we have IPI(p) = 1, while if we were to replace PI(β) ⊆ PI(α) by α ⊢ β, we would also have to consider p ⊢ p∨¬q and thus the less relevant conflict {p ∨ ¬q, ¬p, q} leading to an inconsistency value for p of 2.

Proposition 6. The local measure IPI satisfies SyntaxIndependence, Blameless, Guiltless, Logical Invariance, Monotonicity, Strict Monotonicity, Minimality, Maximality, Minimality, Dominance, Conjunctive, and Weak Dominance.

Proof excerpt. Weak dominance. Let α ∈ K and PI(β) ⊆ PI(α). Then, one can show that ⋃({M ⊆ (K ⊖ α ⊕ β) ⊖ γ | PI(γ) ⊆ PI(β)M ⊕ γ ∈ mi(γ,K ⊖ α ⊕ β ⊕ γ)} ⊆ ⋃({M ⊆ K ⊖ γ | PI(γ) ⊆ PI(α) M ⊕ γ ∈ mi(γ, K ⊕ γ)}. Consequently, IPI(β, K) ≤ IPI(α, K).

Example 11. Let K = {p∧q∧r, ¬p, p∨¬q∨¬r}, α = p∧ q ∧ r and β = q ∧ r. There is no subset M ⊆ K that conflicts β. Now, let M = {¬p, p ∨ ¬q ∨ ¬r}. Clearly, M ⊂ K⊖ β. Moreover, PI(β) ⊆ PI(α) and M ⊕ β ∈ mi(β,K ⊕ β). By Definition 6, all the formulas of M are considered in the computation of the inconsistency value of α. This illustrates a violation of the free formula independence, since p ∨ ¬q ∨ ¬r ∈ free(K).

The next example shows the independence of dominance and conjunctive dominance properties.

Example 12. Let K = {p, ¬p, q} and α = p. We have IPI(α,K) = 1. Let β = p ∨ ¬q. We have α ⊢ β and IPI(β,K ⊖ α ⊕ β) = 2 since K ⊖ α ⊕ β = {p ∨ ¬q, ¬p, q} consisting of a single minimal inconsistent set. Thus, IPI(α,K) < IPI(β,K). So, IPI violates the dominance postulate.

Next, we propose a new class of local measures that satisfy at least the free formula independence, monotonicity, and dominance postulates. Moreover, we prove in our principlebased study (Table 1) that one of our new measures, named I℘, satisfies all the proposed criteria.

4.2 Freeness and Conflict-based Local Measures

We now move on to the second class of local measures. To start this, let us first recall that free formulas belong to all maximal consistent sets of the knowledge base. Clearly, the contraction of free formulas leaves the set of minimal inconsistent sets, and thus the set of problematic formulas, of the original base unchanged. Then, the contribution of a (nonfree) formula α to the overall conflict of a knowledge base K can be measured by its impact on the "freeness" when α is retracted from K. Based on this observation, a way to compute the inconsistency of a formula is to evaluate the cost required to make it free while maximizing the remaining problematic formulas of K. In other words, we determine the number of problematic formulas that remain in K after the removal of a minimal subset of formulas from K to make α free. This allows us to quantify the portion of conflicts in K that depend essentially on the presence of α in K. It gives rise to the local measure Ifree defined as follows.

Definition 7. Where α ∈ K we define the freeness-based measure of α, denoted Ifree:

In words, the local measure Ifree assesses the cost associated with making α free (i.e., resolving conflicts within α) in K. Now, we provide a characterization of the Ifree measure through the notion of conflict-hitting-set.

Where α ∈ K we let M ⊆ prob(K) \ {α} be a conflicthitting-set (CHS, for short) for α in K iff for every M ′ ∈ mi(α, K), M ′ ∩M ̸= ∅. A CHS M for α in K is minimal iff |M| is minimal among all CHSs for α in K.

Fact 1. Let α ∈ K\⊥(K). Then, there is a minimal CHS for α in K.

Proposition 7. Let α ∈ K \ ⊥(K). Then, Ifree(α, K) = |M| for any minimal CHS M for α in K.

Proof. Let M be a minimal CHS for α in K and let N ⊆ prob(K)\{α} be such that α ∈ free(K\N) and Ifree(α, K) = |N|. Then, M ⊆ prob(K) \ {α}. Assume for a contraction, that α /∈ free(K \M). So, there is an M ′ ∈ mi(α,K \M). But then M ′ ∈ free(α,K) and so M ∩M ′ ̸= ∅, which is a contraction. So, α ∈ free(K \M) and hence, |N| ≤ |M| by the minimality of N.

We now show that N is a CHS for α in K. Let for this M ′ ∈ mi(α, K). Assume for a contradiction that M ′∩N = ∅. But thenM ′ ∈ mi(α,K\N) and so α /∈ free(K\N). This is a contradiction. So N is a CHS for α in K. By the minimality of M therefore |M| ≤ |N|. Altogether |M| = |N|.

Proposition 8. Let α ∈ K \⊥(K). Then, we have:

Proposition 9. Ifree satisfies Syntax-Independence, Blameless, Guiltless, Logical Invariance, Monotonicity, Free Formula Independence, Maximality, Minimality, Dominance, Conjunctive Dominance, and Weak Dominance.

Proof excerpt. Monotonicity. Let α ∈ ⊥(K ∪ K′ ). Then, Ifree(α, K) ≤ |prob(K)| ≤ |prob(K∪K′ )| = Ifree(α, K∪K′ ). Let α ∈ K \ ⊥(K ∪ K′ ). So, by Proposition 7, Ifree(α, K ∪ K′ ) = |M| for some minimal CHS M for α in K ∪ K′ . Note that mi(α, K) ⊆ mi(α, K ∪ K′ ), and therefore M is also an CHS for α in K. Thus, by Proposition 7, Ifree(α, K) ≤ |M|.

Dominance. Let α ⊢ β and α ⊬ ⊥. Let M ∈ mi(β, K ⊖ α ⊕ β). So, M ⊢ ⊥ and since α ⊢ β also M ⊖ β ⊕ α ⊢ ⊥. Also, M ⊖ β ⊬ ⊥. So, there is a M ′ ⊆ M such that M ′ ⊕ α ∈ mi(α,K). Thus, for every CHS M for α in K, there is an M ′ ⊆ M that is an CHS for β in K ⊖ α ⊕ β. So, where M is a minimal CHS for β in K ⊖ α ⊕ β and M ′ is a minimal CHS for α in K, |M| ≤ |M ′ . By Prop. 7, Ifree(β, K ⊖ α ⊕ β) ≤ Ifree(α, K).

Conjunctive Dominance. Let α ∈ K. Note that where N ∈ mi(α, K), N ⊖ α ⊕ α ∧ β ⊢ ⊥ and N ⊖ α ⊬ ⊥. So, there is a N ′ ⊆ N ⊖ α such that N ′ ⊕ α ∧ β ∈ mi(α ∧ β,K ⊖ α ⊕ α ∧ β). This implies that every CHS for α ∧ β in K ⊖ α ⊕ α ∧ β is also a CHS for α in K. Thus, where M is a minimal CHS for α in K and M ′ is a minimal CHS for α ∧ β in K ⊖ α ⊕ α ∧ β, |M| ≤ |M ′ |. By Proposition 7, Ifree(α, K) ≤ Ifree(α ∧ β, K ⊖ α ⊕ α ∧ β).

Example 13. Let K = {p, q∧q′ , ¬(p∧q), ¬(p∧q′ )}. Then, K ⊖ p ⊬ ⊥ and K ⊖ ¬(p ∧ q) ⊢ ⊥. Nevertheless, Ifree(p) = 1 = Ifree(¬(p ∧ q)) in violation of centrality conflict.

Interestingly, we show next that there is a local measure that satisfies all the postulates considered in this paper. Intuitively, our measure can be considered in the spirit of the previous prime implicate-based measure. It takes into account all consistent subsets involved in generating conflicts with the formula α.

Definition 8. Let Conf(α,K) = {M ⊆ K ⊖ α | (∃M ′ ⊆ M)M ′ ⊬ ⊥ and M ′ ⊕ α ⊢ ⊥} and ℘(K) the powerset of K. The conflict-based local measure, denoted I℘, is defined as:

Intuitively, the set Conf(α,K) considers all consistent sets of formulas in K that conflict with α. Since this leads to double counting (in terms of also computing strict supersets of sets conflicting with α), we normalize by dividing through the size of the powerset of K. Now, one can rewrite the conflictbased local measure as:

Proposition 10. The local measure I℘ satisfies SyntaxIndependence, Blameless, Guiltless, Logical Invariance, Monotonicity, Strict Monotonicity, Free Formula Independence, Minimality, Maximality, Centrality Conflict, Dominance, Conjunctive Dominance, and Weak Dominance.

Proof excerpt. Monotonicity. We note that Conf(α,K) ⊆ {M ⊕ β | M ∈ Conf(α, K)} ∪ Conf(α, K) ⊆ Conf(α, K ⊕ β) and so I℘(α,K) = |Conf(α,K)| |℘(K)| = 2·|Conf(α,K)| 2·|℘(K)| = |Conf(α,K)|+|{M⊕β|M∈Conf(α,K)}| |℘(K⊕β)| ≤ |Conf(α,K⊕β)| |℘(K⊕β)| = I℘(α, K ⊕ β).

Strict Monotonicity. Suppose mi(α,K) ⊂ mi(α,K ⊕ β). Thus, β /∈ K. Since Conf(α, K) ⊆ Conf(α, K⊕β) and there is a M ∈ Conf(α, K ⊕ β) for which β ∈ M, Conf(α, K) ⊆ {M ⊕ β | M ∈ Conf(α, K)} ∪ Conf(α, K) ⊂ Conf(α, K ⊕ β). So, I℘(α,K) = |Conf(α,K)| |℘(K)| = 2·|Conf(α,K)| 2·|℘(K)| = |Conf(α,K)|+|{M⊕β|M∈Conf(α,K)}| |℘(K⊕β)| < |Conf(α,K⊕β)| |℘(K⊕β)| = I℘(α,K⊕β). So, I℘(α,K) < I℘(α,K⊕β).

Centrality Conflict. Suppose α, β ∈ K, K ⊖ α ⊬ ⊥ and K ⊖ β ⊢ ⊥. We note that Conf(β, K) = {M ∈ Conf(β, K) | α ∈ M} ∪ {M ∈ Conf(β, K) | α /∈ M}. Since K ⊖ α ⊬ ⊥, {M ∈ Conf(β,K) | α /∈ M} = ∅ and so Conf(β,K) = {M ∈ Conf(β, K) | α ∈ M}.

We now show that for every M ∈ Conf(β, K), M ⊖ α ⊕ β ∈ Conf(α, K) and therefore |Conf(α, K)| ≥ |Conf(β, K)|. Let M ∈ Conf(β,K). So, there is a M ′ ⊆ M for which M ′ ⊕β ⊢ ⊥ while M ′ ⊬ ⊥. So, α ∈ M ′ , M ′ ⊖α, β ⊬ ⊥ and M ′ ⊖α⊕β ⊕α ⊢ ⊥ and therefore M ⊖α⊕β ∈ Conf(α, K).

We also note that K⊖α⊖β⊕α ⊢ ⊥ while K⊖α⊖β ⊬ ⊥ and therefore K ⊖ β ∈ Conf(α,K). So, |Conf(α,K)| ≥ |{K ⊖ β}| + |{M ⊖ α ⊕ β | M ∈ Conf(β,K)}| > |Conf(β, K)|. Thus, I℘(α, K) > I℘(β, K).

Maximality. Suppose α ∈ ⊥(K). So, Conf(α,K) = ℘(K ⊖ α). For every β ∈ K, Conf(β,K) ⊆ ℘(K ⊖ β). So, I℘(α,K) = |℘(K⊖α)| |℘(K)| = 12 ≥ |Conf(β,K)| |℘(K)| = I℘(β,K).

Dominance. Suppose α ⊢ β and let n = |℘(K)|. Let M ∈ Conf(β, K⊖α⊕β). So, M ⊆ K⊖α⊖β and there is a M ′ ⊆ M for which M ′ ⊬ ⊥ and M ′ ⊕β ⊢ ⊥. So, M ′ ⊕α ⊢ ⊥ and so M ∈ Conf(α,K). Thus, |Conf(α,K)| ≥ |Conf(β,K ⊖ α ⊕ β)| and so I℘(α, K) = |Conf(α,K)| n ≥ |Conf(β,K⊖α⊕β)| n = |Conf(β,K⊖α⊕β)| |℘(K⊖α⊕β)| = I℘(β,K⊖α⊕β).

5 Concluding Remarks

In this paper, we have analysed existing and new local inconsistency measures in the propositional logic setting by means of a postulate-based evaluation and comparison. We investigated several rationales to local measures, based on free and problematic formulas. Ultimately, we identified one measure, I℘ that outperforms previous attempts by satisfying all presented postulates.

Our paper opens potentially fruitful future research: we will investigate characterization results for postulate-based studies of local measures, the relation between local and global measures (e.g. issues of interdefinabilitiy) as well as applications of local measures, e.g., in the context of belief revision and deontic logic.

Acknowledgments

This work was funded, in part, by the Agence Nationale de la Recherche ANR under grant EXPIDA: ANR-22-CE23-0017.