Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Inconsistency measures have gained much interest recently (Ammoura et al. 2015; Grant and Hunter 2013; Hunter et al. 2014; Jabbour et al. 2015, 2016; Liu and Mu 2016; McAreavey et al. 2014; Mu et al. 2012; Mu 2015; Thimm 2013, 2016a, 2016b; Thimm and Wallner 2016; Xiao and Ma 2012). An inconsistency measure ascribes a quantity to a logical knowledge base, a quantity which is meant to tell how inconsistent the knowledge base is. Here, we apply forgetting (Lin and Reiter 1994), a well-known method to restore consistency (Lang and Marquis 2002), in order to get a new inconsistency measure from the following idea: How much effort is needed to restore consistency of a knowledge base is presumably indicative of how inconsistent the knowledge base is.

1.1 Formal Preliminaries

By a knowledge base, we mean a finite multiset of formulas of propositional logic. We use \(\lnot \), \(\wedge \), \(\vee \) to denote the usual Boolean connectives: negation, conjunction, disjunction. We use Greek letters \(\varphi , \psi , \ldots \), whether indexed or not, to denote formulas of propositional logic. We use capital Greek letters \(\varDelta , \varGamma \),... to denote knowledge bases (i.e., multisets of formulas of propositional logic, as just said). We use \(\kappa \) (which is introduced in Definition 1) to denote forgetting: Intuitively, \(\kappa \) “forgets” occurrences of a propositional variable.

2 An Inconsistency Measure

We consider formulas labelled with superscripts denoting occurrences of atoms. Every formula \(\varphi \) in which an unlabelled atom v occurs \(k > 0\) times is identified as \(\varphi (v^1,\ldots ,v^k)\) where \(v^i\) denotes the ith unlabelled occurrence of v in \(\varphi \).Footnote 1

Example.  The unlabelled formula \(a\,\wedge \,b\,\wedge \,\lnot \,b\) is identified with the labelled formula \(a^1 \wedge b^1 \wedge \lnot b^2\).

Accordingly, given the list of propositional variables \(\mathcal {P} = v_1, v_2,\ldots \) define the set of atom occurrences as

$$\begin{aligned} \mathcal {A} \mathop {=}\limits ^{\mathrm {def}} \bigcup _{v \in \mathcal {P}} \{v^1,v^2,\ldots \} \end{aligned}$$

Importantly, \(v^i\) is identified with \(v^j\) for all purposes (e.g., consistency issues) except for purposes of occurrences of atoms. In particular, a Boolean combination of labelled formulas may display multiple copies of the same atom occurrence e.g., \((a^1 \wedge b^1 \wedge \lnot b^2)\left| \begin{array}{c@{}}{b^{1} \rightarrow \top ,\bot }\end{array}\right. \!\) (see below) is \((a^1 \wedge \top \wedge \lnot b^2) \vee (a^1 \wedge \bot \wedge \lnot b^2)\).

Notation. The symbol \(\rightarrow \) is used for substitution as follows.

$$ \varphi \left| \begin{array}{c}{\scriptstyle v_1^{i_1} \rightarrow ~\psi _{1}}\\ {\scriptstyle \vdots }\\ {\scriptstyle v_k^{i_h} \rightarrow ~\psi _{h}}\end{array}\right. $$

denotes the formula resulting from \(\varphi \) by replacing simultaneously each atom occurrence \(v_j^{i_j}\) by \(\psi _j\) (informally speaking, an atom occurrence refers either to an unlabelled occurrence of the atom or to a labelled version of the atom). The abbreviation

$$ \bigvee _1^m \varphi \left| \begin{array}{c}{\scriptstyle v^{i} \rightarrow ~\psi _1,\ldots ,\psi _m}\end{array}\right. $$

is used to denote the disjunction whose each disjunct is the formula obtained from \(\varphi \) by replacing \(v^{i}\) by one of \(\psi _1,\ldots ,\psi _m\) in turn.

