Augmenting Concept Languages by Transitive Closure of Roles: An Alternative to Terminological Cycles

1 Introduction

In knowledge representation (KR) languages based on KL­ ONE (Brachman&Schmolze (1985)), one starts with atomic concepts and roles, and can use the language formalism to defme new concepts and roles. Concepts can be considered as unary predicates which are interpreted as sets of individuals whereas roles are binary predicates which are interpreted as binary relations between individuals. The languages (e.g., 'f£ and ']'£-of Levesque&Brachman (1987), T.f and ?(P.J of Nebel (1990)) differ in what kind of constructs are allowed for the definition of concepts and roles. Their com­ mon feature-besides the use of concepts and roles-is that the meaning of the constructs is defined with the help of a model-theoretic semantics. Most of these languages do not go beyond the scope of frrst-order predicate logic, and they usually have very restricted formalisms for defining roles.

· This work was supported by the German "Bundesministerium filr Forschung und Technologie" under Grant ITW 8903 0.

However, for many applications it would be very useful to have means for expressing things like transitive closure of roles. For example, if we have a role child (resp. is­ direct-part-of) we might want to·use its transitive closure offspring (resp. is-part-of) in order to define concepts like "man who has only male offsprings" (resp. "car which has onl¥ functioning parts"). Obviously, we cannot just introduce a new role offspring without enforcing the appropriate relationship between offspring and child. Since the transitive closure of binary relations cannot be expressed in frrst-order predicate logic (see Abo& Ullman (1979)), the concept languages mentioned above cannot be used for that purpose.

There are two possibilities to overcome this problem. On the one hand, one may introduce a new role-forming operator trans, and define its semantics such that, for any role R, trans(R) is interpreted as the transitive closure of R. This operator is e.g. contained in the terminological representation language LOOM (MacGregor&Bates (1987)). However, LOOM does not have a complete algorithm to determine subsumption relationships between concepts.

On the other hand, cyclic concept definitions together with an appropriate fixed-point semantics can be used to express value-restrictions with respect to the transitive closure of roles (see Baader (1990,1990a)). However, cyclic definitions are prohibited in most terminological knowledge representation languages because, from a theoretical point of view, their semantics is not clear and, from a practical point of view, existing inference algorithms cannot handle cycles.

The frrst thorough investigation of cycles in terminologi­ cal knowledge representation languages can be found in Nebel (1990,1990a). Nebel has introduced three different kinds of semantics-namely, least fixed-point semantics (lfp-semantics), greatest fixed-point semantics (gfp­ semantics), and what he called descriptive semantics-for cyclic definitions in his language 9{_rz'if. Baader (1990,1990a) considers terminological cycles in a small KL­ ONE-based language which allows only concept conjunctions and value-restrictions. For this language, which will be called 'fLo in the following, the effect of the three ~hove mentioned types of semantics can be completely descnbed with the help of finite automata. As a conse­ quence, subsumption determination for each type of semantics can be reduced to a well-known decision problem for finite automata. For the language 'f £ 0 , the gfp­ semantics comes off best. The characterization of this semantics is easy and has an obvious intuitive interpreta­ tion. It also shows that gfp-semantics is the appropriate semantics for expressing value-restrictions with respect to the transitive closure of roles.

However, the results described in Baader (1990a) have two major drawbacks which we intend to overcome in the present paper. First, the language J"Lo is too small to be sufficient for practical purposes. As shown in Baader (1990), the results can be extended to the language 1" L- of Levesque&Brachman (1987), and it seems to be relatively easy to include number-restrictions. However, as soon as we also consider disjunction of concepts and exists-in­ restrictions (see Def. 2.1), the unpleasant features which lfp­ semantics had for J".Lo (see Baader (1990,1990a)) also occur for gfp-semantics in this larger language. If we should like to have general negation of concepts, least or greatest fixed­ points may not even exist, thus rendering fixed-point semantics impossible.

Second, the characterization of gfp-semantics for 1" Lo­ though relatively easy and intuitive-still involves notions from formal language theory such as regular languages and fmite automata. In the present paper we shall show that the concept defining facilities of 1" Lo with cyclic definitions and gfp-semantics can also be obtained in a different way. One may prohibit cycles and instead allow role definitions using union, composition, and transitive closure of roles. The regular languages which occur in the characterization of gfp­ semantics for J".Lo can directly be translated into role defini­ tions in this new language.

This proposes a way of retaining, in an extended lan­ guage, the pleasant features of gfp-semantics for 1" Lo with cyclic definitions without running into the troubles caused by cycles in larger languages. Starting with the language .9lLC of Schmidt-SchauB&Smolka (1988}-which allows negation, conjunction and disjunction of concepts as well as value-restrictions and exists-in-restrictions-we shall disal­ low cyclic concept definitions, but instead shall add the possibility of role definitions involving union, composi­ tion, and transitive closure· of roles. In contrast to other terminological KR-systems which incorporate the transitive closure operator for roles, we shall be able to give a sound and complete algorithm for concept subsumption.

Because of the space limitations it is not possible to include a complete formal description of this algorithm into the present paper. Instead we shall frrst recall by an example how the subsumption algorithm for ~LC works. It will then be explained how the ideas underlying this algorithm can be generalized to the extended language. Two more examples will be used to demonstrate what kind of new problems may occur. A complete description of the algorithm, together with the proof of its correctness can be found in Baader (1990b).

2 The Languages .!JLLC and !fLo

The language which we shall use as a starting point for the extension described in Section 4 is called "attributive concept desCription language with unions and comple­ ments", for short )UC (Schmidt-SchauS&Smolka (1988)). The reason for choosing ~was that it is large enough to exhibit most of the problems connected with such an extension. Taking a larger language (e.g., including number restrictions) would only mean more work without bringing new insights.

