Decidable Reasoning in Terminological Knowledge Representation Systems

1 Introduction

A general characteristic of many proposed Terminolog­ ical Knowledge Representation Systems (TKRSs) such as BACK, LOOM, CLASSIC , KRIS, [Rich, 1991: Woods and Schmolze, 1 992] is that they are made up of two different components . Informally speaking, the first. is a general schema concerning the classes of individuals to be represented, their general properties and mutual relationships, while the second is a (partial) instantia­ tion of this schema, containing assertions relating either individuals to classes, or individuals to each other .

Retneving information in actual knowledge bases (KBs) built up using one of these systems is a deduc­ tive process involving both the schema (TBox) and its instantiation (ABox) .

During the realization and use of a KB. a TI\RS should provide a mechanical solution for at least the fol-

·This work has been supported by the ESPRIT Ba$iC Re­ search Act.ion N .6810 COMPULOG 2 and by the Progetto Fi­ nalizzato Sist.emi Informatici e Calcolo Parall€'lo of t.he Cl'\ R (Italian Research Council).

1 This research was partly done while the first author was visiting the Dipart.imento di Informatica e Sist.emistica . l.ini­ versita di Rom a "La Sapienza".

Francesco M. Donini, Andrea Schaerf

Dipart.imento di Informatica e Sistemistica

Universit.a di Roma "La Sapienza"

Via Salaria 113, 1-00198 Roma, Italy

e-mail: { donini,aschaerf}@assi.ing.uniromal .it

lowing problems (from now on, we use the word concepts to refer to classes):

1. Concept Satisfiability: given a KB and a concept C, does there exist at least one model of the KB assigning a nonempty extension to C?
2. Subsumption : given a KB and two concepts C and D, is C more general than D in any model of the KB?
3. :3 . 1\'B-satisfiabi/ity: are an ABox and a TBox consis­ tent with each other?
4. Instance Checking: given a KB, an individual a and a concept C, is a an instance of C in any model of the KB?

Up to now, all the proposed systems (except for A.~RIS) give incomplete procedures for solving the above problems 1-4. That is, some inferences are missed, in some cases without a precise semantical characteriza­ tion of which ones are. If the designer or the user needs a (more) complete reasoning, she/he must either write programs in a suitable programming language, or de­ fine appropriate inference rules completing the inference capabilities of the system {as in BACK, LOOM, and CLAS­ SlC).

In our opinion incomplete procedures are just a pro­ visional answer to the problem-the best possible up to now. In order t.o improve on such an answer, a theoret­ ical analysis of the general problems 1-4 must be done. But most. importantly, theoretical analysis is needed for making cyclic definitions of concepts (see [Nebel, 1990, Chapter 5]) fully available in TKRSs. Such a feature is of undoubtable practical interest, yet present TKRSs can only approximate cycles, by using forward inference rules.

Previous results do not deal with the problems 14 in their full generality. The problems are studied in [Nebel. 1990, Chapter 4], but only incomplete pro­ cedures are given, and cycles are not considered. In [Donini et a/., 1 992] the complexity of instance check­ ing has been analyzed, but only KBs without a TBox are treated . Previous theoretical work on cycles was done in [Baader, 1990b; Baader, 1990a; Nebel, 1990; Nebel , 1991; Schild, 1991], but only KBs formed by the TBox alone are considered. Moreover, these approaches do not deal with number restrictions (except for [Nebel,

1990, Section 5.3.5]), which constitute a basic feature already provided by many TKRSs, and the techniques used do not seem easily extensible to reasoning wit.h A Boxes.

In this paper, we propose a TKRS equipped with a highly expressive language of practical significance, and prove the decidability of problems 1-4. In particular . our system makes use of the language ACCNn, which sup­ ports general complements of concepts, number restric­ tions and role conjunction. Moreover, the system allows one to express inclusion statements between general con­ cepts and, as a particular case, terminological cycles. \-\ 1 e prove decidability by means of a suitable calculus, which is developed within the quite well established frame­ work of constraint systems (see [Donini et a/., 1991 a: Schmidt-SchauB and Smolka, 1991]) thus exploiting a uniform approach to reasoning in TKRSs. Moreover, our calculus can easily be turned into a decision procedure.

The paper is organized as follows. In Section 2 we in­ troduce the language, and we give it a Tarski-style exten­ sional semantics, which is the most. commonly used. In Section 3 we provide a calculus, and show its correctness and termina.t.ion. In Section 4 we consider a. refinement. of our calculus, working in exponential space. In Sec­ tion 5 we establish the equivalence of general inclusion statements and general concept definitions using the de­ scriptive semantics. Finally, we discuss in detail several practical impacts of our results in Section 6. For the sake of brevity proofs are omitted. They can be found in [Buchheit et a/., 1993] .

