Measuring Disagreement with Interpolants

Abstract

We consider the problem of quantitatively assessing the conflict between knowledge bases in knowledge merging scenarios. Using the notion of Craig interpolation we define a series of disagreement measures and analyse their compliance with properties proposed in previous work by Potyka. We study basic complexity theoretic questions in that scenario and discuss the suitability of our approaches .

1 Introduction

Inconsistencies arise easily whenever knowledge has to be aggregated from different sources [2, 3, 14]. Approaches to belief merging and information fusion address these issues by providing computational approaches for automatically resolving these issues in some sensible way. These fields bear a close relationship with the fields of judgement and preference aggregation [8, 20] and also feature their own version of Arrow’s impossibility result [1], insofar that there cannot be any “rational” belief merging approach [7]. This calls for semi-automatic methods that take human background knowledge into account when knowledge has to be merged in order not to remove important pieces of information. In order to support the task of semi-automatic merging, we investigate approaches to analyse belief merging settings, i. e., approaches that can explain reasons for inconsistency and assess their severity. More specifically, we investigate disagreement measures [17], i. e., functions that take a knowledge base profile $P=\langle \mathcal {K}_{1},\ldots ,\mathcal {K}_{n}\rangle$ as input and return a non-negative value that quantifies the severity of the disagreement between the different sources of information modelled by $\mathcal {K}_{1},\ldots ,\mathcal {K}_{n}$. Disagreement measures are closely related to inconsistency measures [9, 18, 19], which themselves are functions that assess the severity of inconsistency in a single knowledge base. Disagreement and inconsistency measures can be used to help in debugging inconsistencies in semi-automated settings [4, 5, 10].

In this paper, we develop novel disagreement measures based on the concept of Craig interpolation [6]. Given two knowledge bases $\mathcal {K}_{1}$, $\mathcal {K}_{2}$ with $\mathcal {K}_{1}\cup \mathcal {K}_{2}$ being inconsistent, an interpolant is a formula that concisely characterises an aspect of this inconsistency (we will provide formal definitions later). Thus, interpolants play a similar role in analysing the disagreement between two knowledge bases as minimal inconsistent subsets do in analysing the inconsistency within a single knowledge base. As a matter of fact, minimal inconsistent subsets play a dominant role in many approaches to measuring inconsistency [12, 15, 21] and, therefore, it seems plausible to explore the use of interpolants in measuring disagreement. In order to do that, we consider the set of all interpolants (up to semantical equivalence) and define measures based on the size of that set and on the information content of the weakest/strongest interpolants (which are well-defined concepts due to the fact that the set of interpolants form a complete lattice). We show that our approaches provide meaningful results and comply with many of the rationality postulates introduced in [17]. We also undertake a small study of the computational complexity of several tasks relevant for our work, showing that (unsurprisingly) all of those are intractable. In summary, the contributions of this paper are as follows:

• 1. We make some general observations on interpolants in order to establish a framework suitable for measuring disagreement (Sect. 3).

• 2. We present novel disagreement measures based on interpolants (Sect. 4).

• 3. We investigate the compliance of these disagreement measures with rationality postulates from the literature (Sect. 5).

• 4. We investigate the computational complexity of several tasks pertaining to our disagreement measures (Sect. 6).

We introduce necessary preliminaries in Sect. 2 and conclude in Sect. 7.

We omit several proofs due to space restrictions. These can be found in an online appendix¹.

2 Preliminaries

Let $\mathsf {At}$ be some fixed propositional signature, i. e., a (possibly infinite) set of propositions, and let $\mathcal {L}(\mathsf {At})$ be the corresponding propositional language constructed using the usual connectives $\wedge$ (conjunction), $\vee$ (disjunction), $\rightarrow$ (implication), and $\lnot$ (negation). A literal is a proposition p or a negated proposition $\lnot p$.

Definition 1

A knowledge base $\mathcal {K}$ is a finite set of formulas $\mathcal {K}\subseteq \mathcal {L}(\mathsf {At})$. Let $\mathbb {K}$ be the set of all knowledge bases.

A clause is a disjunction of literals. A formula is in conjunctive normal form (CNF) if the formula is a conjunction of clauses. If $\varPhi$ is a formula or a set of formulas we write $\mathsf {At}(\varPhi )$ to denote the set of propositions appearing in $\varPhi$. For a set $\varPhi =\{\phi _{1},\ldots , \phi _{n}\}$ let $\bigwedge \varPhi = \phi _{1}\wedge \ldots \wedge \phi _{n}$ and $\lnot \varPhi = \{\lnot \phi \mid \phi \in \varPhi \}$.

Semantics for a propositional language is given by interpretations where an interpretation $\omega$ on $\mathsf {At}$ is a function $\omega :\mathsf {At}\rightarrow \{\mathsf {true},\mathsf {false}\}$. Let $\varOmega (\mathsf {At})$ denote the set of all interpretations for $\mathsf {At}$. An interpretation $\omega$ satisfies (or is a model of) an atom $a\in \mathsf {At}$, denoted by $\omega \models a$, if and only if $\omega (a)=\mathsf {true}$. The satisfaction relation $\models$ is extended to formulas in the usual way. For $\varPhi \subseteq \mathcal {L}(\mathsf {At})$ we also define $\omega \models \varPhi$ if and only if $\omega \models \phi$ for every $\phi \in \varPhi$.

In the following, let $\varPhi ,\varPhi _{1},\varPhi _{2}$ be formulas or sets of formulas. Define the set of models $\mathsf {Mod}(\varPhi )=\{\omega \in \varOmega (\mathsf {At})\mid \omega \models \varPhi \}$. We write $\varPhi _{1}\models \varPhi _{2}$ if $\mathsf {Mod}(\varPhi _{1})\subseteq \mathsf {Mod}(\varPhi _{2})$. $\varPhi _{1},\varPhi _{2}$ are equivalent, denoted by $\varPhi _{1}\equiv \varPhi _{2}$, if and only if $\mathsf {Mod}(\varPhi _{1})=\mathsf {Mod}(\varPhi _{2})$. Define the closure $\mathsf {Cn}(\varPhi )$ of a formula or set of formulas $\varPhi$ via $\mathsf {Cn}(\varPhi )=\{\phi \mid \varPhi \models \phi \}$. If $\mathsf {Mod}(\varPhi )=\emptyset$ we also write $\varPhi \models \perp$ and say that $\varPhi$ is inconsistent (or unsatisfiable).

