We consider CF Dnc, an alternative to the description logic CF D that retains the latter's ability to support PTIME reasoning in the presence of terminological cycles with universal restrictions over functional roles and also in the presence of functional constraints over functional role paths. In contrast, CF Dnc replaces the ability to have conjunction on left-hand-sides of inclusion dependencies with the ability to have primitive negation on right-hand-sides. This makes it possible to say that primitive concepts must denote disjoint sets of individuals, a common requirement with many information sources.
Scalability issues in reasoning over the semantic web have led the W3C to adopt two
description logic (DL) fragments of OWL 2 that are designed to ensure PTIME
complexity in the size of respective knowledge bases for a number of important reasoning
problems. Called profiles, the DLs are E L++ [
Toman and Weddell proposed an alternative to DL-Lite called CF D that was designed to provide better support for data sources based on relational schema that include more extensive collections of dependencies such as primary and foreign keys [22]. The paper showed that the problem of deciding concept subsumption in CF D had PTIME complexity, and therefore might qualify as a useful additional option for an OWL 2 profile. However, there are two problems with CF D that make it less attractive in this role: (1) unlike DL-Lite, it is not possible to say that two primitive concepts must denote disjoint sets of individuals or entities, a common requirement with many information sources, and (2) computing the certain answers to conjunctive queries is PSPACE-complete, even for queries of the form 9x:A(x), for A a primitive concept.
In this paper we introduce CF Dnc, an alternative to CF D that retains the latter’s key abilities: supporting terminological cycles with universal restrictions over functional roles, and supporting a rich variety of functional constraints over functional role paths. In particular, CF Dnc replaces the ability in CF D to have conjunction on lefthand-sides of inclusion dependencies with a new ability to have primitive negation on right-hand-sides (the same is also true for the original version of DL-Lite). This removes both problems with CF D. In particular, we show that the following fundamental reasoning problems are in PTIME. C ::= A j :A j C1 u C2 j 8 Pf :C
SEMANTICS: “( )I ” AI C1I \ C2I fx : PfI (x) 2 CI g j A : Pf1; : : : ; Pfk ! Pf fx : 8 y 2 AI : Vik=1 PfiI (x) = PfiI (y) ) PfI (x) = PfI (y)g
Fig. 1. CF Dnc CONCEPTS. 1. Knowledge base consistency: determining if at least one model exists for a given knowledge base; 2. Logical implication: determining if a given inclusion dependency is logically entailed by the terminological component of a given knowledge base; and 3. Instance checking: determining if a given concept assertion is entailed by a given knowledge base.
We also show that the problem of computing certain answers for arbitrary conjunctive queries over a CF Dnc knowledge base K is in PTIME in the size of K and is PSPACEcomplete for combined complexity, that is, when the size of a query is included.
Reasoning in DL-Lite, E L, and their variants often relies on the existence of
polynomially-sized canonical models (or canonical structures that closely resemble such
models) to address the above reasoning tasks [
We begin in the next section by introducing the syntax and semantics of CF Dnc and talk about some of its key features and limitations. The problems above are the focus of Section 4 in which we appeal to an automata-based method for their resolution. This method is introduced in Section 3 where we consider the simpler problem of concept satisfiability. Computing certain answers for conjunctive queries is considered in Section 5, and a review of related work and summary comments then follow in Sections 6 and 7, respectively. 2
The Description Logic CF Dnc A formal definition of CF Dnc knowledge bases and the above reasoning problems now follows. Observe that the logic is based on attributes or features instead of the more common case of roles which can denote arbitrary binary relations. However, this is not really a issue. Indeed, CF Dnc is ideal for expressing reification for predicates of arbitrary arity [19].
Definition 1 (CF Dnc Knowledge Bases) Let F, PC and IN be disjoint sets of (names of) attributes, primitive concepts and individuals, respectively. A path function Pf is a word in F with the usual convention that the empty word is denoted by id and concatenation by “:”. Concept descriptions are defined by the grammar on the left-hand-side of Metadata and data in a CF Dnc knowledge base K are respectively defined by a TBox TK consisting of a finite set of inclusion dependencies of the form A v C, and by an ABox AK consisting of a finite set of concept assertions of the form A(a) and path function assertions of the form Pf1(a) = Pf2(b), where A is a primitive concept, C an arbitrary concept, fPf1; Pf2g F and where fa; bg IN.
Semantics is defined in the standard way with respect to a structure (4; ( )I ), where 4 is a domain of “objects” and ( )I an interpretation function that fixes the interpretation of primitive concepts A to be subsets of 4, attributes f to be total functions on 4, and individuals a to be elements of 4. The interpretation is extended to path expressions by interpreting id , the empty word, as the identity function x:x, concatenation as function composition, and to derived concept descriptions C as defined on the right-hand-side for the remaining concept constructors.
An interpretation satisfies an inclusion dependency A v C if AI CI , a concept
assertion A(a) if aI 2 AI and a path function assertion Pf1(a) = Pf2(b) if Pf1I (aI ) =
Pf2I (bI ). An interpretation satisfies a knowledge base K if it satisfies each inclusion
dependency and assertion in K. 1
There are several reasoning problems for CF Dnc that shall concern us. Logical
implication asks if T j= A v C holds; that is, if A v C is satisfied by any interpretation
satisfying T . Knowledge base consistency asks if there exists at least one interpretation
for a give knowledge base K, and instance checking asks if K j= A(a) holds; that is, if
A(a) is satisfied by any interpretation that satisfies K. 2
(aside on notation) We write FK and PCK to denote all attributes and primitive concepts
occurring in K, respectively, and write: (1) ? as shorthand for A u :A, (2) a = b as
shorthand for id (a) = id (b), and (3) f (a) = b and shorthand for f (a) = id (b). Also
we elide any mention of subscripts in our notation when their presence is clear from
context. (end of aside)
The conditions imposed on PFDs in (1) distinguish, for example, PFDs of the form
C : f ! id and C : f ! g from PFDs of the form C : f ! g:h. This is necessary to
ensure PTIME complexity for reasoning problems in CF Dnc [
Observe that only atomic concepts can appear on the left-hand-side or as part of a PFD. Indeed, relaxing this assumption in some cases will lead to a loss of PTIME 1 Note that CF Dnc does not assume the unique name assumption, but that its ability to express disjointness enables mutual inequality between each pair of n individuals to be captured by introducing O(n) new atomic concepts, concepts assertions and inclusion dependencies in a straightforward way. complexity for at least one of the reasoning problems for CF Dnc, and remains an open issue for others. (See related work and our conclusions below.) 3
It is easy to see that every CF Dnc TBox T is consistent (by setting all primitive concepts to be interpreted as the empty set). However, for other reasoning tasks such as concept satisfiability and knowledge base consistency, it is convenient to assume by default, and without loss of generality, that CF Dnc knowledge bases are given in a normal form.
ists an equivalent TBox T 0 that adheres to the following (more limited) grammar for CF Dnc concept descriptions.
C ::= A j :A j 8f:A j A : Pf1; : : : ; Pfk ! Pf Also, for every ABox A, there exists an equivalent ABox A0 containing only assertions of the form f (a) = b and a = b. 2 Obtaining T 0 and A0 from an arbitrary knowledge base K is achieved by a straightforward introduction of auxiliary names for intermediate concept descriptions and individuals (e.g., see defn. of simple concepts in [21]).
We define a transition relation (T ) over the set of states S = PC [ f:A j A 2 PCg and the alphabet F as follows:
A1 !f A2 2 (T ) if A1 v 8f:A2 2 T where is the empty letter transition.
A1 ! A2 2 (T ) if A1 v A2 2 T A1 ! :A2 2 (T ) if A1 v :A2 2 T 2 The transition relation will allow us to construct non-deterministic finite automata (NFA) that can be used for various reasoning problems that relate to a CF Dnc TBox T . Note that we also follow common practice in automata theory and use for the empty letter in transition relations.2 Lemma 4 Let M = (S; fAg; fBg; (T )) be an NFA with the set of states S, start state A, final state B, and transition relation (T ). Then T j= A v 8 Pf :B whenever Pf 2 L(M ).
A = A0 !l1 A1 !l2 A2
Ak 1 !lk Ak = B 2 Another option would have been to use id for this purpose, but we thought, on balance, that this would hinder readability. in M where li 2 F [ f g and such that Pf = l1:l2: of (T ) that Ai 1 !li Ai exists if Ai 1 v Ai, for li = , or Ai 1 v 8li:Ai, for li 2 F (and hence these dependencies are trivially implied by T ). The claim then follows by simple transitive reasoning, all necessary cases derive from the fact that :lk. It follows from the definition fB1 v 8 Pf :B2; B2 v 8 Pf0 :B3g j= B1 v 8 Pf : Pf0 :B3; and by induction on the length of the run. 2 Note that the converse implication in this lemma may not hold, such as when A is inconsistent with respect to T .
The problem of concept satisfiability asks, for a given concept C and TBox T , if there exists an interpretation I for T in which CI is non-empty. Such problems can be reduced to the case where C is a primitive concept A by simply augmenting T with fA v Cg, where A is a fresh primitive concept.
Given a primitive concept A and TBox T , one can test for primitive concept satisfiability by using the following NFA, denoted nfaaB(T ; fA(a)g):
(S [ fag; fag; fBg; (T ) [ fa ! Ag); with states given by primitive concepts, their negations, and a distinguished node a, with start state a, with final state B 2 S, and with transition relation (T ) [ fa ! Ag. Theorem 5 (Concept Satisfiability) A is satisfiable with respect to the TBox T if and only if
L(nfaaB(T ; fA(a)g)) \ L(nfaa:B(T ; fA(a)g)) = ; for every B 2 PC.
Proof (sketch) For a primitive concept B 2 PC, a word Pf in the intersection language of the two automata above is a witness of the fact that PfI (aI ) 2 BI and PfI (aI ) 2 :BI must hold in every model of T , for reasons analogous to the proof of Lemma 4, which leads to a contradiction since Pf is a (total) function.
Conversely, if no such word exists then one can construct a deterministic finite automaton from nfaaB(T ; fA(a)g), using the standard subset construction, in which no state containing both B and :B is reachable from the start state fag. Unfolding the transition relation of this automaton, starting from the state fag, labelling nodes by the concepts associated with the automaton’s states, and adding missing features to complete trees in which no primitive concept is true for any node, yields a tree interpretation that satisfies T (in particular in which all PFD constraints are satisfied vacuously) and whose root a provides a witness for consistency of A. 2 Since all the automata operations run in PTIME we immediately get the following result.
Corollary 6 Concept satisfiability with respect to CF Dnc TBoxes is in PTIME. Note it is not possible to precompute all inconsistent classes for an arbitrary C since that would require consideration of all possible types over PC (i.e., finite subsets of primitive concepts), a process essentially equivalent to constructing the deterministic automaton used in the proof of Theorem 5, and in turn make the procedure exponential.
The automata-based approach to concept satisfiability can be extended to the more general problem of knowledge base consistency. Intuitively, each ABox individual a must be linked to the TBox automaton in a fashion similar to how the “prototypical object” a was linked in Section 3. This idea leads to the following definition:
We create a transition relation (A) for an nfa over the set of states S = PC [ fa j a in Ag and the alphabet F as follows: a ! a 2 (A) if a appears in A; a ! A 2 (A) if A(a) 2 A;
f a ! b 2 (A) if f (a) = b 2 A and a ! b; b ! a 2 (A) if a = b 2 A: where is the empty letter transition. 2 Observe that we have used transitions to simulate equality assertions in A. This is justified, e.g., by considering the ABox individuals to be nominals. (aside on notation) Hereon, we write “n ;Pf m in ” if Pf 2 L(nfa(S; fmg; fng; )), where S will be some set of states (that will be clear from the context), where m and n will be two states in S, and where will denote a NFA transition relation over S (that will also be clear from context). (end of aside) Unfortunately, taking (T ) [ (A) alone as the transition relation of an NFA and then testing for consistency of every ABox individual (as in Theorem 5) is not sufficient as the following cases illustrate. The problems raised by each case will be addressed by defining rules that impose conditions on a transition relation.
To begin, we need to ensure that ABox assertions f (a) = b are functional: Example 8 (Path Function Assertions) Consider the ABox A = ff (a) = b; f (a) = cg. Clearly bI must equal cI in any model I of a knowledge base that includes A. 2 To remedy this, we define a functionality rule for the transition relation (T ; A) as follows: if a ;f b and a ;f c in (T ; A) then fb ! c; c ! bg (T ; A).
Next, we need to ensure that ABox assertions of the form f (a) = b are coherent with TBox assertions A v 8f:B with respect to concept memberships of a and b: Example 9 (ABox and Value Restrictions) Consider the TBox T = fA v 8f:Bg and an ABox A = ff (a) = b; A(a)g. Clearly, in any model I of the knowledge base (T ; A), bI must be an element of BI . However, B cannot be reached from b in (T ) [ (A), and therefore an automaton based on this transition relation alone cannot reflect the correct concept membership of b. 2 We define a coherence rule for the transition relation (T ; A) to remedy this as follows: if a ;f b, a ; A, and A ; B in (T ; A) then b ! B 2 (T ; A).
f And finally, consider that tree interpretations, such as the one we used to show concept consistency in Theorem 5, vacuously satisfy all PFDs in T , but that this is not necessarily the case for a given ABox A.
Example 10 (ABox and PFDs) Consider A = fA(a); B(b); f (a) = c; f (b) = cg. – A TBox T = fA v B : f ! id g implies that the individuals a and b must denote the same domain element. – A TBox T = fA v B : f ! gg implies that there must be an additional (anonymous) individual d such that g(a) = d and g(b) = d.
Note that the PFD A v B : f:g ! id is also violated by the pair of individuals a and b, this despite the fact that neither of these two individuals is the origin of an explicit f:g path in A: since features are interpreted as total functions, individual c must have an “outgoing” g feature, and therefore a and b must agree on f:g. 2 A remedy for these cases is obtained by defining a PFD closure rule for the transition relation (T ; A) for each PFD A v B : Pf1; : : : ; Pfk ! Pf 2 T : The rule will refer to the following auxiliary functions. match(a; b; Pf; (T ; A)): Returns true if there is a (possibly empty) prefix Pf0 of Pf such that a P;f0 c and b P;f0 c in (T ; A) for some individual c; it returns false otherwise. expf(a; Pf; (T ; A)): Returns the minimal set of transitions (by creating new individuals) such that a ;Pf c in (T ; A) holds for some c. mkeq(a; b; Pf; (T ; A)): Returns fc ! d; d ! cg where, for some individuals c and d, we have a ;Pf c and b ; d in (T ; A).
Pf The PFD closure rule is then defined as follows: if fa ; A; b ; Bg (T ; A) and
match(a; b; Pfi; (T ; A)), for 0 < i k, and not match(a; b; Pf; (T ; A)) then expf(a; Pf; (T ; A)) (T ; A), expf(b; Pf; (T ; A)) (T ; A), and mkeq(a; b; Pf; (T ; A)) (T ; A) The rules enable one to define a transition relation for an NFA that captures reasoning in the knowledge base (T ; A) as follows.
relation containing (T ) and (A) that is closed under the functionality, coherence, and the PFD closure rules. 2 Note that (T ; A) is constructed by applying the closure rules to (T ) [ (A). Since this process is monotonic, it is sound to check for the preconditions of the rules in the partially completed (T ) [ (A). We use (T ; A) as the transition function for the NFA nfaaB(T ; A) with the start state fag and final state B (similarly to Section 3).
if and only if
L(nfaaB(T ; A)) \ L(nfaa:B(T ; A)) is empty for all primitive concepts B 2 PC and all ABox individuals a in A. Proof (sketch) Assume Pf 2 L(nfaaB(T ; A)) \ L(nfaa:B(T ; A)) for some path function Pf, individual a and primitive concept B, and that I j= (T ; A). Composing all the assertions corresponding to the transitions in (T ; A) along the runs corresponding to Pf in the two automata, however, implies that PfI (aI ) 2 BI and PfI (aI ) 2 :BI (similarly to Lemma 4); a contradiction as interpretations of path functions are functional.
For the other direction we define an interpretation I as follows: let dae be an representative of the equivalence class fa j a ; b; b ; a in (T ; A)g and let PF(a) denote ff: Pf j a ;f b not in (T ; A)g for any individual bg: Then set – 4I = Sa in Afdae: id g [ fdae: Pf j Pf 2 PF(a)g; – aI = dae: id ; – AI = fdae: Pf j a ;Pf A in (T ; A)g; and – f I = f(dae: id ; dbe: id ) j a ;f b in (T ; A)g [
f(dae: Pf; dbe: Pf :f ) j dae: Pf; dae: Pf :f 2 4I g: It is immediate that I j= A since (A) (T ; A) and we corrected for all violations of PFDs. By inspecting inclusion dependencies in T it is also easy to see that I j= T . 2 Note that the core of this construction is again the subset construction for NFA determinization (cf. Theorem 5) where the TBox-ABox interactions are facilitated by the closure rules. What remains is to show that knowledge base consistency can be checked in PTIME.
Proof (sketch) The number of individuals in (T ; A) is bounded by jAj + 2jT jjAj2 since the PFD closure rule can add at most two new individuals per pair of individuals in A and PFD in T . Thus, since the number of states is polynomial in jT j + jAj, the number of transitions in (T ; A) is also at most polynomial in jT j + jAj. 2 Taken together with the argument we made for concept consistency with respect to a TBox yields PTIME algorithm for KB consistency. Since we do not assume the unique name assumption, the problem is also PTIME-hard (we have Horn-SAT embedded in reasoning with the PFDs alone).
Corollary 14 Knowledge base consistency for CF Dnc is PTIME-complete. Now we consider the questions of logical implication of the form (T ; A) j= C(a), (T ; A) j= Pf1(a) = Pf2(b), and ultimately T j= A v C. Since C can be a complex concept and CF Dnc is not closed under negation, logical implication must be resolved by asking several separate questions by exhaustively applying the following simplification rules:
Simp(C) ! fCg Simp(8 Pf :C1 u C2) ! Simp(8 Pf :C1) [ Simp(8 Pf :C2)
Simp(8 Pf :8 Pf0 :C1) ! Simp(8 Pf : Pf0 :C1) where C is one of the irreducible concepts of the forms 8 Pf :A, 8 Pf ::A, and 8 Pf :A : Pf1; : : : ; Pfk ! Pf0. We call the irreducible concepts obtained by these rules the simplifications of the given concept.
Lemma 15 (T ; A) j= C(a) (T j= A v C) if and only if (T ; A) j= D(a) (T j= A v D, respectively) for all D 2 Simp(C).
Proof (sketch) implication.
By observing that the each step of simplifications preserves logical 2 The simplified logical implication questions can now be reduced in a natural way to CF Dnc knowledge base satisfiability as follows: Theorem 16 (Instance Checking) 1. (T ; A) j= 8 Pf :A(a) iff (T ; A [ f8 Pf ::A(a)g) is not satisfiable. 2. (T ; A) j= 8 Pf ::A(a) iff (T ; A [ f8 Pf :A(a)g) is not satisfiable. 3. (T ; A) j= (8 Pf :A : Pf1; : : : ; Pfk ! Pf0)(a) iff (T ; A [ fPf(a) = b; A(c); D(Pf0(b)); :D(Pf0(c)g [ [ fPfi(b) = Pfi(c)g) 0<i k is not satisfiable, where b and c are fresh individual names and D is a fresh primitive concept. 4. (T ; A) j= (Pf1(a) = Pf2(b)) iff (T ; A [ fD(Pf1(a)); :D(Pf2(b))g is not satisfiable, where D a fresh primitive concept. 2 For logical implication questions of the form T j= A v C, where C is irreducible, simply replace the ABox A in the above by fA(a)g. The results then follow by virtue of the first three cases in the preceding theorem. Overall, we have the following: Corollary 17 Both instance checking and logical implication for CF Dnc are in PTIME. 5
We assume the standard definition of conjunctive queries, and begin by considering queries of the form
9x:(A1(x) ^ : : : ^ Ak(x)): It turns out that such queries are the overriding source of complexity in computing certain answers over CF Dnc knowledge bases.
Lemma 18 Let (T ; A) be a consistent CF Dnc knowledge base and q a conjunctive query of the form 9x:(A1(x) ^ : : : ^ Ak(x)), where Ai are primitive concept names. The question (T ; A) j= q is PSPACE-hard (in combined complexity) and in PTIME in jT j + jAj.
Proof (sketch) It is sufficient to show that in every model I of (T ; A) there is a object o 2 4I such that o 2 AiI for all 0 < i k. We set
A0 = A [ ffi(s) = ai j ai an individual in Ag where s and fi do not appear in T and A and an NFA
M = nfasA1 (T ; A0) : : : nfasAk (T ; A0): The remainder of the argument is similar to the concept consistency proof (Theorem 5), namely L(M ) 6= ; if and only if (T ; A) j= q: – If (T ; A) j= q then, in every model I of (T ; A), there must be an ABox individual ai and a path function Pf such that PfI (aiI ) 2 AjI for all 0 < j k. Then, however, it is easy to verify that fi: Pf 2 L(M ) by analysis of the definition of M ; – Conversely, if fi: Pf 2 L(M ), then, in every model I of (T ; A) and every 0 < j k, it follows that PfI (aiI ) 2 AjI since fi: Pf 2 L(nfasAj (T ; A0)), and, by the definition of M , that Pf 2 L(nfaaAij (T ; A)).
Note that every word in L(M ) must start with one of the fi features, thus ensuring that a common individual is used.
The complexity bounds then follow from well known results in automata theory (the
DFA intersection problem, [
PFDs in CF Dnc were first introduced and studied in the context of graph-oriented
data models such as RDF and its refinements [
We also mentioned earlier that relaxing the syntactic restrictions for left-hand sides of inclusion dependencies often causes the loss of PTIME complexity for some of the reasoning problems of CF Dnc. Here are three cases worth noting.
– Allowing conjunction “u” yields the logic CF D? and therefore makes logical
implication PSPACE-complete [22].
– Allowing conjunction and value restriction “8” makes logical implication
EXPTIMEcomplete [
In [
We have presented the DL logic CF Dnc, a variation on the logic CF D with the following notable properties.
– CF Dnc retains what we believe are the most important features of CF D: its ability to capture terminological cycles with universal restrictions over functional roles and its ability to capture a rich variety of functional constraints over functional role paths. – In contrast to CF D, the logic adds an ability to express disjointness of atomic concepts. – Also in contract to CF D, the logic supports important reasoning services in PTIME: determining knowledge base consistency, deciding logical implication and instance checking.
There are a number of open issues and directions for continued research. The consequences of allowing CF Dnc concept constructors other that conjunction on the lefthand-side of inclusion dependencies is, to the best of our knowledge, open. In particular, this includes values restrictions “8”, negated primitive concepts “:A” and PFDs.
One enhancement to CF Dnc that we believe is straightforward, and that would considerably enhance its utility for modelling RDF data sources, would be to allow roles and role inclusion axioms of either the form “f v R” or the form “R1 v R2” to be included in CF Dnc TBoxes, and then to allow roles to be mentioned in conjunctive queries. We conjecture that allowing E L role constructors on right-hand-sides of inclusion dependencies in CF Dnc would also be possible without damage to its PTIME capabilities. 19. David Toman and Grant Weddell. On Reasoning about Structural Equality in XML: A Description Logic Approach. Theoretical Computer Science, 336(1):181–203, 2005. 20. David Toman and Grant Weddell. On the Interaction between Inverse Features and Pathfunctional Dependencies in Description Logics. In Proc. Int. Joint Conf. on Artificial Intelligence (IJCAI), pages 603–608, 2005. 21. David Toman and Grant Weddell. On Keys and Functional Dependencies as First-Class Citizens in Description Logics. In Proc. of Int. Joint Conf. on Automated Reasoning (IJCAR), pages 647–661, 2006. 22. David Toman and Grant E. Weddell. Applications and extensions of ptime description logics with functional constraints. In Proc. Int. Joint Conf. on Artificial Intelligence (IJCAI), pages 948–954, 2009. 23. Grant Weddell. A Theory of Functional Dependencies for Object Oriented Data Models.
In International Conference on Deductive and Object-Oriented Databases, pages 165–184, 1989.