In this paper, we present a new principled framework for evaluating the relative truthfulness of ABox assertions (i.e., the sentence ϕ is an ABox assertion in our framework). By relative, we mean that we are merely interested in ranking ABox assertions: Given two ABox assertions α and β, is α more, less, or equally truthful than β? Our framework is different from CQA in that it does not use the notion of repair. The framework assumes that there is some initial weight function over the ABox assertions, called credibility function, which models the opinion of domain experts concerning the truthfulness of assertions. In their assessments, however, experts may have difficulties to fully understand and take into account the logic that is expressed by, possibly extensive, TBoxes. To overcome this difficulty, we propose an automated mathematical method for adjusting the experts' initial credibility function by taking into account the ontological logic of the TBox: strong logical support for an assertion α should increase its credibility, while strong logical support for ¬α should decrease α's credibility. Eventually, our method results in a ranking of ABox assertions in terms of truthfulness, taking into account both the experts' credibility function and the TBox logic. In our framework, we assume that the TBox has been validated by a multitude of experts and is therefore error-free.

This paper is organized as follows. Section 2 presents a guiding example. Section 3 discusses related work. Section 4 introduces our general theoretical framework, and Section 5 presents a particular instantiation of this framework. Section 6 studies in more detail some theoretical questions and computational tasks raised by this instantiation. Finally, Section 7 concludes the paper.

Consider the following knowledge base K 0 = T 0 , A 0 .

This knowledge base is inconsistent, because from (John, KR) : attends, we can infer John : Student by means of the axiom ∃attends Student. Then, by means of the axiom Student ¬Professor, we can infer John : ¬Professor, which obviously contradicts the first assertion in A 0 . In conclusion, (John, KR) : attends and John : Professor contradict one another. The vertices in the directed graph of Fig. 1 are the assertions of A 0 . A red-colored edge from α to β means that α refutes β. On the other hand, a green-colored edge from α to β means that α supports β. For example, from (John, DB2) : teaches we can infer John : Professor by means of the axiom ∃teaches Professor. Therefore, (John, DB2) : teaches supports John : Professor. In this example, we assumed that domain experts esteemed that assertions in the ABox were equally credible, represented by a value of 1. Then, our proposed method updates values by balancing the value of each assertion α with respect to the values of α's refuters and supporters. Refuters and supporters of α, respectively, lower and increase α's value by an amount that is proportional to their own value. In Fig. 1, we see that John : Professor is attributed a higher value than (John, KR) : attends because it has more supporters and less refuters. Figure 2 shows the effect of adding Ava : Professor to A 0 . One can observe that the values of the assertions (Ava, IA) : attends and Ava : Student have gone down because of conflicts with the new assertion.

Since supporters and refuters are single assertions in this simple example, they can be represented in a directed graph. In our general framework, however, supporters and refuters will be sets of assertions. For example, if A B ¬C is a TBox assertion, then the set {(i, A), (i, B)} is a refuter of (i, C), but neither (i, A) nor (i, B) is a refuter on its own.

In Description Logics, different repairs correspond to different ABoxes, each one consistent with respect to a given fixed TBox. When we move from a single ABox to a set of possible ABoxes, different semantics for logical reasoning become possible, including brave semantics [BR13], ABox Repair (AR) and Intersection ABox Repair (IAR) semantics [LLR + 10]. These semantics can be enriched by taking into account notions of cardinality [LB16], preference [BBG14], or probability [GM12,CLP18]. Some works [DQ15,TBB + 17] in the Description Logics community have already investigated the problems of finding the best repairs according to some criteria, and of extracting consistent information that best complies with specific needs. Sik Chun Lam et al. have proposed logic-based methods for repairing TBox axioms of unsatisfiable ontologies [LPSV06a], as well as numerical methods for rewriting and ranking problematic axioms [LPSV06b].

Ranking the nodes of some sort of knowledge graph in terms of interest, quality, or preference is a recurrent problem in many disciplines. Solving these problems requires to somehow quantify the nodes and their interactions. A quantitative approach, rather than a qualitative one, has been used in argumentation frameworks [AB13,BDKM16,BCPR12,Rad18,HT17], belief revision [SSF16], the Web [Kle99,PBMW99], and social networks [dKD08,TND10].