Example.  Taking \(\varphi \) to be \(a^1 \wedge b^1 \wedge \lnot b^2 \wedge (b^3 \vee \lnot (a^1 \wedge b^1))\), the substitution of \(b^1\) by \(\top \) in \(\varphi \) is denoted by \(\varphi \left| {(\scriptstyle b^{1} \rightarrow ~\top )}\right. \), yielding \(a^1 \wedge \top \wedge \lnot b^2 \wedge (b^3 \vee \lnot (a^1 \wedge \top ))\). That is, all occurrences of \(b^1\) in \(\varphi \) are replaced by occurrences of \(\top \). Also, \(\bigvee \varphi \left| \begin{array}{c}{\scriptstyle b^{1} \rightarrow ~\top ,\bot }\end{array}\right. \) denotes \([a^1 \wedge \top \wedge \lnot b^2 \wedge (b^3 \vee \lnot (a^1 \wedge \top ))] \vee [a^1 \wedge \bot \wedge \lnot b^2 \wedge (b^3 \vee \lnot (a^1 \wedge \bot ))]\).

Definition 1

\(\kappa _{i,v} . \varphi \) is the labelled formula obtained from the labelled formulaFootnote 2 \(\varphi \) by replacing the atom occurrences \(v^{i}\) in \(\varphi \), first by \(\top \), second by \(\bot \), taking the disjunction thereof. In symbols,

$$\begin{aligned} \kappa _{i,v} . \varphi \mathop {=}\limits ^{\mathrm {def}} \varphi (v^1,\ldots ,v^{i-1},\top ,v^{i+1},\ldots ,v^k) \vee \varphi (v^1,\ldots ,v^{i-1},\bot ,v^{i+1},\ldots ,v^k) \end{aligned}$$

For clarity, let us stress that \(\kappa _{i,v} . \varphi \) is a labelled formula hence \(\kappa _{j,u} . (\kappa _{i,v} . \varphi )\) is such that \(\kappa _{j,u}\) introduces no superscript (but it duplicates superscripted atoms).

Lemma 1

  Using the substitution notation,

$$ \kappa _{i_1,v_1}. \kappa _{i_2,v_2} . \cdots . \kappa _{i_h,v_h} . \varphi = \bigvee _{1}^{2^h} \varphi \left| \begin{array}{c}{\scriptstyle v_1^{i_1} \rightarrow \top ,\bot }\\ {\scriptstyle \vdots }\\ {\scriptstyle v_h^{i_h} \rightarrow \top ,\bot }\end{array}\right. $$

In previous work (Lin and Reiter 1994; Lang and Marquis 2002; Lang et al. 2003) about forgetting, it is shown that consistency can be recovered if enough atoms are forgotten. It is of interest to characterize which occurrences of atoms are enough to consider if consistency is to be recovered.

Definition 2

  Define \(\sigma (\varphi )\) as the set of multisets of atom occurrences whose forgetting is enough to turn \(\varphi \) into a consistent formula, in symbols,

Then, the inconsistency number of \(\varphi \) is intuitively the minimum number n of (iterated) applications of \(\kappa \) operators such that i.e. such that \(\varphi \) is turned into a consistent formula.

Definition 3

  The inconsistency number of \(\varGamma \) is \(n(\varGamma )\), defined as

$$ n(\varGamma ) \mathop {=}\limits ^{\mathrm {def}} \min _{A \in \sigma (\wedge \tiny {\varGamma })} \mid A \mid $$

Reminder. Before turning to the examples, it is important to repeat that \(v^i\) is identified with \(v^j\) for most purposes, including consistency issues. For instance, in Example 2, \((\top \wedge a^2) \wedge (\lnot a^3 \wedge \lnot a^4)\) is inconsistent because it is identified with \((\top \wedge a^i) \wedge (\lnot a^i \wedge \lnot a^i)\) which is inconsistent, whatever i.

Example 1

Let \(\varGamma _1 = \{a \vee a, \lnot a \vee \lnot a\}\). Then, \(\bigwedge \varGamma _1 = (a^1 \vee a^2) \wedge (\lnot a^3 \vee \lnot a^4)\). \(\{a^1\} \in \sigma (\varGamma _1)\) since \(\kappa _{1,a} . \bigwedge \varGamma _1\) is \([(\top \vee a^2) \wedge (\lnot a^3 \vee \lnot a^4)] \vee [(\bot \vee a^2) \wedge (\lnot a^3 \vee \lnot a^4)]\) which is consistent. Hence \(n(\varGamma _1) = 1\).