Definition 2.1. (concept terms and terminologies)

Let c· be a set of concept names and R be a set of role names. The set of concept terms of ~LC is inductively defined. As a starting point of the induction, any element of Cis a concept term (atomic terms). Now let C and D be concept terms already defined, and let R be a role name. Then C n D (conjunction), C u D (disjunction), ...,c (negation), 'v'R:C (value-restriction), and 3R:C (exists-in­ restriction) are concept terms.

Let A be a concept name and let D be a concept term. Then A= Dis a terminological axiom. A terminology (T-box) is a finite set of terminological axioms with the additional restriction that no concept name may appear more than once as a left hand side of a defmition. Cl

The sublanguage 1" .Lo of ~is defmed as follows: the concept defining operators are restricted to concept conjunction and value-restriction.

A T -box T contains two different kinds of concept names. Defined concepts occur on the left hand side of a terminolog­ ical axiom of T. The other concepts are called primitive concepts. Cycles in terminologies are defined as follows. Let A, B be concept names and letT beaT-box. We say that A directly uses B in T iff B appears on the right hand side of the definition of A. Let uses denote the transitive closure of the relation directly uses. Then T contains a terminological cycle iff there exists a concept name A in T such that A uses A

For example, assume that we want to describe all "aliens having only melmacian ancestors on the mother's side", using the primitive roles father, mother, and the primitive concepts Alien, Melmacian. In 1" Lo, this concept (for short Mam) is defined by the cyclic terminology Mam = Alien n 'v' mother:Ma, Ma = Melmacian n 'v' mother:M a n 'v'lather:Ma, which introduces the auxiliary concept Ma for "aliens having only melmacian ancestors".

The next definition gives a model-theoretic semantics for the language introduced in Defmition 2.1.

Definition 2.2. (interpretations and models)

An interpretation I consists of a set dom(l), the domain of the interpretation, and an interpretation function which associates with each concept name A a subset A 1 of dom(l), and with each role name R a binary relation Rl on dom(l), i.e., a subset of dom(I) x dom(l).

