We propose an extension of SROIQ with nominal schemas which can be used like “variable nominal concepts” within axioms. This feature allows us to express arbitrary DL-safe rules in description logic syntax. We show that adding nominal schemas to SROIQ does not increase its worst-case reasoning complexity, and we identify a family of tractable DLs SROELVn that allow for restricted use of nominal schemas.
(
that both DL axioms and rules are syntactically allowed, and a combined formal semantics defines how the hybrid language is to be understood. Unfortunately, such a combination often leads to undecidability. This is the case for the Semantic Web Rule Language SWRL [5,6], which is the most straightforward rule extension of OWL, and for the combination of OWL DL ontologies and the Rule
discussed idea for retaining decidability is to restrict the applicability of rules to named individuals, i.e., to logical constants that are explicitly mentioned in the ontology. Rules that are understood in this sense are called DL-safe, and the combination of OWL DL and DL-safe rules is indeed decidable [5,14].
A generalization of DL-safe rules, based on DL-safe variables, has been introduced [11] as part of the definition of the tractable rule language ELP. Rather than restricting all variables in a (DL-safe) rule to binding only to known individuals, DL-safe variables allow the ontology engineer to explicitly specify the variables to be treated this way. This approach was subsequently generalized to obtain DL+safe Rules as a class of expressive rule languages for which reasoning is still decidable [9].
elements of DL syntax. While the semantic intuition behind nominal schemas is the same as that behind DL-safe variables, the difference lies in the fact that
seamlessly with DL syntax. As a consequence, the language which we propose encompasses DL-safe variable SWRL while staying within the DL/OWL language paradigm. It thus achieves within the DL framework what has hitherto only been achieved by hybrid approaches.
hasParent(mary; john) (9hasParent:9married:fjohng)(mary) (2) (3)
Mary belongs to the class of individuals with some (unnamed) parent who is
married to John. Using a first-order logic semantics as in SWRL, rule (
(4)
which is to be read as a variable nominal that can only represent nominals (i.e., z binds to known individuals), where the binding is the same for all occurrences of the nominal schema in an axiom.
tion logics, denoted by the letter V in the DL nomenclature, and define the expressive DL SROIQV as an extension of SROIQ.
N2ExpTime-complete, and thus not harder than for SROIQ.
for which reasoning is possible in polynomial time.
allows DLs to incorporate arbitrary DL-safe rules, given that concept intersections, existential role restrictions, and the universal (top) role are available. Since such rules preclude polytime reasoning, our tractable DLs SROE LV n employ restrictions on the number of certain occurrences of nominal schemas in each axiom.
The close relationship to nominals suggests simple ways of introducing nominal schemas into concrete syntactic forms of OWL 2, e.g. by using the existing syntax for nominal classes with special individual names that represent variables (using some suitable naming convention). This opens a path for introducing this feature into practical applications. While the above worst-case complexity result for SROIQV may seem encouraging, we believe that the tractable ontology languages SROE LV n are the most promising candidates for implementations.
This paper is a condensed presentation of the main results of [13] where we develop all results for the slightly more general case of DLs with Boolean role constructors and concept products [18]. Moreover, [13] also explains how DL-safe rules (and hence DLs with nominal schemas) can be used to express OWL RL ontologies, and provides an extended discussion of related approaches which include description graphs, existential rules and tuple-generating dependencies (TGDs) in Datalog, and DL Rules.
in Section 4. In Section 5 we show how DL-safe rules can be expressed with nominal schemas, and Section 6 concludes. 2
Nominal Schemas in SROI Q
logics. We first generally introduce the feature for SROIQ to obtain the very expressive DL SROIQV.
A signature of SROIQV is a tuple = hNI ; NC ; NR; NV i of mutually disjoint sets of individual names, concept names, role names, and variables. Variables can be used like individuals in nominal expressions, and concept expressions of SROIQV are thus defined as follows:
C ::= > j ? j NC j fNI g j fNV g j :C j C u C j C t C j
9R:C j 8R:C j 9S:Self j 6k S:C j >k S:C where k is a natural number, and R (S) is a (simple) SROIQ role as usual.
usual, but with the extended set of concept expressions. Herein, we restrict our attention to SROIQV knowledge bases with regular RBoxes, which are defined as in SROIQ.
Axiom (4) above is an example of a SROIQV TBox axiom, where fzg is a nominal schema. Intuitively, each nominal schema appearing in an axiom is universally quantified, but ranges only over elements that are referred to by an individual name. We note that it would also be straightforward to introduce nominal schemas into the normative RDF syntax for OWL 2 [16]. One way to do this would be to provide URIs for variables in the OWL namespace, used instead of individuals in owl:oneOf statements (which are used for the RDF syntax for nominals in OWL 2). Attaching the semantics of nominal schemas to “reserved” variable URIs would allow the reuse of existing tools for representation, manipulation, parsing, and serialization.
ers for named individuals, i.e. elements of the interpretation domain that are represented by individual names in NI . This can be accomplished by using a suitably restricted form of variable assignment. Equivalently, one can eliminate nominal schemas by replacing them with the (finitely many) nominals that they can represent, and apply the standard SROIQ semantics to the result [13]. Definition 1. The grounding ground( ) of a SROIQV axiom is the set of all axioms that can be obtained by uniformly replacing nominal schemas in with nominals of the given signature. Given a SROIQV knowledge base KB, we define ground(KB) := S 2KB ground( ).
A DL interpretation I is a model of a SROIQV axiom , written I j= , if and only if I is a model of the knowledge base ground( ). Satisfaction and entailment of SROIQV axioms and knowledge bases is defined as usual.
ity and regularity. Definition 1 provides a direct approach for reasoning with SROIQV, though not necessarily a very practical one given that each SROIQV axiom represents an exponential number of SROIQ axioms obtained by grounding. However, this observation already yields an upper bound for the complexity of reasoning with SROIQV that is exponentially larger than that of SROIQ, i.e. N3ExpTime. In the remainder of this section, we prove that this result can be refined to obtain an N2ExpTime upper complexity bound, showing that this reasoning problem must be N2ExpTime-complete. To accomplish this, we extend the original proof for the worst-case complexity of SROIQ [8].
reduction of DL knowledge bases to theories of C2, the two-variable fragment of
first-order logic with counting quantifiers, for which satisfiability can be checked
in NExpTime [17]. The reduction proceeds in three steps: (
A v 8R:B A v >n S:B A v 6n S:B d Ai v F Bj
A fag A 9S:Self where R(i); S1; S2 2 NR with S1; S2 simple, and C D is short for fC v
The only axioms that are not readily expressed in C2 are complex RIAs. They are eliminated next, with exponential effort.
(NFA) to represent RIAs that entail non-simple roles. Suitable NFA for SROIQ were defined in [4,7]. We do not repeat the details of this construction here, and merely quote the essential results. Proofs for the following facts can be found in [4] and the accompanying technical report.
Fact 1 Consider a SROIQ knowledge base KB. For each (possibly inverse) non-simple role R 2 R, there is an NFA AR over the alphabet NR such that for every model I of KB, and for every word S1 : : : Sn accepted by AR:
If h i; i+1i 2 SiI for all i = 1; : : : ; n, then h 1; n+1i 2 RI .
Moreover, let denote a strict linear order that witnesses regularity of KB as required in [4]. For each non-simple R 2 NR, the number of states of AR is bounded exponentially in the depth of KB that is defined as: maxfn j there are S1 : : : Sn such that
Ti1 : : : Si : : : Timi v Si+1 2 KBg
proceeds by replacing every axiom of the form A v 8R:B by the following set of axioms, where AR is the NFA as introduced above, and Xq are fresh concept names for each state q of AR:
A v Xq Xq v 8S:Xq0
Xq v B q is the initial state of AR AR has a transition q !S q0 q is a final state of AR
The number of new axioms (and fresh concept names) that are introduced for each axiom of the form A v 8R:B is bounded by the sum of the number of states and transitions in AR, and the number of transitions in turn is linear in the number of role names and states. According to Fact 1, the number of axioms introduced for each axiom A v 8R:B is exponentially bounded in the depth of the knowledge base. The overall size of the knowledge base after step (2) therefore is bounded by a function that is linear in the size of the knowledge base and exponential in the depth of the knowledge base.
Step (3), finally, is a simple rewriting to C2 that does not increase the size of the knowledge base. To obtain the main result of this section, it suffices to observe that grounding does not increase the depth of the knowledge base: Theorem 1. The problem of deciding the satisfiability of SROIQV knowledge bases is N2ExpTime-complete.
affected by grounding, hence the depth of ground(KB) is equal to the depth of KB.
(
isfiability is N2ExpTime-hard [8]. tu 3
SROIQ is encouraging, yet we are far from a practical reasoning procedure for this DL. In particular, Theorem 1 is based on a procedure that still takes exponentially longer than the original approach for SROIQ, without this affecting the worst-case complexity. In this section, we therefore focus on identifying cases where inferencing is possible in polynomial time. This still leads to a rather expressive tractable DL. In [13], we also further discuss the relationship to the tractable profiles of OWL 2.
the number of “problematic” occurrences of nominal schemas detailed below. The
complex role inclusions, Self, and concept products [18]. Here, we only need the special concept product > >, denoted as the universal role U . In particular, we also omit range restrictions R v > C since they do not contribute to our treatment.
To preserve tractability when adding nominal schemas, we must avoid the increase in the number of axioms during grounding, which is exponential in the number of nominal schemas per axiom. Unfortunately, one cannot reduce the number of nominal schemas by normal form transformations in general, since they represent complex dependencies that cannot be simplified. But there are special cases where nominal schemas on the left-hand side of TBox axioms can be eliminated, or separated using independent axioms. One such case was identified in [11] for the rule language ELP: if the dependencies expressed in a rule body are tree-shaped then the rule can always be reduced to a small set of normalized rules with a limited number of variables in each. For example, a rule body that consists of a conjunction A(x) ^ R(x; z) ^ S(x; y) ^ B(y) ^ T (y; z) R S T is not tree-shaped since there are parallel paths x ! z and x ! y ! z in the corresponding dependency structure. In our case, binary predicates are role names, unary predicates are concept names, and constant symbols correspond to nominals. Variables can either be “hidden” in the structure of the DL concept expression, or occur explicitly as nominal schemas (the latter are called DLsafe variables in ELP). For example, the above rule body can be expressed as a concept A u 9R:fzg u 9S:(B u 9T:fzg).
mechanism for ensuring that normal form transformations are possible, and merely identify sufficient conditions for which this is the case. An obvious condition that implies tree-shaped dependencies is that a nominal schema occurs only once, and only on the left-hand side of a TBox axiom. As in [11], the treeshape only refers to variables (DL-safe or not), not to constants, in rule bodies.
pendency structure. For instance, if B in the above rule body is replaced by a nominal fag, then the concept would be tree-shaped. In such a case, we say that the nominal fzg occurs in a safe environment, as defined next.
Definition 2. An occurrence of a nominal schema fxg in a concept C is safe if C has a sub-concept of the form fag u 9R:D for some a 2 NI , such that D contains the occurrence of fxg but no other occurrence of any nominal schema. In this case, fag u 9R:D is a safe environment for this occurrence of fxg. S(a; x) will sometimes be used to denote an expression of the form fag u 9R:D within which fxg occurs safely.
A nominal schema fxg is safe for a SROIQV TBox axiom C v D if fxg does not occur in D, and at most one occurrence of fxg in C is not safe. Definition 3. Let n 0. A SROE LV n concept is a SROIQV concept that may contain >, ?, u, 9, Self, the universal role, nominals and nominal schemas, but which does not contain t, :, 8, 6k , >k , or inverse roles.
A SROE LV n TBox axiom is a SROIQV TBox axiom that uses SROE LV n concepts only, and where at most n nominal schemas are not safe for . An RBox axiom of SROE LV n is an RBox axiom of SROIQV that does not contain inverse roles. A SROE LV n knowledge base is a SROIQV knowledge base that contains only SROE LV n axioms.
most jNI jn axioms are introduced during grounding. We will fix n at a constant small value, so this increase is polynomial. When viewing nominal schemas as a way of augmenting DL expressivity in existing applications, it seems plausible that this number remains small. Axiom (4) is an example of a SROE LV 1 axiom. 4
Reasoning with S ROE LV n If n is constant, the problem of checking satisfiability in SROE LV n is possible in polynomial time w.r.t. the size of the knowledge base. To show this, we provide a polynomial transformation to the DL SROE L( ) [12]. baseLegtroKuBndb+e(Ka BS)RaOsfEoLllVownsk.nTohweleRdBgeoxbaansed. AWBeodxefiofnegraouSnRd+O(EKLB() a)reknthowelseadmgee as the RBox and ABox of KB. For each TBox axiom following axioms are added to ground+(KB): = C v D 2 KB, the 1. For each nominal schema fxg safe for , with safe occurrences in environments Si(ai; x) for i = 1; : : : ; l, introduce a fresh concept name Ox; . For every individual b 2 NI in KB, ground+(KB) contains an axiom l l 9U:Si(ai; b) v 9U:(fbg u Ox; ); i=1 where Si(ai; b) denotes Si(ai; x) with fxg replaced by fbg, and the empty conjunction (l = 0) denotes >. 2. A concept C0 is obtained from C as follows. Initialize C0 := C. For each nominal schema fxg that is safe for : (a) replace all safe occurrences S(a; x) in C0 by fag; (b) replace the non-safe occurrence (if any) of fxg in C0 by Ox; ; (c) set C0 := C0 u 9U:Ox; . After these steps, C0 contains only nominal schemas that are not safe for , and neither for C0 v D.
Now add axioms ground(C0 v D) to ground+(KB).
Theorem 2. Given a SROE LVn knowledge base KB, the size of ground+(KB) is exponential in n and polynomial in the size of KB.
then step 1 above introduces at most mk axioms for each axiom with k nominal schemas. This is polynomial in the size of KB. The second step introduces jground(C0 v D)j many axioms, and hence at most mn axioms for each . tu
if ground+(KB) is satisfiable. A knowledge base is unsatisfiable if and only if it entails fag v ? for arbitrary a 2 NI . This reduces satisfiability testing to instance retrieval (checking if a is an instance of ?). Using the polynomial time instance retrieval method for SROE L( ) from [12], we thus obtain the following result. Hardness for P follows from the hardness of SROE L( ). Theorem 3. If KB is a SROE LV n knowledge base of size s, satisfiability of KB can be reduced to instance retrieval w.r.t. a set of Datalog rules of size proportional to sn and at most 4 variables per rule. If n is constant, the problem is P-complete. 5
An interesting feature of nominal schemas is that they can be used to express arbitrary DL-safe rules [14]. These are Datalog rules with unary and binary predicates that are restricted – just like nominal schemas – to apply to domain elements that are represented by individual names. Identifying unary predicates with concept names, binary predicates with role names, constants with individual names, and (DL-safe) variables with the variables in nominal schemas, the syntax of DL-safe rules can be based on a DL signature. As before, we assume the signature = hNI ; NC ; NR; NV i to be fixed and omit explicit references to it.
Definition 4. A concept atom is an expression of the form A(t) with t 2 T and A 2 NC [ f>; ?g. A role atom is an expression of the form R(s; t) with s; t 2 T and R 2 NR. An atom is a concept or role atom.
If B is a finite and non-empty conjunction of atoms and H is an atom, then B ! H is a DL-safe rule. B is called the body, and H is called the head. A DL-safe rule that contains at most n distinct variables is called an n-variable rule. A 0-variable rule is a ground rule. The grounding ground(B ! H) of a DL-safe rule B ! H is the set of all rules that can be obtained by uniformly replacing variables in B ! H with individual names of the signature.
An interpretation I satisfies a ground DL-safe rule B ! H, written I j= B ! H, if either I j= H or I 6j= B. An interpretation I satisfies a DL-safe rule B ! H if it satisfies all rules in ground(B ! H). A set of rules is satisfied if all of its elements are. Models, satisfiability, and entailment are defined as usual.
Definition 5. A syntactic transformation dl from atoms and DL-safe rules to SROIQV concepts and TBox axioms is defined as follows. For a unary atom A(t) and binary atom R(s; t), we set dl(A(t)) := 9U:(ftg u A) and dl(R(s; t)) := 9U:(fsg u 9R:ftg): Given a DL-safe rule B ! H, we set dl(B ! H) := dF 2B dl(F ) v dl(H), and for a set of DL-safe rules RB we define dl(RB) := SB!H2RB dl(B ! H).
the number of variables in the rule. This ensures that none of the restrictions on simple and non-simple roles or regularity are violated. In consequence, dl(RB) is a SROE LV n knowledge base if RB is a set of n-variable rules. The following result of [13] is not hard to show: Theorem 4. The models of a set RB of DL-safe rules are the same as the models of dl(RB), i.e. RB and dl(RB) are semantically equivalent.
to express arbitrary DL-safe rules. The use of nominal schemas, however, in
since the latter correspond to a special form of SROIQV axioms only. Combining Theorem 3 with the observation that dl(RB) is linear in the size of RB, we can state the following: Theorem 5. The problem of deciding whether a knowledge base RB [ KB is satisfiable, where RB is a set of n-variable rules with n constant, and KB is a SROE LV n knowledge base, is P-complete.
the use of nominal schemas supports the integration of DL-safe rules into DL knowledge bases. An important next step is to realize these ideas for the concrete serialization formats of these languages, and to make the corresponding modeling features available in practice.
to handle nominal schemas more efficiently. We have shown that our extension does not increase the worst-case complexity of reasoning in SROIQ, and that versatile tractable sublanguages exist. Whether and how these theoretical results can be put into efficient reasoning algorithms is an open research question.
hand, nominal schemas could be implemented by modifying/extending existing SROIQ implementations that have good support for nominals, such as the
On the other hand, our light-weight description logics could be implemented using rule-based procedures as proposed for SROE L [12]. In this setting, nominal schemas can be treated like DL-safe variables. Thus, the rule-based deduction remains similar with the only modification that some variables can only be instantiated with certain constants. Specifically, the approach in [12] introduces new constant symbols for eliminating existentials, and DL-safe variables must not be allowed to represent these auxiliary symbols.
In conclusion, the close relationship to nominals is not merely of syntactic convenience but prepares a path for the further practical adoption of this feature. Instead of a paradigm shift from ontologies to rules, existing applications could be augmented with bits of rule-based modeling to overcome restrictions of classical DLs. Nominal schemas thus may provide an opportunity for enhancing the expressive power of ontologies without giving up on established tools, formats, or methodologies.
gies” (EP/F065841/1). The third author acknowledges support by a Fulbright
2. de Bruijn, J.: RIF RDF and OWL Compatibility. W3C Recommendation (22 June
2010), available at http://www.w3.org/TR/rif-rdf-owl/
3. Demri, S., Nivelle, H.: Deciding regular grammar logics with converse through
first-order logic. J. of Logic, Language and Information 14(3), 289–329 (2005)
4. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Doherty,
P., Mylopoulos, J., Welty, C. (eds.) Proc. 10th Int. Conf. on Principles of Knowledge
Representation and Reasoning (KR’06). pp. 57–67. AAAI Press (2006)
5. Horrocks, I., Patel-Schneider, P., Bechhofer, S., Tsarkov, D.: OWL Rules: A
proposal and prototype implementation. J. of Web Semantics 3(
Artificial Intelligence 160(
Press/AKA (2010) 10. Krötzsch, M., Rudolph, S., Hitzler, P.: Description logic rules. In: Ghallab, M., et al. (eds.) Proceedings of the 18th European Conference on Artificial Intelligence, ECAI2008. pp. 80–84. IOS Press (2008) 11. Krötzsch, M., Rudolph, S., Hitzler, P.: ELP: Tractable rules for OWL 2. In: Sheth, A., et al. (eds.) Proceedings of the 7th International Semantic Web Conference (ISWC-08). Lecture Notes in Computer Science, vol. 5318, pp. 649–664. Springer (2008) 12. Krötzsch, M.: Efficient rule-based inferencing for OWL EL. In: Walsh, T. (ed.)
Proc. 22nd Int. Conf. on Artificial Intelligence (IJCAI’11). IJCAI (2011), to appear 13. Krötzsch, M., Maier, F., Krisnadhi, A.A., Hitzler, P.: A better uncle for OWL: Nominal schemas for integrating rules and ontologies. In: Proc. 20th Int. Conf. on World Wide Web (WWW’11). pp. 645–654. ACM (2011) 14. Motik, B., Sattler, U., Studer, R.: Query answering for OWL DL with rules. J. of
Web Semantics 3(
J. of Artificial Intelligence Research 36(