3 Craig Interpolants

An important result in first-order logic is Craig’s Interpolation Theorem [6].

Theorem 1

[6]. Let $\phi ,\psi$ be closed formulæ such that $\phi \models \psi$. Then there exists a closed formula I containing only predicate symbols, function symbols and constants occurring in both $\phi$ and $\psi$ such that $\phi \models I$ and $I \models \psi$.

Every formula I satisfying the property in Theorem 1 will be called an interpolant of $\phi$ and $\psi$. In the context of propositional logic, and of finite sets of propositional formulas, the concept of interpolant specializes as follows:

Definition 2

Let $\varPhi$ and $\varPhi '$ be finite sets of propositional logic formulas. A formula $\phi$ is called an interpolant of $\varPhi$ wrt. $\varPhi '$ if

• 1. $\varPhi \models \phi$,

• 2. $\varPhi '\cup \{\phi \}\models \perp$, and

• 3. $\mathsf {At}(\phi )\subseteq \mathsf {At}(\varPhi )\cap \mathsf {At}(\varPhi ')$

Consider, for instance, two sets $\varPhi _1 = \{ r \vee \lnot p, \lnot r \vee \lnot q\}$ and $\varPhi _2 = \{ p, q\}$. The formula $p \rightarrow \lnot q$ is an interpolant of $\varPhi _1$ wrt $\varPhi _2$, as $\varPhi _1 \models p \rightarrow \lnot q$, $\varPhi _2 \cup \{p \rightarrow \lnot q \} \models \perp$ and $\mathsf {At}(\{p\rightarrow \lnot q\}) = \{p,q \} \subseteq \mathsf {At}(\varPhi _1) \cap \mathsf {At}(\varPhi _2)$.

Clearly, two finite sets $\varPhi$ and $\varPhi '$ of formulas in propositional logic have an interpolant if and only if $\varPhi \cup \varPhi '$ is unsatisfiable. Let $\mathbb {I}(\varPhi ,\varPhi ')$ denote the set of interpolants of $\varPhi$ and $\varPhi '$.

Let $\varphi$ be a formula and x a propositional symbol, we write $\varphi [x \mapsto \top ]$ to denote that all occurrences of x in $\varphi$ are replaced by $\top$. Analogously, $\varphi [x \mapsto \perp ]$ means that all ocurrences of x are replaced by $\perp$. For instance, for the formula $\varphi = p \vee \lnot q$, we get $\varphi [p \mapsto \top ] \equiv \top \vee \lnot q$.

Definition 3

Let $\phi$ be a propositional formula and $x \in \mathsf {At}(\phi )$. We use the following notation:

• $\exists x \, \phi := \phi [x \mapsto \mathsf{\perp }] \vee \phi [x \mapsto \mathsf{\top } ]$;

• $\forall x \, \phi := \phi [x \mapsto \mathsf{\perp }] \wedge \phi [x \mapsto \mathsf{\top }]$.

Let $\varPhi$ be a finite set of propositional formulæ, and let $\phi$ be the conjunction of all the formulæ in $\varPhi$. For every $x \in \mathsf {At}(\phi )$, we use the following notation $\exists x \varPhi := \exists x \phi$, $\forall x \varPhi := \forall x \phi$.

Propositional logic allows uniform interpolation: For every formula $\phi$ and every set $\{ y_1, \dots , y_m \} \subseteq \mathsf {At}(\phi )$ there exists a propositional formula $I_{\varPhi }$ such that $\mathsf {At}(I_{\varPhi }) \subseteq \{ y_1, \dots , y_m \}$ with the property that for every formula $\phi '$ such that $\phi \wedge \phi ' \models \perp$ and $\{ y_1, \dots , y_m \} = \mathsf {At}(\phi ) \cap \mathsf {At}(\phi ')$, $I_{\varPhi }$ is an interpolant of $\phi$ and $\phi '$. This follows from the following result (here formulated for finite sets of propositional formulæ).

Proposition 1

Let $\varPhi$ be a finite set of propositional formulas. Assume that $\mathsf {At}(\varPhi ) = \{ x_1, \dots , x_n, y_1, \dots , y_m \}$. Then the following hold:

• 1. $\varPhi \models \exists x_1 \dots \exists x_n \varPhi$.

• 2. Let $\psi$ be a propositional formula with $\mathsf {At}(\psi )\subseteq \{ y_1, \dots , y_m \}$ such that $\varPhi \models \psi$. Then $\exists x_1 \dots \exists x_n \varPhi \models \psi$.

• 3. $\forall x_1 \dots \forall x_n \varPhi \models \varPhi$ (i.e. $\forall x_1 \dots \forall x_n \varPhi \models \phi _i$ for every formula $\phi _i \in \varPhi$).

• 4. Let $\psi$ be a formula with $\mathsf {At}(\psi )\subseteq \{ y_1, \dots , y_m \}$ such that $\psi \models \varPhi$. Then $\psi \models \forall x_1 \dots \forall x_n \varPhi$.

In the following, we define some auxiliary notions for interpolants and make some first observations regarding the structure of $\mathbb {I}(\varPhi ,\varPhi ')$.

Proposition 2

Let $\varPhi$ and $\varPhi '$ be finite sets of formulas.

• 1. If $\varPhi \cup \varPhi '\not \models \perp$ then $\mathbb {I}(\varPhi ,\varPhi ')=\emptyset$.

• 2. If $\varPhi \models \perp$ and $\varPhi '\models \perp$ then $\mathbb {I}(\varPhi ,\varPhi ')=\mathcal {L}(\mathsf {At}(\varPhi )\cap \mathsf {At}(\varPhi '))$.

• 3. If $\varPhi \models \perp$ and $\varPhi '\not \models \perp$ then $\mathbb {I}(\varPhi ,\varPhi ')=\mathcal {L}(\mathsf {At}(\varPhi )\cap \mathsf {At}(\varPhi ')) \cap \bigl (\lnot \mathsf {Cn}(\varPhi ')\cup \{\phi \mid \phi \models \perp \}\bigr )$.

• 4. If $\varPhi \not \models \perp$ and $\varPhi '\models \perp$ then $\mathbb {I}(\varPhi ,\varPhi ')=\mathcal {L}(\mathsf {At}(\varPhi )\cap \mathsf {At}(\varPhi ')) \cap \mathsf {Cn}(\varPhi )$.

Proof

(1) Assume that $\mathbb {I}(\varPhi ,\varPhi ') \ne \emptyset$. Then there exists a formula $\phi$ such that $\varPhi \models \phi$ and $\varPhi '\cup \{\phi \}\models \perp$. Hence, $\varPhi \cup \varPhi ' \models \perp$.

(2) If $\varPhi \models \perp$ and $\varPhi '\models \perp$ then (i) $\varPhi \models \phi$ for all $\phi \in \mathcal {L}(\mathsf {At}(\varPhi )\cap \mathsf {At}(\varPhi '))$ and (ii) $\varPhi ' \cup \{ \phi \} \models \perp$ for all $\phi \in \mathcal {L}(\mathsf {At}(\varPhi )\cap \mathsf {At}(\varPhi '))$.

(3) If $\varPhi \models \perp$ then $\varPhi \models \phi$ for all $\phi \in \mathcal {L}(\mathsf {At}(\varPhi )\cap \mathsf {At}(\varPhi '))$. If $\varPhi '\not \models \perp$ then $\varPhi ' \cup \{ \phi \} \models \perp$ for all $\phi$ such that (i) $\phi = \lnot \phi '$, where $\phi ' \in \mathsf {Cn}(\varPhi ')$ or (ii) $\phi \models \perp$.

(4) If $\varPhi \not \models \perp$ and $\varPhi '\models \perp$ then a formula $\phi$ is an interpolant iff $\varPhi \models \phi$ and $\phi \in \mathcal {L}(\mathsf {At}(\varPhi )\cap \mathsf {At}(\varPhi '))$.