2 Preliminaries

ln concept languages, concepts represent. the classt's of objects in the domain of interest, while roles represent. binary relations between objects. Complex concepts and roles can be defined by means of suitable constructors ap­ plied to primitive concepts and primitive roles. In par­ ticular, concepts and roles in ACCNR can be formed by means of the following syntax (A denotes a primi­ tive concept, P; (i = 1, .. . , m) denotes a primitive role. C and D denote arbitrary concepts and R an arbitrary role):

C,D R AI Tl .LI (Cn D) 1 (CUD) I ..,cl VR.C I 3R.C I (~ nR) I(~ nR) PI n . .. npm (primitive concept.) (top) (bottom) (conjunction) (disjunction) (complement) (universal quantification) (existential quantification) (number restrictions) (role conjunction)

We interpret concepts as subsets of a domain and roles as binary relations over a domain. More precisely, an 111terpretation I= (L~I, .I) consists of a nonempt.y set ~I (the domaiu of I) and a function .I (the e:rfenswn fuur­ tion of I) that maps every conc1t to a subset of f1I and every role to a subset of D. I x D. such that the follo\\'ing equations are satisfied (~{} denotes the cardinality of a set):

T 1 = ti 7 , .L 1 =0. (CnDf=C 7 nD 7 , (C u D) 7 = C 7 u D 7 , (..,C) 7 = ~r \ C 1 (VR.C) 1 ={dE ~rIVe: (d,e) E R 7 -- e E C 1 } (3R.C) 7 ={dE ~r l3e : (d,e) E R 1 1\e E C 1 } (~nR) 1 ={dE~ 1 1 U{el(d,e)ER 1 } ~n} (~nR) 1 ={dE~ 1 1 U{el(d,e)ER 1 } ~n} ( P1 n .. · n Pm) 1 = Pf n .. · n PJ,

A KB built by means of concept languages is formed by two components: The intensional one, called the TBox. and the extensional one, called the ABox.

We first turn our attention to the TBox. As we said before. the intensional level specifies the properties of the concepts of interest in a particular application. Syntacti­ cally, such properties are expressed in terms of so-called wclusion statements (see [Nebel, 1990, Chapter 3]). An inclusion statement (or simply inclusion) has the form

where C and D are two arbitrary concepts. Intuitively, the statement specifies that every instance of C is also an instance of D. More precisely, an interpretation 1 satisfies the inclusion C ~ D if CI ~ DI. A TBox T is a finite set of inclusions. An interpretation I is a model for a TBox T if 1 satisfies all inclusions in T .

Many TKRSs provide the user with mechanisms for stating concept definitions (e.g. [Nebel, 1990, Section :3.2)) of the form A :::: D (interpreted as set equality), or .·iSD (primitive concept definition, interpreted as set inclusion), with the restrictions that the left-hand side concept A must be a. concept name, that for each concept name at most one definition is allowed, and that no so­ cal led terminological cycles are allowed, i.e. no concept name may occur-neither directly nor indirectly-within its own definition .

\Ve do not. impose any of these restrictions to the form of inclusions, obtaining statements that are syntactically more expressive than concept definitions. In particular, a definition of the form A :::: D can be expressed in our system using the pair of inclusions A ~ D and D ~ A, whereas an inclusion of the form C ~ D, where C and D art' arbitrary concepts , cannot be expressed with concept definitions. :t\1oreover, cyclic inclusions are allowed in our statements , realizing terminological cycles.

As shown in [Nebel, 1991], there are at least three t.ypes of semantics for terminological cycles, namely the least fixed point, the greatest fixed point, and the de­ scriptive semantics. However, fixed point semantics ap­ ply only to fixed point statements, which are much less general than our inclusion statements. Instead, the de­ scriptive semantics interprets statements as just restrict­ ing the set of possible models, with no definitional im­ port. Hence, it can be suitably extended to our case, and is exactly the one we adopt .

\Vt> can now turn our attention to the extensional/eve/ of t.lw KB, i.e. the ABox. The ABox essentially allows one to specify instance-of relations between individuals and concepts, and between pairs of individuals and roles.

Lf:'l. 0 be an alphabet of symbols, called individuals. Instance-of relationships are expressed in terms of mem­ bership assertions of the form:

where a and b are individuals, C is a concept.. and R is a role. Intuitively, the first form states that a is an instance of C, whereas the second form states that a is related to b by means of the role R.

In order to assign a meaning to membership asser­ tions, the ext.ension function .I of an interpretation I is extended to individuals by mapping them to elements of !).I in such a way that a.I :j: bi if a :j: b (Unique Name Assumption) . An interpretation I satisfies the assertion C( a) if a I E cr, and satisfies R.( a , b) if (a. I . bi) E R.I . An ABox A is a finite set of membership assertions. I is a model for an A Box A if I satisfies all the assertions in A .

