On Specialization Constraints over Complex Objects^{∗}

Minoru Ito

Department of Information and Computer Science

Faculty of Engineering Science

Osaka University Toyonaka, Osaka 560, Japan

Grant E. Weddell and Neil Coburn Department of Computer Science

University of Waterloo Waterloo, Ontario, Canada, N2L 3G1

Technical Report CS-91-62

∗This research was supported in part by the Ministry of Education, Science and Culture of Japan, by the Natural Sciences and Engineering Research Council of Canada, by Bell-Northern Research Ltd., Ottawa, and by ITRC: Information Technology Research Center.

2 Ito, Weddell and Coburn

Abstract

Most semantic data models and object-oriented data models allow entity and object classes to be organized according to a generalization taxonomy. In addition, range restrictions (or property typing) may be specified not only on properties associated with a given class, but also on properties inherited from superclasses. In this paper, we consider a more general form of specialization constraint in which range restrictions are associated with property value paths, instead of with the properties themselves. One consequence is that the constraints enable a form of molecular abstraction, in which the internals of more complicated objects can be defined in terms of a collection of more primitive classes.

We consider the problem for two models. The first imposes no constraints on class membership for an object beyond those implied by subclassing constraints. In this case, we present a sound and complete axiomatization for arbitrary specialization constraints, and efficient decision procedures for the corresponding membership problems.

The second model is more typical and requires that each object is created with respect to a particular class. Membership problems in this case are shown to be NP-hard, and NP-complete if class schema include a “bottom” class. We exhibit polynomial-time decision procedures when a bottom class does exist and antecedent specialization constraints satisfy a bounded path length condition.

We also consider a case concerning the second model in which class schema satisfy a lower semi-lattice condition. A sound and complete axiomatization for well-formed specialization constraints is presented, together with efficient decision procedures for the membership problem for well-formed constraints, and for determining if an arbitrary constraint is well-formed. We prove that the membership problem for arbitrary specialization constraints remains NP-complete, however, even for class schema satisfying the lower semi-lattice condition.

Key Words: complex objects, dependency theory, logical database design, object-oriented databases

Contents

1 Introduction 4 1.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2 Review and outline . . . . . . . . . . . . . . . . . . . . . . . . . 12

2 Implication Problems for Specialization Constraints 13 2.1 On finite implications . . . . . . . . . . . . . . . . . . . . . . . 13 2.2 Axioms for SCs . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.3 Decision Procedures . . . . . . . . . . . . . . . . . . . . . . . . 26

3 The Most Specialized Class Rule (MSC) 33 3.1 NP-completeness results . . . . . . . . . . . . . . . . . . . . . . 36 3.2 The case of bounded path lengths . . . . . . . . . . . . . . . . . 47

4 MSC with the Lower Semilattice Condition 54 4.1 Axiomatization . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 4.2 The three decision problems . . . . . . . . . . . . . . . . . . . . 59 4.3 An NP-completeness result . . . . . . . . . . . . . . . . . . . . 63

5 Conclusion 66

1. Introduction

Most semantic or object-oriented data models assume that entities or objects have an identity separate from any of their parts, and allow users to define complex object types in which part values may be any other objects [1, 2, 9, 13, 14, 15]. Such types are usually called classes, and can be organized in a generalization taxonomy by allowing a class definition to mention at least one superclass—more than one if the data model supports so-called multiple inheritance. In addition, range restrictions (or property typing) may be specified, not only on properties associated with a given class, but also on properties inherited from superclasses. In this paper, we consider a more general abstraction, called specialization constraints, in which range restrictions are associated with path descriptions. Specialization constraints can be used to assert property typing, since one kind of path description is an individual property name. Since another kind of path description, denoted Id, allows one to refer to property value paths of zero length, specialization constraints also abstract superclass relationships.

To concentrate on the essential ideas, we define a simple complex object model in the next subsection. An example class schema characterizing information about students and courses for a hypothetical UNIVERSITY application in terms of this model appears in Figure 1. Our diagrammatic convention is to represent each class by a labeled rectangular box, where the label mentions the class name together with a set of immediate properties; a * following a property name indicates that the property is set-valued. For example, an object in the student class has a set-valued Takes property, while each object in the course class has three single-valued properties: Inst, In and Num.

We represent specialization constraints as directed arcs between classes. The path description associated with an unlabeled arc is assumed to correspond to Id, and therefore asserts that the ‘to’ class is a superclass of the ‘from’ class. Thus, the unlabeled arc from gradCourse to course implies that each gradCourse object is also in the course class, and must therefore also have Inst, In and Num property values (although it is more common to say that gradCourse inherits these properties from course). The arc labeled Num, from course to int[100-699], represents a property typing constraint which restricts the values of the Num property for course objects. Another arc, from gradCourse to int[500-699], represents another property typing constraint which further restricts the values of the Num property for course objects that are also gradCourse objects.

Most semantic or object-oriented data models can express the organiza-

person student{Takes*}  course{Inst,In,Num} gradStudent                        gradCourse                      prof{In} dept{Head} int[100-699] int[400-699] int[500-699] Takes                              InstIn Num        In       Head Takes.Num                        Num

Figure 1: A UNIVERSITY Schema Diagram.

tion of information discussed so far in this example, without recourse to a general purpose constraint language containing arbitrary queries. However, so far as we are aware, the use of such a language would be necessary to express the specialization constraint represented by the arc labeled Takes.Num. This constraint also limits property values, but this time for a complex property of graduates, corresponding to the (set of) integers that are the course numbers of courses that they are taking. Since most models are unable to express such constraints, it is unlikely that existing query languages, or their parsers or optimizers, can benefit in any way from the use of such constraints.

To see how such constraints can be beneficial, consider a second schema, Figure 2. This schema characterizes (some of) the form of a parse tree for the relational algebra, and therefore how a query optimizer may access and update objects representing algebraic queries. First focus on the part of the schema outside of the area bounded by the dashed line. The four classes named sel, proj, join and rName represent four kinds of objects corresponding to selection, projection, and join operators, and relation names respectively. (For simplicity our discussion will ignore the project list and selection condition of the project and select operators, respectively. That is, we will only consider the expressions that these operators take as operands.) The sel and proj objects have single expressions as their Arg, while join objects have any number of expressions as their Args. The rName objects do not have properties. The part of the schema inside of the area bounded by the dashed line captures the additional structure of algebraic expressions in so-called project-select-join (PSJ) normal form. A PSJ query is a “projection of a selection of a join of a canonical expression,” where a canonical expression may in turn be a relation name or PSJ query.

    exp unExp{Arg} sel         proj                              join{Args*} rName canExp psj Arg Arg              Arg.Arg.Args Arg.ArgArgs

Figure 2: An ALGEBRA Schema Diagram.

Access to the components of a PSJ object can now be expressed more easily. For example, suppose it is known (through type checking) that a variable V references a psj object. Then, by following the generalization hierarchy (i.e. unlabeled arcs) to unExp, we find that V.Arg references an exp object. However, the arc from psj, labeled Arg, indicates that, for this subclass of unExp, Arg is actually a sel object. Thus V.Arg references a sel object; a subclass of exp. Similarly, access to the join of V’s selection can be expressed

simply as V.Arg.Arg.

It is also possible to create more sophisticated object indices. Assume that the sel and join classes have additional real-valued Selectivity and Size properties, respectively. Then one can create an index of PSJ objects sorted in order of the value of

                (Arg.Selectivity)∗(Arg.Arg.Size).

Such an index would be useful, for example, in performing join order selection.

In summary, specialization constraints also support a form of molecular abstraction useful to components of software development environments, which often require the manipulation of canonical forms. Although space prevents us from elaborating further on this, they are also useful to applications in computer aided design; they can be used to model typing information relating to the interconnection of internal components of complicated objects [4]. Finally, as the previous example illustrates, they enable more convenient object access as well as more sophisticated object encoding.

The remainder of this section is organized as follows. A formal definition of specialization constraints and the data model outlined above is presented next. Note that our definition of logical consequence will be based on a recent trend to view databases, hereafter referred to as interpretations, as labeled directed graphs [5, 6, 10, 18, 17]. We conclude with an overview of related work, and an outline of our results in the remaining sections.

1.1 Definitions A database schema is an ordered pair ⟨S, Σ⟩ consisting of a class schema and a finite set of constraints. The class schema S consists of a finite set of declarations of the form

C{P_{1}, ..., P_{n}}

in which C is a class name, and the P_{i} are its immediate properties, written Props(C). The set of class names in S is denoted Classes(S), and the domain of a property P, written Dom(P), is defined as {C ∈ Classes(S) | P ∈ Props(C)}. (Our usual convention when presenting examples will be to begin class names in lowercase and property names in uppercase.)

An interpretation for S is a (possibly infinite) labeled directed graph G(V, A). The label for a vertex v is denoted Cl(v), and corresponds to a subset of Classes(S). The label for an arc corresponds to a property name. G(V, A) must also satisfy the following condition.

A property value integrity condition: If u ⟶^{P} v ∈ A, then Cl(u) ∩ Dom(P) ≠ ∅.

The condition requires any object with one or more values for property P to be in at least one class for which P is an immediate property.

Example 1: The declarations for the ALGEBRA class schema, Figure 2, are listed in the first column of Table 1. An example interpretation for the ALGEBRA class schema appears in Figure 3. There are a total of five objects (we take the words “object” and “vertex” to be synonymous): a projection, a selection, a join and two relation names. The interpretation corresponds to (part of) the parse tree that might be produced by a query optimizer when applied to the input expression π_{X}(σ_{ρ}(R_{1} ⋈ R_{2})). □

Table 1: An ALGEBRA Schema.

S  Σ

  exp{}

  join{Args}  join(Id:exp)      join(Args:exp)
  rName{}  rName(Id:canExp)
  unExp{Arg}  unExp(Id:exp)     unExp(Arg:exp)

                                      FUNC(Arg)

  sel{}  sel(Id:unExp)
  proj{}  proj(Id:unExp)
  canExp{}  canExp(Id:exp)
  psj{}  psj(Id:proj)      psj(Arg:sel)
                    psj(Id:canExp)    psj(Arg.Arg:join)

                                      psj(Arg.Arg.Args:canExp)

A path description, pd, is either Id (short for identity), or a sequence of property names separated by dots. Their composition and length are defined as follows:

pd_{1} ∘ pd_{2} ≡ \{ \begin{matrix}pd_{1} & if pd_{2} is Id, \\ pd_{2} & if pd_{1} is Id, \\ pd_{1}.pd_{2} & otherwise. \end{matrix}

len(pd) ≡ \{ \begin{matrix}0 & if pd is Id, \\ 1 + len(pd_{1}) & otherwise, where pd has the form P ∘ pd_{1}, \\ & where P is a property. \end{matrix}

 {psj, canExp, proj, unExp, exp}  {sel, unExp, exp}  {join, exp}  {rName, canExp, exp} {rName, canExp, exp} Arg                Arg              Args Args u  v

Figure 3: An interpretation of the ALGEBRA schema.

Note that composition is associative, that is, pd_{1} ∘(pd_{2} ∘pd_{3}) = (pd_{1} ∘pd_{2})∘pd_{3}. The following is also a straightforward consequence of our definitions.

len(pd_{1} ∘ pd_{2}) = len(pd_{1}) + len(pd_{2})

Given an interpretation G(V, A), we say that a path in G(V, A) is described by a path description pd if and only if the path is of zero length (i.e. consists of a single vertex) and pd is Id, or pd corresponds to the sequence of property labels on the path.

Example 2: In Figure 3, the single path from the vertex u to the vertex v is described by the path description Arg.Arg.Args. □

We consider two kinds of constraints in Σ. The first, called a property functionality constraint (FUNC), allows us to characterize properties that are single-valued and total on their domain classes. Each is declared with the form FUNC(P), and is satisfied by an interpretation G(V, A) for S if and only if G(V, A) satisfies the following two additional conditions.

1. (property functionality) If u ⟶^{P} v and u ⟶^{P} w are in A, then v = w.

2. (property value completeness) If Cl(u) ∩ Dom(P) ≠ ∅, then there is an arc

u ⟶^{P} v ∈ A.

The second kind of constraint is called a specialization constraint (SC), and is our main concern in this paper. An SC (over S) is used to assert a type condition on a path description, and has the form C_{1}(pd : C_{2}). Assuming that S is the schema over which the constraint is expressed, then C_{1}(pd : C_{2}) is satisfied by an interpretation G(V, A) for S if and only if whenever there exists a path in G(V, A) from a vertex u to a vertex v described by pd, then C_{1} ∈ Cl(u) implies C_{2} ∈ Cl(v).

Example 3: The third entry in the third column of Table 1 is the only FUNC needed for the ALGEBRA schema. Note that this constraint is satisfied by the interpretation in Figure 3. The remaining entries in the second and third columns of Table 1 are the SCs needed for the ALGEBRA database. It is a simple exercise to confirm that each is satisfied by the interpretation for ALGEBRA given in Figure 3. Recall from our introductory comments that the entries in the second column, with the form C_{1}(Id : C_{2}), represent the superclass relationships. This should be clear from the above definitions, since such constraints distinguish interpretations in which a vertex v has C_{1} in its class label, but not C_{2}. □

Let Σ be a finite set of constraints (SCs and FUNCs). By Σ_{FUNC} and Σ_{SC}, we mean the sets of FUNCs and SCs in Σ, respectively. An instance of either kind of constraint σ is a logical consequence of Σ, written Σ ⊧ σ, if any interpretation satisfying Σ must also satisfy σ.

As discussed, specialization constraints using Id are our means of establishing a generalization taxonomy among classes. It is therefore worthwhile to distinguish database schema which fail to satisfy the usual requirement that such taxonomies be acyclic. Accordingly, we shall say that S is a generalization taxonomy with respect to Σ if and only if there are no two distinct classes C_{1}, C_{2} ∈ Classes(S) such that

Σ ⊧ C_{1}(Id : C_{2}) and Σ ⊧ C_{2}(Id : C_{1}).

However, note that we continue to allow multiple inheritance; there may exist C_{1}, C_{2}, C_{3} ∈ Classes(S) such that Σ ⊧ C_{1}(Id : C_{2}) and Σ ⊧ C_{1}(Id : C_{3}), but where Σ |̸= C_{2}(Id : C_{3}) and Σ |̸= C_{3}(Id : C_{2}). The three ALGEBRA classes psj, proj and canExp are an example of this.

The notion of a specialization constraint so far presented is very general, allowing us to express such constraints as

     exp(Arg : exp)  (1.1)

or even

     rName(Arg : exp).  (1.2)

Concerning the first example, the diagram of the ALGEBRA schema in Figure 2, together with our intuition about the information it describes, suggests that not all exp object can meaningly have an Arg property value, such as those that are also join objects. The second example is more extreme; we might expect that there will never be any rName object with an Arg property value, which implies that 1.2 is vacuously satisfied. These examples illustrate the need to be able to distinguish some kinds of path descriptions—in particular, those that correspond to single or set-valued functions which are total with respect to some class.

We begin by first defining the more restricted notion of well-formed path function [17]. A path description pd is a well-formed path function with respect to ⟨S, Σ⟩ and a class C ∈ Classes(S) if and only if for any interpretation G(V, A) satisfying Σ, whenever there is a vertex u ∈ V such that C ∈ Cl(u), then there must be a unique path in G(V, A) from u described by pd. The set of well-formed path functions with respect to ⟨S, Σ⟩ and C is denoted PathFuncs(C), where ⟨S, Σ⟩ is assumed to be understood from context.

A path description pd is well-formed with respect to ⟨S, Σ⟩ and a class C ∈ Classes(S) if and only if it is a well-formed path function with respect to ⟨S, Σ ∪ S_{FUNC}⟩ and C, where

S_{FUNC} = { FUNC(P) | P is a property in S}.

As above, the set of path descriptions that are well-formed with respect to ⟨S, Σ⟩ and C is denoted PathDescs(C). Note that that PathDescs(C) (and PathFuncs(C)) can still be countably infinite for some classes. For example, when S = { a{A} } and Σ = { a(A : a) }, then PathDescs(a) consists of Id, A, A.A, A.A.A, and so on.

We extend the concept of well-formedness to SCs. An SC C_{1}(pd : C_{2}) is well-formed with respect to ⟨S, Σ⟩ if and only if pd ∈ PathDescs(C_{1}). Finally, a finite set of constraints Σ_{1} is well-formed with respect to ⟨S, Σ⟩ if and only if every SC in Σ_{1} is well-formed with respect to ⟨S, Σ⟩.

Example 4: For the ALGEBRA schema in Table 1, PathFuncs(psj) and PathDescs(psj) denote

                       {Id, Arg, Arg.Arg}

and

                {Id, Arg, Arg.Arg, Arg.Arg.Args}

respectively. Also, both SCs 1.1 and 1.2 above are not well-formed with respect to the ALGEBRA schema, since Arg ∉ PathDescs(RName) ∪ PathDescs(exp). □

1.2 Review and outline Our form of specialization constraint is more general than the combination of subsetting and typing constraints considered by Di Battista and Lenzerini [11], although other forms of constraints are included in their theory which are not expressible in our own. Arisawa and Miura [3] consider richer forms of subclass constraints, such as C_{1} ∗ C_{2} ∗ C_{3} < C_{4} + C_{5}, which states that the intersection of (the extensions of) classes C_{1}, C_{2} and C_{3} is a subset of the union of classes C_{4} and C_{5}. They also outline polynomial time decision algorithms for cases in which either unions or intersections appear exclusively. Specialization and subsetting constraints have also been considered in the context of the relational model. Such constraints are called inclusion dependencies, and have the form R(A_{1}, ..., A_{n}) ⊆ S(B_{1}, .., B_{n}), where R and S are relation names, and A_{1}, ..., B_{n} are attribute names. The constraint is satisfied by relations r and s if the projection of r over A_{1}, ..., A_{n} is a subset of the projection of s over B_{1}, ..., B_{n}. The inference problem for inclusion dependencies is P-space complete in the general case [7], but can be solved in linear time if dependencies are unary (i.e. n = 1) [12]. Casanova et al. [7] also considered the interaction of inclusion dependencies with functional dependencies. A more general form of functional dependency, for a data model similar to the one in this paper, has been considered in Weddell [16, 17]; its interaction with specialization constraints is under study [8].

The concept of a specialization constraint, as we have defined it, was first presented in [19]. In the remainder of this paper, we expand on the results presented by this earlier work, focusing on the various membership problems for specialization constraints, including the problems of identifying well-formed path functions and path descriptions. In general, we consider these problems for two models. The first, the subject of Section 2 which follows, imposes no constraints on class membership for an object beyond those implied by subclassing constraints. An object may be a member of any set of classes as long as the superclass-subclass relationships are maintained. (An interpretation of the UNIVERSITY database schema, Figure 1, might therefore include objects in both the student and prof classes, or indeed in all classes.) For this case, we present a sound and complete axiomatization for arbitrary specialization constraints, and efficient decision procedures for the corresponding membership problems.

The second model is more typical and requires that each object is created with respect to at most one class. If the set of classes to which an object belongs is nonempty, then the set must include one class for which all other classes in the set are superclasses. In Section 3, membership problems for this model are shown to be NP-hard, and NP-complete if class schema include a “bottom” class, denoted ⊥. We exhibit polynomial-time decision procedures when ⊥ does exist and the length of any path descriptions mentioned in antecedent specialization constraints is bounded by some constant.

In Section 4, we consider another special case for the second model, in which class schema also satisfy a lower semi-lattice condition. A sound and complete axiomatization for well-formed specialization constraints is presented, together with efficient decision procedures for the membership problem for well-formed constraints, and for determining if an arbitrary constraint is well-formed. We prove that the membership problem for arbitrary specialization constraints remains NP-complete, however, even for class schema satisfying the lower semi-lattice condition.

Table 2 summarizes our complexity results for the various membership problems, and indicates those cases for which a complete axiomatization is also presented. The number in parenthesis is the subsection in which the result is derived. Further summary comments appear in Section 5.

2. Implication Problems for Specialization Constraints

2.1 On finite implications Let Σ be a finite set of constraints and let σ be an additional SC. In this section, it will be shown that σ is a logical consequence of Σ if and only if σ is a finite logical consequence of Σ. Formally, σ is a finite logical consequence of Σ, written Σ ⊧^{finite} σ, if any finite interpretation satisfying Σ must also satisfy σ. By definition, Σ ⊧ σ implies Σ ⊧^{finite} σ. In the following, we will prove its opposite direction; that is, Σ |̸= σ implies Σ |̸=^{finite} σ. Let us denote σ by C(pd : C′).

For a path description pd (= P_{1}.P_{2}. · · · .P_{n}), a pd-List (for S) is a directed graph

v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n},

where each v_{i} has a label Cl(v_{i}) that is a subset of Classes(S). If pd = Id, then the pd-List consists of a single vertex v_{0} with no arcs. Note that the pd-List is not necessarily an interpretation, since it may not satisfy a property value integrity condition.

Table 2: Complexity results for membership problems.

problem  (general case)  MSC/⊥  MSC/⊥ ; (bounded)  MSC/LSL

pd ∉ P athDescs(C)  {P-time \atop (2.3)}  NP-complete (3.1)  {P-time \atop (3.2)}  {P-time \atop (4.2)}

pd ∉ P athF uncs(C)  {P-time \atop (2.3)}  NP-complete (3.1)  {P-time \atop (3.2)}  {P-time \atop (4.2)}

\begin{matrix}Σ |̸= C(pd : C′) \\ (where pd ∈ P athDescs(C)) \end{matrix}  {P-time(*) \atop (2.3)}  NP-complete (3.1)  {P-time \atop (3.2)}  {P-time(*) \atop (4.2)}

Σ |̸= C(pd : C′)  {P-time(*) \atop (2.3)}  NP-complete (3.1)  {P-time \atop (3.2)}  NP-complete (4.3)

(*) – complete axiomatization

Lemma 1: If Σ |̸= C(pd : C′), then there is a pd-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} that satisfies the following three conditions, where pd = P_{1}.P_{2}. · · · .P_{n}.

PDL 1: The pd-List satisfies a property value integrity condition.

PDL 2: The pd-List satisfies Σ_{SC}.

PDL 3: The pd-List violates C(pd : C′); that is, C ∈ Cl(v_{0}) and C′ ∉ Cl(v_{n}).