The interpretation function-which gives an interpretation for atomic terms---<an be extended to arbitrary terms as follows: Let C, D be concept terms and R be a role name. Assume that Cl and oi are already defmed. Then (C n D) 1 := Cl n oi, (C u D)l := Cl u oi, (-,C)I := dom(l) \ Cl, ('v'R:C)I := {x e dom(D; for ally such that (x,y) e R 1 we have y e Cl), and (3R:C) 1 := {x E dom(l); there exists y such that (x,y) E R 1 and y E ci).

An interpretation I is a model of the T-box Tiff it satisfies AI= oi for all terminological axioms A= DinT. Cl

An important service terminological representation systems provide is computing the subsumption hierarchy.

Let T be a terminology and let A, B be concept names. Then we say that B subsumes A with respect to T (symbolically A s;;T B) iff AI~ Bl for all models I ofT

3 Extensions of ~ Lo

The semantics we have given in Definition 2.2 is not restricted to non-cyclic terminologies. But for cyclic terminologies this kind of semantics, which will be called descriptive semantics in the following, turns out to be unsatisfactory (see Baader (1990a), Example 2.3). For this reason, alternative types of semantics for terminological cycles have been considered, namely greatest fixed-point semantics (gfp-semantics) and least fixed-point semantics (lfp-semantics). Roughly speaking, gfp-semantics (lfp­ semantics) means that, with respect to a given interpretation of the primitive concepts and roles, the defined concepts are interpreted as large (small) as possible in gfp-models (lfp­ models) of the terminology (see Nebel (1990,1990a) or Baader (1990,1990a) for details).

In Baader (1990,1990a) it was shown that a finite automaton ;tT can be associated to each terminology T of '.fLo. The alphabet of ;tT is the set RT of all role names occurring in T, the states of ;tT are the concept names occurring in T, and the transitions of ;tT are defmed by the terminological axioms ofT (see Baader (1990,1990a) for details). This automaton was used to describe the effect of the three above mentioned types of semantics with the help of well-known notions from automata theory. The characterization of gfp-semantics is easy, and it involves only regular languages over the alphabet of role names. More precisely, the automaton ;tT defines a regular languages L(A,B) for each pair of concepts A, B occurring in T. For an interpretation I and a word W = RtRz ... Rn over RT, W1 denotes the composition RtloRzlo ... oRnl of the · binary relations R1 1, R21, .·. , Rn1. For the empty word E, el denotes the identity relation, i.e., ei = ( ( d,d); d e dom{l)}.

Theorem 3.1. LetT be a terminology of '.JLQ, and let ;tT be the corresponding automaton. Let I be a gfp-model ofT, and let A be a concept name occurring in T.

For any d e dom{l) we have d e A 1 iff for all primitive concepts P, all words W e L{A.P). and all individuals e e dom{l), (d,e) E WI implies e E pi, 0

In our example which is about aliens from Melmac, we have L(Mam ,Melmacian) = (mother(fatheru mother)·)

The characterization in Theorem 3.1 means that, if we start with an individual d = ALF and consider first his mother, and then arbitrarily mothers or fathers of the individuals already obtained, then ALF is an alien having only melmacian ancestors on the mother's side if and only if all the individuals reached that way come from Melmac.

Theorem 3.1 motivates the definition of regular value­ restrictions in the following "regular extension" of '.ff.o.

Definition 3.2. (1) Let L be a regular language over the set of role names, and let C be a concept term already defined. Then 'v'L:C is a re$ular value-restriction. Its semantics is defmed as ('v'L:CY := ( d e dom{l); for all words W e L and all individuals e e dom(l), (d,e) e wr implies e e C 1 }.

(2) In the regular extension '.f4e 8 of '.JLQ we allow to use regular value-restrictions and concept conjunction as concept forming operators. 0

Theorem 3.1 implies that, with respect to gfp-semantics, cyclic terminologies of '.! Lo can be expressed by acyclic terminologies of '.!Lre 8 . On the other hand, it can be shown that any acyclic terminology of '.! Lre 8 can be expressed by a possibly cyclic terminology of '.JLQ. Moreover, any cyclic terminology of '.f4e 8 (considered with gfp-semantics) can be transformed into an equivalent acyclic terminology of '.!Lre/. (Baader (1990b)). In our example, we can describe Mam by the following concept term of '.f4e 8 :

Alien n 'v' (mother(fatheru mothert):Melmacian

Proposition 3.3. Possibly cyclic terminologies of '.f LQ considered with gfp-semantics, acyclic terminologies of '.f Lreg· and possibly cyclic terminologies of '.! Lreg considered with gfp-semantics have the same expressive power. 0

In place of cyclic definitions or regular languages in value-restrictions, we shall now allow role terms involving union, composition and transitive closure of roles in the following "transitive extension" of '.fLo. All these role forming operators have already been considered in KL-ONE based systems, though not necessarily together. It will turn out that we get a language having exactly the same expressiveness as '.f.Lre 8 .

Definition 3.4. (1) Let R be a set of role names. The set of role terms is inductively defined as follows. As a starting point of the induction, any role name is a role term (atomic role), and the symbol0 is a role term (empty role). Now assume that R and S are role terms already defined. Then R u S (union), RoS (composition), and trans(R) (transitive closure) are role terms. The semantics of the role forming operators is defined in the obvious way: 0 1 := 0, (R u S)l := Rl u Sl, (RoS)I := RloSI, and (trans(R))I := U~t(R 1 f, i.e., (trans(R)) 1 is the transitive closure ofR 1 . (2) In the transitive extension '.F4ans of '.fLQ we allow to use role terms instead of simply roles in value-restrictions.O

It is now easy to see that there is a direct correspondence between the regular languages in value-restrictions of '.f Lre, and the role terms in value-restrictions of '.! Ltrans· Consequently, acyclic (resp. cyclic) terminologies of '.! 4rans have the same expressive power as acyclic (resp. cyclic) terminologies of '.f.Lre 8 · and thus as possibly cyclic terminologies of '.fLo considered with gfp-semantics.

In '.! 4rans we can use the following term to define the concept Mam of our example:

Alien n 'v' mother:Melmacian n 'v' (motherotrans(fatheru mother)): Melmacian.

4 The Extension of ..9LLC

In the previous section we have seen that the expressiveness of possibly cyclic terminologies of '.! Lo considered with gfp-semantics can also be obtained without involving cyclic definitions; we just have to include the appropriate role forming operators into the language. These role forming operators can now be integrated into the larger language fJlLC without causing any of the troubles we should have with cyclic definitions in fJlLC.

Definition 4.1. (1) In the transitive extension Jt£Cuans of Jt£Cwe allow to use role terms (as defined in part (1) of Definition 3.4) instead of simply roles in value-restrictions and exists-in-restrictions. The semantics of JtLCtrans is defmed as in Definition 2.2 and 3.4.

(2) In the regular extension fJlLCreg of fJlLC we allow to use regular value-restrictions and regular exists-in­ restrictions in place of the usual restrictions of fJlLC. The semantics of the regular value-restrictions is defined as in part (1) of Defmition 3.2. The semantics of the regular exists-in-restrictions will be defined in a way such that -,(3L:C) is equivalent to 'v'L:(-,C). That means that we define (3L:C)f := { d e dom(I); there exists a word W e L and an individual e e dom(l) such that (d,e) e WI and e e c 1 }. Cl

Please note that the regular exists-in-restriction is very similar to what is called "Functional Uncertainty" in computational linguistic (see Kaplan&Maxwell (1988)).

As for '.FLrcg and '.FLtrans· acyclic terminologies of fJlLCtrana and acyclic terminologies of fJlLCrcg have the same expressive power. This shows that we may restrict our attention to one of these two languages. The definition of ~. is more intuitive, and thus J{£Ctran1 may be more appropriate if we want to apply the language to actual representation problems. But UCreg turns out to be more convenient for describing the subsumption algorithm. We can now state the main result of the paper.

Theorem 4.2. There exists a sound and complete algorithm for testing subsumption relationships w.r.t. acyclic terminologies of Jt£Crcg (or equivalently iJlLCuana). Cl

All the existing system which incorporate transitive closure of roles have only sciund but incomplete algorithms, i.e., these algorithms may sometimes fail to detect subsumption relationships.

Since we only allow acyclic terminologies of UCrcg· subsumption with respect to terminologies can be reduced to subsumption of concept terms by expanding concept defmitions (see e.g., Nebel (1990)). For two concept terms C, D we say that C is subsumed by D (symbolically C Iii D) iff Cl ~ oi for all interpretations I. As for Jt£C, the subsumption problem for concept terms can further be reduced tO the satisfiability problem, where a concept term C is called satisfmble iff there exists an interpretation I such that C 1 ~ 0. In fact, for concept terms C, D and an interpretation I, we have Cl ~ oi iff Cl \ oi = 0, i.e., iff (C n -,D)I = 0. This shows that Cis subsumed by D iff C n -,0 is unsatisfiable. Thus it is sufficient to have an algorithm which decides satisfmbility of concept terms.

This algorithm will use the idea of constraint propagation, as proposed by Schmidt-Schau8&Smolka (1988) for JtLC, and successfully used by Hollunder et al. (1990) and Hollunder&Nutt (1990) for various other languages. However, an algorithm for fJlLCreg has to treat regular restrictions of the form 3L:C, 'v'L:C instead of simple restrictions 3R:C, 'v'R:C.

In order to clarify this difference, let us first recall by an example how satisfiability can be checked for concept terms of Jt£C (see Schmidt-Schau8&Smolka (1988), and Hollunder&Nutt (1990) for details).

4.1 The Satisfiability Test for Jt£C

Assume that C is a concept term of fJlLC which has to be checked for satisfiability. In a first step we can push all negations as far as possible into the term using the fact that the terms -,-,0 and D, -,(D n E) and -,D u .E, -,(D u E) and -,D n .E, -,(3R:D) and 'v'R:(-,0), as well as -,('v'R:D) and 3R:(-,D) are equivalent. We end up with a term C' in negation normal form where negation is only applied to concept names.

Example 4.3. Assume that we want to know whether the term 3R:A n 3R:B is subsumed by 3R:{A n B). That means that we have to check whether the term C := 3R:A n 3R:B n -,(3R:(A n B)) is unsatisfiable. The negation normal form of C is the term C' := 3R:A n 3R:B n 'v'R:(-,A u .B).

In a second step, we try to construct a fmite interpretation I such that C' 1 ~ 0. That means that there has to exist an individual in dom(I) which is an element of C'l. Thus the algorithm generates such an individual b and imposes the constraint b e c·l on it. In the example, this means that b has to satisfy the following constraints: be (3R:A)I, be (3R:B)I, and bE ('v'R:(-,A u -,B))I.

From be (3R:A)I we can deduce that there has to exist an individual c such that (b,c) e Rl and c e AI. Analogously, b e (3R:B)I implies the existence of an individual d with (b,d) e Rl and de Bl. We should not assume that c = d since this would possibly impose too many constraints on the individuals newly introduced to satisfy the exists-in-restrictions on b. Thus the algorithm introduces for any exists-in-restriction a new individual as role-successor, and this individual has to satisfy the constraints expressed by the restriction.

Since b also has to satisfy the value-restriction 'v'R:(-,A u -,B), and c, d were introduced as Rtsuccessors ofb, we also get the constraints c e (.Au .B)I, and de (-,Au -,B)I. Now c has to satisfy the constraints c e AI and c e (-,Au -,B)I whereas d has to satisfy the constraints d e Bl and d e (-,Au -,B)I. Thus the algorithm uses value-restrictions in interaction with already defmed role-relationships to impose new constraints on individuals.

Now c e (-,Au -,B)I means that c e (.A)I or c e (.B)I, and we have to choose one of these possibilities. If we assume c e (-,A )I, this clashes with the other constraint c e AI. Thus we have to choose c e (-,B)I. Analogously, we have to choose d e (-,A )I in order to satisfy the constraint d e (-,Au .B)I without creating a contradiction to de Bl. Thus, for disjunctive constraints, the algorithm tries both possibilities in successive attempts. It has to backtrack, if it reaches a contradiction, i.e., if the same individual has to satisfy complementary constraints.

In the example, we have now satisfied all the constraints without getting a contradiction. This shows that C' is satisfiable, and thus 3R:A n 3R:B is not subsumed by

3R:(A n B). We have generated an interpretation I as witness for this fact: dom(l) = {b, c, d); Rl = ((b,c), (b,d)); AI= (c) and Bl ={d). For this interpretation, b e C'l. That means that b e (3R:A n 3R:B)l, but b ~ (3R:(A n B))l.

Termination of the algorithm is ensured by the fact that the newly introduced constraints are always smaller than the constraints which enforced their introduction.

4. 2 The Generalization to JilLCreg

A satisfiability algorithm for JilLCreg has to treat regular restrictions of the form 3L:C and V'L:C instead of simple restrictions 3R:C and V'R:C. In order to satisfy a constraint of the form be (3R:C)I, the algorithm described above introduces a new individual c which has to satisfy bRlc and c e C 1 . This is not so easy if we have to satisfy a regular constraint of the form b e (3L:C)I. All we know is that there has to exist some word W e L and an individual c such that bWic and c e cr. But we do not know which W does the job, and if L is infinite, there are infinitely many canditates. Thus trying them one after another will not do.

Obviously, the concept terms 3L:C and C u 3(L \ (E)):C are equivalent. For that reason we may without loss of generality assume that L does not contain the empty word. Thus the correct word W e L has some role symbol R as its first symbol. That means that there exists a word U such that W = RU. The alphabet of role symbols over which L is built is finite, and thus there are only finitely many possibilities for choosing a symbol R. Once we have chosen R, we still do not know which word U does the job. All we know about U is that it is an element of the set R-lL := (V; RV e L).

Definition 4.4. Let L be a language and let W be a word. The left quotient w-lL of L with respect toW is defmed as w-1L:=(V;WVeL). Q

For a regular language L, the language w-lL is also regular (see Eilenberg (1974), p. 37), and obviously, this is also true for w·1L \(£).For words V, W we have (VW)-1L = w-l(V-lL). For example, let L be the regular language (RS)+. Then R-lL = S(RS)*, s-lL = 0, and (RS)-lL = s-l(R-1L) = (RS)*.

In the satisfiability test, we can now choose between two possibilities: U e R-lL can be the empty word (provided that R e L) or U can be nonempty (provided that R-lL \ ( £) :F. 0). If we assume U = £, then the new individual c has to satisfy bR 1 c and c e cr, and the exists-in-restriction is worked off. If we assume U :f:. £,then b(RU)lc ensures the existence of an individual d such that bRid, dUic, and c e ci. We still do not know the appropriate U, but the existence of such a word U and an individual c with dUic, and c e cr can be expressed by the constraint de (3(R-1L \ (E)):C)I.

Thus we have seen how the treatment of exists-in­ restrictions in the satisfiability algorithm for UC can be generalized to JilLCreg· We shall now turn to value­ restrictions.

Assume that we have a constraint be (V'L:C)l, and-to satisfy an exists-in-constraint on ~we have introduced an individual c such that bRic. Obviously, if R e L, we have to add the constraint c e C 1 ; but this is not sufficient for the following reason. Assume that U is an element of R-lL \

{£),i.e., U is a nonempty word such that RUe L. If, in some step of the algorithm, an individual d is introduced such that cUid holds, then d has to satisfy the constraint d e Cl. This is so because b(RU)ld, RUe L, and b has to satisfy b e (V'L:C) 1 · We can keep track of this possibility by imposing the constraint c e (V'(R-1L \ (E)):C)l on c.

Unlike the situation for UC one can no longer be sure of the termination of the algorithm, unless one imposes an appropriate control structure, and tests for cycles. The problem of nontermination will be demonstrated by the following example.

Example 4.5. We consider the following concept term of JilLCreg: C := A n 3R:A n V'R+:(3R:A).

(1) We introduce an individual ao which has to satisfy the constraints ao E A 1 , ao E (3R:A)l, ao E (VR+:(3R:A))l.

(2) Because of the exists-in-restriction for ao we introduce a new individual a1 such that aoR 1 at. and this individual has to satisfy the constraint a1 e AI.

(3) Now the interaction between aoR 1 a1 and the value­ restriction ao e (V'R+:(3R:A)Y has to be taken into account. Because of R e R+ we obtain the constraint a1 e (3R:A)I. In addition, we have R-1R+ \ (£) = R+ :f:. 0, which yields the constraint a1 e (V'R+:(3R:A))I. To sum up, a1 has to satisfy the constraints a1 e A\ a1 e (3R:A) 1 , and a1 e (V'R+:(3R:A))I, i.e., the same constraints as previously ao. If we continue with the constraints on a1 we get an individual a2 which, in the end, has to satisfy the same constraints as a1. This yields an individual a3, and so on. In other words, the algorithm has run into a cycle.

On the other hand, we could just identify ao with a1. This would yield the following interpretation J: dom(J) := (ao); R 1 := { (ao,ao) ); A 1 := (ao}- It is easy to see that this interpretation satisfies ao E C . Q

The phenomenon that such cycles may occur is not particular for this example. After sufficiently long computation, the algorithm will always reproduce sets of constraints which have already been considered. Basically, this is a consequence of the following fact, which in turn is an easy consequence of the quotient criterion for regular languages (see Eilenberg (1974), Theorem 8.1).

Proposition 4.6. Let K be a finite set of regular languages. Then the set (W-1L \(£);where L e K and W is a word} is also finite. Q

However, it turns out that there are two different types of cycles: "good cycles" and "bad cycles". The cycle of Example 4.5 is a "good cycle"; its occurrence indicated that the concept term under consideration is in fact satisfiable. The following example will demonstrate how "bad cycles" may arise.

Example 4.7. We consider the following concept term of ~g: D :=-,An 3R+:A n V'R+:(-,A).

(1) We introduce an individual ao which has to satisfy ao e (-,Aj, ao E (3R+:A)l, and ao E (V'R+:(-,A))l.

(2) Because of the exists-in-restriction for ao we introduce a new individual a1 such that aoRlat. But now we haveR e R+ as well as R·1R+ \(E) = R+ :~:- 0. Thus we have to choose between two possibilities for the constraint on a1.

1. First, we may consider the constraint a1 e AI (corresponding to the case U =£from above). But aoR 1 a1 together with the value-restriction 3() E (v'R+:(-,A))I yields a1 e (-.A)I, and we have a clash with a1 e AI.

(4) Thus we have to backtrack and choose the constraint a1 e (3R+:A)I (corresponding to the case U-:;:. £from above). As before, aoR 1 a1 together with the value-restriction on ao yields a1 e (-,A)I and a1 e (v'R+:(-,A))I. Thus a1 has to satisfy the same constraints as previously ao. This shows that we have again run into a cycle; but this time the situation is different. In fact, it is easy to see that the concept term D is unsatisfiable whereas the term C of Example 4.5 was satisfiable. Cl

We may now ask what makes the difference between the cycle of Example 4.5 and that of Example 4. 7. In the second example we have postponed satisfying the exists-in­ restriction for ao by introducing the new exists-in-restriction for a1. It is easy to see that we should have to postpone satisfying the restriction forever because trying to actually satisfy it will always result in a clash. In the first example however, we had already satisfied the exists-in-restriction before the cycle occurred.

Building up on these ideas, an algorithm for deciding satisfiability of concept terms of Jii.LC'reg is presented, and proved to be sound, complete, and terminating in Baader (1990b). The algorithm uses so-called concept trees (which are similar to AND/OR search trees) to impose an appropriate control on the search for· a finite model. This makes it possible to detect cycles at the right moment, and to distinguish between good ones and bad ones. The termination proof mainly depends on Proposition 4.6, that is, on a result from formal language theory.

5 Conclusion

Augmenting JitLC by a transitive closure operator for roles means not just adding yet another construct to this languages, and thus getting a language and an algorithm which are only slightly different from those previously considered. The transitive closure is of a rather different quality.

This claim is substantiated by the following observa­ tions. Firstly, by adding transitive closure, we are leaving the realm of first order logic. Secondly, the algorithm de­ pends on new methods, namely on the use of results from formal language theory, and on a more sophisticated data structure to cope with the nonl.ermination problem. Thirdly, adding features (i.e., functional roles) and feature agreements would make the subsumption problem undecidable (Baader et al. (1991)), whereas this was never a problem for the languages considered by Hollunder&Nutt (1990).

Finally, the expressiveness of ;;tLCreg is also demon­ strated by the fact that concept terms of this language can be used to simulate general concept equations, i.e., equations of the form C = D where both C and D may be complex concept terms of UC or j<l£Creg (see Baader (1990b), Section 6, Baader et al. (1991)). For this reason, the algorithm for ~g can be used to decide satisflability and subsumption of concepts with respect to finite sets of concept equations. As a special case, one thus gets algorithms for satisfiability and subsumption of concepts with respect to cyclic T -boxes of j<ILC, provided that these T-boxes are interpreted with descriptive semantics.