On the Interaction between Inverse Features and Path-functional Dependencies in Description Logics

1 Introduction

For many applications, there is considerable incentive to enhance the modeling utility of feature based description logics (DLs) with an ability to capture richer varieties of uniqueness constraints such as keys and functional dependencies [DeHaan et al., 2003; Khizder et al., 2000; Stanchev and Weddell, 2003; Toman and Weddell, 2004b]. Unfortunately, in combination with feature or role inversion, the associated logical implication problem quickly becomes undecidable [Calvanese et al., 2001]. We investigate conditions under which inverse features can be added to a boolean complete DL with path-functional dependencies (PFDs) [Weddell, 1989] without any consequent impact on the complexity of the associated logical implication problem.

Two conditions are presented that ensure this problem remains EXPTIME-complete. The first is syntactic in nature and imposes a prefix condition on PFDs that occur in argument terminologies. The condition complements and extends the results in [Calvanese et al., 2001] which considered the problem of adding keys and functional dependencies to a DL with predicates in place of roles. The second is a coherence condition on terminologies that allows unrestricted use of PFDs, and is sufficiently weak to allow the formal specification of arbitrary relational or object-oriented schema, including those that fail to satisfy normalization conditions.

✄ The support of Nortel Ltd. and of the Canadian governments through NSERC and CITO is gratefully acknowledged.

This latter observation is important since it enables an incremental development of terminologies that encode schema. One can begin, for example, with a "relational" terminology that fails to satisfy the conditions of Boyce-Codd Normal Form. (The approach used in [Calvanese et al., 2001] is not generally capable of handling such anomalous cases.) Standard normalization algorithms and methodology can then employ reasoning services based on our results. Thus, our DL together with coherence is better equipped to enable the transfer of results in normalization and emerging object design theory for relational and object-oriented data models [Biskup et al., 1996; Biskup and Polle, 2000].

1.1 RelatedWork

Our coherence condition derives from a similar condition proposed in [Biskup and Polle, 2003] to enable the development of a sound and complete axiomatization for an objectoriented data model, which essentially adds inclusion dependencies to a data model defined earlier in [Weddell, 1989]. The DL we consider in this paper is a further generalization; thus, our EXPTIME-completeness result settles an open problem on the decidability of the implication problem for their model.

In [Calvanese et al., 2001], the authors consider a DL with (relational) functional dependencies together with a general form of keys called identification constraints. They show that their dialect is undecidable in the general case, but becomes decidable when unary functional dependencies are disallowed. We show undecidability in a simpler setting, in particular without the use of number restrictions. Our prefix condition on PFDs complements and extends their decidability result to more general PFDs, and our coherency condition serves as an alternative method for regaining decidability.

A form of key dependency with left-hand-side feature paths is considered for a DL coupled with various concrete domains [Lutz et al., 2003; Lutz and Milicic, 2004]. The authors explore how the complexity of satisfaction is influenced by the selection of a concrete domain together with various syntactic restrictions on the key dependencies themselves. In contrast, we consider a DL that admits more general kinds of key constraints (and functional dependencies) for which identifying values can be defined on arbitrary domains.

The remainder of the paper is organized as follows. We begin by introducing the DL dialect a0 ✁ ✄ ✆ a0 that will be the focus of the remainder of the paper. The dialect is feature based and therefore more functional in style as opposed to the more common role based derivatives of ✆ ✁ ✟ . As a consequence, it becomes straightforward to incorporate dependencies into the logic for capturing PFDs. In Section 3, we show that the combination of inverse features and arbitrary PFDs in a0 ✁ ✄ ✆ a0 leads to the undecidability of its associated logical implication problem. Our main results then follow in Section 4 in which we consider two ways to recover decidability based on a prefix restriction condition for PFDs in argument terminologies and on a coherency condition for terminologies. Our summary comments follow in Section 5.

2 Preliminaries

Definition 1 (Description Logic a0 ✁ ✄ ✆ a0 ) Let ✡ and ☛ be sets of feature names and primitive concept names, respectively. A path expression is defined by the grammar " ☞ ✌ ✎ ✎ ✒ ✔ ✕ ☞ ✌ ✖ ✘ ✚ " for ✔ ✜ ✡ . We define derived concept descriptions by a second grammar on the left-hand-side of Figure 1. A concept description obtained by using the final production of this grammar is called a path-functional dependency (PFD).