Proof. Assume that Σ |̸= C(pd : C′). Then there is an interpretation G(V, A) that satisfies Σ but violates C(pd : C′). That is, there is a path in G(V, A) from a vertex u to a vertex v described by pd such that C ∈ Cl(u) but C′ ∉ Cl(v). The path can be denoted u_{0} ⟶^{P_{1}} u_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} u_{n}, where u_{0} = u and u_{n} = v.^{1} Let v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} be a pd-List such that Cl(v_{i}) = Cl(u_{i}) for 0 ≤ i ≤ n. We will prove that the pd-List satisfies PDLs 1 to 3.

Since G(V, A) is an interpretation, it satisfies a property value integrity condition. Thus it holds that Cl(u_{i−1}) ∩ Dom(P_{i}) ≠ ∅ for 1 ≤ i ≤ n. Since Cl(v_{i−1}) = Cl(u_{i−1}) by definition, the pd-List also satisfies a property value integrity condition; that is, PDL 1 holds.

1A vertex u_{i} may coincide with another u_{j}, since G(V, A) may contain cycles.

Since G(V, A) satisfies Σ_{SC} (⊆ Σ) and the path u_{0} ⟶^{P_{1}} u_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} u_{n} is a subgraph of G(V, A), the path must satisfy Σ_{SC}. Thus the pd-List also satisfies Σ_{SC}; that is, PDL 2 holds.

Since C ∈ Cl(u_{0}) = Cl(v_{0}) and C′ ∉ Cl(u_{n}) = Cl(v_{n}), the pd-List violates C(pd : C′); that is, PDL 3 holds. This completes proving Lemma 1. □

Example 5: Let S be a class schema defined as follows:

a_{1}{ C }, a_{2}{ }, a_{3}{ B }, b{ A,D }, c_{1}{ }, c_{2}{ }, e{ C }, where

    Dom(A) = { b }, Dom(B) = { a_{3} }, Dom(C) = { a_{1},e }, Dom(D)

= { b }. Let Σ_{SC} consist of the following seven SCs:

    a_{1}(Id:a_{2}), a_{1}(C:c_{2}), a_{2}(Id:a_{3}), a_{3}(B:b), b(A:a_{2}), c_{1}(Id:c_{2}),
e(C:c_{2}).

Assume that Σ_{FUNC} = ∅. The database schema ⟨S, Σ⟩ can be illustrated as in Figure 4.

              a_{3}{B}_{a_{2}} a_{1}{C}  b{A,D}_{c_{2}}_{c_{1}}  e{C} B          A C             C

Figure 4: A database schema ⟨S, Σ⟩.

Let us consider whether or not Σ ⊧ a_{2}(B.A.C:c_{1}). To say the conclusion first, it holds that Σ |̸= a_{2}(B.A.C:c_{1}). In fact, for the SC a_{2}(B.A.C:c_{1}), there is a ‘B.A.C’-List v_{0} ⟶^{B} v_{1} ⟶^{A} v_{2} ⟶^{C} v_{3} satisfying PDLs 1 to 3, as is given in Figure 5. □

{a_{2},a_{3}}  {b}  {a_{2},a_{3},e}  {c_{2}} B                 A                   C v_{0}  v_{1}  v^{2}  v_{3}

Figure 5: A ‘B.A.C’-List.

The pd-List obtained in Lemma 1 does not necessarily satisfy Σ_{FUNC}, though it satisfies Σ_{SC}. Note that if the pd-List does not satisfy Σ_{FUNC}, then there is a vertex v_{i} that violates property value completeness for some FUNC(P) ∈ Σ_{FUNC}; that is, Cl(v_{i}) ∩ Dom(P) ≠ ∅ but v_{i} has no out-arc labeled P.^{2} By adding one vertex and a number of arcs to the pd-List, however, we can construct an interpretation G(V, A) that satisfies Σ ∪ S_{FUNC}.^{3} Let us first consider how to construct such an interpretation.

Let v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} be a pd-List, where pd = P_{1}.P_{2}. · · · .P_{n}.

The augmented graph of the pd-List with respect to S is a directed graph G(V, A) obtained by the following procedure.

Procedure 1: (Computing the augmented graph G(V, A) of a pd-List with respect to S.) input: a database schema ⟨S, Σ⟩ and a pd-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n}.

1. Assign the pd-List to G(V, A).

2. Add a new vertex u to V, where Cl(u) = Classes(S).

3. For each property P in S and each v_{i}, where 0 ≤ i ≤ n, if Cl(v_{i})∩Dom(P) ≠ ∅ and v_{i} has no out-arc labeled P, then add an arc v_{i} ⟶^{P} u to A.

4. For each property P in S, add an arc u ⟶^{P} u to A. □

Example 6: Let us consider how to construct the augmented graph G(V, A) of the ‘B.A.C’-List v_{0} ⟶^{B} v_{1} ⟶^{A} v_{2} ⟶^{C} v_{3} in Figure 5 with respect to S.

In Step 1, a vertex u with Cl(u) = Classes(S) is added to V. Since b ∈ Cl(v_{1}) ∩ Dom(D), an arc v_{2} ⟶^{B} u is added to A in Step 3. Similarly, since a_{3} ∈ Cl(v_{2}) ∩ Dom(B), an arc v_{2} ⟶^{B} u is also added to A in Step 3. Since S consists of four properties A,B,C,D, four arcs (such as u ⟶^{A} u) is added to A in Step 4. As a result, the augmented graph G(V, A) is constructed as in Figure 6. It is important to note that G(V, A) is a finite interpretation satisfying Σ ∪ S_{FUNC} but violating a_{2}(B.A.C:c_{1}), where S_{FUNC} = { FUNC(A), FUNC(B), FUNC(C), FUNC(D) }. Thus it turns out that Σ |̸=^{finite} a_{2}(B.A.C:c_{1}). Note that there is an infinite interpretation for S satisfying Σ, because of a

2Since each vertex in the pd-List has at most one out-arc, it satisfies property functionality.

3Note that ΣFUNC ⊆ SFUNC by definition.

cycle a_{2}(Id:a_{3}), a_{3}(B:b), b(A:a_{2}).  □

{a_{2},a_{3}}  {b}  {a_{2},a_{3},e}  {c_{2}} B                 A                   C v_{0}  v_{1}  v^{2}  v_{3} Classes(S) D            B u  A,B,C,D

Figure 6: The augmented graph of the ‘B.A.C’-List in Figure 5.

Lemma 2: If the pd-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} satisfies PDLs 1 to 3, then its augmented graph G(V, A) with respect to S is a finite interpretation satisfying Σ ∪ S_{FUNC} but violating C(pd : C′).

Proof. Clearly, G(V, A) is finite. In order to prove that G(V, A) is an interpretation, it suffices to show that G(V, A) satisfies a property value integrity condition. This is true as explained below: For each v_{i−1} ⟶^{P_{i}} v_{i} ∈ A, it holds that Cl(v_{i−1}) ∩ Dom(P_{i}) ≠ ∅, since the pd-List satisfies a property value integrity condition by PDL 1. For each v_{i} ⟶^{P} u added to A in Step 3, it follows from the if condition in Step 3 that Cl(v_{i}) ∩ Dom(P) ≠ ∅. Furthermore, for each u ⟶^{P} u added to A in Step 4, it also follows that Cl(u) ∩ Dom(P) ≠ ∅, since Cl(u) = Classes(S). Thus G(V, A) satisfies a property value integrity condition.

We next prove that G(V, A) satisfies Σ ∪ S_{FUNC}. By construction, it is clear that G(V, A) satisfies FUNC(P) for every property P in S. It remains to show that G(V, A) satisfies Σ_{SC}. For an SC C_{1}(pd′ : C_{2}) ∈ Σ_{SC}, assume that there is a path in G(V, A) from a vertex w to a vertex w′ described by pd′ such that C_{1} ∈ Cl(w). It suffices to show that C_{2} ∈ Cl(w′). If w′ = u, then this is true, since Cl(u) = Classes(S) by definition. Assume that w′ ≠ u. Since the destination of every arc added in Steps 3 and 4 is the new vertex u, the assumption w′ ≠ u implies that the path from w to w′ must be on the pd-List. Since the pd-List satisfies C_{1}(pd′ : C_{2}) ∈ Σ_{SC} by PDL 2, C_{1} ∈ Cl(w) implies C_{2} ∈ Cl(w′).

Finally, G(V, A) violates C(pd : C′), since the pd-List is a subgraph of G(V, A) and violates the SC by PDL 3. This completes proving Lemma 2. □

We are now ready to prove the following theorem.

Theorem 1: The following three statements are equivalent.

1. Σ |̸= C(pd : C′).

2. Σ |̸=^{finite} C(pd : C′).

3. There is a pd-List satisfying PDLs 1 to 3.

Proof. By definition, (2) implies (1). By Lemma 1, (1) implies (3). We prove that (3) implies (2). Assume that there is a pd-List satisfying PDLs 1 to 3. Let G(V, A) be the augmented graph of the pd-List with respect to S. Since Σ ⊆ Σ ∪ S_{FUNC}, it follows from Lemma 2 that G(V, A) is a finite interpretation satisfying Σ but violating C(pd : C′). Hence Σ |̸=^{finite} C(pd : C′). □

2.2 Axioms for SCs Let Σ be a finite set of constraints and let σ be an SC. For a finite set A of axioms, if σ is derivable from Σ using the axioms in A, then we denote Σ ⊢_{A} σ (or Σ ⊢ σ, if A is understood from context). In this section, we will show the following result.

The following axioms A1 to A3 are sound and complete for deciding whether or not Σ ⊧ σ; that is, Σ ⊧ σ if and only if Σ ⊢_{{A1,A2,A3}} σ. In particular, if σ is well-formed with respect to ⟨S, Σ⟩, then only A1 and A2 are sound and complete.

A1: (identity) If C ∈ Classes(S), then C(Id : C).

A2: (composition) If C(pd : C′) and C′(pd′ : C′′), then C(pd ∘ pd′ : C′′).

A3: (prefix augmentation) For a property P, if C_{p}(P ∘ pd : C′) for every C_{p} ∈ Dom(P), then C(pd′ ∘ P ∘ pd : C′) for every C ∈ Classes(S) and every path description pd′.

Lemma 3: Axioms A1 to A3 are sound; that is, Σ ⊢ σ implies Σ ⊧ σ.

Proof. Clearly, A1 and A2 are sound. Consider A3. Assume that an interpretation G(V, A) satisfies C_{p}(P ∘ pd : C′) for every C_{p} ∈ Dom(P). We must show that G(V, A) satisfies C(pd′ ∘ P ∘ pd : C′). Assume that there is a path in G(V, A) from a vertex u to a vertex v described by pd′ ∘ P ∘ pd such that C ∈ Cl(u). It suffices to show that C′ ∈ Cl(v). The path can be divided into two parts: one path from u to a vertex w described by pd′ and the other from w to v described by P ∘ pd. Since (1) G(V, A) satisfies a property value integrity condition and (2) w has an out-arc labeled P, it holds that Cl(w) ∩ Dom(P) ≠ ∅. Let C_{p} ∈ Cl(w) ∩ Dom(P). Then G(V, A) satisfies C_{p}(P ∘ pd : C′) by assumption. Furthermore, since there is a path in G(V, A) from w to v described by P ∘ pd, C_{p} ∈ Cl(w) implies C′ ∈ Cl(v). □

Example 7: Consider the database schema ⟨S, Σ⟩ of Example 5. For property C, where Dom( C ) = { a_{1}, e }, both a_{1}(C:c_{2}) and e(C:c_{2}) are in Σ. Thus by axiom A3, an SC b(D.C:c_{2}) is derived from Σ. Similarly, an SC a_{2}(B.A.C:c_{2}) is also derived from Σ by axiom A3. □

In the following we will prove completeness of the axioms; that is, Σ ⊬ σ implies Σ |̸= σ. Let us denote σ by C(pd : C′). The proof will be done by showing that if Σ ⊬ C(pd : C′), then there is a pd-List satisfying PDLs 1 to 3, and thus Σ |̸= C(pd : C′) by Theorem 1. In order to construct such a pd-List, we will introduce the concept of chase, which is a pd-List satisfying Σ_{SC} for a class C ∈ Classes(S) and a path description pd.

The chase of C and pd under Σ_{SC}, written Chase_{ΣSC}(C, pd), is a pd-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} obtained by the following procedure, where pd = P_{1}.P_{2}. · · · .P_{n}.

Procedure 2: (Computing Chase_{ΣSC}(C, pd).) input: a database schema ⟨S, Σ⟩, a class C ∈ Classes(S), and a path description pd (= P_{1}.P_{2}. · · · .P_{n}).

1. Construct a pd-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} such that Cl(v_{0}) = { C } and Cl(v_{i}) = ∅ for 1 ≤ i ≤ n.

2. Apply the following rule to the pd-List exhaustively:

SC-rule: For an SC C_{a}(pd′ : C_{b}) ∈ Σ_{SC}, if there are two vertices v_{i}, v_{j} such that C_{a} ∈ Cl(v_{i}), C_{b} ∉ Cl(v_{j}), and pd′ = P_{i+1}.P_{i+2}. · · · .P_{j}, then add C_{b} to Cl(v_{j}).^{4} □

Example 8: For the database schema ⟨S, Σ⟩ in Example 5, let us compute Chase_{ΣSC}(a_{2}, B.A.C).

In Step 1, a ‘B.A.C’-List v_{0} ⟶^{B} v_{1} ⟶^{A} v_{2} ⟶^{C} v_{3} is constructed, where Cl(v_{0}) = { a_{2} } and Cl(v_{i}) = ∅ for 1 ≤ i ≤ 3.

For SC a_{2}(Id : a_{3}) ∈ Σ_{SC}, since a_{2} ∈ Cl(v_{0}) and a_{3} ∉ Cl(v_{0}), class a_{3} is added to Cl(v_{0}) by applying the SC-rule for a_{2}(Id:a_{3}). Then by applying the SC-rule for a_{3}(B : b) ∈ Σ_{SC}, class b is added to Cl(v_{1}), since a_{3} ∈ Cl(v_{0}) and b ∉ Cl(v_{1}). Finally, we obtain the ‘B.A.C’-List given in Figure 7 as Chase_{ΣSC}(a_{2}, B.A.C). Note that Chase_{ΣSC}(a_{2}, B.A.C) satisfies Σ_{SC}. □

{a_{2},a_{3}}  {b}  {a_{2},a_{3}}  ∅ B                 A                   C v_{0}  v_{1}  v^{2}  v_{3}

Figure 7: Chase_{ΣSC}(a_{2}, B.A.C).

Note that the result of Procedure 2 is independent of the order of applying SC-rules in Step 2.

Let us first consider the case that C(pd : C′) is well-formed with respect to ⟨S, Σ⟩; that is, pd ∈ PathDescs(C). We want to show that if Σ ⊬_{{A1,A2}} C(pd : C′), then Chase_{ΣSC}(C, pd) satisfies PDLs 1 to 3. We will present three lemmas, which will be used for the chase to satisfy the three conditions.

Assume in the rest of this section that pd = P_{1}.P_{2}. · · · .P_{n} and that the result of Chase_{ΣSC}(C, pd) is v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n}, unless stated otherwise. Furthermore, let us denote a prefix P_{1}.P_{2}. · · · .P_{i} of pd by pd_{i}, where 0 ≤ i ≤ n.^{5} Lemma 4: (a) The pd_{i}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} v_{i} satisfies Σ_{SC}, where 0 ≤ i ≤ n. In particular, Chase_{ΣSC}(C, pd) satisfies Σ_{SC}.

4If pd′ = Id, then let i = j.

5Note that pd_{0} = Id and pd_{n} = pd.

(b) Chase_{ΣSC}(C, pd_{i}) coincides with the pd_{i}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} v_{i}, where 0 ≤ i ≤ n.

Proof. By definition, if a pd-List does not satisfy an SC in Σ_{SC}, then the SCrule for the SC must apply to the pd-List. In order to compute Chase_{ΣSC}(C, pd), SC-rules for Σ_{SC} have been exhaustively applied, and thus Chase_{ΣSC}(C, pd) satisfies Σ_{SC}. Hence the pd_{i}-List also satisfies Σ_{SC}, since it is a subgraph of Chase_{ΣSC}(C, pd). That is, Lemma 4(a) holds.

We next prove Lemma 4(b). Since the order of applying SC-rules in Step 2 does not affect the final result, Procedure 2 can yield, as an intermediate result,

a pd-List v′_{0} ⟶^{P_{1}} v′_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v′_{n} such that (1) Cl(v′_{j}) = ∅ for i + 1 ≤ j ≤ n

and (2) the pd_{i}-List v′_{0} ⟶^{P_{1}} v′_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} v′_{i} satisfies Σ_{SC}. Clearly, the pd_{i}-List coincides with Chase_{ΣSC}(C, pd_{i}). On the other hand, by the definition of SCrule, once v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} v_{i} satisfies Σ_{SC} in Step 2, the pd_{i}-List remains unchanged afterward. Hence Lemma 4(b) holds. □

Lemma 5: Cl(v_{i}) = {C_{i} ∈ Classes(S) | Σ_{SC} ⊢_{{A1,A2}} C(pd_{i} : C_{i})} for 0 ≤ i ≤ n.

Proof. We first prove that if Σ_{SC} ⊢_{{A1,A2}} C(pd_{i} : C_{i}), then C_{i} ∈ Cl(v_{i}). Assume that Σ_{SC} ⊢_{{A1,A2}} C(pd_{i} : C_{i}). Then Σ_{SC} ⊧ C(pd_{i} : C_{i}) by Lemma 3. Thus Chase_{ΣSC}(C, pd) satisfies C(pd_{i} : C_{i}) by Lemma 4(a). Hence C ∈ Cl(v_{0}) implies C_{i} ∈ Cl(v_{i}).

We next prove that if C_{i} ∈ Cl(v_{i}), then Σ_{SC} ⊢_{{A1,A2}} C(pd_{i} : C_{i}). Induction on the number of applying SC-rules in Step 2.

The basis follows from axiom A1, since Cl(v_{0}) = { C } and Cl(v_{j}) = ∅ for 1 ≤ j ≤ n in Step 1.

As an induction hypothesis, assume during an execution of Step 2 that Σ_{SC} ⊢_{{A1,A2}} C(pd_{i} : C_{i}) for every C_{i} ∈ Cl(v_{i}). Assume that a class C_{b} should be added to Cl(v_{j}) by applying an SC-rule for C_{a}(pd′ : C_{b}) ∈ Σ_{SC}. Then by the definition of SC-rule, it holds that C_{b} ∉ Cl(v_{j}), C_{a} ∈ Cl(v_{k}), and pd′ = P_{k+1}.P_{k+2}. · · · .P_{j} for some k. We must prove that Σ_{SC} ⊢_{{A1,A2}} C(pd_{j} : C_{b}). By the induction hypothesis, C_{a} ∈ Cl(v_{k}) implies that Σ_{SC} ⊢_{{A1,A2}} C(pd_{k} : C_{a}). By axiom A2, C(pd_{k} : C_{a}) and C_{a}(pd′ : C_{b}) imply C(pd_{k} ∘pd′ : C_{b}). Note that pd_{k} ∘ pd′ = pd_{j}. Hence Σ_{SC} ⊢_{{A1,A2}} C(pd_{j} : C_{b}). This completes proving Lemma 5. □

Lemma 6: pd ∈ PathDescs(C) if and only if Chase_{ΣSC}(C, pd) satisfies a property value integrity condition.

Proof. \underline{If part.} Induction on len(pd).

Basis. If len(pd) = 0, that is pd = Id, then clearly pd ∈ PathDescs(C). Hence the basis holds.

Induction. As an induction hypothesis, assume that if len(pd) ≤ n − 1 and Chase_{ΣSC}(C, pd) satisfies a property value integrity condition, then pd ∈ PathDescs(C), where n ≥ 1.

Assume that len(pd) = n and Chase_{ΣSC}(C, pd) satisfies a property value integrity condition. Then it holds that Cl(v_{i−1}) ∩ Dom(P_{i}) ≠ ∅ for 1 ≤ i ≤ n. In particular, there is a class C_{n−1} ∈ Classes(S) such that

C_{n−1} ∈ Cl(v_{n−1}) ∩ Dom(P_{n}). (2.1)

Let G(V, A) be an interpretation satisfying Σ ∪ S_{FUNC}. Let u be a vertex in V such that C ∈ Cl(u). In order to prove that pd ∈ PathDescs(C), it suffices to show that there is a path in G(V, A) from u described by pd. We claim that

pd_{n−1} ∈ PathDescs(C). (2.2)

Since len(pd_{n−1}) = n − 1, it follows from the induction hypothesis that if Chase_{ΣSC}(C, pd_{n−1}) satisfies a property value integrity condition, then 2.2 holds. Thus it suffices to show that Chase_{ΣSC}(C, pd_{n−1}) satisfies a property value integrity condition. By Lemma 4(b), Chase_{ΣSC}(C, pd_{n−1}) coincides with the pd_{n−1}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n−1}} v_{n−1}. Furthermore, the pd_{n−1}-List satisfies a property value integrity condition, since Chase_{ΣSC}(C, pd) satisfies that condition by assumption and pd_{n−1} is a prefix of pd. Hence 2.2 holds.

By 2.2, there must be a path in G(V, A) from u to a vertex w described by pd_{n−1}.^{6} We next claim that

Cl(w) ∩ Dom(P_{n}) ≠ ∅. (2.3)

By 2.1, it suffices to show that C_{n−1} ∈ Cl(w). Since C_{n−1} ∈ Cl(v_{n−1}) by 2.1, it follows from Lemma 5 that Σ ⊢_{{A1,A2}} C(pd_{n−1} : C_{n−1}), and thus Σ ⊧ C(pd_{n−1} : C_{n−1}) by Lemma 3. This implies that G(V, A) satisfies C(pd_{n−1} : C_{n−1}), since G(V, A) satisfies Σ. Note that C ∈ Cl(u) and there is a path in G(V, A) from u to w described by pd_{n−1}. Hence it must hold that C_{n−1} ∈ Cl(w), which implies 2.3.

6Since G(V, A) satisfies SFUNC, the vertex w is unique.

Since G(V, A) satisfies FUNC(P_{n}) ∈ S_{FUNC}, it follows from 2.3 and property value completeness for FUNC(P_{n}) that there must be an arc w ⟶^{P_{n}} w′ ∈ A. Furthermore, since there is a path in G(V, A) from u to w described by pd_{n−1}, there is also a path in G(V, A) from u to w′ described by pd_{n−1} ∘ P_{n} (= pd). This completes the induction proof of the if part.

