On Partial Features in the DLF Dialects of Description Logic with Inverse Features

Abstract

The DLF dialects of description logic are fragments of rst order logic with underlying signatures based on unary predicate symbols and on unary function symbols interpreted as total functions. In earlier work, we have shown how computational properties of logical consequence for dialects of this family without inverse features are preserved when unary function symbols are interpreted instead as partial functions, and when a \9f " concept constructor for feature value existence is added that can be used to enforce function totality. In this paper, we resolve a number of open problems mentioned in this earlier work that concerns DLF dialects with inverse features. Our main result shows how the dialect CF DInc can be extended with a limited form of conjunction on 8 left-hand-sides of inclusion dependencies that enables a straightforward simulation of partial functions together with the 9f concept constructor.

Introduction

The DLF dialects of description logics (DLs) are fragments of rst order logic with underlying signatures that replace binary predicate symbols, called roles, with unary function symbols, interpreted as total functions, called features. In earlier work [ 7 ], we have shown how computational properties of logical consequence for dialects of this family are preserved when unary function symbols are now interpreted as partial functions, where equality is based on the so-called strict interpretation of unde ned values, and when an \9f " concept constructor is added for identifying subsets of a domain for which f -values must exist. Note that the latter yields an ability to de ne cases in which partial functions become total functions, such as to say that every employee has a salary, or to de ne cases in which partial functions are not meaningful, such as to say that departments do not have a salary.

In this paper, we resolve a number of open problems mentioned in this earlier work that concern DLF dialects with inverse features, among which is the more 8 recent CF DInc dialect in the CF D sub-family [ 6 ]. Members of this sub-family are distinguished by having PTIME complexity for logical consequence. One of 8 our results shows how CF DInc can be extended with a form of conjunction on left-hand-sides of inclusion dependencies while still retaining PTIME complexity for logical consequence. We show how the added expressiveness enables a straightforward simulation of partial functions and the 9f concept constructor.

The paper is organized as follows. In the next section, we provide the necessary background and de nitions: an overview of the syntax and semantics of the DLF dialects, and of their general extension to partial functions as we have proposed in [ 7 ]. In Section 3, we introduce the dialects DLF I and DLF DI, and how, by following the same reduction introduced in [ 7 ], each can simulate their partial extensions in a straightforward manner. The results mentioned above 8 regarding the dialect CF DInc are then presented in Section 4. Mainly, this en8 tails introducing an extension we call CF DIkc that admits a limited use of conjunction on the left-hand-sides of inclusion dependencies. We then show how 8 CF DIkc can also be used to simulate its partial extension in a similar fashion to how we did this for DLF I and DLF DI in Section 3. 2

Background and De nitions

We begin with a review of the basic de nitions for member dialects of the DLF family in which features replace roles and are interpreted as total functions. Following this, we introduce the necessary modi cations that enable features to be interpreted instead as partial functions.

De nition 1 (Feature-based DLs) Let F and PC be sets of feature names and primitive concept names, respectively. A path expression is de ned by the grammar \ Pf ::= f: Pf j id " for f 2 F.1 We de ne derived concept descriptions by the grammar on the left-hand-side of Figure 1.

An inclusion dependency C is an expression of the form C1 v C2. A terminology (TBox) T consists of a nite set of inclusion dependencies. A posed question Q is a single inclusion dependency.

The semantics of expressions is de ned with respect to a structure I = (4; I ), where 4 is a domain of \objects" and I an interpretation function that xes the interpretations of primitive concepts A to be subsets of 4 and primitive features f to be total functions f I : 4 ! 4. The interpretation is extended to path expressions, id I = x:x, (f: Pf)I = PfI f I and derived concept descriptions C as de ned in the center column of Figure 1. An interpretation I satis es an inclusion dependency C1 v C2 if C1I C2I and is a model of T (I j= T ) if it satis es all inclusion dependencies in T . The logical implication problem asks if T j= Q holds, that is, if Q is satis ed in all models of T . 2 Here, we do not consider so-called ABoxes, that is, sets of assertions about membership of individuals in descriptions, nor do we consider the associated problem of knowledge base consistency. Note, however, that such issues can be reduced to logical implication problems involving posed questions that utilize value restrictions and equational same-as descriptions [ 5 ].