Example 2

Let \(\varGamma _2 = \{a \wedge a, \lnot a \wedge \lnot a\}\). Hence, \(\bigwedge \varGamma _2 = (a^1 \wedge a^2) \wedge (\lnot a^3 \wedge \lnot a^4)\). It does not matter whether considering \(a^1\) instead of \(a^2\) and \(a^3\) instead of \(a^4\). \(\kappa _{1,a} . \bigwedge \varGamma _2\) is \([(\top \wedge a^2) \wedge (\lnot a^3 \wedge \lnot a^4)] \vee [(\bot \wedge a^2) \wedge (\lnot a^3 \wedge \lnot a^4)]\) which is inconsistent. \(\kappa _{3,a} . \kappa _{1,a} . \bigwedge \varGamma _2\) is \([(\top \wedge a^2) \wedge (\lnot \top \wedge \lnot a^4)] \vee [(\bot \wedge a^2) \wedge (\lnot \top \wedge \lnot a^4)] \vee [(\top \wedge a^2) \wedge (\lnot \bot \wedge \lnot a^4)] \vee [(\bot \wedge a^2) \wedge (\lnot \bot \wedge \lnot a^4)]\) i.e. \([\bot \vee \bot ] \vee [\bot \vee \bot ]\) which is inconsistent (and so is \(\kappa _{4,a} . \kappa _{1,a} . \bigwedge \varGamma _2\)). However, \(\kappa _{2,a} . \kappa _{1,a} . \bigwedge \varGamma _2\) is \([(\top \wedge \top ) \wedge (\lnot a^3 \wedge \lnot a^4)] \vee [(\bot \wedge \top ) \wedge (\lnot a^3 \wedge \lnot a^4)] \vee [(\top \wedge \bot ) \wedge (\lnot a^3 \wedge \lnot a^4)] \vee [(\bot \wedge \bot ) \wedge (\lnot a^3 \wedge \lnot a^4)]\) i.e. \([(\lnot a^3 \wedge \lnot a^4) \vee \bot ] \vee [\bot \vee \bot ]\), it is consistent. Hence, \(n(\varGamma _2) = 2\).

Keep in mind that n refers to the minimum amount of forgetting needed to restore consistency. E.g., each of the knowledge bases \(\varGamma \) below satisfies \(n(\varGamma ) = 1\).

$$\begin{array}{c} \{a, \lnot a\} \\ \{a \wedge a, \lnot a\} \\ \{a \vee b, a \vee \lnot b, \lnot a \vee b, \lnot a \vee \lnot b\} \end{array}$$

3 How Inconsistent About v?

Besides determining how inconsistent \(\varGamma \) is, it would be interesting to determine how inconsistent \(\varGamma \) is about some v.

Definition 4

  \(n\!\mid _v\!(\varGamma ) \mathop {=}\limits ^{\mathrm {def}} \min \limits _{A \in \sigma (\wedge \tiny {\varGamma })} \mid A \cap \{v\}_\omega \mid \)

Notation. \(\{v\}_\omega \) denotes the multiset consisting of countably many copies of v.

Example 3

Let \(\varGamma _3 = \{(a \wedge \lnot a) \vee (b \wedge \lnot b)\}\). Therefore, \(\{b^1\} \in \sigma (\varGamma _3)\) because \(\kappa _{1,b} . \bigwedge \varGamma _3\) is \([(a^1 \wedge \lnot a^2) \vee (\top \wedge \lnot b^2)] \vee [(a^1 \wedge \lnot a^2) \vee (\bot \wedge \lnot b^2)]\) which is consistent. Hence, \(n\!\mid _a\!(\varGamma _3) = 0\) due to \(\{b^1\} \cap \{a\}_\omega \) being empty. Similarly, \(n\!\mid _b\!(\varGamma _3) = 0\). However, \(n(\varGamma _3) = 1\).