\underline{Only if part.} Assume that Chase_{ΣSC}(C, pd) does not satisfy a property value integrity condition. (We will prove that pd ∉ PathDescs(C).) Then there is an index i such that

Cl(v_{i}) ∩ Dom(P_{i+1}) = ∅, (2.4)

where 0 ≤ i ≤ n − 1. Let i be the smallest index satisfying 2.4. For the pd_{i}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} v_{i}, construct the augmented graph G(V, A) with respect to S. We will prove that G(V, A) is an example showing that pd ∉ PathDescs(C). It suffices to show that (1) G(V, A) is an interpretation satisfying Σ ∪ S_{FUNC} and (2) there is no path in G(V, A) from v_{0} described by pd. Note that C ∈ Cl(v_{0}).

By the minimality of i, it holds that Cl(v_{j}) ∩ Dom(P_{j+1}) ≠ ∅ for 0 ≤ j ≤ i − 1. Thus the pd_{i}-List satisfies a property value integrity condition. Furthermore, since the pd_{i}-List satisfies Σ_{SC} by Lemma 4(a), it follows from Lemma 2 that G(V, A) is an interpretation satisfying Σ ∪ S_{FUNC}.

Clearly, there is a path in G(V, A) from v_{0} to v_{i} described by pd_{i}. Note that the path is unique, since G(V, A) satisfies S_{FUNC}. By Step 3 of Procedure 1, if there is an arc v_{i} ⟶^{P} u ∈ A, then Cl(v_{i}) ∩ Dom(P) ≠ ∅. Hence it follows from 2.4 that there is no arc v_{i} ⟶^{P_{i+1}} u ∈ A. That is, there is no path in G(V, A) from v_{0} described by pd_{i} ∘ P_{i+1}. Since pd_{i} ∘ P_{i+1} is a prefix of pd, there is no path in G(V, A) from v_{0} described by pd, either. This completes proving the only if part. Hence Lemma 6 holds. □

Example 9: Consider Chase_{ΣSC}(a_{2}, B.A.C), given in Figure 7, for the database schema ⟨S, Σ⟩ of Example 5. Then Chase_{ΣSC}(a_{2}, B.A.C) does not satisfy a property value integrity condition, since Cl(v_{2}) ∩ Dom(C) = ∅. Thus B.A.C ∉ PathDescs(a_{2}) by Lemma 6. On the other hand, Chase_{ΣSC}(a_{2}, B.A) satisfies a property value integrity condition, since a_{3} ∈ Cl(v_{0}) ∩ Dom(B) and a_{2} ∈ Cl(v_{1}) ∩ Dom(A). Thus B.A ∈ PathDescs(a_{2}) by Lemma 6. □

We are now ready to prove the following theorem.

Theorem 2: If pd ∈ PathDescs(C), then the following three statements are equivalent.^{7}

1. Σ ⊧ C(pd : C′).

2. Σ ⊢_{{A1,A2}} C(pd : C′).

3. C′ ∈ Cl(v_{n}).

Proof. By Lemma 3, (2) implies (1). By Lemma 5, (3) implies (2). We prove that (1) implies (3); that is, if C′ ∉ Cl(v_{n}), then Σ |̸= C(pd : C′). By Theorem 1, it suffices to show that if C′ ∉ Cl(v_{n}), then Chase_{ΣSC}(C, pd) satisfies PDLs 1 to 3.

Since pd ∈ PathDescs(C), PDL 1 follows from Lemma 6. PDL 2 follows from Lemma 4(a). Finally, since C ∈ Cl(v_{0}) by definition, if C′ ∉ Cl(v_{n}), then Chase_{ΣSC}(C, pd) violates C(pd : C′); that is, PDL 3 follows. □

Finally, let us consider the case that pd is not necessarily in PathDescs(C). Then we have the following theorem, which is a generalization of Theorem 2.

Theorem 3: The following three statements are equivalent.

1. Σ ⊧ C(pd : C′).

2. Σ ⊢_{{A1,A2,A3}} C(pd : C′).

3. At least one of the following two conditions holds.

Condition A: Σ ⊢_{{A1,A2}} C(pd : C′).

Condition B: For some i such that 0 ≤ i ≤ n − 1, Σ ⊢_{{A1,A2}} C_{i}(P_{i+1}.P_{i+2}. · · · .P_{n} : C′) for every C_{i} ∈ Dom(P_{i+1}).

Proof. By Lemma 3, (2) implies (1). We next prove that (3) implies (2).

Clearly, Condition A implies (2). Assume that Condition B holds. Then by axiom A3, for every C′′ ∈ Classes(S) and every path description pd′,

Σ ⊢_{{A1,A2,A3}} C′′(pd′ ∘ P_{i+1}.P_{i+2}. · · · .P_{n} : C′). In particular, by letting C′′ = C and pd′ = pd_{i},

Σ ⊢_{{A1,A2,A3}} C(pd : C′). Hence Condition B also implies (2). As a result, (3) implies (2).

Finally, we prove that (1) implies (3) by induction on len(pd).

7Σ is not necessarily well-formed with respect to ⟨S, Σ⟩.

Basis. If len(pd) = 0, that is pd = Id, then clearly pd ∈ PathDescs(C). Thus (1) implies Condition A by Theorem 2. Hence the basis holds.

Induction. As an induction hypothesis, assume that for any SC C(pd : C′), if len(pd) ≤ n − 1, then (1) implies (3). Assume that len(pd) = n. In the following we will prove that if C(pd : C′) satisfies neither Condition A nor B, then Σ |̸= C(pd : C′). (Thus it will turn out that (1) implies (3).)

Assume that C(pd : C′) satisfies neither Condition A nor B. The negation of Condition A is that

Σ ⊬_{{A1,A2}} C(pd : C′). (2.5)

The negation of Condition B is that for every i such that 0 ≤ i ≤ n − 1,

Σ ⊬_{{A1,A2}} C_{i}(P_{i+1}.P_{i+2}. · · · .P_{n} : C′) for some C_{i} ∈ Dom(P_{i+1}). (2.6)

There are two cases to be considered: C ∈ Dom(P_{1}) and C ∉ Dom(P_{1}).

Case 1. Assume that C ∈ Dom(P_{1}). For simplicity, let pd′ = P_{2}.P_{3}. · · · .P_{n}. By 2.6, there is a class C_{1} ∈ Dom(P_{2}) such that

Σ ⊬_{{A1,A2}} C_{1}(pd′ : C′). (2.7)

We claim that

Σ |̸= C_{1}(pd′ : C′). (2.8)

Since len(pd′) = n − 1, it follows from the induction hypothesis that if C_{1}(pd′ : C′) satisfies neither Condition A nor B, then 2.8 holds. Hence it suffices to show that C_{1}(pd′ : C′) satisfies neither Condition A nor B. By 2.7, C_{1}(pd′ : C′) does not satisfy Condition A. Furthermore, by ignoring the case of i = 0 in 2.6, we notice that C_{1}(pd′ : C′) does not satisfy Condition B, either. This completes proving 2.8.

By 2.8 and Theorem 1, there is a pd′-List u_{1} ⟶^{P_{2}} u_{2} ⟶^{P_{3}} ⋯ ⟶^{P_{n}} u_{n} satisfying PDLs 1 to 3. Let w_{0} ⟶^{P_{1}} w_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} w_{n} be a pd-List such that Cl(w_{0}) = Cl(v_{0}) and Cl(w_{i}) = Cl(u_{i}) ∪ Cl(v_{i}) for 1 ≤ i ≤ n. By Theorem 1, in order to prove that Σ |̸= C(pd : C′), it suffices to show that the pd-List

w_{0} ⟶^{P_{1}} w_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} w_{n} satisfies PDLs 1 to 3.

As for PDL 1, it suffices to show that Cl(w_{i−1}) ∩ Dom(P_{i}) ≠ ∅ for 1 ≤ i ≤ n. If i = 0, then Cl(w_{0}) ∩ Dom(P_{1}) ≠ ∅, since C ∈ Cl(v_{0}) = Cl(w_{0}) and C ∈ Dom(P_{1}). Assume that i ≥ 1. Since the pd′-List u_{1} ⟶^{P_{2}} u_{2} ⟶^{P_{3}} ⋯ ⟶^{P_{n}} u_{n} satisfies PDL 1, it holds that Cl(u_{i}) ∩ Dom(P_{i+1}) ≠ ∅. Since Cl(u_{i}) ⊆ Cl(w_{i}), it holds that Cl(w_{i}) ∩ Dom(P_{i+1}) ≠ ∅. Hence PDL 1 holds.

As for PDL 2, assume that there is an SC C_{a}(P_{j}.P_{j+1}. · · · .P_{k} : C_{b}) ∈ Σ_{SC} such that C_{a} ∈ Cl(w_{j}), where 0 ≤ j ≤ k ≤ n. It suffices to show that C_{b} ∈ Cl(w_{k}). If C_{a} ∈ Cl(v_{j}), then C_{b} ∈ Cl(v_{k}) ⊆ Cl(w_{k}), since Chase_{ΣSC}(C, pd) satisfies C_{a}(P_{j}.P_{j+1}. · · · .P_{k} : C_{b}) ∈ Σ_{SC} by Lemma 4(a). On the other hand, if C_{a} ∈ Cl(u_{j}), then C_{b} ∈ Cl(u_{k}) ⊆ Cl(w_{k}), since the pd′-List u_{1} ⟶^{P_{2}} u_{2} ⟶^{P_{3}} ⋯ ⟶^{P_{n}} u_{n} satisfies C_{a}(P_{j}.P_{j+1}. · · · .P_{k} : C_{b}) ∈ Σ_{SC} by PDL 2. Hence PDL 2 holds.

Finally, since the pd′-List u_{1} ⟶^{P_{2}} u_{2} ⟶^{P_{3}} ⋯ ⟶^{P_{n}} u_{n} satisfies PDL 3, it holds that C′ ∉ Cl(u_{n}). Furthermore, C′ ∉ Cl(v_{n}) by 2.5 and Lemma 5. Since Cl(w_{n}) = Cl(v_{n}) ∪ Cl(u_{n}), it holds that C′ ∉ Cl(w_{n}). On the other hand, C ∈ Cl(v_{0}) implies C ∈ Cl(w_{0}). Hence PDL 3 holds. This completes Case 1.

Case 2. Assume that C ∉ Dom(P_{1}). By 2.6, there is a class C_{0} ∈ Dom(P_{1}) such that Σ ⊬_{{A1,A2}} C_{0}(pd : C′). Since C_{0} ∈ Dom(P_{1}), it follows from Case 1 above that

Σ ⊬_{{A1,A2}} C_{0}(pd : C′) implies Σ |̸= C_{0}(pd : C′).

Thus by Theorem 1, there is a pd-List u_{0} ⟶^{P_{1}} u_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} u_{n} satisfying PDLs 1 to 3. Let w_{0} ⟶^{P_{1}} w_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} w_{n} be a pd-List such that Cl(w_{i}) = Cl(u_{i}) ∪ Cl(v_{i}) for 0 ≤ i ≤ n. It can be proved in the same way as in Case 1 that the latter pd-List satisfies PDLs 1 to 3. Hence Σ |̸= C(pd : C′) by Theorem 1. This completes the induction proof that (1) implies (3). Consequently, Theorem 3 holds. □

2.3 Decision Procedures In this section, we will prove the following theorem.

Theorem 4: The following three decision problems can be solved in O(D · (len(pd) + 1)) time, where D is the size of database schema ⟨S, Σ⟩.

a. pd ∈ PathDescs(C) ?

b. pd ∈ PathFuncs(C) ?

c. Σ ⊧ C(pd : C′) ? □

To say the conclusion first, the time for computing Chase_{ΣSC}(C, pd) dominates the time complexities of the three decision problems. Let us present a procedure for computing Chase_{ΣSC}(C, pd), which is a refinement of Procedure 2, and then estimate its computation time. In order to construct Chase_{ΣSC}(C, pd), it suffices to compute Cl(v_{0}), Cl(v_{1}), ⋯, Cl(v_{n}). The following procedure will compute them in the order of 0, 1, ⋯, n.

Procedure 3: (Computing Cl(v_{0}), Cl(v_{1}), ⋯, Cl(v_{n}).) input: a database schema ⟨S, Σ⟩, a class C ∈ Classes(S), and a path description pd (= P_{1}.P_{2}. · · · .P_{n}).

1. Divide Σ_{SC} into two sets: Σ_{Id} = {C_{a}(pd′ : C_{b}) ∈ Σ_{SC} | pd′ = Id} and Σ_{¬Id} = Σ_{SC} − Σ_{Id}.

2. Let CL_{0} ← {C_{0} ∈ Classes(S) | Σ_{Id} ⊢_{{A1,A2}} C(Id : C_{0})}.

3. for i ← 1 to n

do begin

4. Let CL ← {C_{b} ∈ Classes(S) | there is an SC C_{a}(pd′ : C_{b}) ∈ Σ_{¬Id}

such that pd′ = P_{j+1}.P_{j+2}. · · · .P_{i} and C_{a} ∈ CL_{j} for some j }.

5. Let CL_{i} ← ⋃_{C_{b}∈CL}{C_{i} ∈ Classes(S) | Σ_{Id} ⊢_{{A1,A2}} C_{b}(Id : C_{i})}.

end □

Example 10: Consider the database schema ⟨S, Σ⟩ in Example 5. Let us execute Procedure 3 for class a_{2} and path description B.A.C. In Step 1, Σ_{SC} is divided as follows:

Σ_{Id} = {a_{1}(Id : a_{2}), a_{2}(Id : a_{3}), c_{1}(Id : c_{2})}

Σ_{¬Id} = {a_{1}(C : c_{2}), a_{3}(B : b), b(A : a_{2}), e(C : c_{2})}

In Step 2, CL_{0} = {a_{2}, a_{3}}, since (1) Σ_{Id} ⊢_{A1} a_{2}(Id : a_{2}) and (2) a_{2}(Id : a_{2}) and a_{2}(Id : a_{3}) ∈ Σ_{Id} imply a_{2}(Id : a_{3}) by axiom A2; that is, Σ_{Id} ⊢_{{A1,A2}} a_{2}(Id : a_{3}). No other classes are added to CL_{0}.

Consider the for loop in Step 3. Let i = 1. In Step 4, for each C_{a}(pd′ : C_{b}) ∈ Σ_{¬Id}, it is examined whether or not C_{b} should be added to CL. In this case, only for a_{3}(B:b), class b is added to CL, since a_{3} ∈ CL_{0}. That is, CL = {b}. In Step 5, CL_{1} = {b}, since there is no SC in Σ_{Id} of the form b(Id : C) for any C ∈ Classes(S). Similarly, for i = 2, we have CL = {a_{2}} and CL_{2} = {a_{2}, a_{3}}. For i = 3, we have CL = CL_{3} = ∅.

Consider Chase_{ΣSC}(a_{2}, B.A.C) (= v_{0} ⟶^{B} v_{1} ⟶^{A} v_{2} ⟶^{C} v_{3}), which was constructed in Example 8. Then it holds that Cl(v_{i}) = CL_{i} for all i. □

The correctness of Procedure 3 follows from the following lemma.

Lemma 7: CL_{i} = Cl(v_{i}) for 0 ≤ i ≤ n.

Proof. Induction on i.

Basis. Consider the case that i = 0. Assume that a class C_{b} should be added to Cl(v_{0}) by applying an SC-rule for C_{a}(pd′ : C_{b}) ∈ Σ_{SC} in Step 2 of Procedure 2. Then clearly, pd′ = Id, that is, C_{a}(pd′ : C_{b}) ∈ Σ_{Id}. Thus Σ_{SC} ⊢_{{A1,A2}} C(Id : C_{0}) if and only if Σ_{Id} ⊢_{{A1,A2}} C(Id : C_{0}). Hence it follows from Lemma 5 that CL_{0} = Cl(v_{0}). That is, the basis holds.

Induction. As an induction hypothesis, assume that if j ≤ i − 1, then CL_{j} = Cl(v_{j}), where i ≥ 1. By Lemma 5, it suffices to show that

CL_{i} = {C_{i} ∈ Classes(S) | Σ_{SC} ⊢_{{A1,A2}} C(pd_{i} : C_{i})}. (2.1)

Proof of ‘⊆’: We prove that if C_{i} ∈ CL_{i}, then Σ_{SC} ⊢_{{A1,A2}} C(pd_{i} : C_{i}). Let C_{i} ∈ CL_{i}. There are two cases to be considered: C_{i} ∈ CL and C_{i} ∉ CL.

Case 1. Assume that C_{i} ∈ CL. By definition, there is an SC C_{a}(pd′ : C_{i}) ∈ Σ_{¬Id} such that pd′ = P_{j+1}.P_{j+2}. · · · .P_{i} and C_{a} ∈ CL_{j} for some j. Since pd′ ≠ Id by the definition of Σ_{¬Id}, it holds that j ≤ i − 1. Thus C_{a} ∈ CL_{j} implies C_{a} ∈ Cl(v_{j}) by the induction hypothesis. Hence Σ_{SC} ⊢_{{A1,A2}} C(pd_{j} : C_{a}) by Lemma 5. By axiom A2, C(pd_{j} : C_{a}) and C_{a}(pd′ : C_{i}) imply C(pd_{i} : C_{i}), where pd_{j} ∘ pd′ = pd_{i}. That is, Σ_{SC} ⊢_{{A1,A2}} C(pd_{i} : C_{i}).

Case 2. Assume that C_{i} ∉ CL. By the definition of CL_{i}, the assumption implies that Σ_{Id} ⊢_{{A1,A2}} C_{b}(Id : C_{i}) for some C_{b} ∈ CL. Since C_{b} ∈ CL, it follows from Case 1 above that Σ ⊢_{{A1,A2}} C(pd_{i} : C_{b}). By axiom A2, C(pd_{i} : C_{b}) and C_{b}(Id : C_{i}) imply C(pd_{i} : C_{i}), since pd_{i} ∘ Id = pd_{i}. That is, Σ_{SC} ⊢_{{A1,A2}} C(pd_{i} : C_{i}). This completes the proof of ‘⊆’.

Proof of ‘⊇’: We prove that if Σ_{SC} ⊢_{{A1,A2}} C(pd_{i} : C_{i}), then C_{i} ∈ CL_{i}. Assume that Σ_{SC} ⊢_{{A1,A2}} C(pd_{i} : C_{i}). Then Σ_{SC} ⊧ C(pd_{i} : C_{i}) by Lemma 3. Let u_{0} ⟶^{P_{1}} u_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} u_{i} be a pd_{i}-List such that Cl(u_{j}) = CL_{j} for 0 ≤ j ≤ i. We will prove that the pd_{i}-List satisfies Σ_{SC}. Since C ∈ CL_{0}, this will imply that C_{i} ∈ CL_{i}.

Since CL_{j} = Cl(v_{j}) for 0 ≤ j ≤ i − 1 by the induction hypothesis, it follows from Lemma 4(a) that the pd_{i−1}-List u_{0} ⟶^{P_{1}} u_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} u_{i−1} satisfies Σ_{SC}. By Step 4, for every SC C_{a}(pd′ : C_{b}) ∈ Σ_{¬Id}, if pd′ = P_{j+1}.P_{j+2}. · · · .P_{i} and C_{a} ∈ CL_{j}, then C_{b} ∈ CL_{i}. Thus the pd_{i}-List satisfies Σ_{¬Id}. Similarly, by Step 5, for every SC C_{a}(Id : C_{b}) ∈ Σ_{Id}, if C_{a} ∈ CL_{i}, then C_{b} ∈ CL_{i}. Thus the pd_{i}-List also satisfies Σ_{Id}. Since Σ_{SC} = Σ_{¬Id} ∪ Σ_{Id} by definition, the pd_{i}-List satisfies Σ_{SC}. This completes the induction proof. Consequently, Lemma 7 holds. □

Now consider the time complexity of Procedure 3. Let Classes(S) consist of K classes. (Note that K ≤ D.) We use bit arrays of size K to represent arbitrary subsets of Classes(S), such as those denoted by the variables CL or CL_{i} which are used in the procedure. Testing for class membership or inserting a class into a given subset can then be executed in constant time. Also, each of these variables can then be initialized to the empty set in O(K) time.

Clearly, Step 1 runs in O(∥Σ∥) time, where ∥Σ∥ is the size of Σ, and Step 2 requires O(K) time to initialize CL_{0}. By the definition of Σ_{Id}, each application of axiom A2 must be of the form: ‘if C_{1}(Id : C_{2}) and C_{2}(Id : C_{3}), then C_{1}(Id : C_{3}).’ That is, axiom A2 is considered as a transitivity rule. Clearly, axiom A1 is considered as a reflexivity rule. Thus CL_{0} must coincide with the reflexive transitive closure of C with respect to Σ_{Id}. Hence CL_{0} can be computed by a usual algorithm for computing a reflexive transitive closure. In fact, CL_{0} can be computed in O(∥Σ_{Id}∥) time. Since ∥Σ_{Id}∥ ≤ D, Step 2 can be executed in O(D) time.

In Step 4, it takes O(K) time to initialize CL. In order to compute CL, it suffices to test once for each C_{a}(pd′ : C_{b}) ∈ Σ_{¬Id} whether or not pd′ = P_{j+1}.P_{j+2}. · · · .P_{i} and C_{a} ∈ CL_{j} for some j. Testing pd′ = P_{j+1}.P_{j+2}. · · · .P_{i} can be done in O(len(pd′)) time. Testing C_{a} ∈ CL_{j} can be done in constant time. If both conditions holds, then C_{b} is inserted into CL, which can be done in constant time. That is, for each C_{a}(pd′ : C_{b}), it takes O(len(pd′)) time. Since ∑_{C_{a}(pd′:C_{b})∈Σ_{¬Id}} len(pd′) ≤ ∥Σ_{¬Id}∥, it can be done in O(∥Σ_{¬Id}∥) time as a whole. Since ∥Σ_{¬Id}∥ ≤ D, Step 4 can be executed in O(D) time.

In Step 5, it takes O(K) time to initialize CL_{i}. As in Step 2, CL_{i} coincides with the reflexive transitive closure of CL with respect to Σ_{Id}, and can be computed in O(∥Σ_{Id}∥) time. Thus Step 5 can be executed in O(D) time.

As a result, one execution of Steps 4 and 5 can be done in O(D) time. Since n = len(pd), the for loop in Step 3 can be executed in O(D · len(pd)) time as a whole. Consequently, we have the following lemma.

