\documentstyle[jair,twoside,11pt,theapa]{article} \jairheading{1}{1993}{109-138}{7/93}{12/93} \ShortHeadings{Decidable Reasoning in Terminological KR Systems}% {Buchheit, Donini, \& Schaerf} \firstpageno{109} %%%%%%%%%%%%%%%%%%%%%%%%%%% theorems, proofs, examples and general assumptions \newtheorem% {theorem}{Theorem}[section] \newtheorem% {corollary}[theorem]{Corollary} \newtheorem% {proposition}[theorem]{Proposition} \newtheorem% {lemma}[theorem]{Lemma} \newtheorem% {definition}[theorem]{Definition} \newtheorem% {exampleAux}[theorem]{Example} \newenvironment% {example}{\begin{exampleAux}\rm}{\end{exampleAux}} \newtheorem% {examplesAux}[theorem]{Examples} \newenvironment% {examples}{\begin{examplesAux}\rm}{\end{examplesAux}} \newtheorem% {constructionAux}[theorem]{Construction} \newenvironment% {construction}{\begin{constructionAux}\rm}{\end{constructionAux}} \def\proof{{\sl Proof.\ \ }} \def\qed{\hfill{\boxit{}} \ifdim\lastskip<\medskipamount \removelastskip\penalty55\medskip\fi} \long\def\boxit#1{\vbox{\hrule\hbox{\vrule\kern3pt \vbox{\kern3pt#1\kern3pt}\kern3pt\vrule}\hrule}} \newcommand{\hangif}[1]{\raisebox{-1ex}{\hspace{2em} \makebox[1.0em][l]{if} \parbox[t]{340pt}{#1}}} \newcommand {\boxfigure}[1]% {\framebox[\textwidth]{% \parbox {0.99\textwidth} {{#1}\vspace {0cm}\hfill}}} \newcommand {\boxfigureone}[1]% {\framebox[\textwidth]{% \parbox {0.90\textwidth} {{#1}\vspace {0cm}\hfill}}} \newcounter{nr} \newenvironment{deflist}% {\begin{list}{\arabic{nr}. \hfill} {\usecounter{nr} \itemsep0ex plus0.2ex \topsep0ex \leftmargin1.15cm \labelsep0.1cm \labelwidth0.5cm } }% {\end{list}} %%%% end of format %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% General Math \def\A{{\cal A}} \def\B{{\cal B}} \def\C{{\cal C}} \def\D{{\cal D}} \def\E{{\cal E}} \def\F{{\cal F}} \def\G{{\cal G}} \def\H{{\cal H}} \def\I{{\cal I}} \def\J{{\cal J}} \def\K{{\cal K}} \def\L{{\cal L}} \def\M{{\cal M}} \def\N{{\cal N}} \def\O{{\cal O}} \def\P{{\cal P}} \def\Q{{\cal Q}} \def\R{{\cal R}} \def\S{{\cal S}} \def\T{{\cal T}} \def\U{{\cal U}} \def\V{{\cal V}} \def\W{{\cal W}} \def\X{{\cal X}} \def\Y{{\cal Y}} \def\Z{{\cal Z}} \def\IS{{{\cal I}_S}} \def\alphaS{{\alpha_S}} \def\asp{\makebox[3pt]{}} %arrow space, put before and after arrows \def\osp{\hskip1pt} %operator space, put before and after operators \def\asps#1{{\asp#1\asp}} \def\osps#1{{\osp{#1}\osp}} \def\eset{\emptyset} \def\incl{\subseteq} \def\qland{\;\;\land\;\;} \def\col{\colon} \def\imp{\Rightarrow} \def\cld{,\ldots,} %comma lower dots \def\braces#1{$\{$ #1 $\}$} \def\con{\asp\asp\&\asp} \def\deq{\doteq} \def\sbox{\vbox{\hrule \hbox{\vrule\hskip4pt\vbox{\vskip4pt}\vrule} \hrule}} \def\per{\mbox{\bf .}} % period \def\ol#1{\overline{#1}} %overline \def\dd#1#2{#1_1,\ldots,#1_{#2}} %da da, makes x1,...,xn \def\set#1{\{#1\}} \def\bigset#1{ \Bigl\{ #1 \Bigr\} } % makes the big set { #1 } \def\bigmid{\ \Big|\ } \def\card#1{|{#1}|} \def\sub#1{[#1]} \def\Onlyif{\lq\lq$\Rightarrow$\rq\rq\ \ } %1st direction of iff-proof \def\If{\lq\lq$\Leftarrow$\rq\rq\ \ } %2nd direction of iff-proof %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% General Commands %%%%%%%%%%%%%%%%%%%%%%% abbreviations \newcommand{\cs}{constraint system} \newcommand{\KLONE}{{\sc kl-one}} %%%%%%%%%%%%%%%%%%%%%%% Symbols \newcommand{\dom}{\Delta^\I} % D "power" I, % domain of interpretation \I \newcommand{\Int}[1]{#1^\I} % argument^I % interpretation function \newcommand{\INT}[1]{(#1)^\I} % (argument)^I, % interpretation function \newcommand{\al}[1]{\alpha(#1)} % mapping of variables \newcommand{\domS}{\Delta^\IS} % D "power" I_S, % domain of interpretation \I \newcommand{\IntS}[1]{#1^\IS} % argument^I_S % can. interpretation function \newcommand{\INTS}[1]{(#1)^\IS} % (argument)^I_S, % can. interpretation function \newcommand{\alS}[1]{\alpha_S(#1)} % can. mapping of variables %%%%%%%%%%%%%%%%%%%%%%% Concept forming operators \def\AND{\sqcap} \def\OR{\sqcup} \def\NOT{\neg} \def\INV#1{#1^{-1}} \def\ALL#1#2{\forall #1 \per #2} \def\SOME#1#2{\exists #1 \per #2} \def\SOMET#1{\exists #1} \def\ALLRC{\ALL R C} \def\SOMERC{\SOME R C} \def\SOMERT{\SOMET R} \newcommand{\ATMOST}[2]{(\leq #1 \, #2)} \newcommand{\ATLEAST}[2]{(\geq #1 \, #2)} \newcommand{\DISAGREE}[2]{{#1 \not\doteq #2}} %%%%%%%%%%%%%%%%%%%%%%% Constraints \newcommand{\inclc}[2]{#1 \sqsubseteq #2} \newcommand{\inc}[2]{#1\col#2} \newcommand{\relc}[3]{#1#2#3} \newcommand{\InCon}[2]{#1 \!:#2} \newcommand{\nrs}[1]{n_{R,S}(#1)} \newcommand{\ddxpy}{\relc x{P_1}y ,\ldots, \relc x{P_k}y} % "dada x P y" % makes x P1 y,...,x Pk y \newcommand{\ddspt}{\relc s{P_1}t ,\ldots, \relc s{P_k}t} \newcommand{\RISPS}{R= P_1\AND\ldots\AND P_k} % R = P1 and ... and Pk %%%%%%%% universal constraints %%%%%%% \newcommand{\univinc}[2]{\forall#1\per{\inc #1 #2}} %%%%%%%% sets of concept constraints %%%%%%%%%% \newcommand{\SC}[2]{\sigma(#1,#2)} %%%%%%%%%%%%%%%%%%%%%%% Language Names \newcommand{\ALN}{{\cal ALN}} \newcommand{\AL}{{\cal AL}} \newcommand{\ALC}{{\cal ALC}} \newcommand{\ALE}{{\cal ALE}} \newcommand{\ALU}{{\cal ALU}} \newcommand{\ALCNR}{{\cal ALCNR}} \newcommand{\FL}{{\cal FL}} %%%%%%%%%%%%%%%%%%%%%%% Arrows \newcommand{\rtall}{\rightarrow_\forall} \newcommand{\rtsome}{\rightarrow_\exists} \newcommand{\rtor}{\rightarrow_\sqcup} \newcommand{\rtand}{\rightarrow_\sqcap} \newcommand{\rtuniv}{\rightarrow_{\forall x}} \newcommand{\rtatmost}{\rightarrow_\leq} \newcommand{\rtatleast}{\rightarrow_\geq} %%%%%%%%%%%%%%%%%%%%%%%%% end of macros %%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{document} \title{Decidable Reasoning in Terminological Knowledge Representation Systems} \author{\name Martin Buchheit \email buchheit@dfki.uni-sb.de\\ \addr German Research Center for Artificial Intelligence (DFKI)\\ Stuhlsatzenhausweg 3, D-66123 Saarbr\"ucken, Germany \AND \name Francesco M. Donini \email donini@assi.dis.uniroma1.it\\ \name Andrea Schaerf \email aschaerf@assi.dis.uniroma1.it\\ \addr Dipartimento di Informatica e Sistemistica\\ Universit\`a di Roma ``La Sapienza", Via Salaria 113, I-00198 Roma, Italy} \maketitle \begin{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 $\ALCNR$, 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 $\ALCNR$-knowledge bases. Our calculus extends the general technique of \cs s. As a byproduct of the proof, we get also the result that inclusion statements in $\ALCNR$ can be simulated by terminological cycles, if descriptive semantics is adopted. \end{abstract} \section{Introduction}\label{sec-introduction} A general characteristic of many proposed terminological knowledge representation systems (TKRSs) such as {\sc krypton} \cite{BrPL85}, {\sc nikl} \cite{KaBR86}, {\sc back} \cite{QuKi90}, {\sc loom} \cite{MaBa87}, {\sc classic} \cite{BBMR89}, {\sc kris} \cite{BaHo91}, {\sc k-rep} \cite{MaDW91}, and others \cite{Rich91,WoSc92}, 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 \KLONE\ \cite{BrSc85}, is shared also by several proposals of database models such as Abrial's \citeyear{Abri74}, {\sc candide} \cite{BeGN89}, and {\sc taxis} \cite{MyBW80}. 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). 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 {\em concept} to refer to a class): \begin{enumerate} \item {\em 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. \item {\em 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. \item {\em 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. \item {\em 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 {\em query} in the database lexicon) can be formulated as a set of parallel instance checkings. \end{enumerate} 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 {\sc kris}\footnote{Also the system {\sc 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 coNP-hard \cite{LeSc91}.}. 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 {\sc taxis}), or define appropriate inference rules completing the inference capabilities of the system (as in {\sc back}, {\sc loom}, and {\sc classic}). From the theoretical point of view, for several systems (e.g., {\sc 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. \citeB{BrLe84} started this research analyzing the complexity of subsumption between pure concept expressions, abstracting from KBs (we call this problem later in the paper as {\em 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 \cite{Nebe88,DLNN91,DLNN91b,ScSm91,DHLM92}. Also, beyond computational complexity, pure subsumption was proved undecidable in the TKRSs ${\cal U}$ \cite{Schi88}, \KLONE\ \cite{Schm89} and {\sc nikl} \cite{Pate89b}. 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 \citeB{Leve84} first noted. This result has been interpreted in two different ways, leading to two different TKRSs design philosophies: \begin{enumerate} \item `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 {\sc nikl}, {\sc loom} and {\sc back}) incomplete procedures for pure subsumption are considered satisfactory (e.g., see \cite{MaBr92} for {\sc 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 \cite{HKNP92}, and how to judge a procedure ``complete enough" \cite{MacG90}. 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. \item `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 {\sc krypton} and {\sc classic}) provide limited tractable languages for expressing concepts, following the ``small-can-be-beautiful" approach \cite{Pate84}. 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 \cite{McGu92}. \end{enumerate} 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 \cite[Chapter~4]{Nebe90b}, but only incomplete procedures are given, and cycles are not considered. In \cite{DLNS93,Scha93} the complexity of instance checking has been analyzed, but only KBs without a TBox are treated. Instance checking has also been analyzed in \cite{Vila91}, 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 \cite[Chapter 5]{Nebe90b} available in TKRSs. Such a feature is of undoubtable practical interest \cite{MacG92}, yet most present TKRSs can only approximate cycles, by using forward inference rules (as in {\sc 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 \cite{Baad90b,Baad90,BBHN90,DiMO92,DiMO93,Nebe90b,Nebe91,Schi91}, but considering KBs formed by the TBox alone. Moreover, these approaches do not deal with number restrictions \cite[Section 5.3.5]{Nebe90b} ---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~\ref{sec-prevwork}. 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 $\ALCNR$, 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 \cs s \cite{DLNN91,ScSm91}, 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~\ref{sec-preliminaries} 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~\ref{sec-decidability} we provide a calculus for KB-satisfiability, and show correctness and termination of the calculus. Hence, we conclude that KB-satisfiability is decidable in $\ALCNR$, which is the main result of this paper. In Section~\ref{sec-prevwork} 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~\ref{sec-conclusions}. \section{Preliminaries}\label{sec-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. \subsection{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 defined by means of suitable constructors applied to concept names and role names. In particular, concepts and roles in $\ALCNR$ can be formed by means of the following syntax (where $P_i$ (for $i=1,\dots,k$) denotes a role name, $C$ and $D$ denote arbitrary concepts, and $R$ an arbitrary role): \[ \begin{array}{rcl@{\qquad}l} C,D & \ \longrightarrow\ & A \mid & \mbox{(concept name)}\\ & & \top \mid & \mbox{(top concept)} \\ & & \bot \mid & \mbox{(bottom concept)} \\ & & (C\AND D) \mid & \mbox{(conjunction)} \\ & & (C\OR D) \mid & \mbox{(disjunction)} \\ & & \NOT C \mid &\mbox{(complement)} \\ & & \ALLRC \mid &\mbox{(universal quantification)} \\ & & \SOME R C\mid & \mbox{(existential quantification)}\\ & &\ATLEAST n R\mid \ATMOST n R& \mbox{(number restrictions)}\\ R & \ \longrightarrow\ & P_1\AND\cdots\AND P_k & \mbox{(role conjunction)} \end{array} \] 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 {\em interpretation\,} $\I = (\dom, \Int\cdot)$ consists of a nonempty set $\dom$ (the {\em domain\,} of $\I$) and a function $\Int{\cdot}$ (the {\em extension function\,} of $\I$), which maps every concept to a subset of $\dom$ and every role to a subset of $\dom\times\dom$. The interpretation of concept names and role names is thus restricted by $\Int A \subseteq \dom$, and $\Int P \subseteq \dom\times\dom$, respectively. Moreover, the interpretation of complex concepts and roles must satisfy the following equations ($\sharp\set{}$ denotes the cardinality of a set): \begin{eqnarray} \Int\top & = & \dom \nonumber \\ \Int\bot & = & \emptyset \nonumber \\ \INT{C\AND D} & = & \Int C \cap \Int D \nonumber \\ \INT{C\OR D} & = & \Int C \cup \Int D \label{int-eq} \\ \INT{\NOT C} & = & \dom \setminus \Int C \nonumber \\ \INT\ALLRC & = & \set{ d_1\in\dom \mid \forall d_2: (d_1,d_2) \in\Int R \rightarrow\ d_2\in\Int C} \nonumber \\ \INT{\SOMERC } & = & \set{ d_1\in\dom \mid \exists d_2: (d_1,d_2)\in\Int R \wedge d_2\in\Int C} \nonumber \\ \Int{\ATLEAST n R} &=& \set{d_1\in\dom\mid~~~\sharp\set{d_2\mid (d_1,d_2) \in\Int R}~~\geq n}\nonumber\\ \Int{\ATMOST n R} &=& \set{d_1\in\dom\mid~~~\sharp\set{d_2\mid (d_1,d_2) \in\Int R}~~\leq n}\nonumber\\ \INT{P_1\AND\cdots\AND P_k} & = & \Int P_1 \cap\cdots\cap \Int P_k \nonumber \end{eqnarray} \subsection{Knowledge Bases} A knowledge base built by means of concept languages is generally formed by two components: The {\em intensional} one, called TBox, and the {\em 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 {\em inclusion statements}. An inclusion statement (or simply inclusion) has the form $$C \sqsubseteq D$$ where $C$ and $D$ are two arbitrary $\ALCNR$-concepts. Intuitively, the statement specifies that every instance of $C$ is also an instance of $D$. More precisely, an interpretation $\I$ {\em satisfies} the inclusion $C \sqsubseteq D$ if $\Int C \subseteq \Int D$. A TBox is a finite set of inclusions. An interpretation $\I$ is a {\em model} for a TBox $\T$ if $\I$ satisfies all inclusions in $\T$. In general, TKRSs provide the user with mechanisms for stating {\em concept introductions\/} \cite[Section 3.2]{Nebe90b} of the form $A \doteq D$ (concept definition, interpreted as set equality), or $A ~\dot\leq~ 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 {\em 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 \doteq D$ can be expressed in our system using the pair of inclusions $A \sqsubseteq D$ and $D \sqsubseteq A$ and a specification of the form $A ~\dot\leq~ D$ can be simply expressed by $A \sqsubseteq D$. Conversely, an inclusion of the form $C \sqsubseteq 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 \cite{Nebe91}, 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 \doteq 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 \doteq 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 \cite{Baad90,Nebe91}, 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. \vskip 1\baselineskip Observe that our decision to put general inclusions in the TBox is not a standard one. In fact, in TKRS like {\sc krypton} such statements were put in the ABox. However, we conceive 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. \vskip 1\baselineskip Notice that role conjunction allows one to express the practical feature of {\em subroles}. For example, the role {\tt ADOPTED\-CHILD} can be written as ${\tt CHILD}\AND {\tt ADOPTED\-CHILD'}$, where {\tt ADOPTED\-CHILD'} is a role name, making it a subrole of {\tt 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\doteq R$ and $P~\dot\leq~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 \cite[Sec.5.3.1]{Nebe90b}. 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 \cite{CaLe93b}. 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 \[ \SOME R {\top}\sqsubseteq C,~~\top\sqsubseteq\ALL R D \] It is straightforward to show that if an interpretation $\I$ satisfies the two inclusions, then $\Int R\subseteq\Int C\times\Int D$. Combining subroles with domain and range restrictions it is also possible to partially express the constructor for {\em role restriction}, which is present in various proposals \cite{BrLe84}. Role restriction, written as $R\!:C$, is defined by $\INT{R\!:C}=\set{(d_1,d_2)\in \dom\times\dom\mid (d_1,d_2)\in \Int R \wedge d_2\in \Int C}$. For example the role {\tt DAUGHTER}, which can be formulated as {\tt CHILD:Female}, can be partially simulated by ${\tt CHILD}\AND{\tt DAUGHTER'}$, with the inclusion $\top\sqsubseteq\ALL {{\tt DAUGHTER'}}{{\tt 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. %Similarly, we can express roles obtained by the combination of subroles with %both domain and range restrictions. For example, the role {\tt WIFE} %is expressed as ${\tt SPOUSE}\AND{\tt WIFE'}$ %with the inclusions $\top\sqsubseteq\ALL {{\tt WIFE'}}{{\tt Female}}$ and %$\SOME {{\tt WIFE'}}{\top}\sqsubseteq {{\tt Male}}$. \vskip 1\baselineskip We can now turn our attention to the {\em 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 {\em individuals}. Instance-of relationships are expressed in terms of {\em membership assertions} of the form: % \[ C(a),~~~~~R(a,b), \] % where $a$ and $b$ are individuals, $C$ is an $\ALCNR$-concept, and $R$ is an $\ALCNR$-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 assertions, the extension function $\Int \cdot$ of an interpretation $\I$ is extended to individuals by mapping them to elements of $\dom$ in such a way that $\Int a \neq \Int b$ if $a \neq b$. This property is called {\em Unique Name Assumption}; it ensures that different individuals are interpreted as different objects. An interpretation $\I$ {\em satisfies} the assertion $C(a)$ if $\Int a \in \Int C$, and {\em satisfies} $R(a,b)$ if $(\Int a,\Int b) \in \Int R$. An ABox is a finite set of membership assertions. $\I$ is a {\em model} for an ABox $\A$ if $\I$ satisfies all the assertions in $\A$. \vskip 1\baselineskip An $\ALCNR$-{\em knowledge base} $\Sigma$ is a pair $\Sigma = \langle\T ,\A\rangle $ where $\T$ is a TBox and $\A$ is an ABox. An interpretation $\I$ is a {\em 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 $\ALCNR$-knowledge base. \begin{enumerate} \item {\em KB-satisfiability} : $\Sigma$ is {\em satisfiable}, if it has a model; \item {\em Concept Satisfiability} : $C$ is {\em satisfiable} w.r.t\ $\Sigma$, if there exists a model $\I$ of $\Sigma$ such that $\Int C \neq \emptyset$; \item {\em Subsumption} : $C$ is {\em subsumed} by $D$ w.r.t.\ $\Sigma$, if $\Int C \incl \Int D$ for every model $\I$ of $\Sigma$; \item {\em Instance Checking} : $a$ is an instance of $C$, written $\Sigma \models C(a)$, if the assertion $C(a)$ is satisfied in every model of $\Sigma$. \end{enumerate} In \cite[Sec.3.3.2]{Nebe90b} 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 \cite{Nebe90b}, the above property is stated for a language less expressive than $\ALCNR$. However, it is easy to show that it extends to $\ALCNR$. 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 {\sc one-of} \cite{BBMR89} 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 \cite{Scha93c}. As a consequence, both concept satisfiability and subsumption depend also on the ABox. \begin{example} Consider the following knowledge base $\Sigma=\langle\T,\A\rangle$: \begin{tabbing} \indent $\T = \{$\= $\SOME {\tt TEACHES}{\tt Course} \sqsubseteq ({\tt Student}\AND\SOME{{\tt DEGREE}}{{\tt BS}})\OR {\tt Prof},$ \+\\ ${\tt Prof } \sqsubseteq \SOME {\tt DEGREE}{\tt MS},$ \\ $\SOME {{\tt DEGREE}}{{\tt MS}} \sqsubseteq \SOME {{\tt DEGREE}}{{\tt BS}},$ \\ ${\tt MS} \AND {\tt BS} \sqsubseteq \bot\}$\-\\ \indent $\A = \{ {\tt TEACHES(john,cs156)},~\ATMOST 1 {{\tt DEGREE}}({\tt john}), {\tt Course(cs156)} \}$ \end{tabbing} \noindent $\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 in $\A$, and therefore it is a model for $\Sigma$:\\[1.3ex] \indent $\dom = \set{{\tt john},{\tt cs156},{\tt csb}}, ~\Int{\tt john}={\tt john},~\Int{\tt cs156} = {\tt cs156}$ $\Int{\tt Student}=\set{{\tt john}},~ \Int{\tt Prof} = \emptyset,~ \Int{\tt Course}= \set{{\tt cs156}},~ \Int{\tt BS} = \set{{\tt csb}}$ $\Int{\tt MS} = \emptyset,~ \Int{\tt TEACHES}= \set{({\tt john},{\tt cs156})},~ \Int{\tt DEGREE}= \set{({\tt john},{\tt csb})}$\\[1.3ex] % \noindent We have described the interpretation $\I$ by giving only $\dom$, 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~\ref{int-eq} on page~\pageref{int-eq}. Notice that it is possible to draw several non-trivial conclusions from $\Sigma$. For example, we can infer that $\Sigma\models {\tt 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. \qed \end{example} 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=\langle\T,\A\rangle$, two concepts $C$ and $D$, an individual $a$, and an individual $b$ not appearing in $\Sigma$, the following equivalences hold: \begin{eqnarray*} C {\rm ~is~ satisfiable~ w.r.t~} \Sigma &{\rm iff}& \langle \T,\A\cup\set{C(b)} \rangle {\rm ~is~ satisfiable.}\\ C {\rm ~is ~subsumed ~by~} D~ {\rm w.r.t.~} \Sigma &{\rm iff}& \langle \T,\A\cup\set{(C \AND \NOT D)(b)} \rangle {\rm ~is~ not~ satisfiable.}\\ \Sigma \models C(a) &{\rm iff}& \langle \T,\A\cup\set{(\NOT C)(a)} \rangle {\rm ~is ~not ~satisfiable.} \end{eqnarray*} A slightly different form of these equivalences has been given in \cite{Holl90}. 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 \cite{Scha93c}. Based on the above equivalences, in the next section we concentrate just on KB-satisfiability. \section{Decidability Result}\label{sec-decidability} 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. \subsection{The calculus and its correctness} Our method makes use of the notion of {\em constraint system} \cite{DLNN91,ScSm91,DLNS91}, and is based on a tableaux-like calculus \cite{Fitt90} that tries to build a model for the logical formula corresponding to a KB. We introduce an alphabet of variable symbols $\V$ together with a well-founded total ordering `$\prec$' 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 {\em object} as an abstraction for individual and variable (i.e., an object is an element of $\O \cup \V$). Objects are denoted by the symbols $s,t$ and, as in Section~\ref{sec-preliminaries}, individuals are denoted by $a,b$. A {\em constraint} is a syntactic entity of one of the forms: $$\inc s C,~~~~ \relc s P t,~~~~ \univinc x C,~~~~ \DISAGREE s t,$$ \noindent where $C$ is a concept and $P$ is a role name. Concepts are assumed to be {\em simple}, i.e., the only complements they contain are of the form $\NOT A$, where $A$ is a concept name. Arbitrary $\ALCNR$-concepts can be rewritten into equivalent simple concepts in linear time \cite{DLNN91}. A constraint system is a finite nonempty set of constraints. Given an interpretation $\I$, we define an {\em $\I$-assignment} $\alpha$ as a function that maps every variable of $\V$ to an element of $\dom$, and every individual $a$ to $\Int a$ (i.e., $\al a = \Int a$ for all $a \in \O$). A pair $(\I,\alpha)$ {\em satisfies} the constraint $\inc s C$ if $\al s \in \Int C$, the constraint $\relc s P t$ if $(\al s, \al t)$ $\in \Int P$, the constraint $\DISAGREE s t$ if $\al s\neq \al t$, and finally, the constraint $\univinc x C$ if $\Int C = \dom$ (notice that $\alpha$ does not play any role in this case). A \cs\ $S$ is {\em satisfiable} if there is a pair $(\I,\alpha)$ that satisfies every constraint in $S$. An $\ALCNR$-knowledge base $\Sigma = \langle\T,\A \rangle$ can be translated into a \cs\ $S_\Sigma$ by replacing every inclusion $C \sqsubseteq D \in \T$ with the constraint $\univinc x {\NOT C \OR D}$, every membership assertion $C(a)$ with the constraint $\inc a C$, every $R(a,b)$ with the constraints $\relc a {P_1} b , \ldots , \relc a {P_k} b$ if $\RISPS$, and including the constraint $\DISAGREE a b$ for every pair $(a,b)$ of individuals appearing in $\A$. It is easy to see that $\Sigma$ is satisfiable if and only if $S_\Sigma$ is satisfiable. In order to check a \cs\ $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 {\em propagation rules}. Before providing the rules, we need some additional definitions. Let $S$ be a \cs\ and $\RISPS$ $(k \ge 1)$ be a role. We say that $t$ is an {\em $R$-successor of $s$ in $S$\/} if $\ddspt$ are in $S$. We say that $t$ is a {\em 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 {\em successor} the transitive closure of the relation direct successor, and we denote by {\em predecessor} its inverse. We assume that variables are introduced in a \cs\ according to the ordering `$\prec$'. This means, if $y$ is introduced in a \cs\ $S$ then $x \prec y$ for all variables $x$ that are already in $S$. We denote by $S[x/s]$ the \cs\ obtained from $S$ by replacing each occurrence of the variable $x$ by the object $s$. We say that $s$ and $t$ are {\em separated in $S$\/} if the constraint $\DISAGREE s t$ is in $S$. Given a \cs\ $S$ and an object $s$, we define the function $\SC \cdot \cdot$ as follows: $\SC S s :=\set{C \mid \inc s C \in S}$. Moreover, we say that two variables $x$ and $y$ are $S$-{\em equivalent}, written $x \equiv_s y$, if $\SC S x =\SC S y$. Intuitively, two S-equivalent variables can represent the same element in the potential interpretation built by the rules, unless they are separated. \vskip 1\baselineskip \noindent The {\em propagation rules} are: % \begin{enumerate} \item $S \asps\rtand \set{\inc s{C_1},\ \inc s{C_2}} \cup S$ \\ \hangif{ 1. $\inc s{C_1\AND C_2}$ is in $S$,\\ 2. $\inc s{C_1}$ and $\inc s {C_2}$ are not both in $S$} % \item $S \asps\rtor \set{\inc s D} \cup S$ \\ \hangif{ 1. $\inc s{C_1\OR C_2}$ is in $S$,\\ 2. neither $\inc s{C_1}$ nor $\inc s {C_2}$ is in $S$, \\ 3. $D=C_1$ or $D=C_2$} % \item $S \asps\rtall \set{\inc t C} \cup S$ \\ \hangif{ 1. $\inc s \ALLRC$ is in $S$,\\ 2. $t$ is an $R$-successor of $s$, \\ 3. $\inc t C$ is not in $S$} % \item $S \asps\rtsome \set{\relc s P_1 y,\ldots, \relc s P_k y,\ \inc y C}\cup S$ \\ \hangif{ 1. $\inc s\SOMERC$ is in $S$,\\ 2. $\RISPS$,\\ 3. $y$ is a new variable, \\ 4. there is no $t$ such that $t$ is an $R$-successor of $s$ in $S$ and $\inc t C$ is in $S$,\\ 5. if $s$ is a variable there is no variable $w$ such that $w\prec s$ and $s\equiv_s w$} \item $S \asps\rtatleast \set{\relc s P_1 y_i,\ldots,\relc s P_k y_i \mid i \in 1..n} \cup \set{\DISAGREE{y_i}{y_j} \mid i,j \in 1..n,i \neq j} \cup S$ \\ \hangif{ 1. $\inc s \ATLEAST n R$ is in $S$, \\ 2. $\RISPS$, \\ 3. $y_1,\ldots,y_n$ 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\prec s$ and $s\equiv_s w$} \item $S \asps\rtatmost S[y/t]$ \\ \hangif{ 1. $\inc s \ATMOST 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} \item $S \asps\rtuniv \set{\inc s C} \cup S$ \\ \hangif{ 1. $\univinc x C$ is in $S$, \\ 2. $s$ appears in $S$, \\ 3. $\inc s C$ is not in $S$.} \end{enumerate} We call the rules $\rtor$ and $\rtatmost$ {\em nondeterministic} rules, since they can be applied in different ways to the same \cs\ (intuitively, they correspond to branching rules of tableaux). All the other rules are called {\em deterministic} rules. Moreover, we call the rules $\rtsome$ and $\rtatleast$ {\em generating} rules, since they introduce new variables in the \cs. All other rules are called {\em nongenerating} ones. 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 \cs\ 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 $\inc s C$ (condition 1), or, in the case of the $\rtuniv$-rule, because of the presence of an object $s$ in $S$. When no confusion arises, we will say that a rule is {\em applied to} the constraint $\inc s C$ or the object $s$ (instead of saying that it is applied to the \cs\ $S$). \begin{proposition}[Invariance]\label{invariance} Let $S$ and $S'$ be \cs s. Then: \begin{enumerate} \item If $S'$ is obtained from $S$ by application of a deterministic rule, then $S$ is satisfiable if and only if $S'$ is satisfiable. \item If $S'$ is obtained from $S$ by application of a nondeterministic rule, then $S$ is satisfiable if $S'$ 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. \end{enumerate} \end{proposition} \proof The proof is mainly a rephrasing of typical soundness proofs for tableaux methods \cite[Lemma 6.3.2]{Fitt90}. The only non-standard constructors are number restrictions. \noindent {\it 1.} \If Considering the deterministic rules one can directly check that $S$ is a subset of $S'$. So it is obvious that $S$ is satisfiable if $S'$ is satisfiable. \Onlyif In order to show that $S'$ is satisfiable if this is the case for $S$ we consider in turn each possible deterministic rule application leading from $S$ to $S'$. % We assume that $(\I,\alpha)$ satisfies $S$. If the $\rtand$-rule is applied to $\inc s {C_1 \AND C_2}$ in $S$, then $S' = S \cup \set{\inc s{C_1},\ \inc s{C_2}}$. Since $(\I,\alpha)$ satisfies $\inc s{C_1\AND C_2}$, $(\I,\alpha)$ satisfies $\inc s{C_1}$ and $\inc s{C_2}$ and therefore $S'$. If the $\rtall$-rule is applied to $\inc s \ALLRC$, there must be an $R$-successor $t$ of $s$ in $S$ such that $S' = S \cup \set{\inc t C}$. Since $(\I,\alpha)$ satisfies $S$, it holds that $(\al s, \al t) \in \Int R$. Since $(\I,\alpha)$ satisfies $\inc s \ALLRC$, it holds that $\al t \in \Int C$. So $(\I,\alpha)$ satisfies $\inc t C$ and therefore $S'$. If the $\rtuniv$-rule is applied to an $s$ because of the presence of $\univinc x C$ in $S$, then $S' = S \cup \set{\inc s C}$. Since $(\I,\alpha)$ satisfies $S$ it holds that $\Int C = \dom$. Therefore $\al s \in \Int C$ and so $(\I,\alpha)$ satisfies $S'$. If the $\rtsome$-rule is applied to $\inc s\SOMERC$, then $S' = S \cup \set{\relc s P_1 y,\ldots, \relc s P_k y,\ \inc y C}$. Since $(\I,\alpha)$ satisfies $S$, there exists a $d$ such that $(\al s, d) \in \Int R$ and $d \in \Int C$. We define the $\I$-assignment $\alpha'$ as $\alpha'(y) := d$ and $\alpha'(t) := \al t$ for $t \neq y$. It is easy to show that $(\I,\alpha')$ satisfies $S'$. If the $\rtatleast$-rule is applied to $\inc s \ATLEAST n R$, then $S' = S \cup \set{\relc s P_1 y_i,\ldots,\relc s P_k y_i \mid i \in 1..n} \cup \set{\DISAGREE{y_i}{y_j} \mid i,j \in 1..n,i \neq j}$. Since $(\I,\alpha)$ satisfies $S$, there exist $n$ distinct elements $d_1,\ldots,d_n \in \dom$ such that $(\al s, d_i) \in \Int R$. We define the $\I$-assignment $\alpha'$ as $\alpha'(y_i) := d_i$ for $i \in 1..n$ and $\alpha'(t) := \al t$ for $t \not\in \set{y_1,\ldots,y_n}$. It is easy to show that $(\I,\alpha')$ satisfies $S'$. \vskip 1\baselineskip \noindent {\it 2.} \If Assume that $S'$ is satisfied by $(\I,\alpha')$. We show that $S$ is also satisfiable. If $S'$ is obtained from $S$ by application of the $\rtor$-rule, then $S$ is a subset of $S'$ and therefore satisfied by $(\I,\alpha')$. If $S'$ is obtained from $S$ by application of the $\rtatmost$-rule to $\inc s \ATMOST n R$ in $S$, then there are $y,t$ in $S$ such that $S' = S[y/t]$. We define the $\I$-assignment $\alpha$ as $\al y := \alpha'(t)$ and $\al v := \alpha'(v)$ for every object $v$ with $v \neq y$. Obviously $(\I,\alpha)$ satisfies $S$. \Onlyif Now suppose that $S$ is satisfied by $(\I,\alpha)$ and a nondeterministic rule is applicable to an object $s$. If the $\rtor$-rule is applicable to $\inc s{C_1\OR C_2}$ then, since $S$ is satisfiable, $\al s\in\Int{(C_1\OR C_2)}$. It follows that either $\al s\in\Int{C_1}$ or $\al s\in\Int{C_2}$ (or both). Hence, the $\rtor$-rule can obviously be applied in a way such that $(\I,\alpha)$ satisfies the resulting constraint system $S'$. If the $\rtatmost$-rule is applicable to $\inc s \ATMOST n R$, then---since $(\I,\alpha)$ satisfies $S$---it holds that $\al s \in \Int{\ATMOST n R}$ and therefore the set $\set{d \in \dom \mid (\al s, d) \in \Int R}$ 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 $(\al s, \al t) \in \Int R$. Thus, we can conclude by the Pigeonhole Principle \cite[page 26]{LePa81} that there exist at least two $R$-successors $t,t'$ of $s$ such that $\al t = \al{t'}$. Since $(\I,\alpha)$ satisfies $S$, the constraint $\DISAGREE{t}{t'}$ is not in $S$. Therefore one of the two must be a variable, let's say $t'=y$. Now obviously $(\I,\alpha)$ satisfies $S[y/t]$. % \qed Given a \cs\ $S$, more than one rule might be applicable to it. We define the following {\em strategy} for the application of rules: \begin{enumerate} \item apply a rule to a variable only if no rule is applicable to individuals; \item apply a rule to a variable $x$ only if no rule is applicable to a variable $y$ such that $y\prec x$; \item apply generating rules only if no nongenerating rule is applicable. \end{enumerate} The above strategy ensures that the variables are processed one at a time according to the ordering `$\prec$'. From this point on, we assume that rules are always applied according to this strategy and that we always start with a \cs\ $S_\Sigma$ coming from an $\ALCNR$-knowledge base $\Sigma$. The following lemma is a direct consequence of these assumptions. \begin{lemma}[Stability] \label{stability} Let $S$ be a \cs\ and $x$ be a variable in $S$. Let a generating rule be applicable to $x$ according to the strategy. Let $S'$ be any \cs\ derivable from $S$ by any sequence (possibly empty) of applications of rules. Then \begin{enumerate} \item No rule is applicable in $S'$ to a variable $y$ with $y\prec x$ \item $\SC S x = \SC {S'} x$ \item If $y$ is a variable in $S$ with $y \prec x$ then $y$ is a variable in $S'$, i.e., the variable $y$ is not substituted by another variable or by a constant. \end{enumerate} \end{lemma} % \proof % {\it 1.} By contradiction: Suppose $S \equiv S_0 \to_\ast S_1 \to_\ast \cdots \to_\ast S_n \equiv S'$, where $\ast \in \set{\OR,\AND,\exists,\forall,\geq,\leq,\forall x }$ and a rule is applicable to a variable $y$ such that $y\prec x$ in $S'$. Then there exists a minimal $i$, where $i \leq n$, such that this is the case in $S_i$. Note that $i \neq 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\prec x$ in $S_0,\ldots,S_{i-1}$. It follows that from $S_{i-1}$ to $S_i$ a rule is applied to $x$ or to a variable $w$ such that $x\prec w$. By an exhaustive analysis of all rules we see that---whichever is the rule applied from $S_{i-1}$ to $S_i$---no new constraint of the form $\inc y C$ or $\relc y R z$ can be added to $S_{i-1}$, and therefore no rule is applicable to $y$ in $S_i$, contradicting the assumption. \noindent {\it 2.} By contradiction: Suppose $\SC S x \neq \SC {S'} 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\prec x$, therefore the former case cannot be because of point {\it 1}. A case analysis shows that the only rules which can have been applied to $x$ are generating ones and the $\rtall$ and the $\rtatmost$ rules. But these rules add new constraints only to the direct successors of $x$ and not to $x$ itself and therefore do not change $\SC \cdot x$. % \noindent {\it 3.} This follows from point {\it 1.} and the strategy. \qed Lemma \ref{stability} proves that for a variable $x$ which has a direct successor, $\SC \cdot 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~\ref{stability}.2) from that point on $\SC \cdot x$ does not change. A \cs\ is {\em complete\/} if no propagation rule applies to it. A complete system derived from a system $S$ is also called a {\em completion\/} of $S$. A~{\em clash} is a \cs\ having one of the following forms: \begin{itemize} \item $\set{\inc s\bot}$ \item $\set{\inc s A,\ \inc s{\NOT A}}$, where $A$ is a concept name. \item \begin{tabbing} $\set{\inc s{\ATMOST n R}}$\= $\mbox{} \cup \set{\relc s{P_1}t_i ,\ldots, \relc s{P_k}t_i \mid i\in 1..n+1} $ \\%[0.8ex] \> $\mbox{} \cup \set{\DISAGREE{t_i}{t_j} \mid i,j \in 1..n+1, i \neq j}$, \\[0.8ex] where $\RISPS$. \end{tabbing} \end{itemize} A clash is evidently an unsatisfiable \cs. For example, the last case represents the situation in which an object has an at-most restriction and a set of $R$-successors that cannot be identified (either because they are individuals or because they have been created by some at-least restrictions). Any \cs\ 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 $S_\Sigma$ 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. \begin{example}% Consider the following knowledge base $\Sigma = \langle\T,\A \rangle$: \def\i{{\tt Italian}} \begin{tabbing} \indent$\T = \{\inclc {\i} {\SOME {\tt FRIEND}{\i}}\}$\\[0.8ex] \indent$\A = \{$\=$ {\tt FRIEND(peter,susan),}$\+\\ $\ALL {{\tt FRIEND}} {\NOT \i}({\tt peter}), $\\ $\SOME {{\tt FRIEND}} {\i} ({\tt susan})$\}\-\\[1.3ex] The corresponding \cs\ $S_{\Sigma}$ is:\\[1.3ex] \indent$S_{\Sigma} = \{$\=$\univinc x {\NOT \i\OR\SOME {\tt FRIEND}{\i}},$\+\\ $\relc {\tt peter} {\tt FRIEND} {\tt susan},$\\ $\inc {\tt peter} {\ALL {\tt FRIEND} {\NOT \i}},$\\ $\inc {\tt susan} {\SOME {\tt FRIEND} {\i}}$\\ ${\tt peter}\not\doteq{\tt susan}$\} \- \end{tabbing} \noindent A sequence of applications of the propagation rules to $S_{\Sigma}$ is as follows:\\[1.3ex] \indent $S_1 = S_{\Sigma} \cup \set{\inc {\tt susan} {\NOT \i}}$ ($\rtall$-rule) $S_2 = S_1 \cup \set{\inc {\tt peter} {\NOT \i\OR\SOME {FRIEND}{\i}}}$ ($\rtuniv$-rule) $S_3 = S_2 \cup \set{\inc {\tt susan} {\NOT \i\OR\SOME {FRIEND}{\i}}}$ ($\rtuniv$-rule) $S_4 = S_3 \cup \set{\inc {\tt peter} {\NOT \i}}$ ($\rtor$-rule) $S_5 = S_4 \cup \set{ \relc {\tt susan} {\tt FRIEND} {\tt x},\inc {\tt x} {\i}}$ ($\rtsome$-rule) $S_6 = S_5 \cup \set{\inc {\tt x} {\NOT \i\OR\SOME {FRIEND}{\i}}}$ ($\rtuniv$-rule) $S_7 = S_6 \cup \set{\inc {\tt x} {\SOME {FRIEND}{\i}}}$ ($\rtor$-rule) $S_8 = S_7 \cup \set{ \relc {\tt x} {\tt FRIEND} {\tt y},\inc {\tt y} {\i}}$ ($\rtsome$-rule) $S_9 = S_8 \cup \set{\inc {\tt y} {\NOT \i\OR\SOME {FRIEND}{\i}}}$ ($\rtuniv$-rule) $S_{10} = S_9 \cup \set{\inc {\tt y} {\SOME {FRIEND}{\i}}}$ ($\rtor$-rule)\\[1.3ex] % One can verify that $S_{10}$ is a complete clash-free constraint system. In particular, the $\rtsome$-rule is not applicable to $y$. In fact, since $x\equiv_{S_{10}} y$ condition 5 is not satisfied. From $S_{10}$ one can build an interpretation $\I$, as follows (again, we give only the interpretation of concept and role names):\\[1.3ex] % \indent $\dom = \set{{\tt peter},{\tt susan},{\tt x},{\tt y}}$ $\Int {\tt peter} = {\tt peter}$,~$\Int {\tt susan} = {\tt susan}$, $\alpha({\tt x}) = {\tt x}$, $\alpha({\tt y}) = {\tt y}$, $\Int{\i} = \set{{\tt x},{\tt y}}$ $\Int{\tt FRIEND}= \set{({\tt peter},{\tt susan}),({\tt susan},{\tt x}),({\tt x},{\tt y}), ({\tt y},{\tt y})}$\\[1.3ex] % It is easy to see that $\I$ is indeed a model for $\Sigma$. \qed \end{example} In order to prove that it is always possible to obtain an interpretation from a complete clash-free \cs\ we need some additional notions. Let $S$ be a \cs\ and $x$, $w$ variables in $S$. We call $w$ a {\em witness of $x$ in $S$} if the three following conditions hold: \begin{enumerate} \item $x\equiv_s w$ \item $w\prec x$ \item there is no variable $z$ such that $z\prec w$ and $z$ satisfies conditions 1.\ and 2.,\ i.e., $w$ is the least variable w.r.t.\ $\prec$ satisfying conditions 1.\ and 2. \end{enumerate} % We say {\em $x$ is blocked} ({\em by $w$}) in $S$ if $x$ has a witness ($w$) in $S$. The following lemma states a property of witnesses. \begin{lemma} \label{no-succ-for-blocked-vars} Let $S$ be a \cs, $x$ a variable in $S$. If $x$ is blocked then \begin{enumerate} \item $x$ has no direct successor and \item $x$ has exactly one witness. \end{enumerate} \end{lemma} \proof {\it 1.} By contradiction: Suppose that $x$ is blocked in $S$ and $\relc x P y$ is in $S$. During the completion process leading to $S$ a generating rule must have been applied to $x$ in a system $S'$. It follows from the definition of the rules that in $S'$ for every variable $w\prec x$ we had $x {\not\equiv}_{s'} w$. Now from Lemma~\ref{stability} we know, that for the \cs\ $S$ derivable from $S'$ and for every $w\prec x$ in $S$ we also have $x {\not\equiv}_s w$. Hence there is no witness for $x$ in $S$, contradicting the hypothesis that $x$ is blocked. \noindent {\it 2.} This follows directly from condition 3. for a witness. \qed As a consequence of Lemma \ref{no-succ-for-blocked-vars}, in a \cs\ $S$, if $w_1$ is a witness of $x$ then $w_1$ cannot have a witness itself, since both the relations `$\prec$' 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 \cs. We define the {\em canonical interpretation} $\IS$ and the {\em canonical $\IS$-assignment} $\alphaS$ as follows: \begin{enumerate} \item $\domS := \{s \mid s$ is an object in $S\}$ \item $\alS s := s$ \item $s \in \IntS A$ if and only if $\inc s A $ is in $S$ \item $(s,t) \in \IntS P$ if and only if \begin{enumerate} \item $\relc s P t$ is in $S$ \quad or \item $s$ is a blocked variable, $w$ is the witness of $s$ in $S$ and $\relc w P t$ is in $S$. \end{enumerate} \end{enumerate}\label{can-int} We call $(s,t)$ a {\em P-role-pair} of $s$ in $\IS$ if $(s,t) \in \IntS P$, we call $(s,t)$ a {\em role-pair} of $s$ in $\IS$ if $(s,t)$ is a {\em P-role-pair} for some role $P$. We call a role-pair {\em explicit} if it comes up from case 4.(a) of the definition of the canonical interpretation and we call it {\em implicit} if it comes up from case 4.(b). From Lemma~\ref{no-succ-for-blocked-vars} 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. \begin{lemma} \label{no-ex-im-mix} 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 \begin{enumerate} \item all role-pairs of $x$ in $\IS$ are implicit \item there is exactly one witness $w$ of $x$ in $S$ such that for all roles $P$ in $S$ and all $P$-role-pairs (x,y) of $x$, the constraint $\relc w P y$ is in $S$. \end{enumerate} \end{lemma} \proof The first statement follows from Lemma~\ref{no-succ-for-blocked-vars} (point {\it 1\/}). The second statement follows from Lemma~\ref{no-succ-for-blocked-vars} (point {\it 2\/}) together with the definition of $\IS$. \qed We have now all the machinery needed to prove the main theorem of this subsection. \begin{theorem}\label{completeness} Let $S$ be a complete \cs. If $S$ contains no clash then it is satisfiable. \end{theorem} %{\parindent0cm \proof % Let $\IS$ and $\alphaS$ be the canonical interpretation and canonical $\I$-assignment for $S$. We prove that the pair $(\IS,\alphaS)$ satisfies every constraint $c$ in $S$. If $c$ has the form $ \relc s P t$ or $\DISAGREE s t$, then $(\IS,\alphaS)$ satisfies them by definition of $\IS$ and $\alphaS$. Considering the $\rtatleast$-rule and the $\rtatmost$-rule we see that a constraint of the form $\DISAGREE s s$ can not be in $S$. If $c$ has the form $\inc s C$, we show by induction on the structure of $C$ that $s \in \IntS C$. We first consider the base cases. If $C$ is a concept name, then $s \in \IntS C$ by definition of $\IS$. If $C=\top$, then obviously $s \in \IntS \top$. The case that $C=\bot$ cannot occur since $S$ is clash-free. Next we analyze in turn each possible complex concept $C$. % If $C$ is of the form $\neg C_1$ then $C_1$ is a concept name since all concepts are simple. Then the constraint $\inc s C_1$ is not in $S$ since $S$ is clash-free. Then $s \not\in \IntS{C_1}$, that is, $s \in \domS \;\backslash\; \IntS {C_1}$. Hence $s \in \INTS{\neg C_1}$. If $C$ is of the form $C_1 \AND C_2$ then (since $S$ is complete) $\inc s C_1$ is in $S$ and $\inc s {C_2}$ is in $S$. By induction hypothesis, $s \in \IntS {C_1}$ and $s \in \IntS C_2$. Hence $s \in \INTS{C_1 \AND C_2}$. If $C$ is of the form $C_1 \OR C_2$ then (since $S$ is complete) either $\inc s C_1$ is in $S$ or $\inc s {C_2}$ is in $S$. By induction hypothesis, either $s \in \IntS {C_1}$ or $s \in \IntS C_2$. Hence $s \in \INTS{C_1 \OR C_2}$. If $C$ is of the form $\ALL R D$, we have to show that for all $t$ with $(s,t) \in \IntS R$ it holds that $t \in \IntS D$. If $(s,t) \in \IntS R$, then according to Lemma \ref{no-ex-im-mix} 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 $\inc t D$ must also be in $S$ since $S$ is complete. Then by induction hypothesis we have $t \in \IntS D$. In the second case by definition of witness, $\inc w \ALL R D$ is in $S$ and then because of completeness of $S$, $\inc t D$ must be in $S$. By induction hypothesis we have again $t \in \IntS D$. If $C$ is of the form $\SOME R D$ we have to show that there exists a $t \in \domS$ with $(s,t) \in \IntS R$ and $t \in \IntS D$. Since $S$ is complete, either there is a $t$ that is an $R$-successor of $s$ in $S$ and $\inc 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 \in \IntS D$ and $(s,t) \in \IntS R$. In the second case $\inc w \SOME R 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 $\inc t D$ is in $S$. So by induction hypothesis we have $t \in \IntS D$ and by the definition of $\IS$ we have $(s,t) \in \IntS R$. If $C$ is of the form $\ATMOST n R$ we show the goal by contradiction. Assume that $s \not\in \IntS{\ATMOST n R}$. Then there exist atleast $n+1$ distinct objects $t_1,\ldots,t_{n+1}$ with $(s,t_i) \in \IntS R,\ i \in 1..n+1$. This means that, since $\RISPS$, there are pairs $(s,t_i) \in \IntS {P_j}$, where $i \in 1..n+1$ and $j \in 1..k$. Then according to Lemma \ref{no-ex-im-mix} one of the two following cases must occur. Either all $\relc s P_j t_i$ for $j \in 1..k,\,i \in 1..n+1$ are in $S$ or there exists a witness $w$ of $s$ in $S$ with all $\relc w P_i t_i$ for $j \in 1..k$ and $i \in 1..n+1$ are in $S$. In the first case the $\rtatmost$-rule can not be applicable because of completeness. This means that all the $t_i$'s are pairwise separated, i.e., that $S$ contains the constraints $\DISAGREE {t_i} {t_j},~ i,j \in 1..n+1,i \neq 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 $\ATLEAST n R$ we show the goal by contradiction. Assume that $s \not\in \IntS{\ATLEAST n R}$. Then there exist atmost $m[page 41]{Wand80} we conclude that every object $s$ of $\Delta^{\I_{S'}}$ is in $A^{\I_{S'}}$. This proves that Equation \ref{a=dom} holds. From Equation \ref{a=dom}, and the fact that $\I_{S'}$ satisfies the inclusion $A^{\I_{S'}} \subseteq (C_\T)^{\I_{S'}}$, we derive that $(C_\T)^{\I_{S'}}=\Delta^{\I_{S'}}$, that is $\I_{S'}$ satisfies the equation $C_{\T}=\top$. Hence, from Proposition \ref{c=top}, $\I_{S'}$ satisfies $\T$, and this completes the proof of the theorem. \qed The machinery present in this proof is not new. In fact, realizing that the inclusions $\inclc A {\ALL {P_1} A},\dots,\inclc A {\ALL{P_n} A}$ simulate a transitive closure on the roles $P_1,\ldots,P_n$, one can recognize similarities with the proofs given by \citeB{Schi91} and \citeB{Baad90b}. The difference is that their proofs rely on the notion of {\em connected model} (Baader uses the equivalent notion of {\em 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 `$\OR$' and complement `$\NOT$' 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 $C_\T$. Therefore, the proof holds for $\ALC$-knowledge bases, but does not hold for TKRSs not allowing for these constructors of concepts (e.g., {\sc back}). Furthermore, for the language $\FL_0$ introduced in Section \ref{reasoning-techniques}, the opposite result holds. In fact, \citeB{McAl91} proves that computing subsumption w.r.t.\ a set of inclusions is EXPTIME-hard, even in the small language $\FL_0$. Conversely, \citeB{Nebe91} proves that subsumption w.r.t.\ a set of cyclic definitions in $\FL_0$ can be done in PSPACE. Combining the two results, we can conclude that for $\FL_0$ 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 $\neq$ PSPACE) inclusion statements are strictly more expressive than concept definitions in $\FL_0$. It is still open whether inclusions and definitions are equivalent in languages whose expressivity is between $\FL_0$ and $\ALC$. \section{Discussion}\label{sec-conclusions} In this paper we have proved the decidability of the main inference services of a TKRS based on the concept language $\ALCNR$. 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~\ref{sec-decidability}. 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 \cite{BHNPF92}. 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 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 \cite{MacG92}. 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 $\ALCNR$ can be applied also to unknown individuals (our variables in a \cs) without endangering decidability. This result is to be compared with the negative result in \cite{BaHo92}, where it is shown that subsumption becomes undecidable if rules are applied to unknown individuals in {\sc 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 \cite{HoBa91} should be taken into account. Also, the language resulting from the addition of enumerated sets (called {\sc one-of} in {\sc classic}), and role fillers to $\ALCNR$ 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 $\ALCNR$, since the finite model property is lost \cite{Schi91}. Finally, the addition of concrete domains \cite{BaHa91} remains open. \section*{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~\ref{sec-decidability}, 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''. \vskip 0.2in %\bibliographystyle{theapa} %\bibliography{/home/assi/bibliografie/terminologia} \begin{thebibliography}{} \bibitem[\protect\BCAY{Abrial}{Abrial}{1974}]{Abri74} Abrial, J. \BBOP1974\BBCP. \newblock \BBOQ Data semantics\BBCQ\ \newblock In Klimbie, J.\BBACOMMA\ \BBA\ Koffeman, K.\BEDS, {\Bem Data Base Management}, \BPGS\ 1--59. North-Holland Publ.\ Co., Amsterdam. \bibitem[\protect\BCAY{Baader}{Baader}{1990a}]{Baad90b} Baader, F. \BBOP1990a\BBCP. \newblock \BBOQ Augmenting concept languages by transitive closure of roles: An alternative to terminological cycles\BBCQ\ \newblock \BTR\ RR-90-13, Deutsches Forschungszentrum f{\"u}r K{\"u}nstliche Intelligenz (DFKI), Kaiserslautern, Germany. \newblock An abridged version appeared in {\Bem Proc.\ of the 12th Int.\ Joint Conf.\ on Artificial Intelligence IJCAI-91}, pp. 446--451. \bibitem[\protect\BCAY{Baader}{Baader}{1990b}]{Baad90} Baader, F. \BBOP1990b\BBCP. \newblock \BBOQ Terminological cycles in {KL-ONE}-based knowledge representation languages\BBCQ\ \newblock \BTR\ RR-90-01, Deutsches Forschungszentrum f{\"u}r K{\"u}nstliche Intelligenz (DFKI), Kaiserslautern, Germany. \newblock An abridged version appeared in {\Bem Proc.\ of the 8th Nat.\ Conf.\ on Artificial Intelligence AAAI-90}, pp. 621--626. \bibitem[\protect\BCAY{Baader, B{\"u}rkert, Hollunder, Nutt, \BBA\ Siekmann}{Baader et~al.}{1990}]{BBHN90} Baader, F., B{\"u}rkert, H.-J., Hollunder, B., Nutt, W., \BBA\ Siekmann, J.~H. \BBOP1990\BBCP. \newblock \BBOQ Concept logics\BBCQ\ \newblock In Lloyd, J.~W.\BED, {\Bem Computational Logics, Symposium Proceedings}, \BPGS\ 177--201. Springer-Verlag. \bibitem[\protect\BCAY{Baader \BBA\ Hanschke}{Baader \BBA\ Hanschke}{1991}]{BaHa91} Baader, F.\BBACOMMA\ \BBA\ Hanschke, P. \BBOP1991\BBCP. \newblock \BBOQ A schema for integrating concrete domains into concept languages\BBCQ\ \newblock In {\Bem Proc.\ of the 12th Int.\ Joint Conf.\ on Artificial Intelligence IJCAI-91}, \BPGS\ 452--457\ Sydney. \bibitem[\protect\BCAY{Baader \BBA\ Hollunder}{Baader \BBA\ Hollunder}{1991}]{BaHo91} Baader, F.\BBACOMMA\ \BBA\ Hollunder, B. \BBOP1991\BBCP. \newblock \BBOQ A terminological knowledge representation system with complete inference algorithm\BBCQ\ \newblock In {\Bem Proc.\ of the Workshop on Processing Declarative Knowledge, PDK-91}, Lecture Notes in Artificial Intelligence, \BPGS\ 67--86. Springer-Verlag. \bibitem[\protect\BCAY{Baader \BBA\ Hollunder}{Baader \BBA\ Hollunder}{1992}]{BaHo92} Baader, F.\BBACOMMA\ \BBA\ Hollunder, B. \BBOP1992\BBCP. \newblock \BBOQ Embedding defaults into terminological knowledge representation formalisms\BBCQ\ \newblock In {\Bem Proc.\ of the 3rd Int.\ Conf.\ on Principles of Knowledge Representation and Reasoning KR-92}, \BPGS\ 306--317. Morgan Kaufmann, Los Altos. \bibitem[\protect\BCAY{Baader, Hollunder, Nebel, Profitlich, \BBA\ Franconi}{Baader et~al.}{1992}]{BHNPF92} Baader, F., Hollunder, B., Nebel, B., Profitlich, H.-J., \BBA\ Franconi, E. \BBOP1992\BBCP. \newblock \BBOQ An empirical analisys of optimization techniques for terminological representation systems\BBCQ\ \newblock In {\Bem Proc.\ of the 3rd Int.\ Conf.\ on Principles of Knowledge Representation and Reasoning KR-92}, \BPGS\ 270--281. Morgan Kaufmann, Los Altos. \bibitem[\protect\BCAY{Beck, Gala, \BBA\ Navathe}{Beck et~al.}{1989}]{BeGN89} Beck, H.~W., Gala, S.~K., \BBA\ Navathe, S.~B. \BBOP1989\BBCP. \newblock \BBOQ Classification as a query processing technique in the {CANDIDE} semantic data model\BBCQ\ \newblock In {\Bem Proc.\ of the 5th IEEE Int.\ Conf.\ on Data Engineering}. \bibitem[\protect\BCAY{Borgida, Brachman, McGuinness, \BBA\ {Alperin Resnick}}{Borgida et~al.}{1989}]{BBMR89} Borgida, A., Brachman, R.~J., McGuinness, D.~L., \BBA\ {Alperin Resnick}, L. \BBOP1989\BBCP. \newblock \BBOQ {CLASSIC}: A structural data model for objects\BBCQ\ \newblock In {\Bem Proc.\ of the ACM SIGMOD Int.\ Conf.\ on Management of Data}, \BPGS\ 59--67. \bibitem[\protect\BCAY{Brachman \BBA\ Levesque}{Brachman \BBA\ Levesque}{1984}]{BrLe84} Brachman, R.~J.\BBACOMMA\ \BBA\ Levesque, H.~J. \BBOP1984\BBCP. \newblock \BBOQ The tractability of subsumption in frame-based description languages\BBCQ\ \newblock In {\Bem Proc.\ of the 4th Nat.\ Conf.\ on Artificial Intelligence AAAI-84}, \BPGS\ 34--37. \bibitem[\protect\BCAY{Brachman, {Pigman Gilbert}, \BBA\ Levesque}{Brachman et~al.}{1985}]{BrPL85} Brachman, R.~J., {Pigman Gilbert}, V., \BBA\ Levesque, H.~J. \BBOP1985\BBCP. \newblock \BBOQ An essential hybrid reasoning system: Knowledge and symbol level accounts in {KRYPTON}\BBCQ\ \newblock In {\Bem Proc.\ of the 9th Int.\ Joint Conf.\ on Artificial Intelligence IJCAI-85}, \BPGS\ 532--539\ Los Angeles. \bibitem[\protect\BCAY{Brachman \BBA\ Schmolze}{Brachman \BBA\ Schmolze}{1985}]{BrSc85} Brachman, R.~J.\BBACOMMA\ \BBA\ Schmolze, J.~G. \BBOP1985\BBCP. \newblock \BBOQ An overview of the {KL-ONE} knowledge representation system\BBCQ\ \newblock {\Bem Cognitive Science}, {\Bem 9\/}(2), 171--216. \bibitem[\protect\BCAY{Buchheit, Donini, \BBA\ Schaerf}{Buchheit et~al.}{1993}]{BuDS93b} Buchheit, M., Donini, F.~M., \BBA\ Schaerf, A. \BBOP1993\BBCP. \newblock \BBOQ Decidable reasoning in terminological knowledge representation systems\BBCQ\ \newblock \BTR\ RR-93-10, Deutsches Forschungszentrum f{\"u}r K{\"u}nstliche Intelligenz (DFKI), Saarbr\"ucken, Germany. \newblock An abridged version appeared in {\Bem Proc.\ of the 13th Int.\ Joint Conf.\ on Artificial Intelligence IJCAI-93} pp. 704--709. \bibitem[\protect\BCAY{Catarci \BBA\ Lenzerini}{Catarci \BBA\ Lenzerini}{1993}]{CaLe93b} Catarci, T.\BBACOMMA\ \BBA\ Lenzerini, M. \BBOP1993\BBCP. \newblock \BBOQ Representing and using interschema knowledge in cooperative information systems\BBCQ\ \newblock {\Bem Journal of Intelligent and Cooperative Inf.\ Syst.} \newblock To appear. \bibitem[\protect\BCAY{Dionne, Mays, \BBA\ Oles}{Dionne et~al.}{1992}]{DiMO92} Dionne, R., Mays, E., \BBA\ Oles, F.~J. \BBOP1992\BBCP. \newblock \BBOQ A non-well-founded approach to terminological cycles\BBCQ\ \newblock In {\Bem Proc.\ of the 10th Nat.\ Conf.\ on Artificial Intelligence AAAI-92}, \BPGS\ 761--766. {AAAI} Press/The {MIT} Press. \bibitem[\protect\BCAY{Dionne, Mays, \BBA\ Oles}{Dionne et~al.}{1993}]{DiMO93} Dionne, R., Mays, E., \BBA\ Oles, F.~J. \BBOP1993\BBCP. \newblock \BBOQ The equivalence of model theoretic and structural subsumption in description logics\BBCQ\ \newblock In {\Bem Proc.\ of the 13th Int.\ Joint Conf.\ on Artificial Intelligence IJCAI-93}, \BPGS\ 710--716\ Chambery, France. Morgan Kaufmann, Los Altos. \bibitem[\protect\BCAY{Donini, Hollunder, Lenzerini, Marchetti~Spaccamela, Nardi, \BBA\ Nutt}{Donini et~al.}{1992}]{DHLM92} Donini, F.~M., Hollunder, B., Lenzerini, M., Marchetti~Spaccamela, A., Nardi, D., \BBA\ Nutt, W. \BBOP1992\BBCP. \newblock \BBOQ The complexity of existential quantification in concept languages\BBCQ\ \newblock {\Bem Artificial Intelligence}, {\Bem 2--3}, 309--327. \bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, \BBA\ Nutt}{Donini et~al.}{1991a}]{DLNN91} Donini, F.~M., Lenzerini, M., Nardi, D., \BBA\ Nutt, W. \BBOP1991a\BBCP. \newblock \BBOQ The complexity of concept languages\BBCQ\ \newblock In Allen, J., Fikes, R., \BBA\ Sandewall, E.\BEDS, {\Bem Proc.\ of the 2nd Int.\ Conf.\ on Principles of Knowledge Representation and Reasoning KR-91}, \BPGS\ 151--162. Morgan Kaufmann, Los Altos. \bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, \BBA\ Nutt}{Donini et~al.}{1991b}]{DLNN91b} Donini, F.~M., Lenzerini, M., Nardi, D., \BBA\ Nutt, W. \BBOP1991b\BBCP. \newblock \BBOQ Tractable concept languages\BBCQ\ \newblock In {\Bem Proc.\ of the 12th Int.\ Joint Conf.\ on Artificial Intelligence IJCAI-91}, \BPGS\ 458--463\ Sydney. \bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, \BBA\ Schaerf}{Donini et~al.}{1991c}]{DLNS91} Donini, F.~M., Lenzerini, M., Nardi, D., \BBA\ Schaerf, A. \BBOP1991c\BBCP. \newblock \BBOQ A hybrid system integrating datalog and concept languages\BBCQ\ \newblock In {\Bem Proc.\ of the 2nd Conf.\ of the Italian Association for Artificial Intelligence}, \lowercase{\BNUM}\ 549 in Lecture Notes in Artificial Intelligence. Springer-Verlag. \newblock An extended version appeared also in the Working Notes of the AAAI Fall Symposium ``Principles of Hybrid Reasoning''. \bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, \BBA\ Schaerf}{Donini et~al.}{1993}]{DLNS93} Donini, F.~M., Lenzerini, M., Nardi, D., \BBA\ Schaerf, A. \BBOP1993\BBCP. \newblock \BBOQ Deduction in concept languages: From subsumption to instance checking\BBCQ\ \newblock {\Bem Journal of Logic and Computation}. \newblock To appear. \bibitem[\protect\BCAY{Fitting}{Fitting}{1990}]{Fitt90} Fitting, M. \BBOP1990\BBCP. \newblock {\Bem First-Order Logic and Automated Theorem Proving}. \newblock Springer-Verlag. \bibitem[\protect\BCAY{Garey \BBA\ Johnson}{Garey \BBA\ Johnson}{1979}]{GaJo79} Garey, M.\BBACOMMA\ \BBA\ Johnson, D. \BBOP1979\BBCP. \newblock {\Bem Computers and Intractability---A guide to {NP}-completeness}. \newblock W.H. Freeman and Company, San Francisco. \bibitem[\protect\BCAY{Harel}{Harel}{1984}]{Hare84} Harel, D. \BBOP1984\BBCP. \newblock \BBOQ Dynamic logic\BBCQ\ \newblock In {\Bem Handbook of Philosophical Logic}, \lowercase{\BVOL}~2, \BPGS\ 497--640. D. Reidel, Dordrecht, Holland. \bibitem[\protect\BCAY{Heinsohn, Kudenko, Nebel, \BBA\ Profitlich}{Heinsohn et~al.}{1992}]{HKNP92} Heinsohn, J., Kudenko, D., Nebel, B., \BBA\ Profitlich, H.-J. \BBOP1992\BBCP. \newblock \BBOQ An empirical analysis of terminological representation systems\BBCQ\ \newblock In {\Bem Proc.\ of the 10th Nat.\ Conf.\ on Artificial Intelligence AAAI-92}, \BPGS\ 767--773. {AAAI} Press/The {MIT} Press. \bibitem[\protect\BCAY{Hollunder}{Hollunder}{1990}]{Holl90} Hollunder, B. \BBOP1990\BBCP. \newblock \BBOQ Hybrid inferences in {KL-ONE}-based knowledge representation systems\BBCQ\ \newblock In {\Bem Proc.\ of the German Workshop on Artificial Intelligence}, \BPGS\ 38--47. Springer-Verlag. \bibitem[\protect\BCAY{Hollunder \BBA\ Baader}{Hollunder \BBA\ Baader}{1991}]{HoBa91} Hollunder, B.\BBACOMMA\ \BBA\ Baader, F. \BBOP1991\BBCP. \newblock \BBOQ Qualifying number restrictions in concept languages\BBCQ\ \newblock \BTR\ RR-91-03, Deutsches Forschungszentrum f{\"u}r K{\"u}nstliche Intelligenz (DFKI), Kaiserslautern, Germany. \newblock An abridged version appeared in {\Bem Proc.\ of the 2nd Int.\ Conf.\ on Principles of Knowledge Representation and Reasoning KR-91}. \bibitem[\protect\BCAY{Hughes \BBA\ Cresswell}{Hughes \BBA\ Cresswell}{1984}]{HuCr84} Hughes, G.~E.\BBACOMMA\ \BBA\ Cresswell, M.~J. \BBOP1984\BBCP. \newblock {\Bem A Companion to Modal Logic}. \newblock Methuen, London. \bibitem[\protect\BCAY{Kaczmarek, Bates, \BBA\ Robins}{Kaczmarek et~al.}{1986}]{KaBR86} Kaczmarek, T.~S., Bates, R., \BBA\ Robins, G. \BBOP1986\BBCP. \newblock \BBOQ Recent developments in {NIKL}\BBCQ\ \newblock In {\Bem Proc.\ of the 5th Nat.\ Conf.\ on Artificial Intelligence AAAI-86}, \BPGS\ 978--985. \bibitem[\protect\BCAY{Lenzerini \BBA\ Schaerf}{Lenzerini \BBA\ Schaerf}{1991}]{LeSc91} Lenzerini, M.\BBACOMMA\ \BBA\ Schaerf, A. \BBOP1991\BBCP. \newblock \BBOQ Concept languages as query languages\BBCQ\ \newblock In {\Bem Proc.\ of the 9th Nat.\ Conf.\ on Artificial Intelligence AAAI-91}, \BPGS\ 471--476. \bibitem[\protect\BCAY{Levesque}{Levesque}{1984}]{Leve84} Levesque, H.~J. \BBOP1984\BBCP. \newblock \BBOQ Foundations of a functional approach to knowledge representation\BBCQ\ \newblock {\Bem Artificial Intelligence}, {\Bem 23}, 155--212. \bibitem[\protect\BCAY{Lewis \BBA\ Papadimitriou}{Lewis \BBA\ Papadimitriou}{1981}]{LePa81} Lewis, H.~R.\BBACOMMA\ \BBA\ Papadimitriou, C.~H. \BBOP1981\BBCP. \newblock {\Bem Elements of the Theory of Computation}. \newblock Prentice-Hall, Englewood Cliffs, New Jersey. \bibitem[\protect\BCAY{Mac{G}regor}{Mac{G}regor}{1991}]{MacG90} Mac{G}regor, R. \BBOP1991\BBCP. \newblock \BBOQ Inside the {LOOM} description classifier\BBCQ\ \newblock {\Bem {SIGART} Bulletin}, {\Bem 2\/}(3), 88--92. \bibitem[\protect\BCAY{Mac{G}regor}{Mac{G}regor}{1992}]{MacG92} Mac{G}regor, R. \BBOP1992\BBCP. \newblock \BBOQ What's needed to make a description logic a good {KR} citizen\BBCQ\ \newblock In {\Bem Working Notes of the AAAI Fall Symposium on Issues on Description Logics: Users meet Developers}, \BPGS\ 53--55. \bibitem[\protect\BCAY{Mac{G}regor \BBA\ Bates}{Mac{G}regor \BBA\ Bates}{1987}]{MaBa87} Mac{G}regor, R.\BBACOMMA\ \BBA\ Bates, R. \BBOP1987\BBCP. \newblock \BBOQ The {L}oom knowledge representation language\BBCQ\ \newblock \BTR\ ISI/RS-87-188, University of Southern California, Information Science Institute, Marina del Rey, Cal. \bibitem[\protect\BCAY{Mac{G}regor \BBA\ Brill}{Mac{G}regor \BBA\ Brill}{1992}]{MaBr92} Mac{G}regor, R.\BBACOMMA\ \BBA\ Brill, D. \BBOP1992\BBCP. \newblock \BBOQ Recognition algorithms for the {LOOM} classifier\BBCQ\ \newblock In {\Bem Proc.\ of the 10th Nat.\ Conf.\ on Artificial Intelligence AAAI-92}, \BPGS\ 774--779. {AAAI} Press/The {MIT} Press. \bibitem[\protect\BCAY{Mays, Dionne, \BBA\ Weida}{Mays et~al.}{1991}]{MaDW91} Mays, E., Dionne, R., \BBA\ Weida, R. \BBOP1991\BBCP. \newblock \BBOQ {K-REP} system overview\BBCQ\ \newblock {\Bem {SIGART} Bulletin}, {\Bem 2\/}(3). \bibitem[\protect\BCAY{Mc{A}llester}{Mc{A}llester}{1991}]{McAl91} Mc{A}llester, D. \BBOP1991\BBCP. \newblock Unpublished manuscript. \bibitem[\protect\BCAY{Mc{G}uinness}{Mc{G}uinness}{1992}]{McGu92} Mc{G}uinness, D.~L. \BBOP1992\BBCP. \newblock \BBOQ Making description logic based knowledge representation systems more usable\BBCQ\ \newblock In {\Bem Working Notes of the AAAI Fall Sysmposium on Issues on Description Logics: Users meet Developers}, \BPGS\ 56--58. \bibitem[\protect\BCAY{Mylopoulos, Bernstein, \BBA\ Wong}{Mylopoulos et~al.}{1980}]{MyBW80} Mylopoulos, J., Bernstein, P., \BBA\ Wong, E. \BBOP1980\BBCP. \newblock \BBOQ A language facility for designing database-intensive applications\BBCQ\ \newblock {\Bem ACM Trans.\ on Database Syst.}, {\Bem 5\/}(2), 185--207. \bibitem[\protect\BCAY{Nebel}{Nebel}{1988}]{Nebe88} Nebel, B. \BBOP1988\BBCP. \newblock \BBOQ Computational complexity of terminological reasoning in {BACK}\BBCQ\ \newblock {\Bem Artificial Intelligence}, {\Bem 34\/}(3), 371--383. \bibitem[\protect\BCAY{Nebel}{Nebel}{1990}]{Nebe90b} Nebel, B. \BBOP1990\BBCP. \newblock {\Bem Reasoning and Revision in Hybrid Representation Systems}. \newblock Lecture Notes in Artificial Intelligence. Springer-Verlag. \bibitem[\protect\BCAY{Nebel}{Nebel}{1991}]{Nebe91} Nebel, B. \BBOP1991\BBCP. \newblock \BBOQ Terminological cycles: Semantics and computational properties\BBCQ\ \newblock In Sowa, J.~F.\BED, {\Bem Principles of Semantic Networks}, \BPGS\ 331--361. Morgan Kaufmann, Los Altos. \bibitem[\protect\BCAY{Nutt}{Nutt}{1992}]{Nutt92} Nutt, W. \BBOP1992\BBCP. \newblock Personal communication. \bibitem[\protect\BCAY{{Patel-Schneider}}{{Patel-Schneider}}{1984}]{Pate84} {Patel-Schneider}, P.~F. \BBOP1984\BBCP. \newblock \BBOQ Small can be beautiful in knowledge representation\BBCQ\ \newblock In {\Bem Proc.\ of the {IEEE} Workshop on Knowledge-Based Systems}. \newblock An extended version appeared as Fairchild Tech.\ Rep.\ 660 and {FLAIR} Tech.\ Rep.\ 37, October 1984. \bibitem[\protect\BCAY{{Patel-Schneider}}{{Patel-Schneider}}{1989}]{Pate89b} {Patel-Schneider}, P. \BBOP1989\BBCP. \newblock \BBOQ Undecidability of subsumption in {NIKL}\BBCQ\ \newblock {\Bem Artificial Intelligence}, {\Bem 39}, 263--272. \bibitem[\protect\BCAY{Pratt}{Pratt}{1978}]{Prat78} Pratt, V.~R. \BBOP1978\BBCP. \newblock \BBOQ A practical decision method for propositional dynamic logic\BBCQ\ \newblock In {\Bem Proc.\ of the 10th ACM SIGACT Symp.\ on Theory of Computing STOC-78}, \BPGS\ 326--337. \bibitem[\protect\BCAY{Quantz \BBA\ Kindermann}{Quantz \BBA\ Kindermann}{1990}]{QuKi90} Quantz, J.\BBACOMMA\ \BBA\ Kindermann, C. \BBOP1990\BBCP. \newblock \BBOQ Implementation of the {BACK} system version 4\BBCQ\ \newblock \BTR\ {KIT}-Report 78, {FB} Informatik, Technische Universit{\"a}t Berlin, Berlin, Germany. \bibitem[\protect\BCAY{{Rich, editor}}{{Rich, editor}}{1991}]{Rich91} {Rich, editor}, C. \BBOP1991\BBCP. \newblock \BBOQ {SIGART} bulletin. {S}pecial issue on implemented knowledge representation and reasoning systems\BBCQ\ \newblock (2)3. \bibitem[\protect\BCAY{Schaerf}{Schaerf}{1993a}]{Scha93} Schaerf, A. \BBOP1993a\BBCP. \newblock \BBOQ On the complexity of the instance checking problem in concept languages with existential quantification\BBCQ\ \newblock {\Bem Journal of Intelligent Information Systems}, {\Bem 2}, 265--278. \newblock An abridged version appeared in {\Bem Proc.\ of the 7th Int.\ Symp.\ on Methodologies for Intelligent Systems ISMIS-93}. \bibitem[\protect\BCAY{Schaerf}{Schaerf}{1993b}]{Scha93c} Schaerf, A. \BBOP1993b\BBCP. \newblock \BBOQ Reasoning with individuals in concept languages\BBCQ\ \newblock \BTR\ 07.93, Dipartimento di Informatica e Sistemistica, Universit{\`a} di Roma ``La Sapienza''. \newblock An abridged version appeared in {\Bem Proc.\ of the 3rd Conf.\ of the Italian Association for Artificial Intelligence AI*IA-93}. \bibitem[\protect\BCAY{Schild}{Schild}{1988}]{Schi88} Schild, K. \BBOP1988\BBCP. \newblock \BBOQ Undecidability of subsumption in {$\cal U$}\BBCQ\ \newblock \BTR\ {KIT}-Report 67, {FB} Informatik, Technische Universit{\"a}t Berlin, Berlin, Germany. \bibitem[\protect\BCAY{Schild}{Schild}{1991}]{Schi91} Schild, K. \BBOP1991\BBCP. \newblock \BBOQ A correspondence theory for terminological logics: Preliminary report\BBCQ\ \newblock In {\Bem Proc.\ of the 12th Int.\ Joint Conf.\ on Artificial Intelligence IJCAI-91}, \BPGS\ 466--471\ Sydney. \bibitem[\protect\BCAY{{Schmidt-Schau{\ss}}}{{Schmidt-Schau{\ss}}}{1989}]{Schm% 89} {Schmidt-Schau{\ss}}, M. \BBOP1989\BBCP. \newblock \BBOQ Subsumption in {KL-ONE} is undecidable\BBCQ\ \newblock In Brachman, R.~J., Levesque, H.~J., \BBA\ Reiter, R.\BEDS, {\Bem Proc.\ of the 1st Int.\ Conf.\ on Principles of Knowledge Representation and Reasoning KR-89}, \BPGS\ 421--431. Morgan Kaufmann, Los Altos. \bibitem[\protect\BCAY{{Schmidt-Schau{\ss}} \BBA\ Smolka}{{Schmidt-Schau{\ss}} \BBA\ Smolka}{1991}]{ScSm91} {Schmidt-Schau{\ss}}, M.\BBACOMMA\ \BBA\ Smolka, G. \BBOP1991\BBCP. \newblock \BBOQ Attributive concept descriptions with complements\BBCQ\ \newblock {\Bem Artificial Intelligence}, {\Bem 48\/}(1), 1--26. \bibitem[\protect\BCAY{Vardi \BBA\ Wolper}{Vardi \BBA\ Wolper}{1986}]{VaWo86} Vardi, M.\BBACOMMA\ \BBA\ Wolper, P. \BBOP1986\BBCP. \newblock \BBOQ Automata-theoretic techniques for modal logics of programs\BBCQ\ \newblock {\Bem Journal of Computer and System Science}, {\Bem 32}, 183--221. \newblock A preliminary version appeared in {\Bem Proc.\ of the 16th ACM SIGACT Symp.\ on Theory of Computing STOC-84}. \bibitem[\protect\BCAY{Vilain}{Vilain}{1991}]{Vila91} Vilain, M. \BBOP1991\BBCP. \newblock \BBOQ Deduction as parsing: Tractable classification in the {KL-ONE} framework\BBCQ\ \newblock In {\Bem Proc.\ of the 9th Nat.\ Conf.\ on Artificial Intelligence AAAI-91}, \BPGS\ 464--470. \bibitem[\protect\BCAY{Wand}{Wand}{1980}]{Wand80} Wand, M. \BBOP1980\BBCP. \newblock {\Bem Induction, Recursion, and Programming}. \newblock North-Holland Publ.\ Co., Amsterdam. \bibitem[\protect\BCAY{Woods \BBA\ Schmolze}{Woods \BBA\ Schmolze}{1992}]{WoSc92} Woods, W.~A.\BBACOMMA\ \BBA\ Schmolze, J.~G. \BBOP1992\BBCP. \newblock \BBOQ The {KL-ONE} family\BBCQ\ \newblock In Lehmann, F.\BED, {\Bem Semantic Networks in Artificial Intelligence}, \BPGS\ 133--178. Pergamon Press. \newblock Published as a special issue of {\it Computers \& Mathematics with Applications}, Volume 23, Number 2--9. \end{thebibliography} \end{document}