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.
Introduction
The first work on explaining DL entailments is probably the PhD thesis of
McGuinness [
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 [
In this paper, we extend the results of [
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 [
We now list a few approaches for defining proof complexity, which we discuss
throughout this paper.
1. A proof is at least as hard to understand as its hardest axiom.
2. The complexity of a proof is the sum (product, average, . . . ) of all weights of
its axioms.
3. As a special case of the previous item, the number of axioms constituting
the proof defines its complexity.
4. The hardness of a proof corresponds to its (weighted) tree size, i.e., the
number (weighted sum) of vertices in its tree unraveling [
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 [
Preliminaries
We assume a basic familiarity with description logics [
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. 2.1
Definition 1 (Hypergraph). A (finite, directed, labeled) hypergraph [
X |(S, d)|, where |(S, d)| := |`(d)| +
X|`(v)|. (S,d)∈E v∈S A vertex v ∈ V is called a leaf if it 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 H0 = (V 0, E0, `0) is called a subgraph of H = (V, E, `) if V 0 ⊆ V , E0 ⊆ E and `0 = `|V 0 . In this case, we also say that H contains H0 and write H0 ⊆ H. Given two hypergraphs H1 = (V1, E1, `1) and H2 = (V2, E2, `2) s.t. `1(v) = `2(v) for every v ∈ V1 ∩ V2, their union is defined as H1 ∪ H2 := (V1 ∪ V2, E1 ∪ E2, `1 ∪ `2).
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
P = (d0, (S1, d1), d1, (S2, d2), . . . , dq−1, (Sq, dq), dq), where d0 = s, dq = t, and dj−1 ∈ Sj 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. The hypergraph H is acyclic if it does not contain a cycle. The hypergraph H is connected if every vertex is connected to every other vertex by a series of paths and reverse paths.
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.
Definition 3 (Homomorphism). Let H = (V, E, `), H0 = (V 0, E0, `0) be two hypergraphs. A homomorphism from H to H0, denoted h : H → H0, is a mapping h : V → V 0 s.t. for all (S, d) ∈ E, one has h(S, d) := ({h(v) | v ∈ S}, h(d)) ∈ E0 and, for all v ∈ V , it holds that `0(h(v)) = `(v). Such an h is an isomorphism if it is a bijection and, its inverse, h− : H0 → H, is also a homomorphism. A v B
B v ∃r.A – grounded, i.e., every leaf v in D is labeled by `(v) ∈ T ; and – sound, i.e., for every (S, d) ∈ E, the entailment {`(s) | s ∈ S} |= `(d) holds. We now define proofs as special derivation structures that derive a goal axiom. Definition 5 (Proof). 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. – leaf (P−v) = leaf (P) ∪ {v} and – sink(P−v) = sink(P).
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 P0 = (V 0, E0, `0) with sink v such that V ∩ V 0 = {v} and `(v) = `0(v), we define the proof P[v 7→ P0] as P−v ∪ P0. 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 7→ P0] is the result of “replacing” the proof above v by P0. Moreover, since P and P0 have only one vertex in common, it is guaranteed that the resulted hypergraph P[v 7→ P0] is acyclic. Additionally, unravelling P into a tree can be seen as the result of recursively applying P[v 7→ Pv] to every vertex v in P. 2.3
As in [
Definition 6 (Deriver). A deriver D is given by a set CL ⊆ SL and a function that assigns derivation structures to pairs (T , η) of TBoxes T ⊆ SL and axioms η ∈ CL, 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 [
There are consequence-based derivers for other DLs, but they may not be
polynomial [
Measuring Proof Complexity 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 : PL → Q≥0, where PL 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 ∈ PL, [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(P00) ≤ m(P) for any homomorphism h : P → P0 and P00 ⊆ h(P) such that P00 ∈ PL.
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 P0 ⊂ 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.
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 [SI].
The remaining items (9–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 [
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 η ∈ CL, 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 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 [
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]. tu 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. Theorem 12. OPpΨoly(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. tu
Note that, one can similarly show an upper bound of NP for pathwidth, since
checking m(P) ≤ q is in NP [
Matching lower bounds hold for OPpoly(D, m) with a fixed D and m being
Ψ
vertex size [
Ψ 4
Local Measures
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 [
A Ψ-measure m is local if it is local for every vertex in 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:
m(H, v) := |`(v)| + P(S,v)∈E Pw∈S m(H, w). – the measures hardest axiom, hardest inference step, from Table 1; – tree size defined for an ayclic H = (V, E, `) by m(H) := Pv∈sink(H) m(H, v), where m(H, v) := 1 + P(S,v)∈E Pw∈S m(H, w); – weighted tree size, defined similarly by m(H) := Pv∈sink(H) m(H, v) with 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 7→ Pv] for all vertices v in P. That is
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
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é [
Algorithm 1 describes a Dijkstra-like approach that is inspired by the algorithm
in [
Theorem 16. For any local Ψ-measure m, OPpΨoly(D, m) is in P.
A matching lower bound was shown in [
Ψ 5
Chunks 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.
`(d) Definition 18. Given a proof P, a chunk of P is a maximal connected subgraph H ⊆ P such that ρ(e) = ρ(e0) for all hyperedges e, e0 in H0.
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 P1 and P2 depicted in Figure 4. Both are proofs for the same entailment A v ∃r.F , and P1 has three chunks, while P2 has only one (all inference steps follow the same rule schema), hence P2 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 v F1 u F2
A v F1
F1 v ∃r.F2 A v ∃r.F2
F2 v F A v ∃r.F
A v B
A v C
B v C A v D
C v D A v E
D v E A v ∃r.F
E v ∃r.F
Fig. 4. Two proofs P1 (on the left) and P2 of the same entailment A v ∃r.F . 6
Conclusion
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. [
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.
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 [SI].
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 [
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) = `(v0). 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]. tu 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 v0 h(v) h(v0)
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, v0 in P such that h(v) = h(v0) and there is a path between v and v0 (or due to multiple such pairs of vertices). Since P is acyclic, we can assume that there is a path from v to v0, but no path from v0 to v. We now consider the two subproofs Pv and Pv0 . As there is a path from v to v0, we have Pv ⊂ Pv0 . Since h(v) = h(v0), both vertices are labeled with the same axiom. The idea of the following construction is to remove Pv0 from P and replace it with Pv, which effectively removes all paths from v to v0.
More formally, we first consider the hypergraph H = P−v0 ∪ Pv and then, in the hyperedges (S, d) in H that still contain v0 ∈ S, we replace v0 by v, effectively merging the two vertices, remove v0 from the set of vertices, and thus obtain a hypergraph P0. If there was no such hyperedge, then v0 was the sink of P, i.e., `(v0) = η, and v will now be the new sink in P0 with `(v) = `(v0) = η. We now show that P0 is also an admissible proof w.r.t. D(T , η). Our construction does not produce new leafs, and hence P0 is still grounded. Clearly, all remaining edges are sound since they were already sound in P. Moreover, P0 is acyclic since all cycles in P0 can be traced back to paths in P that involve both v and v0; but we have assumed that there are no paths from v0 to v, and have destroyed all paths from v to v0. 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 P0 to D(T , η) (when restricted to the vertex set of P0), because h(v) = h(v0), and moreover h(P0) ⊆ h(P).
The resulting proof P0 has less vertices than P since we have removed at least v0. 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. tu 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. tu 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 η.
(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 1. The ones in Line 4 consist of a single leaf v, which is labeled by a TBox axiom, and hence are sound, grounded, acyclic, and have the single sink v. Similarly, P(v) in Line 6 is always a proof since it consists of a single edge from D(T , η), has no leafs, and has v as the only sink.
Consider now the hypergraph P constructed in Line 14 as a possible candidate for P(v) (where v = d). At this point, all P(s), s ∈ S, are already defined since the counter k(e) can only reach |S| if each s ∈ S has already been chosen in Line 9, and thus P(s) must have been defined. Hence, by induction, each P(s) is a proof for `(s) contained in D(T , η), and, because we assume that D(T , η) contains no two vertices with the same label, must have s as sink. This shows that the hypergraph P constructed in Line 14 is sound, grounded, and has a single sink, namely v. Finally, P(v) is only updated to P in Line 17 if P is acyclic and therefore it is a proof. (II) If vertex v is chosen before vertex w in Line 9, then m(P(v)) ≤ m(P(w)).
We show that after choosing v in Line 9 the algorithm cannot produce a new proof P in Line 14 with m(P) < m(P(v)), and thus the smallest weight min{m(P(w)) | w ∈ Q} can never decrease. Consider the proof P from Line 15. Since v ∈ S, we have P(v) ⊂ P, and therefore m(P(v)) ≤ m(P) by [SI]. (III) Algorithm 1 terminates in polynomial time.
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(P0) for every other proof P0 for `(v) in D(T , η) (cf. Corollary 11), and ii) among all other vertices v0 ∈ V for which there exists a proof P0 for `(v0) in D(T , η) such that m(P0) < m(P(v0)), we also have m(P) ≤ m(P0) and whenever m(P) = m(P0), then |P| ≤ |P0|.
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 Pw must be similarly minimal.
If this were not the case, then there would be a proof Pw0 for `(w) in D(T , η) such that m(Pw0) < m(Pw). But then, by locality, we have m(P[w 7→ Pw00 ]) < m(P), where Pw00 is constructed from Pw0 by renaming all vertices except w. Since P[w 7→ Pw00 ] is an admissible proof for `(v) w.r.t. D(T , η), by Lemma 10 we know that D(T , η) contains a proof P0 for `(v) with m(P0) ≤ m(P[w 7→ Pw00 ]) < m(P), contradicting the optimality of P. Hence, Pw must be optimal among all proofs for `(w) in D(T , η).
Moreover, by [SI], we have m(Pw) ≤ m(P) and |Pw| < |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 Pw and P(w) are optimal in this sense, we obtain that m(P(w)) = m(Pw) ≤ 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(Pw) 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 P0 is constructed from the subproofs P(w) and the edge (S, v) in Line 14. If we consider the variant P00 of P0 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(P00) = m(P0). Moreover, since m(P(w)) = m(Pw) holds for all w ∈ S, locality also yields that m(P00) = m(P). Since P0 was constructed as a candidate for P(v) by the algorithm, we know that m(P(v)) ≤ m(P0) = m(P), which contradicts our assumption that m(P) < m(P(v)). We obtain that P(v) must be optimal.