DeFind: A Protege Plugin for Computing Concept Definitions in EL Ontologies

We introduce an extension to the Protege ontology editor, which allows for discovering concept definitions, which are not explicitly present in axioms, but are logically implied by an ontology. The plugin supports ontologies formulated in the Description Logic EL, which underpins the OWL 2 EL profile of the Web Ontology Language and despite its limited expressiveness captures most of the biomedical ontologies published on the Web. The developed tool allows to verify whether a concept can be defined using a vocabulary of interest specified by a user. In particular, it allows to decide whether some vocabulary items can be omitted in a formulation of a complex concept. The corresponding definitions are presented to the user and are provided with explanations generated by an ontology reasoner.


Introduction
The development and application of large terminological systems pose new challenges for ontology engineering and automated reasoning tools. A question which becomes evidently important in the context of large ontologies is whether their content and logical consequences are easy to comprehend. To address this problem, a number of visualization and explanation tools has been integrated into ontology editing environments such as, e.g., visualization and explanation services implemented for the Protégé ontology editor. It is common that an expert exploring an ontology encounters concepts, which are formulated in a vocabulary she is not familiar with. More generally, only a certain part of an ontology vocabulary may be familiar to an expert, while the remaining part may be not. When a formulation of some concept employs vocabulary items unknown to an expert, typically she would like to know whether this concept can be reformulated in the familiar vocabulary. To give a simplified example, suppose an ontology of cuisines contains axiom Dumplings Entree Gnocci (stating that Dumplings being Entree are Gnocci) together with concept inclusions Gnocci Dumplings and Dumplings Entree. Assume an expert is familiar with concepts Entree and Gnocci and she encounters the concept Dumplings Entree mentioned in the ontology. First, one may notice that this concept can be simplified, i.e., it is equivalent to Dumplings wrt the ontology, due to the inclusions above. Second, the ontology entails that Dumplings and Gnocci are equivalent, thus, the original concept can be reformulated as Gnocci (or as Gnocci Entree) in the vocabulary known to the user.
In this paper, we introduce DeFind, an extension to the Protégé ontology editor, which allows to find concept definitions in a user specified vocabulary consisting of concept and relations names from an input ontology. In particular, it allows to verify whether some concept or relation names can be omitted in a formulation of a (complex) concept. To the best of our knowledge, this is the first implementation of these reasoning services as a part of an ontology editing tool. Specifically, for a given ontology Ø, vocabulary Σ, and a concept C of interest, DeFind computes definitions of C wrt Ø in Σ, i.e. concepts {D 1 , . . . , D n } (whenever they exist) such that D i contains symbols only from Σ and Ø |= C ≡ D i , for all i = 1, . . . , n. DeFind supports ontologies formulated in the Description Logic EL, which allows for building concepts using conjunction and existential restriction, and includes built-in concepts such as ⊥ and . For example, it is possible to state in EL that some concepts are disjoint (e.g., Entree Dessert ⊥), specify subsumption relationship between concepts (Dumplings Entree Gnocci) or domains of relations (∃hasIngredient. F ood), and use existential restriction to specify relationships of other kinds (e.g., Salad ∃hasDressing. , ∃hasIngredient.M eat N onV egeterianF ood). The expressive features of EL although limited (e.g., negation/disjunction of concepts is not allowed), are sufficient to capture a great variety of ontologies. Most of the biomedical ontologies published on the Web fall within the formalism of EL, which underpins the OWL 2 EL profile of the Web Ontology Language.