An inclusion dependency ✟ is an expression of the form ✣ ✤ ✦ . A terminology ★ consists of a finite set of inclusion dependencies.

Figure 1: SYNTAX AND SEMANTICS OF a0 ✁ ✄ ✆ a0 .

The semantics of expressions is defined with respect to a structure ✩ ✴ ▲ ✪ ✭ ✬ , where ✴ is a domain of "objects" and ✩ ✕ ✬ ✭ an interpretation function that fixes the interpretations of primitive concepts ☛ to be subsets of ✴ and primitive features ✔ to be total functions ✩ ✔ ✬ ✭ ✎ ✴ ◗ ✴ . The interpretation is extended to path expressions, ✩ ✘ ✚ ✬ ✭ ✒ ❢ ❇ ✕ ❇ , ✩ ✔ ✕ ☞ ✌ ✬ ✭ ✒ ✩ ☞ ✌ ✬ ✭ ❥ ✩ ✔ ✬ ✭ and derived concept descriptions ✣ and ✦ as defined on the right-hand-side of Figure 1.

An interpretation satisfies an inclusion dependency ✣ ✤ ✦ if ✩ ✣ ✬ ✭ ✲ ✩ ✦ ✬ ✭ . The logical implication problem asks if ★ ✖ ✒ ✣ ✤ ✦ holds; that is, if ✩ ✣ ✬ ✭ ✲ ✩ ✦ ✬ ✭ for all interpretations that satisfy all constraints in ★ .

For the remainder of the paper, we use the following abbreviated notation: ❄ ☞ ✌ ✕ a114 is shorthand for ❄ ✔ ✶ ✕ ❄ ✔ ✺ ✕ ✕ ✕ ✕ ❄ ✔ a80 ✕ a114 , and ● ☞ ✌ ❍ ✶ ✕ a114 for ● ✔ a80 ❍ ✶ ✕ ✕ ✕ ✕ ● ✔ ✺ ❍ ✶ ✕ ● ✔ ✶ ❍ ✶ ✕ a114 for ☞ ✌ ✒ ✔ ✶ ✕ ✔ ✺ ✕ ✪ ✪ ✪ ✕ ✔ a80 ✕ ✘ ✚ . We also identify single feature names ✔ with path descriptions ✔ ✕ ✘ ✚ and allow concatenation of path descriptions, ☞ ✌ ☞ ✌ ✈ to denote their composition ☞ ✌ ❥ ☞ ✌ ✈ .

In addition, we classify constraints by the description on their right-hand side as PFDs, when the right-hand side is of the form ✣ ✎ ☞ ✌ ✶ ▲ ✕ ✕ ✕ ▲ ☞ ✌ a80 ◗ ☞ ✌ , and as simple constraints otherwise.

3 Undecidability of ① ② ④ ⑤ ① Implication

We show a reduction of the unrestricted tiling problem to the a0 ✁ ✄ ✆ a0 implication problem using a construction similar to that presented in [Calvanese et al., 2001]. An unrestricted tiling problem ⑥ is a triple ✩ ⑦ ▲ ⑧ ▲ ⑨ ✬ where ⑦ is a finite set of tile types and ⑧ ▲ ⑨ ✲ ⑦ ⑩ ⑦ two binary relations. A solution to ⑦ is a mapping ❶ ✎ N ⑩ N ◗ ⑦ such that ✩ ❶ ✩ ❸ ▲ ❹ ✬ ▲ ❶ ✩ ❸ ❺ ❼ ▲ ❹ ✬ ✬ ✜ ⑧ and ✩ ❶ ✩ ❸ ▲ ❹ ✬ ▲ ❶ ✩ ❸ ▲ ❹ ❺ ❼ ✬ ✬ ✜ ⑨ for all ❸ ✜ N. This problem is ❾ ❿ ❿ -complete [Berger, 1966; van Emde Boas, 1997].

O

O

o

o

/

/

O

O

o

o

/

/

O

O

�

�

o

o

/

/

�

�

o

o

/

/

�

�

Figure 2: DEFINING A GRID.

The first step in the reduction is to establish an integer grid. This can be achieved, for example, as follows.

1. Introduce four disjoint concepts, ➎ ✶ , ➎ ✺ , ➎ ➏ , and ➎ ➐ , denoting cell edges.

1. Grid cells are mapped to concepts ➟ and ➠ that have four incoming ✔ and ➡ features, respectively.

1. To ensure that squares are formed, add the following.

1. And force squares to extend to the right and up by including the following.

/

/

�

�

O

O

o

o

/

/

�

�

O

O

o

o

The accumulated effect of these inclusion dependencies on an interpretation is illustrated in Figure 2.

The adjacency rules for the instance ⑥ of the tilingproblem can now be captured, e.g., as follows:

where ⑦ ❲ corresponds to a tile type ❶ ❲ ✜ ⑦ ; we assume ⑦ ❲ ✸ ⑦ ➑ ✤ ➒ for all ❸ ➙ ❹ . The above constraints form a terminology ★ ✓ associated with an unrestricted tiling problem ⑥ .

Theorem 2 A tiling problem ⑥ admits a solution iff ★ ✓ ✕ ✖ ✒ ➟ ✸ ✩ a0 ✂ ☎ ☛ ✘ ⑦ ❲ ✬ ✤ ➒ .

Thus, the a0 ✁ ✄ ✆ a0 implication problem is undecidable for unrestricted terminologies.

4 On Recovering Decidability

In this section, we present two ways to recover decidability for the a0 ✁ ✄ ✆ a0 logical implication problem based on a syntactic prefix condition for PFDs occurring in argument terminologies and on a coherency condition for terminologies. Decidability in both cases is shown by exhibiting a reductionof logical implicationproblems in a0 ✁ ✄ ✆ a0 to decidability problems of monadic sentences in the Ackermann prefix class.

Definition 3 (Monadic Ackerman Formulae) Let ✚ ❲ be monadic predicate symbols and ❇ ▲ ❚ ❲ ▲ ✛ ❲ variables. A monadic first-order formula in the Ackermann class is a formula of the form ● ✛ ✶ ✕ ✕ ✕ ● ✛ a80 ❄ ❇ ● ❚ ✶ ✕ ✕ ✕ ● ❚ ✢ ✕ ✣ where ✣ is a quantifier-free formula over the symbols ✚ ❲ .

Every formula with the Ackermann prefix can be converted to Skolem normal form: by replacing variables ✛ ❲ by Skolem constants and ❚ ❲ by unary Skolem functions not appearing in the original formula. This, together with standard boolean equivalences, yields a finite set of universally-quantified clauses containing at most one variable ( ❇ ).

It is known that an Ackerman sentence has a model if and only if it has a Herbrand model; this allows us to use syntactic techniques for model construction. To establish the complexity bounds we use the following result for the satisfiability of Ackermann formulae:

Proposition 4 ([F¨urer, 1981]) The complexity of the satisfiability problem for Ackerman formulae is EXPTIME-complete.

4.1 Prefix-restricted PFDs

Recall that the first of our conditions is syntactic and applies to the argument PFDs occurring in a terminology. This condition complements and extends the results in [Calvanese et al., 2001]. However, because of "accidental common prefixes", it is not sufficient to follow the approach in [Calvanese et al., 2001] of simply requiring unary PFDs to resemble keys. Nonunary PFDs can also cause trouble, as the following example illustrates.

Example 5 Consider the ➨ -ary PFD

This PFD has a logical consequence ➎ ✶ ✤ ➎ ✺ ✎ ✔ ◗ ➧ and thus we can construct tiling similar to the one presented in the previous section.

The problemwith the above ➨ -ary PFD is that all the ➨ paths in the precondition have the same prefix, ✔ . To avoid this problem, it suffices to impose the following prefix condition.

Definition 6 (Prefix-restricted PFDs) Let

be an arbitrary PFDwhere ☞ ✌ is the maximal common prefix of the path expressions ❆ ☞ ✌ ☞ ✌ ✶ ▲ ✕ ✕ ✕ ▲ ☞ ✌ ☞ ✌ a80 ❊ . The PFD is prefix-restricted if either ☞ ✌ ✈ is a prefix of ☞ ✌ or ☞ ✌ is a prefix of ☞ ✌ ✈ .

