=Paper=
{{Paper
|id=None
|storemode=property
|title=CFDnc: A PTIME Description Logic with Functional Constraints and Disjointness
|pdfUrl=https://ceur-ws.org/Vol-1014/paper_65.pdf
|volume=Vol-1014
|dblpUrl=https://dblp.org/rec/conf/dlog/TomanW13
}}
==CFDnc: A PTIME Description Logic with Functional Constraints and Disjointness==
<pdf width="1500px">https://ceur-ws.org/Vol-1014/paper_65.pdf</pdf>
<pre>
            CF Dnc: A PTIME Description Logic
         with Functional Constraints and Disjointness

                             David Toman and Grant Weddell

                           Cheriton School of Computer Science
                             University of Waterloo, Canada
                        {david,gweddell}@cs.uwaterloo.ca


       Abstract. We consider CFDnc, an alternative to the description logic CFD that
       retains the latter’s ability to support PTIME reasoning in the presence of termi-
       nological cycles with universal restrictions over functional roles and also in the
       presence of functional constraints over functional role paths. In contrast, CFDnc
       replaces the ability to have conjunction on left-hand-sides of inclusion dependen-
       cies 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.


1   Introduction
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 com-
plexity in the size of respective knowledge bases for a number of important reasoning
problems. Called profiles, the DLs are EL++ [2] and DL-Lite [1, 6, 7]. Medical ontolo-
gies were an important motivation for the former, whereas the latter was heavily influ-
enced by a need to access information residing in data sources conforming to relational
schema, particularly in cases where the schema has been derived via ER modelling.
    Toman and Weddell proposed an alternative to DL-Lite called CF D that was de-
signed to provide better support for data sources based on relational schema that in-
clude 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 ∃x.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 func-
tional 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 left-
hand-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 re-
moves both problems with CF D. In particular, we show that the following fundamental
reasoning problems are in PTIME.
S YNTAX                          S EMANTICS : “(·)I ”

C ::= A                          AI ⊆ 4
    | ¬A                         4 \ AI
    | C1 u C2                    CI1 ∩ CI2
    | ∀ Pf .C                    {x : Pf I (x) ∈ CI }
                                                     Vk
    | A : Pf 1 , . . . , Pf k → Pf {x : ∀ y ∈ AI .    i=1
                                                            Pf Ii (x) = Pf Ii (y) ⇒ Pf I (x) = Pf I (y)}


                                    Fig. 1. CFDnc C ONCEPTS .


 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 en-
    tailed 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 PSPACE-
complete for combined complexity, that is, when the size of a query is included.
    Reasoning in DL-Lite, EL, and their variants often relies on the existence of poly-
nomially-sized canonical models (or canonical structures that closely resemble such
models) to address the above reasoning tasks [14, 16]. It is worth noting that CF Dnc
does not share this property: an equivalent of a canonical model for a CF Dnc knowl-
edge base is necessarily exponential in the size of the knowledge base.
    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 Sec-