Techniques
In the Description Logic EL, concepts are built using a countably infinite alphabet of roles names N r and concept names N c , with two distinguished concepts ⊥, ∈ N c . The notion of concept is defined inductively: any element of N c is a concept and if C, D are concepts and r ∈ N r is a role then C D and ∃r.C are concepts. A concept inclusion is an expression of the form C D, where C, D are concepts. A concept equivalence is a expression C ≡ D. An ontology is a finite set of concept inclusions and equivalences (called axioms). A signature is a subset of N r ∪ N c \ {⊥, }. The signature of a concept C, denoted as sig (C), is the set of role and concept names (excluding ⊥ and ), which occur in C. The signature of a concept inclusion or ontology is defined similarly. Semantics is defined by using the notion of interpretation, which is a pair I = ∆, · I , where ∆ is a universe and · I is a function which maps every concept name from N c to a subset of ∆ such that (⊥) I = ∅, ( ) I = ∆, and every role name to a subset of ∆ × ∆. This function is extended to arbitrary concepts by setting (C D) I = C I ∩D I and (∃r.C) I = {x ∈ ∆ | ∃y x, y ∈ r I and y ∈ C I }. Let Σ be a signature. We say that a concept C is Σ-definable wrt an ontology Ø if Ø |= C ≡ D, where sig (D) ⊆ Σ. The concept D is called Σ-definition of C (wrt ontology Ø). For example, the concept Dumplings Entree is Σ-definable wrt the ontology from the introduction, where Σ = {Gnocci}. It is known that in EL a concept C is Σ-definable wrt an ontology Ø iff it holds Ø ∪ Ø * |= C C * , where Ø * and C * are "copies" of Ø and C, respectively, obtained by an injective renaming of all non-Σ-symbols into "fresh" ones, not occurring in Ø and C. Indeed, if Ø |= C ≡ D, for some concept D, with sig (D) ⊆ Σ, then it holds Ø |= C D and Ø * |= D C * , which means Ø ∪ Ø * |= C C * . The converse can be proved constructively by computing the corresponding concept D from a proof of the inclusion C C * from Ø ∪ Ø * ; we provide a justification below. Various proof systems have been proposed for the Description Logic EL in the literature. For example, it follows from the results in [1] that the following set of inference rules is sound and complete for entailment of concept inclusions C D from an ontology Ø, where C and D occur in the axioms of Ø:

. Basic inference rules for reasoning in EL
An inference is a triple rule name, premises, conclusion of the form R, {ϕ 1 , .., ϕ n }, ψ , where n 0 and ψ is obtained by an inference rule R with premises ϕ 1 , , . . . , ϕ n . A proof of a concept inclusion ψ (from an ontology Ø) is a set of inferences {ι 1 , . . . , ι n }, where n 1, such that ψ is the conclusion of ι n and for all k = 1, . . . , n and any axiom ϕ, if ϕ is a premise of ι k , then there is a unique j < k such that ϕ is the conclusion of ι j and if ϕ is the conclusion of ι k and k = n then there is l > k such that ϕ is a premise of ι l . Observe that due to the injective renaming of non Σ-symbols it holds sig (Ø) ∩ sig (Ø * ) ⊆ Σ and whenever a concept C occurs in ontology Ø, we have sig (C) ⊆ sig (Ø) and hence, sig Proof. We note the following property (referred to as ), which immediately follows from the definition of the inference rules: if there is a proof of a concept inclusion C E from an ontology Ø then either it is obtained by one of the rules R , R ⊥ , R ⊥ ∃ , or E occurs in C or Ø. We use induction on the number of inferences in a proof ι i , . . . , ι n of a concept inclusion ϕ = C 1 which is an interpolant for ϕ. If i = 1 then sig (E 1 ) ⊆ sig (Ø 2 ) yields sig (E 1 ) ⊆ Σ and hence, E 1 is an interpolant for ϕ. Finally, if the rule is R ∃ then it follows from ( ) that sig (∃r.E) ⊆ sig (Ø i ), for some i = 1, 2. If i = 2 then there is an interpolant for C ∃r.E, which is an interpolant for ϕ. If i = 1 then it follows from the condition sig (∃r.F ) ⊆ sig (Ø 2 ) that r ∈ Σ and by the induction assumption there is an interpolant D for E F . Then ∃r.D is an interpolant for ϕ.
The proof of the theorem gives an idea of a recursive algorithm for computing interpolants and hence, concept definitions, by traversing proofs of C C * from the union Ø Ø * . In general, there can exist several proofs and each of them can yield a different definition of the concept C. Although the idea is simple, its implementation is not straightforward. First, it requires an ontology reasoner, which is not only able to decide entailment of concept inclusions from an ontology, but supports proof tracing, i.e., provides proofs as certificates for entailment. Second, the method presented by Theorem 1 has to rely on a proof system implemented by a reasoner. DeFind employs ELK [1], which is a highly optimized reasoner for the Description Logic EL and its extensions. The add-ons to ELK, which provide proof tracing and explanation services, employ the set of inference rules given in Figure 2. Showing a direct analogue of Theorem 1 for this proof system is not straightforward, since (in contrast to the rules from Figure  1) there exist proofs, from which an interpolant can not be directly computed. However, it can be shown that there always exists (at least a single) proof, which is appropriate for computing interpolants and hence, concept definitions.
DeFind implements a recursive procedure, which traverses proofs obtained by using the tracing service for ELK reasoner. Proofs are built for the entailment Ø ∪ Ø * |= C C * , where Ø * and C * are "copies" (of a given ontology Ø and concept C) constructed wrt a specified signature Σ. The procedure applies recursively the rules below to compute a label expression L(ϕ) for every concept inclusion ϕ appearing as the conclusion of an inference and outputs a label computed for C C * . Whenever there are several proofs for the same ϕ, each of them is traversed. A label is a concept formulated in an extension of EL with disjunction (denoted as EL ) and a distinguished "empty" concept , for which the following holds: D = , D = D, ∃r. = , and ∃r.(D E) = ∃r.D ∃r.E, for any concepts D, E and role r. By using the latter equation, the notion of Disjunctive Normal Form of a EL -concept is naturally defined. We say that a label expression is empty if it equals . Initially the label of every conclusion appearing in a proof is assumed to be empty. Each rule below is provided with a name and gives a label to the conclusion ϕ of an inference being visited during proof traversal, depending on the type of the inference rule and the labels of its premises. We use the notations from Figure 2 for the premises of each inference rule mentioned below: Theorem 2. Let Σ be a signature, Ø ontology, and C a concept occurring in Ø. The concept C is Σ-definable wrt Ø iff the procedure returns a non-empty EL -expression L(C C * ). Every conjunct from the Disjunctive Normal Form of L(C C * ) is a EL-concept and it is a Σ-definition of C wrt Ø.

