In this paper, we present a reasoner capable of epistemic inferences in SROIQ knowledge bases. We rst identify some counter intuitive e ects of imposing the traditional semantics in epistemic extensions of expressive description logics (DLs). Thus, we provide a revised downward compatible semantics with a more intuitive behavior in such cases. Based on the new semantics, we present a reduction method for epistemic queries to standard DL reasoning. This enables us to deploy state-of-the-art DL reasoners for such non-standard inferences. Additionally, we provide an implementation of our approach and present rst evaluation results.
In the early 1980s, Hector J. Levesque questioned the adequateness of
the query language in knowledge formalisms [
To see the usefulness of the K operator for epistemic querying, consider the following example. Assume we want to query for \known white wines that are not known to be produced in a French region" which can be solved by performing instance retrieval w.r.t. the epistemic DL concept KWhiteWine u :9KlocatedIn:fFrenchRegiong: This query will not only retrieve the wines that are explicitly excluded from being French wines but also those for which there is just no evidence that they are French (neither directly nor indirectly via deduction). For a knowledge base containing fWhiteWine(MountadamRiesling); locatedIn(MountadamRiesling; AustralianRegion)g as a subset, the query would yield MountadamRiesling as a result, whereas the same query without epistemic operators would produce an empty result. Moreover, by adding additional information such as MountadamRiesling being located in a French region, the answer to the epistemic query would also become empty, which illustrates that introducing the epistemic operator into a logic brings about non-monotonicity.
Another typical use case for epistemic querying is integrity constraint checking: testing whether the axiom
KWine v 9KhasSugar :fDryg t 9KhasSugar :fO Dryg t 9KhasSugar :fSweetg is entailed allows to check whether for every named individual in the knowledge base that is known to be a wine it is also known (i.e. it can be logically derived from the ontology) what degree of sugar it has. Note that this cannot be taken for granted even if Wine v 9hasSugar.fDryg t 9hasSugar.fO Dryg t 9hasSugar.fSweetg is stated in (or can be derived from) the ontology.
These examples illustrate an obvious added value of epistemic extensions of description logics in practical applications. However former research { focused on extending tableaux algorithms for less expressive languages { has not paced up with the development of reasoners for very expressive DLs. In fact, as we will discuss in the course of this paper, some expressive features like nominal concepts require special care when combined with the idea of introspection by epistemic operators.
This paper investigates the epistemic extension of the very
expressive DL SROIQ [
We consider SROIQ as the underlying DL (for details see [
Following the way epistemic semantics for DLs have been hitherto
de ned (see, e.g., [
Next, we provide the de nition of epistemic interpretations. The main di erence to the non-epistemic case, is that we provide a \context" of relevant models which are inspected whenever the extension of an epistemic concept or role is to be determined.
De nition 1. An epistemic interpretation for SROIQK is a pair (I; W) where I is a SROIQ-interpretation and W is a set of SROIQ-interpretations, where I and all of W have the same in nite domain with NI . The interpretation function I;W is then de ned as follows: aI;W = a for a 2 NI
XI;W = XI for X 2 NC [ NR [ f>; ?g fa1;:::; angI;W = fa1;:::; ang (KC)I;W = T (CJ;W ) (KR)I;W = T
J 2W (C u D)I;W = CI;W \ DI;W
(:C)I;W = n CI;W (9R:Self)I;W = fx j (x; x) 2 RI;W g (9R:C)I;W = fx j 9y:(x; y) 2 RI;W ^ y 2 CI;W g (8R:C)I;W = fx j 8y:(x; y) 2 RI;W ! y 2 CI;W g (6nR:C)I;W = fx j #fy 2 CI;W j (x; y) 2 RI;W g (>nR:C)I;W = fx j #fy 2 CI;W j (x; y) 2 RI;W g
J 2W (C t D)I;W = CI;W [ DI;W (RJ;W ) ng ng where C and D are SROIQK-concepts and R is a SROIQK-role.
From the above, one can see that KC is interpreted as the set of objects that are in the extension of C under every interpretation in W. This also makes clear why the common domain and rigid term assumption have to be imposed; otherwise the respective extension intersections would be empty. Note that the rigid term assumption implies the unique name assumption (UNA), i.e., for any epistemic interpretation I 2 W and for any two distinct individual names a and b, we have that aI 6= bI .
The notions of knowledge base, TBox, RBox and Abox, their respective axioms, and their interpretations can be extended from SROIQ to SROIQK in the obvious way.
An epistemic model for a SROIQK-knowledge base is a maximal non-empty set W of SROIQ-interpretations such that (I; W) satis es for each I 2 W. A SROIQK-knowledge base is said to be satis able if it has an epistemic model. The knowledge base (epistemically) entails an axiom (written jj= ), if for every epistemic model W of , we have that for each I 2 W, the epistemic interpretation (I; W) satis es . By de nition, every SROIQ-knowledge base is a SROIQK-knowledge base. Note that a given SROIQ-knowledge base has up to isomorphism only one unique epistemic model which is the set of all models of having in nite domain and satisfying the unique name assumption. We denote this model by M( ). 3
Following the intuition that led to the introduction of the K operator as an extension of K-free standard DL reasoning, a rather intuitive basic requirement to an epistemic DL semantics is arguably the following. De nition 2. For a given DL L, an epistemic DL semantics represented by an entailment relation j is called L-backward-compatible if it coincides with the (non-epistemic) standard semantics (represented by j=) on nonepistemic axioms, i.e. for an L knowledge base and an L axiom both of which not containing K, we have j exactly if j= . Moreover, j is called L-UNA-backward-compatible, if j exactly if j= under the unique name assumption.
We can show that jj= is SRIQnU -UNA-backward-compatible, where SRIQnU denotes the description logic SROIQ without nominal concepts and the universal role. The main ingredient for this is the insight that for any nite interpretation of a given SRIQnU knowledge base, we can come up with an in nite interpretation such that both interpretations behave in exactly the same way in terms of satisfaction of axioms. Lemma 3. Let be a SRIQnU knowledge base. For any interpretation I there is an interpretation I! with in nite domain such that I j= if and only if I! j= :
As a consequence, the restriction to in nite models imposed by the common domain assumption turns out to be not essential in the case of SRIQnU . However, this situation changes drastically once nominals or the universal role are involved. To see this, consider the axioms > v fa; b; cg or > v 63U:>. Each of these axioms considered as a knowledge base has only models with at most three elements. Consequently, in both cases we have that is unsatis able w.r.t. the classical epistemic semantics and consequently by ex falso quodlibet we, e.g., obtain jj= > v ? whereas we clearly have 6j= > v ? even under the UNA. So we conclude that jj= is not UNA-backward-compatible for any description logic that features nominals or simultaneously number restrictions and the universal role; in particular, it is not SROIQ-UNA-backwardcompatible.
While the imposed UNA may be a deliberate decision, we believe that
non-SROIQ-UNA-backward-compatibility of classical epistemic
entailment is not intended but rather a side e ect of a semantics crafted for
and probed against less expressive description logics; it contradicts the
intuition behind the K operator. This motivates our quest for a more
appropriate, \domain- exible" epistemic semantics. In [
In order to allow for the necessary exibility, we need to relinquish the common domain assumption and the rigid term assumption in the epistemic semantics: The domains we consider in the possible worlds should be allowed to have arbitrary (yet non-empty) size and be composed of arbitrary elements. An individual name may refer to di erent elements in di erent possible worlds. Also, individuals denoted by di erent individual names may coincide in some worlds but not in others.
Still, due to the reasons discussed before, we have to nd a substitute for the common domain and rigid term assumptions as otherwise, every epistemic role or concept would have the empty set as extension. We solve the problem by introducing one abstraction layer that assigns abstract individual names to domain elements. These abstract individual names are elements from NI [ N and hence common to all interpretations, thus they can serve as the \common ground" for di erent interpretations with di erent domains. We require that every domain element is associated with at least one abstract name, however, we also allow for di erent names denoting the same domain element (thus allowing for the possibility of nite domains). This intuition leads to the de nition of extended interpretations.
Thereby, an extended SROIQ-interpretation I is a tuple ( I; I; 'I) such that { ( I; I) is a standard DL interpretation, { 'I : NI [ N I is a surjective function from NI [ N onto that for all a 2 NI we have that 'I(a) = aI.
Note that the function 'I returns the actual interpretation of an individual, given its (abstract) name, under the interpretation I. We lift 'I to sets of names and let 'I 1 denote the corresponding inverse. Based on the notion of extended interpretations, we de ne an extended epistemic interpretation for SROIQK as a pair (I; W), where I is an extended SROIQinterpretation and W is a set of extended SROIQ-interpretations. Similar to epistemic interpretations, we de ne an extended interpretation function I;W as I;W in De nition 1 with the following modi cations: (KC)I;W = 'I T (KR)I;W = 'I TJ2W 'J 1 CJ;W
J2W 'J 1 RJ;W Again, we set [(KR) ]J;W := (KR )J;W for an epistemic role (KR) .
The semantics of TBox, RBox and ABox axioms follows exactly that for the classical semantics. Here, instead of jj=, we use the symbol jj=e, where e indicates that the relation is w.r.t. the extended semantics.
Like in case of the traditional (epistemic) semantics, we can de ne the notions of extended epistemic modelhood and the satis ability of a SROIQK-knowledge base by considering extended interpretations instead of the standard DL interpretations. Similarly, the entailment (under the new semantics) of an axiom from a knowledge base can be de ned.
We now rst note that the newly established semantics has the desired compatibility property.
Theorem 4. jj=e is SROIQ-backward-compatible.
Proof sketch: First note that every satis able K-free knowledge base has exactly one extended epistemic model
M( ) = ( I; I; 'I) j ( I; I) j= ; 'I = IjNI [ f; f :N
I : Hence we have jj=e exactly if every I 2 Me( ) satis es , which (presuming being K-free) is the case exactly if j= .
Consequently, this new semantics is more adequate for very expressive DLs such as SROIQ. Yet, as will be shown later in the paper, it is also generic in the sense that for SRIQnU knowledge bases it behaves similar to the (classical) epistemic interpretation introduced earlier. With this new semantics, we avoid the aforementioned problems arising from nominals and the universal role in the language of a knowledge base. Arguably, this makes the revisited semantics a more suitable and appropriate choice for K-extensions of expressive description logics, like SROIQK. 5
We next introduce a novel technique for answering epistemic queries to SROIQ knowledge bases under the revised semantics. More precisely, we provide a way of checking whether a given knowledge base entails concept assertions, role assertions or concept subsumptions where the involved concepts and roles may contain K. Our method reduces this problem to a number of iterative entailment checks for K-free axioms. To justify the translation, we establish two lemmata (c.f., Lemma 25 and Lemma 27 in the technical report) that characterize possible instances of epistemic concepts and roles, respectively. The idea is that the extension of a concept that is preceded by K can only contain named individuals unless it comprises the whole domain. For roles we get a more intricate case distinction, however, it boils down to characterizing the set of \(inverse) role neighbors" of a xed individual as the whole domain or a set of named individuals. As an \exceptional case" to this, we might get the diagonal of I I as additional instances of an epistemic role.
Based on these characteristics of epistemic concepts and roles, we present a translation of epistemic concept expressions into equivalent Kfree ones. Note that the translation itself requires to check entailment of (K-free) axioms, hence it is not strictly syntactical and it depends on the underlying knowledge base.
Let be a SROIQ-knowledge base. For a SROIQ concept A and a SROIQ role R, let trgA;R denote the nominal concept fa1; : : : ; ang containing all ai for which j= A v 9R:faig and let trgA;R = ? if there are no such ai. We recursively de ne the function [[ ]] mapping SROIQK concept expressions to SROIQ concept expressions:
[[KD]] = f>a 2 NI j j= [[D]] (a)g [[9KS:Self]] = [[K9S:Self]] [[ KR:D]] = R:[[D]] for [[8KP:D]] = :[[9KP::D]] if C is from NI [ f>; ?g, a nominal,
or a K-free self concept; for 2 f8; 9; >n; 6ng, R K-free if j= [[D]] >
otherwise 2 f8; 9; >n; 6ng and j= R U [[9KP:D]] = 9P: trg>;P u [[D]] t (trg>;P u 9P:[[D]] ) t F a2NI (fag u 9P:(trgfag;P u [[D]] )) t [[D]] only|if {jz=>}v9P:Self [[6nKP:D]] = :[[>(n+1)KP:D]] [[>nKP:D]] = >nP:(trg>;P u [[D]] ) t (trg>;P u >nP:[[D]] ) t Fa2NI (fag u >nP:(trgfag;P u [[D]] g)) t (:fa j a2NIg u [[D]] u >(n 1)P: trg>;P u [[D]] ) | only if j={z>v9P:Self }
Observe that by de nition, the result of applying this function to an epistemic concept indeed yields a concept not containing K. Moreover the following lemma, which can be proved by structural induction over the concept expression, ensures that the translation function preserves the concept extension.
Lemma 6. Let be a SROIQ-knowledge base and C be a SROIQK concept. Then for any extended interpretation I 2 M( ), we have that CI;M( ) = [[C]] I;M( ).
Consequently this lemma can be employed to prove our main result justifying our approach of deciding entailment of epistemic axioms based on non-epistemic standard reasoning.
Theorem 7. For a SROIQ-knowledge base , SROIQK concept C, D, and an individual a, the following hold: 1. 2.
jj=eC(a) if and only if jj=eC v D if and only if j= [[C]] (a).
j= [[C]] v [[D]] .
Finally, we are also able to establish the correspondence that the classical and the newly introduced semantics coincide, as far as epistemic querying on SRIQnU knowledge bases is concerned. This result further substantiates our claim that our semantics is a natural extension of the original intuition behind epistemic DLs.
Theorem 8. Let be a SRIQnU knowledge base, C and D SROIQK concepts, and a an individual name. Then, the following hold: 1. 2.
jj=e C(a) under the unique name assumption if and only if C(a).
jj=e C v D under the unique name assumption if and only if C v D. jj= jj=
This can be proved by providing a transformation function similar to [[ ]] for the classical semantics, proving its correctness and showing that it coincides with [[ ]] on SRIQnU knowledge bases. 6
Based on the results established in the preceding section, we have implemented a preliminary prototype. The system takes an epistemic concept as input and translates it into an equivalent non-epistemic one according to De nition 5. A detailed system description is provided in the technical report. A running system has been uploaded and shared on googlecode1. For the purpose of testing, we consider two versions of the wine ontology2 with 483 and 1127 individuals. As a measure, we consider the translation time of an epistemic concept to a non-epistemic equivalent one and the instance retrieval time of the translated concept. We consider di erent epistemic concepts. For each such concept C, we consider a non-epistemic concept obtained from C by dropping the K-operators from it (see Table 1). Given a concept C, t(C) and jCij represent the time in seconds required to compute the instances and the number of instances computed for Ci. Finally for an epistemic concept ECi, tT(ECi) represents the time required to translate ECi to its non-epistemic equivalent. Table 2 provides our evaluation results. From Table 2, the time 1 http://code.google.com/p/epistemicdl/ 2 http://www.w3.org/TR/owl-guide/wine.rdf required to compute the number of instances is feasible; it is roughly in the same order of magnitude as for non-epistemic concepts. Note also that the runtime comparison between epistemic concepts ECi and their nonepistemic counterparts Ci should be taken with a grain of salt as they are semantically di erent in general, as also indicated by the fact that there are cases where retrieval for the epistemic concept takes less time than for the non-epistemic version. As a general observation, we noticed that instances retrieval for an epistemic concept where a K-operator occurs within the scope of a negation, tends to require much time. 7
We argued how the traditional semantics for epistemic DLs causes problems and thus suggested a revision to the semantics. We proved that this revised semantics solves the aforementioned problem while coinciding with the traditional semantics on less expressive DLs (up to SRIQnU ). Focusing on the new semantics, we provided a way of answering epistemic queries to SROIQ knowledge bases via a reduction to a series of standard reasoning steps. Finally, we presented an implementation allowing for epistemic querying in SROIQ.
Avenues for future research include the following: First, we will investigate to what extent the methods described here can be employed for entailment checks on SROIQK knowledge bases, i.e., in cases where K occurs inside the knowledge base. In that case, stronger non-monotonic e ects occur and the unique-epistemic-model property is generally lost. On the more practical side, we aim at further developing our initial prototype. We are con dent that by applying appropriate optimizations such as caching strategies and syntactic query preprocessing a signi cant improvement in terms of runtime can be achieved. In the long run, we aim at demonstrating the added value of epistemic querying by providing an appropriate user-front-end and performing user studies. Furthermore, we will propose an extension of the current OWL standard by epistemic constructs in order to provide a common ground for future applications.