We propose a new procedure that can enumerate justifications of a logical entailment given a set of inferences using which this entailment can be derived from axioms in the ontology. The procedure is based on the extension of the resolution method with so-called answer literals. In comparison to other (SAT-based) methods for enumerating justifications, our procedure can enumerate justifications in any user-defined order that extends the subset relation. The procedure is easy to implement and can be parametrized with ordering and selection strategies used in resolution. We describe an implementation of the procedure provided in PULi-a new Java-based Proof Utility Library, and provide an empirical comparison of (several strategies of) our procedure and other SAT-based tools on popular E L ontologies. The experiments show that our procedure provides a comparable, if not better performance than those highly optimized tools. For example, using one of the strategies, we were able to compute all justifications for all direct subsumptions of Snomed CT in about 1.5 hour. No other tool used in our experiments was able to do it even within a much longer period.
Axiom pinpointing, or computing justifications—minimal subsets of axioms of the
ontology that entail a given logical consequence—has been a widely studied research
topic in ontology engineering [
In this paper, we present a new resolution-based procedure that enumerates all
justifications of an entailment given a complete set of inferences. Apart from requiring
completeness, the form of inferences can be arbitrary and does not depend on any
logic. For example, our method can be used with the inferences provided by existing
consequence-based procedures [
The paper is organized as follows. In Section 2 we describe related work. Section 3 defines basic notions such as inferences and resolution. In Section 4 we present the new procedure, and in Section 5 we describe its implementation and empirical evaluation. 2
There are, generally, two kinds of procedures for computing justifications [19] using a reasoner. Black-Box procedures use a reasoner solely for entailment checking, and thus can be used for any reasoner and DL. Glass-Box procedures require some additional information provided from a reasoner, such as inferences that the reasoner has used, and thus can only work with such reasoners.
In a nutshell, Black-Box procedures [
Many Glass-Box procedures focus on E L, because E L reasoning is relatively
simple and efficient. Some of them employ propositional satisfiability (SAT) solvers. Their
input are inferences recorded by the reasoner during classification of an ontology. The
inferences are used to reduce entailment to satisfiability of Horn clauses. This approach
was first used by EL+SAT [21, 23], that includes an E L reasoner which records the
inferences plus a few optimizations for reducing the set of inferences relevant to the goal.
A common feature of the SAT-based procedures is enumeration of the candidate
axiom sets exploiting the hitting set duality and further minimization of these candidates.
EL+SAT and EL2MUS [
Up to few optimizations, the mentioned SAT-based procedures use inferences only for the entailment check. Had they delegated the entailment check to a separate DL reasoner, they could be considered Black-Box. Our approach uses a similar encoding of derivability check, however, it does not rely on the hitting set duality and, instead, manipulates the inferences directly. 3
3.1 Inferences, Supports, and Justifications In this section, we introduce a general type of inferences that can manipulate any types of objects, that we call axioms. An inference is an expression inf of the form h 1; : : : ; n ` i where 1; : : : ; n is a (possibly empty) sequence of axioms called the premises of inf, and is an axiom called the conclusion of inf. An ontology is a finite set of axioms.
Let I be an inference set. An I-derivation from O is a sequence of inferences d = hinf1; : : : ; infki from I such that for every i with (1 i k), and each premise 0 of infi that is not in O, there exists j < i such that 0 is the conclusion of infj . An axiom is derivable from O using I (notation: O `I ) if either 2 O or there exists an Iderivation d = hinf1; : : : ; infki from O such that is the conclusion of infk. A support for O `I is a subset of O0 O such that O0 `I . A subset-minimal support for O `I is called a justification for O `I .
Suppose that j= is an entailment relation between ontologies and axioms. A support
for O j= is a subset of O0 O such that O0 j= . A subset-minimal support for
O j= is called a justification for O j= (also called a minimal axiom set MinA [
:a _ d c _ d
c _ a
In this section we introduce the resolution calculus, which is a popular method for
automated theorem proving [
To reduce the number of resolution inferences (and hence the size of the closure)
several refinements of the resolution calculus were proposed. The rules in Figure 1 can
be restricted using orderings and selection functions [
Example 2. Consider the set of Horn clauses 1-7 below. We apply resolution with free selection that selects the underlined literals in clauses. Clauses 8-10 are obtained by resolution inferences from clauses shown on the right.
1: :p1 _ p2 2: :p1 _ p3 3: :p2 _ :p3 _ p4 4: p1 5: p2 6: p3 7: :p4 8: :p3 _ p4 h3; 5i 9: p4 h6; 8i 10: h7; 9i
Note that the resolution rule was not applied, e.g., to clauses 3 and 6 because literal :p3 in clause 3 is not selected. Also note that many clauses in the closure above can be derived by several resolution inferences. For example, clause 5 can be obtained by 1Note that the factoring rule cannot apply to Horn clauses. resolving clauses 1 and 4 and clause 6 by resolving 2 and 4. Therefore the empty clause 10 can be derived from several subsets of the original clauses 1-7.
Although the resolution calculus is mainly used for checking satisfiability of a
clause set, it can be also used for finding unsatisfiable subsets of clauses. To do this,
it is sufficient to add to every input clause a fresh positive answer literal [
1: :p1 _ p2 2: :p1 _ p3 3: :p2 _ :p3 _ p4 4: p1 _ a1 5: p2 _ a2 6: p3 _ a3 7: :p4 8: p2 _ a1 h1; 4i 9: p3 _ a1 h2; 4i 10: :p3 _ p4 _ a2 h3; 5i 11: :p3 _ p4 _ a1 h3; 8i 12: p4 _ a2 _ a3 h6; 10i 13: p4 _ a1 _ a2 h9; 10i 14: p4 _ a1 _ a3 h6; 11i 15: p4 _ a1 h9; 11i 16: a2 _ a3 h7; 12i 17: a1 _ a2 h7; 13i 18: a1 _ a3 h7; 14i 19: a1 h7; 15i
The framed clauses 16-19 contain only answer literals, so the corresponding sets of clauses are unsatisfiable in conjunction with the input clauses without answer literals. For example, clause 16 means that clauses 1-3, 5-7 are unsatisfiable and clause 19 means that clauses 1-4, 7 are also unsatisfiable. Note that clause 19 subsumes clauses 17-18; if subsumed clauses are deleted, we obtain only clauses with answer literals that correspond to minimal subsets of clauses 4-6 that are unsatisfiable in conjunction with the remaining input clauses 1-3, 7. 4
In this section, we present a new procedure that, given an ontology O, an inference set I and a goal axiom g, enumerates justifications for O `I g. It uses the usual reduction of the derivability problem O `I g to satisfiability of propositional Horn clauses in combination with the resolution procedure with answer literals.
Given the derivability problem O `I g, we assign to each axiom i occurring in I a fresh atom p i . Each inference h 1; : : : ; n ` i 2 I is then translated to the Horn clause :p 1 _ _ :p n _ p . In addition, for each axiom 2 O that appears in I, we introduce a (unit) clause p . Finally, we add the clause :p g encoding the assumption that g is not derivable. It is easy to see that O `I g if and only if the resulting set of clauses is unsatisfiable.
We now extend this reduction to find justifications for O `I g. Recall that a subset O0 O is a support for O `I g if O0 `I g. Hence, the subset of clauses p for 2 O0 is unsatisfiable in combination with the clauses for the encoding of inferences and :p g . We can find all such minimal subsets (corresponding to justifications) by adding a fresh answer literal to every clause p with 2 O, and applying resolution on non-answer literals together with elimination of redundant clauses.
Example 4. Consider the ontology Oe, inferences Ie and axiom e from Example 1. To encode the derivability problem Oe `Ie e we assign atoms p1–p4 to the axioms occurring in Ie as follows: p1 : A v B u C; p2 : A v B; p3 : A v C; p4 : A v C u B: The encoding produces clauses 1-7 from Example 3: the inferences Ie are encoded by clauses 1-3, the axioms in Oe result in clauses 4-6 with answer literals, and the assumption that e is not derivable is encoded by clause 7. The derived clauses 16-19 correspond to supports of Oe `Ie e, and by eliminating redundant clauses 17-18, we obtain clauses 16 and 19 that correspond to justifications Oe0 and Oe00 from Example 1.
One disadvantage of the described procedure is that it requires the closure under the resolution rules to be fully computed before any justification can be found. Indeed, since derived clauses may be subsumed by later clauses, one cannot immediately see whether a clause with only answer literals corresponds to a justification or not. For example, clauses 17-18 in Example 3 are subsumed by clause 19 that is derived later, and hence do not correspond to justifications. We address this problem by using non-chronological application of resolution inferences. Intuitively, instead of processing clauses in the order in which they are derived, we process clauses containing fewer answer literals first. Thus, in Example 3, we process clause 15 before clauses 12-14.
The improved procedure can enumerate justifications, i.e., return justifications one by one without waiting for the algorithm to terminate. The procedure is described in Algorithm 1. It is a minor variation of the standard saturation-based procedure for computing the closure under (resolution) rules, which uses a priority queue to store unprocessed clauses instead of an ordinary queue. Let - be a total preorder on clauses (a transitive reflexive relation for which every two clauses are comparable). As usual, we write c1 c2 if c1 - c2 but c2 6- c1. We say that - is admissible if c1 c2 whenever the set of answer literals of c1 is a proper subset of the set of answer literals of c2. For example, it is required that :p3 _ p4 _ a1 p4 _ a1 _ a2, but not necessary that p4 _ a1 p4 _ a2 _ a3. Note that if c is derived by resolution from clauses c1 and c2 then c1 - c and c2 - c since c contains the answer literals of both c1 and c2.
We say that a clause d (not necessarily occurring in Q) is minimal w.r.t. Q if there exists no clause c 2 Q such that c d. A priority queue based on - is a queue in which the remove operation can take out only minimal elements w.r.t. Q.2 Given such a queue Q, Algorithm 1 initializes it with the translation of the input problem O `I (line 3) 2If there are several minimal elements in the queue, one of them is chosen arbitrarily. Algorithm 1: Enumeration of justifications using resolution
Enumerate(O `I , -): enumerate justifications for O `I input : O `I – the problem for which to enumerate justifications,
- – an admissible preorder on clauses 1 S createEmptyList() ; // for processed clauses 2 Q createEmptyQueue(-) ; // for unprocessed clauses 3 Q:addAll(encode(O `I )); // add the clause encoding of the problem 4 while Q 6= ; do 5 c Q:remove(); // take one minimal element out of the queue 6 c simplify(c); // remove duplicate literals from c 7 if c is not subsumed by any c0 2 S then 8 S:add(c); 9 if c contains only answer literals then 10 report decode(c); // a new justification is found 11 else // apply resolution rules to c and clauses in S 12 for c0 2 resolve(c,S) do 13 Q:add(c0); and then repeatedly applies resolution inferences between minimal clauses taken out of this queue (loop 4-13) and the clauses in S that were processed before. Specifically, the removed minimal clause c is first simplified by removing duplicate literals (line 6) and then checked if it is subsumed by previously processed clauses in S (in particular, if c was processed before). If c is subsumed by some c0 2 S, it is ignored and the next (minimal) clause is taken from the queue Q. Otherwise, c is added to S (line 8). If c contains only answer literals, then it corresponds to a justification (as we show next), which is then reported by the algorithm (line 10). Otherwise, resolution inferences are then applied on the selected non-answer literal in c (line 12). The new clauses derived by resolution are then added to Q (line 13) and the loop continues.
We now prove that Algorithm 1 in line 10 always returns a (new) justification. It is easy to see that if a clause d was minimal w.r.t. Q in the beginning of the while loop (line 4) then it remains minimal w.r.t. Q at the end of the loop (line 13). Indeed, for the clause c taken from the queue (line 5), we have c 6 d. For all clauses c0 obtained by resolving c with clauses from S (line 12) we have c - c0. Hence c0 6 d for all c0 added to Q (line 13) (for otherwise, c - c0 d). This, in particular, implies that each clause in S is always minimal w.r.t. Q and, consequently, if c1 was added to S before c2 then c1 - c2 (for otherwise c2 c1 and c1 would not be minimal w.r.t. Q when c2 2 Q). Hence, there cannot be two clauses c1 and c2 in S that contain only answer literals such that c1 is a proper sub-clause of c2 since in this case c1 c2, thus c2 must be added to S after c1, but then c2 would be subsumed by c1 (see line 7). Hence each result returned in line 10 is a (new) justification.
Since clauses are added to S in the order defined by -, the justifications are also returned according to this order. Hence Algorithm 1 can return justifications in any user-defined order - on subsets of axioms as long as s1 ( s2 implies s1 s2. Indeed, any such an order - can be lifted to an admissible order on clauses by comparing the sets of answer literals of clauses like the corresponding sets of axioms. For example, one can define s1 - s2 by jjs1jj jjs2jj where jjsjj is the cardinality of s. Instead of jjsjj one can use any other measure m(s) that is monotonic over the proper subset relation (i.e., s1 ( s2 implies m(s1) < m(s2)), e.g., the length of s—the total number of symbols needed to write down all axioms in s.
We have implemented Algorithm 1 as a part of the new Java-based Proof Utility Library (PULi).3 In our implementation, we used the standard Java priority queue for Q, and employed a few optimisations to improve the performance of the algorithm.
First, we have noticed that our implementation spends over 95% of time on checking subsumptions in line 7. To improve subsumption checks, we developed a new datastructure for storing sets of elements and checking if a given set is a superset of some stored set. In a nutshell, we index the sets by 128 bit vectors, represented as a pair of 64 bit integers, where each element in a set sets one bit of the bit vector to 1 using its hash value. This idea is reminiscent of Bloom filters.4 We store the sets in a trie5 with the bit vector as the key, and use bitwise operations to determine if one vector has all bits of the other vector, which gives us a necessary condition for set inclusion. Using this datastructure, we were able to significantly improve the subsumption tests.
We have also noticed that the queue Q often contains about 10 times more elements than the closure S. To improve the memory consumption, we do not create the resolvents c0 immediately (see line 12), but instead store in the queue Q the pairs of clauses (from S) from which these resolvents were obtained. This does not reduce the number of elements in the queue, but reduces the memory consumed by each element to essentially a few pointers.
We have evaluated our implementation on inferences computed for entailed
axioms in some large E L ontologies, and compared performance with SAT-based tools
for enumeration of justifications from inferences EL2MUS [
For our evaluation, we chose ontologies GO-PLUS, GALEN and SNOMED, which contain (mostly) E L axioms. GO-PLUS is a recent version of Gene Ontology,6 which imports a number of other ontologies. The provided distribution included subsumption axioms that were inferred (annotated with is_inferred), which we have removed. GALEN is the version 7 of OpenGALEN.7 We did not use the more recent version 8,
4https://en.wikipedia.org/wiki/Bloom_filter 5https://en.wikipedia.org/wiki/Trie 6http://geneontology.org/page/download-ontology 7http://www.opengalen.org/sources/sources.html because the other tools were running out of memory. SNOMED is the version of Snomed CT8 released on 2015-01-31. From the first two ontologies we removed non-E L axioms, such as functional property axioms, and axioms that contain inverse property expressions and disjunctions. We have also adapted the input ontologies, so that they could be processed by (the reasoner of) EL+SAT. We removed disjointness axioms and replaced property equivalences with pairs of property inclusions. Duplicate axioms were removed by loading and saving the ontologies with OWL API. With these ontologies, we have computed justifications for the entailed direct subsumptions between atomic concepts (in the following called the queries) using various tools. All queries were processed by tools in a fixed random order to achieve a fair distribution of easy and hard problems. We used a global timeout of one hour for each tool and a local timeout of one minute per query. To run the experiments we used a PC with Intel Core i5 2.5 GHz processor and 7.7 GiB RAM operated under 64-bit OS Ubuntu 14.04. Table 1 shows the numbers of axioms, atomic concepts, atomic roles, and queries of each input ontology.
As an admissible order on clauses for our implementation of Algorithm 1, we chose
the relation - that compares the number of different answer literals in clauses. When
using this order, cardinality-minimal justifications are found first. Note that finding such
justifications is NP-hard [
Table 3 shows for how many queries all justifications were computed within the global and local timeouts.9 The first six rows correspond to experiments on sat infer
9All experimental data is available at https://osf.io/9sj8n/ ences and the other six rows to experiments on elk inferences. Note that every tool processed more queries and had less relative timeouts on elk inferences. Notice that the resolution procedure with the Threshold selection strategy processed the most queries and had the least number of timeouts on all ontologies. In particular, for SNOMED it timed out only in one case. It turns out, that without any timeout Threshold was able to find all justifications for all queries of SNOMED within about 1.5 hours, with the longest query taking less than 4 minutes. None of the SAT-based tools was able to find all justifications for all queries of SNOMED even within 24 hours.
To determine whether the Threshold strategy was the best among the resolution strategies on all queries, we have plotted in Figure 2 the distributions of the query times for all resolution strategies. Each point hx; yi of a plot represents the proportion x of queries that were solved by the method in under the time y. For instance, TopDown solved about 90% of the queries of GALEN in under 0.1 seconds. Each plot considers only queries attempted by all tools on that plot. Since each plot represents the distribution of times and not a direct comparison of times for each query, even if one line is completely below another one, this does not mean that the corresponding method is faster for every query. To get a more detailed comparison, we have also plotted the distribution of minimum query times with a thin black line. For a query, minimum time is the time spent by the tool that was the fastest on that query (among the tools on the same plot). If a plot for some tool coincides with this black line at point (x; y), then all queries solved within time y by some tool were also solved within time y by this tool. In particular, this tool is the fastest for all queries with the minimal time y. This analysis shows, for example, that TopDown was the best tool for easy queries (solved under 0.1 seconds by some tool) in GALEN, and Threshold was the best tool for hard queries (solved over 1 second by all tools) on all ontologies.
In Figure 3 we present a similar comparison of Threshold with the SAT-based tools. Threshold comes as the winner for hard queries (solved over 0.1 seconds) in % of queries 80 90 GO-PLUS % of queries 80 90
GALEN 10 scond e s n i 1 iem
t 10 scond e s n i 1 iem
t 10 scond e s n i 1 iem
t 10 scond e s n i 1 iem
t % of queries 80 90 SNOMED % of queries 80 90 minimum % of queries 80 90
SATPin SNOMED.11 EL2MUS wins on queries solved between about 10 and 50 milliseconds in GALEN. For all other query ranges, there appears to be no absolute winner.
We presented a new procedure that enumerates justifications using inferences that derive the goal consequence from an ontology. The inferences are encoded as Horn clauses and resolution with answer literals is applied. Our procedure can be parameterized by an ordering in which the justifications should be enumerated (as long as it extends the subset relation) and by a strategy that selects literals for resolution. The algorithm is relatively easy to implement and it can be easily used also with non-Horn and nonpropositional clauses. Our empirical evaluation shows that the procedure provides comparable, if not better performance than other tools that also use inferences as input. We were able to compute all justifications for all direct subsumptions of Snomed CT in about 1.5 hours. Currently, we cannot explain the difference in the performance of the evaluated selection strategies. We hope to explore this question in the future. 10Plots on sat inferences have the same shape, except that all lines are shifted up. 11For other ontologies Threshold times out on some query for which some other tool does not. 16. Kazakov, Y., Krötzsch, M., Simancˇík, F.: The incredible ELK: From polynomial procedures to efficient reasoning with E L ontologies. J. of Automated Reasoning 53(1), 1–61 (2014) 17. Manthey, N., Peñaloza, R., Rudolph, S.: Efficient axiom pinpointing in EL using SAT technology. In: Lenzerini, M., Peñaloza, R. (eds.) Proc. 29th Int. Workshop on Description Logics (DL’16). CEUR Workshop Proceedings, vol. 1577. CEUR-WS.org (2016), http://ceur-ws.org/Vol-1577/paper_33.pdf 18. Morgado, A., Liffiton, M.H., Marques-Silva, J.: Maxsat-based MCS enumeration. In: Biere, A., Nahir, A., Vos, T.E.J. (eds.) Proc. 8th Int. Haifa Verification Conf. (HVC’12). Lecture Notes in Computer Science, vol. 7857, pp. 86–101. Springer (2012), http://dx.doi. org/10.1007/978-3-642-39611-3_13 19. Parsia, B., Sirin, E., Kalyanpur, A.: Debugging OWL ontologies. In: Ellis, A., Hagino, T. (eds.) Proc. 14th Int. Conf. on World Wide Web (WWW’05). pp. 633–640. ACM (2005), http://doi.acm.org/10.1145/1060745.1060837 20. Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57–95 (1987), http://dx.doi.org/10.1016/0004-3702(87)90062-2 21. Sebastiani, R., Vescovi, M.: Axiom pinpointing in lightweight description logics via hornsat encoding and conflict analysis. In: Schmidt, R.A. (ed.) Proc. 22st Conf. on Automated Deduction (CADE’09). Lecture Notes in Computer Science, vol. 5663, pp. 84–99. Springer (2009), http://dx.doi.org/10.1007/978-3-642-02959-2_6 22. Simancˇík, F., Kazakov, Y., Horrocks, I.: Consequence-based reasoning beyond Horn ontologies. In: Walsh, T. (ed.) Proc. 22nd Int. Joint Conf. on Artificial Intelligence (IJCAI’11). pp. 1093–1098. AAAI Press/IJCAI (2011) 23. Vescovi, M.: Exploiting SAT and SMT Techniques for Automated Reasoning and Ontology Manipulation in Description Logics. Ph.D. thesis, University of Trento, Italy (2011), http: //eprints-phd.biblio.unitn.it/477/