Lemma 8: Chase_{ΣSC}(C, pd) can be computed in O(D · (len(pd) + 1)) time. □

Since it follows from Lemma 6 that pd ∈ PathDescs(C) if and only if Cl(v_{i−1})∩Dom(P_{i}) ≠ ∅ for 1 ≤ i ≤ n, it can be decided in O(∥Chase_{ΣSC}(C, pd)∥) time whether or not pd ∈ PathDescs(C). Hence Theorem 4(a) follows from Lemma 8.

The following lemma implies that it can be decided in O(∥Chase_{ΣSC}(C, pd)∥+ ∥Σ_{FUNC}∥) time whether or not pd ∈ PathFuncs(C). Note that ∥Σ_{FUNC}∥ ≤ D. Hence Theorem 4(b) follows from Lemma 8.

Lemma 9: pd ∈ PathFuncs(C) if and only if pd ∈ PathDescs(C) and FUNC(P_{i}) ∈ Σ_{FUNC} for 1 ≤ i ≤ n.

Proof. \underline{If part.} Assume that (1) pd ∈ PathDescs(C) and (2) FUNC(P_{i}) ∈ Σ_{FUNC} for 1 ≤ i ≤ n. Let G(V, A) be an interpretation satisfying Σ. Let u be a vertex in V such that C ∈ Cl(u). In order to prove that pd ∈ PathFuncs(C), it suffices to show that there is a unique path in G(V, A) from u described by pd. Since Σ = Σ ∪ {FUNC(P_{i}) | 1 ≤ i ≤ n} by assumption 2, G(V, A) satisfies Σ ∪ {FUNC(P_{i}) | 1 ≤ i ≤ n}. Hence assumption 1 implies that there must be a path in G(V, A) from u described by pd. (Strictly, G(V, A) should satisfy not Σ ∪ {FUNC(P_{i}) | 1 ≤ i ≤ n} but Σ ∪ S_{FUNC} according to the definition of PathDescs(C). Each FUNC constraint not in {FUNC(P_{i}) | 1 ≤ i ≤ n}, however, is independent of the path described by pd.) Furthermore, assumption 2 implies that such a path must be unique.

\underline{Only if part.} Assume that pd ∈ PathFuncs(C). Then it holds that pd ∈ PathDescs(C), since PathFuncs(C) ⊆ PathDescs(C) by definition. We next prove that FUNC(P_{i}) ∈ Σ_{FUNC} for 1 ≤ i ≤ n.

Assume contrary that FUNC(P_{i}) ∉ Σ_{FUNC} for some i. Let G(V, A) be the augmented graph of the pd_{i−1}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i−1}} v_{i−1} with respect to S. It suffices to prove that G(V, A) is an example showing that pd ∉ PathFuncs(C). It suffices to show that (1) G(V, A) is an interpretation satisfying Σ and (2) there is no path in G(V, A) from v_{0} described by pd. Note that C ∈ Cl(v_{0}).

Since pd ∈ PathDescs(C), Chase_{ΣSC}(C, pd) satisfies a property value integrity condition by Lemma 6. Thus so does the pd_{i−1}-List. Furthermore, the pd_{i−1}-List satisfies Σ_{SC} by Lemma 4(a). Hence G(V, A) is an interpretation satisfying Σ (⊆ Σ ∪ S_{FUNC}) by Lemma 2.

By Step 3 of Procedure 1, if there is an arc v_{i−1} ⟶^{P} u ∈ A, then FUNC(P) ∈ Σ_{FUNC}. Since FUNC(P_{i}) ∉ Σ_{FUNC}, there is no arc v_{i−1} ⟶^{P_{i}} u ∈ A. Thus there is no path in G(V, A) from v_{0} described by pd_{i−1} ∘ P_{i}. Since pd_{i−1} ∘ P_{i} is a prefix of pd, there is no path in G(V, A) from v_{0} described by pd, either. This completes the only if part proof. □

Finally, let us consider Theorem 4(c). We must show that it can be decided in O(D · (len(pd) + 1)) time whether or not Σ ⊧ C(pd : C′). By Theorem 2, if pd ∈ PathDescs(C), then Σ ⊧ C(pd : C′) if and only if C′ ∈ Cl(v_{n}). Hence by Lemma 8, it can be decided in O(D · (len(pd) + 1)) time. Theorem 2, however, does not apply to the case that pd ∉ PathDescs(C). In general, by Theorem 3, Σ ⊧ C(pd : C′) if and only if C(pd : C′) satisfies either Condition A or B. In the following, let us consider how to decide whether or not C(pd : C′) satisfies either Condition A or B.

Since C(pd : C′) satisfies Condition A if and only if C′ ∈ Cl(v_{n}) by Lemma 5, Condition A can be tested in O(∥Chase_{ΣSC}(C, pd)∥) time, and hence in O(D · (len(pd) + 1)) time by Lemma 8.

It remains to show that Condition B can be tested in O(D ·(len(pd)+1)) time. A naive method for Condition B is to test whether or not Σ ⊢_{{A1,A2}} C_{i}(P_{i}.P_{i+1}. · · · .P_{n} : C′) for every i and every C_{i} ∈ Dom(P_{i}). It, however, takes exponential time in the worst case. There is a tricky way for testing Condition B.

For 0 ≤ i ≤ n − 1, let us define

CL_{i} = {C_{i} ∈ Classes(S) | Σ ⊢_{{A1,A2}} C_{i}(P_{i+1}.P_{i+2}. · · · .P_{n} : C′)}.

Then C(pd : C′) satisfies Condition B if and only if Dom(P_{i+1}) ⊆ CL_{i} for some i. We consider how to compute CL_{0}, CL_{1}, ⋯, CL_{n−1}. Note the analogy between Cl(v_{i}) and CL_{i}, where

Cl(v_{i}) = {C_{i} ∈ Classes(S) | Σ ⊢_{{A1,A2}} C(P_{1}.P_{2}. · · · .P_{i} : C_{i})}.

Hence CL_{i} can be obtained by executing Procedure 2 in the reverse direction as follows:

Procedure 4: (Computing CL_{0}, CL_{1}, ⋯, CL_{n−1}.) input: a database schema ⟨S, Σ⟩, a class C′ ∈ Classes(S), and a path description pd (= P_{1}.P_{2}. · · · .P_{n}.)

1. Construct a pd-List u_{0} ⟶^{P_{1}} u_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} u_{n} such that Cl(u_{n}) = { C′ } and Cl(u_{i}) = ∅ for 0 ≤ i ≤ n − 1.^{8} 2. Apply the following rule to the pd-List exhaustively:

8Note that Cl(v_{0}) = { C } and Cl(v_{n}) = ∅ in Procedure 2.

Reverse-SC-rule: For an SC C_{a}(pd′ : C_{b}) ∈ Σ_{SC}, if there are two vertices u_{i}, u_{j} such that C_{a} ∉ Cl(u_{i}), C_{b} ∈ Cl(u_{j}), and pd′ =

P_{i+1}.P_{i+2}. · · · .P_{j}, then add C_{a} to Cl(u_{i}).^{9}

3. Let CL_{i} ← Cl(u_{i}) for 0 ≤ i ≤ n − 1. □

Example 11: For the database schema ⟨S, Σ⟩ in Example 5, let us decide whether or not Σ ⊧ a_{2}(B.A.C : c_{2}). Chase_{ΣSC}(a_{2}, B.A.C) is given in Figure 7. Since c_{2} ∉ Cl(v_{3}), Condition A does not hold for a_{2}(B.A.C : c_{2}). By Example 9, B.A.C ∉ PathDescs(a_{2}). Thus it must be decided whether or not Condition B holds for a_{2}(B.A.C : c_{2}). For SC a_{2}(B.A.C : c_{2}), let us compute CL_{0}, CL_{1}, CL_{2} by Procedure 4.

In Step 1, a ‘B.A.C’-List u_{0} ⟶^{B} u_{1} ⟶^{A} u_{2} ⟶^{C} u_{3} is constructed, where Cl(u_{3}) = { c_{2} } and Cl(u_{i}) = ∅ for 0 ≤ i ≤ 2.

For SC e(C:c_{2}) in Σ_{SC}, since c_{2} ∈ Cl(u_{3}) and e ∉ Cl(u_{2}), class e is added to Cl(u_{2}) by applying the Reverse-SC-rule for e(C:c_{2}). By applying the Reverse-SC-rule for c_{1}(Id:c_{2}) in Σ_{SC}, class c_{1} is added to Cl(u_{3}), since c_{2} ∈ Cl(u_{3}) and c_{1} ∉ Cl(u_{3}). By applying the Reverse-SC-rule for a_{1}(C:c_{2}) in Σ_{SC}, class a_{1} is added to Cl(u_{2}), since c_{2} ∈ Cl(u_{3}) and a_{1} ∉ Cl(u_{2}). After that, no Reverse-SC-rule can be applied to the ‘B.A.C’-List any more. Thus we obtain the ‘B.A.C’-List given in Figure 8; that is, CL_{0} = Cl(u_{0}) = ∅, CL_{1} = Cl(u_{1}) = ∅, and CL_{2} = Cl(u_{2}) = {a_{1}, e}.

∅  ∅  {a_{1},e}  {c_{1},c_{2}} B                 A                   C u_{0}  u_{1}  u^{2}  u_{3}

Figure 8: Computing CL_{0}, CL_{1}, CL_{2} by Procedure 4.

Note that Dom(C) = {a_{1}, e} ⊆ CL_{2}; that is, Condition B holds for SC a_{2}(B.A.C : c_{2}). Thus Σ ⊧ a_{2}(B.A.C : c_{2}) by Theorem 3. In fact, it was shown in Example 7 that a_{2}(B.A.C:c_{2}) is derived from Σ by axiom A3. □

The correctness of Procedure 4 can be proved along the same line as proving Lemma 5. Furthermore, it can also be proved along the same line as proving Lemma 8 that Procedure 4 can be executed in O(D · (len(pd) + 1)) time. Thus it can be decided in that time whether or not Dom(P_{i+1}) ⊆ CL_{i} for some i. Hence Condition B can also be tested in that time. Consequently, Theorem 4(c) follows. By the discussions above, we have the following procedure that returns YES if and only if Σ ⊧ C(pd : C′).

9Note that C_{a} ∈ Cl(v_{i}) and C_{b} ∉ Cl(v_{j}) in SC-Rule of Procedure 2.

Procedure 5: (Deciding whether or not Σ ⊧ C(pd : C′).) input: a database schema ⟨S, Σ⟩ and an SC C(pd : C′).

1. Execute Procedure 3 to get Cl(v_{n}).

2. if C′ ∈ Cl(v_{n}) then return YES

else begin

3. Execute Procedure 4 to get CL_{0}, CL_{1}, ⋯, CL_{n−1}.

4. if Dom(P_{i+1}) ⊆ CL_{i} for some i then return YES else return NO.

end. □

By Theorems 2 and 3, if C′ ∈ Cl(v_{n}), then Σ ⊧ C(pd : C′), no matter whether or not pd ∈ PathDescs(C). The test is done in Step 2. If C′ ∉ Cl(v_{n}), that is, C(pd : C′) does not satisfy Condition A, then it is tested in Step 4 whether or not C(pd : C′) satisfies Condition B.

3. The Most Specialized Class Rule (MSC)

Most object-oriented data models and many semantic data models impose an additional condition on a database that requires each object to be created with respect to one particular class. For example, in the case of the UNIVERSITY database schema in Figure 1, this would preclude the possibility of there existing an object in both the student and prof classes. As one might expect, limiting our notion of an interpretation in an analogous fashion will affect the various membership problems. In this section, we begin to explore these problems when imposing such a condition on interpretations. The condition, called the most specialized class rule, is formally defined as follows.

The most specialized class rule: Let G(V, A) be an interpretation for S. For a vertex v ∈ V, if there is a class C_{1} ∈ Cl(v) such that Σ ⊧ C_{1}(Id : C_{2}) for every C_{2} ∈ Cl(v), then the class C_{1} is called the most specialized class (MSC) of v, denoted Msc(v). G(V, A) satisfies the most specialized class rule (MSC) with respect to Σ if and only if for every v ∈ V, whenever Cl(v) ≠ ∅, then there exists Msc(v). □

For example, the interpretation in Figure 3 for the ALGEBRA schema satisfies MSC with respect to the set of constraints in Table 1.

A constraint σ is a logical consequence of Σ satisfying MSC , written Σ ⊧_{MSC} σ, if any interpretation satisfying MSC as well as Σ must satisfy σ. We also write PathDescs_{MSC}(C) and PathFuncs_{MSC}(C) to denote the sets of well-formed path descriptions and path functions for a class C, respectively, in which only interpretations satisfying MSC are considered. Since every interpretation satisfying MSC is also a usual interpretation, it holds that:

Σ ⊧ σ implies Σ ⊧_{MSC} σ (3.1)

PathDescs(C) ⊆ PathDescs_{MSC}(C) (3.2)

PathFuncs(C) ⊆ PathFuncs_{MSC}(C) (3.3)

In the remainder of this section, we make an additional assumption about a database schema ⟨S, Σ⟩, beyond the above requirement that interpretations satisfy MSC; we shall assume S contains a unique bottom class, written ⊥, satisfying

Σ ⊧ ⊥(Id : C) for every C ∈ Classes(S). (3.4)

This implies, for example, that ⊥ qualifies as the most specialized class in Classes(S).

Our assumption concerning ⊥ is really our means of avoiding issues relating to schema evaluation, which are beyond the scope this paper. For example, consider the database schema illustrated in Figure 9. Note that an object u in class a must have an A property value to some object v in class b. A reasonable grounds for schema well-formedness might be to require that v may also be in class c, since c is a subclass of class b. However, this is not possible if classes d and e do not have a common subclass—if there is no bottom class ⊥, for example. Our assumption about the existence of ⊥ is a sufficient (but not necessary) condition for avoiding this sort of problem. In particular, it is relatively straightforward to derive the following version of Theorem 1 with regard to finite implication.

Theorem 5: The following three statements are equivalent.

           a{A}  b c{B}  d        e A               B A.B

Figure 9: The need for ⊥.

1. Σ |̸=_{MSC} C(pd : C′).

2. Σ |̸=_{MSC}^{finite} C(pd : C′).

3. There is a pd-List satisfying MSC as well as PDLs 1 to 3.

Proof. By definition, (2) implies (1). It can be proved along the same line as proving Lemma 1 that (1) implies (3). We prove that (3) implies (2).

Assume that there is a pd-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} satisfying MSC as well as PDLs 1 to 3, where pd = P_{1}.P_{2}. · · · .P_{n}. Let G(V, A) be the augmented graph of the pd-List with respect to S. Note that G(V, A) is constructed from the pd-List by adding one vertex u and a number of arcs. Since ⊥ ∈ Classes(S) = Cl(u) by definition, it follows from 3.4 that Msc(u) = ⊥, and thus G(V, A) satisfies MSC. Furthermore, it can be proved along the same line as proving Lemma 2 that G(V, A) is a finite interpretation satisfying Σ∪S_{FUNC} but violating C(pd : C′). Hence Σ |̸=_{MSC}^{finite} C(pd : C′). That is, (3) implies (2). □

Example 12: Let ⟨S, Σ⟩ be a database schema illustrated in Figure 10, where Dom(A) = { a_{1} }, Dom(B) = { a_{3} }, Dom(C) = { b_{2} }, Dom(D) = { b_{3} }. Assume that Σ_{FUNC} = ∅. Then it holds that Σ |̸=_{MSC} a_{1}(A.B.C:c_{1}). In fact, for the SC a_{1}(A.B.C:c_{1}), there is an ‘A.B.C’-List v_{0} ⟶^{A} v_{1} ⟶^{B} v_{2} ⟶^{C} v_{3} satisfying MSC as well as PDLs 1 to 3, as is given in Figure 11. Here, each vertex v_{i} is labeled Msc(v_{i}) instead of Cl(v_{i}) in order to clarify that the ‘A.B.C’-List satisfies MSC. Since Cl(v_{i}) = {C ∈ Classes(S) | Σ ⊧ Msc(v_{i})(Id : C)} by definition, Cl(v_{i}) can be computed from Msc(v_{i}). It holds that Cl(v_{0}) = {a_{1}}, Cl(v_{1}) = {a_{1}, a_{2}, a_{3}}, Cl(v_{2}) = {b_{1}, b_{2}, b_{4}}, and Cl(v_{3}) = {c_{2}}.

The augmented graph G(V, A) of the ‘A.B.C’-List with respect to S is given in Figure 12. Note that G(V, A) is a finite interpretation satisfying MSC

a_{1}{A}  _{a_{2}} a_{3}{B}  _{b_{1}}  b_{2}{C} b_{3}{D}  _{b_{4}}  _{c_{1}}  _{c_{2}} d  ⊥ D                C        C B       B A A

Figure 10: A database schema ⟨S, Σ⟩.

            a_{1}  A     _{a_{3}}  B     _{b_{4}}  C     _{c_{2}}

Figure 11: An ‘A.B.C’-List satisfying MSC.

as well as PDLs 1 to 3. Thus it holds that Σ |̸=_{MSC}^{finite} a_{1}(A.B.C:c_{1}). □

3.1 NP-completeness results In this section, we will prove the following theorem.

Theorem 6: The following three decision problems are NP-complete.

a. Σ |̸=_{MSC} C(pd : C′) ? (It is still NP-complete, even if C(pd : C′) is well-formed with respect to ⟨S, Σ⟩.)

b. pd ∉ PathDescs_{MSC}(C) ?

c. pd ∉ PathFuncs_{MSC}(C) ? □

Theorem 6(a) implies that axioms A1 to A3 are no longer complete for deciding Σ ⊧_{MSC} C(pd : C′), though the axioms are still sound. Theorem 6(a) follows from the following two lemmas.

            a_{1}  _{a_{3}}  _{b_{4}}  _{c_{2}} A            B            C ⊥ A             A,B,C,D

Figure 12: The augmented graph of the ‘A.B.C’-List in Figure 11.

Lemma 10: It is in NP to decide whether or not Σ |̸=_{MSC} C(pd : C′).

Proof. By Theorem 5, Σ |̸=_{MSC} C(pd : C′) if and only if there is a pd-List satisfying MSC as well as PDLs 1 to 3. Since the size of a pd-List is at most D · len(pd), where D is the size of ⟨S, Σ⟩, such a pd-List can be guessed in NP time. After that, it can be tested in (deterministic) polynomial time whether or not the pd-List satisfies MSC and PDLs 1 to 3. Hence Lemma 10 holds. □

Lemma 11: It is NP-hard to decide whether or not Σ |̸=_{MSC} C(pd : C′), even if C(pd : C′) is well-formed with respect to ⟨S, Σ⟩.

Proof. As an NP-complete problem, which will be transformed to the present problem, we consider the dual problem of 3-Satisfiability problem (3SAT). The problem is defined as follows:

A Boolean expression E is in 3DNF if it is in disjunctive normal form such that each term consists of exactly three literals. The problem is: “Is a 3DNF Boolean expression E not a tautology; that is, is there a truth assignment that makes E false?” Since 3SAT is NP-complete, so is this problem.

Let E = t_{1} ∨ t_{2} ∨ ⋯ ∨ t_{m} be a 3DNF Boolean expression over a set of variables {x_{1}, x_{2}, ⋯, x_{n}}. For 1 ≤ j ≤ m, let us denote the three literals in t_{j} by l_{j_{1}}, l_{j_{2}}, l_{j_{3}}. That is, t_{j} is of the form l_{j_{1}}l_{j_{2}}l_{j_{3}}. We must construct, in polynomial time with respect to E, a database schema ⟨S, Σ⟩ and an SC C(pd : C′), which is well-formed with respect to ⟨S, Σ⟩, such that Σ |̸=_{MSC} C(pd : C′) if and only if E is not a tautology.

1. The definition of S: S contains the following 4n + 8m + 2 class names:

C, Z, \{A_{i}, B_{i}, X_{i}, \overline{X}_{i} | 1 ≤ i ≤ n\}, and

{C_{j}, T_{j}, L_{j_{k}}, M_{j_{k}} | 1 ≤ j ≤ m and 1 ≤ k ≤ 3}

X_{i} and \overline{X}_{i} correspond to x_{i} and \overline{x}_{i}, respectively. L_{j_{k}} corresponds to l_{j_{k}}, where 1 ≤ k ≤ 3. The intention of X_{i} and \overline{X}_{i} is that x_{i} is true and false, respectively. The intention of M_{j_{1}}, M_{j_{2}}, and M_{j_{3}} is that L_{j_{1}}L_{j_{2}}, L_{j_{2}}L_{j_{3}}, and L_{j_{3}}L_{j_{1}} are true, respectively. The intention of T_{j} is that t_{j} is true.

S contains the following n + m + 1 properties:

R, {P_{i} | 1 ≤ i ≤ n} and {Q_{j} | 1 ≤ j ≤ m}

The domain of each property is defined as follows:

Dom(R) = { Z }

Dom(P_{1}) = { C }  and Dom(P_{i}) = { A_{i−1}, B_{i−1} }  for 2 ≤ i ≤ n
Dom(Q_{1}) = { A_{n}, B_{n} } and  Dom(Q_{j}) = { C_{j−1} }  for 2 ≤ j ≤ m

2. The definition of C(pd : C′): Let C′ = T_{m} and assume pd has the form

P_{1}.P_{2}. · · · .P_{n}.Q_{1}.Q_{2}. · · · .Q_{m}.

3. The definition of Σ: Let Σ_{FUNC} = {FUNC(P) | P is a property in S}; that is, Σ contains FUNC(P) for every property P in S. Σ_{SC} consists of 4n + 12m SCs of the form C_{a}(Id : C_{b}) and other 2n + 5m + 1 SCs. Only 3m SCs depend on the content of E. All other SCs are defined independently of the content of E; that is, these depend only on the number of variables and the number of terms in E. The former is a varying part and the latter is a fixed part.

3.1. The fixed part: Intuitively, the fixed part consists of n truth-setting components, and m satisfaction testing components, and additional 2n+2m+1 SCs for communicating between the various components.

(a) Truth-setting components: For each variable x_{i}, 1 ≤ i ≤ n, there is a truth-setting component that consists of the following four SCs:

\{X_{i}(Id : A_{i}), X_{i}(Id : B_{i}), \overline{X}_{i}(Id : A_{i}), \overline{X}_{i}(Id : B_{i})\}

