Self-referential concepts in description logic may formally be viewed as concepts that at some point mention an individual previously encountered in the evaluation; this corresponds to a restricted form of the down-arrow binder known from hybrid logic. Typical examples include being a narcissist, (someone who loves himself); a celebrity (someone who is known by everyone she meets) or a grant application reviewer (who can only review proposals of researchers with whom she did not collaborate in the past). While reasoning in ALC plus self-reference is known to be undecidable, it has recently been shown that one can often safely restrict self-reference to at most two indirections (allowing the definition of narcissists and celebrities, but not of grant reviewers). In particular, the extension of ALCQ with this construct has an expressive power roughly equivalent to ALCHIQ plus safe Boolean combinations of roles. Here, we discuss a translation-based approach to reasoning in this logic. The translation goes into ALCHIQ (without Boolean roles) and therefore can be used in combination with off-the-shelf reasoners for OWL. The translation strategy encodes the semantics of the source axiomatically in the target logic. We use an implementation of this type of translations to evaluate the feasibility of the whole approach.
Modern description logics reasoners accept definitions and queries in very expressive
logical languages such as SROIQ, which contains nominals, complex role inclusions,
disjoint roles, universal roles, etc. among its features [
We suggest a translation-based methodology as a cost-effective alternative for such
scenarios. Satisfiability-preserving translations are a common tool in computational
logic, usually as a means of establishing complexity bounds (but not always, see
e.g. [
More concretely, we employ what we shall call logical interpreters. Extending the
example above, we represent complex L-concepts with atomic L0-concepts and encode
the semantics of L (restricted to a finite set of L-concepts) using a set of L0-axioms, so
that we can say that we are interpreting the semantics of L in L0. This is reminiscent of
works such as [
We showcase this technique by building a logical interpreter in ALCHIQ for the
logic ALCQme2, the extension of ALCQ with Marx’s I-me operators [
In ALCQme2 one can define inverses, role hierarchies and safe Boolean
combination of roles (where full role complementation is replaced by role subtraction R S).
In fact it has been shown that ALCQme2 is expressively equivalent to the extension
of ALCHIQ with safe Boolean combination of roles and the 9R:Self operator of
SROIQ (but ALCQme2 is conjectured exponentially more succinct) [
We formally introduce ALCQme2 in Sec. 2. The general idea of logical interpreters is first explained in Sec. 3 by describing a trivial self-interpreter for ALCHIQ. We then extend this construction to a logical interpreter for ALCQme2 in Sec. 4. Finally we present in Sec. 5 preliminary results on empirical evaluation of the approach. 2
The DL ALCQme2 extends ALCQ with the I-me construct originally proposed in [
An interpretation or model is an structure I = h I ; I i where I is a non-empty set (the domain of I); AI I for each A 2 NC; and, for Ri 2 NR, RiI I I . For a set Ni of individual names and an individual i 2 Ni, we also expect iI 2 I . Now, for every a 2 I , we use CaI to denote the extension of an ALCQme2-concept C under the assumption that me stands for a. This is formally defined as:
AaI = AI (:C)aI =
I
CaI
meaI = fag (C u D)aI = CaI \ DaI (I: nR:C)aI = fb : b 2 ( nR:C)bI g ( nR:C)aI = fb : jRI (b) \ CaI j ng A concept C is said closed if it has no free occurrences of me. It is easy to prove that: Proposition 1. If C is a closed concept, then CaI = CbI for all a; b 2 I .
We thus denote the extension of a closed concept C just by CI . From Proposition 1 it is clear that ALCQme2 is a conservative extension of ALCQ.
An ALCQme2 knowledge-base (KB) T is a pair hT; Ai —a TBox and an ABox— with the provision that every concept occurring in it must be closed. Formally, T is a set of concept equivalence axioms of the form C D and A is a set of assertions of the form Ri(a; b) or a : C with a; b 2 Ni (individual names). We say that I satisfies T , notation I j= T , whenever: i) CI = DI for all C D 2 T; ii) aI 2 CI for all a : C 2 A. iii) (aI ; bI ) 2 RiI for all R(a; b) 2 A. We say that T is consistent if it is satisfied by some model. We may also write axioms of the form C v D in TBoxes, which are short for C t A D, for some fresh atomic concept A.
We assume the reader to be familiar with the DL ALCHIQ (see e.g. [
We now introduce the notion of logical interpreters via a toy example: a self-interpreter for ALCHIQ. This will be later turned into an ALCHIQ-interpreter for ALCQme2.
When discussing logical interpreters, one needs to clearly distinguish the language to be interpreted from the language in which the interpreting axioms are written; we shall refer to the latter as the host language. In the example of this section, ALCHIQ is both the host and the interpreted language. The main idea is then simple to describe: we represent each concept of the interpreted language as an atomic concept of the host language, called the host representation, and describe its semantics by suitable axioms.
To illustrate this, consider a concept 5R:C of the interpreted language. We associate to it an atomic concept H 5R:C and, if the host language includes qualified number restrictions among its features, we can describe its meaning with the TBox axiom H 5R:C 5R:HC , where HC is the host representation of the concept C, which in turn needs to be suitably axiomatized. As this example already suggests, in order to axiomatize the semantics of a concept C, we need to provide axiomatizations for the host representations of the subconcepts of C (this, of course, is a consequence of the fact that Tarski-style semantics are compositional in nature).
Formally, assume then for the rest of the section that the interpreted language is ALCHIQ over a vocabulary hN Ci ; N Rii. For a finite set of concepts of this language, we let hNCh ( ); NRh( )i denote the vocabulary of ALCHIQ as host language, and put: NRh( ) := N Ri
NCh ( ) := fHC j C or C are subconcepts of a D 2 g: For convenience we shall usually identify A 2 N Ci with HA and thus assume that N Ci NCh ( ). We shall also identify H> with > and H? with ?. We denote by S0( ) the set of axioms used to interpret the concepts in NCh ( ); S0( ) contains axioms
H nR:C HC t HD nR:HC
H nR:C
HC u HD nR:HC
H:A :HA whenever the index of the left hand side is in . Notation involving is extended to a KB T by considering the set of all subconcepts of concepts occurring in T .
Let T = hTi; Ai; Rii be a KB to be interpreted. Our logical interpreter maps T to the KB I0(T ) = hTh; Ah; Rhi, where Th := S0(T ) [ fHC HD j C D 2 Tig, Ah := fa : HC j a : C 2 Aig and Rh := Ri.
One can now make the relation between a KB T and its interpretation I0(T ) precise. It suffices to observe how models for one are to be converted into models for the other, and vice versa. In general, we need to define two functions on models: I" taking a model of the interpreted language to one in the host language, and I# in the converse direction. In the case of the self-interpreter under consideration, we have that I# is the restriction of I to the signature N Ci NCh ( ), while I" interprets each HC 2 NCh ( ) N Ci as HC I" := CI . It is then straightforward to show the following: Proposition 2. For all T , I and J , we have that I j= T J # j= T () J j= I0(T ). ()
I" j= I0(T ) and This proposition shows that I0 is satisfiability-preserving in a strong sense; in particular, individuals mentioned in the ABox are preserved both by I" and J #, so that it is safe to map even ABox-queries on T to analogous queries in I0(T 0), where T 0 is a suitable extension of T . For example, for any given a concept C, it is easy to see that the instance retrieval problem for C on T = hT; A; Ri corresponds to the instance retrieval problem for a fresh atomic concept A0 on I0(T 0) where T 0 = hT [ fA0 Cg; A; Ri. Restricting the interpreter to tree-models. The interpreter for ALCQme2 to be defined in Sec. 4 exploits heavily a tree-like model property of ALCQme2. This means that we will want to restrict our attention to models of the host language that are trees (or rather forests). We now show how to enforce this, and discuss some associated pitfalls. Definition 3. We say that a binary relation R X2 is a tree whenever there exists r 2 X, the root of R, such that there is exactly one directed path in (X; R) from r to any x 2 X. We say that R is a forest if it is isomorphic to a disjoint union of trees. We say that I is a tree model whenever U = SR RI is a forest. Observation 4. If R is such that R 1 is a partial function and R 1(r) is undefined, r is the root of a tree obtained by restricting R to the connected component of r in R. The observation serves as a guiding principle in refining I0. For T = hTi; ;; Rii, define I0(T ) := hTht; Aht; Rhti, where for a fresh role symbol f and a fresh individual i;, t Tht := Th [ f> v; 1f:>g, A;htt := fi; : 8f:?g and Rht := Rh [ SR2N Ri fR v f g.
Clearly, any model I for I0(T ) is turned into a tree model T (I) for I0t(T ) by restricting it to only the connected components of elements satisfying 8f:?, like i;I . In the presence of non-empty ABoxes we have to be more careful since it is easy to have one that forces non-tree models. We will consider this when interpreting ALCQme2. 4
An Interpretation of ALCQme2 in ALCHI Q Self-interpretation as was done in Sec. 3 is an extreme case: since the host and interpreted languages coincide, the interpreter is trivial. We are now faced with the problem of interpreting in ALCHIQ a radically different language, namely, ALCQme2. We shall overcome here several challenges.
First and foremost, there is a radical mismatch between the semantics of ALCQme2 and that of ALCHIQ: the extension of concepts in the latter corresponds to subsets of the domain, while in the former they induce a binary relation (i.e., we need two points of evaluation: the current one and that denoted by me). To circumvent this problem, we observe that ALCQme2 possesses a tree-like model property (cf. Theorem 6 below); i.e., for purposes of reasoning we can in general restrict our attention to tree-like models. Now, it turns out that if we intend to decide whether x 2 CyI on a tree-like model I where the distance between x and y is at most 1 (i.e., they either coincide or one is the father of the other), we will only need to consider subproblems of the form z 2 DwI, where the distance between z and w is 1 as well (for closed concepts, in particular, we can assume distance 0). In the end, there is a finite combination of relevant cases that we will be able to encode in the host representation.
Definition 5. A relation S X 2 is a quasi-tree with root r if there is a tree R with root
r and R S R [ R 1 [ IdX . Such R is unique and called the underlying tree of S.
Terms quasi-forest and quasi-tree model are used in analogy to Def. 3. The following is
proved with an unraveling similar to the one in the analogous proof for ALCme2 [
In the self-interpreter of Sec. 3, a concept C of the interpreted language was mapped to the atomic concept HC of the host language. We could think of HC as meaning “satisfies concept C in the interpreted language”. In order to account for the extension of me we will need a richer set of atomic concepts in the host language. We will use atomic concept H :C to describe “those elements that satisfy C in the interpreted language when they are also the value of me”. Similarly, Hf :C shall represent “those elements that satisfy C in the interpreted language when their father is the value of me”. It will be crucial to consider a third family, namely H f:C , which is to be read as “those elements whose father satisfies C under the assumption that they are the value of me”. Although dispensable, we find it conceptually clearer to include an additional family, H :C , where C is a closed concept, for “those elements that satisfy C regardless the value of me”. We refer to L := f ; ; f ; f g as the set of possible contexts.
For the case where C has u or t as top-level operator, we can mimic the corresponding axioms from Sec. 3. For atomic negation we observe some differences in contexts involving the father: by definition, elements satisfying Hf ::A or H f::A must have a father, so the corresponding axioms need to be H f::A 9f:H ::A and Hf ::A H ::A u9f:>. In fact, we will generalize these axioms to any closed concept (not just negated atoms) and also have H :C H :C when C is closed.
The last missing ingredient of the interpreter is the handling of concepts of the form (I:) nR:C and (I:) nR:C, that is, those whose top-level operator is a qualified number restriction or an I binder in front of one. This requires some effort since we need to take into account the “virtual” part of roles (i.e., the "R and R) in the counting. The general idea in handling this is to interpret H`: nR:C by way of a case-analysis: depending on which of R and "R hold, and whether C holds at the current state and/or at the father, we pick a suitable discount 0 d 2 and then test if n dR:C holds. For example, a discount value of 1 indicates that either the current node or its father (but not both) is one of the n successors required, so it suffices to find n 1 more. The axioms for contexts other than f are given in terms of the following helper construct: Rn is defined using instead of . Observe that whenever m > n, then n mR:C3 (resp. n mR:C3) shall represent > (resp. ?). The intuition is that Rn (C1; C2; C3) is discounting 2 when both R and "R hold and C1, a suitable modification of C, holds “at the father” while C2, another suitable modification of C, holds at the current node; it discounts 1 when only one of these conditions hold; and nothing otherwise.
Now, why do we need concepts C1, C2 and C3 in (2) instead of just one concept C? There are two reasons for this: i) adjusting the context and ii) dealing with free occurrences of me in C. This will become clear with an example. Assume we need to interpret H :I: nR:C . In order to see if the father node (if any) needs to be discounted from the n successors, we need to know whether C holds at the father under the assumption that the current node stands for me. So, in principle, we would like to use H f:C for C1. But we know more: if we are evaluating this formula on a tree, then the current node and its father will be distinct nodes, so evaluating C at the father will be equivalent to evaluating C0 at the father, where C0 is obtained from replacing every toplevel occurrence of me in C by ?. Observe that the fact that no me appearing under the scope of a qualified number restriction is replaced by ? is critical for the correctness of the argument. The following piece of notation will be handy: Definition 7. For concepts C and D, C(D) is the concept obtained by replacing every free occurrence of me outside the scope of a qualified number restriction in C by D. Now we can formalize the axioms for H :(I:) nR:C , H : nR:C and Hf : nR:C : H :(I:) nR:C
H : nR:C Hf : nR:C
Rn (H f:C(?); H :C(>); Hf :C(?)) Rn (9f:H :C(?); H :C(>); H :C(?))
Rn (9f:H :C(>); H :C(?); H :C(?)) u 9f:> Three things are worth observing. First, notice the relation between the context of the interpreted concept and the assignments of > and ?. Second, (3) is the first axiom we discussed so far that contains a concept with context other than that does not occur at the left of the . In fact, this and the dual axiom for (I:) nR:C concepts will be the only such axioms. From this observation and because in ALCQme2 there are at most two qualified number restrictions between I and me, it is clear that C in (4) and (5) can be assumed to have all occurrences of me at the top-level, so that C(?) and C(>) are closed concepts. Finally, notice that unlike the self-interpreter of Sec. 3, the set of relevant concepts needs to be closed by replacements of top-level me by > and ? (recall, also, from Sec. 2, that nR:C as not a subconcept of I: nR:C).
The only kind of axiom we are missing is that for H f: nR:C . Because nR:C is expected to hold at the father of the current node, we will need to use 9f: n+c (: : :), which will take care of the father’s virtual relations, if any, picking also a correction factor 1 c 1 that will compensate for “interferences” of the current node in the counting. Formally, the required axiom is H f: nR:C #Rn (C) u 9f:>, where: 0 (9R :> u #Rn (C) := l B@ (:9R :> t (9R :> u (:H :C(>) u (H :C(>) u :H :C(?))) ! 9f: "R (H :C(>) $
H :C(?))) ! 9f: "R H :C(?))) ! 9f: "R n 1 (C) 1 n+0 (C) C
A n+1 (C) (3) (4) (5) (6) Here "Rn (C) stands for Rn (9f:H :C(?); H :C(?); H :C(?)). Firstly, it is helpful to compare the latter with the -expressions of (4) and (5) and observe that me is not being replaced by > anywhere. In particular, if the current state satisfies H :C(?) it may get counted when it should not be. More precisely, in order to have a non-zero correction factor, we need the current state to be an R-successor of its father. If it additionally satisfies H :C(>) then we need to discount it from the expected R-successors of the father satisfying C (c = 1), except when H :C(?) holds as well, since then it will be incorrectly be counted as one of the R-successors of its father that satisfies C under the assumption that me is not current node (c = 0). The case where c = 1 is analogous.
To formalize the whole procedure, we assume the vocabulary of ALCQme2 to be hN Ci ; N Rii and fix a set of concepts . Let 0 be the smallest set closed by
H ::A H :C0 Hf :C0 H f:C0
H`:C t H`:D :H :A H :C0 H :C0 u 9f:> 9f:H :C0 H :(I:)QnR:C
H :QnR:C Hf :QnR:C H f:QnR:C
RQn (H f:C(?); H :C(>); Hf :C(?)) RQn (9f:H :C(?); H :C(>); H :C(?)) RQn (9f:H :C(>); H :C(?); H :C(?)) u 9f:> #RQn (C) u 9f:> subconcepts and such that if C 2 0 then C(?); C(>) 2 0 as well. We then have: NCh ( ) := fH`:C j ` 2 f ; f; f g; C 2 0g [ fH :C j C 2 rs; C is closedg : We identify H :> with >, H :? with ? and H :A with A, for A 2 N Ci . We then define the atomic roles of the host language with NRh( ) := N Ri [ ff g [ f R; "Rj R 2 N Rig. The set S1( ) of axioms needed to interpret relevant concepts in is listed in Table 1. Again, we extend the notation from sets of concepts to knowledge-bases as expected.
For simplicity, we shall first discuss the interpretation of ALCQme2-KBs with i empty ABoxes. So let T = hT ; ;i be such a knowledge-base. A logical interpreter for T is the ALCHIQ-KB I1(T ) = hTh; A;h; Rhi where Rh := SR2NRi f"Rv 9f:>g, A;h :W=efnio;w: l8ofo:k?agt hanodwTqhua:s=i-tSre1e(Tm)od[efls>fovrAL1CfQ:>mge[2 afr"eRtvurn9efd: >intjoRtre2e mNoRidge.ls of the host logic and vice versa. We first take a quasi-tree model I and observe that since every rooted quasi-tree induces a unique tree, I induces some tree model I0 (which only depends on the elements picked as roots). Then I0 is extended to a model I" in the signature of the host language by interpreting R and "R in the obvious way (e.g.,
RI0 := fx j (x; x) 2 RI g); making f I0 the union of the converse of every role in I0, and interpreting all the other concepts in the expected way, for instance, one defines (Hf :C )I" = fx j 9y : (x; y) 2 f I0 and x 2 CyI )g. Also, i0 denotes some root of I". On the other direction, for a model J of the host language we let J 0 be the restriction of the domain of J to all elements the connected components that include an “f -root”, i.e., an element that has no f -predecessor (or J 0 = J when no such element exist). We then define J # as the restriction of J 0 to the vocabulary of the interpreted language, plus RJ # := RJ 0 [ f(x; x) j x 2 JR0 g [ f(x; y) j 9y : (y; x) 2 f J 0 and x 2 "RJ 0 g. Proposition 8. Fix an ALCQme2-KB T . If I is a quasi-tree model, then I j= T I" j= I1(T ). If J j= I1(T ), then J # is a quasi-tree model and J # j= T . () Example 9. Let T = hf> I: 2R:meg; ;i and let T 0 = I1(T ). We want to verify that T 0 is unsatisfiable (we use j= for the global entailment relation). Clearly, we have that T 0 j= H :I: 2:me, and because of (3), we get T 0 j= R2 (H f:?; H :>; Hf :?) as well. Now, we know T 0 j= (H f:? $ 9f:H :?) u (H :> $ H :>) and H :? and H :> were identified with ? and >, respectively. Hence, T 0 j= R2 (?; >; Hf :?). Simplifying in (2), we conclude that T 0 j= ( R! 1R:Hf :?) u (: R! 2R:Hf :?). However, T 0 j= Hf :? $ ? u 9f:>, so in particular T 0 j= Hf :? ! ?. Therefore, we have T 0 j= ( R! 1R:?) u (: R! 2R:?), so T 0 must be unsatisfiable. We shall end this section by briefly discussing the handling of ABoxes. The first thing to observe is that for ABox reasoning there is no tree-like model property one can use: that is, it is trivial to build a consistent ALC ABox without tree models. That models in the host language are trees is a crucial part of the interpreter (it is what allows us to safely replace me by ? in the axiom for H f: nR:C ), so we cannot let go this property. The upshot is: we can only handle ABoxes whose graph can be embedded in a quasi-forest.
We assume that the so called Unique Name Assumption (UNA) does not hold, that is, different individual names may denote the same individual (this corresponds with the OWL standard and, moreover, the case where the UNA holds is somewhat simpler). The following tells us how to eliminate all role assertions from such an ABox: Proposition 10. Let T = hT; Ai be an ALCQme2-KB and let I be the set of individual names in A. If the graph of A can be embedded in a quasi-tree, then for each i 2 I there is a Ci such that T is consistent iff T = hT; Si2I fCigi is consistent.
Proof (sketch). Because individual names cannot occur in concepts we are free in principle to replace an assertion R(i; j) 2 A by an assertion R(i; j0), where j0 is a fresh individual that realizes the same formulas as j. Moreover, ALCQme2 is expressive enough to describe such an individual without needing a fresh individual name. We only need a fresh atomic concept in combination with two fresh role symbols U and U .
Formally, fix i 2 I and let Ai be the ABox obtained by renaming every j 2 I fig by ji. Moreover, let Aji denote a fresh concept for each such j. We assume i to be the root of Ai from which the underlying tree structure is uniquely determined. Ci is then the conjunction of i) all concepts C such that i : C 2 A; ii) I:R:me for each R(i; i) 2 A; and iii) for each ji that is an immediate successor of i in Ai we add 1U:Aji plus: I:9U:(Aji uCji u9S1:meu: : : 9Sn:meu9U :meu8U :meuI:8U :(9R1:meu: : : 9Rm:me)) where R1(i; ji) : : : Rm(i; ji) and S1(ji; i) : : : Sm(ji; i) are all such role assertions in Ai. For Cji we iterate conditions i-iii; the tree guarantees the recursion to terminate.
The proof of the left-to-right implication is then straightforward; for the converse direction one needs to reassign the interpreted individuals to make sure that those that were in the same connected component in A are in the same connected component of the model, the fact that A was a quasi-tree guarantees that this can be done. 5
Feasibility of Logical Interpreters: Preliminary Results The interpreters we have considered are, of course, more complex than the knowledgebases they interpret; yet, it is not hard to see that the blow-up (measured in number of axioms and assertions, and size of all complex concepts mentioned) is only linear – or O(n log n) if one considers the representation cost of fresh symbols. Although the translation is in principle small, it is not clear a priori how it is to interact in practice with off-the-shelve DL reasoners. On the other hand, these interpreters are not hard to implement, so it is worth experimenting. We report here some preliminary results.
We implemented a translation from ALCQme2 to ALCHIQ1 following the interpreter approach of Sect. 4. The translator takes OWL files (where we expect certain role-name and certain atomic concept to stand for I and me respectively) and outputs OWL files. This means that we can use them in combination with standard tools. We included only very basic optimizations in order to reduce the size of the interpreter, the most important one is simplifying complex concepts using Boolean identities such as ? t C 7! C. This is important since these type of concepts are generated often when replacing top-level occurrences of me by > and ?.
[secs] 10 8 6 4 2 .11638 .54513 .835 .7931 .2281 .2783 t eou m i
T Isexxo062dunndB Isexxo69undndB I,,frtseexxyx310oo2ndnudBOmM i,Itseexxx94o1odnudnuBTm i,Itseexxx4o9ondunduBTm i,Itseexxx2o352odnudnuBTm i,rtteexx50o1uhTOm i,rtteexx50o1uhTOm rtex2hO rtex2hO rtex527hO rtex257hO u O x 2 2 3
Since there are of course no real examples of ALCQme2 ontologies, we have to
rely on artificial examples. We downloaded from the TONES ONTOLOGY
REPOSITORY2 ontologies that corresponded to fragments of ALCHIQ and turned them into
ALCQme2 ontologies by interpreting some atomic concept A as me and, nR as I,
for some atomic role R. Care was put to delete role inclusion axioms mentioning R
and ignoring occurrences of A that were free or not under at most two qualified number
restrictions from the binding point. We actually did this conversion for up to 400
hundred combinations per ontology, which in most of the cases was exhaustive. Each of the
resulting ontologies was translated to ALCHIQ using our tool and checked for
consistency with PELLET [
We measured the time to required for each ontology (usertime) and, for those derived from the same TONES ontology, took the average time and the standard deviation (only for those that ended before the timeout of 600 seconds). The results are summarized in Fig. 1 (the raw data can be found on Table 4, in the Appendix).
We are including in Fig. 1 also ontologies which consistently failed either by outof-memory errors, triggered what seems like an internal bug in PELLET (“ArrayIndexOutOfBoundsError”) or simply could not be parsed by the reasoners, even though they were generated using the OWLAPI (indicated by “Other”).
One can clearly see that most of the cases that could be handled end within a minute, regardless of the reasoner (although HERMIT seems to be able to handle more cases). In principle, the results are positive, although one needs to be cautious here: because of the artificial nature of the examples, it is possible that they are being solved simply because they are trivial (e.g., if there are no interactions between the chosen I and me).
Instead of performing a case-by-case analysis, we decided to conduct a quick experiment that could give us an idea of the cost of interpretation. We extended our tool to turn it into a very simple self-interpreter generator, trivially extending the one of Sect. 3 to S HIQ. We downloaded from TONES all the ontologies for fragments of S HIQ, which made for a total of 45 ontologies of diverse complexity. We had to discard 17 of them because our OWL API-based tool failed to parse them. Of the remaining 62%, we rejected three more ontologies since they required (undeclared) features beyond S HIQ. For the 25 surviving ontologies, we ran a consistency check, both on the original and the translated ontologies and measured the runtime (same setup as before).
These results are summarized in Fig. 2 (the raw data can be found in Table 3 in the Appendix). We plotted, for each ontology, the quotient between the runtime for the translated and for the original version. Even though the sample is small, it is still noticeable that PELLET exhibits a relatively consistent behavior, staying in general within a factor of 2, which is more than acceptable. HERMIT on the other hand shows a more erratic behavior (sample 16 is actually way off the scale). At the moment we were unable to find any noticeable correlation between file size, number of axioms in the original ontology or language, and the performance of the reasoner on the interpreter. 6
We have described a translation-based approach to reasoning in the context of Description Logics, based on the idea of axiomatizing the semantics of the original logic – what we have called a logical interpreter. We illustrated the idea with a trivial example, a self-interpreter, and then constructed a non-trivial one for the case of ALCQme2: a language with a binder construct, capable to express features such as role-intersections. We also report preliminary results on the behavior of off-the-shelf DL reasoners on both on an interpreter for ALCQme2 and several self-interpreters. The results are suggestive that the logical-interpreter approach may be effective in some real scenarios. Building a logical interpreter is relatively cheap, so it appears as a cost-effective alternative.
Pellet
HermiT frteyoooumm itteoum frteyoooumm itteoum frteyoooumm frteyoooumm teou teou itm itm 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
From all ontologies which were considered because of their claimed expressitivity, the ontologies listed in Table 2 had to be discarded. The remaining ontologies are listed by Table 3 – together with the exact data measured.
Ontology action atom-complex-proton-2.0 biochemistry-complex chemistry-complex expression heart legal-action legal-role lkif-rules mereology molecule-complex norm process relative-places role time yowl-complex
DL ALCHIN ALE Q ALC ALCHQ ALCHI SHI ALC ALC ALCH SHIN ALCH SHI ALCHI SHIF ALCI SHI ALCH
Syntax Syntax Syntax Syntax Syntax Syntax Syntax Syntax Syntax Syntax Syntax Syntax Syntax Syntax Syntax Syntax tambis-full tambis-patched biochemical-reaction-complex
LEC loogy .
L .ow .o e l - g x a p n . o ic
n ob -co l .
m o it w o t w p l o u o o w k l 3 b 0 y 0 t , M f M e a s o n e r , T 9 . 9 4 1 8 A S A
A S A A A A A A A A A A A A A A A A A A A D L H L
L H L L L L L L L L L L L L L L L L L L L L C I C Q F H
C F C C C C C C U C C C H C E C C C C I C
I H F N Q F N N Q F H F H I
I I
Q F
Q 1 1 4 1 1 2 4 1 2 3 1 3 3 7 3 4 4 2 3 4 1 4 9 4 1 6 0 4 1 1 3 6 4 8 9 0 3 2 6 5 8 0 1 9 3 9 3 4 6 5 2 5 4 7 9 1 1 6 6 3 5 1 4 7 9 0 6 1 8 2 3 2 6 8 7 5 4
7 6 3 3 8 1 7 3 3 8 9 8 5 0 1 9 2 1 0 4 1 5 5 0 3 9 3 3 9 0 2 8 9 2 7 9 3 8 9 7 4 9 3 0 6 8 4 6 6 3 b F e il fo e re isz e 2 1 3 3 2 1 M 1 1 1 1 1 2 2 1 2 1 3 2 1 1 1 1 1 3 8 2 4 9 5 0 4 1 6 1 7 3 9 2 2 7 9 5 5 7 3 4 3 9 3 1 5 7 3 4 4 8 6 1 6 1 6 4 0 3 0 o 4 5 4 7 6 8 5 1 3 5 7 3 5 7 2 2 3 3 3 8 1 8 7 1 2 a u f n 7 9 1 T 4 T T T 1 T 1 1 T 2 1 2 2 2 2 1 3 5 1 1 1 1 0 1 . 7 4 e x fro io e m b H e E f o R r e M
I b P fe E o L r L e E
T u a s f e t r e r ti m e O / y
M r /e o r m r i E T : r i
o e a t a i a v
a LL re e E v m P A ti rs /M
e o r m r i E T : d n e r i o t a
1 3 .8 .9 .1 .9 2 5 5 3 – – – – – – – – – 1 4 9 1 7 7 8 0 2 a s 7 0 3 4 1 2 4 1 3 P te 70 19 76 39 11 1 3 5 1 5 0 0 0 1 5 2 1 1
8 P te 70 19 15 34 0 0 0 0 0 0 0 0 0 1 5 2 1 1 1 2 5 1
e m k m
o to to r
z m iz d
P ao n l n ie lo
v t o l p - k e icm ecn ed o
o m C
a m t
t a b u u ann sn a s b b 3 0 32 /9 /
n Ae
v ll i a g
e a d s e d
r
r w e a h R w : s m x o e c - d l n a u n
m g o 2 e 6 2 e0 .51 .0 .3 .9 . 8