Nonmonotonic Nominal Schemas Revisited

Abstract

Recently, a very general description logic (DL) that extends SROIQ (the DL underlying OWL 2 DL) at the same time with nominal schemas and epistemic modal operators has been proposed, which encompasses some of the most prominent monotonic and non-monotonic rule languages, including Datalog under the answer set semantics. A decidable fragment is also presented, but the restricted language does not fully cover all formalisms encompassed by the complete language. In this paper, we aim to remedy that by studying an alternative set of restrictions to achieve decidability, and we show that the existing embeddings of the formalisms covered by the full language can be adjusted accordingly.

1 Introduction

Extending Description Logics (DLs) with modeling features admitting non-monotonic reasoning has been frequently requested in many application domains (see, e.g., [ 14 ] for semantic matchmaking on annotations at electronic online marketplaces). In fact, the vast amount of work dedicated to the topic may serve as a witness in its own right. DLs have been extended, for example, with defaults [ 2 ], with notions of circumscription [ 4,33 ], and epistemic reasoning provided by the inclusion of modal1 operators within the language [ 8 ] or only in queries [ 29 ]. In addition, a plethora of approaches combine DLs with (often non-monotonic) rules (see, e.g., [ 9,30,19 ] and references in their sections on related work). As these approaches are commonly of different expressivity and based on quite advanced different formal grounds, a uniform overarching formalism allowing the integration of possibly all the various modeling features is an extremely complicated problem.

In [ 20 ], a very general DL language is introduced that extends the expressive DL underlying OWL 2, SROIQ, with nominal schemas [ 24 ] and epistemic operators as defined in [ 8 ] with the aim of integrating the W3C standards OWL [ 15 ] and (nonmonotonic) RIF [ 18 ] and their underlying formalisms, DLs and rule languages respectively, thus contributing towards the goal of a unifying logic for the Semantic Web (as foreseen in the well-known Semantic Web stack). The full language is in fact very expressive, capturing a variety of different formalisms, among them two based on MKNF logics [ 27 ] that had been considered of different expressivity so far – MKNF DLs [ 8 ], i.e., the epistemic extension of DLs, and Hybrid MKNF, one very expressive combination of DLs and non-monotonic rules. Though not the full language of the latter is 1 In the remainder of the paper, we use the terms modal and epistemic operator interchangeably to refer to the same notion. considered, coverage of Answer Set Programming [ 11 ] is ensured, arguably the most widely used non-monotonic reasoning rule formalism.

A decidable fragment of the full language is also considered in [ 20 ], which is strongly related to the one presented in [ 8 ]. In fact, the restrictions are such that the tableau algorithm presented in [ 8 ] can in principle be re-used. As it turns out, however, the decidable language does not encompass all the formalisms for which coverage within the full language is shown. While this does not invalidate the approach as such, in particular, if one views such a unifying formalism mainly as a conceptual underpinning, it is certainly undesired if one rather wants to use it for modeling and reasoning.

In this paper, we aim to solve this problem, i.e., we consider a different set of restrictions, for which we show that reasoning is decidable and that, at the same time, encompasses all the formalisms discussed in [ 20 ] with only minor adjustments to the previously presented embeddings. The principal idea builds on the usage of nominals and nominal schemas, which are necessarily present in the language by design anyway, to limit the applicability of concept inclusions containing modal operators. As an additional result, we believe that the new restrictions are more succinct and that the resulting adaptation of the procedure for verifying the existence of models becomes less complicated. To further simplify notation, here we do not consider the full language presented in [ 20 ], which is based on SROIQ, but rather a language based on ALC with only the minimally necessary extensions and we term this language eALCOV (see Sect. 2 for a detailed explanation on the name). As we can show, such language is already expressive enough to cover the desired non-monotonic modeling features.

The remainder of the paper proceeds as follows. In Sect. 2, we recall the syntax and semantics of the DL eALCOV we consider here. We then introduce the new alternative conditions of so-called safe eALCOV KBs in Sect. 3 and we subsequently show that these do ensure decidability of reasoning, i.e., checking (MKNF-)satisfiability. In Sect. 4, we show that, with minor adaptations, the applied changes do now permit coverage of the discussed formalisms in [ 20 ] within the decidable fragment (of safe eALCOV KBs), before we conclude and discuss future work in Sect. 5. 2

Epistemic DLs

