Given the high expressivity of modern ontology languages, such as OWL, there is the possibility for great diversity in the logical content of ontologies. Informally, this can be seen by the constant evolution of reasoners to deal with new sorts of content and the range of optimisations reasoners need in order to be competitive. More formally, the fact that many naturally occurring entailments have multiple justications (i.e., minimal entailing subsets) indicates that ontologies often overdetermine their consequences, indicating a diversity in supporting reasons. However, the multiplicity of justi cations might be due mostly to diverse material, not formal, grounds for an entailment. That is, the logical form of these multiple reasons could be less diverse than their numbers suggest. In the present paper, we introduce and explore several equivalence relations over justi cations for entailments of OWL ontologies. These equivalence relations range from strict isomorphism to a looser notions which cover similarities between justi cations containing di erent concept expressions or possibly di erent numbers of axioms. We survey a corpus of ontologies from the bio-medical domain and nd that large numbers of justi cations can often be reduced to a signi cantly smaller set of justi cations which are isomorphic with respect to one of the given de nitions.
Since its standardisation by the W3C in 2004, the Web Ontology Language
OWL has been used to represent domain knowledge from diverse areas, such
as medicine and general biology. OWL 21 is based on the highly expressive
Description Logic SROIQ [
Justi cations, minimal entailing subsets of an OWL ontology, provide helpful and easy-to-understand explanation support when repairing unwanted entailments in the ontology debugging process. While previous research has focused on the issue of making individual justi cations easier to understand, only little attention has been paid to the occurrence of multiple justi cations other than
the computational problems they often imply. An entailment of an OWL ontology can have a large number of justi cations (potentially exponential in the number of axioms in the ontology), with up to several thousands found in large real-life ontologies.
When encountering justi cations for a nite set of entailments of an ontology (e.g. the set of entailed atomic subsumptions), we are often faced with a seemingly large and diverse body of reasons why these entailments hold. On closer inspection, however, we frequently nd that multiple justi cations for di erent entailments are identical sets of axioms, or that justi cations are structurally identical and only diverge in the concept, role, and individual names they use.
In order to draw a clearer picture of the logical diversity of a corpus of justications, we need to take into account these similarities between justi cations. Grouping the set of justi cations into subsets according to some similarity measure helps structuring the unsorted pool of justi cations. Rather than trying to understand each individual justi cation, users can focus on understanding the template of a particular subset of justi cations. This can lead to signi cantly fewer justi cations that the user has to deal with, and therefore to a reduction in user e ort.
A well-known syntactical equivalence relation in OWL is structural equivalence. The OWL Structural Speci cation2 states the condition for two OWL objects (named concepts, roles, or instances, complex expressions, or OWL axioms) to be structurally equivalent. In short, it de nes the objects to be equivalent if they contain the same names and constructors, regardless of ordering and repetition (in an unordered association). The OWL API,3 a Java API which is used to manipulate OWL ontologies, implements this notion of structural equivalence by default.
Justi cation isomorphism [
While justi cation isomorphism helps to eliminate the e ects of diverging concept, role, and individual names, we can also identify types of justi cations which may be considered to be very similar despite their use of di erent constructors:
J1 = fA v B u C; B u C v Dg j= A v D
J2 = fA v 9r:C; 9r:C v Dg j= A v D In this example, the semantics of the complex concept expressions BuC in J1 and 9r:C in J2 are not relevant for the respective entailment; their occurrences in the 2 http://www.w3.org/TR/owl2-syntax 3 http://owlapi.sourceforge.net 4 Modulo structural equivalence, which takes into account redundant expressions and the commutativity of constructors. justi cations and their entailments can be replaced by freshly generated atomic concept names without a ecting the entailment relation. Such a substitution in turn would make the two justi cations isomorphic.
Likewise, justi cations of di erent lengths may be considered similar if their general structure of reasoning is identical:
J1 = fA v B; B v Cg j= A v C
J2 = fA v B; B v C; C v Dg j= A v D
These two justi cations clearly require the same form of reasoning from a user. Strict isomorphism only applies to justi cations which contain the same number of axioms; it does not cover situations like the above. However, for the purpose of structuring sets of justi cations and analysing the logical diversity of a corpus of justi cations, capturing those kinds of similarities illustrated in the above examples would be highly desirable.
These examples motivate a looser notion of isomorphism, which allows us to identify justi cations as equivalent if they require the same reasoning mechanisms, regardless of size, signature and logical constructors used. In the present paper, we introduce two new types of equivalence relations based on matching subexpressions and lemmas, and show how these extended relations are applied to a corpus of justi cations from the bio-medical domain. 2
Justi cations in OWL We assume the reader to be familiar with OWL and the underlying Description Logic SROIQ. In what follows, A; B; : : : denote concept names in an ontology O, r; s role names, and sig( ) denotes the set of concept, role, and individual names in an OWL axiom .
Justi cations [
O; J j=
For every axiom which is asserted in the ontology, the axiom itself naturally is a justi cation. We call an entailment which has only itself as a justi cation a self-supporting entailment, and the justi cation a self-justi cation.
It is important to note that a justi cation is always de ned with respect to an entailment . In the remainder of this paper we will therefore use the term justi cation to describe a justi cation-entailment pair (J , ) where J is a justi cation for .
Justi cation Isomorphism Isomorphism between justi cations was rst
introduced as a method to reduce the number of similar justi cations when
sampling from a large corpus to justi cations of distinct types [
De nition 2 (Justi cation Isomorphism) Two justi cations (J1; 1), (J2; 2) are isomorphic ((J1; 1) i (J1; 1)) if there exists an injective renaming which maps concept, role, and individual names in J1 and 1 to concept, role, and individual names in J2 and 2, respectively, such that (J1) = J2 and ( 1) = 2.
J1 = fA v B u 9r:C; B u 9r:C v Dg J2 = fE v B u 9s:F; B u 9s:F v Dg = fA 7! E; C 7! F; r 7! sg j= A v D j= E v D
The relation i is symmetric, re exive and transitive, from which it follows that i is an equivalence relation and thus partitions a set of justi cations. Justi cation isomorphism preserves the numbers and types of axioms and subexpressions in the justi cations: 1. J1 i J2 ! jJ1j = jJ2j 2. J1 i J2 ! jsig(J1)j = jsig(J2)j 3. The sets of logical constructs used in J1 and J2 coincide.
In the remainder of this paper, we may refer to the isomorphism de ned above as strict isomorphism in order to distinguish it from the other equivalence relations. 3
From the above de nition of isomorphism it follows that only justi cations which have the same number and types of axioms and subexpressions can be isomorphic. It is easy to see, however, that justi cations can have a similar structure despite their use of di erent concept expressions, as demonstrated in Example 1. This motivates a notion of isomorphism which allows not only the mapping of concept names, but also that of subexpressions.
The idea of nding similarities between concepts in Description Logics has
been widely explored in the work on uni cation and matching, e.g. [
While the basic idea behind extended subexpression-isomorphism is based on uni cation and matching, the concepts are not directly applicable to the given problem of matching justi cations. We therefore introduce a unifying justi cation J , which functions as the template for the isomorphic justi cations: De nition 3 (Subexpression-Isomorphism) Two justi cations (J1; 1), (J2; 2) are s-isomorphic ((J1; 1) s (J2; 2)) if there exists a justi cation (J ; ) and two injective substitutions 1; 2, such that 1(J ) = J1, 2(J ) = J2, 1( ) = 1, and 2( ) = 2. The mappings 1 and 2 map concept, role, and individual names in (J ; ) to subexpressions of (J1, 1) and (J2; 2), respectively.
It can be shown that the relation s is re exive, transitive and symmetric; it is therefore an equivalence relation and thus partitions a set of justi cations.
The substitutions 1; 2 are injective, but not surjective, as the set of subexpressions in the justi cations J1 and J2 can be of higher arity than the set of concept names in the unifying justi cation J (unless the justi cations themselves contain no complex expressions).
S-isomorphism can easily be shown to be a more general case of strict isomorphism between two justi cations J1 and J2: The unifying justi cation J is set to J1, 1 is the identity relation id which maps J1 to itself, and 2 corresponds to the mapping , which maps concept, role, and individual names in J2 to the respective names in J1. It follows that J1 i J2 ! J1 s J2.
In order to be s-isomorphic, the justi cations may di er in the number of subexpressions. They must, however, have the same number of axioms: J1 s J2 ! jJ1j = jJ2j
While we focus on entailed atomic subsumptions in the present paper, we point out that s-isomorphism between justi cations is not restricted to a speci c axiom type as entailment, as the substitutions 1; 2 preserve all entailment relations regardless of the axiom type and constructor usage. 4
While s-isomorphism covers a number of justi cations that can be regarded
as equivalent due to them requiring the same type of reasoning to reach the
entailment, it only applies to justi cations which have the same number of
axioms. This does not take into account cases where the justi cations di er only
marginally in some subset, but where the general reasoning may be regarded as
similar nonetheless. We therefore introduce the notion of lemma-isomorphism,
which extends subexpression-isomorphism with the substitution of subsets of
justi cations through intermediate entailments, so-called lemmas [
J1 = fA v B; B v Cg J2 = fA v B; B v C; C v Dg j= A v C j= A v D
It is straightforward to see that both J1 and J2 require the same type of reasoning from a human user. As the justi cations only di er in the length of the atomic subsumption chains that lead to the entailment, we can certainly consider them to be similar with respect to some similarity measure. However, the two justi cations are not considered isomorphic with respect to the de nitions for strict isomorphism or subexpression-isomorphism. We therefore introduce a new type of isomorphism which takes into account the fact that subsets of justi cations can be replaced with intermediate entailments which follow from them.
Lemmas of OWL justi cations have previously found use in the extension of
justi cations to justi cation-oriented proofs [
De nition 4 (Lemma) Let J be a justi cation for an entailment . A lemma of (J ; ) is an axiom for which there exists a subset S J such that S j= . A summarising lemma of (J ; ) is a lemma for which there exists an S J such that J n S [ f g j= for S j= .
De nition 5 (Lemmatisation) Let (J ; ) be a justi cation, let S1 : : : Sk be subsets of J , and let 1 : : : k be axioms satisfying Si j= i for i 2 f1; : : : ; kg. Then the set J := (J n S Si) [ S i is called a lemmatisation of J if J j= .
If clear from the context, a lemmatisation J may also be called a lemmatised justi cation. Given the de nitions for lemmatisations, we can now de ne lemmaisomorphism as an extension to subexpression-isomorphism: De nition 6 (Lemma-isomorphism) Two justi cations (J1; 1), (J2; 2) are `-isomorphic ((J1; ) ` (J2; )) if there exist lemmatisations J1 1 ; J2 2 which are s-isomorphic: J1 1 s J2 2 .
Lemma-isomorphism using arbitrary lemmas as de ned above carries some undesirable properties: First, unlike the previously de ned relations, it describes a relation which is not transitive. Further, the lemmatised justi cations might di er strongly from the original justi cations; in the most extreme case, the lemmatisation of a justi cation can be the entailment itself. We therefore have to introduce some constraints on the admissible lemmatisations in order to guarantee the transitivity of the isomorphism relation, as well as preserve the nature of the original justi cations. In what follows we will focus on lemmatisations through obvious steps in justi cations. 4.1
The notion of obvious proof steps [
In atomic subsumption chains of the type A0 v A1; A1 v A2 : : : An 1 v An only the relation between the subconcept A0 in the rst axiom and the superconcept An in the last axiom are relevant for understanding the subsumption chain; i.e. the step from the subconcept to the nal superconcept is obvious. We can say that it is only important to understand that there is a connection between the subconcept and the nal superconcept, but we do not need to know what this connection is. Therefore, it seems reasonable to substitute the chain with its conclusion in the form of a single axiom A0 v An. Restricting lemmatisations to atomic subsumption chains leads to the de nition for a transitivity-preserving type of l-isomorphism:
(J1; 1), (J2; 2) are `t-isomorphic ((J1; ) `t (J2; )) if there exist summarising lemmatisations J1 1 ; J2 2 which are s-isomorphic, and every Si Ji where Si j= i 2 1( i 2 2, respectively) is of type fAi v Ai+1 j i 2 f0; : : : ; ngg where n is the number of axioms in the respective chain of subsumption axioms, and Ai a concept name.
Atomic subsumption chains represent only one of many examples of such lemmatisations which preserve transitivity. For the purpose of introducing lemmaisomorphism as an equivalence relation, it su ces to focus on this particular type of lemmatisations, as it captures a frequently occurring pattern in OWL justi cations. 5 5.1
We performed a survey of equivalence relations in OWL- and OBO-ontologies from the NCBO BioPortal. The BioPortal provides ontologies from various groups from the biomedical domain, including the full set of daily updated OBO Foundry5 ontologies, which are built based on common design principles. OBO ontologies use a at- le format, which can be translated into OWL 2 and were therefore included in the test corpus.
At the time of downloading (January 2012), the BioPortal listed 278 OWLand OBO-ontologies, of which 241 could be downloaded, merged with their imports, and serialised as OWL/XML. 15 of those ontologies could not be processed in the given time frame of 30 minutes using the selected reasoner, and another 25 did not contain any relevant entailments (direct subsumptions between named classes). For the remaining 201 ontologies, we computed justi cations for all entailments with a maximum of 500 justi cations per entailment. Self-supporting entailments and self-justi cations were excluded from the survey, which led to the discarding of further ontologies.
The nal corpus of justi cations consisted of 6,744 justi cations from 83 ontologies, covering a broad spectrum of sizes and complexity. Half of the ontologies had less than 1000 named concepts and axioms, with the other half reaching a maximum of 13,959 concepts and 70,015 axioms. Likewise, the expressivity of the corpus ranged from AL to several highly expressive samples in SROIQ, which corresponds to the OWL 2 language. A detailed listing of the surveyed ontologies, as well the complete data from the study is available online.6 5.2
The algorithm for detecting structural similarities between justi cations (and therefore, OWL axioms) uses a purely syntactic search for matching subexpressions of OWL axioms. The axioms are rst parsed into a tree form, which allows for pairwise comparison of the nodes which represent connectives as well as concept and role names. The implementation uses the OWL API (v3.2.4.) and the HermiT (v1.3.6.) reasoner. Our experiments were performed on a 3GHz Intel Core2 Duo machine with 4GB of RAM allocated to the Java Virtual Machine. The 7051 justi cations in the test corpus could be analysed for strict isomorphism in approximately 3 minutes. 5.3
Isomorphic Justi cations Strict isomorphism applied to all justi cations of the individual ontologies drastically reduces the number of regular justi cations from an average of 81.3 ( = 185:5) justi cations per ontology to 10.5 ( = 18:0) templates for equivalent justi cations. The mean number of justi cations per template is 7.7 ( = 41:7) , which means that in each ontology nearly 8 justi cations have an identical structure. This e ect is highly visible in the Orphanet Ontology of Rare Diseases, where the a single template covers 901 (of 1139) justi cations for distinct entailments. These justi cations are all of the type fgen x v (9geneOf:pat y); Domain(geneOf; gen id 1)g j= gen x v gen id 1 where x and y denote identi ers used in the ontology.
Likewise, in the Cognitive Atlas ontology, all 401 justi cations for a single entailment are reduced to only one template. Intuitively, it seems that we can observe a much stronger reduction on a large set of justi cations than those ontologies that produce only 1 or 2 justi cations. And indeed, there exists a strong correlation between the number of justi cations of an ontology and the amount of reduction (Spearman's = 0:78). However, even some of the larger sets of justi cations are only reduced by a small proportion. The 95 justi cations of the Gene Regulation Ontology are represented by 61 distinct templates, which indicates a fairly diverse corpus.
When applied across all justi cations from the corpus, strict isomorphism reduces the corpus from 6,744 justi cations to only 614 templates, a reduction 6 http://owl.cs.manchester.ac.uk/research/publications/supporting-material/justiso-dl2012 to only 9.1% of the original corpus. On average, 11 justi cations share the same template, with the most frequent template occurring 1,603 times across 18 di erent ontologies; coincidentally, this template is of the same form as the Orphanet Ontology described above. The most prevalent template in the corpus, based on its occurrence in 37 distinct ontologies, is an atomic subsumption chain with 2 axioms.
Subexpression-Isomorphism The reduction from strict isomorphism to sisomorphism is clearly less drastic than the di erence between the main pool and the non-isomorphic pool. The justi cations of the 83 ontologies are reduced from an average of 81.3 justi cations to 8.8 templates ( = 13:1), which is a reduction by 1.7 templates compared to strict isomorphism. An average of 9.2 justi cations ( = 46:6) in an ontology share the same template.
Surprisingly, the majority of ontologies (67) does not show any di erence between strict isomorphism and s-isomorphism. Only 2 ontologies, the Lipid Ontology and Bleeding History Phenotype, are signi cantly a ected by s-isomorphism, with a reduction from 118 to 13 templates (11.0%) and 32 to 14 templates (43.8%), respectively. Recall that two justi cations are s-isomorphic, if their different complex subexpressions can be mapped to an atomic variable name. The signi cant reduction therefore suggests that in these two ontologies complex expressions are frequently used in the same way as atomic concepts.
Closer inspection reveals, however, that a large number of justi cations in the Lipid Ontology consist of one axiom of the form A B u x, with the entailment being A v B. Here, x represents a number of complex expressions of varying nesting depth. While s-isomorphism captures these types of justi cations as equivalent, the actual reason for their similarity lies in their identical cores, with the remainder x being a super uous part (with respect to the given entailment).
Across the entire corpus, the number of justi cations is reduced from 6,744 to 456 templates (6.8% of the corpus), which is a further reduction compared to strict isomorphism (614 templates). The most frequent templates in terms of number of justi cations and prevalence across all ontologies are the same as for strict isomorphism, with numbers only di ering slightly.
Lemma-Isomorphism As with s-isomorphism, the e ects of l-isomorphism were not as signi cant as the rst reduction through strict isomorphism. The justi cations were further reduced to an average of 7.4 templates per ontology ( = 11:4), with 11 justi cations per template ( = 51:5). Still, 35 of the 83 ontologies show at least a minor di erence between s-isomorphism and lisomorphism, which indicates that they contain at least 1 atomic subsumption chain.
L-isomorphism reduces the 106 justi cations generated for the Cereal Plant Gross Anatomy ontology to only 14 templates, compared to 29 templates for sisomorphism. This shows that, while not very frequent, there are indeed ontologies in which justi cations with subsumption chains of di ering lengths occur.
In the Plant Ontology, l-isomorphism reduces the 74 justi cations to 12 templates, with one template capturing 32 justi cations of varying sizes. These justi cations contain atomic subsumption chains ranging from 2 to 6 atomic subsumption axioms, which can all be reduced to a single axiom (namely the entailment of the subsumption chain) in the lemmatised version of the justi cation.
Across the corpus, l-isomorphism reduces the 6,744 justi cations to a mere 384 templates, which is an overall reduction of 94.3%. The e ect of lemmaisomorphism is visible when we look at the most prevalent justi cation, an atomic subsumption chain of size 2, which occurs in 44 (compared to previously 37) ontologies. This chain represents all 701 atomic subsumption chains of di ering sizes that can be found in the corpus. 5.4
For the purpose of detecting how many distinct types of justi cations there are for a given set of entailments, we have seen that it is crucial to focus not on the material form of a justi cation, but rather on the justi cation templates in an ontology. By only considering the abstract template of a set of justi cations, we can represent the reasoning that underlies not only one, but a whole class of justi cations in the ontology.
Surprisingly, while the newly introduced equivalence relations, s-isomorphism and l-isomorphism, could be shown to capture some of the structural similarities in the surveyed corpus, a large number of justi cations were indeed strictly isomorphic. We can argue, however, that even a small reduction can be bene cial when presenting multiple justi cations to OWL ontology developers for the purpose of explaining entailments, as it prevents repetitive actions and gives a higher-level view of the set of justi cations. This is made obvious in the example of the Plant Ontology, where a large number of justi cations that di ered only in the length of their atomic subsumption chains, could be captured by a single template.
Another aspect to take into account when dealing with OWL justi cations
is the super uousness of expressions, as we have seen in the case of the Lipid
Ontology. Two justi cations may be nearly identical and only di er in
expressions that are not necessary for the entailment to hold; these super uous parts
would prevent them from being isomorphic with respect to any of the above
de nitions, but it is clear that their form is the same. This situation describes
one of several types of justi cation masking [
A laconic justi cation [
Future work will involve exploring further notions of obvious proof steps in order to extend lemma-isomorphism beyond atomic subsumption chains. We will also consider the issue of overlapping chains, i.e. subsumption chains which lead to non-summarising lemmas. Since the present paper demonstrates the e ects of the di erent equivalence relations on only a subset of the justi cations from the BioPortal corpus, we are planning a survey of the entire set of justi cations, taking into account the di erences between laconic and non-laconic justi cations. Finally, we aim to obtain more detailed knowledge about the application of ontology design patterns in the surveyed ontologies, which will allow us to investigate the relations between these design patterns and the form and frequency of justi cation templates.