Decidability of SHIQ with Complex Role Inclusion Axioms

1 Motivation

The description logic (DL) SHIQ [Horrocks et al., 1999; Horrocks and Sattler, 2002b] is an expressive knowledge rep­ resentation formalism that extends A.CC [Schmidt-SchauB and Smolka, 1991] (a notational variant of the multi modal logic K [Schild, 1991]) with qualifying number restrictions, inverse roles, role inclusion axioms (RIAs) R ~ S, and transitive roles. The development of SHIQ was motivated by several applications, one of which was the representation of knowledge about complex physically structured domains found, e.g., in chemical engineering [Sattler, 2000] and med­ ical terminology [Rector and Horrocks, 1997].

Although SHI Q allows many important properties of such domains to be captured (e.g., transitive and inverse roles), one extremely useful feature that it cannot express is the "propagation" of one property along another prop­ erty [Padgham and Lambrix, 1994; Rector, 2002; Spackman, 2000]. E.g., it may be useful to express the fact that certain locative properties are transfered across certain partonomic properties so that a trauma or lesion located in a part of a body structure is recognised as being located in the body structure as a whole. This enables highly desirable inferences such as a fracture of the neck of the femur being inferred to be a kind of fracture of the femur, or an ulcer located in the gastric mucosa being inferred to be a kind of stomach ulcer.

The importance of these kinds of inference, particularly in medical terminology applications, is illustrated by the fact that the Grail DL [Rector et al., 1997], which was specifically Ulrike Sattler Institut fiir Theoretische Informatik, TU Dresden, Germany sattler®tcs.inf.tu-dresden.de designed for use with medical terminology, is able to repre­ sent these kinds of propagation (although it is quite weak in other respects). Moreover, in another medical terminology application using the comparatively inexpressive DL A.CC, a rather complex "work around" is performed in order to repre­ sent similar propagations [Schulz and Hahn, 2001]. 1 Similar expressiveness was also provided in the CycL language by the transfersThro statement [Lenat and Guha, 1989].

It is quite straightforward to extend SHI Q so that this kind of propagation can be expressed: simply allow for role inclusion axioms of the form R o S C P, which then enforces all models I to interpret the compo~tion of RI with si as a sub-relation of pi. E.g., the above examples translate into

hasLocation o isDivisionDf ~ hasLocation,

which implies that

Fracturen:lhasLocation.(Neckn:lisDivisionDf.Femur)

is subsumed by/a specialization of

Fracture n :lhasLocation.Femur

Unfortunately, this extension leads to the undecidability of the interesting inference problems; see [Wessel, 2001] for an undecidability proof and [Baldoni, 1998; Baldoni eta/., 1998; Dernri, 2001] for the closely related family of Grammar Log­ ics. On closer inspection of the problem, we observe that only RIAs of the form RoS ~ S or SoR ~ S are required in order to express propagation. Surprisingly, it turns out that SHIQ extended with this restricted form of RIAs is still undecidable. Decidability can be regained, however, by further restricting the set of RIAs to be acyclic (in a non-standard way). This additional restriction does not seem too severe: the above ex­ amples are still covered, acyclic sets of RIAs should suffice for many applications, and cycles in RIAs may even be an indicator of modelling flaws [Rector, 2002]. We call this de­ cidable logic RIQ.

Here, we present the above undecidability result and prove the decidability of SHIQ with acyclic RIAs via a tableau­ based decision procedure for concept satisfiability. The al­ gorithm works by transforming concepts of the form \:IR.C, where R is a role, into concepts of the form \:IA.C, where A is a non-deterministic finite automaton (NFA). These automata are derived from a set of RIAs R by first unfolding R into a set of implications exp(R) between regular expressions and roles, and then transforming the regular expressions into au­ tomata. The algorithm is of the same complexity as the one for SHI Q-in the size of exp(R) and the length of the input concept-but, unfortunately, exp(R) is exponential in R. We present a syntactic restriction that avoids this blow-up; inves­ tigating whether this blow-up can be avoided in general will be part of future work. Finally, in order to evaluate the prac­ ticability of this algorithm, we have extended the DL system FaCT [Horrocks, 1998] to deal with acyclic RIAs. We discuss how the properties of NFAs are exploited in the implementa­ tion, and we present some preliminary results showing that the performance of the extended system is comparable with that of the original, and that it is able to compute inferences of the kind mentioned above w.r.t. the well known Galen medi­ cal terminology knowledge base [Rector and Horrocks, 1997; Horrocks, 1998].