The above restriction allows us to recover an almost treemodel property for the logic. By using this restriction, we are able to construct special interpretations that satisfies all constraints in a given terminology but falsify a PFD constraint whenever an interpretation exists at all-essentially, the interpretation has the shape of two trees rooted by the two elements of the domain that provide an counterexample to the given PFD. To capture the effect of equalities implied by PFDs, the two trees are allowed to share nodes that are in the range of the same path function applied to the respective roots. In addition, we are able to bound the indegree branching in such an interpretation.

Definition 7 (Rank of Implication Problem) Let ★ be a a0 ✁ ✄ ✆ a0 terminology, ✟ a constraint. We define ✦ ✧ ✩ ✪ ✩ ★ ▲ ✟ ✬ to be the number of occurrences of the ● ✔ ❍ ✶ ✕ a114 concept constructors in ★ and ✟ .

The ✦ ✧ ✩ ✪ ✩ ★ ▲ ✟ ✬ limits the maximal number of different predecessors needed to satisfy all constraints in the terminology. The above observations provide the necessary tools for describing a single Herbrand interpretation with a fixed branching outdegree using monadic sentences that simulate the (special) interpretation showing that ★ ✕ ✖ ✒ ✟ .

In the Herbrand interpretation, each term represents two elements, a left element and a right element of the original interpretation, unless these two elements are made equal by the effect of a PFD. We use the following unary predicates and function symbols:

Unary function symbols ✔ (representing a feature ✔ ) and ✔ ✶ ▲ ✕ ✕ ✕ ▲ ✔ ✬ ✭ ✮ ✰ ✁ ✱ ✝ ✳ ✡ (representing the possible inverses of ✔ ) for each feature ✔ ✜ ✡ . These function symbols are used, together with the constant ↔ denoting the two roots in the original interpretation, to form terms. We overload the notation for path descriptions and use ☞ ✌ ✩ ↔ ✬ to denote terms as well.

• Predicates a0 ✁ ✩ ❶ ✬ and a0 ✄ ✩ ❶ ✬ true for ❶ representing elements that exist in the left and right parts of the original interpretation; these emulate partiality of the inverses.
• Predicates ✚ ✁ ✆ ✩ ❶ ✬ and ✚ ✄ ✆ ✩ ❶ ✬ that are true for ❶ that represent elements belonging to the description a114 in the respective parts of the original interpretation.

Predicates ✦ ✝ ✟ ✩ ❶ ✬ true for ❶ whenever the two elements denoted by ❶ agree on ☞ ✌ in the original interpretation.

To ensure a finite number of assertions, we assume in the following that concept descriptions and features ✔ are subconcepts of concepts or are features appearing in ★ and ✟ . We call the followingcollectionof assertions ❾ ✱ (assertionswith a superscript ✡ stand for a pair of assertions, onewith ✡ substituted by ☛ and one by ☞ ):

1. Totality of features: each object must have one outgoing feature ✔ .

1. Functionality of features: Each element has at most one outgoing feature ✔ .

1. Rules of equality: equalities propagate through function application, equal nodes have the same predecessors, must exist, and must belong to the same descriptions.

1. Concept formation-boolean constructors: enforce the excluded-middle law and the correct behavior of conjunction.

1. Concept formation-value restrictions: assert value restrictions for pairs of neighboring nodes.

1. Concept formation-existential restrictions: satisfy existential restrictions for inverses. Note that in the case of the left and right sides of the interpretations agreeing, the appropriate predecessor can be on either side of the interpretation (first two assertions).

1. Satisfaction of simple constraints in the terminology (GCDs): enforce simple subsumption constraints present in ★ .

1. Satisfaction of prefix-restricted PFDs by inverses: disallow violations of prefix-restricted PFDs due to existence of multiple inverse features agreeing on a node.

for all a114 ✶ ✤ a114 ✺ ✎ ☞ ✌ ✶ ▲ ✕ ✕ ✕ ▲ ☞ ✌ a80 ◗ ☞ ✌ ✜ ★ such that ☞ ✌ ☞ ✌ ✈ ✔ ☞ ✌ ✈ ✈ is the common prefix of ☞ ✌ ✶ ▲ ✕ ✕ ✕ ▲ ☞ ✌ a80 .