Note that every SC has Id as its path description. A truth-setting component is illustrated in Figure 13.

(b) Satisfaction testing components: For each term t_{j}, 1 ≤ j ≤ m, there is a satisfaction testing component that consists of the following twelve SCs:

{L_{j_{k}}(Id : C_{j}), M_{j_{k}}(Id : L_{j_{k}}), M_{j_{k}}(Id : L_{j_{k+1}}), T_{j}(Id : M_{j_{k}}) | 1 ≤ k ≤ 3}

A_{i}\{P_{i+1}\}  B_{i}\{P_{i+1}\} X_{i}  _{\overline{X}_{i}}

Figure 13: A truth-setting component.

C_{j}{Q_{j+1}} L_{j1}  L_{j2}  L_{j3} M_{j1}  M_{j2}  M_{j3} T_{j}

Figure 14: A satisfaction testing component.

where if k = 3 then let k + 1 = 1 for convenience. Note that every SC has Id as its path description. A satisfaction testing component is illustrated in Figure 14.

(c) The other SCs: The fixed part contains additional 2n + 2m + 1 SCs as follows:

T_{m}(R : Z)
{C(P_{1} : A_{1}), C(P_{1} : B_{1})} and {A_{i−1}(P_{i} : A_{i}), B_{i−1}(P_{i} : B_{i}) | 2 ≤ i ≤ n}
{A_{n}(Q_{1} : C_{1}), B_{n}(Q_{1} : C_{1})} and {C_{j−1}(Q_{j} : C_{j}), T_{j−1}(Q_{j} : T_{j}) | 2 ≤ j ≤ m}

This completes constructing the fixed part. Its whole construction is illustrated in Figure 15. Class Z, property R, and SC T_{m}(R : Z) are not used in this proof, but will be used for proving Theorems 6(b) and (c), later.

3.2. The varying part: This consists of 3m SCs, each of which corresponds to a literal occurring in E. (Hence this part depends on the content of E.) For 1 ≤ j ≤ m and 1 ≤ k ≤ 3, if l_{j_{k}} is a positive (or negative) literal of a variable x_{i}, then the varying part contains an SC X_{i}(pd_{ij} : L_{j_{k}}) (or an SC \overline{X}_{i}(pd_{ij} : L_{j_{k}})), where

C\{P_{1}\}  A_{1}\{P_{2}\} B_{1}\{P_{2}\} X_{1}  _{\overline{X}_{1}}  A_{2}\{P_{3}\} B_{2}\{P_{3}\} X_{2}  _{\overline{X}_{2}}  A_{n}\{Q_{1}\} B_{n}\{Q_{1}\} X_{n}  _{\overline{X}_{n}} P_{1} P_{1}  P_{2}  P_{2}  P_{3}  P_{3}  P_{n}  P_{n}  C_{1}\{Q_{2}\} T_{1} C_{2}\{Q_{3}\} T_{2} C_{m} T_{m}\{R\} Z  Q_{1} Q_{1} Q_{2} Q_{2} Q_{3} Q_{3} Q_{m} Q_{m} R  · · · · · ·

Figure 15: The fixed part of Σ_{SC}.

pd_{ij} = P_{i+1}.P_{i+2}. · · · .P_{n}.Q_{1}.Q_{2}. · · · .Q_{j}.^{10}

An example of the varying part will be illustrated in Figure 16 of Example 13, later.

This completes constructing ⟨S, Σ⟩ and C(pd : C′) from E. It is not hard to see that ⟨S, Σ⟩ and C(pd : C′) can be constructed from E in polynomial time. Strictly, ⟨S, Σ⟩ should contain the bottom class ⊥ and its related SCs. The bottom class, however, is unimportant for this proof, and is not described explicitly. It remains to prove that (1) C(pd : C′) is well-formed with respect to ⟨S, Σ⟩ and (2) Σ |̸=_{MSC} C(pd : C′) if and only if E is not a tautology.

Let us first prove that C(pd : C′) is well formed with respect to ⟨S, Σ⟩; that is, pd ∈ PathDescs_{MSC}(C). By 3.2, it suffices to show that pd ∈ PathDescs(C). Let Chase_{ΣSC}(C, pd) be

w_{0} ⟶^{P_{1}} w_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} w_{n} ⟶^{Q_{1}} w_{n+1} ⟶^{Q_{2}} ⋯ ⟶^{Q_{m}} w_{n+m}.

10If i = n, then let pd_{ij} = Q_{1}.Q_{2}. · · · .Q_{j}.

Since Σ_{SC} contains C(P_{1} : A_{1}), A_{i−1}(P_{i} : A_{i}) for 2 ≤ i ≤ n, A_{n}(Q_{1} : C_{1}), and C_{j−1}(Q_{j} : C_{j}) for 2 ≤ j ≤ m, it holds that:

Σ_{SC} ⊢_{A2} C(P_{1}.P_{2}. · · · .P_{i} : A_{i}) for 1 ≤ i ≤ n  (3.5)
Σ_{SC} ⊢_{A2} C(P_{1}.P_{2}. · · · .P_{n}.Q_{1}.Q_{2}. · · · .Q_{j} : C_{j}) for 1 ≤ j ≤ m (3.6)

Thus it follows from Lemma 5 that A_{i} ∈ Cl(w_{i}) and C_{j} ∈ Cl(w_{n+j}). Since (1) C ∈ Dom(P_{1}), (2) A_{i−1} ∈ Dom(P_{i}) for 2 ≤ i ≤ n, (3) A_{n} ∈ Dom(Q_{1}), and (4) C_{j−1} ∈ Dom(Q_{j}) for 2 ≤ j ≤ m, it holds that Cl(w_{i−1})∩Dom(P_{i}) ≠ ∅ for 1 ≤ i ≤ n and Cl(w_{n+j−1})∩Dom(Q_{j}) ≠ ∅ for 1 ≤ j ≤ m. That is, Chase_{ΣSC}(C, pd) satisfies a property value integrity condition. Hence pd ∈ PathDescs(C) by Lemma 6. This completes proving that C(pd : C′) is well-formed with respect to ⟨S, Σ⟩. In the following we will prove that Σ |̸=_{MSC} C(pd : C′) if and only if E is not a tautology.

\underline{Only if part.} Assume that Σ |̸=_{MSC} C(pd : C′). By Theorem 5, there is a pd-List

v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} ⟶^{Q_{1}} u_{1} ⟶^{Q_{2}} ⋯ ⟶^{Q_{m}} u_{m}

satisfying MSC and PDLs 1 to 3. We first prove the following three claims.

Claim 1: Cl(v_{i}) contains either X_{i} or \overline{X}_{i} for 1 ≤ i ≤ n.

Claim 2: {L_{j_{1}}, L_{j_{2}}, L_{j_{3}}} ⊈ Cl(u_{j}) for 1 ≤ j ≤ m.

Claim 3: If either (1) X_{i} ∈ Cl(v_{i}) and l_{j_{k}} is a positive literal of x_{i} or (2) \overline{X}_{i} ∈ Cl(v_{i}) and l_{j_{k}} is a negative literal of x_{i}, then L_{j_{k}} ∈ Cl(u_{j}), where

1 ≤ i ≤ n, 1 ≤ j ≤ m, and 1 ≤ k ≤ 3.

Proof of Claim 1 : Since Σ_{SC} ⊧ C(P_{1}.P_{2}. · · · .P_{i} : A_{i}) by 3.5 and Lemma 3, it follows from 3.1 that Σ_{SC} ⊧_{MSC} C(P_{1}.P_{2}. · · · .P_{i} : A_{i}), where 1 ≤ i ≤ n. Furthermore, since (1) C ∈ Cl(v_{0}) by PDL 3 and (2) the pd-List satisfies Σ_{SC} by PDL 2, Cl(v_{i}) should contain A_{i}. Similarly, Cl(v_{i}) should also contain B_{i} by the symmetry between A_{i} and B_{i}. That is, {A_{i}, B_{i}} ⊆ Cl(v_{i}) for 1 ≤ i ≤ n. Since the pd-List satisfies MSC, Msc(v_{i}) exists for v_{i}. From Figure 13, we can see that Cl(v_{i}) should contain either X_{i} or \overline{X}_{i}.^{11} Hence Claim 1 follows.

Proof of Claim 2 : Assume that {L_{j_{1}}, L_{j_{2}}, L_{j_{3}}} ⊆ Cl(u_{j}) for some j. From Figure 14, we can see that Cl(u_{j}) should contain T_{j} in order that Msc(u_{j}) exists for u_{j}. Since Σ_{SC} contains T_{l−1}(Q_{l} : T_{l}) for 2 ≤ l ≤ m, it holds that Σ_{SC} ⊧_{MSC} T_{j}(Q_{j+1}.Q_{j+2}. · · · .Q_{m} : T_{m}). Furthermore, since the pd-List satisfies Σ_{SC} by PDL 2, T_{j} ∈ Cl(u_{j}) implies T_{m} ∈ Cl(u_{m}). On the other hand, since the pd-List satisfies PDL 3, it holds that T_{m} = C′ ∉ Cl(u_{m}). Contradiction. Hence {L_{j_{1}}, L_{j_{2}}, L_{j_{3}}} ⊈ Cl(u_{j}) for any j. That is, Claim 2 follows.

11Cl(v_{i}) may contain both of them. Then Msc(v_{i}) is the bottom class ⊥.

Proof of Claim 3 : Assume that l_{j_{k}} is a positive literal of x_{i}. Since (1) Σ_{SC} contains X_{i}(pd_{ij} : L_{j_{k}}) by definition and (2) the pd-List satisfies Σ_{SC} by PDL 2, X_{i} ∈ Cl(v_{i}) implies L_{j_{k}} ∈ Cl(u_{j}). Similarly, if l_{j_{k}} is a negative literal of x_{i}, then \overline{X}_{i} ∈ Cl(v_{i}) implies L_{j_{k}} ∈ Cl(u_{j}). Hence Claim 3 follows.

Let us define a truth assignment τ : {x_{1}, x_{2}, ⋯, x_{n}} → {T (rue), F (alse)} such that if X_{i} ∈ Cl(v_{i}), then τ(x_{i}) = T; otherwise τ(x_{i}) = F. We prove that τ makes E false; that is, E is not a tautology. It suffices to prove that τ makes t_{j} false for 1 ≤ j ≤ m.

By Claim 2, there is a class L_{j_{k}} that is not in Cl(w_{j}), where 1 ≤ k ≤ 3. There are two cases to be considered.

Assume that l_{j_{k}} is a positive literal of a variable x_{i}. Then L_{j_{k}} ∉ Cl(w_{j}) implies X_{i} ∉ Cl(v_{i}) by Claim 3. Thus τ(x_{i}) = F by definition. Hence τ makes t_{j} false.

Assume that l_{j_{k}} is a negative literal of x_{i}. Then L_{j_{k}} ∉ Cl(w_{j}) implies \overline{X}_{i} ∉ Cl(v_{i}) by Claim 3. Furthermore, \overline{X}_{i} ∉ Cl(v_{i}) implies X_{i} ∈ Cl(v_{i}) by Claim 1. Thus τ(x_{i}) = T by definition. Hence τ also makes t_{j} false in this case. Consequently, if Σ |̸=_{MSC} C(pd : C′), then E is not a tautology.

\underline{If part.} Assume that E is not a tautology. There is a truth assignment τ : {x_{1}, x_{2}, ⋯, x_{n}} → {T, F } that makes E false. Let us define a pd-List

v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} ⟶^{Q_{1}} u_{1} ⟶^{Q_{2}} ⋯ ⟶^{Q_{m}} u_{m},

which satisfies MSC (by showing Msc(v_{i}) and Msc(u_{j}) for all i and j), as follows:

1. Cl(v_{0}) = { C } and Msc(v_{0}) = C.

2.1. If τ(x_{i}) = T, then Cl(v_{i}) = {A_{i}, B_{i}, X_{i}} and Msc(v_{i}) = X_{i}, where 1 ≤ i ≤ n.

2.2. If τ(x_{i}) = F, then Cl(v_{i}) = \{A_{i}, B_{i}, \overline{X}_{i}\} and Msc(v_{i}) = \overline{X}_{i}.

3.1. If τ makes all the three literals in t_{j} false, then Cl(u_{j}) = {C_{j}} and Msc(u_{j}) = C_{j}, where 1 ≤ j ≤ m.

3.2. If τ makes just one literal l_{j_{k}} true, then Cl(u_{j}) = {C_{j}, L_{j_{k}}} and Msc(u_{j}) = L_{j_{k}}, where 1 ≤ k ≤ 3.

3.3. If τ makes two literals l_{j_{k}} and l_{j_{k+1}} true, then Cl(u_{j}) must be {C_{j}, L_{j_{k}}, L_{j_{k+1}}, M_{j_{k}}} and Msc(u_{j}) = M_{j_{k}}.^{12}

12Since τ makes E false, τ does not make all the three literals true.

By Theorem 5, in order to prove that Σ |̸=_{MSC} C(pd : C′), it suffices to show that the pd-List satisfies PDLs 1 to 3 (as well as MSC).

By considering the domain of each property, we can see that C ∈ Cl(v_{0})∩ Dom(P_{1}), A_{i−1} ∈ Cl(v_{i−1}) ∩ Dom(P_{i}) for 2 ≤ i ≤ n, A_{n} ∈ Cl(v_{n}) ∩ Dom(Q_{1}), and C_{j−1} ∈ Cl(u_{j−1}) ∩ Dom(Q_{j}) for 2 ≤ j ≤ m. Hence the pd-List satisfies PDL 1.

It is easy to see that the pd-List satisfies all the SCs in the fixed part. By 2.1 and 2.2 above, X_{i} ∈ Cl(v_{i}) if and only if τ(x_{i}) = T, and \overline{X}_{i} ∈ Cl(v_{i}) if and only if τ(x_{i}) = F. Furthermore, by 3.1 to 3.3, L_{j_{k}} ∈ Cl(u_{j}) if and only if τ makes l_{j_{k}} true. Thus the pd-List also satisfies all the SCs in the varying part. That is, the pd-List satisfies PDL 2.

Since C ∈ Cl(v_{0}) and C′ = T_{m} ∉ Cl(u_{m}), the pd-List satisfies PDL 3. This completes proving that Σ |̸=_{MSC} C(pd : C′) if and only if E is not a

tautology. As a result, Lemma 11 holds. □

Example 13: Let E = x_{1} \overline{x}_{2} x_{3} ∨ \overline{x}_{1} \overline{x}_{2} x_{3} be a 3DNF Boolean expression. Then the SC C(pd : C′) has the form C(P_{1}.P_{2}.P_{3}.Q_{1}.Q_{2} : T_{2}). Furthermore, the varying part of Σ_{SC} consists of the following six SCs, as illustrated in Figure 16:

X_{1}(P_{2}.P_{3}.Q_{1} : L_{11}), \overline{X}_{2}(P_{3}.Q_{1} : L_{12}), X_{3}(Q_{1} : L_{13}),

\overline{X}_{1}(P_{2}.P_{3}.Q_{1}.Q_{2} : L_{21}), \overline{X}_{2}(P_{3}.Q_{1}.Q_{2} : L_{22}), X_{3}(Q_{1}.Q_{2} : L_{23})

It is easy to construct the whole database schema ⟨S, Σ⟩ from E. □

X_{1}  _{\overline{X}_{1}}  X_{2}  _{\overline{X}_{2}}  X_{3}  _{\overline{X}_{3}}  L_{11} L_{12} L_{13}  L_{21} L_{22} L_{23} P_{2}.P_{3}.Q_{1} P_{3}.Q_{1} Q^{1} P_{2}.P_{3}.Q_{1}.Q_{2} P_{3}.Q_{1}.Q_{2} Q_{1}.Q_{2}

Figure 16: The varying part of Σ_{SC}.

This completes proving Theorem 6(a). Let us next prove Theorem 6(b); that is, it is NP-complete to decide whether or not pd ∉ PathDescs_{MSC}(C). The following lemma will be used for proving that the problem is in NP.

Lemma 12: Let pd = P_{1}.P_{2}. · · · .P_{n}. Then pd ∉ PathDescs_{MSC}(C) if and only if there is a pd_{i}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} v_{i} satisfying the following six conditions: (1) i < n, (2) C ∈ Cl(v_{0}), (3) Cl(v_{i}) ∩ Dom(P_{i+1}) = ∅, (4) MSC,

(5) PDL 1, and (6) PDL 2.

Proof. \underline{If part.} Assume that there is a pd_{i}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} v_{i} satisfying the six conditions above. Let G(V, A) be the augmented graph of the pd_{i}-List with respect to S. As is proving Theorem 5, G(V, A) is an interpretation satisfying MSC as well as Σ∪S_{FUNC}. By Step 3 of Procedure 1, if there is an arc v_{i} ⟶^{P} u ∈ A, then Cl(v_{i})∩Dom(P) ≠ ∅. Thus by condition (3), there is no arc v_{i} ⟶^{P_{i+1}} u ∈ A. Hence there is no path in G(V, A) from v_{0} described by pd_{i} ∘ P_{i+1}. Since pd_{i} ∘ P_{i+1} is a prefix of pd, there is no path in G(V, A) from v_{0} described by pd, either. As a result, pd ∉ PathDescs_{MSC}(C).

\underline{Only if part.} Assume that pd ∉ PathDescs_{MSC}(C). Let i be the largest index such that pd_{i} ∈ PathDescs_{MSC}(C). Then pd_{i+1} ∉ PathDescs_{MSC}(C). By definition, there is an interpretation G(V, A) satisfying MSC and Σ ∪ S_{FUNC} such that for a vertex u_{0} ∈ V with C ∈ Cl(u_{0}), there is no path in G(V, A) from u_{0} described by pd_{i+1}. Since pd_{i} ∈ PathDescs_{MSC}(C), however, there must be a path in G(V, A) from u_{0} described by pd_{i}. Let us denote the path

by u_{0} ⟶^{P_{1}} u_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} u_{i}. Let v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} v_{i} be a pd_{i}-List such

that Cl(v_{j}) = Cl(u_{j}) for 0 ≤ j ≤ n. We will prove that the pd_{i}-List satisfies all the six conditions.

Clearly, the pd_{i}-List satisfies conditions (1), (2), and (4). As is proving Lemma 1, the pd_{i}-List satisfies PDLs 1 and 2, that is, conditions (5) and (6). If the pd_{i}-List does not satisfy condition (3), then it holds that Cl(u_{i}) ∩ Dom(P_{i+1}) ≠ ∅, since Cl(v_{i}) = Cl(u_{i}). Since FUNC(P_{i+1}) ∈ S_{FUNC}, this implies that there must be an arc u_{i} ⟶^{P_{i+1}} w ∈ A. Hence G(V, A) contains a path from u_{0} to w described by pd_{i+1}, since G(V, A) contains a path from u_{0} to u_{i} described by pd_{i} and pd_{i+1} = pd_{i} ∘ P_{i+1}. Contradiction. Thus the pd_{i}-List must satisfy condition (3). This completes proving the only if part. □ Example 14: For the database schema ⟨S, Σ⟩ in Example 12, let us show that A.B.D ∉ PathDescs_{MSC}(a_{1}) by Lemma 12. Consider the ‘A.B’-List in Figure 17, where each vertex is labeled its MSC. It is easy to verify that the ‘A.B’-List satisfies all the conditions of Lemma 12. For example, it satisfies condition (3), since Cl(v_{2}) ∩ Dom(D) = {c_{1}, c_{2}, c_{4}} ∩ {c_{3}} = ∅. On the other hand, it holds that A.B.C ∈ PathDescs_{MSC}(a_{1}), since there is no list satisfying the conditions of Lemma 12. □

[figure: a_{1}; a_{3}; b_{4}; v_{0}; v_{1}; v_{2}; A; B]

Figure 17: An ‘A.B’-List showing A.B.D ∉ PathDescs_{MSC}(a_{1}).

\underline{Proof of Theorem 6(b)}: We first prove that it is in NP to decide whether or not pd ∉ PathDescs_{MSC}(C). By Lemma 12, pd ∉ PathDescs_{MSC}(C) if and only if there is a pd_{i}-List satisfying the six conditions of Lemma 12. Since the size of the pd_{i}-List is at most D · len(pd), where D is the size of ⟨S, Σ⟩, the pd_{i}-List can be guessed in NP time. After that, it can be tested in polynomial time whether or not the pd_{i}-List satisfies all the six conditions. Hence the problem is in NP.

We now prove that it is NP-hard to decide if pd ∉ PathDescs_{MSC}(C). Consider the database schema ⟨S, Σ⟩ in Lemma 11. We will prove that

Σ ⊧_{MSC} C(pd : C′) if and only if pd ∘ R ∈ PathDescs_{MSC}(C).

Since Σ |̸=_{MSC} C(pd : C′) if and only if E is not a tautology, this implies that pd ∘ R ∉ PathDescs_{MSC}(C) if and only if E is not a tautology. Hence it is NP-hard to decide whether or not pd ∘ R ∉ PathDescs_{MSC}(C).

\underline{If part.} Assume that pd ∘ R ∈ PathDescs_{MSC}(C). Let G(V, A) be an interpretation satisfying MSC and Σ. Assume that there is a path in G(V, A) from a vertex u to a vertex v described by pd, where C ∈ Cl(u). In order to prove that Σ ⊧_{MSC} C(pd : C′), it suffices to show that C′ = T_{m} ∈ Cl(v).

Since FUNC(P) ∈ Σ for every property P in S by definition, it holds that Σ = Σ ∪ S_{FUNC}. Thus G(V, A) satisfies Σ ∪ S_{FUNC} as well as MSC. Furthermore, since pd ∘ R ∈ PathDescs_{MSC}(C), there must be a path from u to a vertex w described by pd ∘ R. Because of property functionality, the path from u to w is unique. Hence the path from u to v should be on the path from u to w; that is, there is an arc v ⟶^{R} w ∈ A. Since G(V, A) is an interpretation, it satisfies a property value integrity condition. Thus it holds that Cl(v) ∩ Dom(R) ≠ ∅. Since Dom(R) = { T_{m} } by definition, it holds that T_{m} ∈ Cl(v). Hence Σ ⊧_{MSC} C(pd : C′).