Throughout this paper, we will assume that TBoxes are satisfiable. That is, for every TBox T , the knowledge base T , ∅ is consistent. If a knowledge base T , A is inconsistent, we will assume that the inconsistency is caused by one or more assertions in A. When humans are faced with such an inconsistent knowledge base T , A , they may not be able to quickly pinpoint the "wrong" assertion(s) in A, because the inconsistency may only become apparent after an involved reasoning process that uses many axioms and assertions. We present a method for ranking assertions such that higher-ranked assertions are more "truthful" than lower-ranked assertions. Significantly, the ranking only requires some superficial input from the user, who is modeled by the notion of a credibility function, which is a mapping from A to R. Such a credibility function will be combined with TBox assertions to result in the desired ranking. All definitions that follow are relative to a fixed knowledge base T , A in some fixed Description Logic.

We define what it means for a set B of assertions to support or refute an assertion α not in B. In our framework, assertions will be higher ranked if they have strong supporters and no strong refuters. Definition 1. The following definitions are relative to a knowledge base T , A , and an assertion α ∈ A.

A refuter of α is an inclusion-minimal subset B of A with the property that T , B is consistent and T , B ∪ {α} is inconsistent.

A supporter of α is an inclusion-minimal subset B of A with the property that T , B is consistent, α ∈ B, and

-{a : A} is a refuter of a : D, and a supporter of a : C.

-{a : C} is neither a refuter nor a supporter of a : A.

Proposition 1. Let T , A be a knowledge base in a monotonic Description Logic, and let α ∈ A. Then, 1. distinct refuters of α are not comparable by set inclusion; 2. distinct supporters of α are not comparable by set inclusion; and 3. if B is a refuter of α and B is a supporter of α, then B and B are not comparable by set inclusion.

Proof. The proof of the first two items is straightforward. We next prove the last item. Assume B is a refuter of α, and B is a supporter of α. Consequently, From here on, we will assume that all Description Logics considered are monotonic.

As explained in the beginning of Section 4, we assume a credibility function mapping every assertion α in A to a real number that can be thought of as the truthfulness associated by an expert to the assertion α.

We will assume that the credibility function induces a function f from 2 A to R by means of some aggregation operator ⊕. Examples of ⊕ are min, max, avg, sum. In the theoretical development, we will abstract away from the aggregation operator ⊕ and treat f as a basic construct. To keep our framework flexible and general, we do not impose any restrictions on the choice of the credibility function, which can be instantiated and adapted later on to fit a particular setting, for example, as a probability distribution.

An ABox assessment for an ABox A is a total function ν : A → R. Informally, our goal is to define ν such that if two ABox assertions are logically conflicting, then the assertion with the higher ν-value is preferred.

Although credibility functions and ABox assessments are both mappings from

A to R, it is important to understand that they are conceptually distinct. In particular, ABox assessments improve credibility functions by taking into account the axioms of the TBox, via the notions of refuter and supporter defined previously.

Informally, we want that for every α ∈ A, its value under ν is greater if α has strong supporters, and smaller if α has strong refuters. Here, the strength of a supporter or refuter is recursively determined by the aggregated ν-values of its elements. This can be expressed as follows, where ∼ denotes some proportionality that will be made explicit later on:

The expression at the righthand of ∼ will be abbreviated Σ ± (α). Informally, Σ ± (α) sums over all supporters and refuters of α. The formulas for supporters and refuters are signed positively and negatively respectively. The magnitude of each supporter's or refuter's contribution is proportional to its aggregated credibility and ABox assessment values. It is significant that (1) is recursive, in the sense that ν appears at both the lefthand and righthand of ∼.

To shorten notations, we define mappings T : A → 2 A and F : A → 2 A , as follows:

Informally, one can think of T and F as True and False respectively. B ∈ T (α) is shorthand for "B is a supporter of α," and B ∈ F (α) is shorthand for "B is a refuter of α". Obviously, the complexity of computing T and F will depend on the underlying Description Logic.

To have a more compact form for Σ ± (α), we define an indicator function I from {T, F } × 2 A × A × A to {0, 1}:

Thus, I(T, B, α, β) is one if B is a supporter of α that contains β, and is zero otherwise. Likewise, I(F, B, α, β) is one if B is a refuter of α that contains β, and is zero otherwise. Note incidentally that α = β implies I(L, B, α, β) = 0, because α does not belong to a supporter or a refuter of itself. Then, for α ∈ A,

An ABox assessment ν induces a ranking of an ABox, as follows: α is ranked higher than β if ν(α) > ν(β); and α is ranked equal to β if ν(α) = ν(β). Two ABox assessments ν 1 and ν 2 are rank-equivalent, denoted ν 1