An ACCNR-knowledge base E is a pair E = (T. A) where ! is a TBox, and A is an ABox. An interpretation I is a model for E if it is both a model for T and a moue! for A. We can now formally define the problems 1-4 mentioned in the introduction, w.r .t . a given KB E:

1. Concept Satisfiability : C is satisfiable w.r.t ~. if there exists a model I of E such that C 1 f- 0:
2. Subsumption: Cis subsumed by D w .r.t.. ~.if cr c DI for every model I of E; -
3. KB-satl.sfiability: E itself is satisfiable, if it. has il model;
4. Instance Checking: a is an instance of C, writt en E F= C(a.), if the assertion C(a.) is satisfied in ewry model of~.

Example 2.1 Consider the following KB E = (T. A):

T = { 3TEACHES.Course [; (Studentn 3DEGREE.BS) U Prof . Prof [; 3DEGREE.MS. 3DEGREE.MS C 3DEGREE.BS .

MS nBS [; .l}

-

A= {TEACHES(john,csl), (~ 1 DEGREE){j ohn). Course(csl)}

It is easy t.o see that E is satisfiable. Notice also that. it is possible to draw several non-trivial conclusions from L: . For example, we can infer that L: F= Student(john ). Intuitively this can be shown as follows: john teaches a course, thus he is either a student with a BS or a professor. But he can't be a professor since professors have at least two degrees (BS and MS) and he has at most one , therefore he is a student. D

Given the above semantics, the problems 1- 4 can Rll be reduced to KB-satisfiability (or to its complement) in linear time. In fact, given a KB E = (T, A) . a concept Cis satisfiable w.r.t E iff the KB (T ,A U {C(b)}) is satisfiable, and C' is subsumed by D w .r. t. E iff the h B (T,A U {(C' n ·D)(b)}) is not satisfiable, where b is il new individual not appearing in E. Finally, E f= C( a) iff the KB (T,AU{(-.C)(a.)}) is not satisfiable. Hence, we can concentrate just on KB-satisfiabilit.y in I he next section.

3 Decidability Result

In this section we present. a calculus for deciding 1\ 8satisfiability and state its correctness and termination.

Our method makes use of the notion of constraint. svs­ t.ems [Donini et a/. , 1991 a; Schmidt-Schauf3 and Smoli,il .

1991: Donini et al., 1991b), and is based on a tableaux­ like calculus that tries to build a model for the logical formula corresponding to a KB.

Consider an alphabet of variable symbols V. The el­ ements of V are denoted by the letters x, y, z, w. In the sequel we use the term object as an abstraction for indi­ vid~Ial and variable (i.e. an object is an element of OUV) . ObJects are denoted by the symbols s, t and, as in Sec­ tion 2, individuals are denoted by a, b. In the rest of this section, R denotes the role R = P1 n ... n P~c (k ~ 1).

A constraint is a syntactic entity of one of the forms :

where C is a concept and P is a primitive role. Con­ cepts are assumed to be simple, i.e. they contain only complements of the form -.A, where A is a primitive concept . Arbitrary ACCNR.-concepts can be rewritten into equivalent simple concepts in linear time [Donini et a/., 1991a]. A constraint system is a finite nonempty set of constraints.

Given an interpretation I, we define anI-assignment o as a function that maps every variable in V to an element. of ~I (not necessarily injectively), and every individual a to a 1 (i.e. a(a) = ai for all a E 0).

A pair (I , rx) satisfies the constraint s: C: if a( s) E CI, the constraint sPt if (a(s), a(t)) E pi, the constraint s # t if a(s) f- a(t) , and finally, the constraint Vx.x : C if C 1 = .D_I A constraint system s is satisfiable if there is a pair (I , a·) that satisfies every constraint inS.