\underline{Only if part.} Assume that Σ ⊧_{MSC} C(pd : C′). Let G(V, A) be an interpretation satisfying MSC and Σ∪S_{FUNC}. Let u ∈ V, where C ∈ Cl(u). In order to prove that pd ∘R ∈ PathDescs_{MSC}(C), it suffices to show that there is a path in G(V, A) from u described by pd ∘ R. Since C(pd : C′) is well-formed with respect to ⟨S, Σ⟩, that is, pd ∈ PathDescs_{MSC}(C), there is a path in G(V, A) from u to a vertex v described by pd. Since Σ ⊧_{MSC} C(pd : C′), C ∈ Cl(u) implies C′ = T_{m} ∈ Cl(v). Since T_{m} ∈ Dom(R) by definition, it holds that Cl(v) ∩ Dom(R) ≠ ∅. Furthermore, since G(V, A) satisfies FUNC(R) ∈ S_{FUNC}, there must be an arc v ⟶^{R} w ∈ A. Thus G(V, A) contains a path from u to w described by pd ∘ R. Hence pd ∘ R ∈ PathDescs_{MSC}(C). This completes proving Theorem 6(b). □

We finally prove Theorem 6(c); that is, it is NP-complete to decide whether or not pd ∉ PathFuncs_{MSC}(C). It is easy to see that the proof of Lemma 9 applies also to the case of MSC, and thus we have the following corollary of Lemma 9.

Corollary 1: pd ∈ PathFuncs_{MSC}(C) if and only if pd ∈ PathDescs_{MSC}(C) and FUNC(P_{i}) ∈ Σ_{FUNC} for 1 ≤ i ≤ n, where pd = P_{1}.P_{2}. · · · .P_{n}. □

\underline{Proof of Theorem 6(c)}: Since (1) it is in NP to decide whether or not pd ∉ PathDescs_{MSC}(C) by Theorem 6(b) and (2) it can be decided in polynomial time whether or not FUNC(P_{i}) ∈ Σ_{FUNC} for 1 ≤ i ≤ n, it follows from Corollary 1 that it is in NP to decide whether or not pd ∉ PathFuncs_{MSC}(C).

Finally, we prove that it is NP-hard to decide if pd ∉ PathFuncs_{MSC}(C). Consider the database schema ⟨S, Σ⟩ in Lemma 11. Since FUNC(P) ∈ Σ for every property P in S by definition, it follows from Corollary 1 that pd ∘ R ∈ PathFuncs_{MSC}(C) if and only if pd ∘ R ∈ PathDescs_{MSC}(C). Since it is NPhard to decide whether or not pd ∘ R ∉ PathDescs_{MSC}(C), it is also NP-hard to decide whether or not pd ∘ R ∉ PathFuncs_{MSC}(C). Hence Theorem 6(c) holds. □

3.2 The case of bounded path lengths Let l = max {len(pd′) | C_{a}(pd′ : C_{b}) ∈ Σ}. If l = 0, that is, if every SC in Σ_{SC} has the form C_{a}(Id : C_{b}), then the problems in this section will be trivial. Thus consider the case that l ≥ 1. Let Classes(S) = {C_{1}, C_{2}, ⋯, C_{K}}.

In the following we will prove the following theorem. By the theorem, if l is bounded, then the three decision problems of Theorem 6 can be solved in polynomial time.

Theorem 7: The following decision problems are solved in O(K^{l+1} · D · l · (len(pd) + 1)) time, where D is the size of ⟨S, Σ⟩.

a. Σ ⊧_{MSC} C(pd : C′) ?

b. pd ∈ PathDescs_{MSC}(C) ?

c. pd ∈ PathFuncs_{MSC}(C) ? □

Proof of Theorem 7(a): As before, let us denote pd by P_{1}.P_{2}. · · · .P_{n}. For 0 ≤ i ≤ n, let PDL_{i} denote the set of pd_{i}-Lists v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} v_{i} satisfying the four conditions:

(1) MSC, (2) PDL 1, (3) PDL 2, and (4) C ∈ Cl(v_{0}). Then by Theorem 5, Σ |̸=_{MSC} C(pd : C′) if and only if there is a pd-Lists v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} in PDL_{n} such that C′ ∉ Cl(v_{n}).^{13} Thus by computing PDL_{n}, we can decide whether or not Σ ⊧_{MSC} C(pd : C′). It is important to note that a pd_{i}-List satisfying MSC can be represented by specifying Msc(v_{j}) (instead of Cl(v_{j})) for each vertex v_{j}, where 0 ≤ j ≤ i, since

Cl(v_{j}) = {C′′ ∈ Classes(S) | Σ ⊧ Msc(v_{j})(Id : C′′)}.^{14}

Strictly, there may be a vertex v_{j} such that Cl(v_{j}) = ∅. (Then Msc(v_{j}) is undefined.) In order to treat such a case uniformly, it is convenient to introduce a special class C_{0}, and to consider Cl(v_{j}) = ∅ if Msc(v_{j}) = C_{0}. By the observations above, the number of pd_{i}-Lists in PDL_{i} is at most (K +1)^{i+1}, since a pd_{i}-List consists of i + 1 vertices.

The following procedure computes PDL_{i} by (1) generating all pd_{i}-Lists satisfying MSC and (2) checking PDL 1, PDL 2, and C ∈ Cl(v_{0}) for each generated pd_{i}-List.

13Note that pd_{n} = pd by definition.

14If the pd_{i}-List does not satisfy MSC, then Cl(v_{j}) may be an arbitrary subset of Classes(S), so that the number of possible Cl(v_{j}) becomes 2^{K}.

Procedure 6: (Computing PDL_{i}.) input: a database schema ⟨S, Σ⟩, a class C ∈ Classes(S), and a path description pd_{i} (= P_{1}.P_{2}. · · · .P_{i}).

1. Let PDL_{i} ← ∅.

2. for k_{0} ← 0 to K; for k_{1} ← 0 to K; ⋯; for k_{i} ← 0 to K

do begin

3. Construct a pd_{i}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} v_{i} such that Msc(v_{j}) = C_{k_{j}}, that is, Cl(v_{j}) = {C_{j} ∈ Classes(S) | Σ ⊧ C_{k_{j}}(Id : C_{j})} for 0 ≤ j ≤ i.

4. if the pd_{i}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} v_{i} satisfies PDL 1, PDL 2, and C ∈ Cl(v_{0}) then add the pd_{i}-List to PDL_{i}.

end □

Example 15: Consider the database schema ⟨S, Σ⟩ in Example 12. For a class a_{3} and a path description A.B, let us execute Procedure 6. Then PDL_{2} consists of the following twelve ‘A.B’-Lists, where each ‘A.B’-List v_{0} ⟶^{A} v_{1} ⟶^{B} v_{2} is denoted by (Msc(v_{0}), Msc(v_{1}), Msc(v_{2})) for simplicity:

(a_{3}, a_{3}, b_{3}), (a_{3}, a_{3}, b_{4}), (a_{3}, a_{3}, ⊥), (a_{3}, ⊥, b_{3}), (a_{3}, ⊥, b_{4}), (a_{3}, ⊥, ⊥),

(⊥, a_{3}, b_{3}), (⊥, a_{3}, b_{4}), (⊥, a_{3}, ⊥), (⊥, ⊥, b_{3}), (⊥, ⊥, b_{4}), (⊥, ⊥, ⊥)

Since b_{2} ∈ Cl(v_{2}) for every ‘A.B’-List in PDL_{2}, it holds that Σ ⊧_{MSC} a_{3}(A.B : b_{2}). On the other hand, since b_{4} ∉ Cl(v_{2}) for (a_{3}, a_{3}, b_{3}) ∈ PDL_{2}, it holds that Σ |̸=_{MSC} a_{3}(A.B : b_{4}). □

Let us estimate the time complexity of Procedure 6. By the for loop of Step 2, Steps 3 and 4 are executed exactly (K + 1)^{i+1} times, that is, O(K^{i+1}) times. Step 3 can be executed in O(D · (i + 1)) time, since each Cl(v_{j}) can be computed in O(D) time as in estimating Step 2 of Procedure 3. Step 4 can be executed in O(D · (i + 1)) time, since the size of the pd_{i}-List is at most D · (i + 1). Hence Procedure 6 can be executed in O(K^{i+1} · D · (i + 1)) time.

We now consider how to decide whether or not Σ ⊧_{MSC} C(pd : C′). There are two cases to be considered: len(pd) ≤ l and len(pd) > l.

Case 1. Assume that len(pd) ≤ l. PDL_{n} can be computed in O(K^{len(pd)+1}· D · (len(pd) + 1)) time by Procedure 6. After that, it can be decided in O(K^{len(pd)+1} · D · (len(pd) + 1)) time whether or not there is a pd-Lists v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} in PDL_{n} such that C′ ∉ Cl(v_{n}), since the size of PDL_{n} is O(K^{len(pd)+1} · D · (len(pd) + 1)). Thus it can be decided in O(K^{len(pd)+1} · D · (len(pd) + 1)) time whether or not Σ ⊧_{MSC} C(pd : C′). Hence Theorem 7(a) holds in this case.

Case 2. Assume that len(pd) > l. PDL_{n} cannot be used, since its size may exceed O(K^{l+1} · D · l · (len(pd) + 1)). Note that in order to decide whether or not Σ ⊧_{MSC} C(pd : C′), we do not need PDL_{n} but only the set {v_{n} | v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} ∈ PDL_{n}}. The following lemma will be useful for computing the set.

Lemma 13: A pd_{i+l}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i+l}} v_{i+l} is in PDL_{i+l} if and only if

(1) the pd_{i+l−1}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i+l−1}} v_{i+l−1} is in PDL_{i+l−1} and (2) the

P_{i+1}.P_{i+2}. · · · .P_{i+l}-List v_{i} ⟶^{P_{i+1}} v_{i+1} ⟶^{P_{i+2}} ⋯ ⟶^{P_{i+l}} v_{i+l} satisfies MSC, PDL 1,

and PDL 2, where 1 ≤ i ≤ n − l.

Proof. The only if part is clear. Assume that (1) the pd_{i+l−1}-List v_{0} ⟶^{P_{1}}

v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i+l−1}} v_{i+l−1} is in PDL_{i+l−1} and (2) the P_{i+1}.P_{i+2}. · · · .P_{i+l}-List

v_{i} ⟶^{P_{i+1}} v_{i+1} ⟶^{P_{i+2}} ⋯ ⟶^{P_{i+l}} v_{i+l} satisfies MSC, PDL 1, and PDL 2. By the definition of PDL_{i+l}, it suffices to show that the pd_{i+l}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i+l}} v_{i+l} satisfies MSC, PDL 1, PDL 2, and C ∈ Cl(v_{0}).

Clearly, the pd_{i+l}-List satisfies MSC, PDL 1, and C ∈ Cl(v_{0}). As for PDL 2, assume that there is an SC C_{a}(pd′ : C_{b}) ∈ Σ_{SC} such that C_{a} ∈ Cl(v_{j}) and pd′ = P_{j+1}.P_{j+2}. · · · .P_{j+m} for some j and m. It suffices to show that C_{b} ∈ Cl(v_{j+m}). Note that m ≤ l by the definition of l. Hence the

P_{j+1}.P_{j+2}. · · · .P_{j+m}-List v_{j} ⟶^{P_{j+1}} v_{j+1} ⟶^{P_{j+2}} ⋯ ⟶^{P_{j+m}} v_{j+m} must be included in

either the pd_{i+l−1}-List or the P_{i+1}.P_{i+2}. · · · .P_{i+l}-List. Since both the pd_{i+l−1}- List and the P_{i+1}.P_{i+2}. · · · .P_{i+l}-List satisfy C_{a}(pd′ : C_{b}) by PDL 2, C_{a} ∈ Cl(v_{j}) implies C_{b} ∈ Cl(v_{j+l}). This completes proving Lemma 13. □

For 1 ≤ i ≤ n−l+1, let PDL_{i+l−1}^{i} denote the set of P_{i+1}.P_{i+2}. · · · .P_{i+l−1}-

Lists such that v_{i} ⟶^{P_{i+1}} v_{i+1} ⟶^{P_{i+2}} ⋯ ⟶^{P_{i+l−1}} v_{i+l−1} is in PDL_{i+l−1}^{i} if and only if

there is a pd_{i+l−1}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i+l−1}} v_{i+l−1} in PDL_{i+l−1} satisfying

the four conditions: MSC, PDL 1, PDL 2, and C ∈ Cl(v_{0}). Note that if l = 1, then PDL_{i+l−1}^{i} is the set of vertices v_{i} such that v_{i} is in PDL_{i+l−1}^{i} if and only

if there is a pd_{i+l−1}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i+l−1}} v_{i+l−1} in PDL_{i+l−1} satisfying

those four conditions. In order to decide whether or not Σ ⊧_{MSC} C(pd : C′), it suffices to compute PDL_{n}^{n−l+1}. Lemma 13 suggests that PDL_{i+l}^{i+1} is computed from PDL_{i+l−1}^{i}, as follows:

Procedure 7: (Computing PDL_{i+l}^{i+1} from PDL_{i+l−1}^{i}.) input: a database schema ⟨S, Σ⟩, a path description pd (= P_{1}.P_{2}. · · · .P_{n}), and PDL_{i+l−1}^{i}.

1. Let PDL_{i+l}^{i+1} ← ∅.

2. for each v_{i} ⟶^{P_{i+1}} v_{i+1} ⟶^{P_{i+2}} ⋯ ⟶^{P_{i+l−1}} v_{i+l−1} in PDL_{i+l−1}^{i}; for k ← 0 to K

do begin

3. Construct a P_{i+1}.P_{i+2}. · · · .P_{i+l}-List

v_{i} ⟶^{P_{i+1}} v_{i+1} ⟶^{P_{i+2}} ⋯ ⟶^{P_{i+l−1}} v_{i+l−1} ⟶^{P_{i+l}} v_{i+l}

by adding a vertex v_{i+l} such that Msc(v_{i+l}) = C_{k}, that is, Cl(v_{i+l}) = {C_{i+l} ∈ Classes(S) | Σ ⊧ C_{k}(Id : C_{i+l})}.

4. if the P_{i+1}.P_{i+2}. · · · .P_{i+l}-List satisfies PDLs 1 and 2

then add the P_{i+2}.P_{i+3}. · · · .P_{i+l}-List v_{i+1} ⟶^{P_{i+2}} v_{i+2} ⟶^{P_{i+3}} ⋯ ⟶^{P_{i+l}}

v_{i+l} to PDL_{i+l}^{i+1}.

end □

Example 16: In Example 15, let us compute PDL_{2}^{2} from PDL_{1}^{1}. Note that l = 1 in the example. By executing Procedure 6 for class a_{3} and path description A, we obtain PDL_{1} as follows: {(a_{3}, a_{3}), (a_{3}, ⊥), (⊥, a_{3}), (⊥, ⊥)}. Thus PDL_{1}^{1} = {(a_{3}), (⊥)}, which is obtained from PDL_{1} by removing v_{0} for each ‘A’-List

v_{0} ⟶^{A} v_{1} ∈ PDL_{1}.

For (a_{3}) ∈ P DL_{1}^{1}, the set of ‘B’-Lists satisfying the if condition of Step 4 is {(a_{3}, b_{3}), (a_{3}, b_{4}), (a_{3}, ⊥)}, which are constructed in Step 3. Thus (b_{3}), (b_{4}), and (⊥) should be added to PDL_{2}^{2} in Step 4. Similarly, Steps 3 and 4 are executed for (⊥) ∈ PDL_{1}^{1}. Finally, we obtain PDL_{2}^{2} = {(b_{3}), (b_{4}), (⊥)}.

For (b_{3}) ∈ PDL_{2}^{2}, since b_{4} ∉ Cl(v_{2}) = {b_{1}, b_{2}, b_{3}} where Msc(v_{2}) = b_{3}, it holds that Σ |̸=_{MSC} a_{3}(A.B : b_{4}). On the other hand, since b_{2} ∈ Cl(v_{2}) for every list in PDL_{2}^{2}, it holds that Σ ⊧_{MSC} a_{3}(A.B : b_{2}). These facts was also shown in Example 15. □

We prove that PDL_{i+l}^{i+1} is correctly computed by Procedure 7. Let v_{i} ⟶^{P_{i+1}}

v_{i+1} ⟶^{P_{i+2}} ⋯ ⟶^{P_{i+l−1}} v_{i+l−1} be in PDL_{i+l−1}^{i}. By definition, there is a pd_{i+l−1}-

List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i+l−1}} v_{i+l−1} in PDL_{i+l−1} satisfying the four conditions: MSC, PDL 1, PDL 2, and C ∈ Cl(v_{0}). By the for loop on variable k in Step 2, we check exhaustively whether or not the P_{i+1}.P_{i+2}. · · · .P_{i+l}-List v_{i} ⟶^{P_{i+1}} v_{i+1} ⟶^{P_{i+2}} ⋯ ⟶^{P_{i+l}} v_{i+l} satisfies PDLs 1 and 2 for all possible Msc(v_{i+l}). Clearly, the P_{i+1}.P_{i+2}. · · · .P_{i+l}-List satisfies MSC. Thus by Lemma 13, PDL_{i+l}^{i+1} can be computed by Procedure 7.

Now consider the time complexity of Procedure 7. Since a P_{i+1}.P_{i+2} · · · .P_{i+l−1}- List consists of l vertices, the number of lists in PDL_{i+l−1}^{i} is at most (K + 1)^{l}. Thus by the for loop of Step 2, Steps 3 and 4 are executed at most (K + 1)^{l+1} times, that is, O(K^{l+1}) times. Step 3 can be executed in O(D) time, since Cl(v_{i+l}) can be computed in O(D) time. Since the size of a P_{i+1}.P_{i+2}. · · · .P_{i+l}-List is O(D ·l), it can be tested in O(D ·l) time whether or not the P_{i+1}.P_{i+2}. · · · .P_{i+l}-List constructed in Step 4 satisfies PDLs 1 and 2. That is, one execution of Steps 3 and 4 can be done in O(D · l) time. Hence Procedure 7 can be executed in O(K^{l+1} · D · l) time.

In order to decide whether or not Σ ⊧_{MSC} C(pd : C′), we want to compute PDL_{n}^{n−l+1} by Procedure 7. Initially, we must compute PDL_{l}^{1}. By Procedure 6, PDL_{l} can be computed in O(K^{l+1} · D · l) time. After that, PDL_{l}^{1} can be constructed by removing vertex v_{0} and its incident arc v_{0} ⟶^{P_{1}} v_{1} for each pd_{l}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{l}} v_{l} in PDL_{l}. This can be done in O(K^{l+1} · D · l) time, since the size of PDL_{l} is O(K^{l+1} · D · l). Thus PDL_{l}^{1} can be computed in O(K^{l+1} · D · l) time.

By executing Procedure 7 for 2 ≤ i ≤ n−l+1, we can compute PDL_{n}^{n−l+1}. It takes O(K^{l+1} · D · l · (n − l + 1)) time, since each execution of Procedure 7 takes O(K^{l+1} · D · l) time. Hence PDL_{n}^{n−l+1} can be computed in O(K^{l+1} · D · l · (len(pd) + 1)) time, where n = len(pd). Since the size of PDL_{n}^{n−l+1} is O(K^{l+1} · D · l), it can be decided in O(K^{l+1} · D · l) time whether or not

there is a P_{n−l+2}.P_{n−l+3}. · · · .P_{n}-List v_{n−l+1} ⟶^{P_{n−l+2}} v_{n−l+2} ⟶^{P_{n−l+3}} ⋯ ⟶^{P_{n}} v_{n} in

PDL_{n}^{n−l+1} such that C′ ∉ Cl(v_{n}).

Therefore, it can be decided in in O(K^{l+1} · D · l · (len(pd) + 1)) time whether or not Σ ⊧_{MSC} C(pd : C′). Consequently, Theorem 7(a) also holds in the case that len(pd) > l. This completes proving Theorem 7(a). □

Proof of Theorem 7(b):

Since Id is trivially in PathDescs_{MSC}(C), assume that pd ≠ Id. By Lemma 12, pd ∉ PathDescs_{MSC}(C) if and only if there is a pd_{i}-List satisfying the six conditions of Lemma 12. We first show that given an integer i with i < len(pd), it can be decided in O(K^{i+1} ·D ·(i+1)) time whether or not there is a pd_{j}-List satisfying the six conditions of Lemma 12 and j ≤ i.

Intuitively, this can be done by (1) generating all pd_{i}-Lists satisfying MSC and (2) checking whether or not there is a pd_{j}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{j}} v_{j} satisfying the six conditions of Lemma 12 for each generated pd_{i}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} v_{i}. By slightly modifying Procedure 6, we can execute Step 1. Consider Step 2. Let v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} v_{i} be a pd_{i}-List satisfying MSC. We must check whether or not there is an index j such that the pd_{j}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{j}} v_{j} satisfies the six conditions of Lemma 12. This can be done by the following procedure.

Procedure 8: (Deciding whether or not there is an index j such that the pd_{j}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{j}} v_{j} satisfies the six conditions of Lemma 12.) input: a class C ∈ Classes(S), a path description pd (= P_{1}.P_{2}. · · · P_{n}), and a pd_{i}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} v_{i} satisfying MSC.

1. for j ← 0 to i do

2. if C ∈ Cl(v_{0}), Cl(v_{j}) ∩ Dom(P_{j+1}) = ∅, and the pd_{j}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{j}} v_{j} satisfies Σ_{SC} then return YES. □

Example 17: Consider Example 14. Let us execute Procedure 8 for class a_{1}, path description A.B.C, and the ‘A.B’-List given in Figure 17. Then YES should be returned when j = 2. In fact, the ‘A.B’-List satisfies all the conditions of Lemma 12. □

We prove that Procedure 8 returns YES if and only if there is an index j such that the pd_{j}-List satisfies the six conditions of Lemma 12. Assume that Procedure 8 returns YES when j = m. We must prove that the pd_{m}- List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{m}} v_{m} satisfies the six conditions of Lemma 12. By the if condition of Step 2, the pd_{m}-List satisfies conditions (2), (3), and (6) of Lemma 12. Since the pd_{i}-List satisfies MSC, so does the pd_{m}-List; that is, the pd_{m}-List satisfies condition (4). Since m < i ≤ len(pd), the pd_{m}- List satisfies conditions (1). It remains to show that the pd_{m}-List satisfies condition (5). Assume that the pd_{m}-List does not satisfy condition (5). Let m′ be the smallest index such that the pd_{m′}-List satisfies condition (5). Then m′ < m. Since the pd_{m}-List satisfies Σ_{SC} and C ∈ Cl(v_{0}), so does the pd_{m′}- List. By the minimality of m′, it holds that Cl(v_{m′}) ∩ Dom(P_{m′+1}) = ∅. Thus the if condition of Step 2 should hold when j = m′; that is, Procedure 8 should return YES when j = m′. Contradiction. Hence the pd_{m}-List satisfies the six conditions of Lemma 12. Conversely, assume that there is an index m such that the pd_{m}-List satisfies the six conditions of Lemma 12. It is easy to see that Procedure 8 returns YES when j = m. This completes proving the correctness of Procedure 8.