tion 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 concate-
nation by “.”. Concept descriptions are defined by the grammar on the left-hand-side of
Figure 1 in which occurrences of “A” denote primitive concepts. A concept produced
by the “A : Pf 1 , . . . , Pf k → Pf” production of this grammar is called a path functional
dependency (PFD). In addition, any occurrence of a PFD must adhere to one of the fol-
lowing two forms:

                         1. A : Pf 1 , . . . , Pf . Pf i , . . . , Pf k → Pf or
                                                                                            (1)
                         2. A : Pf 1 , . . . , Pf . Pf i , . . . , Pf k → Pf .f
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 Pf 1 (a) = Pf 2 (b), where A is a primitive concept, C an
arbitrary concept, {Pf 1 , Pf 2 } ⊆ F∗ and where {a, b} ⊆ 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 ∈ AI and a path function assertion Pf 1 (a) = Pf 2 (b) if Pf I1 (aI ) =
Pf I2 (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 impli-
cation asks if T |= 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 |= 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 [13] and does not impact
the modelling utility of CF Dnc for formatted legacy data sources. It remains possible,
for example, to capture arbitrary keys or functional dependencies in a relational schema.
    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 CFDnc 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     TBox and Concept Satisfiability

It is easy to see that every CF Dnc TBox T is consistent (by setting all primitive con-
cepts 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.

Lemma 2 (TBox and ABox Normal Forms) For every CF Dnc TBox T , there ex-
ists an equivalent TBox T 0 that adheres to the following (more limited) grammar for
CF Dnc concept descriptions.
                    C ::= A | ¬A | ∀f.A | A : Pf 1 , . . . , Pf k → 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 straightfor-
ward introduction of auxiliary names for intermediate concept descriptions and individ-
uals (e.g., see defn. of simple concepts in [21]).

Definition 3 (A Transition Relation for T ) Let T be a CF Dnc TBox in normal form.
We define a transition relation δ(T ) over the set of states S = PC ∪ {¬A | A ∈ PC}
and the alphabet F as follows:
                                 
                            A1 → A2 ∈ δ(T ) if A1 v A2 ∈ T
                              
                           A1 → ¬A2 ∈ δ(T ) if A1 v ¬A2 ∈ T
                                 f
                          A1 → A2 ∈ δ(T ) if A1 v ∀f.A2 ∈ T
where  is the empty letter transition.                                                      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, {A}, {B}, δ(T )) be an NFA with the set of states S, start
state A, final state B, and transition relation δ(T ). Then T |= A v ∀ Pf .B whenever
Pf ∈ L(M ).
Proof (sketch) For Pf ∈ L(M ) there must be a run
                                 1   l2   l           k    l
                          A = A0 → A1 → A2 · · · Ak−1 → 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 ∈ F ∪ {} and such that Pf = l1 .l2 . · · · .lk . It follows from the definition
                    li
of δ(T ) that Ai−1 →   Ai exists if Ai−1 v Ai , for li = , or Ai−1 v ∀li .Ai , for li ∈ 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
               {B1 v ∀ Pf .B2 , B2 v ∀ Pf 0 .B3 } |= B1 v ∀ Pf . Pf 0 .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
{A v C}, where A is a fresh primitive concept.
    Given a primitive concept A and TBox T , one can test for primitive concept satisfi-
ability by using the following NFA, denoted nfaaB (T , {A(a)}):
                                                            
                          (S ∪ {a}, {a}, {B}, δ(T ) ∪ {a → A}),
with states given by primitive concepts, their negations, and a distinguished node a,
                                                                                    
with start state a, with final state B ∈ S, and with transition relation δ(T ) ∪ {a → A}.

Theorem 5 (Concept Satisfiability) A is satisfiable with respect to the TBox T if and
only if
              L(nfaaB (T , {A(a)})) ∩ L(nfaa¬B (T , {A(a)})) = ∅
for every B ∈ PC.
Proof (sketch) For a primitive concept B ∈ PC, a word Pf in the intersection language
of the two automata above is a witness of the fact that Pf I (aI ) ∈ BI and Pf I (aI ) ∈
¬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 automa-
ton from nfaaB (T , {A(a)}), using the standard subset construction, in which no state
containing both B and ¬B is reachable from the start state {a}. Unfolding the transition
relation of this automaton, starting from the state {a}, 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 re-
sult.

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.
4   ABox Reasoning
The automata-based approach to concept satisfiability can be extended to the more gen-
eral 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:

Definition 7 (A Transition Relation for A) Let A be a CF Dnc ABox in normal form.
We create a transition relation δ(A) for an nfa over the set of states S = PC ∪ {a |
a in A} and the alphabet F as follows:
                                
                             a → a ∈ δ(A) if a appears in A,
                               
                             a → A ∈ δ(A) if A(a) ∈ A,
                                f
                               a → b ∈ δ(A) if f (a) = b ∈ A and
                                
                      a → b, b → a ∈ δ(A) if a = b ∈ 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.
                                           Pf
(aside on notation) Hereon, we write “n ; m in δ” if Pf ∈ L(nfa(S, {m}, {n}, δ)),
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 = {f (a) = b, f (a) =
c}. 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:
         f          f                               
    if a ; b and a ; c in δ(T , A) then {b → c, c → b} ⊆ δ(T , A).
Next, we need to ensure that ABox assertions of the form f (a) = b are coherent with
TBox assertions A v ∀f.B with respect to concept memberships of a and b:

Example 9 (ABox and Value Restrictions) Consider the TBox T = {A v ∀f.B}
and an ABox A = {f (a) = b, A(a)}. 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:
         f                             f                
    if a ; b, a ; A, and A ; B in δ(T , A) then b → B ∈ δ(T , A).
And finally, consider that tree interpretations, such as the one we used to show con-
cept 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 = {A(a), B(b), f (a) = c, f (b) = c}.

 – A TBox T = {A v B : f → id } implies that the individuals a and b must denote
   the same domain element.
 – A TBox T = {A v B : f → g} implies that there must be an additional (anony-
   mous) 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 : Pf 1 , . . . , Pf k → Pf ∈ 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 Pf 0 of Pf
                 Pf 0            Pf 0
    such that a ; c and b ; c in δ(T , A) for some individual c; it returns false other-
    wise.
expf(a, Pf, δ(T , A)): Returns the minimal set of transitions (by creating new individ-
                            Pf
   uals) such that a ; c in δ(T , A) holds for some c.
                                           
mkeq(a, b, Pf, δ(T , A)): Returns {c → d, d → c} where, for some individuals c and d,
                 Pf              Pf
    we have a ; c and b ; d in δ(T , A).
The PFD closure rule is then defined as follows:
                       
    if {a ; A, b ; B} ⊆ δ(T , A) and
       match(a, b, Pf i , δ(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.

Definition 11 (Transition Relation δ(T , A)) Let δ(T , A) be the smallest transition
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 {a} and final state B (similarly to Section 3).
Theorem 12 (Knowledge Base Consistency) A knowledge base (T , A) is consistent
if and only if
                     L(nfaaB (T , A)) ∩ L(nfaa¬B (T , A))

is empty for all primitive concepts B ∈ PC and all ABox individuals a in A.
Proof (sketch) Assume Pf ∈ L(nfaaB (T , A)) ∩ L(nfaa¬B (T , A)) for some path func-
tion Pf, individual a and primitive concept B, and that I |= (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 Pf I (aI ) ∈ BI and Pf I (aI ) ∈ ¬BI
(similarly to Lemma 4); a contradiction as interpretations of path functions are func-
tional.
For the other direction we define an interpretation I as follows: let dae be an represen-
                                             
tative of the equivalence class {a | a ; b, b ; a in δ(T , A)} and let PF(a) denote
                             f
                {f. Pf | a ; b not in δ(T , A)} for any individual b}.
Then set

 – 4I = a in A {dae. id } ∪ {dae. Pf | Pf ∈ PF(a)};
         S

 – aI = dae. id ;
                        Pf
 – AI = {dae. Pf | a ; A in δ(T , A)}; and
                                  f
 – f I = {(dae. id , dbe. id ) | a ; b in δ(T , A)} ∪
                                      {(dae. Pf, dbe. Pf .f ) | dae. Pf, dae. Pf .f ∈ 4I }.

It is immediate that I |= 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 |= T .
2

Note that the core of this construction is again the subset construction for NFA deter-
minization (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.

Lemma 13 |δ(T , A)| is polynomial in |T | + |A|.
Proof (sketch) The number of individuals in δ(T , A) is bounded by |A| + 2|T ||A|2
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 |T | + |A|, the
number of transitions in δ(T , A) is also at most polynomial in |T | + |A|.         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.                    2
4.1   Logical Implication
Now we consider the questions of logical implication of the form (T , A) |= C(a),
(T , A) |= Pf 1 (a) = Pf 2 (b), and ultimately T |= 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 simplifica-
tion rules:
                                 Simp(C) → {C}
                    Simp(∀ Pf .C1 u C2 ) → Simp(∀ Pf .C1 ) ∪ Simp(∀ Pf .C2 )
                    Simp(∀ Pf .∀ Pf 0 .C1 ) → Simp(∀ Pf . Pf 0 .C1 )
where C is one of the irreducible concepts of the forms ∀ Pf .A, ∀ Pf .¬A, and ∀ Pf .A :
Pf 1 , . . . , Pf k → Pf 0 . We call the irreducible concepts obtained by these rules the sim-
plifications of the given concept.

Lemma 15 (T , A) |= C(a) (T |= A v C) if and only if (T , A) |= D(a) (T |= A v
D, respectively) for all D ∈ Simp(C).
Proof (sketch)    By observing that the each step of simplifications preserves logical
implication.                                                                        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) |= ∀ Pf .A(a) iff (T , A ∪ {∀ Pf .¬A(a)}) is not satisfiable.
 2. (T , A) |= ∀ Pf .¬A(a) iff (T , A ∪ {∀ Pf .A(a)}) is not satisfiable.
 3. (T , A) |= (∀ Pf .A : Pf 1 , . . . , Pf k → Pf 0 )(a) iff
                                                              [
     (T , A ∪ {Pf(a) = b, A(c), D(Pf 0 (b)), ¬D(Pf 0 (c)} ∪         {Pf i (b) = Pf i (c)})
                                                                 0<i≤k
    is not satisfiable, where b and c are fresh individual names and D is a fresh primitive
    concept.
 4. (T , A) |= (Pf 1 (a) = Pf 2 (b)) iff (T , A ∪ {D(Pf 1 (a)), ¬D(Pf 2 (b))} is not satisfi-
    able, where D a fresh primitive concept.                                               2
For logical implication questions of the form T |= A v C, where C is irreducible,
simply replace the ABox A in the above by {A(a)}. 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     Conjunctive Queries
We assume the standard definition of conjunctive queries, and begin by considering
queries of the form
                           ∃x.(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 ∃x.(A1 (x) ∧ . . . ∧ Ak (x)), where Ai are primitive concept names.
The question (T , A) |= q is PSPACE-hard (in combined complexity) and in PTIME in
|T | + |A|.
Proof (sketch) It is sufficient to show that in every model I of (T , A) there is a object
o ∈ 4I such that o ∈ AIi for all 0 < i ≤ k. We set
                   A0 = A ∪ {fi (s) = ai | ai an individual in A}
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) |= q:

    – If (T , A) |= q then, in every model I of (T , A), there must be an ABox individual
      ai and a path function Pf such that Pf I (aIi ) ∈ AIj for all 0 < j ≤ k. Then,
      however, it is easy to verify that fi . Pf ∈ L(M ) by analysis of the definition of M ;
    – Conversely, if fi . Pf ∈ L(M ), then, in every model I of (T , A) and every 0 <
      j ≤ k, it follows that Pf I (aIi ) ∈ AIj since fi . Pf ∈ L(nfasAj (T , A0 )), and, by the
      definition of M , that Pf ∈ 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, [15]); for the lower bound we simply use a knowledge base
in which the query is not directly satisfied by any ABox individual.                  2

This result can be extended to all rooted and tree shaped conjunctive queries by appro-
priately modifying the final states in the individual automata in the above construction.
For general conjunctive queries, it becomes necessary to analyze the query in order
to search for ABox matches for non-tree components, matches close to the ABox for
tree-shaped parts connected to non-tree components, and use the above technique for
tree-shaped disconnected components. A full elaboration of this is straightforward but
requires much more space than is available. This yields a PTIME query answering al-
gorithm in the size of the knowledge base, |T | + |A|, and shows PSPACE-completeness
for combined complexity.


6     Related Work

PFDs in CF Dnc were first introduced and studied in the context of graph-oriented
data models such as RDF and its refinements [11, 23]. Subsequently, an FD concept
constructor was proposed and incorporated in Classic [5], an early DL with PTIME
reasoning capabilities, without changing the complexity of its implication problem. We
mentioned earlier that removing the conditions imposed on PFDs in (1) for CF Dnc
makes all of its reasoning problems EXPTIME-complete [13]. This remains unchanged
in the absence of primitive negation or in the presence of additional concept constructors
common in very rich DLs such as (general) concept negation, roles, qualified number
restrictions, and so on [17, 18]. Relating to applications, PFDs have been incorporated
in graph-based data models to address problems in schema diagnosis and synthesis [3,
4] and in query optimization [10, 12].
    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 im-
      plication PSPACE-complete [22].
    – Allowing conjunction and value restriction “∀” makes logical implication EXPTIME-
      complete [13].
In [9], the authors consider a DL with functional dependencies and a general form of
keys added as additional varieties of dependencies, called a key box. They show that
their dialect is undecidable for DLs with inverse roles, but becomes decidable when
unary functional dependencies are disallowed. This line of investigation is continued
in the context of PFDs and inverse features, with analogous results [20]. Subsequently,
Calvanese et al. have shown how DL-Lite can be extended with a path-based variety
of identification constraints analogous to PFDs without affecting the complexity of rea-
soning problems [8].


7     Summary
We have presented the DL logic CF Dnc, a variation on the logic CF D with the fol-
lowing 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 con-
sequences of allowing CF Dnc concept constructors other that conjunction on the left-
hand-side of inclusion dependencies is, to the best of our knowledge, open. In particular,
this includes values restrictions “∀”, negated primitive concepts “¬A” and PFDs.
    One enhancement to CF Dnc that we believe is straightforward, and that would con-
siderably 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 EL role constructors on right-hand-sides of in-
clusion dependencies in CF Dnc would also be possible without damage to its PTIME
capabilities.
References
 1. Alessandro Artale, Diego Calvanese, Roman Kontchakov, and Michael Zakharyaschev. The
    DL-Lite family and relations. J. Artif. Intell. Res. (JAIR), 36:1–69, 2009.
 2. Franz Baader, Sebastian Brandt, and Carsten Lutz. Pushing the EL Envelope. In Proc. Int.
    Joint Conf. on Artificial Intelligence (IJCAI), pages 364–369, 2005.
 3. Joachim Biskup and Torsten Polle. Decomposition of Database Classes under Path Func-
    tional Dependencies and Onto Constraints. In Foundations of Information and Knowledge
    Systems, pages 31–49, 2000.
 4. Joachim Biskup and Torsten Polle. Adding inclusion dependencies to an object-oriented data
    model with uniqueness constraints. Acta Informatica, 39:391–449, 2003.
 5. Alexander Borgida and Grant Weddell. Adding Uniqueness Constraints to Description Log-
    ics (Preliminary Report). In International Conference on Deductive and Object-Oriented
    Databases, pages 85–102, 1997.
 6. Diego Calvanese, Giuseppe De Giacomo, Domenico Lembo, Maurizio Lenzerini, and Ric-
    cardo Rosati. DL-Lite: Tractable description logics for ontologies. In Proc. of the 20th Nat.
    Conf. on Artificial Intelligence (AAAI 2005), pages 602–607, 2005.
 7. Diego Calvanese, Giuseppe de Giacomo, Domenico Lembo, Maurizio Lenzerini, and Ric-
    cardo Rosati. Tractable Reasoning and Efficient Query Answering in Description Logics:
    The DL-Lite Family. Journal of Automated Reasoning, 39(3):385–429, 2007.
 8. Diego Calvanese, Giuseppe De Giacomo, Domenico Lembo, Maurizio Lenzerini, and Ric-
    cardo Rosati. Path-Based Identification Constraints in Description Logics. In Proc. of the
    11th Int. Joint Conf. on Principles of Knowledge Representation and Reasoning (KR), pages
    231–241, 2008.
 9. Diego Calvanese, Giuseppe De Giacomo, and Maurizio Lenzerini. Identification Constraints
    and Functional Dependencies in Description Logics. In Proc. Int. Joint Conf. on Artificial
    Intelligence (IJCAI), pages 155–160, 2001.
10. David DeHaan, David Toman, and Grant Weddell. Rewriting Aggregate Queries using De-
    scription Logics. In Description Logics 2003, pages 103–112. CEUR-WS vol.81, 2003.
11. Minoru Ito and Grant Weddell. Implication Problems for Functional Constraints on
    Databases Supporting Complex Objects. Journal of Computer and System Sciences,
    49(3):726–768, 1994.
12. Vitaliy L. Khizder, David Toman, and Grant Weddell. Reasoning about Duplicate Elimina-
    tion with Description Logic. In Rules and Objects in Databases (DOOD, part of CL’00),
    pages 1017–1032, 2000.
13. Vitaliy L. Khizder, David Toman, and Grant Weddell. On Decidability and Complexity of
    Description Logics with Uniqueness Constraints. In Int. Conf. on Database Theory ICDT’01,
    pages 54–67, 2001.
14. Roman Kontchakov, Carsten Lutz, David Toman, Frank Wolter, and Michael Zakharyaschev.
    The combined approach to query answering in DL-Lite. In KR, 2010.
15. Dexter Kozen. Lower bounds for natural proof systems. In Proceedings of the 18th Annual
    Symposium on Foundations of Computer Science, pages 254–266. IEEE Computer Society,
    1977.
16. Carsten Lutz, David Toman, and Frank Wolter. Conjunctive query answering in the de-
    scription logic EL using a relational database system. In Proc. Int. Joint Conf. on Artificial
    Intelligence (IJCAI), pages 2070–2075, 2009.
17. David Toman and Grant Weddell. On Attributes, Roles, and Dependencies in Description
    Logics and the Ackermann Case of the Decision Problem. In Description Logics 2001, pages
    76–85. CEUR-WS vol.49, 2001.
18. David Toman and Grant Weddell. Attribute Inversion in Description Logics with Path Func-
    tional Dependencies. In Description Logics 2004, pages 178–187. CEUR-WS vol.104, 2004.
19. David Toman and Grant Weddell. On Reasoning about Structural Equality in XML: A De-
    scription Logic Approach. Theoretical Computer Science, 336(1):181–203, 2005.
20. David Toman and Grant Weddell. On the Interaction between Inverse Features and Path-
    functional Dependencies in Description Logics. In Proc. Int. Joint Conf. on Artificial Intel-
    ligence (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.

</pre>