Complexity of Definitions
We now estimate the size and the number of definitions computed by DeFind. The above mentioned procedure recursively computes labels for conclusions of inferences appearing in proofs. Under the assumption that every proof is computed in polynomial time in the size of an input ontology Ø (which is true when using the ELK reasoner), the size of every proof is polynomially bounded by the size of Ø. For any conclusion, the label is computed once, when traversing a single proof. The rules (L ⊥ ), (L Σ ) give a label concept from a conclusion of some inference and hence, its size is bounded by the size of Ø. Every other rule of the procedure gives a label, which is obtained as a combination (under , , or ∃r., with r ∈ sig (Ø)) of k expressions computed at the previous steps of the recursion, where k 1 is the number of premises of an inference rule and hence, k is bounded by the size of the proof. In particular, the rules L , L + give a label, which is at most k times longer than the labels of the premises of S , S + . Therefore, the size of any label computed from a single proof is at most exponential in the size of the ontology. Since every proof is polynomially bounded, there are at most exponentially many proofs for any conclusion and hence, the output of the procedure has at most exponential size. By Theorem 2, every conjunct from the DNF of the output label is a definition and therefore, the upper bound on the number of definitions computed by DeFind is double exponential in the size of the ontology. To estimate the size of the computed definitions one can w.l.o.g. assume that every rule of the procedure gives a label in DNF and show the following by induction. Every conjunct from a label obtained by some rule of the procedure is either a concept from a conclusion of an inference from a proof, or a combination (under , , or ∃r.) of conjuncts from the labels computed at the previous steps. Therefore, the size of every definition is at most exponential in the size of the input ontology. We now show that these bound are tight by giving an example of an ontology Ø, concept C, and a signature Σ such that there is a double exponential number of shortest Σ-definitions of C wrt Ø, where every definition has size exponential in the size of Ø. Let Σ = {r, s, D 1 , D 2 }, C = A 0 , and for n 1, let Ø consist of axioms: Converting this expression into DNF gives four Σ-definitions of A n−1 wrt Ø, i.e., concepts ∃r.D i ∃s.D j , where i, j = 1, 2. Similarly, A 0 is equivalent wrt Ø to a EL -concept, which has 2 n occurrences of D 1 D 2 . Converting this concept into DNF gives a double exponential number of Σ-definitions of A 0 wrt Ø and it can be shown that no shorter Σ-definitions exist.