We now estimate the time complexity. By slightly modifying Procedure 6, we can generate all pd_{i}-Lists v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{l}} v_{i} satisfying MSC in O(K^{i+1}·D·(i+1)) time. After that, Procedure 8 is executed for each generated pd_{i}-List. Since the number of pd_{i}-Lists is at most (K + 1)^{i+1}, Procedure 8 is executed at most (K + 1)^{i+1} times, that is, O(K^{l+1}) times. Furthermore, since the size of a pd_{i}-List is O(D · (i + 1)), Procedure 8 can be executed in O(D ·(i+1)) time. Thus the total time for Procedure 8 is O(K^{i+1} ·D ·(i+1)). Consequently, it can be decided in O(K^{i+1} · D · (i + 1)) time whether or not there is a pd_{j}-List satisfying the six conditions of Lemma 12 and j ≤ i.

Consider how to decide whether or not pd ∈ PathDescs_{MSC}(C). By the discussions above, it can be decided in O(K^{len(pd)+1} · D · (len(pd) + 1)) time whether or not there is a pd_{j}-List satisfying the six conditions of Lemma 12 and j < len(pd). That is, it can be decided in O(K^{len(pd)+1} · D · (len(pd) + 1)) time whether or not pd ∈ PathDescs_{MSC}(C). Hence if len(pd) ≤ l, then Theorem 7(b) holds.

Assume that len(pd) > l. By the discussions above, it can be decided in O(K^{l+1} · D · l) time whether or not there is a pd_{j}-List satisfying the six conditions of Lemma 12 and j < l. It remains to check whether or not there is a pd_{j}-List satisfying the six conditions of Lemma 12 for some j such that l ≤ j ≤ n − 1. Note that PDL_{i+l−1}^{i} is the set of P_{i+1}.P_{i+2}. · · · .P_{i+l−1}-

Lists such that v_{i} ⟶^{P_{i+1}} v_{i+1} ⟶^{P_{i+2}} ⋯ ⟶^{P_{i+l−1}} v_{i+l−1} is in PDL_{i+l−1}^{i} if and

only if there is a pd_{i+l−1}-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i+l}} v_{i+l−1} satisfying the four conditions: MSC, PDL 1, PDL 2, and C ∈ Cl(v_{0}). Thus there is a pd_{i+l−1}-List satisfying the six conditions of Lemma 12 if and only if there is a

P_{i+1}.P_{i+2}. · · · .P_{i+l−1}-List v_{i} ⟶^{P_{i+1}} v_{i+1} ⟶^{P_{i+2}} ⋯ ⟶^{P_{i+l−1}} v_{i+l−1} in PDL_{i+l−1}^{i} satis-

fying Cl(v_{i+l−1})∩Dom(P_{i+l}) = ∅. That is, by using PDL_{i+l−1}^{i} for 1 < i ≤ n−l, we can check whether or not there is a pd_{j}-List satisfying the six conditions of Lemma 12 for some j such that l ≤ j ≤ n − 1. Since the size of PDL_{i+l−1}^{i} is O(K^{l+1} · D · l), it can be decided in O(K^{l+1} · D · l) time whether

or not there is a P_{i+1}.P_{i+2}. · · · .P_{i+l−1}-List v_{i} ⟶^{P_{i+1}} v_{i+1} ⟶^{P_{i+2}} ⋯ ⟶^{P_{i+l−1}} v_{i+l−1}

in PDL_{i+l−1}^{i} satisfying Cl(v_{i+l−1}) ∩ Dom(P_{i+l}) = ∅. Thus we can check in O(K^{l+1}·D·l·(len(pd)+1)) time, provided that PDL_{i+l−1}^{i} is known for all i such that 1 ≤ i ≤ n−1. Note that when deciding whether or not Σ ⊧_{MSC} C(pd : C′), we have computed PDL_{i+l−1}^{i} for all i in O(K^{l+1} · D · l · (len(pd) + 1)) time. As a result, it can be checked in O(K^{l+1} · D · l · (len(pd) + 1)) time whether or not there is a pd_{j}-List satisfying the six conditions of Lemma 12 for some j such that l ≤ j ≤ n − 1. Consequently, Theorem 7(b) also holds in the case that len(pd) > l. This completes proving Theorem 7(b). □

Proof of Theorem 7(c): Consider how to decide whether or not pd ∈ PathFuncs_{MSC}(C). Since it can be decided in O(D · (len(pd) + 1)) time whether or not FUNC(P_{i}) ∈ Σ_{FUNC} for 1 ≤ i ≤ n, Theorem 7(c) follows from Corollary 1 and Theorem 7(b). □

4. MSC with the Lower Semilattice Condition

If we restrict our attention to interpretations which satisfy MSC, then the decision problems related to SCs are NP-complete, as shown in Section 3.1. In this section, we consider a special case in which a given database schema ⟨S, Σ⟩ satisfies the following additional condition.

The lower semilattice condition: A class C is called a greatest common subclass of C_{1} and C_{2} if and only if the following two conditions hold.

1. Σ ⊧ C(Id : C_{1}) and Σ ⊧ C(Id : C_{2}).

2. If there is a class C_{3} ∈ Classes(S) such that Σ ⊧ C_{3}(Id : C_{1}) and Σ ⊧ C_{3}(Id : C_{2}), then Σ ⊧ C_{3}(Id : C).

Then ⟨S, Σ⟩ satisfies the lower semilattice condition if and only if for all C_{1}, C_{2} ∈ Classes(S), there is a unique greatest common subclass of C_{1} and C_{2}, denoted C_{1} ⊓ C_{2}.^{15} □

For example, the taxonomy illustrated in Figure 14 satisfies the lower semilattice condition (if the taxonomy is considered as a database schema by itself). On the other hand, the taxonomy illustrated in Figure 13 does not satisfy the lower semilattice condition, since classes A_{i} and B_{i} do not have a unique greatest common subclass. Thus the whole database schema constructed in Lemma 11 does not satisfy the lower semilattice condition, either. Through this section, we consider the case that ⟨S, Σ⟩ satisfies the lower semilattice condition.

15This condition implies that Classes(S) contains a bottom class ⊥.

4.1 Axiomatization In this section, it will be shown that the following axiom together with A1 and A2 in Section 2.2 are sound and complete for deciding whether or not Σ ⊧_{MSC} C(pd : C′), provided that pd ∈ PathDescs_{MSC}(C).

A4: (restriction) If C_{1}(pd : C_{2}) and C_{1}(pd : C_{3}), then C_{1}(pd : C_{2} ⊓ C_{3}).

Soundness of axiom A4 is straightforward. The proof of completeness is analogous to Theorem 2 in Section 2.2. In particular, if Σ ⊬_{{A1,A2,A4}} C(pd : C′), then we will construct a pd-List satisfying MSC as well as PDLs 1 to 3. (Thus Σ |̸=_{MSC} C(pd : C′) by Theorem 5.) We need to modify the concept of chase in order to satisfy MSC.

The MSC-chase of C and pd under Σ_{SC}, written ChaseΣSC^{MSC}(C, pd), is a pd-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} obtained by the following procedure, where pd = P_{1}.P_{2}. · · · .P_{n}.

Procedure 9: (Computing ChaseΣSC^{MSC}(C, pd).) input: a database schema ⟨S, Σ⟩ satisfying the lower semilattice condition, a class C ∈ Classes(S), and a path description pd (= P_{1}.P_{2}. · · · .P_{n}).

1. Construct a pd-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} such that Cl(v_{0}) = { C } and Cl(v_{i}) = ∅ for 1 ≤ i ≤ n.

2. Apply the following rule to the pd-List exhaustively. Note that the pd-List always satisfies MSC, as will be shown in Lemma 14 below.

MSC-SC-rule: For an SC C_{a}(pd′ : C_{b}) ∈ Σ_{SC}, if there are two vertices v_{i}, v_{j} such that C_{a} ∈ Cl(v_{i}), C_{b} ∉ Cl(v_{j}), and pd′ has the form P_{i+1}.P_{i+2}. · · · .P_{j}, then add not only C_{b} but also Msc(v_{j}) ⊓ C_{b} to Cl(v_{j}).^{16} For convenience, if Cl(v_{j}) = ∅, then let Msc(v_{j})⊓C_{b} = C_{b}.

□

16Msc(v_{j}) ⊓ C_{b} is unique, since ⟨S, Σ⟩ satisfies the lower semilattice condition.

Example 18: Let ⟨S, Σ⟩ be a database schema illustrated in Figure 18, where Dom(A) = { a_{1} }, Dom(B) = { a_{3} }, Dom(C) = { b_{2} }. For class a_{1} and path description A.B.C, let us execute Procedure 9.

   a_{1}{A}  _{a_{2}} a_{3}{B}  _{b_{1}}  b_{2}{C}_{b_{3}}  _{c_{1}}_{c_{2}}  _{c_{3}} ⊥  C     C B        B A A

Figure 18: A database schema ⟨S, Σ⟩.

In Step 1, an ‘A.B.C’-List v_{0} ⟶^{B} v_{1} ⟶^{A} v_{2} ⟶^{C} v_{3} is constructed, where Cl(v_{0}) = { a_{1} } and Cl(v_{i}) = ∅ for 1 ≤ i ≤ 3.

For SC a_{1}(A:a_{1}) in Σ_{SC}, since a_{1} ∈ Cl(v_{0}) and a_{1} ∉ Cl(v_{1}), class a_{1} is added to Cl(v_{1}) by applying the MSC-SC-rule for a_{1}(A:a_{1}), where Msc(v_{1}) ⊓ a_{1} = a_{1} since Cl(v_{1}) = ∅. The MSC of v_{1} becomes a_{1} by the application. For SC a_{1}(A:a_{2}) in Σ_{SC}, since a_{1} ∈ Cl(v_{0}) and a_{2} ∉ Cl(v_{1}), classes Msc(v_{1}) ⊓ a_{2} as well as a_{2} are added to Cl(v_{1}) by applying the MSC-SC-rule for a_{1}(A:a_{2}), where Msc(v_{1}) ⊓ a_{2} = a_{1} ⊓ a_{2} = a_{3}. The MSC of v_{1} changes from a_{1} to a_{3} by the application. Finally, we obtain the ‘A.B.C’-List given in Figure 19 as ChaseΣSC^{MSC}(a_{1}, A.B.C), where each vertex is labeled its MSC. Note that ChaseΣSC^{MSC}(a_{1}, A.B.C) satisfies Σ_{SC}. □

            a_{1}  A     _{a_{3}}  B     _{b_{3}}  C     _{c_{2}}

Figure 19: ChaseΣSC^{MSC}(a_{1}, A.B.C).

It will be shown that if Σ ⊬_{{A1,A2,A4}} C(pd : C′) and pd ∈ PathDescs_{MSC}(C), then ChaseΣSC^{MSC}(C, pd) satisfies MSC as well as PDLs 1 to 3.

Lemma 14: ChaseΣSC^{MSC}(C, pd) satisfies MSC.

Proof. We prove by induction on the number of applying MSC-SC-rules in Step 2 that the pd-List v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} satisfies MSC during Procedure 9. Thus Lemma 14 will hold.

The basis is trivial, since Cl(v_{0}) = { C } and Cl(v_{i}) = ∅ for 1 ≤ i ≤ n in Step 1.

As an induction hypothesis, assume that the pd-List satisfies MSC during an execution of Step 2. Let Msc(v_{j}) = C_{j} and assume that C_{j}⊓C_{b} as well as C_{b} are added to Cl(v_{j}) by applying an MSC-SC-rule to the pd-List. We show that Msc(v_{j}) is changed from C_{j} to C_{j} ⊓C_{b} by the application. Since Msc(v_{j}) = C_{j} before the application, Σ ⊧ C_{j}(Id : C′_{j}) for every C′_{j} ∈ Cl(v_{j}) − {C_{b}, C_{j} ⊓ C_{b}}. By definition, Σ ⊧ C_{j} ⊓ C_{b}(Id : C_{j}) and Σ ⊧ C_{j} ⊓ C_{b}(Id : C_{b}). Thus Σ ⊧ C_{j} ⊓ C_{b}(Id : C′_{j}) for every C′_{j} ∈ Cl(v_{j}). That is, Msc(v_{j}) = C_{j} ⊓ C_{b} after the application. Hence the pd-List still satisfies MSC. This completes the induction proof. □

Consider PDL 2. By the definition of MSC-SC-rule, unless the pd-List satisfies Σ_{SC}, Procedure 9 does not terminate. Thus ChaseΣSC^{MSC}(C, pd) satisfies Σ_{SC}; that is, PDL 2 holds.

Consider PDL 3. By Step 1 of Procedure 9, it holds that C ∈ Cl(v_{0}). By the following lemma, if Σ ⊬_{{A1,A2,A4}} C(pd : C′), then it holds that C′ ∉ Cl(v_{n}). Thus if Σ ⊬_{{A1,A2,A4}} C(pd : C′), then ChaseΣSC^{MSC}(C, pd) satisfies PDL 3.

Lemma 15: Cl(v_{i}) = {C_{i} ∈ Classes(S) | Σ_{SC} ⊢_{{A1,A2,A4}} C(pd_{i} : C_{i})} for 0 ≤ i ≤ n.

Proof. The proof is analogous to Lemma 5.

We first prove that if Σ_{SC} ⊢_{{A1,A2,A4}} C(pd_{i} : C_{i}), then C_{i} ∈ Cl(v_{i}). Assume that Σ_{SC} ⊢_{{A1,A2,A4}} C(pd_{i} : C_{i}). Then Σ_{SC} ⊧_{MSC} C(pd_{i} : C_{i}) by soundness of the axioms. Thus ChaseΣSC^{MSC}(C, pd) satisfies C(pd_{i} : C_{i}), since it satisfies Σ_{SC} by PDL 2. Hence C ∈ Cl(v_{0}) implies C_{i} ∈ Cl(v_{i}).

We next prove that if C_{i} ∈ Cl(v_{i}), then Σ_{SC} ⊢_{{A1,A2,A4}} C(pd_{i} : C_{i}). If Cl(v_{i}) = ∅, then there is nothing to prove. Assume that C_{i} ∈ Cl(v_{i}). By definition, Σ ⊧ Msc(v_{i})(Id : C_{i}). Thus by Theorem 2, Σ ⊢_{{A1,A2}} Msc(v_{i})(Id : C_{i}), since Id ∈ PathDescs(C). Hence in order to prove that Σ_{SC} ⊢_{{A1,A2,A4}} C(pd_{i} : C_{i}), it suffices to show that Σ ⊢_{{A1,A2,A4}} C(pd_{i} : Msc(v_{i})). Induction on the number of applying MSC-SC-rules in Step 2.

The basis follows from axiom A1, since Cl(v_{0}) = { C } and Cl(v_{i}) = ∅ for 1 ≤ i ≤ n in Step 1.

As an induction hypothesis, assume that Σ ⊢_{{A1,A2,A4}} C(pd_{i} : Msc(v_{i})) during an execution of Step 2, where Cl(v_{i}) ≠ ∅. Assume that Msc(v_{j}) ⊓ C_{b} as well as C_{b} should be added to Cl(v_{j}) by applying an MSC-SC-rule for C_{a}(pd′ : C_{b}) ∈ Σ_{SC}. Then by the definition of SC-rule, it holds that C_{b} ∉ Cl(v_{j}), C_{a} ∈ Cl(v_{k}), and pd′ = P_{k+1}.P_{k+2}. · · · .P_{j} for some k. It suffices to show that Σ ⊢_{{A1,A2,A4}} C(pd_{j} : Msc(v_{j}) ⊓ C_{b}), since the MSC of v_{j} is changed from Msc(v_{j}) to Msc(v_{j}) ⊓ C_{b}. Since C_{a} ∈ Cl(v_{k}), it follows from the induction hypothesis that Σ ⊢_{{A1,A2,A4}} C(pd_{k} : C_{a}). By axiom A2, C(pd_{k} : C_{a}) and C_{a}(pd′ : C_{b}) imply C(pd_{k} ∘ pd_{j} : C_{b}), where pd_{k} ∘ pd′ = pd_{j}. That is, Σ ⊢_{{A1,A2,A4}} C(pd_{j} : C_{b}). Furthermore, Σ ⊢_{{A1,A2,A4}} C(pd_{j} : Msc(v_{j})) by the induction hypothesis. Thus C(pd_{j} : Msc(v_{j})) and C(pd_{j} : C_{b}) imply C(pd_{j} : Msc(v_{j}) ⊓ C_{b}) by axiom A4. Hence Σ ⊢_{{A1,A2,A4}} C(pd_{j} : Msc(v_{j}) ⊓ C_{b}). This completes the induction proof. Consequently, Lemma 15 holds. □

By the following lemma, if pd ∈ PathDescs_{MSC}(C), then ChaseΣSC^{MSC}(C, pd) satisfies PDL 3.

Lemma 16: pd ∈ PathDescs_{MSC}(C) if and only if ChaseΣSC^{MSC}(C, pd) satisfies a property value integrity condition.

Proof. (Almost the same as proving Lemma 6.) □

Consequently, we have the following theorem, which can be proved in the same way as proving Theorem 2.

Theorem 8: Assume that ⟨S, Σ⟩ satisfies the lower semilattice condition. If pd ∈ PathDescs_{MSC}(C), then the following three statements are equivalent.^{17}

1. Σ ⊧_{MSC} C(pd : C′).

2. Σ ⊢_{{A1,A2,A4}} C(pd : C′).

3. C′ ∈ Cl(v_{n}). □

17Σ is not necessarily well-formed with respect to ⟨S, Σ⟩.

Example 19: Consider Example 18. We have obtained the ‘A.B.C’-List in Figure 19 as ChaseΣSC^{MSC}(a_{1}, A.B.C). The ‘A.B.C’-List satisfies a property value integrity condition. Thus A.B.C ∈ PathDescs_{MSC}(a_{1}) by Lemma 16. Since c_{2} ∈ Cl(v_{2}) = {c_{1}, c_{2}} where Msc(v_{2}) = c_{2}, it follows from Theorem 8 that Σ ⊧_{MSC} a_{1}(A.B.C : c_{2}). On the other hand, Σ |̸=_{MSC} a_{1}(A.B.C : c_{3}) by Theorem 8, since c_{3} ∉ Cl(v_{2}). □

4.2 The three decision problems In this section, we will prove the following theorem.

Theorem 9: Assume that ⟨S, Σ⟩ satisfies the lower semilattice condition. The following three decision problems are solved in O(D·(len(pd)+1)) time, where D is the size of ⟨S, Σ⟩.

a. Σ ⊧_{MSC} C(pd : C′) (provided that pd ∈ PathDescs_{MSC}(C)) ?

b. pd ∈ PathDescs_{MSC}(C) ?

c. pd ∈ PathFuncs_{MSC}(C) ? □

As in Section 2.3, the time for computing ChaseΣSC^{MSC}(C, pd) dominates the time complexities of the three decision problems. In the following, we will present a procedure for computing ChaseΣSC^{MSC}(C, pd). After that, it will be proved that the procedure can be executed in O(D · (len(pd) + 1)) time. Hence Theorem 10 can be proved in the same way as Theorem 4.

The procedure is a modification of Procedure 3. Note that Cl(v_{i}) is computed from Msc(v_{i}). In fact, the procedure will compute Msc(v_{i}) and then Cl(v_{i}) for 1 ≤ i ≤ n.

Procedure 10: (Computing ChaseΣSC^{MSC}(C, pd).) input: a database schema ⟨S, Σ⟩ satisfying the lower semilattice condition, a class C ∈ Classes(S), and a path description pd (= P_{1}.P_{2}. · · · .P_{n}).

1. Divide Σ_{SC} into two sets: Σ_{Id} = {C_{a}(pd′ : C_{b}) ∈ Σ_{SC} | pd′ = Id} and Σ_{¬Id} = Σ_{SC} − Σ_{Id}.

2. Let CL_{0} ← {C_{0} ∈ Classes(S) | Σ_{Id} ⊢_{{A1,A2}} C(Id : C_{0})}.

3. for i ← 1 to n

do begin 4. Let CL ← {C_{b} ∈ Classes(S) | there is an SC C_{a}(pd′ : C_{b}) ∈ Σ_{¬Id} such that pd′ = P_{j+1}.P_{j+2}. · · · .P_{i} and C_{a} ∈ CL_{j} for some j }.

5. if CL = ∅ then let CL_{i} ← ∅

else begin

6. Let M_{i} ← ⊓_{C_{b}∈CL} C_{b}.^{18}

7. Let CL_{i} ← {C_{i} ∈ Classes(S) | Σ_{Id} ⊢_{{A1,A2}} M_{i}(Id : C_{i})}. end

end □

The correctness of Procedure 10 follows from the following lemma.

Lemma 17: CL_{i} = Cl(v_{i}) for 0 ≤ i ≤ n, where ChaseΣSC^{MSC}(C, pd) is v_{0} ⟶^{P_{1}}

v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n}.

Proof. The proof is analogous to Lemma 7. By Lemma 15, it suffices to show that

CL_{i} = {C_{i} ∈ Classes(S) | Σ_{SC} ⊢_{{A1,A2,A4}} C(pd_{i} : C_{i})}. (4.1)

We prove 4.1 by induction on i.

Basis. Consider the case that i = 0. Note that Steps 1 and 2 of Procedure 10 is the same as Steps 1 and 2 of Procedure 3. Thus it follows from Lemmas 5 and 7 that CL_{0} = {C_{0} ∈ Classes(S) | Σ_{SC} ⊢_{{A1,A2}} C(Id : C_{0})}. Hence v_{0} satisfies Σ_{SC} by itself. Clearly, Msc(v_{0}) = C; that is, v_{0} satisfies MSC. These facts imply that no class is added to CL_{0} by applying axiom A4. Thus 4.1 holds for i = 0.