∼ is an equivalence relation on the set of all ABox assessments. In our study, we will be primarily interested in the set of ABox assessments modulo • ∼. That is, we are not so much interested in the real numbers in the range of two different ABox assessments, but rather in their induced rankings.

We will assume A = {α 1 , . . . , α N }. In this section, we elaborate an instantiation of the framework in Section 4. With the previous abbreviations, Eq. (1) reads as ν(α i ) ∼ Σ ± (α i ). We will instantiate ∼ as a linear proportionality, i.e., for some numbers a, b, c with a = 0:

A more natural formulation may introduce only two numbers d, e and impose ν(α i ) = d * Σ ± (α i ) + e for 1 ≤ i ≤ N . This is tantamount to fixing a = 1. The choice for using three numbers was made for reasons of flexibility, but is not fundamental.

Since we think of (1) as a positive proportionality, we require that a and b have the same sign, say both positive. Let A f be the square N × N matrix such that for 1 ≤ i, j ≤ N ,

It is easily verified that for every i ∈ {1, . . . , N }, A f i,i = 0. For i ∈ {1, . . . , N }, we introduce a variable x i for the unknown ν(α i ). We define X = x 1 x 2 • • • x N . Then, using (3), the system of equations (4) can be equivalently written as follows:

where 1 is the square identity matrix. Equation (6) has a unique solution if and only if the matrix a • 1 − b • A f (which does not depend on c) is non-singular (i.e., is invertible). In that case, the solution ABox assessment is given by:

We should pick c = 0 to avoid the all-zero solution. Indeed, if a • 1 − b • A f is non-singular and c = 0, then the solution to (7) yields the ABox assessment

which obviously is of no interest for ranking ABox assertions.

Then, it is easily verified that for fixed values of a and b, different choices for c lead to rank-equivalent solutions. Therefore, we can choose c = 1 without loss of generality, in which case in the solution, x i is the sum of all elements in the ith row of a • 1 − b • A f −1 . Two significant questions remain:

1. For which values of a and b is the square matrix a • 1 − b • A f non-singular, such that (7) gives us a unique ABox assessment? Obviously, a

Therefore, only the ratio between a and b matters in our subsequent analysis. 2. Are ABox assessments obtained for different values of a, b rank-equivalent?

From a graph-theoretical viewpoint, A f can be interpreted as an edge-weighted directed graph whose vertices are the assertions of the ABox. This view is used in Figures 1 and 2. An edge from α j to α i (i = j) has weight A f i,j . The task is then to assign a real number to each vertex such that the resulting graph satisfies the sort of equilibrium expressed by (4). The ratio between a and b determines how strongly a vertex is impacted (supported or refuted) by its incoming edges. The question arising is whether an equilibrium (4) can be attained for some values of a, b. It is equally important to examine the robustness of such an equilibrium (if it exists) with respect to rank-equivalence. Ideally, different ABox assessments obtained by small parameter changes should be close modulo rank-equivalence.

In Section 5, we presented the matrix equation (6) whose unique solution, if it exists, yields an ABox assessment. This matrix equation has parameters a, b. A remaining problem is how to pick appropriate values for these parameters. One solution could be to choose values for a, b in an empirical fashion, relying, for instance, on information obtained from some learning experience. Although we have conducted some experiments (cf. Figures 1 and 2), a thorough empirical or experimental validation is left for future research. Instead, we will focus more on theoretical aspects in the current paper. In Section 6.1, we will show a parameterization scheme for a, b that guarantees the existence of a solution for (6): pick a b > 0. What is probably more important is that when the ratio a/b grows, the ABox assessments obtained for different a, b become all rank-equivalent. Informally, the parameterization scheme converges to a unique ABox assessment modulo rank-equivalence.

Note that all diagonal elements in a • 1 − b • A f are equal to a. The invertibility of a • 1 − b • A f can be guaranteed by (some form of) diagonal dominance, a concept that is easily grasped and has turned out to be useful in applications [Var76]. An example is the Levy-Desplanques theorem recalled next.

From Theorem 1, it immediately follows that (7) has a unique solution if for all i ∈ {1, . . . , N }, we have |a| > |b| * N j=1 A f i,j . This is illustrated by Example 2.

