M. Buchheit, F. M. Donini and A. Schaerf
Volume 1, 1993Links to Full Text:
© Copyright 1993-2006 AI Access Foundation, Inc.
Journal of Artificial Intelligence Research 1 (1993) 109-138 Submitted 7/93; published 12/93 Decidable Reasoning in Terminological Knowledge Representation Systems Martin Buchheit email@example.com German Research Center for Artificial Intelligence (DFKI) Stuhlsatzenhausweg 3, D-66123 Saarbr"ucken, Germany Francesco M. Donini firstname.lastname@example.org Andrea Schaerf email@example.com Dipartimento di Informatica e Sistemistica Universit`a di Roma "La Sapienza", Via Salaria 113, I-00198 Roma, Italy Abstract Terminological knowledge representation systems (TKRSs) are tools for designing and using knowledge bases that make use of terminological languages (or concept languages). We analyze from a theoretical point of view a TKRS whose capabilities go beyond the ones of presently available TKRSs. The new features studied, often required in practical applications, can be summarized in three main points. First, we consider a highly expressive terminological language, called ALCN R, including general complements of concepts, number restrictions and role conjunction. Second, we allow to express inclusion statements between general concepts, and terminological cycles as a particular case. Third, we prove the decidability of a number of desirable TKRS-deduction services (like satisfiability, subsumption and instance checking) through a sound, complete and terminating calculus for reasoning in ALCN R-knowledge bases. Our calculus extends the general technique of constraint systems. As a byproduct of the proof, we get also the result that inclusion statements in ALCN R can be simulated by terminological cycles, if descriptive semantics is adopted. 1. Introduction A general characteristic of many proposed terminological knowledge representation systems (TKRSs) such as krypton (Brachman, Pigman Gilbert, & Levesque, 1985), nikl (Kaczmarek, Bates, & Robins, 1986), back (Quantz & Kindermann, 1990), loom (MacGregor & Bates, 1987), classic (Borgida, Brachman, McGuinness, & Alperin Resnick, 1989), kris (Baader & Hollunder, 1991), k-rep (Mays, Dionne, & Weida, 1991), and others (see Rich, editor, 1991; Woods & Schmolze, 1992), 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) instantiation of this schema, containing assertions relating either individuals to classes, or individuals to each other. This characteristic, which the mentioned proposals inherit from the seminal TKRS kl-one (Brachman & Schmolze, 1985), is shared also by several proposals of database models such as Abrial's (1974), candide (Beck, Gala, & Navathe, 1989), and taxis (Mylopoulos, Bernstein, & Wong, 1980). Retrieving information in actual knowledge bases (KBs) built up using one of these systems is a deductive process involving both the schema (TBox) and its instantiation (ABox). cfl1993 AI Access Foundation and Morgan Kaufmann Publishers. All rights reserved. Buchheit, Donini, & Schaerf In fact, the TBox is not just a set of constraints on possible ABoxes, but contains intensional information about classes. This information is taken into account when answering queries to the KB. During the realization and use of a KB, a TKRS should provide a mechanical solution for at least the following problems (from this point on, we use the word concept to refer to a class): 1. KB-satisfiability: are an ABox and a TBox consistent with each other? That is, does the KB admit a model? A positive answer is useful in the validation phase, while the negative answer can be used to make inferences in refutation-style. The latter will be precisely the approach taken in this paper. 2. Concept Satisfiability: given a KB and a concept C, does there exist at least one model of the KB assigning a non-empty extension to C? This is important not only to rule out meaningless concepts in the KB design phase, but also in processing the user's queries, to eliminate parts of a query which cannot contribute to the answer. 3. Subsumption: given a KB and two concepts C and D, is C more general than D in any model of the KB? Subsumption detects implicit dependencies among the concepts in the KB. 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? Note that retrieving all individuals described by a given concept (a query in the database lexicon) can be formulated as a set of parallel instance checkings. The above questions can be precisely characterized once the TKRS is given a semantics (see next section), which defines models of the KB and gives a meaning to expressions in the KB. Once the problems are formalized, one can start both a theoretical analysis of them, and--maybe independently--a search for reasoning procedures accomplishing the tasks. Completeness and correctness of procedures can be judged with respect to the formal statements of the problems. Up to now, all the proposed systems give incomplete procedures for solving the above problems 1-4, except for kris1. That is, some inferences are missed, in some cases without a precise semantical characterization of which ones are. If the designer or the user needs (more) complete reasoning, she/he must either write programs in a suitable programming language (as in the database proposal of Abrial, and in taxis), or define appropriate inference rules completing the inference capabilities of the system (as in back, loom, and classic). From the theoretical point of view, for several systems (e.g., loom) it is not even known if complete procedures can ever exist--i.e., the decidability of the corresponding problems is not known. Recent research on the computational complexity of subsumption had an influence in many TKRSs on the choice for incomplete procedures. Brachman and Levesque (1984) 1. Also the system classic is complete, but only w.r.t. a non-standard semantics for the treatment of individuals. Complete reasoning w.r.t. standard semantics for individuals is not provided, and is coNPhard (Lenzerini & Schaerf, 1991). 110 Decidable Reasoning in Terminological KR Systems started this research analyzing the complexity of subsumption between pure concept expressions, abstracting from KBs (we call this problem later in the paper as pure subsumption). The motivation for focusing on such a small problem was that pure subsumption is a fundamental inference in any TKRS. It turned out that pure subsumption is tractable (i.e., worst-case polynomial-time solvable) for simple languages, and intractable for slight extensions of such languages, as subsequent research definitely confirmed (Nebel, 1988; Donini, Lenzerini, Nardi, & Nutt, 1991a, 1991b; Schmidt-Schauss & Smolka, 1991; Donini, Hollunder, Lenzerini, Marchetti Spaccamela, Nardi, & Nutt, 1992). Also, beyond computational complexity, pure subsumption was proved undecidable in the TKRSs U (Schild, 1988), kl-one (Schmidt-Schauss, 1989) and nikl (Patel-Schneider, 1989). Note that extending the language results in enhancing its expressiveness, therefore the result of that research could be summarized as: The more a TKRS language is expressive, the higher is the computational complexity of reasoning in that language--as Levesque (1984) first noted. This result has been interpreted in two different ways, leading to two different TKRSs design philosophies: 1. `General-purpose languages for TKRSs are intractable, or even undecidable, and tractable languages are not expressive enough to be of practical interest'. Following this interpretation, in several TKRSs (such as nikl, loom and back) incomplete procedures for pure subsumption are considered satisfactory (e.g., see (MacGregor & Brill, 1992) for loom). Once completeness is abandoned for this basic subproblem, completeness of overall reasoning procedures is not an issue anymore; but other issues arise, such as how to compare incomplete procedures (Heinsohn, Kudenko, Nebel, & Profitlich, 1992), and how to judge a procedure "complete enough" (MacGregor, 1991). As a practical tool, inference rules can be used in such systems to achieve the expected behavior of the KB w.r.t. the information contained in it. 2. `A TKRS is (by definition) general-purpose, hence it must provide tractable and complete reasoning to a user'. Following this line, other TKRSs (such as krypton and classic) provide limited tractable languages for expressing concepts, following the "small-can-be-beautiful" approach (see Patel-Schneider, 1984). The gap between what is expressible in the TKRS language and what is needed to be expressed for the application is then filled by the user, by a (sort of) programming with inference rules. Of course, the usual problems present in program development and debugging arise (McGuinness, 1992). What is common to both approaches is that a user must cope with incomplete reasoning. The difference is that in the former approach, the burden of regaining useful yet missed inferences is mostly left to the developers of the TKRS (and the user is supposed to specify what is "complete enough"), while in the latter this is mainly left to the user. These are perfectly reasonable approaches in a practical context, where incomplete procedures and specialized programs are often used to deal with intractable problems. In our opinion incomplete procedures are just a provisional answer to the problem--the best possible up to now. In order to improve on such an answer, a theoretical analysis of the general problems 1-4 is to be done. Previous theoretical results do not deal with the problems 1-4 in their full generality. For example, the problems are studied in (Nebel, 1990, Chapter 4), but only incomplete 111 Buchheit, Donini, & Schaerf procedures are given, and cycles are not considered. In (Donini, Lenzerini, Nardi, & Schaerf, 1993; Schaerf, 1993a) the complexity of instance checking has been analyzed, but only KBs without a TBox are treated. Instance checking has also been analyzed in (Vilain, 1991), but addressing only that part of the problem which can be performed as parsing. In addition, we think that the expressiveness of actual systems should be enhanced making terminological cycles (see Nebel, 1990, Chapter 5) available in TKRSs. Such a feature is of undoubtable practical interest (MacGregor, 1992), yet most present TKRSs can only approximate cycles, by using forward inference rules (as in back, classic, loom). In our opinion, in order to make terminological cycles fully available in complete TKRSs, a theoretical investigation is still needed. Previous theoretical work on cycles was done in (Baader, 1990a, 1990b; Baader, B"urkert, Hollunder, Nutt, & Siekmann, 1990; Dionne, Mays, & Oles, 1992, 1993; Nebel, 1990, 1991; Schild, 1991), but considering KBs formed by the TBox alone. Moreover, these approaches do not deal with number restrictions (except for Nebel, 1990, Section 5.3.5) --a basic feature already provided by TKRSs-- and the techniques used do not seem easily extensible to reasoning with ABoxes. We compare in detail several of these works with ours in Section 4. In this paper, we propose a TKRS equipped with a highly expressive language, including constructors often required in practical applications, and prove decidability of problems 1-4. In particular, our system uses the language ALCN R, which supports general complements of concepts, number restrictions and role conjunction. Moreover, the system allows one to express inclusion statements between general concepts and, as a particular case, terminological cycles. We prove decidability by means of a suitable calculus, which is developed extending the well established framework of constraint systems (see Donini et al., 1991a; Schmidt-Schauss & 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 introduce the language, and we give it a Tarski-style extensional semantics, which is the most commonly used. Using this semantics, we establish relationships between problems 1-4 which allow us to concentrate on KB-satisfiability only. In Section 3 we provide a calculus for KB-satisfiability, and show correctness and termination of the calculus. Hence, we conclude that KB-satisfiability is decidable in ALCN R, which is the main result of this paper. In Section 4 we compare our approach with previous results on decidable TKRSs, and we establish the equivalence of general (cyclic) inclusion statements and general concept definitions using the descriptive semantics. Finally, we discuss in detail several practical issues related to our results in Section 5. 2. Preliminaries In this section we first present the basic notions regarding concept languages. Then we describe knowledge bases built up using concept languages, and reasoning services that must be provided for extracting information from such knowledge bases. 2.1 Concept Languages In concept languages, concepts represent the classes of objects in the domain of interest, while roles represent binary relations between objects. Complex concepts and roles can be 112 Decidable Reasoning in Terminological KR Systems defined by means of suitable constructors applied to concept names and role names. In particular, concepts and roles in ALCN R can be formed by means of the following syntax (where Pi (for i = 1; : : :; k) denotes a role name, C and D denote arbitrary concepts, and R an arbitrary role): C; D Gamma ! A j (concept name) ? j (top concept) ? j (bottom concept) (C u D) j (conjunction) (C t D) j (disjunction) :C j (complement) 8R.C j (universal quantification) 9R.C j (existential quantification) (* n R) j (^ n R) (number restrictions) R Gamma ! P1 u Delta Delta Delta u Pk (role conjunction) When no confusion arises we drop the brackets around conjunctions and disjunctions. We interpret concepts as subsets of a domain and roles as binary relations over a domain. More precisely, an interpretation I = (Delta I ; Delta I) consists of a nonempty set Delta I (the domain of I) and a function Delta I (the extension function of I), which maps every concept to a subset of Delta I and every role to a subset of Delta I Theta Delta I. The interpretation of concept names and role names is thus restricted by AI ` Delta I, and P I ` Delta I Theta Delta I , respectively. Moreover, the interpretation of complex concepts and roles must satisfy the following equations (]fg denotes the cardinality of a set): ?I = Delta I ?I = ; (C u D)I = CI " DI (C t D)I = CI [ DI (1) (:C)I = Delta I n CI (8R.C)I = fd1 2 Delta I j 8d2 : (d1; d2) 2 RI ! d2 2 CIg (9R.C)I = fd1 2 Delta I j 9d2 : (d1; d2) 2 RI ^ d2 2 CIg (* n R)I = fd1 2 Delta I j ]fd2 j (d1; d2) 2 RI g * ng (^ n R)I = fd1 2 Delta I j ]fd2 j (d1; d2) 2 RI g ^ ng (P1 u Delta Delta Delta u Pk)I = P I1 " Delta Delta Delta " P Ik 2.2 Knowledge Bases A knowledge base built by means of concept languages is generally formed by two components: The intensional one, called TBox, and the extensional one, called 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. Syntactically, such properties are expressed in terms of what we call inclusion statements. An inclusion 113 Buchheit, Donini, & Schaerf statement (or simply inclusion) has the form C v D where C and D are two arbitrary ALCN R-concepts. Intuitively, the statement specifies that every instance of C is also an instance of D. More precisely, an interpretation I satisfies the inclusion C v D if CI ` DI . A TBox is a finite set of inclusions. An interpretation I is a model for a TBox T if I satisfies all inclusions in T . In general, TKRSs provide the user with mechanisms for stating concept introductions (e.g., Nebel, 1990, Section 3.2) of the form A := D (concept definition, interpreted as set equality), or A .^ D (concept specification, 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 introduction is allowed, and that no terminological cycles are allowed, i.e., no concept name may occur--neither directly nor indirectly--within its own introduction. These restrictions make it possible to substitute an occurrence of a defined concept by its definition. We do not impose any of these restrictions to the form of inclusions, obtaining statements that are syntactically more expressive than concept introductions. In particular, a definition of the form A := D can be expressed in our system using the pair of inclusions A v D and D v A and a specification of the form A .^ D can be simply expressed by A v D. Conversely, an inclusion of the form C v D, where C and D are arbitrary concepts, cannot be expressed with concept introductions. Moreover, cyclic inclusions are allowed in our statements, realizing terminological cycles. As shown in (Nebel, 1991), there are at least three types of semantics for terminological cycles, namely the least fixpoint, the greatest fixpoint, and the descriptive semantics. Fixpoint semantics choose particular models among the set of interpretations that satisfy a statement of the form A := D. Such models are chosen as the least and the greatest fixpoint of the above equation. The descriptive semantics instead considers all interpretations that satisfy the statement (i.e., all fixpoints) as its models. However, fixpoint semantics naturally apply only to fixpoint statements like A := D, where D is a "function" of A, i.e., A may appear in D, and there is no obvious way to extend them to general inclusions. In addition, since our language includes the constructor for complement of general concepts, the "function" D may be not monotone, and therefore the least and the greatest fixpoints may be not unique. Whether there exists or not a definitional semantics that is suitable for cyclic definitions in expressive languages is still unclear. Conversely, the descriptive semantics interprets statements as just restricting the set of possible models, with no definitional import. Although it is not completely satisfactory in all practical cases (Baader, 1990b; Nebel, 1991), the descriptive semantics has been considered to be the most appropriate one for general cyclic statements in powerful concept languages. Hence, it seems to be the most suitable to be extended to our case and it is exactly the one we have adopted above. Observe that our decision to put general inclusions in the TBox is not a standard one. In fact, in TKRS like krypton such statements were put in the ABox. However, we conceive 114 Decidable Reasoning in Terminological KR Systems inclusions as a generalization of traditional TBox statements: acyclic concept introductions, with their definitional import, can be perfectly expressed with inclusions; and cyclic concept introductions can be expressed as well, if descriptive semantics is adopted. Therefore, we believe that inclusions should be part of the TBox. Notice that role conjunction allows one to express the practical feature of subroles. For example, the role ADOPTEDCHILD can be written as CHILDu ADOPTEDCHILD0, where ADOPTEDCHILD' is a role name, making it a subrole of CHILD. Following such idea, every hierarchy of role names can be rephrased with a set of role conjunctions, and vice versa. Actual systems usually provide for the construction of hierarchies of roles by means of role introductions (i.e., statements of the form P := R and P .^ R) in the TBox. However, in our simple language for roles, cyclic definitions of roles can be always reduced to acyclic definitions, as explained in (Nebel, 1990, Sec.5.3.1). When role definitions are acyclic, one can always substitute in every concept each role name with its definition, obtaining an equivalent concept. Therefore, we do not consider role definitions in this paper, and we conceive the TBox just as a set of concept inclusions. Even so, it is worth to notice that concept inclusions can express knowledge about roles. In particular, domain and range restrictions of roles can be expressed, in a way similar to the one in (Catarci & Lenzerini, 1993). Restricting the domain of a role R to a concept C and its range to a concept D can be done by the two inclusions 9R.? v C; ? v 8R.D It is straightforward to show that if an interpretation I satisfies the two inclusions, then RI ` CI Theta DI . Combining subroles with domain and range restrictions it is also possible to partially express the constructor for role restriction, which is present in various proposals (e.g., the language F L in Brachman & Levesque, 1984). Role restriction, written as R : C, is defined by (R : C)I = f(d1; d2) 2 Delta I Theta Delta I j (d1; d2) 2 RI ^ d2 2 CIg. For example the role DAUGHTER, which can be formulated as CHILD:Female, can be partially simulated by CHILD u DAUGHTER0, with the inclusion ? v 8DAUGHTER0.Female. However, this simulation would not be complete in number restrictions: E.g., if a mother has at least three daughters, then we know she has at least three female children; if instead we know that she has three female children we cannot infer that she has three daughters. We can now turn our attention to the extensional level, 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. Let O be an alphabet of symbols, called individuals. Instance-of relationships are expressed in terms of membership assertions of the form: C(a); R(a; b); where a and b are individuals, C is an ALCN R-concept, and R is an ALCN R-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. 115 Buchheit, Donini, & Schaerf In order to assign a meaning to membership assertions, the extension function Delta I of an interpretation I is extended to individuals by mapping them to elements of Delta I in such a way that aI 6= bI if a 6= b. This property is called Unique Name Assumption; it ensures that different individuals are interpreted as different objects. An interpretation I satisfies the assertion C(a) if aI 2 CI, and satisfies R(a; b) if (aI; bI) 2 RI . An ABox is a finite set of membership assertions. I is a model for an ABox A if I satisfies all the assertions in A. An ALCN R-knowledge base Sigma is a pair Sigma = hT ; Ai where T is a TBox and A is an ABox. An interpretation I is a model for Sigma if it is both a model for T and a model for A. We can now formally define the problems 1-4 mentioned in the introduction. Let Sigma be an ALCN R-knowledge base. 1. KB-satisfiability : Sigma is satisfiable, if it has a model; 2. Concept Satisfiability : C is satisfiable w.r.t Sigma , if there exists a model I of Sigma such that CI 6= ;; 3. Subsumption : C is subsumed by D w.r.t. Sigma , if CI ` DI for every model I of Sigma ; 4. Instance Checking : a is an instance of C, written Sigma j= C(a), if the assertion C(a) is satisfied in every model of Sigma . In (Nebel, 1990, Sec.3.3.2) it is shown that the ABox plays no active role when checking concept satisfiability and subsumption. In particular, Nebel shows that the ABox (subject to its satisfiability) can be replaced by an empty one without affecting the result of those services. Actually, in (Nebel, 1990), the above property is stated for a language less expressive than ALCN R. However, it is easy to show that it extends to ALCN R. It is important to remark that such a property is not valid for all concept languages. In fact, there are languages that include some constructors that refer to the individuals in the concept language, e.g., the constructor one-of (Borgida et al., 1989) that forms a concept from a set of enumerated individuals. If a concept language includes such a constructor the individuals in the TBox can interact with the individuals in the ABox, as shown in (Schaerf, 1993b). As a consequence, both concept satisfiability and subsumption depend also on the ABox. Example 2.1 Consider the following knowledge base Sigma = hT ; Ai: T = f9TEACHES.Course v (Student u 9DEGREE.BS) t Prof; Prof v 9DEGREE.MS; 9DEGREE.MS v 9DEGREE.BS; MS u BS v ?g A = fTEACHES(john; cs156); (^ 1 DEGREE)(john); Course(cs156)g Sigma is a fragment of a hypothetical knowledge base describing the organization of a university. The first inclusion, for instance, states that the persons teaching a course are either graduate students (students with a BS degree) or professors. It is easy to see that Sigma is satisfiable. For example, the following interpretation I satisfies all the inclusions in T and all the assertions 116 Decidable Reasoning in Terminological KR Systems in A, and therefore it is a model for Sigma : Delta I = fjohn; cs156; csbg; johnI = john; cs156I = cs156 StudentI = fjohng; ProfI = ;; CourseI = fcs156g; BSI = fcsbg MSI = ;; TEACHESI = f(john; cs156)g; DEGREEI = f(john; csb)g We have described the interpretation I by giving only Delta I, and the values of I on concept names and role names. It is straightforward to see that all values of I on complex concepts and roles are uniquely determined by imposing that I must satisfy the Equations 1 on page 113. Notice that it is possible to draw several non-trivial conclusions from Sigma . For example, we can infer that Sigma j= 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. Given the previous semantics, the problems 1-4 can all be reduced to KB-satisfiability (or to its complement) in linear time. In fact, given a knowledge base Sigma = hT ; Ai, two concepts C and D, an individual a, and an individual b not appearing in Sigma , the following equivalences hold: C is satisfiable w:r:t Sigma iff hT ; A [ fC(b)gi is satisfiable: C is subsumed by D w:r:t: Sigma iff hT ; A [ f(C u :D)(b)gi is not satisfiable: Sigma j= C(a) iff hT ; A [ f(:C)(a)gi is not satisfiable: A slightly different form of these equivalences has been given in (Hollunder, 1990). The equivalences given here are a straightforward consequence of the ones given by Hollunder. However, the above equivalences are not valid for languages including constructors that refer to the individuals in the concept language. The equivalences between reasoning services in such languages are studied in (Schaerf, 1993b). Based on the above equivalences, in the next section we concentrate just on KBsatisfiability. 3. Decidability Result In this section we provide a calculus for deciding KB-satisfiability. In particular, in Subsection 3.1 we present the calculus and we state its correctness. Then, in Subsection 3.2, we prove the termination of the calculus. This will be sufficient to assess the decidability of all problems 1-4, thanks to the relationships between the four problems. 3.1 The calculus and its correctness Our method makes use of the notion of constraint system (Donini et al., 1991a; SchmidtSchauss & Smolka, 1991; Donini, Lenzerini, Nardi, & Schaerf, 1991c), and is based on a tableaux-like calculus (Fitting, 1990) that tries to build a model for the logical formula corresponding to a KB. 117 Buchheit, Donini, & Schaerf We introduce an alphabet of variable symbols V together with a well-founded total ordering `OE' on V. The alphabet V is disjoint from the other ones defined so far. The purpose of the ordering will become clear later. The elements of V are denoted by the letters x; y; z; w. From this point on, we use the term object as an abstraction for individual and variable (i.e., an object is an element of O [ V). Objects are denoted by the symbols s; t and, as in Section 2, individuals are denoted by a; b. A constraint is a syntactic entity of one of the forms: s: C; sP t; 8x.x: C; s 6 := t; where C is a concept and P is a role name. Concepts are assumed to be simple, i.e., the only complements they contain are of the form :A, where A is a concept name. Arbitrary ALCN R-concepts can be rewritten into equivalent simple concepts in linear time (Donini et al., 1991a). A constraint system is a finite nonempty set of constraints. Given an interpretation I, we define an I-assignment ff as a function that maps every variable of V to an element of Delta I, and every individual a to aI (i.e., ff(a) = aI for all a 2 O). A pair (I; ff) satisfies the constraint s: C if ff(s) 2 CI , the constraint sP t if (ff(s); ff(t)) 2 P I , the constraint s 6 := t if ff(s) 6= ff(t), and finally, the constraint 8x.x: C if CI = Delta I (notice that ff does not play any role in this case). A constraint system S is satisfiable if there is a pair (I; ff) that satisfies every constraint in S. An ALCN R-knowledge base Sigma = hT ; Ai can be translated into a constraint system SSigma by replacing every inclusion C v D 2 T with the constraint 8x.x: :C t D, every membership assertion C(a) with the constraint a: C, every R(a; b) with the constraints aP1b; : : :; aPkb if R = P1 u : : : u Pk, and including the constraint a 6 := b for every pair (a; b) of individuals appearing in A. It is easy to see that Sigma is satisfiable if and only if SSigma is satisfiable. In order to check a constraint system S for satisfiability, 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 of so-called propagation rules. Before providing the rules, we need some additional definitions. Let S be a constraint system and R = P1 u : : : u Pk (k * 1) be a role. We say that t is an R-successor of s in S if sP1t; : : : ; sPkt are in S. We say that t is a direct successor of s in S if for some role R, t is an R-successor of s. We call direct predecessor the inverse relation of direct successor. If S is clear from the context we omit it. Moreover, we denote by successor the transitive closure of the relation direct successor, and we denote by predecessor its inverse. We assume that variables are introduced in a constraint system according to the ordering `OE'. This means, if y is introduced in a constraint system S then x OE y for all variables x that are already in S. We denote by S[x=s] the constraint system obtained from S by replacing each occurrence of the variable x by the object s. We say that s and t are separated in S if the constraint s 6 := t is in S. Given a constraint system S and an object s, we define the function oe(Delta ; Delta ) as follows: oe(S; s) := fC j s: C 2 Sg. Moreover, we say that two variables x and y are S-equivalent, 118 Decidable Reasoning in Terminological KR Systems written x js y, if oe(S; x) = oe(S; y). Intuitively, two S-equivalent variables can represent the same element in the potential interpretation built by the rules, unless they are separated. The propagation rules are: 1. S !u fs: C1; s: C2g [ S if 1. s: C1 u C2 is in S, 2. s: C1 and s: C2 are not both in S 2. S !t fs: Dg [ S if 1. s: C1 t C2 is in S, 2. neither s: C1 nor s: C2 is in S, 3. D = C1 or D = C2 3. S !8 ft: Cg [ S if 1. s: 8R.C is in S, 2. t is an R-successor of s, 3. t: C is not in S 4. S !9 fsP1y; : : : ; sPky; y: Cg [ S if 1. s: 9R.C is in S, 2. R = P1 u : : : u Pk, 3. y is a new variable, 4. there is no t such that t is an R-successor of s in S and t: C is in S, 5. if s is a variable there is no variable w such that w OE s and s js w 5. S !* fsP1yi; : : :; sPkyi j i 2 1::ng [ fyi 6 := yj j i; j 2 1::n; i 6= jg [ S if 1. s: (* n R) is in S, 2. R = P1 u : : : u Pk, 3. y1; : : : ; yn are new variables, 4. there do not exist n pairwise separated R-successors of s in S, 5. if s is a variable there is no variable w such that w OE s and s js w 6. S !^ S[y=t] if 1. s: (^ n R) is in S, 2. s has more than n R-successors in S, 3. y; t are two R-successors of s which are not separated 7. S !8x fs: Cg [ S if 1. 8x.x: C is in S, 2. s appears in S, 3. s: C is not in S. We call the rules !t and !^ nondeterministic rules, since they can be applied in different ways to the same constraint system (intuitively, they correspond to branching rules of tableaux). All the other rules are called deterministic rules. Moreover, we call the rules !9 and !* generating rules, since they introduce new variables in the constraint system. All other rules are called nongenerating ones. 119 Buchheit, Donini, & Schaerf The use of the condition based on the S-equivalence relation in the generating rules (condition 5) is related to the goal of keeping the constraint system finite even in presence of potentially infinite chains of applications of generating rules. Its role will become clearer later in the paper. One can verify that rules are always applied to a system S either because of the presence in S of a given constraint s: C (condition 1), or, in the case of the !8x-rule, because of the presence of an object s in S. When no confusion arises, we will say that a rule is applied to the constraint s: C or the object s (instead of saying that it is applied to the constraint system S). Proposition 3.1 (Invariance) Let S and S0 be constraint systems. Then: 1. If S0 is obtained from S by application of a deterministic rule, then S is satisfiable if and only if S0 is satisfiable. 2. If S0 is obtained from S by application of a nondeterministic rule, then S is satisfiable if S0 is satisfiable. Conversely, if S is satisfiable and a nondeterministic rule is applicable to an object s in S, then it can be applied to s in such a way that it yields a satisfiable constraint system. Proof. The proof is mainly a rephrasing of typical soundness proofs for tableaux methods (e.g., Fitting, 1990, Lemma 6.3.2). The only non-standard constructors are number restrictions. 1. "(" Considering the deterministic rules one can directly check that S is a subset of S0. So it is obvious that S is satisfiable if S0 is satisfiable. ")" In order to show that S0 is satisfiable if this is the case for S we consider in turn each possible deterministic rule application leading from S to S0. We assume that (I; ff) satisfies S. If the !u-rule is applied to s: C1 u C2 in S, then S0 = S [ fs: C1; s: C2g. Since (I; ff) satisfies s: C1 u C2, (I; ff) satisfies s: C1 and s: C2 and therefore S0. If the !8-rule is applied to s: 8R.C, there must be an R-successor t of s in S such that S0 = S [ft: Cg. Since (I; ff) satisfies S, it holds that (ff(s); ff(t)) 2 RI . Since (I; ff) satisfies s: 8R.C, it holds that ff(t) 2 CI . So (I; ff) satisfies t: C and therefore S0. If the !8x-rule is applied to an s because of the presence of 8x.x: C in S, then S0 = S [ fs: Cg. Since (I; ff) satisfies S it holds that CI = Delta I . Therefore ff(s) 2 CI and so (I; ff) satisfies S0. If the !9-rule is applied to s: 9R.C, then S0 = S [ fsP1y; : : :; sPky; y: Cg. Since (I; ff) satisfies S, there exists a d such that (ff(s); d) 2 RI and d 2 CI . We define the I-assignment ff0 as ff0(y) := d and ff0(t) := ff(t) for t 6= y. It is easy to show that (I; ff0) satisfies S0. If the !*-rule is applied to s: (* n R), then S0 = S [ fsP1yi; : : : ; sPkyi j i 2 1::ng [ fyi 6 := yj j i; j 2 1::n; i 6= jg. Since (I; ff) satisfies S, there exist n distinct elements d1; : : : ; dn 2 Delta I such that (ff(s); di) 2 RI. We define the I-assignment ff0 as ff0(yi) := di for i 2 1::n and ff0(t) := ff(t) for t 62 fy1; : : : ; yng. It is easy to show that (I; ff0) satisfies S0. 2. "(" Assume that S0 is satisfied by (I; ff0). We show that S is also satisfiable. If S0 is obtained from S by application of the !t-rule, then S is a subset of S0 and therefore satisfied by (I; ff0). 120 Decidable Reasoning in Terminological KR Systems If S0 is obtained from S by application of the !^-rule to s: (^ n R) in S, then there are y; t in S such that S0 = S[y=t]. We define the I-assignment ff as ff(y) := ff0(t) and ff(v) := ff0(v) for every object v with v 6= y. Obviously (I; ff) satisfies S. ")" Now suppose that S is satisfied by (I; ff) and a nondeterministic rule is applicable to an object s. If the !t-rule is applicable to s: C1 t C2 then, since S is satisfiable, ff(s) 2 (C1 t C2)I. It follows that either ff(s) 2 CI1 or ff(s) 2 CI2 (or both). Hence, the !t-rule can obviously be applied in a way such that (I; ff) satisfies the resulting constraint system S0. If the !^-rule is applicable to s: (^ n R), then--since (I; ff) satisfies S--it holds that ff(s) 2 (^ n R)I and therefore the set fd 2 Delta I j (ff(s); d) 2 RIg has at most n elements. On the other hand, there are more than n R-successors of s in S and for each R-successor t of s we have (ff(s); ff(t)) 2 RI. Thus, we can conclude by the Pigeonhole Principle (see e.g., Lewis & Papadimitriou, 1981, page 26) that there exist at least two R-successors t; t0 of s such that ff(t) = ff(t0). Since (I; ff) satisfies S, the constraint t 6 := t0 is not in S. Therefore one of the two must be a variable, let's say t0 = y. Now obviously (I; ff) satisfies S[y=t]. Given a constraint system S, more than one rule might be applicable to it. We define the following strategy for the application of rules: 1. apply a rule to a variable only if no rule is applicable to individuals; 2. apply a rule to a variable x only if no rule is applicable to a variable y such that y OE x; 3. apply generating rules only if no nongenerating rule is applicable. The above strategy ensures that the variables are processed one at a time according to the ordering `OE'. From this point on, we assume that rules are always applied according to this strategy and that we always start with a constraint system SSigma coming from an ALCN R-knowledge base Sigma . The following lemma is a direct consequence of these assumptions. Lemma 3.2 (Stability) Let S be a constraint system and x be a variable in S. Let a generating rule be applicable to x according to the strategy. Let S0 be any constraint system derivable from S by any sequence (possibly empty) of applications of rules. Then 1. No rule is applicable in S0 to a variable y with y OE x 2. oe(S; x) = oe(S0; x) 3. If y is a variable in S with y OE x then y is a variable in S0, i.e., the variable y is not substituted by another variable or by a constant. Proof. 1. By contradiction: Suppose S j S0 !Lambda S1 !Lambda Delta Delta Delta !Lambda Sn j S0, where Lambda 2 ft; u; 9; 8; *; ^; 8xg and a rule is applicable to a variable y such that y OE x in S0. Then there exists a minimal i, where i ^ n, such that this is the case in Si. Note that i 6= 0; in fact, because of the strategy, if a rule is applicable to x in S no rule is applicable to y in S. So no rule is applicable to any variable z such that z OE x in S0; : : : ; SiGamma 1. It follows that from SiGamma 1 to Si a rule is applied to x or to a variable w such that x OE w. By an exhaustive 121 Buchheit, Donini, & Schaerf analysis of all rules we see that--whichever is the rule applied from SiGamma 1 to Si--no new constraint of the form y: C or yRz can be added to SiGamma 1, and therefore no rule is applicable to y in Si, contradicting the assumption. 2. By contradiction: Suppose oe(S; x) 6= oe(S0; x). Call y the direct predecessor of x, then a rule must have been applied either to y or to x itself. Obviously we have y OE x, therefore the former case cannot be because of point 1. A case analysis shows that the only rules which can have been applied to x are generating ones and the !8 and the !^ rules. But these rules add new constraints only to the direct successors of x and not to x itself and therefore do not change oe(Delta ; x). 3. This follows from point 1. and the strategy. Lemma 3.2 proves that for a variable x which has a direct successor, oe(Delta ; x) is stable, i.e., it will not change because of subsequent applications of rules. In fact, if a variable has a direct successor it means that a generating rule has been applied to it, therefore (Lemma 3.2.2) from that point on oe(Delta ; x) does not change. 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: ffl fs: ?g ffl fs: A; s: :Ag, where A is a concept name. ffl fs: (^ n R)g [ fsP1ti; : : :; sPkti j i 2 1::n + 1g [ fti 6 := tj j i; j 2 1::n + 1; i 6= jg, where R = P1 u : : : u Pk. A clash is evidently an unsatisfiable constraint system. For example, the last case represents the situation in which an object has an at-most restriction and a set of Rsuccessors that cannot be identified (either because they are individuals or because they have been created by some at-least restrictions). Any constraint system containing a clash is obviously unsatisfiable. The purpose of the calculus is to generate completions, and look for the presence of clashes inside. If S is a completion of SSigma and S contains no clash, we prove that it is always possible to construct a model for Sigma on the basis of S. Before looking at the technical details of the proof, let us consider an example of application of the calculus for checking satisfiability. Example 3.3 Consider the following knowledge base Sigma = hT ; Ai: T = fItalian v 9FRIEND.Italiang A = fFRIEND(peter; susan); 8FRIEND.:Italian(peter); 9FRIEND.Italian(susan)g The corresponding constraint system SSigma is: SSigma = f8x.x: :Italian t 9FRIEND.Italian; peterFRIENDsusan; 122 Decidable Reasoning in Terminological KR Systems peter: 8FRIEND.:Italian; susan: 9FRIEND.Italian peter 6 := susang A sequence of applications of the propagation rules to SSigma is as follows: S1 = SSigma [ fsusan: :Italiang (!8-rule) S2 = S1 [ fpeter: :Italian t 9FRIEND.Italiang (!8x-rule) S3 = S2 [ fsusan: :Italian t 9FRIEND.Italiang (!8x-rule) S4 = S3 [ fpeter: :Italiang (!t-rule) S5 = S4 [ fsusanFRIENDx; x: Italiang (!9-rule) S6 = S5 [ fx: :Italian t 9FRIEND.Italiang (!8x-rule) S7 = S6 [ fx: 9FRIEND.Italiang (!t-rule) S8 = S7 [ fxFRIENDy; y: Italiang (!9-rule) S9 = S8 [ fy: :Italian t 9FRIEND.Italiang (!8x-rule) S10 = S9 [ fy: 9FRIEND.Italiang (!t-rule) One can verify that S10 is a complete clash-free constraint system. In particular, the !9- rule is not applicable to y. In fact, since x jS10 y condition 5 is not satisfied. From S10 one can build an interpretation I, as follows (again, we give only the interpretation of concept and role names): Delta I = fpeter; susan; x; yg peterI = peter, susanI = susan, ff(x) = x, ff(y) = y, ItalianI = fx; yg FRIENDI = f(peter; susan); (susan; x); (x; y); (y; y)g It is easy to see that I is indeed a model for Sigma . In order to prove that it is always possible to obtain an interpretation from a complete clash-free constraint system we need some additional notions. Let S be a constraint system and x, w variables in S. We call w a witness of x in S if the three following conditions hold: 1. x js w 2. w OE x 3. there is no variable z such that z OE w and z satisfies conditions 1. and 2., i.e., w is the least variable w.r.t. OE satisfying conditions 1. and 2. We say x is blocked (by w) in S if x has a witness (w) in S. The following lemma states a property of witnesses. Lemma 3.4 Let S be a constraint system, x a variable in S. If x is blocked then 1. x has no direct successor and 2. x has exactly one witness. 123 Buchheit, Donini, & Schaerf Proof. 1. By contradiction: Suppose that x is blocked in S and xP y is in S. During the completion process leading to S a generating rule must have been applied to x in a system S0. It follows from the definition of the rules that in S0 for every variable w OE x we had x6js0 w. Now from Lemma 3.2 we know, that for the constraint system S derivable from S0 and for every w OE x in S we also have x6jsw. Hence there is no witness for x in S, contradicting the hypothesis that x is blocked. 2. This follows directly from condition 3. for a witness. As a consequence of Lemma 3.4, in a constraint system S, if w1 is a witness of x then w1 cannot have a witness itself, since both the relations `OE' and S-equivalence are transitive. The uniqueness of the witness for a blocked variable is important for defining the following particular interpretation out of S. Let S be a constraint system. We define the canonical interpretation IS and the canonical IS-assignment ffS as follows: 1. Delta IS := fs j s is an object in Sg 2. ffS(s) := s 3. s 2 AIS if and only if s: A is in S 4. (s; t) 2 P IS if and only if (a) sP t is in S or (b) s is a blocked variable, w is the witness of s in S and wP t is in S. We call (s; t) a P-role-pair of s in IS if (s; t) 2 P IS , we call (s; t) a role-pair of s in IS if (s; t) is a P-role-pair for some role P . We call a role-pair explicit if it comes up from case 4.(a) of the definition of the canonical interpretation and we call it implicit if it comes up from case 4.(b). From Lemma 3.4 it is obvious that a role-pair cannot be both explicit and implicit. Moreover, if a variable has an implicit role-pair then all its role-pairs are implicit and they all come from exactly one witness, as stated by the following lemma. Lemma 3.5 Let S be a completion and x a variable in S. Let IS be the canonical interpretation for S. If x has an implicit role-pair (x; y), then 1. all role-pairs of x in IS are implicit 2. there is exactly one witness w of x in S such that for all roles P in S and all P -rolepairs (x,y) of x, the constraint wP y is in S. Proof. The first statement follows from Lemma 3.4 (point 1 ). The second statement follows from Lemma 3.4 (point 2 ) together with the definition of IS. We have now all the machinery needed to prove the main theorem of this subsection. Theorem 3.6 Let S be a complete constraint system. If S contains no clash then it is satisfiable. 124 Decidable Reasoning in Terminological KR Systems Proof. Let IS and ffS be the canonical interpretation and canonical I-assignment for S. We prove that the pair (IS; ffS) satisfies every constraint c in S. If c has the form sP t or s 6 := t, then (IS; ffS) satisfies them by definition of IS and ffS . Considering the !*-rule and the !^-rule we see that a constraint of the form s 6 := s can not be in S. If c has the form s: C, we show by induction on the structure of C that s 2 CIS . We first consider the base cases. If C is a concept name, then s 2 CIS by definition of IS. If C = ?, then obviously s 2 ?IS . The case that C = ? cannot occur since S is clash-free. Next we analyze in turn each possible complex concept C. If C is of the form :C1 then C1 is a concept name since all concepts are simple. Then the constraint s: C1 is not in S since S is clash-free. Then s 62 CIS1 , that is, s 2 Delta IS n CIS1 . Hence s 2 (:C1)IS . If C is of the form C1 u C2 then (since S is complete) s: C1 is in S and s: C2 is in S. By induction hypothesis, s 2 CIS1 and s 2 CIS2 . Hence s 2 (C1 u C2)IS . If C is of the form C1 t C2 then (since S is complete) either s: C1 is in S or s: C2 is in S. By induction hypothesis, either s 2 CIS1 or s 2 CIS2 . Hence s 2 (C1 t C2)IS . If C is of the form 8R.D, we have to show that for all t with (s; t) 2 RIS it holds that t 2 DIS . If (s; t) 2 RIS , then according to Lemma 3.5 two cases can occur. Either t is an R-successor of s in S or s is blocked by a witness w in S and t is an R-successor of w in S. In the first case t: D must also be in S since S is complete. Then by induction hypothesis we have t 2 DIS . In the second case by definition of witness, w: 8R.D is in S and then because of completeness of S, t: D must be in S. By induction hypothesis we have again t 2 DIS . If C is of the form 9R.D we have to show that there exists a t 2 Delta IS with (s; t) 2 RIS and t 2 DIS . Since S is complete, either there is a t that is an R-successor of s in S and t: D is in S, or s is a variable blocked by a witness w in S. In the first case, by induction hypothesis and the definition of IS, we have t 2 DIS and (s; t) 2 RIS . In the second case w: 9R.D is in S. Since w cannot be blocked and S is complete, we have that there is a t that is an R-successor of w in S and t: D is in S. So by induction hypothesis we have t 2 DIS and by the definition of IS we have (s; t) 2 RIS . If C is of the form (^ n R) we show the goal by contradiction. Assume that s 62 (^ n R)IS . Then there exist atleast n + 1 distinct objects t1; : : :; tn+1 with (s; ti) 2 RIS ; i 2 1::n + 1. This means that, since R = P1 u : : : u Pk, there are pairs (s; ti) 2 P ISj , where i 2 1::n + 1 and j 2 1::k. Then according to Lemma 3.5 one of the two following cases must occur. Either all sPj ti for j 2 1::k; i 2 1::n + 1 are in S or there exists a witness w of s in S with all wPiti for j 2 1::k and i 2 1::n + 1 are in S. In the first case the !^-rule can not be applicable because of completeness. This means that all the ti's are pairwise separated, i.e., that S contains the constraints ti 6 := tj ; i; j 2 1::n + 1; i 6= j. This contradicts the fact that S is clash-free. And the second case leads to an analogous contradiction. If C is of the form (* n R) we show the goal by contradiction. Assume that s 62 (* n R)IS . Then there exist atmost m ! n (m possibly 0) distinct objects t1; : : : ; tm with (s; ti) 2 RIS ; i 2 1::m. We have to consider two cases. First case: s is not blocked in S. Since there are only m R-successors of s in S, the !*-rule is applicable to s. This contradicts the fact that S is complete. Second case: s is blocked by a witness w in S. Since there are m R-successors of w in S, the !*-rule is applicable to w. But this leads to the same contradiction. 125 Buchheit, Donini, & Schaerf If c has the form 8x.x: D then, since S is complete, for each object t in S, t: D is in S--and, by the previous cases, t 2 DIS . Therefore, the pair (IS; ffS) satisfies 8x.x: D. Finally, since (IS; ffS) satisfies all constraints in S, (IS; ffS) satisfies S. Theorem 3.7 (Correctness) A constraint system S is satisfiable if and only if there exists at least one clash-free completion of S. Proof. "(" Follows immediately from Theorem 3.6. ")" Clearly, a system containing a clash is unsatisfiable. If every completion of S is unsatisfiable, then from Proposition 3.1 S, is unsatisfiable. 3.2 Termination and complexity of the calculus Given a constraint system S, we call nS the number of concepts appearing in S, including also all the concepts appearing as a substring of another concept. Notice that nS is bounded by the length of the string expressing S. Lemma 3.8 Let S be a constraint system and let S0 be derived from S by means of the propagation rules. In any set of variables in S0 including more than 2nS variables there are at least two variables x,y such that x js0 y. Proof. Each constraint x: C 2 S0 may contain only concepts of the constraint system S. Since there are nS such concepts, given a variable x there cannot be more than 2nS different sets of constraints x: C in S0. Lemma 3.9 Let S be a constraint system and let S0 be any constraint system derived from S by applying the propagation rules with the given strategy. Then, in S0 there are at most 2nS non-blocked variables. Proof. Suppose there are 2nS + 1 non-blocked variables. From Lemma 3.8, we know that in S0 there are at least two variables y1, y2 such that y1 js y2. Obviously either y1 OE y2 or y2 OE y1 holds; suppose that y1 OE y2. From the definitions of witness and blocked either y1 is a witness of y2 or there exists a variable y3 such that y3 OE y1 and y3 is a witness of y2. In both cases y2 is blocked, contradicting the hypothesis. Theorem 3.10 (Termination and space complexity) Let Sigma be an ALCN R-knowledge base and let n be its size. Every completion of SSigma is finite and its size is O(24n). Proof. Let S be a completion of SSigma . From Lemma 3.9 it follows that there are at most 2n non-blocked variables in S. Therefore there are at most m Theta 2n total variables in S, where m is the maximum number of direct successors for a variable in S. Observe that m is bounded by the number of 9R.C concepts (at most n) plus the sum of all numbers appearing in number restrictions. Since these numbers are expressed in binary, their sum is bounded by 2n. Hence, m ^ 2n + n. Since the number of individuals is also bounded by n, the total number of objects in S is at most mTheta (2n +n) ^ (2n +n)Theta (2n +n), that is, O(22n). 126 Decidable Reasoning in Terminological KR Systems The number of different constraints of the form s: C, 8x.x: C in which each object s can be involved is bounded by n, and each constraint has size linear in n. Hence, the total size of these constraints is bounded by n Theta n Theta 22n, that is O(23n). The number of constraints of the form sP t, s 6 := t is bounded by (22n)2 = 24n, and each constraint has constant size. In conclusion, we have that the size of S is O(24n). Notice that the above one is just a coarse upper bound, obtained for theoretical purposes. In practical cases we expect the actual size to be much smaller than that. For example, if the numbers involved in number restrictions were either expressed in unary notation, or limited by a constant (the latter being a reasonable restriction in practical systems) then an argumentation analogous to the above one would lead to a bound of 23n. Theorem 3.11 (Decidability) Given an ALCN R-knowledge base Sigma , checking whether Sigma is satisfiable is a decidable problem. Proof. This follows from Theorems 3.7 and 3.10 and the fact that Sigma is satisfiable if and only if SSigma is satisfiable. We can refine the above theorem, by giving tighter bounds on the time required to decide satisfiability. Theorem 3.12 (Time complexity) Given an ALCN R-knowledge base Sigma , checking whether Sigma is satisfiable can be done in nondeterministic exponential time. Proof. In order to prove the claim it is sufficient to show that each completion is obtained with an exponential number of applications of rules. Since the number of constraints of each completion is exponential (Theorem 3.10) and each rule, but the !^-rule, adds new constraints to the constraint system, it follows that all such rules are applied at most an exponential number of times. Regarding the !^-rule, it is applied for each object at most as many times as the number of its direct successors. Since such number is at most exponential (if numbers are coded in binary) w.r.t. the size of the knowledge base, the claim follows. A lower bound of the complexity of KB-satisfiability is obtained exploiting previous results about the language ALC, which is a sublanguage of ALCN R that does not include number restrictions and role conjunction. We know from McAllester (1991), and (independently) from an observation by Nutt (1992) that KB-satisfiability in ALC-knowledge bases is EXPTIME-hard (see (Garey & Johnson, 1979, page 183) for a definition) and hence it is hard for ALCN R-knowledge bases, too. Hence, we do not expect to find any algorithm solving the problem in polynomial space, unless PSPACE=EXPTIME. Therefore, we do not expect to substantially improve space complexity of our calculus, which already works in exponential space. We now discuss possible improvements on time complexity. The proposed calculus works in nondeterministic exponential time, and hence improves the one we proposed in (Buchheit, Donini, & Schaerf, 1993, Sec.4), which works in deterministic double exponential time. The key improvement is that we showed that a KB has a model if and only if it has a model of exponential size. However, it may be argued that as it is, the calculus cannot yet be turned into a practical procedure, since such a procedure would simply simulate nondeterminism by a second level of exponentiality, resulting 127 Buchheit, Donini, & Schaerf in a double exponential time procedure. However, the different combinations of concepts are only exponentially many (this is just the cardinality of the powerset of the set of concepts). Hence, a double exponential time procedure wastes most of the time re-analyzing over and over objects with different names yet with the same oe(Delta ; Delta ), in different constraint systems. This could be avoided if we allow a variable to be blocked by a witness that is in a previously analyzed constraint system. This technique would be similar to the one used in (Pratt, 1978), and to the tree-automata technique used in (Vardi & Wolper, 1986), improving on simple tableaux methods for variants of propositional dynamic logics. Since our calculus considers only one constraint system at a time, a modification of the calculus would be necessary to accomplish this task in a formal way, which is outside the scope of this paper. The formal development of such a deterministic exponential time procedure will be a subject for future research. Notice that, since the domain of the canonical interpretation Delta IS is always finite, we have also implicitly proved that ALCN R-knowledge bases have the finite model property, i.e., any satisfiable knowledge base has a finite model. This property has been extensively studied in modal logics (Hughes & Cresswell, 1984) and dynamic logics (Harel, 1984). In particular, a technique, called filtration, has been developed both to prove the finite model property and to build a finite model for a satisfiable formula. This technique allows one to build a finite model from an infinite one by grouping the worlds of a structure in equivalence classes, based on the set of formulae that are satisfied in each world. It is interesting to observe that our calculus, based on witnesses, can be considered as a variant of the filtration technique where the equivalence classes are determined on the basis of our S-equivalence relation. However, because of number restrictions, variables that are S-equivalent cannot be grouped, since they might be separated (e.g., they might have been introduced by the same application of the !*-rule). Nevertheless, they can have the same direct successors, as stated in point 4.(b) of the definition of canonical interpretation on page 124. This would correspond to grouping variables of an infinite model in such a way that separations are preserved. 4. Relation to previous work In this section we discuss the relation of our paper to previous work about reasoning with inclusions. In particular, we first consider previously proposed reasoning techniques that deal with inclusions and terminological cycles, then we discuss the relation between inclusions and terminological cycles. 4.1 Reasoning Techniques As mentioned in the introduction, previous results were obtained by Baader et al. (1990), Baader (1990a, 1990b), Nebel (1990, 1991), Schild (1991) and Dionne et al. (1992, 1993). Nebel (1990, Chapter 5) considers the language T F , containing concept conjunction, universal quantification and number restrictions, and TBoxes containing (possibly cyclic) concept definitions, role definitions and disjointness axioms (stating that two concept names are disjoint). Nebel shows that subsumption of T F-concepts w.r.t. a TBox is decidable. However, the argument he uses is non-constructive: He shows that it is sufficient to con128 Decidable Reasoning in Terminological KR Systems sider finite interpretations of a size bounded by the size of the TBox in order to decide subsumption. In (Baader, 1990b) the effect of the three types of semantics--descriptive, greatest fixpoint and least fixpoint semantics--for the language F L0, containing concept conjunction and universal quantification, is described with the help of finite automata. Baader reduces subsumption of F L0-concepts w.r.t. a TBox containing (possibly cyclic) definitions of the form A := C (which he calls terminological axioms) to decision problems for finite automata. In particular, he shows that subsumption w.r.t. descriptive semantics can be decided in polynomial space using B"uchi automata. Using results from (Baader, 1990b), in (Nebel, 1991) a characterization of the above subsumption problem w.r.t. descriptive semantics is given with the help of deterministic automata (whereas B"uchi automata are nondeterministic). This also yields a PSPACE-algorithm for deciding subsumption. In (Baader et al., 1990) the attention is restricted to the language ALC. In particular, that paper considers the problem of checking the satisfiability of a single equation of the form C = ?, where C is an ALC-concept. This problem, called the universal satisfiability problem, is shown to be equivalent to checking the satisfiability of an ALC-TBox (see Proposition 4.1). In (Baader, 1990a), an extension of ALC, called ALCreg, is introduced, which supports a constructor to express the transitive closure of roles. By means of transitive closure of roles it is possible to replace cyclic inclusions of the form A v D with equivalent acyclic ones. The problem of checking the satisfiability of an ALCreg-concept is solved in that paper. It is also shown that using transitive closure it is possible to reduce satisfiability of an ALC-concept w.r.t. an ALC-TBox T = fC1 v D1; : : : ; Cn v Dng into the concept satisfiability problem in ALCreg (w.r.t. the empty TBox). Since the problem of concept satisfiability w.r.t. a TBox is trivially harder than checking the satisfiability of a TBox, that paper extends the result given in (Baader et al., 1990). The technique exploited in (Baader et al., 1990) and (Baader, 1990a) is based on the notion of concept tree. A concept tree is generated starting from a concept C in order to check its satisfiability (or universal satisfiability). The way a concept tree is generated from a concept C is similar in flavor to the way a complete constraint system is generated from the constraint system fx: Cg. However, the extension of the concept tree method to deal with number restrictions and individuals in the knowledge base is neither obvious, nor suggested in the cited papers; on the other hand, the extension of the calculus based on constraint systems is immediate, provided that additional features have a counterpart in First Order Logic. In (Schild, 1991) some results more general than those in (Baader, 1990a) are obtained by considering languages more expressive than ALCreg and dealing with the concept satisfiability problem in such languages. The results are obtained by establishing a correspondence between concept languages and Propositional Dynamic Logics (PDL), and reducing the given problem to a satisfiability problem in PDL. Such an approach allows Schild to find several new results exploiting known results in the PDL framework. However, it cannot be used to deal with every concept language. In fact, the correspondence cannot be established when the language includes some concept constructors having no counterpart in PDL (e.g., number restrictions, or individuals in an ABox). 129 Buchheit, Donini, & Schaerf Recently, an algebraic approach to cycles has been proposed in (Dionne et al., 1992), in which (possibly cyclic) definitions are interpreted as determining an equivalence relation over the terms describing concepts. The existence and uniqueness of such an equivalence relation derives from Aczel's results on non-well founded sets. In (Dionne et al., 1993) the same researchers prove that subsumption based on this approach is equivalent to subsumption in greatest fixpoint semantics. The language analyzed is a small fragment of the one used in the TKRS k-rep, and contains conjunction and existential-universal quantifications combined into one construct (hence it is similar to F L0). The difficulty of extending these results lies in the fact that it is not clear how individuals can be interpreted in this algebraic setting. Moreover, we believe that constructive approaches like the algebraic one, give counterintuitive results when applied to non-constructive features of concept languages--as negation and number restrictions. In conclusion, all these approaches, i.e., reduction to automata problems, concept trees, reduction to PDL and algebraic semantics, deal only with TBoxes and they don't seem to be suitable to deal also with ABoxes. On the other hand, the constraint system technique, even though it was conceived for TBox-reasoning, can be easily extended to ABox-reasoning, as also shown in (Hollunder, 1990; Baader & Hollunder, 1991; Donini et al., 1993). 4.2 Inclusions versus Concept Definitions Now we compare the expressive power of TBoxes defined as a set of inclusions (as done in this paper) and TBoxes defined as a set of (possibly cyclic) concept introductions of the form A .^ D and A := D. Unlike (Baader, 1990a) and (Schild, 1991), we consider reasoning problems dealing with TBox and ABox together. Moreover, we use the descriptive semantics for the concept introductions, as we do for inclusions. The result we have obtained is that inclusion statements and concept introductions actually have the same expressive power. In detail, we show that the satisfiability of a knowledge base Sigma = hA; T i, where T is a set of inclusion statements, can be reduced to the satisfiability of a knowledge base Sigma 0 = hA0; T 0i such that T 0 is a set of concept introductions. The other direction, from concept introductions to inclusions, is trivial since introductions of the form A := D can be expressed by the pair of inclusions A v D and D v A, while a concept name specification A .^ D can be rewritten as the inclusion A v D (as already mentioned in Section 2). As a notation, given a TBox T = fC1 v D1; : : : ; Cn v Dng, we define the concept CT as CT = (:C1 t D1) u Delta Delta Delta u (:Cn t Dn). As pointed out in (Baader, 1990a) for ALC, an interpretation satisfies a TBox T if and only if it satisfies the equation CT = ?. This result easily extends to ALCN R, as stated in the following proposition. Proposition 4.1 Given an ALCN R-TBox T = fC1 v D1; : : :; Cn v Dng, an interpretation I satisfies T if and only if it satisfies the equation CT = ?. Proof. An interpretation I satisfies an inclusion C v D if and only if it satisfies the equation :C t D = ?; I satisfies the set of equations :C1 t D1 = ?,: : : , :Cn t Dn = ? if and only if I satisfies (:C1 t D1) u Delta Delta Delta u (:Cn t Dn) = ?. The claim follows. 130 Decidable Reasoning in Terminological KR Systems Given a knowledge base Sigma = hA; T i and a concept A not appearing in Sigma , we define the knowledge base Sigma 0 = hA0; T 0i as follows: A0 = A [ fA(b) j b is an individual in Sigma g T 0 = fA .^ CT u 8P1.A u Delta Delta Delta u 8Pn.Ag where P1; P2; : : :; Pn are all the role names appearing in Sigma . Note that T 0 has a single inclusion, which could be also thought of as one primitive concept specification. Theorem 4.2 Sigma = hA; T i is satisfiable if and only if Sigma 0 = hA0; T 0i is satisfiable. Proof. In order to simplify the machinery of the proof, we will use for T 0 the following (logically equivalent) form: T 0 = fA v CT ; A v 8P1.A; : : :; A v 8Pn.Ag (Note that we use the symbol `v' instead of ` .^' because now the concept name A appears as the left-hand side of many statements, we must consider these statements as inclusions). ")" Suppose Sigma = hA; T i satisfiable. From Theorem 3.7, there exists a complete constraint system S without clash, which defines a canonical interpretation IS which is a model of Sigma . Define the constraint system S0 as follows: S0 = S [ fw: A j w is an object in Sg and call IS0 the canonical interpretation associated to S0. We prove that IS0 is a model of Sigma 0. First observe that every assertion in A is satisfied by IS0 since IS0 is equal to IS except for the interpretation of A, and A does not appear in A. Therefore, every assertion in A0 is also satisfied by IS0, either because it is an assertion of A, or (if it is an assertion of the form A(b)) by definition of S0. Regarding T 0, note that by definition of S0, we have AIS0 = Delta IS0 = Delta IS ; therefore both sides of the inclusions of the form A v 8Pi.A (i = 1; : : : ; n) are interpreted as Delta IS0 , hence they are satisfied by IS0 . Since A does not appear in CT , we have that (CT )IS0 = (CT )IS . Moreover, since IS satisfies T , we also have, by Proposition 4.1, that (CT )IS = Delta IS , therefore (CT )IS0 = (CT )IS = Delta IS = Delta IS0 . It follows that also both sides of the inclusion A v CT are interpreted as Delta IS0 . In conclusion, IS0 satisfies T 0. "(" Suppose Sigma 0 = hA0; T 0i satisfiable. Again, because of Theorem 3.7, there exists a complete constraint system S0 without clash, which defines a canonical interpretation IS0 which is a model of Sigma 0. We show that IS0 is also a model of Sigma . First of all, the assertions in A are satisfied because A ` A0, and IS0 satisfies every assertion in A0. To prove that IS0 satisfies T , we first prove the following equation: AIS 0 = Delta IS0 (2) Equation 2 is proved by showing that, for every object s 2 Delta IS0 , s is in AIS0 . In order to do that, observe a general property of constraint systems: Every variable in S0 is a successor of an individual. This comes from the definition of the generating rules, which add variables to the constraint system only as direct successors of existing objects, and at the beginning SSigma 0 contains only individuals. Then, Equation 2 is proved by observing the following three facts: 131 Buchheit, Donini, & Schaerf 1. for every individual b in Delta IS0 , b 2 AIS0 ; 2. if an object s is in AIS0 , then because IS0 satisfies the inclusions AIS0 ` (8P1.A)IS0 ; : : :; AIS0 ` (8Pn.A)IS0 , every direct successor of s is in AIS0 ; 3. the successor relation is closed under the direct successor relation From the Fundamental Theorem on Induction (see e.g., Wand, 1980, page 41) we conclude that every object s of Delta IS0 is in AIS0 . This proves that Equation 2 holds. From Equation 2, and the fact that IS0 satisfies the inclusion AIS0 ` (CT )IS0 , we derive that (CT )IS0 = Delta IS0 , that is IS0 satisfies the equation CT = ?. Hence, from Proposition 4.1, IS0 satisfies T , and this completes the proof of the theorem. The machinery present in this proof is not new. In fact, realizing that the inclusions A v 8P1.A; : : : ; A v 8Pn.A simulate a transitive closure on the roles P1; : : : ; Pn, one can recognize similarities with the proofs given by Schild (1991) and Baader (1990a). The difference is that their proofs rely on the notion of connected model (Baader uses the equivalent notion of rooted model). In contrast, the models we obtain are not connected, when the individuals in the knowledge base are not. What we exploit is the weaker property that every variable in the model is a successor of an individual. Note that the above reduction strongly relies on the fact that disjunction `t' and complement `:' are within the language. In fact, disjunction and complement are necessary in order to express all the inclusions of a TBox T inside the concept CT . Therefore, the proof holds for ALC-knowledge bases, but does not hold for TKRSs not allowing for these constructors of concepts (e.g., back). Furthermore, for the language F L0 introduced in Section 4.1, the opposite result holds. In fact, McAllester (1991) proves that computing subsumption w.r.t. a set of inclusions is EXPTIME-hard, even in the small language F L0. Conversely, Nebel (1991) proves that subsumption w.r.t. a set of cyclic definitions in F L0 can be done in PSPACE. Combining the two results, we can conclude that for F L0 subsumption w.r.t. a set of inclusions and subsumption w.r.t. a set of definitions are in different complexity classes, hence (assuming EXPTIME 6= PSPACE) inclusion statements are strictly more expressive than concept definitions in F L0. It is still open whether inclusions and definitions are equivalent in languages whose expressivity is between F L0 and ALC. 5. Discussion In this paper we have proved the decidability of the main inference services of a TKRS based on the concept language ALCN R. We believe that this result is not only of theoretical importance, but bears some impact on existing TKRSs, because a complete procedure can be easily devised from the calculus provided in Section 3. From this procedure, one can build more efficient (but still complete) ones, as described at the end of Section 3.2, and also by applying standard optimization techniques such as those described in (Baader, Hollunder, Nebel, Profitlich, & Franconi, 1992). An optimized procedure can perform well for small sublanguages where reasoning is tractable, while still being complete when solving more complex tasks. However, such a complete procedure will still take exponential time and 132 Decidable Reasoning in Terminological KR Systems space in the worst case, and it may be argued what could be its practical applicability. We comment in following on this point. Firstly, a complete procedure (possibly optimized) offers a benchmark for comparing incomplete procedures, not only in terms of performance, but also in terms of missed inferences. Let us illustrate this point in detail, by providing a blatant paradox: consider the mostly incomplete constant-time procedure, answering always "No" to any check. Obviously this useless procedure outperforms any other one, if missed inferences are not taken into account. This paradox shows that incomplete procedures can be meaningfully compared only if missed inferences are considered. But to recognize missed inferences over large examples, one needs exactly a complete procedure--even if not an efficient one--like ours. We believe that a fair detection of missed inferences would be of great help even when the satisfaction of end users is the primary criterion for judging incomplete procedures. Secondly, a complete procedure can be used for "anytime classification", as proposed in (MacGregor, 1992). The idea is to use a fast, but incomplete algorithm as a first step in analyzing the input knowledge, and then do more reasoning in background. In the cited paper, resolution-based theorem provers are proposed for performing this background reasoning. We argue that any specialized complete procedure will perform better than a general theorem prover. For instance, theorem provers are usually not specifically designed to deal with filtration techniques. Moreover, our calculus can be easily adapted to deal with rules. As outlined in the introduction, rules are often used in practical TKRSs. Rules behave like one-way concept inclusions--no contrapositive is allowed--and they are applied only to known individuals. Our result shows that rules in ALCN R can be applied also to unknown individuals (our variables in a constraint system) without endangering decidability. This result is to be compared with the negative result in (Baader & Hollunder, 1992), where it is shown that subsumption becomes undecidable if rules are applied to unknown individuals in classic. Finally, the calculus provides a new way of building incomplete procedures, by modifying some of the propagation rules. Since the rules build up a model, modifications to them have a semantical counterpart which gives a precise account of the incomplete procedures obtained. For example, one could limit the size of the canonical model by a polynomial in the size of the KB. Semantically, this would mean to consider only "small" models, which is reasonable when the intended models for the KB are not much bigger than the size of the KB itself. We believe that this way of designing incomplete procedures "from above", i.e., starting with the complete set of inferences and weakening it, is dual to the way incomplete procedures have been realized so far "from below", i.e., starting with already incomplete inferences and adding inference power by need. Further research is still needed to address problems issuing from practical systems. For example, to completely express role restrictions inside number restrictions, qualified number restrictions (Hollunder & Baader, 1991) should be taken into account. Also, the language resulting from the addition of enumerated sets (called one-of in classic), and role fillers to ALCN R is still to be studied, although it does not seem to endanger the filtration method we used. Instead, a different method might be necessary if inverse roles are added to ALCN R, since the finite model property is lost (as shown in Schild, 1991). Finally, the addition of concrete domains (Baader & Hanschke, 1991) remains open. 133 Buchheit, Donini, & Schaerf Acknowledgements We thank Maurizio Lenzerini for the inspiration of this work, as well as for several discussions that contributed to the paper. Werner Nutt pointed out to us the observation mentioned at the end of Section 3, and we thank him and Franz Baader for helpful comments on earlier drafts. We thank also the anonymous reviewers, whose stimulating comments helped us in improving on the submitted version. The research was partly done while the first author was visiting the Dipartimento di Informatica e Sistemistica, Universit`a di Roma "La Sapienza". The third author also acknowledges Yoav Shoham for his hospitality at the Computer Science Department of Stanford University, while the author was developing part of this research. This work has been supported by the ESPRIT Basic Research Action N.6810 (COMPULOG 2) and by the Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo of the CNR (Italian Research Council), LdR "Ibridi". References Abrial, J. (1974). Data semantics. In Klimbie, J., & Koffeman, K. (Eds.), Data Base Management, pp. 1-59. North-Holland Publ. Co., Amsterdam. Baader, F. (1990a). Augmenting concept languages by transitive closure of roles: An alternative to terminological cycles. Tech. rep. RR-90-13, Deutsches Forschungszentrum f"ur K"unstliche Intelligenz (DFKI), Kaiserslautern, Germany. An abridged version appeared in Proc. of the 12th Int. Joint Conf. on Artificial Intelligence IJCAI-91, pp. 446-451. Baader, F. (1990b). Terminological cycles in KL-ONE-based knowledge representation languages. Tech. rep. RR-90-01, Deutsches Forschungszentrum f"ur K"unstliche Intelligenz (DFKI), Kaiserslautern, Germany. An abridged version appeared in Proc. of the 8th Nat. Conf. on Artificial Intelligence AAAI-90, pp. 621-626. Baader, F., B"urkert, H.-J., Hollunder, B., Nutt, W., & Siekmann, J. H. (1990). Concept logics. In Lloyd, J. W. (Ed.), Computational Logics, Symposium Proceedings, pp. 177-201. Springer-Verlag. Baader, F., & Hanschke, P. (1991). A schema for integrating concrete domains into concept languages. In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence IJCAI-91, pp. 452-457 Sydney. Baader, F., & Hollunder, B. (1991). A terminological knowledge representation system with complete inference algorithm. In Proc. of the Workshop on Processing Declarative Knowledge, PDK-91, Lecture Notes in Artificial Intelligence, pp. 67-86. SpringerVerlag. Baader, F., & Hollunder, B. (1992). Embedding defaults into terminological knowledge representation formalisms. In Proc. of the 3rd Int. Conf. on Principles of Knowledge Representation and Reasoning KR-92, pp. 306-317. Morgan Kaufmann, Los Altos. 134 Decidable Reasoning in Terminological KR Systems Baader, F., Hollunder, B., Nebel, B., Profitlich, H.-J., & Franconi, E. (1992). An empirical analisys of optimization techniques for terminological representation systems. In Proc. of the 3rd Int. Conf. on Principles of Knowledge Representation and Reasoning KR92, pp. 270-281. Morgan Kaufmann, Los Altos. Beck, H. W., Gala, S. K., & Navathe, S. B. (1989). Classification as a query processing technique in the CANDIDE semantic data model. In Proc. of the 5th IEEE Int. Conf. on Data Engineering. Borgida, A., Brachman, R. J., McGuinness, D. L., & Alperin Resnick, L. (1989). CLASSIC: A structural data model for objects. In Proc. of the ACM SIGMOD Int. Conf. on Management of Data, pp. 59-67. Brachman, R. J., & Levesque, H. J. (1984). The tractability of subsumption in framebased description languages. In Proc. of the 4th Nat. Conf. on Artificial Intelligence AAAI-84, pp. 34-37. Brachman, R. J., Pigman Gilbert, V., & Levesque, H. J. (1985). An essential hybrid reasoning system: Knowledge and symbol level accounts in KRYPTON. In Proc. of the 9th Int. Joint Conf. on Artificial Intelligence IJCAI-85, pp. 532-539 Los Angeles. Brachman, R. J., & Schmolze, J. G. (1985). An overview of the KL-ONE knowledge representation system. Cognitive Science, 9 (2), 171-216. Buchheit, M., Donini, F. M., & Schaerf, A. (1993). Decidable reasoning in terminological knowledge representation systems. Tech. rep. RR-93-10, Deutsches Forschungszentrum f"ur K"unstliche Intelligenz (DFKI), Saarbr"ucken, Germany. An abridged version appeared in Proc. of the 13th Int. Joint Conf. on Artificial Intelligence IJCAI-93 pp. 704-709. Catarci, T., & Lenzerini, M. (1993). Representing and using interschema knowledge in cooperative information systems. Journal of Intelligent and Cooperative Inf. Syst. To appear. Dionne, R., Mays, E., & Oles, F. J. (1992). A non-well-founded approach to terminological cycles. In Proc. of the 10th Nat. Conf. on Artificial Intelligence AAAI-92, pp. 761-766. AAAI Press/The MIT Press. Dionne, R., Mays, E., & Oles, F. J. (1993). The equivalence of model theoretic and structural subsumption in description logics. In Proc. of the 13th Int. Joint Conf. on Artificial Intelligence IJCAI-93, pp. 710-716 Chambery, France. Morgan Kaufmann, Los Altos. Donini, F. M., Hollunder, B., Lenzerini, M., Marchetti Spaccamela, A., Nardi, D., & Nutt, W. (1992). The complexity of existential quantification in concept languages. Artificial Intelligence, 2-3, 309-327. Donini, F. M., Lenzerini, M., Nardi, D., & Nutt, W. (1991a). The complexity of concept languages. In Allen, J., Fikes, R., & Sandewall, E. (Eds.), Proc. of the 2nd Int. Conf. on Principles of Knowledge Representation and Reasoning KR-91, pp. 151-162. Morgan Kaufmann, Los Altos. 135 Buchheit, Donini, & Schaerf Donini, F. M., Lenzerini, M., Nardi, D., & Nutt, W. (1991b). Tractable concept languages. In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence IJCAI-91, pp. 458-463 Sydney. Donini, F. M., Lenzerini, M., Nardi, D., & Schaerf, A. (1991c). A hybrid system integrating datalog and concept languages. In Proc. of the 2nd Conf. of the Italian Association for Artificial Intelligence, No. 549 in Lecture Notes in Artificial Intelligence. SpringerVerlag. An extended version appeared also in the Working Notes of the AAAI Fall Symposium "Principles of Hybrid Reasoning". Donini, F. M., Lenzerini, M., Nardi, D., & Schaerf, A. (1993). Deduction in concept languages: From subsumption to instance checking. Journal of Logic and Computation. To appear. Fitting, M. (1990). First-Order Logic and Automated Theorem Proving. Springer-Verlag. Garey, M., & Johnson, D. (1979). Computers and Intractability--A guide to NPcompleteness. W.H. Freeman and Company, San Francisco. Harel, D. (1984). Dynamic logic. In Handbook of Philosophical Logic, Vol. 2, pp. 497-640. D. Reidel, Dordrecht, Holland. Heinsohn, J., Kudenko, D., Nebel, B., & Profitlich, H.-J. (1992). An empirical analysis of terminological representation systems. In Proc. of the 10th Nat. Conf. on Artificial Intelligence AAAI-92, pp. 767-773. AAAI Press/The MIT Press. Hollunder, B. (1990). Hybrid inferences in KL-ONE-based knowledge representation systems. In Proc. of the German Workshop on Artificial Intelligence, pp. 38-47. SpringerVerlag. Hollunder, B., & Baader, F. (1991). Qualifying number restrictions in concept languages. Tech. rep. RR-91-03, Deutsches Forschungszentrum f"ur K"unstliche Intelligenz (DFKI), Kaiserslautern, Germany. An abridged version appeared in Proc. of the 2nd Int. Conf. on Principles of Knowledge Representation and Reasoning KR-91. Hughes, G. E., & Cresswell, M. J. (1984). A Companion to Modal Logic. Methuen, London. Kaczmarek, T. S., Bates, R., & Robins, G. (1986). Recent developments in NIKL. In Proc. of the 5th Nat. Conf. on Artificial Intelligence AAAI-86, pp. 978-985. Lenzerini, M., & Schaerf, A. (1991). Concept languages as query languages. In Proc. of the 9th Nat. Conf. on Artificial Intelligence AAAI-91, pp. 471-476. Levesque, H. J. (1984). Foundations of a functional approach to knowledge representation. Artificial Intelligence, 23, 155-212. Lewis, H. R., & Papadimitriou, C. H. (1981). Elements of the Theory of Computation. Prentice-Hall, Englewood Cliffs, New Jersey. MacGregor, R. (1991). Inside the LOOM description classifier. SIGART Bulletin, 2 (3), 88-92. 136 Decidable Reasoning in Terminological KR Systems MacGregor, R. (1992). What's needed to make a description logic a good KR citizen. In Working Notes of the AAAI Fall Symposium on Issues on Description Logics: Users meet Developers, pp. 53-55. MacGregor, R., & Bates, R. (1987). The Loom knowledge representation language. Tech. rep. ISI/RS-87-188, University of Southern California, Information Science Institute, Marina del Rey, Cal. MacGregor, R., & Brill, D. (1992). Recognition algorithms for the LOOM classifier. In Proc. of the 10th Nat. Conf. on Artificial Intelligence AAAI-92, pp. 774-779. AAAI Press/The MIT Press. Mays, E., Dionne, R., & Weida, R. (1991). K-REP system overview. SIGART Bulletin, 2 (3). McAllester, D. (1991). Unpublished manuscript. McGuinness, D. L. (1992). Making description logic based knowledge representation systems more usable. In Working Notes of the AAAI Fall Sysmposium on Issues on Description Logics: Users meet Developers, pp. 56-58. Mylopoulos, J., Bernstein, P., & Wong, E. (1980). A language facility for designing databaseintensive applications. ACM Trans. on Database Syst., 5 (2), 185-207. Nebel, B. (1988). Computational complexity of terminological reasoning in BACK. Artificial Intelligence, 34 (3), 371-383. Nebel, B. (1990). Reasoning and Revision in Hybrid Representation Systems. Lecture Notes in Artificial Intelligence. Springer-Verlag. Nebel, B. (1991). Terminological cycles: Semantics and computational properties. In Sowa, J. F. (Ed.), Principles of Semantic Networks, pp. 331-361. Morgan Kaufmann, Los Altos. Nutt, W. (1992). Personal communication. Patel-Schneider, P. F. (1984). Small can be beautiful in knowledge representation. In Proc. of the IEEE Workshop on Knowledge-Based Systems. An extended version appeared as Fairchild Tech. Rep. 660 and FLAIR Tech. Rep. 37, October 1984. Patel-Schneider, P. (1989). Undecidability of subsumption in NIKL. Artificial Intelligence, 39, 263-272. Pratt, V. R. (1978). A practical decision method for propositional dynamic logic. In Proc. of the 10th ACM SIGACT Symp. on Theory of Computing STOC-78, pp. 326-337. Quantz, J., & Kindermann, C. (1990). Implementation of the BACK system version 4. Tech. rep. KIT-Report 78, FB Informatik, Technische Universit"at Berlin, Berlin, Germany. Rich, editor, C. (1991). SIGART bulletin. Special issue on implemented knowledge representation and reasoning systems. (2)3. 137 Buchheit, Donini, & Schaerf Schaerf, A. (1993a). On the complexity of the instance checking problem in concept languages with existential quantification. Journal of Intelligent Information Systems, 2, 265-278. An abridged version appeared in Proc. of the 7th Int. Symp. on Methodologies for Intelligent Systems ISMIS-93. Schaerf, A. (1993b). Reasoning with individuals in concept languages. Tech. rep. 07.93, Dipartimento di Informatica e Sistemistica, Universit`a di Roma "La Sapienza". An abridged version appeared in Proc. of the 3rd Conf. of the Italian Association for Artificial Intelligence AI*IA-93. Schild, K. (1988). Undecidability of subsumption in U . Tech. rep. KIT-Report 67, FB Informatik, Technische Universit"at Berlin, Berlin, Germany. Schild, K. (1991). A correspondence theory for terminological logics: Preliminary report. In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence IJCAI-91, pp. 466-471 Sydney. Schmidt-Schauss, M. (1989). Subsumption in KL-ONE is undecidable. In Brachman, R. J., Levesque, H. J., & Reiter, R. (Eds.), Proc. of the 1st Int. Conf. on Principles of Knowledge Representation and Reasoning KR-89, pp. 421-431. Morgan Kaufmann, Los Altos. Schmidt-Schauss, M., & Smolka, G. (1991). Attributive concept descriptions with complements. Artificial Intelligence, 48 (1), 1-26. Vardi, M., & Wolper, P. (1986). Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32, 183-221. A preliminary version appeared in Proc. of the 16th ACM SIGACT Symp. on Theory of Computing STOC84. Vilain, M. (1991). Deduction as parsing: Tractable classification in the KL-ONE framework. In Proc. of the 9th Nat. Conf. on Artificial Intelligence AAAI-91, pp. 464-470. Wand, M. (1980). Induction, Recursion, and Programming. North-Holland Publ. Co., Amsterdam. Woods, W. A., & Schmolze, J. G. (1992). The KL-ONE family. In Lehmann, F. (Ed.), Semantic Networks in Artificial Intelligence, pp. 133-178. Pergamon Press. Published as a special issue of Computers & Mathematics with Applications, Volume 23, Number 2-9. 138