In this section, we recall the syntax and semantics of epistemic description logics (DLs) from [ 20 ]. Here, we focus on a subset of the language considered in [ 20 ] to make the presentation more concise and to ease the reading. Namely, we consider the epistemic DL ALCKN F [ 8 ], which is ALC enhanced with epistemic operators, extended by nominals, nominal schemas [ 24 ], and the universal role. Nominal schemas represent variable nominals that can only be bound to known individuals, and the universal role can be represented using role hierarchies and negation on roles [ 23 ], but as we want to keep the presentation simple, we leave this implicit. Since the name of the resulting language ALCOVKN F (or even ALCHOV (:)KN F for the implicit encoding of the universal role) following standard and historic patterns would be quite cumbersome, we propose using the name eALCOV instead, which stands for epistemic ALCOV (including the universal role). The term epistemic originates from the two epistemic/modal operators K and A, where K is interpreted in terms of minimal knowledge, while A is interpreted j 9 with ( ; ) 2 R(I;M;N );Z and 2 C(I;M;N );Z g j ( ; ) 2 R(I;M;N );Z implies 2 C(I;M;N );Z g Interpretation I; MKNF structure (I; M; N ); variable assignment Z; A 2 NC ; C; D 2 C; V 2 NR; R 2 R; a; b 2 NI ; x 2 NV , and t 2 NV [ NI . as autoepistemic assumption and corresponds to :not, i.e., the classical negation of the negation as failure operator not used in [ 27 ] instead of A.

We consider a signature = hNI ; NC ; NR; NV i where NI , NC , NR, and NV are pairwise disjoint and finite sets of individual names, concept names, role names, and variables. In the following, we assume that has been fixed. We define concepts and roles in eALCOV by the following grammar.

R ::=V j U j KV j AV

C ::=> j ? j A j fig j fxg j :C j C u C j C t C j 9R:C j 8R:C j KC j AC where V 2 NR, A 2 NC , i 2 NI , and x 2 NV . The names of the individual concepts and roles can be found in Table 1. Epistemic concepts are knowledge and assumption concepts, while epistemic roles are knowledge and assumption roles.

As usual, a TBox axiom (or general concept inclusion (GCI)) is an expression C v D where C; D 2 C. An ABox axiom is of the form C(a) or V (a; b) where C 2 C, V 2 NR, and a; b 2 NI . An eALCOV axiom is any ABox or TBox axiom, and an eALCOV knowledge base (KB) is a finite set of eALCOV axioms.

The semantics of eALCOV as recalled from [ 20 ] is an adaptation from [ 24 ] and [ 8 ]. As common, an interpretation I = ( I ; I ) consists of a domain I 6= ; and a function I that maps elements in NI , NC , and NR to elements, sets, and relations of

I respectively. Additionally, nominal schemas require a variable assignment Z for an interpretation I, which is a function Z : NV ! I such that, for each v 2 NV , Z(v) = aI for some a 2 NI .

As common in MKNF-related semantics used to combine DLs with non-monotonic reasoning (see [ 8,17,19,30 ]), specific restrictions on interpretations are introduced to ensure that certain unintended logical consequences can be avoided (see, e.g., [ 30 ]). Here, we adopt the standard name assumption from [ 20 ]. An interpretation I (over to which is added) employs the standard name assumption if (1) NI extends NI with a countably infinite set of individuals that cannot be used in variable assignments, and I = NI ; (2) for each i in NI , iI = i; and (3) equality is interpreted in I as a congruence relation – that is, is reflexive, symmetric, transitive, and allows for the replacement of equals by equals [ 10 ]. The first condition fixes the (infinite) universe, but limits the application of variable assignments to a finite subset, the second condition defines I as a bijective function, while the third ensures that we still can identify elements of the domain. As an immediate side-effect, the variable assignment is no longer tied to a specific interpretation and we can simplify notation by using without reference to a concrete interpretation.

Now, the first-order semantics is lifted to satisfaction in MKNF structures that treat the modal operators w.r.t. sets of interpretations. An MKNF structure is a triple (I; M; N ) where I is an interpretation, M and N are sets of interpretations, and I and all interpretations in M and N are defined over . For any such (I; M; N ) and assignment Z, the function (I;M;N );Z is defined for arbitrary eALCOV expressions as shown in Table 1. (I; M; N ) and Z satisfy an eALCOV axiom , written (I; M; N ); Z j= , if the corresponding condition in Table 1 holds. (I; M; N ) satisfies , written (I; M; N ) j= , if (I; M; N ); Z j= for all variable assignments Z. A (non-empty) set of interpretations M satisfies , written M j= , if (I; M; M) j= holds for all I 2 M, and M satisfies an eALCOV knowledge base KB, written M j= KB, if M j= for all axioms 2 KB. Note the small deviation of the semantics of ftg in Table 1 compared to that in [ 24 ], which is necessary to ensure that the semantics works as intended under standard name assumption.

It can be verified that the two sets of interpretations are each used to interpret one of the modal operators, but in the monotonic semantics above, they simply coincide. This changes with the non-monotonic MKNF model defined in the usual fashion [ 8,17,19,30 ]: M is fixed to interpret A, and supersets M0 of M are used to test whether the knowledge derived from M (via K) is indeed minimal.

Definition 1. Given an eALCOV knowledge base KB, a (non-empty) set of interpretations M is an MKNF model of KB if (1) M j= KB, and (2) for each M0 with M M0, (I0; M0; M) 6j= KB for some I0 2 M0. KB is MKNF-satisfiable if an MKNF model of KB exists. An axiom is MKNF-entailed by KB, written KB j=K if all MKNF models M of KB satisfy .

As noted in [ 8 ], since M j= KB is defined w.r.t. (I; M; M), the operators K and A are interpreted in the same way, and so we can restrict instance checking KB j=K C(a) and subsumption KB j=K C v D to C and D without occurrences of the operator A. Also, in absence of modal operators in the eALCOV KB, there is a unique MKNF model which simply contains all standard (first-order) models of KB as usual. 3

Reasoning in eALCOV In [ 20 ], reasoning in eSROIQ2 is discussed following [ 8 ] for reasoning in ALCKN F . The problem with this approach is that it is undecidable in general, so, as in [ 8 ], restrictions are applied in [ 20 ] to regain decidability, which in certain cases prevent coverage of the formalisms encompassed by the unrestricted language. To circumvent this, we still rely on the same idea in principle, but we revise the applied restrictions to achieve decidability making use of the gained expressiveness in eALCOV . In the following, we spell out the restrictions with some motivation right away, before we show that this indeed yields a decidable procedure for checking MKNF-satisfiability. Following [ 8 ], the overall idea is to reduce reasoning in eALCOV to a number of reasoning tasks in non-modal ALCOV (again including U ), for which each model of an eALCOV KB is represented by means of an ALCOV KB. Formally, a set of interpretations M is ALCOV representable if there exists an ALCOV KB KBM such that M = fI j I satisfies KBMg. Then, undecidability can be caused by three sources. First, certain partially quantified expressions are not ALCOV representable (Theorem 4.1 in [ 8 ]), which is why we recall the notion of subjectively quantified KBs. For that purpose, we define that an ALCOV expression S is subjective if each ALCOV subexpression in S lies in the scope of at least one modal operator.

Definition 2. An eALCOV KB KB is subjectively quantified if each expression of the form 9R:C, 8R:C occurring in KB satisfies one of the conditions: (1) R is an ALCOV role and C is an ALCOV concept, or (2) R and C are both subjective and C is of the form KD, :KD, AD or :AD.

There exists a slightly relaxed condition on subjectively quantified KBs [ 17 ], but for our purposes the original one suffices.

Second, even if subjectively quantified, certain nested expressions can be problematic, so we introduce (modally) flat concepts, that can be seen as a further restriction of simple concepts in [ 8 ], which prohibit such nesting altogether. Formally, an eALCOV concept is flat if it does not contain any modal operator in scope of another, and an 2 In [ 20 ], the term SROIQV(Bs; )KN F is used, but, for the sake of readability and with a slight abuse of notation, we follow our introduced naming scheme here. eALCOV KB KB is flat if each concept in it is flat. Thus, quantifier expressions of the form (2) in Def. 2 are flat as long as D does not contain further modal operators.

Third, intuitively, we have to make sure that GCIs involving modal operators cannot be used to derive an infinite number of true assertions (see also Theorem 4.10 in [ 8 ]). Rather than introducing simple KBs as in [ 8,20 ], we build on nominals and nominal schemas to introduce safe concepts.

Definition 3. Given a subjectively quantified, flat eALCOV KB KB, an eALCOV concept C in KB is called safe if C is of the form D u ftg for some guard t 2 NI [ NV . The idea is to use the nominal (schema) as a guard that restricts “applicability” of concepts involving modal operators to individuals occurring in KB. This all combines in the definition of safe eALCOV KBs, for which we from now on consider two disjoint subsets of the eALCOV TBox T of KB: T 0, the set of all axioms that contain no modal operators, and , the set of all axioms that contain at least one modal operator. Definition 4. Let KB be an eALCOV KB that is subjectively quantified and flat. Then, KB is safe if the following conditions are satisfied: 1. For each C v D 2 , C is subjective and safe, D is safe for the same guard as C, and no operator K occurs in 9 and 8 restrictions in D; 2. There is no concept assertion in KB containing a subconcept of the form 9KR:KC. Notably, due to KB also being subjectively quantified and flat, any C v D 2 in a safe KB can be rewritten into one such that all subjective subconcepts in it are safe. For example, the safe KB containing just the axiom

((K(C t 9R:D) u 9KR:KG) t :AE) u fxg v 8AS:AF u fxg can be straightforwardly rewritten into ((K(C t 9R:D) u fxg) u (9KR:KG u fxg)) t (:AE u fxg) v 8AS:AF u fxg: In the following, we assume that any C v D 2 in a safe eALCOV KB is already rewritten this way, i.e., all subjective subconcepts in are assumed safe.

Comparing to simple KBs (Def. 8 in [ 20 ]), intuitively, KB being flat covers condition 3. while 1. of Def. 4 covers to 1. and 2. there. Condition 2. in Def. 4 is not strictly required for decidability (as the case can be handled by finitely many models up to renaming of individuals [ 8 ]), but it will simplify the subsequent material without affecting coverage of related formalisms. These new conditions for safe KBs certainly have quite a different flavor compared to simple KBs in [ 8,20 ], but we believe that they are overall simpler and more easy to grasp, and at the same time not jeopardizing coverage of related formalisms. Of course, we still need to show that there is a decidable procedure for reasoning with safe eALCOV KBs. 3.2

Determining MKNF Models

We start by grounding a given safe eALCOV KB, i.e., we replace all occurring nominal schemas with nominals in all possible ways in the usual manner. This yields an eALCO KB (again including U ), which is trivially safe and obtained in finite time, though, in general, of exponential size in terms of the input KB.

From now on, we follow the principal argument from [ 8 ] as used in [ 20 ], but with some variations and simplifications due to our different restrictions and to some extent inspired by the reasoning algorithms for the related Hybrid MKNF [ 30 ].

First, we will collect a set of modal atoms based on the occurrence of epistemic concepts and roles in a given KB. In difference to [ 8 ], we only consider atoms over individuals occurring in the given KB. In the following, we use M to denote either K or A, and N to denote either M or :M, we assume Q 2 f9; 8g, and we remind that we consider that all subjective concepts in are safe. Given a safe eALCO KB KB, the set of modal atoms M A(KB) is defined inductively as follows: (1) if MD u fag for some a 2 NI occurs in KB, then KD(a) 2 M A(KB); (2) if MD occurs (non-safe) in concept assertion C(a), then KD(a) 2 M A(KB); (3) if QMR:ND u fag for some a 2 NI occurs in KB, then KR(a; i); KD(i) 2

M A(KB) for all i 2 NI ; (4) if QMR:ND occurs (non-safe) in concept assertion C(a), then KR(a; i); KD(i) 2

M A(KB) for all i 2 NI ; (5) nothing else belongs to M A(KB).

A further difference to [ 8 ] is that we only collect modal atoms under K. This is justified by the fact that for ensuring condition (1) of Def. 1, the same set of interpretations M is considered for evaluating formulas under K and A. As an immediate benefit, when introducing partitions of these modal atoms next and guessing model candidates, we do not have to verify whether modal atoms under K and A are aligned.

We now introduce a partition of M A(KB), which is a pair (P; N ) of positive modal atoms P and negative modal atoms N such that P \ N = ; and P [ N = M A(KB). As already mentioned, such partition can be understood as a guess about which modal atoms are supposed to be true (P ) and false (N ), and we can use it to simplify an eALCO KB as follows. Given a safe eALCO KB KB and a partition (P; N ) of M A(KB), KB[P ] denotes the eALCO KB obtained from KB and (P; N ) by: 1. replacing each occurrence of the form MD u fag in KB and each (non-safe) occurrence of the form MD in a concept assertion C(a) 2 KB with > if KD(a) 2 P and with ? otherwise; 2. replacing each occurrence of 9MR:M1D u fag (9MR::M1D u fag) in KB and each (non-safe) occurrence of the form 9MR:M1D (9MR::M1D) in a concept assertion C(a) 2 KB with > if there exists y such that KR(a; y) 2 P and KD(y) 2 P (KD(y) 62 P ) and with ? otherwise; 3. replacing each occurrence of 8MR:M1D u fag (8MR::M1D u fag) in KB and each (non-safe) occurrence of the form 8MR:M1D (8MR::M1D) in a concept assertion C(a) 2 KB with > if for each y such that KR(a; y) 2 P , KD(y) 2 P (KD(y) 62 P ) and with ? otherwise.

Note that we leave N implicit here, as it is completely specified by P and the definition of a partition of M A(KB). We generalize the notion of KB[P ], based on two partitions (P; N ); (P 0; N 0) of M A(KB), to KB[P 0][P ] which is obtained from KB in exactly the same way, only that if M or M1 is K, then P 0 is used in the evaluation of the conditions, while for M or M1 being A, P is used. In either case, it can readily be verified that the resulting KB does not contain any modal operators, hence is an ALCO KB (admitting U ) for which satisfiability can be checked using standard DL reasoners.

With this in place, we can define an ALCO KB which takes the modal atoms guessed to be true into account, and use the resulting KB to check whether a guess is consistent with the original eALCO KB. Let KB be a safe eALCO KB and (P; N ), (P 0; N 0) partitions of M A(KB). Then, ObKB;P 0;P denotes the following ALCO KB:

ObKB;P 0;P = KB[P 0][P ] [ fC(x) j KC(x) 2 P 0g [ fR(x; y) j KR(x; y) 2 P 0g Then, partition (P; N ) of M A(KB) is consistent with the (safe) eALCO KB if the following conditions hold: (1) the ALCO KB ObKB;P;P is satisfiable; (2) ObKB;P;P 6j= C(x) for each KC(x) 2 N ; (3) ObKB;P;P 6j= R(x; y) for each KR(x; y) 2 N .

Basically, item (1) checks whether the guessed P does not yield contradictions w.r.t. KB, while (2) and (3) verify that no modal atom occurs wrongfully in N .

A link between a set of interpretations and partitions is established next. Let M be a set of interpretations over . Then, M induces the partition (P; N ) of M A(KB): P = fKC(x) j KC(x) 2 M A(KB) and M j= KC(x)g

[ fKR(x; y) j KR(x; y) 2 M A(KB) and M j= KR(x; y)g N = fKC(x) j KC(x) 2 M A(KB) and M 6j= KC(x)g

[ fKR(x; y) j KR(x; y) 2 M A(KB) and M 6j= KR(x; y)g

We can show that the intended correspondence indeed holds.

Lemma 1. Let KB be a safe eALCO KB, M a set of interpretations over that satisfies KB such that M j= KR(i1; i2) only if i1 a 2 NI and i2 b 2 NI , and (P; N ) the partition of M A(KB) induced by M. Then (P; N ) is consistent with KB. Note that here, the particular restriction on M is necessary, otherwise the property would not hold. Take (9AR:AC)(a). Then, M = fI j I j= R(a; i) ^ C(i) for some i 2 and i 6 ag clearly satisfies the assertion, yet the induced partition with P = ; is not consistent with KB (because of (1) and the fact that that KB[P ][P ] only considers modal atoms in M A(KB)). The same restriction is no longer necessary for MKNF models for which the following one-to-one correspondence between every MKNF model M of KB and the partition induced by M can be shown. Theorem 1. A set M of interpretations over is an MKNF model for a safe eALCO KB KB iff the partition (P; N ) of M A(KB) induced by M satisfies the following: (1) (P; N ) is consistent with KB; (2) M = fI j I j= ObKB;P;P g; and (3) for each partition (P 0; N 0) of M A(KB) such that P 0 P , at least one of the following conditions does not hold: (a) the ALCO KB ObKB;P 0;P is satisfiable; (b) ObKB;P 0;P 6j= C(x) for each KC(x) 2 N 0; (c) ObKB;P 0;P 6j= R(x; y) for each KR(x; y) 2 N 0.

As an immediate consequence of this procedure, we can show that safe eALCOV KBs are ALCOV representable.

Corollary 1. Let KB be a safe eALCOV KB, M an MKNF model of KB, and (P; N ) be the partition of M A (KB) induced by M. Then M = fI j I j= ObKB;P;P g. 4

Coverage within the Decidable Fragment

The established result in the previous section is certainly interesting in its own right, since, arguably, the imposed restrictions and the applied construction is considerably less complicated in terms of notation than the one applied in [ 8,20 ]. Anyway, the main outlined purpose of this revision is to ensure that the new decidable fragment encompasses all the formalisms for which coverage was shown in [ 20 ] only for the full language. In this section, we revisit this material and discuss relevant changes. 4.1

Monotonic Approaches

Naturally, our decidable language fragment of safe eALCOV KBs covers ALCOV (with and without U ) and all its sub-languages. This does not include SROIQ, i.e., OWL 2 DL and its tractable profiles, but a trivial adjustment following the ideas in [ 20 ] where modal operators are limited to ALCOV concepts is easily conceivable.

Coverage of RIF-CORE [ 3 ], i.e., n-ary Datalog, interpreted as DL-safe Rules [ 31 ] carries over from [ 20 ] or alternatively from [ 25 ]. In fact, the latter does not even require the usage of the universal role U which is just fine if we only want to embed a Datalog program. However, if we want to cover an embedding of n-ary Datalog interacting with DLs, then the former is required: consider the Datalog rule C(a) ! D(a) and a concept assertion C(a). The rule can be translated to 9atom:(C u fag) v 9atom:(D u f g a ) (slightly adjusted from [ 25 ]), but there is I such that atomI = ;, i.e., D(a) is no longer derivable. Thus, based on the former Datalog embedding, coverage of DL-safe SWRL [ 31 ], AL-log [ 7 ], and CARIN [ 26 ] carries over, i.e., without much surprise all monotonic approaches as outlined in [ 20 ] are covered. In [ 8 ], it is shown how several non-monotonic reasoning features (defaults, integrity constraints, and role and concept closure) can be modeled in the full language ALCKN F and it is argued that the restriction to simple KBs applied to achieve decidability does not impede coverage. The full eALCOV language obviously includes ALCKN F by design, but since we have changed the restrictions to achieve decidability, these results do not carry over automatically, so we briefly discuss coverage of these features for safe eALCOV KBs (and refer the reader for the detailed discussion to [ 8 ]).

First, closed DL-defaults [ 2 ] of the form are covered in [ 8 ], where , i, and are DL concepts and n 0. Closed defaults are limited in their applicability to individuals explicitly mentioned in the knowledge base. This is achieved in [ 8 ] by using a new atomic concept I in each translation of a default and adding the assertions I(a) for each a appearing in the knowledge base. Conceptually, this matches the idea of nominal schemas, so the translation of closed defaults can be presented as a safe eALCOV axiom

DK (d) = K u :A: 1 u u :A: n u fxg v K u fxg without the need to introduce new concepts or adding additional assertions, and it is easy to see that Theorem 3.1 from [ 8 ] can be adapted accordingly.

Theorem 2. Let h ; Di be an ALC KB with defaults, where is an ALC KB and D is a set of ALC-defaults. The eALCOV KB ( ; D) is such that, for every ALC-concept C and every individual a 2 NI , it holds h ; Di j= C(a) iff DK ( ; D) j= C(a).

Secondly, integrity constraints (ICs) are considered, and it is argued that ICs commonly apply to individuals explicitly mentioned in the considered KB and impose restrictions without changing the content of the KB. This is in line with our restrictions on safe eALCOV KBs and it can be verified that all examples discussed in [ 8 ] can be made safe explicitly by introducing guards fxg as for defaults. Finally, similar observations hold for the considerations on role and concept closure, i.e., all modeling features presented in [ 8 ] can indeed be adjusted to safe eALCOV KBs without much effort. 4.3

Hybrid MKNF

Hybrid MKNF as a combination of DLs with non-monotonic rules is based on MKNF logics as well, but of different expressivity due to the different restrictions applied to the full MKNF language in each of the two approaches [ 30 ]. In [ 20 ], an embedding of hybrid MKNF into epistemic DLs is presented (we refer to that paper for the technical details). Though not the full language of hybrid MKNF is embedded, the presented fragment suffices to cover Answer Set Programming [ 11 ], i.e., disjunctive Datalog with classical negation and non-monotonic negation under the answer set semantics. Unfortunately, the presented embedding is in general not covered within the decidable fragment in [ 20 ] as shown with the simple example > v 9U:(fag u C) and KD(a) KC(a) as the latter would be embedded as K(9U:(fag u C) v K(9U:(fag u C) which is not simple [ 20 ]. This can be remedied with safe eALCOV KB by changing the translation of MKNF rules dl(KH1 _ KHl KA1; : : : ; KAn; notB1; : : : ; notBm) in [ 20 ] to

Kdl(A1) u : : : u Kdl(An) u :Adl(B1) u : : : u :Adl(Bm) u fig v Kdl(H1) t : : : t Kdl(Hl) u fig where i is a fresh individual and dl the translation function on (possibly classically negated) atoms defined in [ 20 ]. Essentially, in the original embedding, such translated concepts in GCIs would due to the universal role either be interpreted as or ;. Here, we introduce a nominal as guard that acts as a surrogate for all elements in , thus reducing such interpretation to either i or ;. An adaptation of the results in [ 20 ] (Lemma 3 and Theorem 4) are then straightforward.

Theorem 3. Let K = (O; P) be a hybrid MKNF KB. M is an MKNF model of K iff M1 = fJ j J 2 f am(I) with I 2 Mg is a hybrid MKNF model of dl(K). This ensures that safe eALCOV KBs in fact embed the restricted version hybrid MKNF and therefore also ASP. 5

Conclusions

We have studied epistemic extensions of DLs focusing here on eALCOV, i.e., ALC extended with nominals, nominals schemas, the universal role, and two epistemic operators for modeling non-monotonic reasoning. We have shown that this language encompasses all non-monotonic modeling features and approaches discussed in [ 20 ], and that an extension to a few missing monotonic languages (e.g., SROIQ) is easily conceivable. We have introduced a set of restrictions on the general language which is different from that in [ 20 ], and we have shown that, under these restrictions, reasoning, i.e., checking MKNF-satisfiability becomes decidable, and, unlike in previous work, the restricted language still covers all the discussed modeling features.

An immediate matter for follow-up work is the computational complexity when reasoning with epistemic DLs, a question that has only received limited attention so far (in [ 8 ] a triple exponential space upper bound for reasoning with simple KBs has been pointed out, while no results are mentioned in [ 20 ]). It is clear that the complexity results established for reasoning with nominal schemas (without epistemic operators) [ 25 ] can serve as first necessary lower bounds, i.e., for eALCOV in particular a minimal lower bound is established by the fact that reasoning in ALCOV is 2EXPTIME-complete. This does neither account for the universal role nor the epistemic operators. Since ALC with arbitrary Boolean role constructors is NEXPTIME-complete [ 28,36 ] (as the restriction to safe Boolean role constructors in [ 36 ] does not suffice to cover U ), and the decision procedure for MKNF-satisfiability requires nondeterministically guessing the right partition, by combining the different sources of complexity we conjecture a lower bound of at least N2EXPTIME.

Another interesting topic for future work is to establish coverage for further related formalisms, for example by extending the expressiveness of rules permitted in the embedding of Hybrid MKNF, which then allows us to include already established embedding results for, e.g., [ 9,32 ] in [ 30 ] or by considering among others work on circumscription in DLs [ 4,33 ]. Building on the existing relation between epistemic extensions of DLs and Hybrid MKNF, we can also investigate the relation to parameterized logic programs [ 12,13 ], or multi-context systems [ 5 ] using the established connection between these and Hybrid MKNF [ 21 ]. Finally, an implementation may be considered given a) the more simple decision procedure proposed here and b) the recent work on implementing nominal schemas [ 22,37,6,34 ] and Hybrid MKNF [ 1,16 ]. In particular the encouraging results for Konclude [ 34,35 ] seem to indicate that this may in fact be achievable in a feasible manner.

Acknowledgments This work was partially supported by Fundac¸a˜o para a Cieˆncia e a Tecnologia under project “ERRO – Efficient Reasoning with Rules and Ontologies” (PTDC/EIA-CCO/121823/2010) and strategic project PEst/UID/CEC/04516/2013, and by FCT grant SFRH/BPD/86970/2012.

References

1. Alferes , J.J. , Knorr , M. , Swift , T. : Query-driven procedures for hybrid MKNF knowledge bases . ACM Trans. Comput. Log . 14 ( 2 ), 16 ( 2013 )

2. Baader , F. , Hollunder , B. : Embedding defaults into terminological representation systems . Journal of Automated Reasoning 14 , 149 - 180 ( 1995 )

3. Boley , H. , Hallmark , G. , Kifer , M. , Paschke , A. , Polleres , A. , Reynolds , D . (eds.): RIF Core Dialect . W3C Recommendation 22 June 2010 ( 2010 ), available from http://www.w3.org/TR/rif-core/

4. Bonatti , P.A. , Lutz , C. , Wolter , F. : The complexity of circumscription in dls . J. Artif. Intell. Res. (JAIR) 35 , 717 - 773 ( 2009 )

5. Brewka , G. , Eiter , T. : Equilibria in heterogeneous nonmonotonic multi-context systems . In: Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence . pp. 385 - 390 . AAAI Press ( 2007 )

6. Carral , D. , Wang , C. , Hitzler , P. : Towards an efficient algorithm to reason over description logics extended with nominal schemas . In: Faber, W. , Lembo , D . (eds.) Web Reasoning and Rule Systems - 7th International Conference , RR 2013 . Proceedings . LNCS, vol. 7994 , pp. 65 - 79 . Springer ( 2013 )

7. Donini , F.M. , Lenzerini , M. , Nardi , D. , Schaerf , A. : AL-log: Integrating datalog and description logics . Journal of Intelligent Information Systems 10 ( 3 ), 227 - 252 ( 1998 )

8. Donini , F.M. , Nardi , D. , Rosati , R.: Description logics of minimal knowledge and negation as failure . ACM Transactions on Computational Logic 3 ( 2 ), 177 - 225 ( 2002 )

9. Eiter , T. , Ianni , G. , Lukasiewicz , T. , Schindlauer , R. , Tompits , H.: Combining answer set programming with description logics for the Semantic Web . Artificial Intelligence 172 ( 12 - 13 ), 1495 - 1539 ( 2008 )

10. Fitting , M. : First-order logic and automated theorem proving . Springer, 2nd edn. ( 1996 )

11. Gelfond , M. , Lifschitz , V. : Classical negation in logic programs and disjunctive databases. New Generation Computing 9 , 365 - 385 ( 1991 )

12. Gonc¸alves, R., Alferes , J.J.: Parametrized logic programming . In: Janhunen, T. , Niemela¨, I. (eds.) Logics in Artificial Intelligence - 12th European Conference, JELIA 2010. Proceedings. LNCS , vol. 6341 , pp. 182 - 194 . Springer ( 2010 )

13. Gonc¸alves, R., Alferes , J.J. : Decidability and implementation of parametrized logic programs . In: Cabalar, P. , Son , T.C. (eds.) Logic Programming and Nonmonotonic Reasoning , 12th International Conference, LPNMR 2013 . Proceedings . LNCS, vol. 8148 , pp. 361 - 373 . Springer ( 2013 )

14. Grimm , S. , Hitzler , P. : Semantic Matchmaking of Web Resources with Local Closed-World Reasoning . International Journal of Electronic Commerce 12 ( 2 ), 89 - 126 ( 2008 )

15. Hitzler , P. , Kro¨ tzsch, M. , Parsia , B. , Patel-Schneider , P.F. , Rudolph , S. (eds.) : OWL 2 Web Ontology Language: Primer. W3C Recommendation 27 October 2009 ( 2009 ), available from http://www.w3.org/TR/owl2-primer/

16. Ivanov , V. , Knorr , M. , Leite , J.: A query tool for E L with non-monotonic rules . In: Alani, H. , Kagal , L. , Fokoue , A. , Groth , P.T. , Biemann , C. , Parreira , J.X. , Aroyo , L. , Noy , N.F. , Welty , C. , Janowicz , K . (eds.) The Semantic Web - ISWC 2013 - 12th International Semantic Web Conference, Proceedings, Part I. LNCS , vol. 8218 , pp. 216 - 231 . Springer ( 2013 )

17. Ke , P. : Nonmonotonic Reasoning with Description Logics . Ph.D. thesis , University of Manchester ( 2011 )

18. Kifer , M. , Boley , H. (eds.): RIF Overview. W3C Working Group Note 22 June 2010 ( 2010 ), available from http://www.w3.org/TR/rif-overview/

19. Knorr , M. , Alferes , J.J. , Hitzler , P. : Local closed world reasoning with description logics under the well-founded semantics . Artificial Intelligence 175 ( 9 - 10 ), 1528 - 1554 ( 2011 )

20. Knorr , M. , Hitzler , P. , Maier , F. : Reconciling OWL and non-monotonic rules for the semantic web . In: Raedt, L.D. , Bessie`re, C. , Dubois , D. , Doherty , P. , Frasconi , P. , Heintz , F. , Lucas , P.J.F . (eds.) ECAI 2012 - 20th European Conference on Artificial Intelligence. Proceedings. Frontiers in Artificial Intelligence and Applications , vol. 242 , pp. 474 - 479 . IOS Press ( 2012 )

21. Knorr , M. , Slota , M. , Leite , J. , Homola , M. : What if no hybrid reasoner is available? hybrid MKNF in multi-context systems . J. Log. Comput . 24 ( 6 ), 1279 - 1311 ( 2014 )

22. Krisnadhi , A. , Hitzler , P.: A tableau algorithm for description logics with nominal schema . In: Web Reasoning and Rule Systems - 6th International Conference , RR 2012 . Proceedings . LNCS, vol. 7497 , pp. 234 - 237 . Springer ( 2012 )

23. Kro¨tzsch, M.: Description Logic Rules , Studies on the Semantic Web , vol. 008 . IOS Press/AKA ( 2010 )

24. Kro¨tzsch, M. , Maier , F. , Krisnadhi , A.A. , Hitzler , P.: A better uncle for OWL: Nominal schemas for integrating rules and ontologies . In: Srinivasan, S. , Ramamritham , K. , Kumar , A. , Ravindra , M.P. , Bertino , E. , Kumar , R . (eds.) Proceedings of the 20th International World Wide Web Conference, WWW2011 . pp. 645 - 654 . ACM ( 2011 )

25. Kro¨tzsch, M. , Rudolph , S. : Nominal schemas in description logics: Complexities clarified . In: Baral, C. , Giacomo , G.D. , Eiter , T. (eds.) Principles of Knowledge Representation and Reasoning: Proceedings of the Fourteenth International Conference , KR 2014 . AAAI Press ( 2014 )

26. Levy , A.Y. , Rousset , M.C. : Combining Horn rules and description logics in CARIN . Artificial Intelligence 104 , 165 - 209 ( 1998 )

27. Lifschitz , V.: Nonmonotonic databases and epistemic queries . In: Mylopoulos, J. , Reiter , R . (eds.) Proceedings of the 12th International Joint Conferences on Artifical Intelligence, IJCAI'91 . pp. 381 - 386 . Morgan Kaufmann ( 1991 )

28. Lutz , C. , Sattler , U. : The complexity of reasoning with Boolean modal logics . In: Wolter, F. , Wansing , H., de Rijke, M. , Zakharyaschev , M. (eds.) Proc. of the 3rd Int. Conf. on Advances in Modal Logic (AiML 2000 ). pp. 329 - 348 . World Scientific ( 2002 )

29. Mehdi , A. , Rudolph , S. : Revisiting semantics for epistemic extensions of description logics . In: Burgard, W. , Roth , D . (eds.) Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence , AAAI 2011 . AAAI Press ( 2011 )

30. Motik , B. , Rosati , R.: Reconciling Description Logics and Rules . Journal of the ACM 57 ( 5 ), 93 - 154 ( 2010 )

31. Motik , B. , Sattler , U. , Studer , R.: Query answering for OWL-DL with rules . Journal of Web Semantics 3 ( 1 ), 41 - 60 ( 2005 )

32. Rosati , R.: DL+ Log: A tight integration of description logics and disjunctive datalog . In: Doherty, P. , Mylopoulos , J. , Welty , C.A . (eds.) 10th International Conference on the Principles of Knowledge Representation and Reasoning , (KR'06), Proceedings. pp. 68 - 78 . AAAI Press ( 2006 )

33. Sengupta , K. , Krisnadhi , A.A. , Hitzler , P. : Local closed world semantics: Grounded circumscription for OWL . In: Aroyo, L. , Welty , C. , Alani , H. , Taylor , J., Bernstein , A. , Kagal , L. , Noy , N.F. , Blomqvist , E. (eds.) The Semantic Web - ISWC 2011 - 10th International Semantic Web Conference, Proceedings. LNCS , vol. 7031 , pp. 617 - 632 . Springer ( 2011 )

34. Steigmiller , A. , Glimm , B. , Liebig , T. : Reasoning with nominal schemas through absorption . J. Autom. Reasoning 53 ( 4 ), 351 - 405 ( 2014 )

35. Steigmiller , A. , Liebig , T. , Glimm , B. : Konclude: System description . J. Web Sem . 27 , 78 - 85 ( 2014 )

36. Tobies , S. : Complexity results and practical algorithms for logics in knowledge representation . Ph.D. thesis , LuFG Theoretical Computer Science, RWTH-Aachen, Germany ( 2001 )

37. Wang , C. , Hitzler , P.: A resolution procedure for description logics with nominal schemas . In: Takeda, H. , Qu , Y. , Mizoguchi , R. , Kitamura , Y . (eds.) Second Joint International Conference, JIST 2012 . Proceedings . LNCS, vol. 7774 , pp. 1 - 16 . Springer ( 2012 )