An ACCNR.-knowledge base E = (T, A) can be trans­ lated into a constraint system Sr. by replacing every in­ clusion C ~ D E T with the constraint Vx.x : -,cUD, every membership assertion C(a) with a: C , R(a, b) with a P1 b .. .. , a.Pkb, and including the constraint a f. b for e\·ery pair (a, b) of individuals appearing in A . It is easy to see that E is satisfiable if and only if Sr. is satisfiable.

In order to check a constraint system S for satisfiabil­ ity, our technique adds constraints to S until either an evident contradiction is generated or an interpretation satisfying it can be obtained from the resulting system. Constraints are added on the basis of a suitable set cf so-called propagation rules.

Before providing the rules, we need some additional definit ions. Let S be a constraint system. We say that t is an R-s1t ccessor of s inS if sP1t , ... , sP~ct are inS. We say that t is a }-s-uccessor of s in S if for some role R, t is an R-successor of s. If Sis clear from the context we simply say that t is an R.-successor or a }-successor of s. :\loreover , we denote by successor the transitive closure of the relation !-successor, and we denote by predecessor it.s inverse.

We denote by S[a:j s] the constraint system obtained from S by replacing each occurrence of the variable x by s. \'Ve say that s and t are separated in S if the constraint 8 # t is inS'.

.Given a constraint. system S we say that two vari­ a hies .r and y are S- equivalent , written x =· y, if { C I .r: C E S} = { C I y: C E S} . Intuitively, two S-equivalent variables could represent the same element in the potential interpretation built by the rules, unless they were separated.

The propagation rules are:

if s: C1 n C2 is in S, s: C\ and s: C2 are not. hot.h inS

S -u {s:D}uS

if s: C1 u C2 is in S, neither s: C1 nor s : C2 is in S and D = C1 or D = C2

if s:YR.C is inS, tis a R-successor of s . t:C is not in S

if s: 3R.C' is inS, y is a new variable, there is not such that t is a R-successor of s in S and t : C is in S; if s is a variable there is no variable uo in S such that w is a predecessor of s and s :=, uo

if s: (~ n R) is in S, y1, ... , y, are new vari­ ables, there do not exist n pairwise separated R-successors of s in S; if s is a variable there is no variable w such that w is a predecessor of s and s =· w

• S -~ S[yjt]

if s : ($ n R) is m S, s has more than u R­ successors in S , y, t are two R-succes~o rs of .­ that. are not separated

We call the rules -+u , -+< nondeterministic rules . since they can be applied in different ways to the same constraint system. All the other rules are called dctn·­ ministic rules. Moreover, we call the rules - 3 . ~> gt n­ erating rules, since they introduce new variables In the constraint system. All other rules are called nongener­ ating ones.

The use of the condition based on the S-equivalence relation in the generating rules is related to t.he goal of keeping the constraint system finite even in presence of potentially infinite chains of applications of generating rules.

One can verify that rules are always applied to a sys­ tem S either because of the presence in S of a given constraint s: Cor, in the case of the -+vx-rule, b1'caus~' of the presence of an object s in S. When no confusion arises, we will say that a. rule is applied to the object. ::; .

Proposition 3.1 (Invariance) Let S and S' be co ll­ straint systems. Then:

1. If S' is obtained from S by application of a d£1u­ ministi.c rule, then S is satisfiable if and onll! I( S' is satisfiable .
2. If S' is obtained from S by application of a nondr­ terministic rule, then S is satisfiable if S' is safi!i­ fiable. Furthermore , if a nondeterminxstic ndt o p­ plies to S , then it can be applied in such a way that it yields a constraint system S' which is saflsjiab!t if and only if S is satisfiable.

Given a constraint system, more than one rule might be applicable to it. We define the following .sfl'(tftgy for the application of rules:

• I . apply a rule to a variable only if no rule is applicable to individuals;
• apply generating rules only if no nongenerating rule is applicable;
• apply a generating rule to a variable x only if no rule is applicable to a predecessor of x.

A constraint system is complete if no propagation rule applies to it. A complete system derived from a system S is also called a completion of S . A clash is a constraint system having one of the following forms:

• {s:.L}
• {s: A. s : -,A}, where A is a primitive concept.

In order to obtain an interpretation from a complete constraint system we need some additional definitions. Let S be a constraint system and x, w be variables in S. We call w a witness of x in S if the three following conditions hold :

:2. w is a predecessor of x in S

• :3. no rule is applicable to any predecessor of x.