The logical implication problem for TBoxes and posed questions characterized so far, that allow arbitrary concepts in inclusion dependencies, is not decidable for a variety of reasons. For example, see [ 4 ] for one case involving arbitrary 1 We also simplify this notation by allowing a syntactic composition \Pf1 : Pf2" that stands for their concatenation. C ::= A j C1 u C2 j C1 t C2 j :C j 8 Pf :C j 9f 1

AI 4 C1I \ C2I C1I [ C2I 4 n CI fx : PfI (x) 2 CI g ff I (x) : x 2 4g (primitive concept; A 2 PC) (conjunction) (disjunction)

(negation) (value restriction) (inverse feature) j C : Pf1; :::; Pfk ! Pf0 j > j ? j (Pf1 = Pf2) fx : 8 y 2 CI : Vik=1 PfiI (x) = PfiI (y)

! Pf0I (x) = Pf0I (y)g 4 ; fx : Pf1I (x) = Pf2I (x)g (PFD)

(top) (bottom) (same-as)

PFDs and ABoxes encoded in the above manner. However, restrictions on occurrences of concept constructors has led to a number of decidable fragments that range from light-weight to expressive dialects of feature-based DLs. The restrictions that obtain DLF I, DLF DI, CF DI8nc and CF DIk8c , the focus of our attention, are given in Section 3 for the rst two cases and in Section 4 for the last two cases.

The two de nitions that follow introduce the necessary modi cations to our characterization of feature-based DLs to accommodate features interpreted as partial functions. To refer to such modi cations, we follow a notational convention of qualifying particular dialects with the word \partial " whenever we intend such modi cations to apply, as in partial DLF DI for example.

De nition 2 (Partial Features and Existential Restrictions) The syntax of feature-based DLs is extended with an additional concept constructor of the form \9f ", called an existential restriction. Semantics is given as follows: 1. Features f 2 F are now interpreted as partial functions on 4 (i.e., the result can be unde ned for some elements of 4); and 2. The 9f concept constructor is interpreted as fx : 9y 2 4:f I (x) = yg. In this setting, a path function Pf naturally denotes a partial function resulting from the composition of partial functions. We also adopt the strict interpretation of unde ned values. This means that equality holds only when both of its arguments are de ned and denote the same object, and that set membership (2) requires only de ned values to be members of its right hand side argument. 2 Observe that features are still functional, and that there is therefore no need for a quali ed existential restriction of the form \9f:C", with semantics given as follows:

(9f:C)I = fx : 9y 2 4:f I (x) = y ^ y 2 CI g: Indeed, such a restriction can be simulated by assuming \9f:C" to be shorthand for \(9f u 8f:C)". Assuming this, we now write \(9Pf)" in the following as shorthand for \(9f1 u 8f1:(9f2 u 8f2:(: : : (9fk) : : :)))": All that remains for our modi cations is to revise the semantics of the PFD constructor to account for the presence of partial features. We adopt the minimum necessary revision needed for recognizing when one violates a PFD inclusion dependency of the form \ C1 v C2 : Pf1; : : : ; Pfk ! Pf0 " : At the least, this should happen when: (1) all path functions Pf0; : : : ; Pfk are de ned for a C1 object e1 and a C2 object e2, and (2) PfiI (e1) = PfiI (e2) holds only for i > 0. This yields the following modi cation to the interpretation of PFDs in the presence of partial features that we now adopt: (C : Pf1; : : : ; Pfk ! Pf0)I = fx : 8y:y 2 CI ^ x 2 (9Pf0)I ^ y 2 (9Pf0)I ^

Vik=1(x 2 (9Pfi)I ^ y 2 (9Pfi)I ^ PfiI (x) = PfiI (y)) ! Pf0I (x) = Pf0I (y)g: Observe that this de nition coincides with the original semantics of the PFD constructor given in Figure 1 when features are interpreted as total functions.

The following illustrates the use of existential restrictions and PFDs in DLF dialects with partial features. This includes two examples of constraints mentioned informally in our introductory comments together with two further examples showing how PFDs can be used to capture keys and functional dependencies. Note that all can be captured in any of the dialects mentioned below: 1. EM P v 9salary (every employee has a salary); 2. DEP T v :9salary (departments do not have a salary); 3. DEP T v DEP T : manager ! id (no two departments have the same manager); and 4. EM P v EM P : paygrade ! salary (employee pay grades determine salaries). 3

Expressive Logics with Inverses in the DLF Family We now introduce a pair of expressive feature-based DLs and show how logical consequence for their partial variants can be simulated in a straightforward fashion. The rst is called DLF I and allows both TBox and posed question dependencies to contain concepts formed from primitive concepts and bottom using the following concept constructors: conjunction, disjunction, negation, value restriction and inverse features. The second is called DLF DI, and allows, in addition, the PFD concept constructor to appear on the right hand sides of inclusion dependencies. Both logics are a special case of the dialect DLF AD introduced in [ 3 ]. This earlier DL admitted quali ed inverse features together with restrictions on their use which yielded cases for which the logical implication problem was complete for EXPTIME. One of the restrictions relating to a coherency condition on terminologies introduced in [ 3 ] is obtained when inverse features are unquali ed, as is the case for both DLF I and DLF DI. Thus, overall restrictions on syntax for these DLs yield expressive Boolean complete dialects with a logical implication problem that is complete for EXPTIME as well. Conversely, extensions, such as allowing PFDs on the left-hand sides of inclusion dependencies, or allowing equational constraints in the posed questions (or equivalently ABoxes), make logical consequence undecidable [ 4 ].

We now proceed to demonstrate that partial features can be e ectively simulated in DLF I and DLF DI by introducing an auxiliary primitive concept G that stands for existing or generated objects, and by using value restrictions to assign membership of objects generated by the 9f constructor to this concept. All remaining inclusion dependencies are then simply preconditioned by this auxiliary concept.

Formally, let T be a partial DLF I TBox in which all inclusion dependencies are of the form > v C. We de ne a DLF I TBox TDLFI as

TDLFI = fG v C[9f 7! 8f:G; for all f 2 F ] j > v C 2 T g

[ f8f:G v G j f 2 F g; where G is a primitive concept not occurring in T . Note that the substitution [9f 7! 8f:G; for all f 2 F ] is applied simultaneously to all occurrences of the 9f constructor in the concept C.

Theorem 3 Let T be a partial DLF I TBox in which all inclusion dependencies are of the form > v C. Then

T j= > v C if and only if TDLFI j= G v C[9f 7! 8f:G; for all f 2 F ]; for G a fresh primitive concept.

Proof (sketch): For any I where I j= TDLFI , we can de ne an interpretation J = (GI ; jIGI ). It is easy to verify that J j= T and also that J j= > v C since I j= G v C[9f 7! 8f:G; for all f 2 F ].

For the other direction, we need to extend a model J of T to a model I of TDLFI by setting GI = 4J and by adding missing features connecting I to complete F trees with all nodes in (:G)I . This way, either I coincides with J or satis es dependencies in TDLFI and G v C[9f 7! 8f:G; for all f 2 F ] vacuously. 2 To extend this construction to the full partial DLF DI logic, it is su cient to encode the path function existence preconditions in terms of the auxiliary concept G as follows: if A v B : Pf1; : : : ; Pfk ! Pf0 2 T then

k k A u (l 8 Pfi :G) v B u (l 8 Pfi :G) : Pf1; : : : ; Pfk ! Pf0 (1) i=0 i=0 is added to TDLFDI . Here, we are assuming w.l.o.g. that A and B are primitive concept names (DLF DI allows one to give such names to complex concepts). Theorem 4 Let T be a partial DLF DI TBox in which all inclusion dependencies are of the form > v C or A v B : Pf1; : : : ; Pfk ! Pf0. Then T j= > v C if and only if TDLFDI j= G v C[9f 7! 8f:G; for all f 2 F ]; and T j= A v B : Pf1; : : : ; Pfk ! Pf if and only if TDLFDI j= (1); for G a fresh primitive concept.

Proof (sketch): The claim follows by observing that (1) captures properly the semantics of PFDs and then by appealing to Theorem 3. 2

DLF DI.

Corollary 5 Logical implication is EXPTIME-complete for partial for partial DLF I and 2 Similar results can be obtained for other members of the DLF I family. 4

Tractable Logics with Inverses in the CF D Sub-Family We now introduce a new member of the DLF I sub-facility of DLs called CF DIk8c , and show how the added expressiveness of partial functions and existential re8 striction can be simulated in CF DIkc in the same general way as was done above for the expressive cases. (Recall that members of this sub-family have 8 PTIME complexity for determining logical consequence.) CF DIkc is an extension of the CF D dialect CF DI8nc in [ 6 ], the rst member of this sub-family to allow the use of feature inversion. The extension adds to this earlier dialect a capability for a limited use of conjunction in left-hand-sides of inclusion dependencies which, among other things, yields the ability to simulate partial features in partial CF DIk8c .

Our new DL, like all members of the CF D family, allows the use of an ABox (optionally captured by using same-as in left-hand-sides of posed questions) and therefore requires PFDs to adhere to one of the following two forms to avoid both undecidability [ 4 ] and indeed intractability [ 6 ]:

PFD ::= A : Pf1; : : : ; Pf : Pfi; : : : ; Pfk ! Pf j A : Pf1; : : : ; Pfi :f; : : : ; Pfk ! Pfi :g (key ) (functional dependency ) (2) With this restriction, introduced in [ 6 ], posed questions can contain inclusion dependencies formed from concepts in Figure 1, albeit with a few mild restrictions when tractability in the size of the posed question is required. For simplicity, however, we assume that the concepts in the posed question Q = E1 v E2 adhere to the following grammar:

E ::= A j ? j E u E j 8 Pf :E j (Pf1 = Pf2): More complex posed questions, e.g., ones that contain the PFD constructor [ 5 ], can be equivalently expressed in the above grammar (perhaps as a sequence of posed questions). 8

Inclusion dependencies C v D in a CF DIkc TBox are respectively given by the following grammars:

C ::= A j 8f:A j A1 u A2

D ::= A j ? j 8f:A j 9f 1 j PFD For technical reasons we assume, w.l.o.g., that either C or D is a primitive concept for the remainder of the paper.

8

In comparison to CF DInc introduced in [ 6 ], this new dialect now allows inclusion dependencies of the form \(A1uA2) v A3". In general, unrestricted use of conjunction on the left-hand side of inclusion dependencies leads to EXPTIMEcompleteness of the associated reasoning problems, and so it is necessary to somehow restrict this use of conjunction. The intuition behind the restriction we adopt below is to limit the number of conjuncts that need to be considered on the left-hand sides of inclusion dependencies. Unfortunately, this property is not a simple syntactic restriction, e.g., on the form of inclusion dependencies in a TBox. Indeed, it is easy to see that allowing inclusion dependencies in 8 CF DIkc of the form above is equivalent to allowing arbitrary conjunctions (due to inference). Hence, a CF DIk8c TBox is instead given as follows: De nition 6 (Restricted Conjunction) Let T be a TBox with inclusion dependencies satisfying the above grammar rules, and let k > 0. We say that T is a CF DIk8c TBox if, whenever T j= (A1 u u An) v B for some set of primitive concepts fA1; : : : ; Ang [ fBg, then T j= (Ai1 u u Aik ) v B for some k-sized subset fAi1 ; : : : ; Aik g of the primitive concepts fA1; : : : ; Ang. 2 The following Lemma shows that verifying whether an TBox is an CF DIk8c TBox can be veri ed in PTIME (for a xed k): Lemma 7 Let T be a CF DIk8c TBox and k > 0. Then T is not a CF DIk8c TBox if there are primitive concepts A1; : : : ; Ak+1 and B such that T j= (A1 u : : : u Ak+1) v B for which the condition in De nition 6 fails.

Proof (sketch): Consider an inclusion dependency (A1 u : : : u An) v B where n > 2 is the smallest value such that the dependency is a logical consequence of T and such that there no (Ai1 u u Aik ) v B that is also a logical consequence of T . Observe that there must be a linear input resolution proof (of the rstorder translation of the problem) of B(x) from T [ fA1(x); : : : ; An(x)g [ 2 ]. Since the resolution steps with A1(x); : : : ; An(x)g can be performed last and they all must be present, there is a clause :A1(x); : : : ; :An(x) in the proof. However, since all input clauses to the problem are binary or ternary and since the proof starts with :B(x), there must be a one-shorter clause preceding this clause in this proof. A contradiction. 2 We now consider TBox and concept satis ability in CF DIk8c , and show an PTIME algorithm by extending the approach for CF DI8nc in [ 6 ]. TBox and Concept Satis ability

8 It is easy to see that every CF DIkc TBox T is consistent (by setting all primitive concepts to be interpreted as the empty set). To test for (primitive) concept satis ability we use the following construction: De nition 8 (TBox Closure) Let T be a CF DIk8c TBox in normal form. We de ne Clos(T ) to be the least set of subsumptions such that: 1. D v D; 2. D v E and E v F then D v F ; 3. D v E and F E, F 6= ; then D v F ; 4. D v E and D v F then D v E + F (for all E + F 5. A v B 2 T and A D then D v B; 6. 8f:? v ? and ? v 8f:?; 7. D v E then 8f:D v 8f:E; E [ F ); 8. D v 9f 1 and 8f:D v 8f:E then D v E where (1) D, E, and F are sets of primitive concepts of size at most k, or sets of value restrictions with respect to a particular feature applied to such sets of primitive concepts, where (2) E + F is a subset of size between 1 and k of E [ F , and where (3) A and B are concepts allowed on the left and right-hand sides of subsumptions in T . We also con ate sets of concepts and their conjunctions and value restriction applied to a conjunction with a conjunction of individual value restrictions. 2 Note that Clos(T ) is polynomial in jT j (and exponential in k). It is also easy to verify that each inclusion added to Clos(T ) by the inferences (1-4) in De nition 8 is logically implied by T . 8 Theorem 9 (Primitive Concept Satis ability) Let T be a CF DIkc TBox in normal form and A a primitive concept description. Then A is satis able with respect to T if and only if A v ? 62 Clos(T ).

Proof (sketch): Given Clos(T ), an object o, and a primitive concept A, we de ne the following family of subsets of PC indexed by paths of features (and their inverses), starting from o, as follows: 1. So = fB j A v B 2 Clos(T )g; 2. Sf(x) = fB j A v 8f:B 2 Clos(T ) and A 2 Sxg, when f 2 F and x not of the form \f (y)"; and 3. Sf (x) = fB j 8f:A v B and A 2 Sxg, when A0 v 9f 1 2 Clos(T ), A0 2 Sx, and x not of the form \f (y)".

We say that Sx is de ned if it conforms to one of the three above cases, and that it is consistent if ? 62 Sx.

It is easy to see that 1. If Sf(x) is not consistent, then Sx is not consistent. 2. If Sf (x) is de ned and not consistent, then Sx is not consistent. We build a model of T in which o 2 AI for some o 2 4 as follows: { 4 = fx j Sx is de nedg; { f I = f(x; f (x)) j Sf(x) is de nedg [ f(f (x); x) j Sf (x) is de nedg; and { AI = fx j Sx is de ned; A 2 Sxg.

Observe all de ned sets Sx must be consistent. Otherwise, A (2 S0) must be inconsistent, implying in turn that A v ? 2 Clos(T ), a contradiction. Hence, I = (4; :I ) is a model of T (it satis es all dependencies in Clos(T )) such that o 2 AI . 2 Note that the model witnessing satis ability of A does not contain any identical path agreements and hence vacuously satis es all PFDs in T .

E(Pf1; Pf2) ! E(Pf2; Pf1) E(Pf1; Pf2) ^ E(Pf2; Pf3) ! E(Pf1; Pf3) E(Pf1; Pf2) ! E(Pf1 :f; Pf2 :f ); for fPf1 :f; Pf2 :f g E(Pf1; Pf2) ^ CC (Pf1) ! CC (Pf2) PF(T ; Q) CC1uC2 (Pf) ! CC1 (Pf) and CC1uC2 (Pf) ! CC2 (Pf) C8 Pf0 :C (Pf) ! CC (Pf : Pf0) for Pf : Pf0 2 PF(T ; Q) C(Pf1=Pf2)(Pf) ! E(Pf : Pf1; Pf : Pf2) CC:Pf1;:::;Pfk!Pf0 (Pf) ^ CC (Pf0) ^ (V0<i k E(Pf : Pfi; Pf0 : Pfi)) ! E(Pf : Pf0; Pf0 : Pf0)) CA1 (Pf) ^ : : : ^ CAk (Pf) ! CD(Pf) for all (A1 u : : : u Ak v D) 2 T CA(Pf :f ) ! CD(Pf) for all (8f:A v D) 2 T

The above theorem can be used to check satis ability of complex (nonPFD) concepts; e.g., satis ability of 8 Pf :B w.r.t. T can be tested by checking satis ability of a new primitive concept A w.r.t. (the normalized version of) T [ fA v 8 Pf :Bg.

The theorem also provides a technique for checking satis ability of nite conjunctions of primitive concepts with respect to T : Logical Implication and Knowledge Base Consistency Allowing inverse features a ects how PFDs interact with a posed question. In particular, PFDs in which all path functions have a common pre x may apply to (pairs of) anonymous individuals mandated by the existence of anonymous inverse features. In general, to enforce PFDs with respect to a posed question while avoiding any need to explicitly create anonymous predecessor objects, we add additional logically implied PFDs to a given TBox as follows: 8 De nition 11 (PFD Enrichment for Inverses) Let T be a CF DIkc TBox in normal form such that A v B : f: Pf1; : : : ; f: Pfk ! f: Pf 2 T (A v B : f: Pf1; : : : ; f: Pfk ! id 2 T ) where Pfi 6= id for all 1 i k. Then we require that A v 8f:A0, B v 8f:B0, and A0 v B0 : Pf1; : : : ; Pfk ! Pf (A0 v B0 : Pf1; : : : ; Pfk ! id ), where A0 and B0 are fresh primitive concepts, are also in T . (For further details on this, see [ 1 ].) 2 With these restrictions we can now show that the logical implication problem 8 for CF DIkc is in PTIME. Our proof is based on encoding a given problem as a collection of Horn clauses. The reduction introduces terms that correspond to path expressions, and relies on the fact that the number of required terms is polynomial in the size of the problem itself.

De nition 12 (Expansion Rules) Let T and Q be a partial CF D terminology and a posed question, respectively. We write CON(T ; Q) to denote the set of all subconcepts appearing in T and Q, de ne PF(T ; Q) to be the set write CC to denote unary predicates for C 2 CON(T ; Q), and introduce a unary predicate D and a binary predicate E, with all predicates ranging over the universe PF(T ; Q). The expansion rules for a given terminology T , denoted R(T ), are de ned in Figure 2. To deal with the possibility of inconsistency, we add the following rule that can be applied after the rules in Figure 2 are are exhaustively applied.2

If CA1 (Pf); : : : ; CAk (Pf) 2 R(T ) for some Pf 2 PF(T ; Q) and A1 u: : :uAk is not consistent in T then add C?(Pf) to R(T ).

A goal for each concept E is a set of ground assertions de ned as follows: for E = A; for E = ?; for E = (Pf1 = Pf2); GE = >8 fCA(id )g > > >>> fC?(id )g > > < fE(Pf1; Pf2)g > GE1 [ GE2 > > > >>> fCC (Pf0 : Pf) j CC (Pf) 2 GE0 g >: [ fE(Pf0 : Pf1; Pf0 : Pf2) j E(Pf1; Pf2) 2 GE0 g for E = 8 Pf0 :E0: for E = E1 u E2; and Given two concept descriptions E1 and E2, we say that

R(T ) [ fCE1 (id )g j= GE2 if GE2 M for every minimal ground model M of R(T ) over PF(T ; Q) that contains CE1 (id ) and D(id ). 2 Intuitively, PF(T ; Q) represents a nite graph of objects, predicates E(Pf1; Pf2) express equality of the objects at the end of paths Pf1 and Pf2, and predicates CC0 (Pf) express that the object at the end of path Pf is in the interpretation of concept C0. Note that the expansion rules do not need to take inverses into account due to De nition 11.

Logical implication for CF DIk8c TBoxes T and posed questions Q can now be solved as follows: Theorem 13 Let T be a terminology and Q a posed question of the form E1 v E2 in CF DIk8c . Then

T j= Q i R(T ) [ fCE1 (id )g j= GE2 or

R(T ) [ fCE1 (id )g j= G8 Pf :?(id ) for some Pf 2 PF(T ; Q): Proof (sketch): If C?(Pf) for Pf 2 PF(T ; Q) appear in M , where M is the least model of R(T ) [ fCE1 (id )g R(T ), then the concept E1 is unsatis able w.r.t. T 2 Observe that this is where we rely on the our previous PTIME result concerning the satis ability of nite conjunctions of primitive concepts. since only implied facts appear in M , and therefore the subsumption holds for any E1 and T .

Otherwise, if R(T ) [ fCE1 (id )g 6j= GE1 , then there must be a model M of R(T ) [ fCE1 (id )g such that G 62 M for some G 2 GE1 . We construct an interpretation IM such that IM j= T but IM 6j= Q. The interpretation IM contains an object o for each equivalence class de ned on the set PF(T ; Q) by the interpretation of E. The class membership of these objects is determined by the membership of the corresponding path in the interpretations of the CC predicates in M . Note that, due to the syntactic restriction imposed on PFDs, this is su cient to satisfy all PFDs in T since any precondition or a non-trivial consequence of a PFD can only manifest on some path belonging to PF(T ; Q) and beginning at the distinguished object o. To complete the construction of IM , we simply attach a unique complete tree F labeled as in Theorem 9 to each leaf node (i.e., a node that is missing successors). Nodes of these complete trees belong to all primitive descriptions in IM and thus satisfy T . Conversely, assume R(T ) [ fCE1 (id )g j= GE1 but that T 6j= Q. Then there must be an interpretation I and an object o 2 4 such that I j= T and o 2 E1I E2I . Thus, there is a model MI of R(T ) such that CE1 (id ) 2 M . In this model, the element id 2 PF(T ; Q) serves as

I the counterpart of the object o and the interpretations of the predicates CC and E is extracted from I by navigating all (pairs of) path functions in PF(T ; Q). However, since o 62 E2I , it must be the case that MI is a strict subset of the least model of R(T ) [ fCE1 (id )g; a contradiction. 2 Corollary 14 Let T be a terminology and Q a posed question in CF DIk8c . Then the implication problem T j= Q is complete for PTIME. 2 Knowledge base consistency can now be reduced to logical implication as shown in [ 5 ].

Logical Consequence in partial CF DIk8c 8 The following de nition now shows how CF DIkc is able to simulate its extension with partial functions and existential restrictions in a straightforward manner. 8 8 De nition 15 Let T be a partial CF DIkc TBox. We de ne a CF DI(k+1 )c TBox TCFDI(8k+1)c associated with T by initializing with the inclusion dependency 8f:G v G and then mapping inclusion dependencies in T to TCFDI(8k+1)c according to the following:

A1 v B 7! (A1 u G) v B (A1 u A2) v B 7! (A1 u A2) v A3; (A3 u G) v B 8f:A1 v B 7! 8f:A1 v A2; (A2 u G) v B

A1 v 9f 7! A1 v 8f:G (where A3 is fresh) (where A2 is fresh) 2 Indeed, it is easy to verify that TCFDI(8k+1)c is a CF DI(8k+1 )c TBox and that: 8 Theorem 16 Let T be a partial CF DIkc TBox and Q a posed question. Then T j= Q if and only if TCFDI(8k+1)c j= Q[9f 7! 8f:G; for all f 2 F ]:

References

1. Jason St. Jacques , David Toman, and Grant E. Weddell . Object-relational queries over CF DInc knowledge bases: OBDA for the SQL-Literate . In Proc. International Joint Conference on Arti cial Intelligence, IJCAI , pages 1258 { 1264 , 2016 .

2. John W. Lloyd. Foundations of Logic Programming . Springer-Verlag, 1987 .

3. David Toman and Grant E. Weddell . On the interaction between inverse features and path-functional dependencies in description logics . In Proc. Int. Joint Conf. on Arti cial Intelligence (IJCAI) , pages 603 { 608 , 2005 .

4. David Toman and Grant E. Weddell . On keys and functional dependencies as rstclass citizens in description logics . J. Aut. Reasoning , 40 ( 2-3 ): 117 { 132 , 2008 .

5. David Toman and Grant E. Weddell . Applications and extensions of PTIME description logics with functional constraints . In Proc. Int. Joint Conf. on Arti cial Intelligence (IJCAI) , pages 948 { 954 , 2009 .

6. David Toman and Grant E. Weddell . On adding inverse features to the description logic CF D8nc . In PRICAI 2014: Trends in Arti cial Intelligence - 13th Paci c Rim International Conference on Arti cial Intelligence , Gold Coast, QLD , Australia, December 1- 5 , 2014 ., pages 587 { 599 , 2014 .

7. David Toman and Grant E. Weddell . On partial features in the DLF family of description logics . In Richard Booth and Min-Ling Zhang, editors, PRICAI 2016: Trends in Arti cial Intelligence - 14th Paci c Rim International Conference on Arti cial Intelligence , Phuket, Thailand, August 22-26 , 2016 , Proceedings, volume 9810 of Lecture Notes in Computer Science, pages 529 { 542 . Springer, 2016 .