1 In this approach, so-called SEP-triplets are used both to com­ pensate for the absence of transitive roles in A.CC, and to express the propagation of properties across a distinguished "part-of' role.

For full proofs, the interested reader is referred to [Hor­ rocks and Sattler, 2002a].

2 Preliminaries

In this section, we introduce the DL SH+IQ. This includes the definition of syntax, semantics, and inference problems.

Definition 1 Let C and R be sets of concept and role names. The set of roles is R U {R- I R E R}. For roles Ri (each of which can be inverse), a role inclusion axiom (RIA) is an expression oftheform R1 ~ R2, R1 oR2 ~ Rr. or R1 oR2 ~ R2. A generalised role box (g-RBox) is a set of R!As.

An interpretation I = (b. I, .I) associates, with each role name R, a binary relation RI ~ b. I x b. I. Inverse roles are interpreted as usual, i.e.,

An interpretation I is a model of a g-RBox R if it satisfies each inclusion assertion inn, i.e., if

Rf C RJ for each R1 ~ R2 E Rand ~oRJ C ~ ~ro~~o~~~ER where o stands for the composition of binary relations.

Transitive role names were not introduced since R oR ~ R is equivalent to saying that R is a transitive role.

To avoid considering roles such as R--, we define a func­ tion lnv on roles as follows : lnv(R) = R- if R is a role name, and lnv(R) = S if R = s- .

Obviously, if S o R ~ S E R (R o S ~ S E R or R ~ S E R), then each model of R also satisfies lnv(R) o lnv(S) ~ lnv(S) (lnv(S) o lnv(R) ~ lnv(S) and lnv(R) ~ lnv(S)). Thus, in the following, we assume that a g-RBox always contains both "directions" of a RIA.

For a g-RBox R, we define the relation ~ to be the transitive-reflexive closure of ~ over n.

Definition 2 A role S is simple if it does not have implied sub-roles, i.e., if s1 0 s2 ~ s3 implies s3 ~ s does not hold.

The set of SH+IQ-concepts is the smallest set such that (i) every concept name is a concept, and, (ii) if C, D are concepts, R is a role (possibly inverse), S is a simple role (possibly inverse), and n is a nonnegative integer, then CnD, CUD, ·C, \:IR.C, 3R.C, (?:;nS.C), and (~nS.C) are also concepts.

An interpretation I = ( .6.X, .I) consists of a set b. I, called the domain ofi, and a valuation .I which maps every concept to a subset of b. I and every role to a subset of b. I x b. I such that, for all concepts C, D, roles R, S, and non-negative integers n, the following equations are satisfied, where UM denotes the cardinality of a set M:

( ·C)I =b. I\ CI, (CnD)I=CinDI, (CuDf=CiuDI, (3R.C)I = {x l3y.(x, y) E RI andy E CI}, ('VR.C)I ={x I 'Vy.(x,y) E RI impliesy E ex}, (?:;nR.C)I = {X I U{y I (x, y) E RI andy E ci} ?! n }, (~nR.Cf ={x I U{y I (x,y) E RI andy E CI} ~ n}.

A concept C is called satisfiable w. r.t. a g-RBox Riff there is a model I of R with ex -::f. 0. A concept D subsumes a concept C w. r. t. R (written C ~ n D) iff CI ~ DI holds for each model I ofR. For an interpretation I, an element X E b. I is called an instance of a concept C iff X E CI.

Remarks: number restrictions (?:;nR.C) and ( ~nR.C) are restricted to simple roles (intuitively these are (possibly in­ verse) roles that are not implied by others) since SHIQ with­ out this restriction is undecidable [Horrocks et al., 1999].

For DLs that are closed under negation, subsumption and (un)satisfiability can be mutually reduced: C ~ D iff Cn-,D is unsatisfiable, and C is unsatisfiable iff C ~ A n ·A for some concept name A. It is straightforward to extend these reductions to g-RBoxes and TBoxes. In contrast, the reduc­ tion of inference problems w.r.t. a TBox to pure concept in­ ference problems (possibly w.r.t. a g-RBox), deserves spe­ cial care: SHIQ is expressive enough to internalise TBoxes, i.e., to reduce reasoning w.r.t. TBoxes to reasoning with­ out TBoxes [Schild, 1991; Horrocks et al., 1999]. Thus, in the following, we restrict our attention to the satisfiability of SH+ I Q-concepts.

2.1 Relationship with other formalisms

Grammar logics are a class of propositional multi modal logics where the accessibility relations are "axiomatised" through a grammar [Farinas del Cerro and Penttonen, 1988]. More precisely, for l7i, Tj modal parameters, the production rule l71 .. . l7m -+ T1 ... T n can be viewed as a notational variant for the RIA T1 o ... o T n ~ l71 o . .. o l7m . Analogously to the DL case, the semantics of a grammar logic takes into ac­ count only those frames/relational structures that "satisfy the grammar".

Now grammars are traditionally organised in (refinements of) the Chomsky hierarchy, which induces a hierarchy of grammar logics, e.g., context free grammar logics are those propositional multi modal logics where the accessibility rela­ tions can be axiomatised through a context free grammar. Un­ surprisingly, the expressiveness of the grammars influences the expressiveness of the corresponding grammar logics. It was shown that satisfiability of regular grammar logics is ExpTime-complete [Demri, 2001], whereas this problem is undecidable for context free grammar logics [Baldoni, 1998; Baldoni et al., 1998]. The latter result is closely related to the undecidability proof in [Wessel, 2001].

Here, we are concerned with (a) multi modal logics that provide for a converse operator on modal parameters and graded modalities (to restrict the number of accessible worlds; see, e.g., [Tobies, 2001 ]) and (b) a certain sub-class of context-free grammars. In our undecidability proof in Sec­ tion 3, the main difficulty was to develop a grammar that generates the language {(ab) n(cd)n I n ;:=: 0} using only productions of the form R -+ RS orR -+ SR. 2 We can construct a "similar" grammar G with L(G) n (ab)*(cd)* = {(ab) n(cd)n In;:=: 0}. The production rules of G are

Role value maps (RVMs) [Brachman and Schmolze, 1985; Schmidt-Schauss, 1989] are closely related to the RIAs investigated here. RVMs are concepts of the form R1 . .. Rm ~ S1 . .. Sn, for Ri, Si roles, whose interpretation (R1 .. . Rm ~ S1 ... Sn)I is defined as follows:

where (R1 .. . Rm)I(x ) denotes the set of those y E LJ.I that are reachable from x via Rf o . .. o R;;,. Thus the RIA R o S ~ T is equivalent to saying that each individual must be an instance of RS t T. The undecidability proof of KL-ONE [Schmidt-Schauss, 1989] also involves RVMs T ~ RS, and thus cannot be adapted easily to our logic.

3 SH+IQ is undecidable

Due to the syntactic restriction on RIAs, we were not able to adapt the undecidability proof for A.CC with context-free or linear grammars in [Baldoni, 1998; Baldoni et al., 1998; Demri, 2001], the one for A.CC with role boxes [Wessel, 2001], or the one for KL-ONE [Schmidt-Schauss, 1989] to prove undecidability of SH+IQ. In the following, we sketch the reduction of the undecidable domino problem [Berger, 1966] to SH+IQ satisfiability.

Definition 3 A domino system D = (D , H, V) consists of a non-empty set of domino types D = { D1 , ... , Dn}, and of sets of horizontally and vertically matching pairs H s;; D x D and V s;; D x D. The problem is to determine if, for a given D, there exists a tiling t : IN x IN -+ D such that for all m, n E IN, (t(m, n), t(m + 1, n)) E H and (t(m, n), t(m, n + 1)) E V.

For a domino system D, we define a SH+IQ-concept Cv and a g-RBox Rv such that D has a tiling iff Cv is satisfiable w.r.t. Rv. Due to space limitation, we only present Rv:

where EB and 8 denotes addition and subtraction modulo four. Existential and number restrictions on roles h and v (for the horizontal and vertical neighbours) are used to ensure that a point has at most one vertical and at most one horizontal successor, and that these successors satisfy the horizontal and vertical matching conditions induced by H and V; this, as well as ensuring that each point is associated with exactly one domino type, is standard in domino reductions.

2 Thanks to Christof Loding at RWTH Aachen!

The next step is rather special: we do not enforce a grid structure, but a structure with "staircases", which is illus­ trated in Figure 1. To this purpose, we introduce four sub­ roles vo, . . . , V3 of v and four sub-roles ho , ... , h3 of h, and ensure that we only have "staircases". An i-staircase is an alternating chain of vi and hi edges, without any other vr or hrsuccessors. At each point on the x-axis, two staircases start that need not meet again, one i-staircase starting with Vi and one i 8 1-staircase starting with hi81. A symmetric behaviour is enforced for the nodes on the y-axis.

It only remains to ensure that, if two elements b, b' repre­ sent the same point in the grid, then they are associated with the same domino type: b and b' "represent the same point" if there is an n and an instance a on the x-or the y-axis such that both b and b' are reachable by following a staircase starting at a for n steps, i.e., if there is a vi hi-path (resp. hivi-path) of length n from a to b, and a hie 1 Vie 1 -path (resp. Vi$1 hi$1path) of length n from a to b'.

To this purpose, we add super roles Xi of hi and Yi of Vi (for which we use dashed arrows in Figure 1), and the last group of RIAs in Rv. These role inclusion axioms en­ force appropriate, additional role successorships between el­ ements, and we use the additional roles Xi and Yi since we only want to have at most one Vi or hi-successor. For each 2 staircases starting at the same element on one of the axes, these RIAs ensure that each pair of elements representing the same point is related by Yi· To see this, consider the conse­ quences of the RIAs for elements representing the four points (1 , 0), ... ,(2,1), and "apply" the RIAy! xo ~ x0 . Next, "apply" x1 xo ~ x!, and finally x! Yo ~ yo, which yields the Yo-link between the two elements representing (2, 1). Then, starting with Y! Yo ~ y1, we can continue with the points (2, 1), . .. , (3, 2) and work up the role inclusion axioms and up the staircase.

The above observations imply that the concept Cv is satis­ fiable w.r.t. Tv and Rv iff D has a solution.

Theorem 1 Satisfiability of Sfi+IQ-concepts w.r.t. gener­ alized RBoxes is undecidable.

4 RI Q is decidable

In this section, we show that SHIQ with acyclic generalised RBoxes, RIQ, is decidable. We present a tableau-based algorithm that decides satisfiability of RIQ-concepts, and therefore also subsumption in RIQ and, using intemalisa­ tion, both inferences w.r.t. TBoxes. The tableau algorithm implemented in the FaCT system [Horrocks, 1998] was ex­ tended to the one presented here, and the empirical results are reported in Section 5.

Definition 4 Let R be a g-RBox (containing always both di­ rections of a RIA; see above). A role R directly affects a role S if R =j:. S and either R !;;;; S E R, R o S !;;;; S E R , or So R !;;;; S E R. Let "affects" be the transitive closure of "directly affects". An acyclic generalised RBox (a-RBox) is a g-RBox where "affects" has no cycles. RIQ is the restric­ tion ofSH+IQ to a-RBoxes.

Please note that, in a-RBoxes, we can no longer say that a role R is symmetric using R !;;;; R- and R- !;;;; R since this would yield an "affects" cycle of length 2.

Syntactic transformations Before specifying this algorithm, we transform the RBox to make the presentation of the algo­ rithm easier-basically, we unfold the role hierarchy to make all implications explicit.

Firstly, for each (possibly inverse) role R we define two regular expressions as follows:

Secondly, we iteratively replace roles in PR with unions of regular expressions of roles, working our way up the affect­ ing relation. We start with roles "almost" minimal w.r.t. the affecting relation, i.e., we start with roles R such that all roles S which affect R are not affected. We proceed with roles di­ rectly affected by roles that are either already treated or not affected by other roles, and do the following:

After this recursion, we define exp(R) := {PR !;;;; R I R occurs in R}.

Due to the acyclicity of R, the recursion in this transfor­ mation terminates after at most n steps for n the number of role inclusion axioms in R. Please note that, by construction, for each (possibly inverse) role R occurring in R, exp(R) contains exactly one inclusion PR !;;;; R.

For example, for the RIAs R

R o S !;;;; S, So W !;;;; S, T1 o R1 !;;;; R1 , R2oT2 !;;;;R2, VoT1 !;;;;T1, R1!;;;;R,R2!;;;;R the above transformation yield a set exp(R) containing

Unfortunately, the size of exp(R) can be exponential in the size of R. A further syntactic restriction which avoids this exponential blow-up is described in Section 4.1 .

The regular role terms on the left hand side of exp(R) are read with the standard semantics for regular role expressions, (i.e., using union, composition, and transitive closure of bi­ nary relations, see, e.g., [Schild, 1991]). We use L(p) to de­ note the language described by a regular expression p.

Lemma 1 An interpretation I is a model of an acyclic gen­ eralised RBox Riff I is a model of exp(R).

The Tableau Algorithm tries to construct, for an input RIQ-concept D and an a-RBox R, a tableau (an abstraction of a model) forD w.r.t. R. We can prove that this algorithm constructs a tableau for D and R iff D is satisfiable w.r.t. R, and thus decides satisfiability of RIQ concepts w.r.t. an a-RBox. But for the use of NFAs introduced below, this algo­ rithm is quite similar to the one for SHIQ [Horrocks et al. , 1999; Horrocks and Sattler, 2002b].

If R occurs in R, then PR !;;;; R E exp(R) , and we can build a non-deterministic finite automaton (NFA) A R with L(AR) = L(pR). Due to the use of non-deterministic au­ tomata, AR can be of size linear in IPRI · Otherwise, AR is a (two-state) automaton with L(AR) = {R}.

For A an NFA and q a state in A , Aq denotes the NFA obtained from A by making q the (only) initial state of A, and we use q -+ s q' E A to denote that A has a transition labelled with S from q to q'.

As usual, each concept can be easily transformed into an equivalent one in negation normal form (NNF, i.e., negation occurs in front of concept names only), and we use .:...c for the NNF of a concept C. For a concept C, clos( C) is the smallest set that contains C and that is closed under sub-concepts and .:.... Then fclos(C, R) is the superset of clos(C, R) that con­ tains VA~ .D for each S occurring in R or C with q a state in A 8 and VS.D E clos(C) .

A completion tree T for a RIQ concept D and an a­ RBox R is a tree where each node x is labelled with a set .c.(x) ~ fclos(D, R) and each edge (x ,y) fromanode x to its successor y is labelled with a non-empty set£,( (x, y)) ~ R of (possibly inverse) roles occurring in D and R. Finally, completion trees come with an explicit inequality relation :f; on nodes which is implicitly assumed to be symmetric.

If R E £,( (x, y)) for a node x and its successor y and R g S, then y is called an S -successor of x and x is called an lnv(S)-predecessor of y. If y is an S-successor or an lnv(S)­ predecessor of x, then y is called an S-neighbour of x. Fi­ nally, ancestor is the transitive closure of predecessor.

For a roleS, a concept C and a node x in T we define ST (x, C) := {y I y is an S-neighbour of x and C E .c.(y) } .

A node is blocked iff it is either directly or indirectly blocked. A node x is directly blocked iff none of its ances­ tors are blocked, and it has ancestors x', y and y' such that (1) y is not the root node; (2) x is a successor of x' and y is a successor of y'; and (3) .c.(x) = .c.(y), .c.(x') = .c.(y'), £,( (x', x)) = £,( (y', y) ). A node y is indirectly blocked if one of its ancestors is blocked.

For a node x , ~(x) is said to contain a clash if, for some concept name A, {A, ·A} ~ ~(x), or if there is some concept (~nS. C) E .c(x) and x has n + 1 S-neighbours Yo, ... , Yn with C E .c(yi) and Yi #; Yi for all 0 ::::; i < j ::::; n . A completion tree is clash-free if none of its nodes con­ tains a clash, and it is complete if no rule from Figure 2 can be applied to it.

For a RIQ-concept D, the algorithm starts with the com­ pletion tree consisting of a single root node x with ~(x) = { D} and f; empty. It applies the expansion rules in Figure 2, stopping when a clash occurs, and answers "D is satisfiable w.r.t. R" iff the completion rules can be applied in such a way that they yield a complete and clash-free completion tree, and "D is unsatisfiable w.r.t. R" otherwise.

Most of the rules have been used before for fragments of RIQ--only the three Vi-rules are new: they are elegant gen­ eralisations of standard rules for value restrictions taking into account automata.

As usual , we can prove termination, soundness, and com­ pleteness of the tableau algorithm to show tllat it indeed decides satisfiability of RIQ-concepts w.r.t. a-RBoxes.

Theorem 2 The tableau algorithm decides satisfiability and subsumption ofRIQ-concepts w.r.t. a-RBoxes and TBoxes.

4.1 Avoiding the blow-up

So far, the satisfiability algorithm presented here involves an exponential blow-up compared to similar algorithms that are implemented in state-of-the-art description logic reason­ ers [Horrocks, 1998; Haarslev and Moller, 2001] : the closure fclos(D, R) is exponential in R since we have "unfolded" the a-RBox R into the possibly exponentially large exp(R) . While investigating whether and how this exponential blow­ up can be avoided, we observe that a further restriction of the syntax of a-RBoxes avoids this blow-up:

An a-RBox R is called simple if, whenever R1 o S ~ S and S o R2 ~ S are in R, then R1 and R2 do not have a common subrole R' that occurs on the right hand side of an axiom R' o S' C:: R' or S' o R' C:: R'.

For a simple -;-RBox R, exp(R) is only polynomial in the size of R since each term used in the substitution step of the construction of exp(R) from R is at most used once in each other axiom.

Thus, for simple role hierarchies, the tableau algorithm presented here is of the same worst case complexity as for SHIQ, namely 2NExpTime. A detailed investigation of the exact complexity will be part of future work .

5 Empirical Evaluation

In order to evaluate the practicability of the above algorithm, we have extended the DL system FaCT [Horrocks, 1998] to deal with RIQ, and we have carried out a preliminary em­ pirical evaluation .

From a practical point of view, one potential problem with the RI Q algorithm is that the number of different automata, and hence the number of different VA.C concepts, could be very large. Moreover, many of these automata could be equivalent (i.e., accept the same languages). This could ad­ versely effect blocking, and thus lead to a serious degradation in performance [Horrocks and Sattler, 2002b].

The FaCT implementation addresses these possible prob­ lems by transforming all of the initial NFAs into minimal deterministic finite automata (DFAs) using the AT&T FSM Library™ [Mohri et al., 1998]. One DFA is constructed for each role, the states in each automaton are uniquely num­ bered, and the implementation uses concepts of the form VA.C, where A is the number of a state in one of the au­ tomata. Because the automata are deterministic, for each con­ cept of the form VA.C in the label of a node x, the RV2-rule can add at most one concept to the label of a given neigh­ bouring node y per role in the label of the edge (x, y). More­ over, because the automata are minimal, if V A.C leads to the presence of VA'.C in some successor node as a result of re­ peated applications of the R\7'2-rule, then V A.C is equivalent to VA'.C iff A = A'. As A and A' are numbers, such com­ parisons are very easy, and minimisation of automata avoids unnecessary blocking delays.

The implementation is still at the "beta" stage, but it has been possible to carry out some preliminary tests using the well known Galen medical terminology KB [Rector and Hor­ rocks, 1997; Horrocks, 1998]. This KB contains 2,740 named concepts and 413 roles, 26 of which are transitive. The roles are arranged in a relatively complex hierarchy with a maxi­ mum depth of 10. Classifying this KB using FaCT's SHIQ reasoner takes 116s on an 800 MHz Pentium III equipped Linux PC. Classifying the same KB using the new RIQ rea­ soner took a total of 275s, but this includes 135s to compute the minimal DFAs for the role box (it should be noted that this is an unusually large and complex role box, and that comput­ ing the DFAs is a preprocessing step that will not need to be repeated when the remainder of the KB is extended, modified, or queried). This result is encouraging as it shows that, in the case of the Galen KB at least, using automata in VA.C con­ cepts does not, in itself, lead to an unacceptable degradation in performance.

The KB was then extended with several R1As that express the propagation of location across various partonomic roles. These included

hasLocation o isSolidDivisionOf !;;; hasLocation, hasLocation o isLayerOf !;;; hasLocation.

Classifying the extended KB took 280s, an increase of only 2% (3.5% if we exclude the DFA computation time). Sub­ sumption queries w.r.t. this KB revealed that, e.g.,

Fracture n :lhasLocation.NeckOfFemur was implicitly a kind of Fracture n :lhasLocation.Femur

(NeckOfFemur is a solid division of Femur), and

Ulcer n :lhasLocation.GastricMucosa was implicitly a kind of

Ulcer n :lhasLocation.Stomach

(GastricMucosa is a layer of Stomach). None of these sub­ sumption relationships held w.r.t. the original KB. The times taken to compute these relationships w.r.t. the classified KB could not be measured accurately as they were of the same order as a system clock tick (lOms).