1. Path agreements: extend the simple equality to assertions of two nodes agreeing on a path; this is necessary to avoid exponential blowup in the length of the path descriptions in the PFDs.

where ☞ ✌ ranges over all prefixes of path descriptions in ★ 's PFDs.

1. Prefix-restricted PFDs: enforce PFDs between the left and right parts of the interpretation.

The above assertions simulate the constraints implied by ★ . To capture the violation of the constraint ✟ we set ❾ ✳ ✒ ❆ a0 ✁ ✩ ↔ ✬ ▲ ✚ ✁ ✆ ▲ ✩ ↔ ✬ ▲ a0 ✄ ✩ ↔ ✬ ▲ ✿ ✚ ✄ ✆ ❖ ✩ ↔ ✬ ▲ ✦ a114 a115 ✩ ↔ ✬ ❊ for ✟ ordinary and ❾ ✳ ✒ ❆ a0 ✁ ✩ ↔ ✬ ▲ a0 ✄ ✩ ↔ ✬ ▲ ✚ ✁ ✆ ▲ ✩ ↔ ✬ ▲ ✚ ✄ ✆ ❖ ✩ ↔ ✬ ▲ ✦ ✝ ✟ ▲ ✩ ↔ ✬ ▲ ✕ ✕ ✕ ▲ ✦ ✝ ✟ a113 ✩ ↔ ✬ ▲ ✿ ✦ ✝ ✟ ✩ ↔ ✬ ❊ for ✟ a PFD.

Theorem 8 Let ★ be a a0 ✁ ✄ ✆ a0 terminology and ✟ a constraint. Then ★ ✒ ✟ if and only if ❾ ✱ a116 ❾ ✳ is not satisfiable.

Proof (sketch): Consider a model ✉ of ❾ ✱ a116 ❾ struct an interpretation ✇ ✒ ✩ ✴ ▲ ✩ ✕ ✬ ✭ ✬ as follows: Let ❶ ❿ ✩ ↔ ❶ ✁ ✩ ↔ ✬ , and ❶ ✄ ✩ ↔ ✬ be distinct values for each term ❶ ✩ ↔ ✬ .

✖ ✳ . We con-✬ ,

It is easy to verify that this interpretation satisfies all constraints in ★ and violates ✟ . Thus ★ ✕ ✖ ✒ ✟ .

Conversely, given an interpretation ✇ such that ✇ ✖ ✒ ★ and ✇ ✕ ✖ ✒ ✟ , we construct a model of ❾ ✱ a116 ❾ ✳ as follows.

For ✟ ✒ a114 ✶ ✤ a114 ✺ ✎ ☞ ✌ ✶ ▲ ✕ ✕ ✕ ▲ ☞ ✌ a80 ◗ ☞ ✌ a PFD, there must be elements ✂ ✶ ▲ ✂ ✺ ✜ ✴ such that ✂ ✶ ✜ ✩ a114 ✶ ✬ ✭ and ✂ ✺ ✜ ✩ a114 ✶ ✬ ✭ such that ✩ ☞ ✌ ❲ ✬ ✭ ✩ ✂ ✶ ✬ ✒ ✩ ☞ ✌ ❲ ✬ ✭ ✩ ✂ ✺ ✬ for ↔ ➙ ❸ ➜ ➨ but ✩ ☞ ✌ ✬ ✭ ✩ ✂ ✶ ✬ ✕ ✒ ✩ ☞ ✌ ✬ ✭ ✩ ✂ ✺ ✬ .

We first define a part of the interpretation that consists of successors of ✂ ✶ and ✂ ✺ :

This part of ✉ violates ✟ and satisfies all constraints in ★ with the exception of the ● ✔ ❍ ✶ ✕ ✣ . We extend ✉ to satisfy the existential restrictions as follows:

for ☞ ✌ ✩ ↔ ✬ such that ✦ a114 a115 ✩ ☞ ✌ ✩ ↔ ✬ ✬ ✕ ✜ ✉ and a0 ✁ ✩ ☞ ✌ ✩ ↔ ✬ ✬ . We chose ✆ ➜ ✦ ✧ ✩ ✪ ✩ ★ ▲ ✟ ✬ predecessors of ✩ ☞ ✌ ✬ ✭ ✩ ✂ ✶ ✬ that satisfy all implied existential restrictions. and identify these with the terms ✔ ✶ ✩ ☞ ✌ ✩ ↔ ✬ ✬ ▲ ✕ ✕ ✕ ▲ ✔ ✢ ✩ ☞ ✌ ✩ ↔ ✬ ✬ and set

for all the chosen a114 ✌ predecessors of ✩ ☞ ✌ ✬ ✭ ✩ ✂ ✶ ✬ for ↔ ➙ ❸ ➜ ✆ . For all the terms ✔ ❲ ✩ ☞ ✌ ✩ ↔ ✬ ✬ we extract a tree interpretation from ✇ . Similarly, we extend ✉ on the right side.

for ☞ ✌ ✩ ↔ ✬ such that ✦ a114 a115 ✩ ☞ ✌ ✩ ↔ ✬ ✬ ✜ ✉ we follow the same steps as above for the left part only.

Note that since ✇ satisfies ★ all (translations of) ordinary constraints are satisfied and no pair of nodes on the left/right sides can violate a prefix-restricted PFD thus satisfying constraints generated from PFDs (8-10 above).

For ✟ ✒ a114 ✶ ✤ a114 ✺ a simple constraint, there must be an element ✂ ✜ ✴ such that ✂ ✜ ✩ a114 ✶ ✬ ✭ and ✂ ✕ ✜ ✩ a114 ✺ ✬ ✭ . We define ✉ using the same process as above noting that the two roots ✂ ✶ and ✂ ✺ are already equal in ✇ . ✎

As a side-effect of the above construction, we can now transform an arbitrary interpretation that satisfies ★ and violates ✟ to an almost-tree interpretation informally referred to above in order to motivate the monadic assertions in ❾ ✱ and ❾ ✳ .

The translation, in itself polynomial, therefore provides an EXPTIME decision procedure by appealing to Proposition 4. Completeness follows from EXPTIME-hardness of the implication problem for the ❆ ✣ ✶ ✸ ✣ ✺ ▲ ❄ ✔ ✕ ✣ ❊ fragment [Toman and Weddell, 2001; 2004b].

Corollary 9 The implication problem for a0 ✁ ✄ ✆ a0 with prefix-restricted PFDs is EXPTIME-complete.

Using similar techniques, the ● ✔ ❍ ✶ ✕ a114 concept constructor can be generalized to more general number restrictions requiring lower and upper bounds (coded in binary) on the number of ✔ predecessors while still maintaining the complexity bound.

4.2 Coherent Terminologies

The second of our conditions for recovering decidability is to impose a coherency condition on terminologies themselves. The main advantage of this approach is that we thereby regain the ability for unrestricted use of PFDs in terminologies. The disadvantage is roughly that there is a "single use" restriction on using feature inversions in terminologies.

Definition 10 (Coherent Terminology) A terminology ★ is coherent if

for all descriptions ✣ ▲ ✦ that appear as subconcepts of concepts that appear in ★ , or their negations.

Note that we can syntactically guarantee that ★ is coherent by adding the ✩ ● ✔ ❍ ✶ ✕ ✣ ✬ ✸ ✩ ● ✔ ❍ ✶ ✕ ✦ ✬ ✤ ● ✔ ❍ ✶ ✕ ✩ ✣ ✸ ✦ ✬ assertions to ★ for all descriptions ✣ ▲ ✦ that appear in ★ . This restriction allows us to construct interpretations of non-PFD descriptions that have the following property:

Definition 11 An interpretation ✩ ✴ ▲ ✩ ✕ ✬ ✭ ✬ is coherent if, for any ✔ ✜ ✡ , description ✣ and ❇ ▲ ❚ ✜ ✴ , ❚ ✜ ✩ ✣ ✬ ✭ if ❇ ✜ ✩ ✣ ✬ ✭ and ✩ ✔ ✬ ✭ ✩ ❇ ✬ ✒ ✩ ✔ ✬ ✭ ✩ ❚ ✬ .