Example 2. Assume four assertions α 1 , α 2 , α 3 , α 4 such that α 1 and α 2 support one another, while α 3 and α 4 refute one another. Take b = 1. If we assume f ({α i }) = 1 for 1 ≤ i ≤ 4, we obtain:

It follows from Theorem 1 that this matrix is invertible for a > 1, giving the following solution:

Although distinct values for a lead to different ABox assessments, it is significant to observe that 1 a−1 > 1 a+1 (a > 1), and therefore all these ABox assessments ν are rank-equivalent: ν(α 1 ) = ν(α 2 ) > ν(α 3 ) = ν(α 4 ). It is intuitively correct that the two assertions that mutually attack one another loose credibility.

The invertibility of a • 1 − b • A f may also follow from Banach's Lemma, which is recalled next.

Theorem 2 (Banach's Lemma). Let M be a square matrix with the property that M < 1 for some operator norm • . Then the matrix 1 − M is invertible and (1 − M )

Therefore, if we fix a = 1 and pick b sufficiently small (which is analogous to fixing b = 1 and picking a sufficiently large), then the matrix

If we limit ourselves to the two most significant terms in this expansion, we get X = 1 + A f • 1 1 • • • 1 as an approximate solution for (7). The ranking obtained by this solution is intuitively meaningful, because it ranks α i based on the sum of the elements in the ith row of A f ; in this row, supporters have a positive sign, and refuters a negative sign.

So it turns out that (6) has a unique solution with a, b ≥ 0 whenever the ratio a/b is sufficiently large. A desirable property is that different solutions be rankequivalent, as was the case in Example 2. We now show that this property indeed holds true beyond some threshold value for a/b.

The notion of rank-equivalence obviously extends to any two vectors of real numbers: two such vectors A, B of the same length N are rank-equivalent if for all 1 ≤ i, j ≤ N , a i < a j if and only if b i < b j . The proof of the following theorem is in Appendix A. Since, as argued before, only the ratio between a and b matters in our analysis, we can fix b and let a increase in the following theorem.

Theorem 3 (Convergence). Let M be an N × N matrix whose diagonal elements are zero. Let b, c ∈ R. Consider the following equation with real-number parameter a:

Then there exists a * ∈ R such that for every a ≥ a * , the equation (8) has a unique solution; and for all a 1 , a 2 ≥ a * , if X 1 and X 2 are solutions to (8) for parameters a 1 and a 2 respectively, then X 1 and X 2 are rank-equivalent.

Moreover, such a bound a * can be computed in polynomial time in the size of N .

Informally, Theorem 3 tells us that for all choices of b and c, there is a threshold value a * such that all choices of a satisfying a ≥ a * lead to the same ABox assessment modulo rank-equivalence.

We discuss the computational complexity of solving (6). The main difficulty is the computation of the non-diagonal elements in A f , which are defined by (5).

Given α i and β j , this requires finding every B ⊆ A such that β j ∈ B and B is a supporter or refuter of α i . In general, the number of supporters or refuters can be exponential in the size of A, because an ABox of size 2N can have 2N N supporters or refuters not comparable by set inclusion. However, in practice, a fixed upper bound on the size of supporters or refuters may be implied by the TBox, in a way captured by the following definition.

Definition 2. We say that a TBox T is conflict-bounded if there exists a polynomial-time computable positive integer m such that for every knowledgebase A, T and α ∈ A, if B is a refuter or supporter of α, then |B| ≤ m.

Conflict-boundedness arises in practice. For example, for every DL-Lite TBox, every supporter or refuter has cardinality ≤ 1 because each conflict in DL-Lite involves at most two assertions. Conflict-boundedness is also guaranteed in EL ⊥nr (EL ⊥ with non-recursive empty concepts) defined in [Ros11].

Theorem 4. Let T be a conflict-bounded TBox such that ABox consistency with respect to T can be checked in polynomial time. Then, for every ABox A, the matrix A f can be computed in polynomial time (in the size of A) if f is polynomial-time computable.

Proof. Let N := |A|. Recall that A f is an N × N matrix given by (5). Since T is conflict-bounded, say with bound m, for every B ⊆ A, if |B| > m, then I(T, B, α i , α j ) = I(F, B, α i , α j ) = 0. Therefore, the sum in (5) must only consider subsets B ⊆ A with |B| ≤ m, which are polynomially many and polynomial-time computable. Furthermore, since ABox consistency checking is in polynomial time by the hypothesis of the theorem, it can be tested in polynomial time whether any such B containing α j is a supporter or a refuter of α i (or neither of both). The computation of f (B) is also in polynomial time by the hypothesis of the theorem. It is now obvious that any entry of A f can be computed in polynomial time.

An inspection of the preceding proof reveals that Theorem 4 remains valid if, throughout its statement, we replace polynomial time by some higher complexity upper bound (e.g., polynomial space or exponential time).

In this work, we have proposed a novel framework to rank the assertions of an inconsistent ABox in terms of their degree of truthfulness. This ranking takes into account an expert's credibility function as well as the logical axioms of the TBox. The theoretical framework can work with any Description Logic, but to gain computational tractability, restrictions have to be imposed.

The framework is implementable using existing libraries for matrix operations and description logics. In the future, we aim to extend our prototype in order to empirically evaluate our theory.

A next step is to use our framework for repairing database and knowledgebase systems. Our ranking of ABox assertions can be extended in several ways to a ranking of repairs, using some notion of Pareto optimality. For example, if two facts α and β contradict one another and α is ranked higher than β, then a repair containing α is preferred over a repair containing β (all other facts being equal). This brings us in the realm of prioritized database repairing [Wij19], which we see as a promising way to enrich existing DL repair semantics (like IAR and AR). By narrowing the search space of possible repairs, we may also hope to gain efficiency compared to existing repair semantics.

Proof (of Theorem 3). Clearly, if x c is the solution to

and x 1 are rank-equivalent, we can fix c = 1 without loss of generality. Define a as follows:

By the Levy-Desplanques theorem, for every a ≥ a , the matrix a * 1 − b * M is invertible. For every a ≥ a , we write x a for the unique solution of the equation

For a ≥ a , define δ ij (a) := x a i − x a j , where x a i is the ith coordinate of x a . We will show that there is a value a * ≥ a such that for all a 1 , a 2 ≥ a * , for all 1 ≤ i < j ≤ N , δ ij (a 1 ) and δ ij (a 2 ) have the same sign, which implies that x a1 and x a2 are rank-equivalent.

Define the following matrix S |i in function of a, for 1 ≤ i ≤ N :

That is, S |i is obtained from a * 1 − b * M by replacing the ith column with 1 1 • • • 1 . By Cramer's Rule, we have

and consequently

Since the determinants det (•) are polynomial expressions, the following are all polynomials of degree at most N :

Let p ij = p i − p j for 1 ≤ i < j ≤ N . We determine a * such that for all a ≥ a * and for all 1 ≤ i < j ≤ N , the sign of p ij (a) does not change (i.e., is either always positive or always negative). Note that the sign of p ij not changing is equivalent to the sign of p ji not changing, so we can assume i < j without loss of generality.

In the remainder of the proof, we show that the desired a * exists and can be computed in polynomial time in N . Pick N +1 real numbers V = {a 1 , . . . , a N +1 }, all greater than a . Compute

for all a k ∈ V and 1 ≤ i < j ≤ N . The set

can be computed in polynomial time in N , because it involves N (N + 1) determinants (i.e., det S |i (a k ) for 1 ≤ i ≤ N and 1 ≤ k ≤ N + 1), each of which can be computed in polynomial time in N . For all 1 ≤ i < j ≤ N , the polynomial p ij can be computed from {(a 1 , p ij (a 1 )), . . . , (a N +1 , p ij (a N +1 ))} in polynomial time using, for example, Lagrange interpolation. The number of polynomials to compute is N (N −1) 2 (i.e., polynomially many), and each of them has at most N coefficients. We will represent the polynomial p ij by its coefficients, i.e., by (p ij ) 0 , . . . , (p ij ) nij where each (p ij ) is the coefficient of degree , and n ij ≤ N is the polynomial's degree. We now define a * ij as a * ij := max a , 2 + max

By Cauchy's bound on positive real roots of polynomials, if x 0 is a root of p ij , then x 0 < a * ij . This implies that if a 1 , a 2 > a * ij , then p ij (a 1 ) and p ij (a 2 ) have the same sign (i.e., either both positive or both negative), and therefore, by definition of δ ij , we have x a1 i < x a1 j if and only if x a2 i < x a2 j . Finally, let

which can be computed in polynomial time. By our construction, if follows that for all a 1 , a 2 > a * , the solutions x a1 , x a2 exist and are rank-equivalent. Finally, we incidentally note that a slightly better bound is obtained by letting a * = max a , 2 + max

This concludes the proof.