This paper concerns the problem of inconsistency in knowledge bases caused by ABox assertions. If such inconsistency occurs, users may be asked to rate the truthfulness of one or more ABox assertions. A potential di culty is that users may not well understand how di erent ABox assertions interact (and possibly con ict) with one another through the TBox axioms. We therefore introduce a principled framework that uses TBox axioms for inferring positive and negative support for ABox assertions. This leads to a system of linear equations whose solution enhances the user's truthfulness rating by means of logical information from the TBox.
Inconsistency is an important and recurrent problem in today's database and knowledge-base systems. Data errors are practically unavoidable in systems that integrate data coming from di erent sources. Two approaches to tackle this problem are data cleaning and consistent query answering (CQA) [Wij19]. The latter approach uses the notion of repair, which is a consistent knowledge base obtained by making some minimal amount of data corrections. A repair is conceptually not di erent from a cleaned knowledge base. However, whereas the process of data cleaning is supposed to end in a single cleaned knowledge base, the CQA approach allows for the possibility of multiple repairs (or possible worlds). In the Description Logics framework, di erent repairs correspond to di erent ABoxes, each one consistent with respect to a given xed TBox. When we move from a single-world perspective to a possible-worlds perspective, di erent semantics for logical reasoning become possible [BR13,LLR+10,LB16,BBG14,GM12,CLP18]. Eventually, all these semantics address the following central problem: Given a logical sentence ', assign some degree of truthfulness to '. Is ' true in some, most, or all repairs? What is the probability of ' being true? Is there strong support for|or resistance against|the sentence '? Throughout this paper, we use the term \truthfulness" in a loose and informal way; we could have used other terms instead: credibility, veracity, accuracy. . .
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 di erent 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 di culties to fully understand and take into account the logic that is expressed by, possibly extensive, TBoxes. To overcome this di culty, 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. 2
Consider the following knowledge base K0 = hT0; A0i.
T0 = 8 Professor v Person; 9 >><>>>>>>>> SSPttuueddrseeonnntt vvv P::eCPrrosooufnres;ses;or; =>>>>>>>>>>
9teaches v Professor; >>>>>>>>>:> 99at9etaatetctnhedenssds vvv SCCtoouuudrresseen;t; >>>>>>>>>>;
A0 = 8 John : Professor 9 >>>>>>>>><> DAKBvR2a ::: SCCtoouuudrresseent >>>>>>>>>=>
(John; DB2) : teaches >>>>>>>>:>> ((JB(oAhovnba;;;KKIARR))) ::: aaatttttteeennndddsss >>>>>>>>>>;
This knowledge base is inconsistent, because from (John; KR) : attends, we can infer John : Student by means of the axiom 9attends v Student. Then, by means of the axiom Student v :Professor, we can infer John : :Professor, which obviously contradicts the rst assertion in A0. In conclusion, (John; KR) : attends and John : Professor contradict one another. The vertices in the directed graph of Fig. 1 are the assertions of A0. 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 9teaches v 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 e ect of adding Ava : Professor to A0. One can observe that the values of the assertions (Ava; IA) : attends and Ava : Student have gone down because of con icts 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 u B v :C is a TBox assertion, then the set f(i; A), (i; B)g is a refuter of (i; C), but neither (i; A) nor (i; B) is a refuter on its own. 3
In Description Logics, di erent repairs correspond to di erent ABoxes, each one consistent with respect to a given xed TBox. When we move from a single ABox to a set of possible ABoxes, di erent 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 nding the best repairs according to some criteria, and of extracting consistent information that best complies with speci c needs. Sik Chun Lam et al. have proposed logic-based methods for repairing TBox axioms of unsatis able 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]. 4
Throughout this paper, we will assume that TBoxes are satis able. That is, for every TBox T , the knowledge base hT ; ;i is consistent. If a knowledge base hT ; Ai 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 hT ; Ai, 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. Signi cantly, the ranking only requires some super cial 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 de nitions that follow are relative to a xed knowledge base hT ; Ai in some xed Description Logic.
We de ne 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.
De nition 1. The following de nitions are relative to a knowledge base hT ; Ai, and an assertion 2 A.
A refuter of is an inclusion-minimal subset B of A with the property that hT ; Bi is consistent and hT ; B [ f gi is inconsistent.
A supporter of is an inclusion-minimal subset B of A with the property that hT ; Bi is consistent, 62 B, and hT ; Bi j= .
Example 1. Let T = fA v C; A v :Dg. Let A = fa : A; a : D; a : Cg. Then, { fa : Ag is a refuter of a : D, and a supporter of a : C.
{ fa : Cg is neither a refuter nor a supporter of a : A.
Proposition 1. Let hT ; Ai be a knowledge base in a monotonic Description Logic, and let 2 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 B0 is a supporter of , then B and B0 are not comparable by set inclusion.
Proof. The proof of the rst two items is straightforward. We next prove the last item. Assume B is a refuter of , and B0 is a supporter of . Consequently, (a) hT ; Bi is consistent; (b) hT ; B [ f gi is inconsistent; (c) hT ; B0i is consistent; and (d) hT ; B0i j= .
From (c) and (d), it follows hT ; B0 [ f gi is consistent.
We rst show B * B0. Assume for a contradiction that B B0, hence B[f g B0[f g. From (b) and our assumption that the underlying Description Logic is monotonic, it follows that hT ; B0 [ f gi is inconsistent, a contradiction.
Finally, we show B0 * B. Assume for a contradiction B0 B. From (d) and our assumption that the underlying Description Logic is monotonic, it follows hT ; Bi j= . By (a), it follows hT ; B [ f gi is consistent, which contradicts (b).
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 2A 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 exible and general, we do not impose any restrictions on the choice of the credibility function, which can be instantiated and adapted later on to t 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 de ne such that if two ABox assertions are logically con icting, 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 de ned previously.
Informally, we want that for every 2 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: ( )
X
B is a supporter of
X B is a refuter of 0
X 2B
1 ( )A 0
X 2B
1 ( )A : (1) 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 signi cant that (1) is recursive, in the sense that appears at both the lefthand and righthand of .
To shorten notations, we de ne mappings T : A ! 2A and F : A ! 2A, as follows:
T ( ) := fB F ( ) := fB
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 de ne an indicator function I from fT; F g 2A A A to f0; 1g:
I(L; B; ; ) = 1 if 2 B and B 2 L( ) 0 otherwise (2) 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 2 A, 0 (3)
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 2, if they rank assertions in the same way, that is, if for all ; 2 A, 1( ) > 1( ) if and only if 2( ) > 2( ). It is easily veri ed that if 1 2, then 1( ) = 1( ) implies 2( ) = 2( ). Obviously, 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 di erent ABox assessments, but rather in their induced rankings. 5
We will assume A = f 1; : : : ; N g. 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 6= 0: 8 a > >>< a > > >: a ( 1) = b ( 2) = b . .
. ( N ) = b ( 1) + c ( 2) + c ( N ) + c (4) 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 xing a = 1. The choice for using three numbers was made for reasons of exibility, but is not fundamental.
B A
Since we think of (1) as a positive proportionality, we require that a and b have the same sign, say both positive. Let Af be the square N N matrix such that for 1 i; j N ,
Aif;j := X f (B) (I(T; B; i; j )
I(F; B; i; j )) : It is easily veri ed that for every i 2 f1; : : : ; N g, Aif;i = 0.
For i 2 f1; : : : ; N g, we introduce a variable xi for the unknown ( i). We de ne X = x1 x2 xN |. Then, using (3), the system of equations (4) can be equivalently written as follows: (5) (6) (7) where 1 is the square identity matrix. Equation (6) has a unique solution if and only if the matrix a 1 b Af (which does not depend on c) is non-singular (i.e., is invertible). In that case, the solution ABox assessment is given by: X = a 1 b Af 1 c c c |
We should pick c 6= 0 to avoid the all-zero solution. Indeed, if a 1 b Af is non-singular and c = 0, then the solution to (7) yields the ABox assessment such that ( 1) = ( 2) = = ( N ) = 0, which obviously is of no interest for ranking ABox assertions.
Then, it is easily veri ed that for xed values of a and b, di erent choices for c lead to rank-equivalent solutions. Therefore, we can choose c = 1 without loss of generality, in which case in the solution, xi is the sum of all elements in the ith row of a 1 b Af 1. Two signi cant questions remain: 1. For which values of a and b is the square matrix a 1 b Af non-singular, such that (7) gives us a unique ABox assessment? Obviously, a 1 b Af is invertible if and only if 1 ab Af is invertible. Therefore, only the ratio between a and b matters in our subsequent analysis. 2. Are ABox assessments obtained for di erent values of a; b rank-equivalent?
From a graph-theoretical viewpoint, Af 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 6= j) has weight Aif;j . The task is then to assign a real number to each vertex such that the resulting graph satis es 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, di erent 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 di erent a; b become all rank-equivalent. Informally, the parameterization scheme converges to a unique ABox assessment modulo rank-equivalence. 6.1
Note that all diagonal elements in a 1 b Af are equal to a. The invertibility of a 1 b Af 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.
N matrix A is invertible if for every i 2 f1; : : : ; N g, jaiij > PjN=1jaij j.
j6=i all i 2 f1; : : : ; N g, we have jaj > jbj
From Theorem 1, it immediately follows that (7) has a unique solution if for PN
j=1 Aif;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 (f ig) = 1 for 1 i 4, we obtain: Then,
20 1 0 It follows from Theorem 1 that this matrix is invertible for a > 1, giving the following solution: Although distinct values for a lead to di erent ABox assessments, it is signi cant to observe that a 1 1 > a +11 (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. tu
The invertibility of a 1 is recalled next.
b Af may also follow from Banach's Lemma, which Theorem 2 (Banach's Lemma). Let M be a square matrix with the property that kM k < 1 for some operator norm k k. Then the matrix 1 M is invertible and (1 M ) 1 = 1 + M + M 2 + M 3 + .
Therefore, if we x a = 1 and pick b su ciently small (which is analogous to xing b = 1 and picking a su ciently large), then the matrix 1 b Af is invertible, and 1 b Af 1 = 1 + Af + . If we limit ourselves to the two most signi cant terms in this expansion, we get X = 1 + Af 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 Af ; in this row, supporters have a positive sign, and refuters a negative sign. 6.2
So it turns out that (6) has a unique solution with a; b 0 whenever the ratio a=b is su ciently large. A desirable property is that di erent 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 , ai < aj if and only if bi < bj . 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 x 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 2 R. Consider the following equation with real-number parameter a: a , the equation (8) has a unique solution; and { for all a1; a2 a , if X1 and X2 are solutions to (8) for parameters a1 and a2 respectively, then X1 and X2 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 di culty is the computation of the non-diagonal elements in Af , which are de ned by (5). Given i and j , this requires nding every B A such that j 2 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 2NN supporters or refuters not comparable by set inclusion. However, in practice, a xed upper bound on the size of supporters or refuters may be implied by the TBox, in a way captured by the following de nition.
De nition 2. We say that a TBox T is con ict-bounded if there exists a polynomial-time computable positive integer m such that for every knowledgebase hA; T i and 2 A, if B is a refuter or supporter of , then jBj m.
Con ict-boundedness arises in practice. For example, for every DL-Lite TBox, every supporter or refuter has cardinality 1 because each con ict in DL-Lite involves at most two assertions. Con ict-boundedness is also guaranteed in E L?nr (E L? with non-recursive empty concepts) de ned in [Ros11].
Theorem 4. Let T be a con ict-bounded TBox such that ABox consistency with respect to T can be checked in polynomial time. Then, for every ABox A, the matrix Af can be computed in polynomial time (in the size of A) if f is polynomial-time computable.
Proof. Let N := jAj. Recall that Af is an N N matrix given by (5). Since T is con ict-bounded, say with bound m, for every B A, if jBj > 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 jBj 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 Af can be computed in polynomial time. tu
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 e ciency compared to existing repair semantics.
Acknowledgments We thank the anonymous reviewers for their helpful comments.
A
Proof (of Theorem 3). Clearly, if xc is the solution to with c > 0, and x1 is the solution to (a 1 b By the Levy-Desplanques theorem, for every a a0, the matrix a 1 b M is invertible. For every a a0, we write xa for the unique solution of the equation (a 1 b
M ) X = 1 1 1 | : For a a0, de ne ij (a) := xia xja, where xia is the ith coordinate of xa.
We will show that there is a value a a0 such that for all a1; a2 a , for all 1 i < j N , ij (a1) and ij (a2) have the same sign, which implies that xa1 and xa2 are rank-equivalent.
De ne the following matrix Sji in function of a, for 1 i
N : (Sji(a))`k = ((a 1 1 b M )`k if k 6= i if k = i
1 1 1 |. By Cramer's Rule, we have M by replacing the ith column with and consequently xia =
det Sji(a) det (a 1 b M )
;
ij(a) =
det Sji(a)
det (a 1
det Sjj(a)
b M )
:
(9)
(
N . The set fpij(ak) j 1 i < j
N; 1 k
N + 1g can be computed in polynomial time in N , because it involves N (N + 1) determinants (i.e., det Sji(ak) 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 pij can be computed from f(a1; pij(a1)), . . . , (aN+1; pij(aN+1))g in polynomial time using, for example, Lagrange interpolation. The number of polynomials to compute is N(N 1) (i.e., polynomially many), and each of them has at most 2 Since the determinants det ( ) are polynomial expressions, the following are all polynomials of degree at most N : { pi(a) = det Sji(a) ; { pj(a) = det Sjj(a) ; and { p(a) = det (a 1 b M ).
If a a0, then since the polynomial p(a) does not vanish, the sign of ij(a) is fully determined by the expression det Sji(a)
det Sjj(a) :
Let pij = pi pj for 1 i < j N . We determine a such that for all a a and for all 1 i < j N , the sign of pij(a) does not change (i.e., is either always positive or always negative). Note that the sign of pij not changing is equivalent to the sign of pji 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 = fa1; : : : ; aN+1g, all greater than a0. Compute N coe cients. We will represent the polynomial pij by its coe cients, i.e., by h(pij )0; : : : ; (pij )nij i where each (pij )` is the coe cient of degree `, and nij N is the polynomial's degree. We now de ne aij as aij := max a0; 2 + By Cauchy's bound on positive real roots of polynomials, if x0 is a root of pij , then x0 < aij . This implies that if a1; a2 > aij , then pij (a1) and pij (a2) have the same sign (i.e., either both positive or both negative), and therefore, by de nition of ij , we have xia1 < xja1 if and only if xia2 < xja2 . Finally, let a = 1 mi<ajx N aij ; which can be computed in polynomial time. By our construction, if follows that for all a1; a2 > a , the solutions xa1 ; xa2 exist and are rank-equivalent.
Finally, we incidentally note that a slightly better bound is obtained by letting
: This concludes the proof.