Lemma 12 Let ★ be a coherent terminology, ✟ a simple constraint, and ✇ an interpretation such that ✇ ✖ ✒ ★ and ✇ ✕ ✖ ✒ ✟ . Then there is a coherent interpretation ✇ ✈ such that ✇ ✈ ✖ ✒ ★ and ✇ ✈ ✕ ✖ ✒ ✟ .

Proof (sketch): Consider distinct ❇ ▲ ❚ ✜ ✴ ✭ such that (i) ❇ ✜ ✩ ✣ ✶ ✬ ✭ , (ii) ❚ ✜ ✩ ✣ ✺ ✬ ✭ , and (iii) ✩ ✔ ✬ ✭ ✩ ❇ ✬ ✒ ✩ ✔ ✬ ✭ ✩ ❚ ✬ . Then, since ★ is coherent, ❇ ✜ ✩ ✣ ✶ ✸ ✣ ✺ ✬ ✭ . For, ❇ ✜ ✩ ✣ ✶ ✸ ✿ ✣ ✺ ✬ ✭ leads to ✩ ✔ ❲ ✬ ✭ ✩ ❇ ✬ ✜ ✩ ● ✔ ❲ ❍ ✶ ✕ ✩ ✣ ✶ ✸ ✿ ✣ ✺ ✬ ✸ ● ✔ ❲ ❍ ✶ ✕ ✣ ✺ ✬ ✭ , a contradiction. Thus, as models of a0 ✁ ✄ ✆ have the tree model property, we can remove the farther of ❇ or ❚ and all its descendants, where the distance is measured from the node falsifying ✟ in ✇ . The resulting interpretation still satisfies ★ and falsifies ✟ . Repeating this process yields a coherent interpretation. ✎

By restricting logical implication problems for a0 ✁ ✄ ✆ a0 to cases in which terminologies are coherent, it becomes possible to apply reductions to satisfiability problems for Ackerman formulae.

Theorem 13 Let ★ be a coherent a0 ✁ ✄ ✆ a0 terminology. Then the implication problem ★ ✖ ✒ ✟ is decidable and EXPTIME-complete.

Proof (sketch): We use a reduction similar to the one for prefix-restricted terminologies. However, as the terminology is coherent, in the left and right parts of the interpretation objects can never have more then one incoming feature with the same name and thus a single inverse ✔ ✶ for ✔ ✜ ✡ is always sufficient to model this situation using the monadic formulas. Also, the left and right sides of the interpretation vacuously satisfy all PFDs (and thus the assertions in item 8 can be dropped). The interaction between PFDs and inverses is now completely captured by the auxiliary ✦ ✝ ✟ predicates. For details see [Toman and Weddell, 2004a]. ✎

Note that we cannot consider coherent interpretations only as then all PFDs would be vacuously satisfied-no two nodes could possibly agree on a common path. This would make all PFDs trivial coherent consequences (i.e., when only coherent interpretations are considered). Our coherency restriction on terminologies is weaker: it only postulates that we can avoid multiple ✔ predecessors if we wish to do so.

5 Summary and FutureWork

We have presented a pair of conditions, one syntactic and one semantic, under which it becomes possible to combine feature inversion with path-functional dependencies in a boolean complete description logic while still ensuring that the associated logical implication problem is EXPTIME-complete; the problem is shown to be undecidable otherwise. The second of these conditions resolves an open issue on decidability of an analogous implication problem in [Biskup and Polle, 2003].

A natural extension of the description logic presented here allows regular languages ( ☛ ) to replace path expressions, yielding the ❄ ☛ ✕ ✣ , ● ☛ ✕ ✣ , ● ☛ ❍ ✶ ✕ ✣ , and ✣ ✎ ☛ ◗ ☛ ✈ constructors, and developing a decision procedure using the approach in [Toman and Weddell, 2004b]. One of the main applications of such an extension we envision is describing data structures for purposes of query optimization, extending [Liu et al., 2002] to inductive data types.

Another direction of research considers weaker restrictions on a0 ✁ ✄ ✆ a0 terminologies that still guarantee decidability, e.g., relaxing our coherence condition with respect to the unary PFDs actually present in a terminology.