Practical Epistemic Entailment Checking in SROIQ Anees Mehdi and Sebastian Rudolph Institute AIFB, Karlsruhe Institute of Technology, DE {anees.mehdi,sebastian.rudolph}@kit.edu Abstract. In this paper, we present a reasoner capable of epistemic inferences in SROIQ knowledge bases. We first identify some counter intuitive effects of imposing the traditional semantics in epistemic exten- sions 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. Addi- tionally, we provide an implementation of our approach and present first evaluation results. 1 Introduction In the early 1980s, Hector J. Levesque questioned the adequateness of the query language in knowledge formalisms [6]. He proposed the idea of embedding the epistemic operator K into a query language, thereby achieving the capabilities of knowledge base introspection. A similar line of research was initiated by R. Reiter in the context of databases [9]. Due to the extended reasoning capabilities, epistemic extensions have also been investigated (cf. e.g. [3, 2, 4]) in the context of Description Logics (DLs, cf. [1]). To see the usefulness of the K operator for epistemic querying, con- sider 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¬∃KlocatedIn .{FrenchRegion }. 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 {WhiteWine (MountadamRiesling ), locatedIn (MountadamRiesling , AustralianRegion )} as a subset, the query would yield MountadamRiesling as a result, whereas the same query without epistemic operators would produce an empty re- sult. 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 op- erator into a logic brings about non-monotonicity. Another typical use case for epistemic querying is integrity constraint checking: testing whether the axiom KWine v ∃KhasSugar .{Dry} t ∃KhasSugar .{OffDry} t ∃KhasSugar .{Sweet} 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 ∃hasSugar.{Dry} t ∃hasSugar.{OffDry} t ∃hasSugar.{Sweet} is stated in (or can be derived from) the ontology. These examples illustrate an obvious added value of epistemic ex- tensions 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 expres- sive DL SROIQ [5]. When applying a semantics along the lines of [4] to SROIQ we observe effects that clearly contradict natural requirements for epistemic reasoning (that we call backward compatibility). This di- rectly leads to the question for an altered semantics that “behaves well” also for SROIQ. We introduce such a semantics and show that it com- plies with the proposed requirements. With the more adequate semantics at hand, we then turn to the question of efficient algorithms for the specific problem of answering queries to classical (i.e., K-free) SROIQ ontolo- gies. We solve this problem by providing a sound and complete reduction from epistemic querying to standard DL reasoning; our approach reduces occurrences of the K operator to intermediate calls to a standard DL rea- soner. Employing this technique, existing reasoners for non-epistemic DLs can be reused in a black-box fashion for the task of answering epistemic queries. Based on this algorithm, we implemented a reasoner capable of answering epistemic queries to SROIQ knowledge bases. For the com- plete proofs and technical details, we refer the interested reader to the accompanying technical report [7]. 2 Epistemic DLs and the Classical Semantics We consider SROIQ as the underlying DL (for details see [5] ). The ex- tension of SROIQ with the epistemic operator K, denoted by SROIQK, allows K to appear in front of concept or role expressions. We call a SROIQK-role an epistemic role if K occurs in it. An epistemic role is simple if it is of the form KS where S is a simple SROIQ-role. Following the way epistemic semantics for DLs have been hitherto defined (see, e.g., [4] ), the classical semantics of SROIQK is given as possible world semantics in terms of epistemic interpretations. Thereby the following two central assumptions are made. (1) Common Domain Assumption: all interpretations are defined over a fixed countably infinite domain ∆. (2) Rigid Term Assumption: for all interpretations, the map- ping from individuals to domains elements is fixed (it is just the identity function). Due to these assumptions, we can w.l.o.g. stipulate ∆ := NI ∪N. Essentially, these assumptions are imposed in order to ensure that (sets of) domain elements can be referred to and dealt with uniformly in a cross-domain manner. Next, we provide the definition of epistemic interpretations. The main difference to the non-epistemic case, is that we provide a “context” of rel- evant models which are inspected whenever the extension of an epistemic concept or role is to be determined. Definition 1. An epistemic interpretation for SROIQK is a pair (I, W) where I is a SROIQ-interpretation and W is a set of SROIQ-interpre- tations, where I and all of W have the same infinite domain ∆ with NI ⊂ ∆. The interpretation function ·I,W is then defined as follows: aI,W = a for a ∈ NI X I,W = X I for X ∈ NC ∪ NR ∪ {>, ⊥} {a1 ,..., an }I,W = {a } T 1 ,..., anJ,W I,W (KR)I,W = J ∈W (RJ,W ) T (KC) = J ∈W (C ) (C u D)I,W = C I,W ∩ DI,W (C t D)I,W = C I,W ∪ DI,W (¬C)I,W = ∆ \ C I,W (∃R.Self)I,W = {x | (x, x) ∈ RI,W } (∃R.C)I,W = {x | ∃y.(x, y) ∈ RI,W ∧ y ∈ C I,W } (∀R.C)I,W = {x | ∀y.(x, y) ∈ RI,W → y ∈ C I,W } (6nR.C)I,W = {x | #{y ∈ C I,W | (x, y) ∈ RI,W } ≤ n} (>nR.C)I,W = {x | #{y ∈ C I,W | (x, y) ∈ RI,W } ≥ n} 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 ∈ 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 respec- tive 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) satisfies Σ for each I ∈ W. A SROIQK-knowledge base Σ is said to be satisfiable if it has an epistemic model. The knowledge base Σ (epistemically) entails an axiom α (written Σ ||= α), if for every epistemic model W of Σ, we have that for each I ∈ W, the epistemic interpretation (I, W) satisfies α. By definition, 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 infinite domain and satisfying the unique name assumption. We denote this model by M(Σ). 3 Problems with the Classical Semantics 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. Definition 2. For a given DL L, an epistemic DL semantics represented by an entailment relation |≈ is called L-backward-compatible if it coincides with the (non-epistemic) standard semantics (represented by |=) on non- epistemic axioms, i.e. for an L knowledge base Σ and an L axiom α both of which not containing K, we have Σ |≈ α exactly if Σ |= α. Moreover, |≈ is called L-UNA-backward-compatible, if Σ |≈ α exactly if Σ |= α under the unique name assumption. ♦ We can show that ||= is SRIQ\U -UNA-backward-compatible, where SRIQ\U denotes the description logic SROIQ without nominal con- cepts and the universal role. The main ingredient for this is the insight that for any finite interpretation of a given SRIQ\U knowledge base, we can come up with an infinite interpretation such that both interpretations behave in exactly the same way in terms of satisfaction of axioms. Lemma 3. Let Σ be a SRIQ\U knowledge base. For any interpreta- tion I there is an interpretation Iω with infinite domain such that I |= Σ if and only if Iω |= Σ. As a consequence, the restriction to infinite models imposed by the common domain assumption turns out to be not essential in the case of SRIQ\U . However, this situation changes drastically once nominals or the universal role are involved. To see this, consider the axioms > v {a, b, c} or > v 63U.>. Each of these axioms considered as a knowl- edge base Σ has only models with at most three elements. Consequently, in both cases we have that Σ is unsatisfiable w.r.t. the classical epis- temic semantics and consequently by ex falso quodlibet we, e.g., obtain Σ ||= > v ⊥ whereas we clearly have Σ 6|= > v ⊥ even under the UNA. So we conclude that ||= is not UNA-backward-compatible for any descrip- tion logic that features nominals or simultaneously number restrictions and the universal role; in particular, it is not SROIQ-UNA-backward- compatible. While the imposed UNA may be a deliberate decision, we believe that non-SROIQ-UNA-backward-compatibility of classical epistemic entail- ment is not intended but rather a side effect 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-flexible” epistemic semantics. In [8], another ap- proach, based on first-order logic (FOL), has been presented which cir- cumvents the described problem by treating the equality as a congruence relation with minimized extension. However, the solution we present is closer to the original DL setting as it extends the standard definition of DL interpretations. 4 A Revisited Semantics In order to allow for the necessary flexibility, we need to relinquish the common domain assumption and the rigid term assumption in the epis- temic 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 different elements in different possible worlds. Also, individuals denoted by different individual names may coincide in some worlds but not in others. Still, due to the reasons discussed before, we have to find a substi- tute 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 different interpretations with different domains. We require that every domain element is associ- ated with at least one abstract name, however, we also allow for different names denoting the same domain element (thus allowing for the possibil- ity of finite domains). This intuition leads to the definition 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 ∆I , such that for all a ∈ NI we have that ϕI (a) = aI . Note that the function ϕI returns the actual interpretation of an indi- vidual, 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 define an extended epistemic inter- pretation for SROIQK as a pair (I, W), where I is an extended SROIQ- interpretation and W is a set of extended SROIQ-interpretations. Sim- ilar to epistemic interpretations, we define an extended interpretation function ·I,W as ·I,W in Definition 1 with the following modifications: (KC)I,W = ϕI −1 C J,W T  J∈W ϕJ (KR)I,W = ϕI −1 RJ,W T  J∈W ϕJ 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 ||=, we use the symbol ||=e, where e indicates that the relation is w.r.t. the extended semantics. Like in case of the traditional (epistemic) semantics, we can define the notions of extended epistemic modelhood and the satisfiability of a SROIQK-knowledge base by considering extended interpretations in- stead of the standard DL interpretations. Similarly, the entailment (under the new semantics) of an axiom from a knowledge base can be defined. We now first note that the newly established semantics has the desired compatibility property. Theorem 4. ||= e is SROIQ-backward-compatible. Proof sketch: First note that every satisfiable K-free knowledge base Σ has exactly one extended epistemic model M(Σ) = (∆I , ·I, ϕI ) | (∆I , ·I ) |= Σ, ϕI = ·I |NI ∪ f, f :N∆I .  Hence we have Σ ||=e α exactly if every I ∈ Me (Σ) satisfies α, which (presuming α being K-free) is the case exactly if Σ |= α.  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 SRIQ\U knowledge bases it behaves similar to the (classical) epistemic interpretation introduced earlier. With this new semantics, we avoid the aforementioned problems arising from nomi- nals 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 Reducing Epistemic Querying to Standard DL Reasoning 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 con- cept that is preceded by K can only contain named individuals unless it comprises the whole domain. For roles we get a more intricate case dis- tinction, however, it boils down to characterizing the set of “(inverse) role neighbors” of a fixed 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 K- free 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. Definition 5. (Translation Function [[·]]Σ ) Let Σ be a SROIQ-knowledge base. For a SROIQ concept A and a SROIQ role R, let trgA,R Σ denote the nominal concept {a1 , . . . , an } containing all ai for which Σ |= A v ∃R.{ai } and let trgA,R Σ = ⊥ if there are no such ai . We recursively define the function [[·]]Σ mapping SROIQK concept expressions to SROIQ concept expressions: [[C]]Σ = C if C is from NI ∪ {>, ⊥}, a nominal, or a K-free self concept; [[C1 u C2 ]]Σ = [[C1 ]]Σ u [[C2 ]]Σ [[C1 t C2 ]]Σ = [[C1 ]]Σ t [[C2 ]]Σ [[¬C]]Σ = ¬[[C]]Σ [[ΞR.D]]Σ = ΞR.[[D]]Σ for Ξ ∈ {∀, ∃, >n, 6n}, R K-free  > if Σ |= [[D]]Σ ≡ > [[KD]]Σ = {a ∈ NI | Σ |= [[D]]Σ (a)} otherwise [[∃KS.Self]]Σ = [[K∃S.Self]]Σ [[ΞKR.D]]Σ = ΞR.[[D]]Σ for Ξ ∈ {∀, ∃, >n, 6n} and Σ |= R≡U [[∀KP.D]]Σ = ¬[[∃KP.¬D]]Σ − [[∃KP.D]]Σ = ∃P. trg>,P u [[D]]Σ t (trg>,P  Σ Σ u ∃P.[[D]]Σ ) F {a},P t a∈NI ({a} u ∃P.(trgΣ u [[D]]Σ )) t [[D]]Σ | {z } only if Σ|=>v∃P.Self [[6nKP.D]]Σ = ¬[[>(n+1)KP.D]]Σ − [[>nKP.D]]Σ = >nP.(trg>,P Σ u [[D]]Σ ) t (trg>,P Σ u >nP.[[D]]Σ ) F {a},P t a∈NI ({a} u >nP.(trgΣ u [[D]]Σ })) t (¬{a | a∈NI } u [[D]]Σ u >(n−1)P. trg>,P  Σ u [[D]]Σ ) | {z } only if Σ|=>v∃P.Self ♦ Observe that by definition, 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 ∈ M(Σ), we have that C I,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. Σ ||= e C(a) if and only if Σ |= [[C]]Σ (a). 2. Σ ||= e C v D if and only if Σ |= [[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 SRIQ\U knowledge bases is concerned. This result further substan- tiates our claim that our semantics is a natural extension of the original intuition behind epistemic DLs. Theorem 8. Let Σ be a SRIQ\U knowledge base, C and D SROIQK concepts, and a an individual name. Then, the following hold: 1. Σ ||= e C(a) under the unique name assumption if and only if Σ ||= C(a). 2. Σ ||= e C v D under the unique name assumption if and only if Σ ||= C v D. 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 SRIQ\U knowledge bases. 6 A System Based on the results established in the preceding section, we have imple- mented a preliminary prototype. The system takes an epistemic concept as input and translates it into an equivalent non-epistemic one according to Definition 5. A detailed system description is provided in the techni- cal report. A running system has been uploaded and shared on google- code1 . 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 con- sider different 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 |Ci | 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 equiv- alent. 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 Table 1. Concepts used for instance retrieval experiments. C1 ∃hasWineDescriptor.WineDescriptor EC1 ∃KhasWineDescriptor.KWineDescriptor C2 ∀hasWineDescriptor.WineDescriptor EC2 ∀KhasWineDescriptor.KWineDescriptor C3 ∃hasWineDescriptor.WineDescriptor u ∃madeFromFruit.WineGrape EC3 ∃KhasWineDescriptor.KWineDescriptor u ∃KmadeFromFruit.KWineGrape C4 WhiteWine u ¬∃locatedIn.{FrenchRegion} EC4 KWhiteWine u ¬∃KlocatedIn.{FrenchRegion} C5 Wine u ¬∃hasSugar .{Dry} u ¬∃hasSugar .{OffDry} u ¬∃hasSugar .{Sweet} EC5 KWine u ¬∃KhasSugar .{Dry} u ¬∃KhasSugar .{OffDry} u ¬K∃hasSugar .{Sweet} Table 2. Evaluation Ontology Concept t(Ci ) |Ci | Concept tT(ECi ) t(ECi ) |ECi | C1 2.13 159 EC1 46.98 0.04 3 Wine 1 C2 0.01 483 EC2 0.18 0.00 0 C3 28.90 159 EC3 79.43 6.52 3 C4 0.13 0 EC4 95.60 107.82 72 C5 52.23 80 EC5 60.78 330.49 119 C1 8.51 371 EC1 351.78 0.13 308 Wine 2 C2 0.30 1127 EC2 0.127 0.00 0 C3 227.10 371 EC3 641.24 19.58 7 C4 0.34 0 EC4 865.04 840.97 168 C5 295.87 240 EC5 381.41 2417.65 331 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 non- epistemic counterparts Ci should be taken with a grain of salt as they are semantically different 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 Conclusion and Outlook We argued how the traditional semantics for epistemic DLs causes prob- lems 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 SRIQ\U ). Focusing on the new semantics, we provided a way of answering epistemic queries to SROIQ knowledge bases via a reduction to a series of stan- dard reasoning steps. Finally, we presented an implementation allowing for epistemic querying in SROIQ. Avenues for future research include the following: First, we will inves- tigate 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 effects occur and the unique-epistemic-model property is generally lost. On the more practical side, we aim at further developing our initial pro- totype. We are confident that by applying appropriate optimizations such as caching strategies and syntactic query preprocessing a significant im- provement 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 con- structs in order to provide a common ground for future applications. References 1. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cam- bridge University Press (2003) 2. Donini, F., Nardi, D., Rosati, R.: Non-first-order features in concept languages. In: Proceedings of the Fourth Conference of the Italian Association for Artificial Intelligence (AI*IA’95). pp. 91–102. Springer (1995) 3. Donini, F.M., Lenzerini, M., Nardi, D., Schaerf, A., Nutt, W.: Adding epistemic operators to concept languages. In: Bernhard Nebel, Charles Rich, W.R.S. (ed.) Proceedings of the 3rd International Conference on Principles of Knowledge Repre- sentation and Reasoning (KR’92). pp. 342–353. Morgan Kaufmann (1992) 4. Donini, F.M., Lenzerini, M., Nardi, D., Schaerf, A., Nutt, W.: An epistemic operator for description logics. Artificial Intelligence 100(1-2), 225–274 (1998) 5. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Doherty, P., Mylopoulos, J., Welty, C.A. (eds.) Proceedings of the 10th International Confer- ence on Principles of Knowledge Representation and Reasoning (KR’06). pp. 57–67. AAAI Press (2006) 6. Levesque, H.J.: Foundations of a functional approach to knowledge representation. Artificial Intelligence 23(2), 155–212 (1984) 7. Mehdi, A., Rudolph, S.: Revisiting semantics for epistemic extensions of description logics. Technical Report 3015, Institute AIFB, Karlsruhe Institute of Technology (2011), available at http://www.aifb.kit.edu/web/Techreport3015/en 8. Motik, B., Rosati, R.: Reconciling description logics and rules. J. ACM 57(5) (2010) 9. Reiter, R.: What should a database know? Journal of Logic Programming 14(1-2), 127–153 (1992)