Induction. As an induction hypothesis, assume that 4.1 holds for j ≤ i−1, where i ≥ 1. Proof of ‘⊆’: We prove that if C_{i} ∈ CL_{i}, then Σ_{SC} ⊢_{{A1,A2,A4}} C(pd_{i} : C_{i}). If CL_{i} = ∅, then there is nothing to prove. Assume that CL_{i} ≠ ∅. We claim that Σ_{SC} ⊢_{{A1,A2,A4}} C(pd_{i} : C_{b}) for every C_{b} ∈ CL.

Let C_{b} ∈ CL. By Step 4, there is an SC C_{a}(pd′ : C_{b}) ∈ Σ_{¬Id} such that pd′ = P_{j+1}.P_{j+2}. · · · .P_{i} and C_{a} ∈ CL_{j} for some j. Since pd′ ≠ Id by the definition of Σ_{¬Id}, it holds that j ≤ i − 1. Thus by the induction hypothesis, C_{a} ∈ CL_{j} implies that Σ_{SC} ⊢_{{A1,A2,A4}} C(pd_{j} : C_{a}). By axiom A2, C(pd_{j} : C_{a}) and C_{a}(pd′ : C_{b}) imply C(pd_{j} ∘ pd′ : C_{b}), where pd_{j} ∘ pd′ = pd_{i}. That is, Σ_{SC} ⊢_{{A1,A2,A4}} C(pd_{i} : C_{b}). Hence the claim holds.

18M_{i} is well-defined, since ⟨S, Σ⟩ satisfies the lower semilattice condition.

Note that M_{i} ← ⊓_{C_{b}∈CL} C_{b} by Step 6. Thus C(pd_{i} : M_{i}) can be derived by applying axiom A4 repeatedly to {C(pd_{i} : C_{b}) | C_{b} ∈ CL}. Hence by the claim above, it holds that Σ_{SC} ⊢_{{A1,A2,A4}} C(pd_{i} : M_{i}). Since M_{i} = Msc(v_{i}) by Step 7, this implies that Σ_{SC} ⊢_{{A1,A2,A4}} C(pd_{i} : C_{i}) for every C_{i} ∈ CL_{i}. This completes the proof of ‘⊆’. Proof of ‘⊇’: We prove that if Σ_{SC} ⊢_{{A1,A2,A4}} C(pd_{i} : C_{i}), then C_{i} ∈ CL_{i}. Assume that Σ_{SC} ⊢_{{A1,A2,A4}} C(pd_{i} : C_{i}). Then Σ_{SC} ⊧_{MSC} C(pd_{i} : C_{i}) by soundness of the axioms. Let u_{0} ⟶^{P_{1}} u_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} u_{i} be a pd_{i}-List such that Cl(u_{j}) = CL_{j} for 0 ≤ j ≤ i. We will prove that the pd_{i}-List satisfies Σ_{SC}, and thus C(pd_{i} : C_{i}). Since C ∈ CL_{0}, this will imply that C_{i} ∈ CL_{i}.

Since CL_{j} = Cl(v_{j}) for 0 ≤ j ≤ i − 1 by the induction hypothesis and Lemma 15, the pd_{i−1}-List u_{0} ⟶^{P_{1}} u_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{i}} u_{i−1} satisfies Σ_{SC}, which can be proved along the same line as proving Lemma 4(a). By Step 4, for every SC C_{a}(pd′ : C_{b}) ∈ Σ_{¬Id}, if pd′ = P_{j+1}.P_{j+2}. · · · .P_{i} and C_{a} ∈ CL_{j}, then C_{b} ∈ CL_{i}. Thus the pd_{i}-List satisfies Σ_{¬Id}. Similarly, by Step 7, for every SC C_{a}(Id : C_{b}) ∈ Σ_{Id}, if C_{a} ∈ CL_{i}, then C_{b} ∈ CL_{i}. Thus the pd_{i}-List also satisfies Σ_{Id}. Since Σ_{SC} = Σ_{¬Id} ∪ Σ_{Id} by definition, the pd_{i}-List satisfies Σ_{SC}. This completes the induction proof. Consequently, Lemma 17 holds. □

Let us estimate the time complexity of Procedure 10. As before, let Classes(S) consist of K classes and use a bit array of size K in order to represent a subset of Classes(S). Procedure 10 is essentially the same as Procedure 3 except Step 6. One obvious way for executing Step 6 is to construct in advance a table containing C_{a} ⊓ C_{b} for every pair of C_{a}, C_{b} ∈ Classes(S). Once the table is constructed, Step 6 can be executed in O(K) time, since the size of CL is at most K. Note that K ≤ D. Thus it will be shown in the same way as estimating Procedure 3 that Procedure 10 can be executed in O(D · (len(pd) + 1)) time. In the following we will present a procedure for constructing the table in O(K^{3}) time. The procedure consists of the following three parts.

1. Sort the classes in Classes(S) in a topological order with respect to the generalization taxonomy. Here, a sequence C_{t_{1}}, C_{t_{2}}, ⋯, C_{t_{K}} is in a topological order if and only if Σ_{Id} ⊧ C_{t_{i}}(Id : C_{t_{j}}) implies i ≤ j.

2. Compute {C_{i} ∈ Classes(S) | Σ_{Id} ⊢_{{A1,A2}} C_{t_{i}}(Id : C_{i})} for 1 ≤ i ≤ K.

3. Compute C_{a} ⊓ C_{b} for every pair of C_{a}, C_{b} ∈ Classes(S).

Consider how to execute Part 1. Let G(V, A) be a directed graph such that V = Classes(S) and A = {C_{a} → C_{b} | C_{a}(Id : C_{b}) ∈ Σ_{Id}}. G(V, A) can be constructed in O(K +∥Σ_{Id}∥) time. Clearly, there is a directed path in G(V, A) from a vertex C_{1} to a vertex C_{2} if and only if Σ_{Id} ⊧ C_{1}(Id : C_{2}). Since S is a generalization taxonomy with respect to Σ by assumption, G(V, A) contains no directed cycle. Thus the vertices in V can be sorted in a topological order. Let C_{t_{1}}, C_{t_{2}}, ⋯, C_{t_{K}} be a sequence in a topological order; that is, if there is a directed path in G(V, A) from C_{t_{i}} to C_{t_{j}}, then i ≤ j. In other words, if Σ_{Id} ⊧ C_{t_{i}}(Id : C_{t_{j}}), then i ≤ j. Such a sequence C_{t_{1}}, C_{t_{2}}, ⋯, C_{t_{K}} can be obtained in O(K + ∥Σ_{Id}∥) time by using G(V, A).^{19} Since the number of SCs of the form C_{a}(Id : C_{b}) is at most K^{2}, the size of Σ_{Id} is O(K^{2}). Hence Part 1 can be execute in O(K^{2}) time.

Consider Part 2. Since {C_{i} ∈ Classes(S) | Σ_{Id} ⊢_{{A1,A2}} C_{t_{i}}(Id : C_{i})} can be computed in O(K + ∥Σ_{Id}∥) time by using an algorithm for computing a reflexive transitive closure as discussed in Section 2.3, Part 2 can be executed in O(K · (K + ∥Σ_{Id}∥)) time, that is, O(K^{3}) time.

Finally, consider how to execute Part 3. For a pair of C_{a}, C_{b} ∈ Classes(S), let i be the largest integer satisfying

{C_{a}, C_{b}} ⊆ {C_{i} ∈ Classes(S) | Σ_{Id} ⊢_{{A1,A2}} C_{t_{i}}(Id : C_{i})}. (4.2)

We claim that C_{t_{i}} = C_{a} ⊓ C_{b}.

Let t_{j} be an index such that C_{t_{j}} = C_{a} ⊓ C_{b}. Since Σ_{Id} ⊧ C_{t_{i}}(Id : C_{a}) and Σ_{Id} ⊧ C_{t_{i}}(Id : C_{b}) by 4.2, it follows from the definition of C_{a} ⊓ C_{b} that Σ_{Id} ⊧ C_{t_{i}}(Id : C_{t_{j}}). Since C_{t_{1}}, C_{t_{2}}, ⋯, C_{t_{K}} is in a topological order, this implies that i ≤ j. On the other hand, it must hold that j ≤ i, since i is the largest integer satisfying 4.2. Thus i = j, that is, C_{t_{i}} = C_{a} ⊓ C_{b}. This completes proving the claim.

Since a subset of Classes(S) can be represented by a bit array of size K, a set membership can be tested in constant time. Thus it can be decided in constant time whether or not an integer i satisfies 4.2, where 1 ≤ i ≤ K. Hence we can find in O(K) time the largest integer i satisfying 4.2, and therefore C_{a} ⊓ C_{b}. Since the number of entries of the table is O(K^{2}), we can construct the table in O(K^{3}) time. That is, Part 3 can be executed in O(K^{3}) time. Consequently, Parts 1 to 3 can also be executed in O(K^{3}) time.

19In general, given a directed acyclic graph G(V, A), the vertices in V can be sorted in a topological order in linear time.

Example 20: For the database schema ⟨S, Σ⟩ in Example 18, let us construct the table by the procedure above. In Part 1, the directed graph G(V, A) is constructed as in Figure 20. By using G(V, A), we may have the following sequence (as an example), which is in a topological order:

⟨⊥, a_{3}, a_{2}, c_{2}, b_{3}, a_{1}, b_{1}, b_{2}, c_{3}, c_{1}⟩

Part 2 is easy to execute. In Part 3, consider how to compute, for example, b_{1} ⊓ b_{2}. It is easy to see that only ⊥ and b_{3} satisfy 4.2 with respect to b_{1} and b_{2}. Since b_{3} occurs later than ⊥ in the sequence above; that is, b_{3} has a larger index than ⊥, it holds that b_{1} ⊓ b_{2} = b_{3}. □

a_{1}  _{a_{2}}_{a_{3}}  _{b_{1}}  _{b_{2}}_{b_{3}}  _{c_{1}}_{c_{2}}  _{c_{3}} ⊥

Figure 20: The directed graph G(V, A) in Part 1.

Once the table above is constructed, for any class C and any path description pd, ChaseΣSC^{MSC}(C, pd) can be computed in O(D · (len(pd) + 1)) time by Procedure 10. Thus it is reasonable to exclude the time for constructing the table from the time complexity of Procedure 10.

4.3 An NP-completeness result By assuming the lower semilattice condition for ⟨S, Σ⟩, the NP-complete decision problems given in Theorem 6 largely become solvable in polynomial time. Unfortunately, it is still NP-complete to decide whether or not Σ |̸=_{MSC} C(pd : C′), if pd ∉ PathDescs_{MSC}(C). (The fact will be proved in this section.) At a glance, one might consider that Σ ⊧_{MSC} C(pd : C′) if and only if Σ ⊢_{{A1,A2,A3,A4}} C(pd : C′). But this is not the case. The intuitive reason is that

even if two pd-Lists v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} and u_{0} ⟶^{P_{1}} u_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} u_{n}

satisfy MSC, a pd-List w_{0} ⟶^{P_{1}} w_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} w_{n} does not always satisfy MSC, where Cl(w_{i}) = Cl(u_{i}) ∪ Cl(v_{i}) for 0 ≤ i ≤ n. Thus we cannot use the same discussion as in proving Theorem 3.

Theorem 10: Assume that ⟨S, Σ⟩ satisfies the lower semilattice condition. It is NP-complete to decide whether or not Σ |̸=_{MSC} C(pd : C′), if pd ∉ PathDescs_{MSC}(C).

Proof. By Lemma 10, the problem is in NP. We prove its NP-hardness. The idea is essentially the same as Lemma 11. We will slightly modify the database schema ⟨S, Σ⟩ constructed in Lemma 11.

1. As for the definition of S, remove class names Z, B_{i} for 1 ≤ i ≤ n, and property R. The domain of each property is changed as follows:

Dom(P_{1}) = \{ C \}  and Dom(P_{i}) = \{ X_{i−1}, \overline{X}_{i−1} \}  for 2 ≤ i ≤ n
Dom(Q_{1}) = \{ X_{n}, \overline{X}_{n} \} and  Dom(Q_{j}) = \{ C_{j−1} \}  for 2 ≤ j ≤ m

2. The SC C(pd : C′) remains unchanged.

3. As for the definition of Σ, we have only to modify the truth-setting components (3.1.a) and the other SCs (3.1.c) in the fixed part of Σ_{SC} as follows:

For each variable x_{i}, 1 ≤ i ≤ n, replace the truth-setting component illustrated in Figure 13 by the one illustrated in Figure 21. That is, the modified truth-setting component consists of the following two SCs:

\{X_{i}(Id : A_{i}), \overline{X}_{i}(Id : A_{i})\}

Clearly, the taxonomy illustrated in Figure 21 satisfies the lower semilattice condition (if the taxonomy is considered as a database schema by itself). Note that the bottom class ⊥ is explicitly described in Figure 21, though it is unimportant for this proof as in Lemma 11.

Replace the other SCs by the following 2n + 2m − 1 SCs:

\begin{matrix}\{C(P_{1} : A_{1})\} & and & \{X_{i−1}(P_{i} : A_{i}), \overline{X}_{i−1}(P_{i} : A_{i}) | 2 ≤ i ≤ n\} \\ \{X_{n}(Q_{1} : C_{1}), \overline{X}_{n}(Q_{1} : C_{1})\} & and & \{C_{j−1}(Q_{j} : C_{j}), T_{j−1}(Q_{j} : T_{j}) | 2 ≤ j ≤ m\} \end{matrix}

Since class name B_{i} is removed from S, all the SCs containing B_{i} (such as \overline{X}_{i}(Id : B_{i}), B_{i}(P_{i} : B_{i+1})) are removed from Σ_{SC} accordingly. Similarly, the SC T_{m}(R : Z) is also removed from Σ_{SC}, since R and Z are removed from S.

A_{i} X_{i}\{P_{i+1}\}  \overline{X}_{i}\{P_{i+1}\} ⊥

Figure 21: A modified truth-setting component.

The modified fixed part of Σ_{SC} is illustrated in Figure 22. The varying part of Σ_{SC} remains unchanged. It is easy to verify that the resulting database schema satisfies the lower semilattice condition.

Note that pd ∉ PathDescs_{MSC}(C). In fact, the interpretation G(V, A) for S given in Figure 23 satisfies MSC and Σ ∪ S_{FUNC} but does not have a path from the vertex u described by pd, where C ∈ Cl(u). We must prove that Σ |̸=_{MSC} C(pd : C′) if and only if E is not a tautology.

\underline{Only if part.} Assume that Σ |̸=_{MSC} C(pd : C′). By Theorem 5, there is a pd-List

v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} ⟶^{Q_{1}} u_{1} ⟶^{Q_{2}} ⋯ ⟶^{Q_{m}} u_{m}

satisfying MSC and PDLs 1 to 3. It is easy to see that Claims 2 and 3 given in the proof of Lemma 11 still hold in this case. As for Claim 1, since the pd-List satisfies PDL 1, it holds that Cl(v_{i}) ∩ Dom(P_{i+1}) ≠ ∅ for 1 ≤ i ≤ n − 1 and that Cl(v_{n}) ∩ Dom(Q_{1}) ≠ ∅. Since Dom(P_{i+1}) = \{ X_{i}, \overline{X}_{i} \} and Dom(Q_{1}) = \{ X_{n}, \overline{X}_{n} \} by definition, Cl(v_{i}) must contain either X_{i} or \overline{X}_{i} for 1 ≤ i ≤ n. That is, Claim 1 still holds. Hence it can be shown that E is not a tautology, along the same line as in the only if part proof of Lemma 11.

\underline{If part.} Assume that E is not a tautology. There is a truth assignment τ : {x_{1}, x_{2}, ⋯, x_{n}} → {T, F } that makes E false. We can define the same pd-List

v_{0} ⟶^{P_{1}} v_{1} ⟶^{P_{2}} ⋯ ⟶^{P_{n}} v_{n} ⟶^{Q_{1}} u_{1} ⟶^{Q_{2}} ⋯ ⟶^{Q_{m}} u_{m}

as in the if part proof of Lemma 11 except 2.1 and 2.2. The definitions of 2.1 and 2.2 are changed as follows:

2.1. If τ(x_{i}) = T, then Cl(v_{i}) = {A_{i}, X_{i}} and Msc(v_{i}) = X_{i}, where 1 ≤ i ≤ n.

C\{P_{1}\}  A_{1} X_{1}\{P_{2}\} \overline{X}_{1}\{P_{2}\}  A_{2} X_{2}\{P_{3}\} \overline{X}_{3}\{P_{2}\}  A_{n} X_{n}\{Q_{1}\} \overline{X}_{n}\{Q_{1}\} P_{1}  P_{2}  P_{3}  P_{n} C_{1}\{Q_{2}\} T_{1} C_{2}\{Q_{3}\} T_{2} C_{m} T_{m}  Q_{1}  Q_{1} Q_{2} Q_{2} Q_{3} Q_{3} Q_{m} Q_{m}  · · · · · ·

Figure 22: The modified fixed part of Σ_{SC}.

[figure: {C}; {A_{1}}; u; P_{1}]

Figure 23: An interpretation G(V, A) for S.

2.2. If τ(x_{i}) = F, then Cl(v_{i}) = \{A_{i}, \overline{X}_{i}\} and Msc(v_{i}) = \overline{X}_{i}.

It can be shown that Σ |̸=_{MSC} C(pd : C′), along the same line as in the if part proof of Lemma 11. Consequently, Theorem 10 holds. □

5. Conclusion

We have considered a more general form of specialization constraint for data models supporting complex objects and object identity. The generalization is achieved by allowing range restrictions to be associated with descriptions of property value paths, instead of with individual properties. By admitting a path description, called Id, for paths of zero length (i.e. consisting of a single object), specialization constraints can also be used to declare subclass relationships. In our introductory comments, we demonstrated how specialization constraints can enable a form of molecular abstraction, and indicated how this can be useful not only in modeling, but also in query formulation and physical database design.

In this paper, we have considered the various membership problems for specialization constraints, including the problems of identifying path descriptions corresponding to single or set-valued functions which are total with respect to a given class. We considered these problems for two models. The first imposed no constraints on class membership for objects beyond those implied by subclassing constraints; the second imposed a most specialized class (MSC) condition on class membership for objects, which effectively required each object to have originally been created with respect to at most one class. Table 2 summarizes the various complexity results derived in the paper. For each case in which Table 2 indicates that a membership problem can be solved in polynomial time, we have exhibited a polynomial time procedure. Also, sound and complete axiomatizations are given for two cases: arbitrary specialization constraints for the first model; and well-formed specialization constraints for the second model, when problem schema satisfy an additional lower-semilattice condition.

A complete axiomatization for arbitrary schema, assuming the MSC condition, remains an open problem at this time. At the least, this requires a more general form of specialization constraint in which union extended generalizations (UXG), as defined in [3], may be used in place of class names. An example of a UXG for the ALGEBRA illustrated in Figure 2 is sel+proj, which represents the union of the (extensions of) classes sel and proj. Note that UXG’s may also be used to express so-called cover constraints, such as unExp(Id:sel+proj), which asserts that any unary expression must be at least one of either a selection or projection. However, note that reasoning about constraints of the form UXG_{1}(Id:UXG_{2}) can be expensive, even not assuming MSC. The membership procedure outlined in [3] has O(n^{4}) time complexity, where n is the description length of the constraints.

References

[1] S. Abiteboul and S. Grumbach. COL: a logic-based langauge for complex objects. In Proc. 1st International Conference on Extending Database Technology (EDBT), pages 271–293, 1988.

[2] S. Abiteboul and P. C. Kanellakis. Object identity as a query language primitive. In Proc. ACM SIGMOD International Conference on Management of Data, pages 159–173, June 1989.

[3] H. Arisawa and T. Miura. On the properties of extended inclusion dependencies. In Proc. 12th International Conference on Very Large Data Bases (VLDB), pages 449–456, August 1986.

[4] D. S. Batory and Won Kim. Modeling concepts for vlsi cad objects. ACM Transactions on Programming Languages and Systems, 10(1):322– 346, January 1989.

[5] C. Beeri. Formal models for object-oriented databases. In Proc. 1st International Conference on Deductive and Object-Oriented Databases, pages 370–395, December 1989.

[6] C. Beeri. A formal approach to object-oriented databases. Data and Knowledge Engineering, 5:353–382, 1990.

[7] M. A. Casanova, R. Fagin, and C. H. Papadimitriou. Inclusion dependencies and their interaction with functional dependencies. Journal of Computer and System Sciences, 28, March 1984.

[8] N. Coburn and G. E. Weddell. Path constraints for graph-based data models: Towards a unified theory of typing constraints, equations and functional dependencies. In Proc. 2nd International Conference on Deductive and Object-Oriented Databases, pages 312–331, December 1991.

[9] Computer Corporation of America. ADAPLEX: Rational and reference manual, cca-83-08 edition, May 1983.

[10] U. Dayal. Queries and views in an object-oriented data model. In Proc. 2nd International Workshop on Database Programming Languages, pages 80–102, June 1989.

[11] G. Di Battista and M. Lenzerini. A deductive method for entityrelationship modeling. In Proc. 15th International Conference on Very Large Data Bases (VLDB), pages 13–21, August 1989.

[12] P. C. Kanellakis, S. S. Cosmadakis, and M. Y. Vardi. Unary inclusion dependencies have polynomial time inference problems. In Proc. 15th ACM Symposium on Theory of Computing, pages 264–277, 1983.

[13] C. Lécluse, P. Richard, and F. Velez. o_{2}: an object-oriented data model. In Proc. ACM SIGMOD International Conference on Management of Data, pages 424–433, June 1988.

[14] J. Mylopoulos, P. A. Bernstein, and H. K. T. Wong. A language facility for designing database-intensive applications. ACM Transactions on Database Systems, 5(2):185–207, June 1980.

[15] D. W. Shipman. The functional data model and the data language daplex. ACM Transactions on Database Systems, 6(1):140–173, March 1981.

[16] G. E. Weddell. Reasoning about functional dependencies generalized for semantic data models. Research Report CS-89-14, Department of Computer Science, University of Waterloo, April 1989.

[17] G. E. Weddell. A theory of functional dependencies for object-oriented data models. In Proc. 1st International Conference on Deductive and Object-Oriented Databases, pages 150–169, December 1989.

[18] G. E. Weddell. Reasoning about functional dependencies generalized for semantic data models. To appear, ACM Transactions on Database Systems, 1992.

[19] G. E. Weddell and N. Coburn. A theory of specialization constraints for complex objects. In Proc. 3rd International Conference on Database Theory, pages 229–244, December 1990.