Tractable Concept Languages

1 Introduction

Concept languages provide a means for express­ ing knowledge about hierarchies of concepts, i.e. classes of objects with common properties. They have been investigated following the ideas ml­ tially embedded in many frame-based and semantic­ network-based languages, especially the KL-ONE lan­ guage [Brachman and Schmolze, 1985) . In contrast to earlier formalisms, concept languages are given a Tarski style declarative semantics that allows them to be conceived as sublanguages of predicate logic [Brachman and Levesque, 1984).

The basic reasoning tasks on concepts are unsatisfia­ bility and subsumption checking. A concept is unsatis­ fiable if it always denotes an empty set . A concept C is subsumed by a concept D if C always denotes a subset of D .

Since the performance of any application developed using concept languages will heavily rely on the above reasoning tasks, it is important both to characterize their computational complexity and to devise algorithms as much efficient as possible.

Recent results allow us to draw a fairly complete pic­ ture

This work was partly funded by the ESPRIT BRA 3012 (Compulog), the Italian CNR under Progetto Finalizzato Sis­ temi Informatici e Calcolo Parallelo, contract 90.00681.PF69, and the German BMFT under grant ITW 8903 0.

Werner Nutt

Deutsches Forschungszentrum fiir K iinstliche Intelligenz Postfach 2080, D-6750 Kaiserslautern Germany

of the complexity of a wide class of concept languages [Schmidt-SchauB and Smolka, 1988,Donini et al., 1990). Such results have been obtained by exploiting a general technique for satisfiability checking in concept languages. The technique relies on a form of tableaux calculus, and has been proved extremely useful for studying both the correctness and the complexity of the algorithms.

The outcomes of this body of research go far beyond a mere complexity analysis. In particular, we think that they shed light on three basic aspects related to the use of concept languages in knowledge representation.

First of all, since the complexity of both satisfiability and subsumption depends upon the constructs allowed in the language, we have now an appropriate framework for the study of the trade-off between the expressive power of the languages and their inherent complexity, which was the initial motivation of the seminal work by Brachman and Levesque (see [Levesque and Brachman, 1987]) .

Secondly, the design of concept languages and the associated reasoning procedures can now be realized through the application of the above mentioned tech­ nique, which provides an algorithmic framework that is parametric with respect to the language constructs.

Thirdly, the study of the computational behaviour of concept languages has led to a clear understanding of the properties of the language constructs and their in­ teraction. The knowledge about the structure of concept languages can thus be used in the design of intelligent reasoning procedures, that-by looking at the form of concepts-can reason about the deductive service, for example estimating the difficulty of performing the re­ quired deduction, attempting to provide quick answers to subproblems, or trying possible simplification of the problem.

The work reported in this paper is concerned with the first of the above three points . Our goal was the design of languages including the most powerful set of constructs, while retaining the tractability of subsump­ tion, in particular extending the basic polynomial lan­ guage :F .c- [Brachman and Levesque, 1984) . :F c- in­ cludes conjunction of concepts (written C n D), univer­ sal role quantification (V R.C), and unqualified existen­ tial role quantification (3R) . Various extensions of :F C­ with a polynomial subsumption problem have already been considered:

• F c- +role concatenation (also called role chaining) (Brachman and Levesque, 1984) ;
• ;:c- +number restrictions [Nebel, 1988);
• ;:c- +role conjunction (Nebel, 1988);
• :F c- + negation of primitive concepts [Schmidt-Schauf3 and Smolka, 1988).

The result of our work is the definition of two new extensions of :F c-, called P £ 1 and P £ 2 · We show that subsumption in both languages can be solved in poly­ nomial time. Moreover, they are maximally expressive, in the sense that no construct can be added to them without losing tractability.

In particular, P £ 1 extends :F c- with number restric­ tions, negation of primitive concepts, and inverse roles, and is therefore maximally expressive relative to the costructs available for concepts. On the other hand, P £ 2 extends :F c- with role conjunction, role concatenation, and inverse roles, and is therefore maximally expressive relative to the costructs available for roles. Notice that the construct for inverse roles has not been considered up to now in tractable languages.