As the notion of an interpolant is a syntactical one, the set $\mathbb {I}(\varPhi ,\varPhi ')$ also contains infinite syntactical variants for each interpolant (except for the case where $\varPhi \cup \varPhi '$ is consistent); in particular, if $\phi \in \mathbb {I}(\varPhi ,\varPhi ')$ then for every formula $\phi ' \in \mathcal {L}(\mathsf {At}(\varPhi )\cap \mathsf {At}(\varPhi '))$, if $\phi \equiv \phi '$ then $\phi ' \in \mathbb {I}(\varPhi ,\varPhi ')$. However, we will consider the following finite representation of $\mathbb {I}(\varPhi ,\varPhi ')$. For that, let $[\cdot ]:\mathcal {L}(\mathsf {At}) \rightarrow \varOmega (\mathsf {At})$ be a function that maps each formula to its equivalence class w.r.t. $\equiv$.

Definition 4

Let $\varPhi$ and $\varPhi '$ be finite set of formulas. We denote by $\mathbb {SI}(\varPhi ,\varPhi ')$ the set of equivalence classes of interpolants wrt. semantical equivalence, i. e.,

$$\begin{aligned} \mathbb {SI}(\varPhi ,\varPhi ')&= \{ [\phi ] \mid \phi \in \mathbb {I}(\varPhi ,\varPhi ')\} \end{aligned}$$

In the following, by abuse of notation we refer to $[\phi ]$ also as an interpolant if $\phi$ is an interpolant.

Remark 1

If the sets $\varPhi , \varPhi '$ of propositional formulæ are finite then the set $\mathsf {At}(\varPhi )\cap \mathsf {At}(\varPhi ')$ is finite, so the set of all equivalence classes of formulæ over this set of atoms is finite and has at most $2^{2^{|\mathsf {At}(\varPhi )\cap \mathsf {At}(\varPhi ')|}}$ elements, thus $\mathbb {SI}(\varPhi ,\varPhi ')$ is finite.

It can be easily seen that the elements of $\mathbb {SI}(\varPhi ,\varPhi ')$ form a lattice wrt. $\models$ and the operations $\wedge$ and $\vee$. Formally, we can make the following observations.

Proposition 3

Let $\varPhi$ and $\varPhi '$ be finite set of formulas.

• 1. If $[\phi ], [\phi ']\in \mathbb {SI}(\varPhi ,\varPhi ')$ then $[\phi \wedge \phi ']\in \mathbb {SI}(\varPhi ,\varPhi ')$.

• 2. If $[\phi ], [\phi ']\in \mathbb {SI}(\varPhi ,\varPhi ')$ then $[\phi \vee \phi ']\in \mathbb {SI}(\varPhi ,\varPhi ')$.

• 3. There is a uniquely defined $[\phi _{w}]\in \mathbb {SI}(\varPhi ,\varPhi ')$ with $\phi '\models \phi _{w}$ for all $[\phi ']\in \mathbb {SI}(\varPhi ,\varPhi ')$.

• 4. There is a uniquely defined $[\phi _{s}]\in \mathbb {SI}(\varPhi ,\varPhi ')$ with $\phi _{s}\models \phi '$ for all $[\phi ']\in \mathbb {SI}(\varPhi ,\varPhi ')$.

Conditions 1 and 2 of the proposition above are trivial. We illustrate the intuition of both conditions 3 and 4 with an example. Consider the knowledge bases $\mathcal {K}_1 = \{ a, b\}$ and $\mathcal {K}_2 = \{ a, \lnot b\}$. We have that

$$\mathbb {SI}(\mathcal {K}_1,\mathcal {K}_2) = \{ [ a \wedge b], [b], [a \rightarrow b], [a \leftrightarrow b] \}. $$

Note that every formula in $\mathbb {SI}(\mathcal {K}_1,\mathcal {K}_2)$ implies $a \rightarrow b$ (the $\phi _{\omega }$ of condition 3). Similarly, the formula $a \wedge b$ implies all formulae in $\mathbb {SI}(\mathcal {K}_1,\mathcal {K}_2)$, which makes $a \wedge b$ the formula $[\phi _s]$ of condition 4.

Remark 2

If the sets $\varPhi , \varPhi '$ of propositional formulæ are finite then as $\mathbb {SI}(\varPhi ,\varPhi ')$ is finite, $(\mathbb {SI}(\varPhi ,\varPhi '), \wedge , \vee )$ is a complete lattice.

We call $[\phi _{w}]$ the weakest interpolant and $[\phi _{s}]$ the strongest interpolant. It can be easily seen that

$$\begin{aligned}{}[\phi _{w}]&= \left[ \bigvee _{[\phi ]\in \mathbb {SI}(\varPhi ,\varPhi ')} \phi \right]&[\phi _{s}]&= \left[ \bigwedge _{[\phi ]\in \mathbb {SI}(\varPhi ,\varPhi ')} \phi \right] \end{aligned}$$

We abbreviate the weakest interpolant of $\mathbb {SI}(\varPhi ,\varPhi ')$ by $\mathsf {Weakest}(\varPhi ,\varPhi ')$ and the strongest interpolant of $\mathbb {SI}(\varPhi ,\varPhi ')$ by $\mathsf {Strongest}(\varPhi ,\varPhi ')$. If $\mathbb {SI}(\varPhi ,\varPhi ')=\emptyset$ both notions are undefined. We conclude this section with some further observations that will be useful in the remainder of the paper.

Proposition 4

Let $\varPhi$, $\varPhi '$, and $\varPhi ''$ be finite set of formulas.

• 1. $\mathbb {I}(\varPhi ,\varPhi ')\subseteq \mathbb {I}(\varPhi ,\varPhi '\cup \varPhi '')$

• 2. $\mathbb {I}(\varPhi ,\varPhi ')\subseteq \mathbb {I}(\varPhi \cup \varPhi '',\varPhi ')$

• 3. $\mathbb {SI}(\varPhi ,\varPhi ')\subseteq \mathbb {SI}(\varPhi ,\varPhi '\cup \varPhi '')$

• 4. $\mathbb {SI}(\varPhi ,\varPhi ')\subseteq \mathbb {SI}(\varPhi \cup \varPhi '',\varPhi ')$

• 5. $\mathsf {Weakest}(\varPhi ,\varPhi ')\models \mathsf {Weakest}(\varPhi ,\varPhi '\cup \varPhi '')$

• 6. $\mathsf {Weakest}(\varPhi ,\varPhi ')\models \mathsf {Weakest}(\varPhi \cup \varPhi '',\varPhi ')$

• 7. $\mathsf {Strongest}(\varPhi ,\varPhi '\cup \varPhi '')\models \mathsf {Strongest}(\varPhi ,\varPhi ')$

• 8. $\mathsf {Strongest}(\varPhi \cup \varPhi '',\varPhi ')\models \mathsf {Strongest}(\varPhi ,\varPhi ')$

Proof

Considering item 1, for $\phi \in \mathbb {I}(\varPhi ,\varPhi ')$, from $\varPhi '\cup \{\phi \}\models \perp$ it directly follows $\varPhi '\cup \varPhi ''\cup \{\phi \}\models \perp$. The other two conditions of Definition 2 remain valid as well. Item 2 is proven analogously and the remaining items follow directly from 2.   $\square$

4 Disagreement Measures Based on Interpolation

We consider the scenario of measuring disagreement between multiple knowledge bases [17] using interpolation. For that, we denote a knowledge base profile by $P=\langle \mathcal {K}_{1},\ldots ,\mathcal {K}_{n}\rangle$ with $\mathcal {K}_{1},\ldots ,\mathcal {K}_{n}$ being knowledge bases. Furthermore, for $P$ of this form and another knowledge base $\mathcal {K}$, we denote by $P\circ \mathcal {K}$ the concatenation of $P$ with $\mathcal {K}$, i. e., $P\circ \mathcal {K}= \langle \mathcal {K}_{1},\ldots ,\mathcal {K}_{n},\mathcal {K}\rangle$. Furthermore, for $k\in \mathbb {N}$ define $P\circ ^{k}\mathcal {K}=(P\circ ^{k-1}\mathcal {K})\circ \mathcal {K}$ and $P\circ ^{1}\mathcal {K}=P\circ \mathcal {K}$. Let $\mathfrak {K}$ denote the set of all knowledge base profiles. Then Potyka [17] defines a disagreement measure as follows. Let $\mathbb {R}^{\infty }_{\ge 0}$ be the set of non-negative real values including $\infty$.

Definition 5

A disagreement measure $\mathcal {D}$ is a function $\mathcal {D}:\mathfrak {K}\rightarrow \mathbb {R}^{\infty }_{\ge 0}$ that satisfies

• Consistency $\mathcal {D}(P)=0$ iff $\bigcup P$ is consistent.

• Symmetry $\mathcal {D}(\langle \mathcal {K}_{1},\ldots ,\mathcal {K}_{n}\rangle )=\mathcal {D}(\langle \mathcal {K}_{\sigma (1)},\ldots ,\mathcal {K}_{\sigma (n)}\rangle )$ for each permutation $\sigma$ of $\{1,\ldots ,n\}$.

We also write $\mathcal {D}(\mathcal {K}_{1},\ldots ,\mathcal {K}_{n})$ for $\mathcal {D}(\langle \mathcal {K}_{1},\ldots ,\mathcal {K}_{n}\rangle )$ to ease notation.

In the following, we define a series of disagreement measures that work on knowledge base profiles with exactly two elements. In order to generalise these measures to arbitrary knowledge base profiles, we consider the following constructions.

Definition 6

Let $\mathcal {D}$ be a function $\mathcal {D}:\mathbb {K}\times \mathbb {K}\rightarrow \mathbb {R}^{\infty }_{\ge 0}$. Then the induced sum-measure $\mathcal {D}^{\varSigma }:\mathfrak {K}\rightarrow \mathbb {R}^{\infty }_{\ge 0}$ and max-measure $\mathcal {D}^{\max }:\mathfrak {K}\rightarrow \mathbb {R}^{\infty }_{\ge 0}$ are defined via

$$\begin{aligned} \mathcal {D}^{\varSigma }(P)&= \sum _{\mathcal {K},\mathcal {K}'\in P} \mathcal {D}(\mathcal {K},\mathcal {K}')\\ \mathcal {D}^{\max }(P)&= \max \{ \mathcal {D}(\mathcal {K},\mathcal {K}')\mid \mathcal {K},\mathcal {K}'\in P\} \end{aligned}$$

In order to obtain valid disagreement measures using these two constructions, we only need to require the Consistency property from the used two-place functions:

• Consistency$^{2}$ $\mathcal {D}(\mathcal {K}_{1},\mathcal {K}_{2})=0$ iff $\mathcal {K}_{1}\cup \mathcal {K}_{2}$ is consistent.

Proposition 5

Let $\mathcal {D}$ be a function $\mathcal {D}:\mathbb {K}\times \mathbb {K}\rightarrow \mathbb {R}^{\infty }_{\ge 0}$ that satisfies Consistency$^{2}$ then both $\mathcal {D}^{\varSigma }$ and $\mathcal {D}^{\max }$ are disagreement measures.

Proof

We first consider $\mathcal {D}^{\varSigma }$. If $\bigcup P$ is consistent then $\mathcal {K}\cup \mathcal {K}'$ is consistent as well for all $\mathcal {K},\mathcal {K}'\in P$, implying $\mathcal {D}(\mathcal {K},\mathcal {K}')=0$. It follows $\mathcal {D}^{\varSigma }(P)=\mathcal {D}^{\max }(P)=0$ showing Consistency. The property Symmetry is satisfied by construction.

Let us now define some concrete measure using interpolants.

Definition 7

Let $\mathcal {K}_{1},\mathcal {K}_{2}$ be finite and consistent set of formulas. Define the measure $\mathcal {D}_{\mathbb {SI}}:\mathbb {K}\times \mathbb {K}\rightarrow \mathbb {R}^{\infty }_{\ge 0}$ via

$$\begin{aligned} \mathcal {D}_{\mathbb {SI}}(\mathcal {K}_{1},\mathcal {K}_{2})&= |\mathbb {SI}(\mathcal {K}_{1},\mathcal {K}_{2})| \end{aligned}$$

Observe that $\mathcal {D}_{\mathbb {SI}}$ satisfies Consistency$^{2}$, as $\mathbb {SI}(\mathcal {K},\mathcal {K}')=\emptyset$ if $\mathcal {K}\cup \mathcal {K}'$ is consistent. So $\mathcal {D}_{\mathbb {SI}}^{\varSigma }$ and $\mathcal {D}_{\mathbb {SI}}^{\max }$ are disagreement measures according to Proposition 5.

Example 1

Consider the three following knowledge bases: $\mathcal {K}_1 = \{ a, b \}, \mathcal {K}_2 = \{ b , c\}$ and $\mathcal {K}_3 = \{ a, \lnot b\}$. Going for their interpolants we get:

• $\mathbb {SI}(\mathcal {K}_1,\mathcal {K}_2) =\mathbb {SI}(\mathcal {K}_2,\mathcal {K}_1) = \emptyset$, as $\mathcal {K}_1$ is consistent with $\mathcal {K}_2$;

• $\mathbb {SI}(\mathcal {K}_1,\mathcal {K}_3) = \{ [b], [a \wedge b], [a \rightarrow b] \}$ and $\mathbb {SI}(\mathcal {K}_3,\mathcal {K}_1) = \{ [\lnot b], [a \rightarrow \lnot b], [a \wedge \lnot b] \}$;

• $\mathbb {SI}(\mathcal {K}_2,\mathcal {K}_3) = \{ [b]\}$ and $\mathbb {SI}(\mathcal {K}_3,\mathcal {K}_2) = \{ [ \lnot b]\}$, as $\mathsf {At}(\{ \mathcal {K}_2, \mathcal {K}_3\}) = \{ b\}$.

Therefore, $\mathcal {D}_{\mathbb {SI}}^{\varSigma }(\mathcal {K}_1, \mathcal {K}_2, \mathcal {K}_3) = 8$ and $\mathcal {D}_{\mathbb {SI}}^{\max }(\mathcal {K}_1, \mathcal {K}_2, \mathcal {K}_3) = 3$.

We consider another measure based on the information content of strongest (resp. weakest) interpolant. We use the following definition of an information measure, similar in spirit to the definition given in [11].

Definition 8

An information measure J is a function $J:\mathcal {L} (\mathsf {At})\rightarrow \mathbb {R}^{\infty }_{\ge 0}$ that satisfies the following four properties:

• 1. $J(\top )=0$.

• 2. $J(\perp )=\infty$.

• 3. If $\phi \models \phi '$ then $J(\phi )\ge J(\phi ')$.

• 4. If $\phi \not \models \bot$ then $J(\phi ) < \infty$.

Here is a simple example of an information measures:

$$\begin{aligned} J_{M}(\phi )&= \left\{ \begin{array}{ll} 0 &{} \text {if~} \top \models \phi \\ \infty &{} \text {if~} \phi \models \perp \\ 1/|\mathsf {Mod}(\phi )| &{} \text {otherwise} \end{array}\right. \end{aligned}$$

(1)

It is easy to verify that $J_{M}$ is indeed an information measure according to Definition 8.

Then consider the following measure.

Definition 9

Let $\mathcal {K}_{1},\mathcal {K}_{2}$ be finite and consistent set of formulas and J some information measure. Define the following measure $\mathcal {D}_{J}:\mathbb {K}\times \mathbb {K}\rightarrow \mathbb {R}^{\infty }_{\ge 0}$:

$$\begin{aligned} \mathcal {D}_{J}(\mathcal {K}_{1},\mathcal {K}_{2})&= \left\{ \begin{array}{ll} 0 &{} \text {if~} \mathcal {K}_{1}\cup \mathcal {K}_{2}\text {~is consistent}\\ \infty &{} \text {if~} J(\mathsf {Weakest}(\mathcal {K}_{1},\mathcal {K}_{2}))=0\\ \frac{J(\mathsf {Strongest}(\mathcal {K}_{1},\mathcal {K}_{2}))}{J(\mathsf {Weakest}(\mathcal {K}_{1},\mathcal {K}_{2}))} &{} \text {otherwise} \end{array}\right. \end{aligned}$$

Again, observe that $\mathcal {D}_{J}$ satisfies Consistency$^{2}$ (independently of J). So $\mathcal {D}_{J}^{\varSigma }$ and $\mathcal {D}_{J}^{\max }$ are disagreement measures according to Proposition 5.

Example 2

Consider the three knowledge bases from Example 1: $\mathcal {K}_1 = \{ a, b \}, \mathcal {K}_2 = \{ b , c\}$ and $\mathcal {K}_3 = \{ a, \lnot b\}$. In the table below, we show their strongest and weakest interpolants as well as their disagreement measure $D_{J_M}$, where $J_M$ is the information measure defined in (1) above.

As $\mathcal {K}_1$ is consistent with $\mathcal {K}_2$ they do not have any interpolant, and therefore their disagreement measure $D_{J_M}$ is zero. Note that each of the weakest interpolants between $\mathcal {K}_1$ and $\mathcal {K}_3$ have each 6 models, while their strongest interpolants have each 2 models.

5 Analysis

Potyka [17] proposes some desirable properties for disagreement measures, inspired by similar properties from inconsistency measurement [18]. Let $\mathcal {D}$ be some disagreement measure. For $P=\langle \mathcal {K}_{1},\ldots ,\mathcal {K}_{n}\rangle$, we say that $\mathcal {K}_{i}$, $i\in \{1,\ldots ,n\}$, is involved in a conflict, if there is $C\subseteq \{1,\ldots ,n\}$ such that $\bigcup _{j\in C}\mathcal {K}_{j}$ is consistent but $\mathcal {K}_{i}\cup \bigcup _{j\in C}\mathcal {K}_{j}$ is inconsistent.

• Monotony (MO) $\mathcal {D}(\mathcal {K}_{1},\ldots ,\mathcal {K}_{n})\le \mathcal {D}(\mathcal {K}_{1}\cup \mathcal {K}',\ldots ,\mathcal {K}_{n})$.

• Dominance (DO) For formulas $\phi , \psi$ with $\phi \models \psi$ and $\phi \not \models \perp$, $\mathcal {D}(\mathcal {K}_{1}\cup \{\phi \},\ldots ,\mathcal {K}_{n})\ge \mathcal {D}(\mathcal {K}_{1}\cup \{\psi \},\ldots ,\mathcal {K}_{n})$.

• Safe Formula Independence (SFI) For a formula $\phi$ with $\phi \not \models \perp$ and $\mathsf {At}(\phi )\cap \mathsf {At}(\bigcup \mathcal {K}_{i})=\emptyset$, $\mathcal {D}(\mathcal {K}_{1}\cup \{\phi \},\ldots ,\mathcal {K}_{n})= \mathcal {D}(\mathcal {K}_{1},\ldots ,\mathcal {K}_{n})$.

• Adjunction Invariance (AI) For formulas $\phi ,\psi$, $\mathcal {D}(\mathcal {K}_{1}\cup \{\phi ,\psi \},\ldots ,\mathcal {K}_{n})= \mathcal {D}(\mathcal {K}_{1}\cup \{\phi \wedge \psi \},\ldots ,\mathcal {K}_{n})$.

• Tautology (TA) If $\mathcal {K}$ is a knowledge base with $\top \models \mathcal {K}$ then $\mathcal {D}(P)\ge \mathcal {D}(P\circ \mathcal {K})$.

• Contradiction (CO) If $\mathcal {K}$ is inconsistent then $\mathcal {D}(P)\le \mathcal {D}(P\circ \mathcal {K})$.

• Majority (MAJ) If $\mathcal {K}\in P$ is consistent and involved in a conflict, then there is $k\in \mathbb {N}$ with $\mathcal {D}(P\circ ^{k}\mathcal {K}) <\mathcal {D}(P)$.

• Majority Agreement in the Limit (MAJL) If M is a maximal consistent subset of $\bigcup P$ then $\lim _{k\rightarrow \infty }\mathcal {D}(P\circ ^{k}M)=0$.

Table 1. Compliance of investigated disagreement measures with postulates.

We check compliance of the disagreement measures $\mathcal {D}_{\mathbb {SI}}^{\varSigma }, \mathcal {D}_{\mathbb {SI}}^{\max }, \mathcal {D}_{J}^{\varSigma }$ and $\mathcal {D}_{J}^{\max }$ against the disagreement measures postulates mentioned above. For this, we introduce the concept of agreement between interpretations. We say that an interpretation w agrees with an interpretation $w'$ modulo a set of propositional symbols X iff $w(p) = w'(p)$, for all $p \in X$. Note that the agreement relation is symmetric, that is, if w agrees with $w'$ modulo X then $w'$ agrees with w modulo X. We recall the Coincidence Lemma on propositional logic:

Lemma 1

(Coincidence Lemma). If two interpretations w and $w'$ agree with $\mathsf {At}(\alpha )$, then $w \models \alpha$ iff $w' \models \alpha$.

Proposition 6

Let $\mathcal {K}$ be knowledge base, and $\varphi$ a consistent formula. If $\mathsf {At}(\mathcal {K}) \cap \mathsf {At}(\varphi ) = \emptyset$, $\mathsf {At}(\alpha ) \subseteq \mathsf {At}(\mathcal {K})$ and $\mathcal {K}\cup \{\varphi \} \models \alpha$ then $\mathcal {K}\models \alpha$.

Proof

The case that $\mathcal {K}$ is inconsistent is trivial. So we focus on the case that $\mathcal {K}$ is consistent. Let then $w \in \mathsf {Mod}(\mathcal {K})$ be an interpretation of $\mathcal {K}$, we will show that $w \in \mathsf {Mod}(\alpha )$. As $\varphi$ is consistent, it has at least one interpretation. Let $w' \in \mathsf {Mod}(\varphi )$, and let $w_0$ be the following interpretation: $w_0(p) = w(p)$, if $p \in \mathsf {At}(\mathcal {K})$; and $w_0(p) = w'(p)$, otherwise. Note that $w_0$ agrees with w modulo $\mathsf {At}(\mathcal {K})$, which implies that $w_0 \models \mathcal {K}$. As $\mathsf {At}(\mathcal {K}) \cap \mathsf {At}(\varphi ) = \emptyset$, we get that $w_0$ agrees with $w'$ modulo $\mathsf {At}(\varphi )$. This implies that $w_0 \models \varphi$. Therefore, as $w_0 \models \mathcal {K}$ and $w_0 \models \varphi$, we have that $w_0 \models \mathcal {K}\cup \{\varphi \}$. Thus, as $\mathcal {K}\cup \{\varphi \} \models \alpha$, we get that $w_0 \models \alpha$. As, by hypothesis, $\mathsf {At}(\alpha ) \subseteq \mathsf {At}(\mathcal {K})$, we get that w agrees with $w_0$ modulo $\mathsf {At}(\alpha )$. This implies, from Lemma 1, that $w \models \alpha$.

Theorem 2

The compliance of the measures $\mathcal {D}_{\mathbb {SI}}^{\varSigma }$, $\mathcal {D}_{\mathbb {SI}}^{\max }$, $\mathcal {D}_{J}^{\varSigma }$, and $\mathcal {D}_{J}^{\max }$ is as shown in Table 1.

Note again that the proof of the above theorem can be found online².

Potyka [17] has defined disagreement measures from inconsistency measures. The idea is that the degree of disagreement in a knowledge profile would correspond to measuring the degree of inconsistencies between the knowledge bases in a knowledge profile. Potyka then discusses about some principles that disagreement measures should satisfy, and show that many of the disagreement measures induced from inconsistency measures fail to satisfy some of these principles. He then proposes the disagreement measure $D_\eta$, based on the $\eta$-inconsistency measure [13], to capture some of these principles. Following this line, we analyse here some desirable properties that disagreement measures on interpolants satisfy. We show that Potyka’s $D_{\eta }$ measure has some issues that are better handled by disagreement measures based on interpolants.

We start by addressing the Adjunction Invariance axiom. Breach of this axiom can lead to unintuitive behaviours. For instance, both $\{\alpha \wedge \lnot \alpha \}$ and $\{\alpha , \lnot \alpha \}$ should have the same disagreement value, since they present the same conflicts. Most of the disagreement measures induced from inconsistency measures analysed by Potyka, including his $D_{\eta }$ measure, is not adjunctive invariant. On the other hand, as shown above, disagreement measures based on interpolants are adjunctive invariant. This is because interpolants are not syntax sensitive, instead they consider formulæ that share the same signature.

Potyka’s disagreement measure $D_\eta$ plateaus when each knowledge base in a knowledge profile conflicts with each other. As he himself criticizes, this scenario makes the measurement purely dependable on the size of the knowledge profile. Precisely, in that case $D_{\eta }(P) = (|P| -1 ) / |P|$. In this scenario, a disagreement measure should still be able to distinguish an increase of conflicts, even if two knowledge profiles have the same size. We illustrate it in the following example.

Example 3

Let $P= \langle \mathcal {K}_1, \mathcal {K}_2, \mathcal {K}_3 \rangle$, and $P' = \langle \mathcal {K}_1, \mathcal {K}_2, \mathcal {K}_4 \rangle$ be two knowledge profiles, where $\mathcal {K}_1 = \{ a, b\}, \mathcal {K}_2 = \{ \lnot a, b\}, \mathcal {K}_3 = \{ \lnot b\}$ and $\mathcal {K}_4 = \{ \lnot b, \lnot a\}$. Note that the four knowledge bases are consistent, but are inconsistent with each other. For the $D_{\eta }$ disagreement measure, we would have $D_{\eta } (P)~=~D_{\eta }(P')~=~2/3.$

Note that, against $\mathcal {K}_1$ and $\mathcal {K}_2$, the knowledge base $\mathcal {K}_4$ presents more conflicts than $\mathcal {K}_3$. Thus, though both $P$ and $P'$ have the same size, $P'$ is more conflicting than $P$. A disagreement measure should be able to distinguish this difference of conflicts. The $D_{\eta }$ measure, however, does not distinguish these conflicts, since when knowledge bases are pairwise inconsistent, the measure considers only the size of the knowledge profile, which is rather simplistic.

On the other hand, disagreement measures on interpolants are able to distinguish this tenuous difference of conflicts. To illustrate this, consider the $\mathcal {D}_{\mathbb {SI}}^{\varSigma }$ measure. For the knowledge bases above we would get $\mathcal {D}_{\mathbb {SI}}(\mathcal {K}_1, \mathcal {K}_2) = 4, \mathcal {D}_{\mathbb {SI}}(\mathcal {K}_1, \mathcal {K}_3) = 1, \mathcal {D}_{\mathbb {SI}}(\mathcal {K}_1,\mathcal {K}_4) = 4, \mathcal {D}_{\mathbb {SI}}(\mathcal {K}_2, \mathcal {K}_3) = 1$ and $\mathcal {D}_{\mathbb {SI}}(\mathcal {K}_2, \mathcal {K}_4) = 4$. Thus, $\mathcal {D}_{\mathbb {SI}}(P)^{\varSigma } = (4 + 1 + 1) *2 = 12$ and $\mathcal {D}_{\mathbb {SI}}^{\varSigma }(P') = (4 + 4 + 4)*2 = 24$.

This shows that disagreement measures on interpolants, such as $\mathcal {D}_{\mathbb {SI}}^{\varSigma }$, present ways of distinguishing sensible conflicts between knowledge bases. Towards this end, a deeper investigation of which rational behaviours interpolants yield for disagreement measures is a path worth to explore.

6 Computational Complexity

To conclude our analysis, we now investigate the computational complexity of problems related to our novel measures.

Let us first consider some general observations on interpolants, which seem—to the best of our knowledge—not have been explicitly mentioned in the literature thus far.

Theorem 3

Let $\varPhi$ and $\varPhi '$ be sets of formulas and let $\phi$ be a formula. Deciding whether $\phi$ is an interpolant of $\varPhi$ wrt. $\varPhi '$ is coNP-complete.

Proof

For coNP-membership, consider the complement problem of deciding whether $\phi$ is not an interpolant of $\varPhi$ wrt. $\varPhi '$ and define the following non-deterministic algorithm. On instance $(\phi ,\varPhi ,\varPhi ')$ we guess a triple $(\omega ,\omega ',a)$ with interpretations $\omega$, $\omega '$, and an atom a. Then $\phi$ is not an interpolant of $\varPhi$ wrt. $\varPhi '$ if either

• 1. $\omega \models \varPhi$ and $\omega \not \models \phi$,

• 2. $\omega '\models \varPhi '\cup \{\phi \}$, or

• 3. $a\in \mathsf {At}(\phi )\setminus (\mathsf {At}(\varPhi )\cap \mathsf {At}(\varPhi '))$.

Observe that each of these checks correspond to disproving one item of Definition 2 and that they can be done in polynomial time. If follows coNP-membership of the original problem.

For coNP-hardness, we reduce the problem Taut to our problem. An instance to Taut consists of a formula $\psi$ and it has to be decided whether $\psi$ is tautological. On input $\psi$ we construct the instance $(\phi ,\varPhi ,\varPhi ')$ for our problem (let a be a fresh atom not appearing in $\psi$) with

$$\begin{aligned} \phi&= a&\varPhi&= \{\psi \rightarrow a\}&\varPhi '&= \{\lnot a\} \end{aligned}$$

It remains to show that $\psi$ is tautological if and only if $\phi$ is an interpolant of $\varPhi$ wrt. $\varPhi '$. Assume that $\psi$ is tautological, then it follows $\varPhi \models a$. Obviously, $\varPhi '\cup \{a\}$ is inconsistent and $\phi$ only contains atoms of the shared vocabulary. It follows that $\phi$ is an interpolant of $\varPhi$ wrt. $\varPhi '$. The other direction is analogous.    $\square$

In [16] it is shown that, essentially, the size³ of an interpolant $\phi \in \mathbb {SI}(\varPhi ,\varPhi ')$ is probably not bound polynomially in the size of both $\varPhi$ and $\varPhi '$ (very surprising results would follow in this case). This makes a characterisation of the complexity of various other computational problems hard. For example, a standard approach to decide whether some given formula $\phi$ would not be the strongest (weakest) interpolant, would be to guess another formula $\phi '$ (e. g., the actual strongest/weakest interpolant) and verify that $\phi '$ is an interpolant and $\phi '\models \phi$ ($\phi \models \phi '$). However, as $\phi '$ might be of exponential size this is not feasible to show membership in some class of the polynomial hierarchy or even Pspace. We can therefore only provide a straightforward upper bound for the complexity of these and other problems of relevance to us.

Theorem 4

Let $\varPhi$ and $\varPhi '$ be sets of formulas.

• 1. For a formula $\phi$, the problem of deciding whether $\phi =\mathsf {Strongest}(\varPhi ,\varPhi ')$ is in Expspace.

• 2. For a formula $\phi$, the problem of deciding whether $\phi =\mathsf {Weakest}(\varPhi ,\varPhi ')$ is in Expspace.

• 3. The problem of determining $\mathsf {Strongest}(\varPhi ,\varPhi ')$ is in FExpspace.

• 4. The problem of determining $\mathsf {Weakest}(\varPhi ,\varPhi ')$ is in FExpspace.

• 5. The problem of counting $|\mathbb {SI}(\varPhi ,\varPhi ')|$ is in FExpspace.

Proof

We first show 5. For that, we enumerate (by reusing space) every subset $M\subseteq \varOmega (\mathsf {At})$ of interpretations (note that every interpretation is of polynomial size and there are exponentially many interpretations; therefore M is of exponential size). Each such set M characterises a formula $\phi _{M}$ and its equivalence class $[\phi _{M}]$ via $\mathsf {Mod}(\phi _{M})=M$. We can then easily verify whether $\phi _{M}$ is an interpolant of $\varPhi$ wrt. $\varPhi$, see Theorem 3 and the fact that $\textsc {coNP}\subseteq \textsc {Expspace}$. In the positive case we add 1 to some counter. After enumerating all possible M, the counter is exactly the number $|\mathbb {SI}(\varPhi ,\varPhi ')|$.

In order to prove 1–4, the above algorithm can easily be adapted. For 1., whenever we have verified a formula $\phi _{M}$ to be an interpolant, we can check whether $\phi _{M}\models \phi$ and $\phi \not \models \phi _{M}$. In that case, $\phi$ cannot be the strongest interpolant. Case 2 is analogous. Cases 3–4 can be realised by keeping track of the strongest (weakest) interpolant found so far and always comparing it newly discovered interpolants.    $\square$

7 Summary and Conclusion

We investigated the problem of measuring disagreement in belief merging scenarios. For that, we made use of the concept of Craig interpolants and defined disagreement measures that consider the number of semantically equivalent interpolants between two knowledge bases and the information content in the strongest and weakest interpolants. We showed that our measures satisfy a number of desirable properties and we briefly discussed the computational complexity of related problems.

For future work, we will investigate the possibility of defining further measures based on interpolation and investigate their properties. Moreover, a deeper analysis of the differences of our measures with the measures proposed by Potyka [17] is needed. Precisely, our approach based on interpolants has a semantic perspective in assessing the culpability degree of the inconsistencies between two knowledge bases. We shall investigate what properties this semantic perspective brings upon these inconsistency measures. We will also explore algorithmic approaches to compute our measures and investigate applying our ideas to the area of inconsistency measurement [19].