Comment. The reader may be unhappy that \(n\!\mid _v\!(\varGamma ) = 0\) captures both the case that v is involved in no contradiction in \(\varGamma \) and the case (as in Example 3) that v is involved in a contradiction together with at least another atom. There are many ways to change Definition 4, e.g. by considering some liability function l (with the constraint \(l_{v,\sigma }(\varGamma ) > 1\)) so as to alternatively define \(n\!\mid _v\) as follows:

Anyway, knowledge bases can be compared in the following way: \(\varGamma \) is at least as v -inconsistent as \(\varGamma '\) iff \(n\!\mid _v\!(\varGamma ) \ge n\!\mid _v\!(\varGamma ')\).

Lemma 2

  If \(n(\varGamma ) \ge n(\varGamma ')\) then there exists an atom v such that \(\varGamma \) is at least as v-inconsistent as \(\varGamma '\).

Lemma 3

  \(n(\varGamma ) \ge n(\varGamma ')\) if for every v, \(\varGamma \) is at least as v-inconsistent as \(\varGamma '\).

It is also possible to compare the involvement of atoms in the conflicts of a knowledge base. Therefore, if atoms can be mapped to topics, such a measure \(n\!\mid _v\) would permit to judge whether a topic gives rise to more severe conflicts than some other topic, or to judge whether the overall inconsistency degree of the knowledge base amounts to the inconsistency degree ascribed to such and such topic. (Please keep in mind that “severe” only refers to intensity, there can be a severe conflict about a topic of little importance.)

4 Postulates for Inconsistency Measures

We now turn to examining what postulates are satisfied by our inconsistency measure n. In this respect, a useful lemma is the following one.

Lemma 4

For all \(j \ge h\), if then . If then for all \(j \ge 0\), (hence \(2^\mathcal {A} \subseteq \sigma (\varphi )\) for ).

We begin with considering postulates proposed in Hunter and Konieczny (2010), expressed using I to denote an arbitrary inconsistency measure.

  • \(I(\varGamma ) = 0\) iff (Consistency Null)

  • \(I(\varGamma \cup \varGamma ') \ge I(\varGamma )\) (Monotony)

  • If \(\varphi \) is freeFootnote 3 for \(\varGamma \) then \(I(\varGamma \cup \{\varphi \}) = I(\varGamma )\) (Free Formula Independence)

It happens that our inconsistency measure n satisfies the postulates above. However, n fails the following postulate, also due to (Hunter and Konieczny 2010).

figure a

Example 4

Let \(\varGamma = \{\lnot a \wedge \lnot a \wedge \lnot a\}\). Take \(\varphi = a\) and \(\psi = a \wedge a \wedge a\). Then, \(n(\varGamma \cup \{\varphi \}) = 1\) but \(n(\varGamma \cup \{\psi \}) = 3\).

Failure of (Dominance) entails failure wrt the postulate (Besnard 2014) below

figure b

Furthermore, our inconsistency measure n satisfies the following postulate, introduced in Besnard (2014).

figure c

Keeping in mind that \(\varGamma \) denotes a multiset of formulas, it is easy to check that n satisfies the next postulate also introduced in Besnard (2014).

figure d

Since n satisfies both (Monotony) and (Adjunction Invariancy), it satisfies

figure e

Similarly, an easy consequence of (Free Formula Independence) is

figure f

which our inconsistency measure n satisfies as well as the related postulate (Besnard 2014) below

figure g

5 Conclusion

The inconsistency measure introduced in this paper shows two main distinctive features. First, it deals with multisets of formulas. Second, it breaks the dichotomy suggested in Hunter and Konieczny (2010) which splits the universe of inconsistency measures into two categories: inconsistency measures based on minimal inconsistent subsets and inconsistency measures based on the alphabet (i.e., what atoms are involved in conflicts). Indeed, Example 4 is such that the inconsistency value differs in two cases with isomorphic sets of minimal inconsistent subsets and also differs in two cases where the alphabet consists of one propositional symbol.