The paper is organized as follows. In Section 2 we summarize the main notions used in the formalization of concept languages. In Section 3 we describe the tech­ nique used for subsumption checking. In Sections 4 and 5 we present the languages P £1 and P £2, together with the corresponding subsumption algorithms. Finally, con­ clusions are drawn in Section 6. For the sake of brevity, the proofs of the theorems are omitted; they are fully reported in [Donini et al., 1991b].

2 Basic Notions on Concept Languages

In this section we provide the essential notions about the concept languages considered in the paper. For a general presentation, see [Nebel and Smolka, 1990].

We start by considering the language F c-, where con­ cepts (denoted by the letters C and D) are built out of primitive concepts (denoted by the letter A) and prim­ itive roles (denoted here by the letter R) according to the syntax rule

An interpretation I = (AI, .I) consists of a set AI (the domain of I) and a function .I (the interpretation function of I) that maps every concept to a subset of AI and every role to a subset of AI x AI such that the following equations are satisfied:

An interpretation I is a model for a concept C if CI is nonempty; C is subsumed by D if CI ~ DI for every interpretation I. A concept is satisfiable if it has a model and unsatisfiable otherwise. Notice that since F c- does not include any form of negation, every :F c--concept is satisfiable.

Other constructs have been considered in the litera­ ture to define more general languages. They are:

• the empty concept and the universal concept, de­ fined by ..li = 0 and TI =AI , respectively;
• disjunction of concepts: ( C U D)I = CI U DI ;
• negation of concepts (also called complement): ( ·Cl = A I \ CI; sometimes negation can only be applied to primitive concepts (in this case we use the notation -.A);
• qualified existential role quantification: (3R.C)I = {a E AI l3(a,b) E RI.b E CI};
• number restrictions: (~ n R)I = {a E AI I l{b E AI I (a, b) E RI}I ~ n}, and(~ nR)I ={a E AI ll{b E AI I (a, b) E RI}I ~ n}.
• role conjunction: (Q n R)I = QI n RI;
• inverse of roles: (R-1)I = {(a,b) E AI x AI (b, a) E RI};
• role chaining: (R1 o R2)I = {(a,b) E AI x AI 3c. (a, c) E Rf, (c, b) E Rf} .

In the following, we consider concept languages ob­ tained as combinations of the above constructs. Several such combinations have been taken into account in the design of concept languages. In general, the constructs for role formation have been introduced only in the most sophisticated and powerful languages. In particular, the construct for the description of inverse roles has been considered very rarely, and never in tractable languages. This is somewhat surprising, especially if one consider its importance in the description of complex concepts.

For example, let child be a primitive role, and let young be a primitive concept. It is easy to see that the concept "someone that has at least one child and all of whose par­ ents are young" cannot be defined in a language without inverse roles. Indeed, the introduction of a new prim­ itive role parent would not solve the problem, because child and parent would be completely unrelated. On the other hand, the notion of parent is obviously captured by the inverse of the role child . Therefore, in a language with inverse roles, the above concept can be defined as: 3child n 'v'child- 1 .young.

One of the goals of this paper is to study the impact of inverse roles in the tractability of concept languages. In fact, we show in Sections 4 and 5 that the construct for inverse roles can be added to F c- without increasing the complexity of subsumption.

3 Checking Subsumption Using Constraint Systems

In this section we present the basic features of a technique for checking concept satisfiability. The technique is a refinement of the one used in [Schmidt-Schauf3 and Smolka, 1988], and is fully de­ scribed in [Donini et al., 1990] .

We assume that there exists an alphabet of variable symbols, which will be denoted by the letters x, y, and z. The calculus operates on constraints consisting of variables, concepts , and roles. A constraint is a syntactic object of one of the forms x: C, xRy where Cis a concept and R is a role.

Let I be an interpretation. AnI-assignment is a func­ tion a that maps every variable to an element of AI. We say that a satisfies the constraint x: C if a(x) E cz, and a satisfies xRy if (a(x),a(y)) E Rz . A constraint c is satisfiable if there is an interpretation I and an I­ assignment a such that a satisfies c. A constraint sys­ tem S is a finite, nonempty set of constraints. An I­ assignment a satisfies S if a satisfies every constraint in S. S is satisfiable if there is an interpretation I and an I-assignment a such that a satisfies S. Using the results reported in [Schmidt-SchauB and Smolka, 1988], it is easy to see that a concept C is satisfiable if and only if the constraint system { x : C} is satisfiable.

In order to check whether a concept Cis satisfiable we start with the constraint system S = { x: C}, and in sub­ sequent steps, we add constraints according to a set of propagation rules, until the resulting system is complete, i.e. none of the propagation rules is applicable. At that point, either the complete system S' contains a contra­ diction (called clash), or an interpretation satisfying C can be obtained from S'. Each propagation rule deals with one of the constructs allowed in the language, and the computational complexity of the method crucially depends on their form. It is interesting to observe that, from the logical viewpoint, the method is essentially a tableaux calculus modified with suitable control mecha­ msms.

In order to use the above technique for subsumption, we can rephrase subsumption in terms of unsatisfiability, exploiting the fact that Cis subsumed by D if and only if Cn·D is unsatisfiable. The problem with this approach is that, in general, C n ·D may include constructs which are not present in the language in which C and D are expressed. We show in the following how to deal with this problem for the language F .C- .

We first define a useful property of a class of concept languages, which includes F .c- . A concept is said to be conjunction-free if it contains no conjunction of con­ cepts (i.e. it does not contain the symbol n applied to concepts) . It is easy to see that in a language including neither disjunction nor qualified existential quantifica­ tion, a concept D can be rewritten into an equivalent concept of the form D1 n .. . n Dn, where each D; is conjunction-free, and is called a conjunction-free compo­ nent of D. This can be done by means of the following rewriting rule:

Theorem 3.1 For every pair of concepts C ,D of a language including neither union nor qualified existen­ tial quantification, C is subsumed by D iff for every conjunction-free component D; of D, C n ·D; is u.n­ satisfiable.

Notice that, although the concept ·D; may contain the negation of a non-primitive concept, it can be rewrit­ ten in linear time into an equivalent simple concept (i .e. a concept where negation occurs only in front of primitive concepts) by using suitable rewriting rules.

When F .c- is the language used to express C and D, the simple concept resulting from the rewriting of C n ·D; does not belong to the original language, not only because primitive concepts are negated, but for new constructs introduced through the rewriting rules. In particular, it is easy to see that C n ·D; is a concept of A.C£, an extension of F .C- with qual­ ified existential quantification and negation of primi­ tive concepts. It follows from the results reported in [Schmidt-SchauB and Smolka, 1988] that the propaga­ tion rules for satisfiability checking in A.C£ are:

if x: 3R.C is in S, there is no z such that both xRz and z: Care in S, and y is a

if x:VR.C is inS, xRy is inS, and y:C

Notice that the complete constraint system S' ob­ tained from S = { x: C} by applying the above rules, may have a number of constraints that is exponential in the size of C, in particular because of the number of variables generated by the -3-rule. It has recently been shown that this is due to the interaction of existential and universal quantification, which makes the unsatis­ fiability problem (and therefore subsumption) in A.C£ NP-complete [Donini et al., 1990].

This problem does not arise when computing sub­ sumption in :F .c-. Indeed, if we look at the form of the concept obtained by negating the candidate subsumer and rewriting it into a simple concept, we realize that the body of a qualified existential quantification may contain only a universal quantification of the form V R .. .L. This implies that the inherent complexity given by the inter­ action of existential and universal quantification in A.C£ is not present in the extension of :F .c- used to compute subsumption.

This allows us to modify the -3-rule in such a way that only one variable y is generated for all the con­ straints of the forms x: 3R.C, x: 3R. The correctness of this method stems from the fact that, even if different variables are generated for each of the above constraints, they all share the same properties of y. Therefore, in or­ der to check whether a contradiction arises in the system, it is sufficient to consider only the variable y.

The above modification directly leads to a polynomial time algorithm for su bumption in :F .c-. In the follow­ ing sections, similar techniques are used to show the tractability of two extensions of :F .c-.

4 The Language P £ 1

The language considered in this section, called P £ 1, is an extension of ;:.c- with negation of primitive concepts, number restrictions and inverse roles. Its syntax is spec­ ified by the following rules:

where R denotes a role, and P a primitive role 1 .

In order to deal with subsumption in 1'£1 , we reduce this problem to the unsatisfiability problem in a suitable extension of 1' cl.

Notice that, since 1' £1 includes neither disjunction nor qualified existential quantification C is subsumed by D iff for every conjunction-free component D; of D, Cn...,D; is unsatisfiable. Moreover, as pointed out in Section 3, -,D; can be rewritten into an equivalent simple concept. The resulting concept may not belong to the language 1'£1, because -,'1/R.C is rewritten as 3R · ...,C. We call 1' £1 + the language constituted by concepts of one of the form: C, D, CnD, where Cis a concept of 1' £1 , and D is a simple concept resulting from rewriting a conjunction­ free 1' £ 1-concept. In the rest of the section, we always refer to concepts of 1' £ 1 +, unless otherwise stated. As a notation, we say that xRy holds in a 1' £ 1 +-constraint systemS if:

• R is a primitive role P and xPy E S;
• R is p-l and yPx E S .

The propagation rules for 1' £ 1 +-constraint system are as follows:

4. s

-~ [yjz]S

if x: (~ 1 R) is in S, xRy and xRz hold inS withy "I z, and [yjz]S is obtained from S by replacing y with z

1. s -~ {xRy} US

6. s if x: (~ n R) is in S, with n > 0, y is a new variable, and there is no z such that x Rz holds in S

-3 {xRy, y: C} US

if x: 3R.C is in S, y is a new variable and there is no z such that both x Rz holds in S and z: C is in S

Notice that the construct (~ n R) is treated like the unqualified existential 3R, and, as discussed in Section 3 for :F c-' only one variable is generated for all the constraints of the forms x: (~ n R) , x: 3R.C. We show in the sequel that this simplification, which is crucial for the tractability of the method, does not affect its correctness. Notice also that the construct (~ n R) is taken into account only if n = 1. This is because using the above rules, no more than 2 variables may be linked to the same variable through a given role.

1 Note that P Ct allows for the representation of unqual­ ified existential role quantification: indeed, 3R can be ex­ pressed as (~ 1 R) .

In a 1' £ 1 +-constraint system a clash is a set of constraints of one of the following forms:

1. {x: ..L};
2. {x:A,x:-,A};
3. {x:(:2: nR),x:(~ mR)}, with n > m;
4. {x:(~ OP),xPy} ;
5. {x:(~ oP- 1 ),yPx}.

The next theorem states that the above propagation rules preserve satisfiability.

Theorem 4.1 LetS be a constraint system. If S' is ob­ tained from S by the application of the above propagation rules, then S is satisfiable if and only if S' is satisfiable.

We say that S' is a completion of {x: C}, if S' is com­ plete, and is obtained from { x: C} by giving priority to the application of the ->3-rule. It is easy to see that, up to variable renaming, only one completion can be derived from {x: C}.

It is important to notice that, differently from the case of ACE-constraint systems, there is not a direct corre­ spondence between a clash-free completion of { x: C} and an assignment satisfying it. This is due to the -~-rule dealing with concepts of the form (:2: n R), which are treated as 3R, independently of the value of n. How­ ever, the crucial point is that it is always possible to obtain from a clash-free completion S' an interpretation I and anI-assignment a that satisfies S'. In particular, I and a are built in such a way that to each variable in S' there corresponds a suitable number of objects in the domain of I, all with the same properties, in order for a to satisfy all constraints of the form x: (:2: n R).

Theorem 4.2 Let C be a 1' £ 1 +-concept, and let S' be the completion of the constraint system { x: C}. Then S' is satisfiable if and only if it contains no clash.

The entire method for testing subsumption in 1' £ 1and satisfiability as a special case-can be summed up as follows. In order to check if C is subsumed by D, we compute the conjunction-free components D1 , ... ,Dn of D, and for each i we rewrite ...,D; into the simple concept D/. Finally, we check if for each i, the completion of C n D;' contains a clash.

The tractability of subsumption in 1' £ 1 can be proved by showing that computing the completion of a constraint system {x: C n ...,D;} requires polyno­ mial time. The proof is based on the following ob­ servations. First of all, giving priority to the ->3rule leads to a constraint system of the form S = {x :C,xR1Yl,YlR2Y2, ····Yh-1RhYh ,Yh:F}, where F is not of the form 3R.E. Second, the number of variables generated in the completion of a constraint system of the form S is bounded by (g + 1) · (h + 1), where g is the number of subconcepts (i.e. substrings that are con­ cepts) of C of the form (:2: n R). Finally, the cost of the entire method is polynomially bounded by the number of variables in the computed completion.

Theorem 4.3 The subsumption problem in 1' £1 can be solved in polynomial time.

It is interesting to observe that none of the con­ structs presented in Section 2 can be added to P .C1 without sacrificing tractability. In particular, it follows from the results reported in (Nebel , 1988) that the addition of role conjunction leads to co­ NP-hardness of subsumption. Also, adding negation of non-primitive concepts leads to PSPACE-hardness, whereas adding union makes subsumption co-NP-hard [Schmidt-SchauB and Smolka, 1988]. Moreover, the ad­ dition of qualified existential quantification results in the language A.C£, and therefore leads to NP-hardness of subsumption [Donini et al., 1990).

We now show that the same problems arise when P .C1 is extended with role chaining. In particular, any con­ cept D of A.C£ can be translated into a concept D' of P .C1 + role chaining such that D is satisfiable if and only if D' is satisfiable. D' is obtained from D by sub­ stituting each subconcept of D having the form 3P.C with (~ 1 (Po Q)) n '1:/(P o Q o Q- 1 ).C, where Q is a new primitive role used only in the substitution of that subconcept. Since the above translation is clearly polynomial, we can conclude that unsatisfiability-and therefore subsumption-in P .C1 with role chaining is NP­ hard.

5 The language P £ 2

The language considered in this section, called P .C2 , is an extension of :F .c- with role conjunction, role chaining, and inverse roles . Its syntax is specified by the following rules:

where P is a primitive role, and R, R1 and R2 are arbi­ trary roles. Notice that, as for :F .c-, every P .C2-concept is satisfiable.

It is possible to verify that every role of P .C2 can be written in a so-called normal form, where the constructor for the inverse role is applied only to primitive roles. The following rewriting rules can be used to transform any role into an equivalent role having such a form. In the sequel , we only refer to roles in normal form.

As done for P .C1 , we reduce the subsumption prob­ lem in P .C2 to the unsatisfiability problem in a suit­ able extension of the language. Moreover, since P .C2 in­ cludes neither disjunction nor qualified existential quan­ tification, it is sufficient to consider the unsatisfiability problem for concepts of the form C n -,D, where D is conjunction-free.

We call P .C2 + the language constituted by concepts of one of the forms: C, -,D, C n -,D, where Cis a concept of P .C2, and D is a conjunction-free concept of P .C2 . In the rest of this section we always refer to concepts of P .C2 +, unless otherwise stated.

In order to present the propagation rules for P .C2 +­ constraint systems, we need the following definition. We say that xRy holds in a P .C2 +-constraint system S if:

• R is a primitive role P and xPy E S;
• R is p- 1 and yPx E S;
• R is R1 n R2, and both xR1y and xR2y hold in S;
• R is R1 o R2 and there is a z such that both xR1z and zR2y hold in S.

The propagation rules for P .C2 +-constraint systems are the -+n-rule, -+v-rule, and the -+_ 1-rule already de­ fined for P .C1 , plus the following ones:

if x: -,'1:/R.C is in S, y is a new variable and there is no z such that z: ..,c is in

• s

if x(R1 nR2)y is inS, and either xR1y or

1. S -+np {xR1y , xR2y} US xR2y is not in S

if x(R1 o R2)Y is inS, z is a new variable and there is no w such that both xR1 w and wR2y are in S

Notice that variables are only generated by the -+..,v­ rule. In particular only one variable is generated for each constraint of the form x: -,'1:/R.C. On the other hand, no rule is needed for constraints of the form x : 3R, since we can avoid to produce new variables for them. This is crucial for keeping the size of the system polynomial. Indeed, even if one generates only one variable for each constraint of the form x: 3R (as done in :F .c-), the pres­ ence of role conjunction may lead to an exponential num­ ber of variables in the completion of the system.

It is easy to see that, up to variable renaming, only one completion can be derived from a P .C2 +-constraint system. The following theorem states that the above rules preserve satisfiabiFty.

Theorem 5.1 Let S be a constraint system. Then, if S' is obtained from S by application of the above rules, then S is satisfiable if and only if S' is satisfiable.

In P .C2 +-constraint systems, a clash is defined as a set of constraints of one of the following forms:

1. {x :A,x:..,A};
2. {x:3R1,x:-,3R2}, where the completion of the new constraint system {xR1y,x:'I:/R2.B} (B is a new symbol denoting a primitive concept) contains a constraint z: B, for some variable z.

Notice that checking whether a completion of a con­ straint system S has a clash may require to compute the completion of other systems, each one constituted by two constraints of the form {xR1y, x :'I:/R2.B}. It is easy to see that if such a completion contains a con­ straint z: B, then the existence of an object y related to x through the role R1 implies that x is also related to an object z through the role R2, and the pair of constraints { x: 3R1, x: ...,3R2} is unsatisfiable.

Theorem 5.2 Let S be the completion of the constraint system { x: C n -,D}. Then S is satisfiable if and only if it contains no clash.

The tractability of subsumption in P .C2 can be proved by showing that computing the completion S' of a con­ straint system { x: C n -.D;} requires polynomial time, and moreover checking whether S' has a clash is also a polynomial task. With regard to the first point, the basic observation is that for every subconcept C' of C n -.D at most one constraint of the form z: C' can be con­ tained inS'. Therefore, the number of constraints in S' is bounded by the size of C n -.D. With regard to the second point, notice that the worst case requires consid­ ering every pair of constraints of S', and checking if they constitute a clash of the form {x: 3Rl , x: -.3R2}· Since the cost of such a check is polynomially bounded by the size of R1 and R2 , we can state the following theorem.

Theorem 5.3 The subsumption problem in P .C2 can be solved in polynomial time.

As for P .C1 , it is possible to show that none of the constructs presented in Section 2 can be added to P .C2 without sacrificing tractability. In particular, the addi­ tion of number restrictions leads to co-NP-hardness of subsumption [Nebel, 1988] . The addition of the nega­ tion of primitive concepts results in a language that is a superset of a language called ACR, shown in­ tractable in [Donini et al., 1991a], whereas the addition of qualified existential quantification results in a super­ set of A.C£. Finally, it is possible to show that adding union to P .C2 makes subsumption intractable. In fact , one can prove that even the simpler problem of check­ ing whether C is subsumed by D 1 U · · · U Dn , where C, D1, ... , Dn are :F .c--concepts is already intractable (see [Lenzerini and Schaerf, 1991]).

6 Conclusion

We have presented two concept laguages, called P .C1 and P .C2 , that include as many as possible of the con­ structs usually considered in terminological reasoning, while avoiding combinations that are proved harmful for tractability.

It is interesting to observe that we can extend both P .C1 and P .C2 with functional roles, functional role value map and disjunction of primitive concepts without en­ dangering the tractability of subsumption.

The algorithms for checking subsumption in P .C1 and P .C2 have been designed by exploiting a gen­ eral technique for satisfiability checking in concept lan­ guages. Such a technique is the basis of recent com­ plexity results about a wide class of concept languages [Schmidt-SchauB and Smolka, 1988,Donini et al., 1991a] . These results allow us to derive lower bounds for the complexity of almost all the possible combinations of the constructs presented in Section 2. There is in fact one single exception, because it is still unknown if subsump­ tion is tractable in the language obtained from :F .c- by adding number restrictions and role chaining. It turns out that we can state an interesting property of P .C1 and P .C2: Let .C be a language extending :F .c- with any combination of the constructs presented in Section 2, ex­ cept for the combination of number restrictions and role chaining; if the subsumption problem in .C is tractable, then .C is a sublanguage of either P .C1 or P .C2 .

Therefore, on the assumption that languages are char­ acterized by the set of constructs they provide , the two languages presented in this paper provide a solution to the problem of singling out an optimal trade-off between expressive power and computational complexity.