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.
A significant body of work has developed investigating the integration of description logics (DLs) and rule languages (typically Datalog). Conceptually, one can distinguish two approaches. On the one hand, description logics have been extended with additional "description-logic-style" expressive features which make it possible to express certain types of rules. For instance, SROIQ role inclusion axioms (RIAs) can be viewed as a type of rule. By combining RIAs with local reflexivity (Self) and the universal role U , many rules with a tree-shaped body can be expressed indirectly [10]. The restriction to tree-shaped rules ensures decidability, but it also excludes many rules. An example is the following rule that defines a concept C of children whose parents are married: hasParent(x,y) ∧ hasParent(x,z) ∧ married(y,z) → C(x).
(
On the other hand, there are approaches of a hybrid nature, in the sense 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 Interchange Format RIF (even when restricted to RIF Core) [1,2]. A prominently 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].
In this paper, we expand on the above idea and improve it in several ways. The key technical innovation is the introduction of nominal schemas as new 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 DL-safe variables are tied to rule languages, while nominal schemas integrate 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.
To give an initial example, consider again the rule (1) extended by the axioms hasParent(mary, john)
(∃hasParent.∃married.{john})(mary)
Axiom (2) asserts that John is a parent of Mary, while axiom (3) states that 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 (1) would thus entail that Mary belongs to the class C. Interpreting rule (1) as DL-safe, however, does not allow this conclusion, since John's spouse is not named by any constant in the ontology. To retain the conclusion, one can weaken this restriction to require only z to be DL-safe, while x and y can still take arbitrary values. This is possible in the rule-based approach of DL+safe Rules, but cannot be captured in an axiom of existing description logics. In contrast, using nominal schemas, rule (1) can be expressed as ∃hasParent.{z} ∃hasParent.∃married.{z} C.
The desired conclusion again follows. The expression {z} is a nominal schema, 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.
The main contributions of this paper are as follows:
1. We introduce nominal schemas as a new general constructor for description logics, denoted by the letter V in the DL nomenclature, and define the expressive DL SROIQV as an extension of SROIQ. 2. We establish the worst-case complexity of reasoning in SROIQV to be N2ExpTime-complete, and thus not harder than for SROIQ.
3. We define SROELV n (n ≥ 0) as a new family of DLs with nominal schemas for which reasoning is possible in polynomial time.
The expressivity of nominal schemas is also witnessed by the fact that it 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 SROELV 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 SROELV 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 this paper, we introduce the syntax and semantics of nominal schemas for SROIQV, and establish the worst-case complexity of reasoning in Section 2. The DLs SROELV n are introduced in Section 3, and their tractability is established in Section 4. In Section 5 we show how DL-safe rules can be expressed with nominal schemas, and Section 6 concludes.
We start by introducing nominal schemas as an extension of existing description logics. We first generally introduce the feature for SROIQ to obtain the very expressive DL SROIQV.
A signature of SROIQV is a tuple Σ = N I , N C , N R , N V 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:
where k is a natural number, and R (S) is a (simple) SROIQ role as usual. We use U to denote the universal role. The common axiom types are defined as 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 {z} 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.
The semantics of SROIQV is defined by interpreting variables as placeholders for named individuals, i.e. elements of the interpretation domain that are represented by individual names in N I . 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) := α∈KB ground(α).
A DL interpretation I is a model of a SROIQV axiom α, written I |= α, 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.
Note that grounding does not affect the structural restrictions of simplicity 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].
We first recall the complexity proof of [8] which is based on an exponential reduction of DL knowledge bases to theories of C 2 , 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: (1) axioms are transformed into a simplified normal form, (2) complex RIAs are eliminated, and (3) the resulting axioms are expressed as formulae of C 2 .
Step (1) yields an equisatisfiable knowledge base that contains only axioms of the following forms:
C}. This normalization can be done in linear time; see [8] for details. The only axioms that are not readily expressed in C 2 are complex RIAs. They are eliminated next, with exponential effort.
Step (2) applies a technique from [3] using nondeterministic finite automata (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 ∈ R, there is an NFA A R over the alphabet N R such that for every model I of KB, and for every word S 1 . . . S n accepted by A R :
i for all i = 1, . . . , n, then δ 1 , δ n+1 ∈ R I . Moreover, let ≺ denote a strict linear order that witnesses regularity of KB as required in [4]. For each non-simple R ∈ N R , the number of states of A R is bounded exponentially in the depth of KB that is defined as:
It suffices to construct the respective NFA for non-simple roles. Now step (2) proceeds by replacing every axiom of the form A ∀R.B by the following set of axioms, where A R is the NFA as introduced above, and X q are fresh concept names for each state q of A R :
A X q q is the initial state of A R X q ∀S.X q A R has a transition q S → q X q B q is a final state of A R Moreover, all complex RIAs of the form
The number of new axioms (and fresh concept names) that are introduced for each axiom of the form A ∀R.B is bounded by the sum of the number of states and transitions in A R , 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 ∀R.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 C 2 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.
Proof. The depth of KB is only affected by RBox axioms. RBox axioms are not affected by grounding, hence the depth of ground(KB) is equal to the depth of KB.
Since ground(KB) is in SROIQ, one can apply the transformation steps (1)-( 3). This yields a C 2 theory T that is equisatisfiable to ground(KB) [8] and thus to KB. The size of T is linear in the size of ground(KB) and exponential in the depth of KB. Both measures are exponential in the size of KB, and so is T . Deciding satisfiability of T can be done in NExpTime [17], thus deciding satisfiability of KB in N2ExpTime.
Hardness follows since SROIQV includes SROIQ, for which deciding satisfiability is N2ExpTime-hard [8].
The result that reasoning in SROIQV has the same worst-case complexity as 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.
Concretely, we define DLs SROELV n for each integer n ≥ 0, n restricting the number of "problematic" occurrences of nominal schemas detailed below. The DLs are based on the tractable DL SROEL(×), introduced as an extension of OWL EL [12]. In essence, SROEL(×) is an extension of EL with , ⊥, nominals, 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 × 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) is not tree-shaped since there are parallel paths x R → z and x S → y T → 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 ∃R.{z} ∃S.(B ∃T.{z}).
Here, we do not introduce tree-shaped dependency structures as a general 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. This means that nominals (our syntax for constants) disconnect a concept's dependency structure. For instance, if B in the above rule body is replaced by a nominal {a}, then the concept would be tree-shaped. In such a case, we say that the nominal {z} occurs in a safe environment, as defined next. Definition 2. An occurrence of a nominal schema {x} in a concept C is safe if C has a sub-concept of the form {a} ∃R.D for some a ∈ N I , such that D contains the occurrence of {x} but no other occurrence of any nominal schema. In this case, {a} ∃R.D is a safe environment for this occurrence of {x}. S(a, x) will sometimes be used to denote an expression of the form {a} ∃R.D within which {x} occurs safely.
A nominal schema {x} is safe for a SROIQV TBox axiom C D if {x} does not occur in D, and at most one occurrence of {x} in C is not safe. Definition 3. Let n ≥ 0. A SROELV n concept is a SROIQV concept that may contain , ⊥, , ∃, Self, the universal role, nominals and nominal schemas, but which does not contain , ¬, ∀, k , k , or inverse roles.
A SROELV n TBox axiom is a SROIQV TBox axiom α that uses SROELV n concepts only, and where at most n nominal schemas are not safe for α. An RBox axiom of SROELV n is an RBox axiom of SROIQV that does not contain inverse roles. A SROELV n knowledge base is a SROIQV knowledge base that contains only SROELV n axioms.
Restricting to at most n non-safe nominal schemas per axiom ensures that at most |N I | n 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 SROELV 1 axiom.
If n is constant, the problem of checking satisfiability in SROELV 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 SROEL(×) [12].
Let KB be a SROELV n knowledge base. We define a SROEL(×) knowledge base ground + (KB) as follows. The RBox and ABox of ground + (KB) are the same as the RBox and ABox of KB. For each TBox axiom α = C D ∈ KB, the following axioms are added to ground + (KB):
1. For each nominal schema {x} safe for α, with safe occurrences in environments S i (a i , x) for i = 1, . . . , l, introduce a fresh concept name O x,α . For every individual b ∈ N I in KB, ground + (KB) contains an axiom As shown in [13], a SROELV n knowledge base KB is satisfiable if and only if ground + (KB) is satisfiable. A knowledge base is unsatisfiable if and only if it entails {a} ⊥ for arbitrary a ∈ N I . This reduces satisfiability testing to instance retrieval (checking if a is an instance of ⊥). Using the polynomial time instance retrieval method for SROEL(×) from [12], we thus obtain the following result. Hardness for P follows from the hardness of SROEL(×). Theorem 3. If KB is a SROELV 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 s n and at most 4 variables per rule. If n is constant, the problem is P-complete.
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 Σ = N I , N C , N R , N V to be fixed and omit explicit references to it. The set of terms T of Σ is N I ∪ N V . Definition 4. A concept atom is an expression of the form A(t) with t ∈ T and A ∈ N C ∪ { , ⊥}. A role atom is an expression of the form R(s, t) with s, t ∈ T and R ∈ N R . 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 Since DL-safe rules use the same models as SROIQV, it is easy to combine DL-safe rules and DL knowledge bases. The entailment relation is immediate: a DL-safe rule or DL axiom ϕ is entailed by a DL knowledge base KB extended with a set of rules RB if ϕ is satisfied by all interpretations that satisfy both KB and RB. The function dl transforms rules into SROELV n TBox axioms, where n is 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 SROELV 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.
Importantly, this result confirms that nominal schemas are powerful enough to express arbitrary DL-safe rules. The use of nominal schemas, however, in SROIQV is more general than the extension of SROIQ with DL-safe rules, 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 SROELV n knowledge base, is P-complete.
We have introduced nominal schemas as an extension to description logics, giving DLs sufficient expressivity to incorporate rule-based modeling. In particular, 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.
The latter task especially includes the implementation of inference algorithms 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. Two different approaches to addressing this problem appear viable. On the one hand, nominal schemas could be implemented by modifying/extending existing SROIQ implementations that have good support for nominals, such as the OWL 2 reasoner HermiT [15]. This can be accomplished by treating nominal schemas like nominals in the deduction procedure, instantiating them with concrete individuals only when this enables relevant deduction steps. This can be viewed as a method of deferred grounding.
On the other hand, our light-weight description logics could be implemented using rule-based procedures as proposed for SROEL [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.
Acknowledgements This work was partially supported by the National Science Foundation under award 1017225 "III: Small: TROn-Tractable Reasoning with Ontologies" and by EPSRC in project "HermiT: Reasoning with Large Ontologies" (EP/F065841/1). The third author acknowledges support by a Fulbright Indonesia Presidential Scholarship PhD Grant 2010.