Notice that. the third condition ensures that no new constraint will be imposed on x. We say x is blocked (by tl') if .r has a witness ( w) in S. In a constraint system obtained from an Sr; by applying the rules according to t.he st.rat.egy, a blocked variable has exactly one witness and no successors.

Let. S be a constraint system. We define the canonical interpretation Is for S and the canonical Is-assignment os for S as follows:

1. j,Is :={sIs is an object inS}
2. '2. ns(s) := s
3. :~. s E .4 1 " iff s: .4 is inS
4. (s, t) E pis iff
5. (a) sPt is inS or
6. (b) s is a blocked variable, w is the witness of s in S and wPt is in S.

The canonical interpretation of complex concepts and roles can be uniquely reconstructed from the interpreta­ tions of the primitive ones imposing the equations stated in Sect ion 2.

Theorem 3.2 (Correctness) LetS be a complete con8/minf s:IJsfem. S is satisfiable iff it contains no clash.

Proof. (Sketch) If S contains a clash, it is clearly unsat­ isfiabl e. [f S contains no clash , it can be shown that the pair (Is, crs ) satisfies every constraint in S . 0

The termination of the calculus is based on the follow­ ing property : In any constraint system obtained from an s~ by applying the rules according to the strategy, every variable can have at most 2n variables among its prede­ ct>ssors. where n is the size of E. The technique we use is similar t.o the standard filtration technique used in modal logics. with the main difference that we must take into account. separated variables.

Theorem 3.3 (Termination) Let S bt a cou.stnuut system. Every completion of S is finite.

Notice that, since the domain of the canonical inter­ pretation jj.Is is always finite, we have also implicitly proved that A£CNR-knowledge bases have the finite model property, i.e. any satisfiable knowledge base has a finite model .

Theorem 3.4 (Decidability) Checking whether au ACCNR.-11 B is satisfiable is a decidabif problem.

4 A Calculus Working in Exponential Space

The calculus proposed in the previous section requires to compute all the completions of the constraint systPm SE . Unfortunately, such completions may be of double exponential size w.r.t . the size of :E.

For an exponential space algorithm it is therefore cru­ cial not. to keep an entire complete constraint. system in memory, but to store only small portions at. a time.

We give propagation rules, called trace rules. that build up only a portion of complete constraint syst.Pm;; .

The trace rules consist of the --n-, --->u-, ........ v- , -v.,.­ and the ---><-rule (the nongenerating rules) together 1rith the two generating rules --->T3 and --T> , which art> obtained respectively from the --+3- and -the ->-rule adding the following condition of application: -

for all constraints tPx in S, either t is a predecessor of s or t = s.

Let 1' be a. constraint system obtained fro111 .... ;~ by application of the trace rules. We call T a tnicf of-"'~ if no trace rule applies to T.

If the trace rules are applied according to the st r<tt­ egy they show the following behavior: Given an object s, if at least one generating rule is applicable. all its 1-successors y1 , . . . , y, are introduced. Then, after non­ generating rules are applied, one variable y; is ( nonde­ terministically) chosen , and all !-successors of y; are in­ troduced . Unlike normal propagation rules, trace rules introduce no successor for any object different from .1/i. Then , one variable is chosen among the !-successors of y; , only its !-successors are added to the constraint sys­ tem, and so on.

The reason why we introduce all the 1-successors oft he "chosen" object is the following . For every chosen object s all !-successors of s must be present simultaneously at some stage of the computation, since only the interplay of role conjunction and number restrictions forc~?s us to identify certain successors. This is important because. when identifying variables , the constraints imposed on them are combined, which may lead to dashes that oth­ erwise would not have occurred.

A calculus based on trace rules, for deciding satisfia­ bility and subsumption of A£CNR-concepts , was pre­ viously defined in [Donini et a/., 199la). Algorithms exploiting traces have been given in [Hollunder fl a/ .. 1990) . However . all these works do not deal with l\ 11s. but only with concept expressions.

Proposition 4.1 Let :E be an ACCNR-KB, SE its as­ wualed constmint s:IJstem, and let n be the size of L:. 7'hfll.'

1. The length of a trace rule derivation issuing from s~ is bounded by 2n.
2. Every complete constraint system extending SE can br obtained as the union of finitely many traces.
3. .J. SupposeS is a complete constraint system extending S~ and T is a finite set of traces such that S = UTET T. Then S contains a clash if and only if .some T E T contains a clash.

Since an ACCNR-KB :E is satisfiable if and only if there exists a complete constraint system derivable from S~ without a clash, it follows from Proposition 4.1 that sat.isfiahility of an ACCNR-KB can be decided with ex­ ponential space. A possible algorithm using space 2P(n) where p(n) is a polynomial in the size of SE may be the following: compute one complete constraint system, one trace at a time, trying all possible applications of the nondeterministic rules -+<, -+u, and finding the choices leading to traces without -a clash.

Theorem 4.2 Satisfiability of an ACCNR-KB can be drndul with exponential space.

Thanks to an unpublished manuscript by D. McAlle­ st l'r. and (independently) from an observation by W. N utt . we know that deciding the satisfiability of an A.CCNR-KB is an EXPTIME-hard problem. Hence, we do not expect t.o find any algorithm solving the prob­ lem in polynomial space, unless PSPACE=EXPTIME. :\evertheless, the algorithm outlined above may require doubl t' exponential time. It is still open whether there exists an algorithm working in (simple) exponential time.

5 Inclusions versus Concept Definitions

In this section we compare the expressive power of T Boxes defined as a set of inclusions (as done in this paper) and TBoxes defined as a set of (possibly cyclic) concept definitions of the form A$D and A ::::: D.

Unlike [Baader, 1990a] and [Schild, 1991], we con­ sider reasoning problems dealing with TBox and ABox together. 1\otoreover, we use the descriptive semantics for the concept definitions, as we do for the inclusions. The result we have obtained is that inclusion statements and concept definitions actually have the same expres­ sive power. In details , we show that the satisfiability of a knowledge base I: = (A, T), where T is a set of inclu­ sion statements, can be reduced to the satisfiability of a knowledge base :E' = (A', T') such that T' is a set of concept definitions. The other direction-from concept definitions to inclusions-is trivial since definitions can be expressed by pairs of inclusions (see Section 2).

As a notation, given a TBox T = { C1 !;;;; D1, ... , Cn ~ D,}, we define the concept Cr as Cr = (...,C1 U Dt) n · · · n ( -,C'n U Dn). As pointed out in [Baader, 1990a] for ACC. an interpretation satisfies a TBox T iff it satisfies t.he ('quation Cr = T. This result easily extends to ACCXR. .

Gi,·en a knowledge base :E = (A, T) and a concept A not appearing in I: , we define the knowledge base :E' =

(A', T') as follows:

A' AU {A(b) Ibis an individual in ~}

where P1 , P2 , ... , Pn are all the primitive roles appearing in E. Interpreting the primitive concept definition (~) as an inclusion, and exploiting canonical interpret.ations. we are able to prove the following result.

Theorem 5.1 E is satisfiable iff E' is salisfinble.

6 Discussion

In this paper we have proved the decidabilit.y of the main inference services of a TKRS based on the concept. lan­ guage A.CCNn. We believe that this result. is not only of theoretical importance, but has the following impact.s on existing TKRSs.

First of all, a. complete pl·ocedure working in expo­ nential space can be easily devised from the calculus provided in Sections 3 and 4. From this procedme. onP can build more efficient (but still complete) ones by ap­ plying optimization techniques. Such procedures might work well in practical cases, despite their worst. case in­ tractability.

Secondly, a complete procedure (possibly optimized) offers a. benchmark for comparing in com plet.P proce­ dures, not only in terms of performance, but also in terms of missed inferences. In fact, incomplete proce­ dures can be meaningfully compared only if missed in­ ferences are considered. However, to recognize missed inferences over large examples, one needs exactly a com­ plete procedure-even if not. an efficient. one---like ours .

Thirdly, new incomplete procedures can be obt.ained from the calculus by modifying some of the propagat.ion rules . Since the rules build up a model , modifi c<t t.ion;.; to them have a semantica.l counterpart which giYes a pre­ cise account of the incomplete procedures obtained. For instance, define the depth of a variable .1· as the 1111111ber of variabl es which are predecessors of .r . Thr n. n il incomplete calculus could be devised, which gen<'rat.e.; variables only to a given depth- say, linear depth in the size of the KB. This calculus would miss contradictions (and hence inferences, by refutation) occurring in ,·ari­ ables which are "far away" from the known individuals of the KB, and this is a meaningful explanation of the incompleteness, even for a non-expert user. From a com­ putational point of view, an immediate consequence of the complexity analysis carried over in this paper is that such an incomplete procedure would run in polynonti nl space.

Acknowledgements

Maurizio Lenzerini inspired us to this work and con­ tributed to the paper in several discussions. Franz Baader and \Verner Nutt. made many helpful comments on earlier drafts. Scott Benson helped us in improving the English . The third author also acknowledges Yoav Shoham for his hospitality at the Computer Science De­ partment of Stanford University.