Features of DeFind
DeFind (available at https://github.com/stiv-yakovenko/defind) requires the ELK reasoner [1] and proof explanation plugin [2] for Protégé. The interface of DeFind is given in Figure 4. The screenshot shows Σ-definitions of concept ∃r.A 1 ∃s.A 1 computed by Defind wrt ontology Ø and signature Σ from the previous section for n = 1. The user can input a complex concept in the Manchester OWL Syntax into the field "Class expression" or drag-and-drop a concept name from the class hierarchy of the ontology. To specify concept and role names for the target signature, one can drag-and-drop items from the class or object property hierarchy. One can simultaneously add all role names from the ontology into the target signature by pressing "Add all Object Properties" button. Selecting "doesn't include symbols" option sets the target signature to consist of all those concept an role names from the ontology, which are not listed in the "Target signature" field. On pressing "Compute definitions", the corresponding Σ-definitions are computed (or a notification is shown if no definition exists). On pressing the question mark at the right-hand side of a definition, an explanation is shown, why it corresponds to the specified class expression: the Protégé proof explanation plugin is called to visualize a proof (see, e.g., Figure 5 in [2]) of the equivalence of the class expression to the concept computed by DeFind.

Related Work
In [3], a similar approach is implemented to compute concept definitions from tableaux proofs in the Description Logic ALC and its extensions. The authors provide a constructive proof of an analogue of Theorem 1 and derive an algorithm, which computes a definition of at most double exponential size, whenever there exists one in a target signature. This bound is tight and is one exponential larger than the size of the shortest definitions in EL. It is known that general tableaux methods, when applied to EL, provide exponentially longer proofs than the ones obtained in the proof systems from this paper. It should be noted that the algorithm from [3] computes a single definition from a proof, whereas DeFind computes several definitions, the number of which is bounded by a double exponential in the size of the ontology. DeFind explores all proofs provided by a reasoner and traversing a single proof can potentially give several definitions for a concept of interest. In [4], the authors propose an algorithm, which finds a single concept definition in a signature of interest wrt a normalised EL-ontology. The algorithm computes an algebraic representation of an ontology as a canonical model provided with an information on how each element of the model is obtained. Essentially, it implements the two features, which are required for computing concept definitions, i.e., ontology reasoning and proof tracing. In contrast, DeFind relies on external reasoning and proof tracing services. The question whether it suffices to compute a single concept definition strongly depends on application. For instance, the method from [3] is employed in [5] to compute query reformulations. In [6], checking for existence of a concept definition (or computing a single one) is used for ontology decomposition. In both applications, the quality of the obtained result is strongly related to the form of a computed definition. On the other hand, it is argued in [7] that having multiple definitions is helpful in the context of ontology alignment, since having a choice of several (semantically equivalent, but syntactically different) definitions facilitates finding matches between concepts from different ontologies. The authors propose a heuristic approach for computing concept definitions based on examination of concept definition patterns, which typically occur in ontologies. This solution does not employ ontology reasoning and is in general faster, but it can miss some definitions computed by the methods that employ proof tracing.
The exponential lower bound for the size and number of shortest concept definitions is shown in this paper by an artificial ontology example. However it demonstrates the natural phenomenon: some concepts can be used as auxiliary ones in ontology to make definitions shorter. If one asks whether there is a definition, which does not contain certain concept or role names, then one may get a positive answer, but the obtained definition may be long and not easy to comprehend. It is to be understood whether a significant increase of definition size can happen in real-world ontologies. Further, it may be important to develop techniques that help to automatically suggest extensions of the target signature, when a blow-up is unavoidable. One of the primary goals of further implementation is to support other language features of OWL 2 EL profile of the Web Ontology Language, e.g., inclusion and composition of roles. These features are particularly interesting, because on one hand they are frequently used in ontologies and on the other hand, Theorem 1 is no longer true for EL extended with these features. Finally, there is a room for optimizations for DeFind. If the plugin is used extensively to compute definitions of the same concept wrt different signatures then it makes sense to implement optimizations proposed in [4], which employ incremental reasoning to reduce computation overhead, when only a small part of the input is changed.