If a Description Logic (DL) system derives a consequence, then one can in principle explain such an entailment by presenting a proof of the consequence in an appropriate calculus. Intuitively, good proofs are ones that are simple enough to be comprehensible to a user of the system. In recent work, we have introduced a general framework in which proofs are represented as labeled, directed hypergraphs, and have investigated the complexity of finding small proofs. However, large size is not the only reason that can make a proof complex. In the present paper, we introduce other measures for the complexity of a proof, and analyze the computational complexity of deciding whether a given consequence has a proof of complexity at most q. This problem can be NP-complete even for EL, but we also identify measures where it can be decided in polynomial time.
The first work on explaining DL entailments is probably the PhD thesis of McGuinness [18], where the results obtained by the structural subsumption algorithm of the CLASSIC system [8] are translated into proofs in a formal calculus. The thesis also investigates how to create shorter, better understandable proofs by pruning away unimportant parts. In [6], proofs of subsumptions generated by a tableau-based system are translated into sequent proofs. The authors then investigate how to make the sequent proofs shorter. More recent work on explaining DL entailment was often focused on computing so-called justifications, i.e., minimal subsets of the knowledge base (KB) from which the consequence in question follows (see, e.g., [4,12,24]). The basic assumption is here that, whereas KBs may be very large and have many consequences, a single consequence often follows from a small subset of the KB by an easy derivation. While this is true in certain applications [5], in general it may be quite hard for a user to see without help why a consequence follows from a given justification [14]. On the one hand, this has triggered research into assessing the complexity of a justification, i.e., how hard it is to derive the given consequence from the justification [13,19]. On the other hand, it has rekindled the interest in generating proofs appropriate for human consumption. For example, the explanation plugin for the ontology editor Protégé described in [15] cannot only produce justfications, but can also display proofs, provided that proofs of an appropriate form are returned by the employed reasoner, an assumption that is, e.g., satisfied by the reasoner ELK [16]. While these proofs are represented in the formal syntax employed by Protégé, the work reported in [19,22,23] uses ontology verbalization techniques to translate proofs into natural language text.
Recently, we have investigated the complexity of deciding whether proofs of a certain size exist, which is measured in the number of steps involved in the proof [1]. Instead of concentrating on a specific DL and proof calculus or reasoner for this DL, we used a general framework in which proofs are represented as labeled, directed, acyclic hypergraphs whose vertices are labeled with axioms and hyperedges correspond to sound derivation steps. Note that such proofs need not be tree-shaped since a single axiom can be reused in multiple inference steps, thereby reducing the overall size of the proof. To abstract away from implementation details, we assume that a reasoner (called deriver to distinguish it from an actual implemented system) generates a so-called derivation structure, which consists of possible proof steps, from which actual proofs can be constructed. For example, if we consider the consequence-based reasoning approaches for the DLs EL and ELI described in [3], then we could obtain a derivation structure for a given KB and consequence by collecting all (finitely many) instantiated classification rules. The EL reasoner ELK actually returns such a derivation structure, which however only contains the rule instances that have actually been used during the reasoning process.
In this paper, we extend the results of [1] by considering more measures of proof complexity (other than size), with the ultimate goal of finding proofs that are easy to understand for users. In a recent user study [7], for example, it was observed that proof understandability can be influenced by the structure (e.g. linear vs. several independent reasoning threads), the complexity of the individual reasoning steps (e.g. whether a combination of quantifiers is involved), the representation of the domain (e.g. abstract concept and role names vs. long domain-specific names), and the overall format (e.g. graphical vs. textual).
In this paper, we consider a few possible approaches to defining proof complexity, where we focus on the overall structure of the proof. For this reason, we are not interested in the complexity/weight of individual axioms or inference steps, which has already been investigated in the literature [13,20]. For most of the paper, we use the size of an axiom (or group of axioms) as a proxy for their complexity, but it is easy to substitute other measures from the literature.
We now list a few approaches for defining proof complexity, which we discuss throughout this paper.
4. The hardness of a proof corresponds to its (weighted) tree size, i.e., the number (weighted sum) of vertices in its tree unraveling [1]. 5. A proof is as hard to understand as the hardest inference step. 6. The hardness of a proof is the sum (product, average, . . . ) of inference step weights. 7. Proof complexity is determined by the number of TBox axioms that are used, i.e., the size of a corresponding justification. 8. A proof is more complex if there are more inference steps between the TBox axioms and the conclusion. We could compute the maximal distance (depth), or the maximal sum of weights along such a path. 9. A linear proof is easier to follow, hence we could measure the pathwidth of a proof (when viewing a proof as an undirected graph obtained by replacing each directed hyperedge with several undirected edges between the conclusion and each premise). 10. We could consider a similary adapted notion of (undirected) treewidth as a measure for the complexity of a proof, which reflects its degree of connectivity. 11. Multiple adjacent reasoning steps using the same rule schema are easier to understand than when these steps are interspersed with other types of inference rules. 12. For the presentation to a user, it may also be relevant whether a proof is planar, i.e., it can be drawn without intersecting (hyper)edges.
There are of course many more ways in which "proof complexity" could be measured. This paper takes a few steps towards classifying the complexity of finding "best" proofs w.r.t. any such measure. Before we can introduce this problem formally, we recall the basic definitions from [1].
We assume a basic familiarity with description logics [3]. Most of our theoretical discussions apply to an arbitrary (description) logic; from now on, we fix one such logic L, where we focus on the terminological part, i.e., the TBox. Following the notation from [1], S L denotes all TBox axioms that can be formulated in L. We assume that the size |α| of such an axiom α is defined in some way, e.g. by the number of symbols in α. Given a TBox T and axiom α, a justification for α in T is a minimal subset J ⊆ T such that J |= α. Already for EL-ontologies, for which finding a single justification is possible in polynomial time, there may be still exponentially many justifications, and finding a justification of size ≤ n is NP-complete [4].
While justifications can pinpoint the reasons for an entailment in a TBox, we are interested in more detailed proofs such as, for example, the one in Figure 1.
As in [1], we view proofs as directed hypergraphs.
A (finite, directed, labeled) hypergraph [21] is a triple H = (V, E, ), where -V is a finite set of vertices, -E is a set of hyperedges (S, d) with source vertices S ⊆ V and target vertex d ∈ V , and -: V → S L is a labeling function that assigns axioms to vertices.
The size of H, denoted |H|, is measured by the size of the labels of its hyperedges:
has no incoming hyperedges, i.e., there is no (S, v) ∈ E, and v is a sink if it has no outgoing hyperedges, i.e., there is no (S, d) ∈ E such that v ∈ S. We denote the set of all leafs and the set of all sinks in H as leaf (H) and sink(H), respectively.
A hypergraph
In this case, we also say that H contains H and write
Definition 2 (Cycle, Tree). Given a hypergraph H = (V, E, ) and s, t ∈ V , a path P of length q > 0 in H from s to t is a sequence of vertices and hyperedges
where d 0 = s, d q = t, and d j−1 ∈ S j for all j, 1 ≤ j ≤ q. If there is such a path in H, we say that t is reachable from s in H. If t = s, then P is called a cycle.
A tree H = (V, E, ) with root t ∈ V is a hypergraph in which t is a sink and is reachable from every vertex v ∈ V \ {t} by exactly one path.
In particular, the root is the only sink in a tree, and all trees are acyclic and connected.
The following definition formalizes basic requirements for hyperedges to be considered valid inference steps from a given TBox.
We now define proofs as special derivation structures that derive a goal axiom.
Given an axiom η and a TBox T , a proof for T |= η is a derivation structure P = (V, E, ) over T that contains exactly one sink v η ∈ V , which is labeled by η, and is acyclic.
A tree proof is a proof that is a tree. A subproof of a hypergraph H is a subgraph of H that is a proof.
A from T = {A B, B ∃r.A}. The first proof is presented in hypergraph notation (cf. Figure 1) as a tree and the second one as a hypergraph without axiom label repetition, where the TBox axioms are marked with a thick border. Both of them can be seen as proofs in the sense of Definition 5 and they use the same inference steps, but have different numbers of vertices.
Two useful operations are the following of removal and replacement of subproofs above a vertex. Given a proof P = (V, E, ) and a vertex v ∈ V , the subproof of P with sink v is the largest subgraph P v = (V v , E v , v ) ⊆ P, where V v contains all vertices in V that have a path to v in P. Dually, we denote by
Intuitively, we obtain P −v by removing every vertex from P from which every path to the sink goes through v. P −v need not be a proof since v is now a leaf, but (v) may not be an axiom from T . Finally, for a proof P = (V , E , ) with sink v such that V ∩ V = {v} and (v) = (v), we define the proof P[v → P ] as P −v ∪ P . The intuitive idea here is that v, as every vertex in V , is labeled with an axiom that has its own proof above it. And P −v is obtained by removing the proof above v; vertices are kept only if they are used to prove other vertices in P. Then, P[v → P ] is the result of "replacing" the proof above v by P . Moreover, since P and P have only one vertex in common, it is guaranteed that the resulted hypergraph P[v → P ] is acyclic. Additionally, unravelling P into a tree can be seen as the result of recursively applying P[v → P v ] to every vertex v in P.
As in [1], we rely on a deriver (imagine a DL reasoner) that, given a TBox T and a goal axiom η, produces a derivation structure D that contains "all possible proofs". This structure describes all instances of inference rules that are relevant for constructing proofs for η, without us having to know how inferences are performed. The quest for a good proof thus becomes a search for a good proof expressible by the inference steps in D. Since reasoners may not be complete for proving arbitrary axioms of L, we restrict η to a subset C L ⊆ S L of supported consequences.
A deriver D is given by a set C L ⊆ S L and a function that assigns derivation structures to pairs (T , η) of TBoxes T ⊆ S L and axioms η ∈ C L , such that T |= η iff D(T , η) contains a proof for T |= η. A proof P for T |= η is called admissible w.r.t. D(T , η) if there is a homomorphism h : P → D(T , η). We call D a polynomial deriver if there exists a polynomial p(x) such that the size of D(T , η) is bounded by p(|T | + |η|).
We assume w.l.o.g. that D(T , η) does not contain two vertices with the same label; this does not affect our results.
Elk [16] can be seen as a polynomial deriver for EL in this sense, because it allows to instantiate the inference rules with only a polynomial number of ELconcepts, namely the subconcepts appearing in T or η. The derivation structure Elk(T , η) contains all allowed instances of these rules, where each axiom is represented by a unique vertex. Since the number of premises in each rule is bounded by 2, the size of this structure is polynomial. Elk is complete only for goal axioms of the form C D, where D is a concept name and C is a subconcept from T . To prove other kinds of entailments T |= η, one first has to adapt T and η, thus leading to a different derivation structure Elk(T , η).
There are consequence-based derivers for other DLs, but they may not be polynomial [9]. In [1], we described a polynomial deriver for expressive description logics that is based on forgetting [17] and may take double-exponential time to compute the polynomial derivation structure D(T , η). In [1], we also investigated exponential derivers, but here we focus on the case of polynomial derivers.
Taking into consideration the variety of examples in the introduction, we define a general class of complexity measures for proofs. Our goal is to find proofs that minimize these measures, i.e., lower numbers are better. Definition 7. A (complexity) measure is a function m : P L → Q ≥0 , where P L is the set of all proofs over L and Q ≥0 is the set of non-negative rational numbers.
We call m a Ψ-measure if, for every P ∈ P L ,
[P] m(P) is computable in polynomial time in the size of P,
[SI] every subproof of a homomorphic image of P weighs no more than P, i.e., m(P ) ≤ m(P) for any homomorphism h : P → P and P ⊆ h(P) such that P ∈ P L .
Intuitively, a Ψ-measure m does not increase when the proof gets smaller, either when parts of the proof are removed (i.e., for a subproof) or when parts are merged (i.e., for a homomorphic image). We cannot replace the property [SI] by two separate properties for each of these cases since the image of a proof P may not be acyclic, but has relevant acyclic subgraphs that should also not have larger weight than P. Due to [SI], there always exists a proof P for T |= η that is minimal w.r.t. m as well as non-redundant, i.e., there is no subproof P ⊂ P for T |= η. Moreover, two isomorphic proofs have the same weight w.r.t. m.
In Table 1, we provide examples of how the complexity measures from the introduction can be defined formally, where by P ∈ P we denote that P is a path in P, and by |P | the length of P . Since P is acyclic, there is always at least one such path. In this table, we use the size of an axiom or edge as a proxy for its complexity; other values from Q ≥0 could be used instead. The table covers all measures from the introduction except for Items 4 and 9-12. Tree size (Item 4) is defined recursively; we discuss this measure in the context of a more general family of "local" measures later in Section 4. The remaining items (9)(10)(11)(12) are not Ψ-measures: the problems behind Items 9 and 10, i.e., to determine the pathwidth or treewidth for proofs which are graphs are NP-hard [2]. Moreover, note that treewidth is not interesting in our context, since we can always obtain a tree-shaped proof (with minimal treewidth 1) by unraveling. A similar argument applies to Item 12 (planarity) since every tree is planar. We will discuss Item 11 separately in Section 5.
We now formally define our main problem: finding optimal admissible proofs w.r.t. a measure m and D(T , η). Definition 9 (Optimal Proof). Let D be a deriver and m be a measure. Given a TBox T and an axiom η ∈ C L , an admissible proof P w.r.t. D(T , η) is called optimal w.r.t. m if m(P) is minimal among all such proofs. The associated decision problem, denoted OP(D, m), is to decide, given T and η as above and q ∈ Q, whether there is an admissible proof P w.r.t. D(T , η) with m(P) ≤ q.
If D is a polynomial deriver, we add the superscript poly to OP. If m is a Ψ-measure, we add a subscript Ψ, e.g. OP poly Ψ (D, m). For the complexity analysis, we assume the deriver to be given in the form of a method that allows to access elements of D(T , η). The complexity of this method is not our concern here, we simply assume in the following that elements of D(T , η) can be accessed in constant time. Since all of our complexity bounds are at least P, our results remain the same for the derivers whose derivation structure can be constructed in polynomial time even if we take the complexity of computing the derivation structure into account.
We can show that if P is optimal w.r.t. a Ψ-measure m and D(T , η), then the homomorphic image of P in D(T , η) is also a proof. Thus, to decide OP Ψ (D, m) we can focus on proofs that are subgraphs of D(T , η). This is shown by the following lemma, which generalizes a result from [1]. The full proof can be found in the appendix. Lemma 10. For any Ψ-measure m, if there is an admissible proof P w.r.t. D(T , η) with m(P) ≤ q for some q ∈ Q, then there exists a subproof Q of D(T , η) for T |= η with m(Q) ≤ q.
Proof (Sketch). Let P be any such proof. Then there is a homomorphism h : P → D(T , η). If h(P) is a proof, then the claim immediately follows from [SI]. Otherwise, h(P) contains cycles, which must be due to different vertices in P with the same label that are connected by a path. We can iteratively remove such paths to obtain another proof P * that can be homomorphically mapped to a subproof Q of h(P) ⊆ D(T , η), and therefore m(Q) ≤ m(P) ≤ q by [SI].
In particular, this shows that an optimal proof always exists (recall that derivation structures are always finite). We can now show the following generic upper bound for our decision problem.
Ψ (D, m) is in NP.
Proof. We start by guessing a subgraph P of D(T , η). This can be done in non-deterministic polynomial time in the size of D(T , η), which is polynomial in the size of T and η. This subgraph P is necessarily sound, and checking the remaining properties of Definitions 4 and 5 and that m(P) ≤ q can be done in polynomial time in the size of P, in particular due to [P] in Definition 7.
Note that, one can similarly show an upper bound of NP for pathwidth, since checking m(P) ≤ q is in NP [2]. (First guessing P and then verifying m(P) ≤ q can be performed by a polynomially bounded sequence of non-deterministic steps.) Matching lower bounds hold for OP poly Ψ (D, m) with a fixed D and m being vertex size [1] or justification size [4]. As we already noted, all the complexity measures from Table 1, including vertex size and justification size, are Ψ-measures.
For m being vertex size or justification size, there is a polynomial deriver D such that OP poly Ψ (D, m) is NP-complete.
In this section, we consider a property that allows us to reduce the upper bound from NP to P. This also generalizes a result from [1]. Recall that intuitively, P[v → P ] denotes the result of replacing in P the proof above v by P .
Definition 14. Let P = (V, E, ) be a proof and v ∈ V . We say that a Ψ-measure m is local for v in P if for every proof Intuitively, if the measure is local, then we can replace subproofs by easier or harder alternative proofs, and the weight of the full proof will change accordingly. Measures that can be defined in a monotone, recursive way on the graph structure usually have this property:
the measures hardest axiom, hardest inference step, from Table 1; tree size defined for an ayclic
where m(H, v) := 1 + (S,v)∈E w∈S m(H, w); weighted tree size, defined similarly by m(H)
As the names of the last two measures indicate, local measures cannot distinguish between hypergraphs and their unravelings into trees, since unraveling of a proof P can be seen as recursively computing P[v → P v ] for all vertices v in P. That is fact to show that whenever v is chosen in Line 9, then P(v) is a minimal proof for (v) in D(T , η). This step uses an inductive argument that is based on the locality property of the measure m. Finally, by Lemma 10 we do not need to consider proofs that are not contained in D(T , η).
Since we can actually compute an optimal proof in polynomial time, the following complexity result follows.
Theorem 16. For any local Ψ-measure m, OP poly Ψ (D, m) is in P.
A matching lower bound was shown in [1] for the problem of finding an admissible tree proof of minimal vertex size. This is equivalent to finding an arbitrary proof of minimal tree size, since a tree proof (with the same tree size) can always be obtained by unravelling, and for tree proofs the measures tree size and vertex size coincide. Since tree size is a local Ψ-measure, we obtain the following.
). For m being tree size, there is a polynomial deriver D such that OP poly Ψ (D, m) is P-complete.
In this section, we discuss Item 11 from the introduction, which is part of ongoing work. To define such a measure, we need to extend the definition of hypergraphs by a function ρ that assigns to each hyperedge (S, d) a label, the idea being that ρ(S, d) is the name of the inference rule that was instantiated to obtain the inference step { (s)|s∈S}
. Based on this, we define the notion of chunks.
Definition 18. Given a proof P, a chunk of P is a maximal connected subgraph H ⊆ P such that ρ(e) = ρ(e ) for all hyperedges e, e in H .
Every proof has a unique decomposition into chunks that do not share hyperedges.
A proof can thus be measured by the chunk count, which is the number of its chunks. This measure follows the idea that proofs with less alternations between inference rules are easier to understand. Consider for example proofs P 1 and P 2 depicted in Figure 4. Both are proofs for the same entailment A ∃r.F , and P 1 has three chunks, while P 2 has only one (all inference steps follow the same rule schema), hence P 2 is easier to understand. Of course one can consider also more complicated measures that also take the size of the chunks into account.
Clearly, the measure satsifies [P]. However, we need extend the notion of homomorphism to take into account the edge labeling function ρ. Nevertheless, we conjecture that we can extend the NP upper bound in Section 3 to cover this measure by carefully adapting Condition [SI]. Unfortunately, the chunk count is not local, because it is not invariant under unraveling (which may copy a single chunk into multiple ones).
A ∃r.F Fig. 4. Two proofs P1 (on the left) and P2 of the same entailment A ∃r.F .
We have investigated the complexity of finding optimal proofs for description logic entailments w.r.t. a variety of measures. Obviously, size is not enough to evaluate the difficulties users face when trying to understand proofs, and existing measures for justification complexity (e.g. [13]) cannot capture the structural aspects of this problem. We identified two classes of structural measures, Ψ-measures and local Ψ-measures, and showed that finding optimal proofs w.r.t. such measures is in NP and in P, respectively, for polynomial derivers. In the future, we will investigate more measures, try to find more tractable subclasses, and identify properties of measures that make them P-hard or NP-hard. Most importantly, we will evaluate which measures are most relevant for practical purposes, to actually help users understand description logic proofs.
Lemma 8. Tree size and all measures in Table 1 except for depth and worst path are Ψ-measures. Indeed, depth, worst path and treewidth do not satisfy
Proof. It should be easy to see that, given a proof P, all the measures in Table 1 can be computed according to the formulas in polynomial time in the size of P.
Tree size also satisfies the property [P], see [1]. Since a homomorphism preserves edges and vertex labels, weights corresponding to the hardest, sum and size measures of subproofs of a homomorphic image is no greater than the weight of the proof.
In order to see why [SI] does not hold for depth and worst path, we use the following example in Figure 5. For simplicity we omit vertex labeling; we assume only (v) = (v ). Clearly, the graph on the left has depth 4, while its homomorphic image and a subproof obtained by omitting the cycle on the right have 5. A similar argument can be applied to worst path since depth is its special case (when the weight of an edge is always equal to 1).
The intuition behind why [SI] does not hold for treewidth is as follows. A connected graph G has treewidth 1 if and only if it is a tree. However, its homomorphic image of a tree is not necessary a tree. One can construct a tree proof and a homomorphism s.t. there is a subproof in the homomorphic image which is not a tree and, thus, has a treewidth greater than 1.
Despite the strong connection between treewidth and pathwidth, i.e., for any graph, its pathwidth is no smaller than its treewidth, we cannot conjecture a similar result for pathwidth. Cycles (if any) created by a homomorphism which also could increase pathwidth are not part of subrpoofs for [SI]. Lemma 10. For any Ψ-measure m, if there is an admissible proof P w.r.t. D(T , η) with m(P) ≤ q for some q ∈ Q, then there exists a subproof Q of D(T , η) for T |= η with m(Q) ≤ q.
Proof. Let P be such a proof with associated homomorphism h : P → D(T , η). If h(P) is acyclic, then by [SI] in Definition 7 we have m(h(P)) ≤ m(P) ≤ q. Since v v h(v) h(v ) Fig. 5. A homomorphism that increases depth and worst path of the graph P has a unique sink v η , it must be mapped to a unique sink h(v η ) in h(P), and thus h(P) is the desired subproof of D(T , η).
If h(P) is not acyclic, our goal is to find another admissible proof P * w.r.t. D(T , η) that uses a subset of the vertices of P such that h(P * ) ⊆ h(P) is acyclic, and therefore satisfies the requirements of the lemma by [SI] in Definition 7. For this purpose, consider an arbitrary cycle in h(P), which must be due to two vertices v, v in P such that h(v) = h(v ) and there is a path between v and v (or due to multiple such pairs of vertices). Since P is acyclic, we can assume that there is a path from v to v , but no path from v to v. We now consider the two subproofs P v and P v . As there is a path from v to v , we have P v ⊂ P v . Since h(v) = h(v ), both vertices are labeled with the same axiom. The idea of the following construction is to remove P v from P and replace it with P v , which effectively removes all paths from v to v .
More formally, we first consider the hypergraph H = P −v ∪ P v and then, in the hyperedges (S, d) in H that still contain v ∈ S, we replace v by v, effectively merging the two vertices, remove v from the set of vertices, and thus obtain a hypergraph P . If there was no such hyperedge, then v was the sink of P, i.e., (v ) = η, and v will now be the new sink in P with (v) = (v ) = η. We now show that P is also an admissible proof w.r.t. D(T , η). Our construction does not produce new leafs, and hence P is still grounded. Clearly, all remaining edges are sound since they were already sound in P. Moreover, P is acyclic since all cycles in P can be traced back to paths in P that involve both v and v ; but we have assumed that there are no paths from v to v, and have destroyed all paths from v to v . As argued above, we have also kept the property that there is exactly one sink, which is labeled with η. Observe that h is also a homomorphism from P to D(T , η) (when restricted to the vertex set of P ), because h(v) = h(v ), and moreover h(P ) ⊆ h(P).
The resulting proof P has less vertices than P since we have removed at least v . This means that, after finitely many such operations, we can obtain from P the desired proof P * such that h(P * ) ⊆ h(P) is acyclic. Since h(P * ) also has a unique sink labeled by η, it is a subproof of D(T , η) and m(h(P * )) ≤ m(P) ≤ q by [SI] in Definition 7.
Corollary 11. If T |= η, then, for every deriver D and Ψ-measure m, there is an optimal proof for T |= η w.r.t. D and m.
Proof. By Definition 6, the derivation structure D(T , η) contains at least one proof for T |= η. Since D(T , η) is finite, there are finitely many proofs for T |= η contained in D(T , η). The finite set of all weights of these proofs always has a minimum. Finally, if there were an admissible proof weighing less than this minimum, it would contradict Lemma 10.
For any local Ψ-measure m and polynomial deriver D, Algorithm 1 computes an optimal proof in time polynomial in the size of T and η.
Proof. We can show the following facts about this algorithm.
(I) Whenever P(v) is defined, then it is a proof for (v) contained in D(T , η).
We prove this by induction on the order in which the hypergraphs P(v) are constructed by Algorithm Item (II) implies that each vertex v ∈ V can be removed from Q at most once: in order for v to be added again to Q in Line 17, there would need to exist a proof other than P(v) with the same sink v but a smaller weight, but according to (II), after choosing v in Line 9, the algorithm does not construct any proofs with a weight smaller than m(P(v)) (for any sink). Therefore, in Line 14, during the complete run of the algorithm, each edge (S, d) ∈ E will be used at most once. Moreover, all primitive operations in the algorithm can be done in polynomial time, such as checking acyclicity of hypergraphs in Line 15 or finding the minimal value m(P(v)) in Line 9. It follows that Algorithm 1 terminates in time polynomial in the size of D(T , η), which is polynomial in the size of T and η. (IV) Every vertex v ∈ V that is the sink of a proof P contained in D(T , η) is added to Q at some point.
We prove this by induction on the structure of P. If P contains only v, then either (v) ∈ T , and hence v is added to Q in Line 4, or otherwise there is an edge (∅, v) in P (and hence in E), in which case v is added to Q in Line 6.
If P has more than one vertex, then it must contain at least one edge e = (S, v) ∈ E, where each s ∈ S is the sink of a subproof of P in D(T , η). By induction we know that each s ∈ S is added to Q at some point during the algorithm. By Item (III), they must also be removed from Q at some point afterwards, and hence eventually k(e) reaches |S| in Line 13. If P(v) was already defined at this point, then v had already been added to Q earlier. Otherwise, v is now added to Q in Line 17. (V) When the algorithm terminates and P(v) is defined, then m(P(v)) is minimal among all proofs for (v) contained in D(T , η). By (I), P(v) is a proof of this form. Assume to the contrary that there is a proof P for (v) contained in D(T , η) such that m(P) < m(P(v)).
Then P and P(v) must both have the sink v, because we assume that D(T , η) contains no two vertices with the same label. Assume moreover that i) P is an optimal proof for (v), that is, m(P) ≤ m(P ) for every other proof P for (v) in D(T , η) (cf. Corollary 11), and ii) among all other vertices v ∈ V for which there exists a proof P for (v ) in D(T , η) such that m(P ) < m(P(v )), we also have m(P) ≤ m(P ) and whenever m(P) = m(P ), then |P| ≤ |P |. Since P is optimal, we know that it has a unique last inference step (S, v). We show that, for every vertex w ∈ S, an optimal proof was assigned to P(w) before v was chosen in Line 9. We first show that for every w ∈ S, the subproof P w must be similarly minimal. If this were not the case, then there would be a proof P w for (w) in D(T , η) such that m(P w ) < m(P w ). But then, by locality, we have m(P[w → P w ]) < m(P), where P w is constructed from P w by renaming all vertices except w. Since P[w → P w ] is an admissible proof for (v) w.r.t. D(T , η), by Lemma 10 we know that D(T , η) contains a proof P for (v) with m(P ) ≤ m(P[w → P w ]) < m(P), contradicting the optimality of P. Hence, P w must be optimal among all proofs for (w) in D(T , η). Moreover, by [SI], we have m(P w ) ≤ m(P) and |P w | < |P|. By Assumption ii) and (IV), this means that P(w) is also optimal w.r.t. m among all proofs for (w) in D(T , η). Since both P w and P(w) are optimal in this sense, we obtain that m(P(w)) = m(P w ) ≤ m(P) < m(P(v)), which by (II) means that w must have been chosen (in Line 9) before v. To summarize, for every vertex w ∈ S, we know that an optimal proof for (w) with weight m(P w ) has already been assigned to P(w) before v is chosen in Line 9, and moreover each w ∈ S was chosen before v. But then, for one of these vertices w (the last one to be processed), a proof P is constructed from the subproofs P(w) and the edge (S, v) in Line 14. If we consider the variant P of P where each of the subproofs P(w) is renamed such that it shares only the vertex w with the rest of the proof, then by locality we have m(P ) = m(P ). Moreover, since m(P(w)) = m(P w ) holds for all w ∈ S, locality also yields that m(P ) = m(P). Since P was constructed as a candidate for P(v) by the algorithm, we know that m(P(v)) ≤ m(P ) = m(P), which contradicts our assumption that m(P) < m(P(v)). We obtain that P(v) must be optimal.
Acknowledgements This work was supported by the DFG in grant 389792660 as part of TRR 248 (https://perspicuous-computing.science), and QuantLA, GRK 1763 (https://lat.inf.tu-dresden.de/quantla). We also want to thank the anonymous reviewers for their many helpful comments.
Input: A derivation structure D(T , η) = (V, E, ), a local Ψ-measure m Output: An optimal proof of T |= η w.r.t. D(T , η) and m
// P(v) is optimal for (v) the reason why they are especially well-suited for cases where proofs are presented to users in the form of trees. This is for example the case for the Elk-proof plugin for Protégé [15].
Algorithm 1 describes a Dijkstra-like approach that is inspired by the algorithm in [10] for finding minimal hyperpaths w.r.t. so-called additive weighting functions, which represent a subclass of local Ψ-measures. It progressively defines proofs P(v) for (v) that are contained in D(T , η). If it reaches a new vertex v in this process, this vertex is added to the set Q. In each step, a vertex with minimal weight m(P(v)) is chosen and removed from Q. Whenever all source vertices of a hyperedge (S, d) have been processed in this way, a new proof for (d) is constructed by joining the proofs for the source vertices using the new hyperedge, and this is compared to the best previously known proof for (d). All proofs constructed in this way are tree proofs, but this restriction does not matter since m is local. For Line 18, recall that we assumed D(T , η) to contain no two vertices with the same label, and hence it contains a unique vertex v η with label η. Lemma 15. For any local Ψ-measure m and polynomial deriver D, Algorithm 1 computes an optimal proof in time polynomial in the size of T and η.
Proof (Sketch). The main argument is that the algorithm is monotone in the sense that the smallest weight min{m(P(w)) | w ∈ Q} can never decrease. Hence, easier proofs (according to m) will be constructed before harder ones. This shows that each vertex v will be removed at most once from Q in Line 17, and hence the algorithm terminates in polynomial time. Moreover, one can use the above