\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<see>{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<see>{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<see>[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<except for>[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<see>{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<e.g.,>[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<e.g., the language $\FL$ in>{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<e.g.,>[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<see e.g.,>[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<n$ ($m$ possibly 0) distinct objects
$t_1,\ldots,t_m$ with $(s,t_i) \in \IntS R,\ i \in 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 $\rtatleast$-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 $\rtatleast$-rule is applicable to $w$.
But this leads to the same contradiction.

If $c$ has the form $\univinc x D$ then, since $S$ is complete, for
each object $t$ in $S$, $\inc t D$ is in $S$---and, by the previous cases,
$t \in \IntS D$.
Therefore, the pair $(\IS,\alphaS)$ satisfies $\univinc x D$.
Finally, since $(\IS,\alphaS)$ satisfies all constraints in $S$,
$(\IS,\alphaS)$ satisfies $S$.
\qed
%}

\begin{theorem}[Correctness]\label{correctness}
A \cs\ $S$ is satisfiable if and only if there exists at least one
clash-free completion of $S$.
\end{theorem}
%
\proof
\If
Follows immediately from  Theorem~\ref{completeness}.
\Onlyif
Clearly, a system containing a clash is unsatisfiable. If every completion of
$S$ is unsatisfiable, then from Proposition~\ref{invariance} $S$, is
unsatisfiable.
\qed

\subsection{Termination and complexity of the calculus}

Given a \cs\ $S$, we call  $n_S$ the number of concepts appearing in
$S$, including also all the concepts appearing as a substring of another
concept. Notice that $n_S$ is bounded by the length
of the string expressing $S$.

\begin{lemma}\label{two-to-the-n}
Let $S$ be a \cs\ and let 
$S'$ be derived from $S$ by means of the propagation rules.
In any set of variables in $S'$ including more than $2^{n_S}$ 
variables there are at
least two variables $x$,$y$ such that $x \equiv_{s'} y$.
\end{lemma} 
\proof 
Each constraint $\inc x C \in S'$ may contain only concepts of the
\cs\ $S$. Since there are $n_S$ such concepts, given a variable
$x$ there cannot be more than $2^{n_S}$ different sets of constraints
$\inc x C$ in $S'$.
\qed

\begin{lemma}\label{number-of-predecessors}
Let $S$ be a \cs\ and
let $S'$ be any \cs\ derived from $S$ by applying the propagation rules with the
given strategy. Then, in $S'$ there are at most $2^{n_S}$ non-blocked
variables.   
\end{lemma}
\proof
Suppose there are  $2^{n_S}+1$ non-blocked variables. From
Lemma~\ref{two-to-the-n},  we know that in $S'$ there are at least 
two variables $y_1$,
$y_2$ such that $y_1 \equiv_s y_2$. 
Obviously either $y_1\prec y_2$ or $y_2\prec y_1$
holds; suppose that  $y_1\prec y_2$.
From the definitions of witness and blocked either $y_1$ is a witness of $y_2$ or
there exists a variable $y_3$ such that $y_3\prec y_1$ and $y_3$ is a witness
of $y_2$. In both cases $y_2$ is blocked, contradicting the hypothesis. 
\mbox{ }\qed

\begin{theorem}[Termination and space complexity] \label{termination}
Let $\Sigma$  be an 
$\ALCNR$-knowledge base and let $n$ be its size. Every
completion of $S_{\Sigma}$ is finite and its size is  $O(2^{4n})$.
\end{theorem}
\proof
Let $S$ be a completion of $S_{\Sigma}$. From Lemma~\ref{number-of-predecessors} it
follows that there are at most $2^n$ non-blocked variables in $S$. Therefore
there are at most $m\times 2^n$ 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 $\SOMERC$ 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 $2^n$. Hence, $m \leq 2^n + n$.
Since the number of
individuals is also bounded by  $n$, the total number of objects
in $S$ is at most $m\times(2^n + n) \le (2^n + n)\times(2^n + n)$, that is,
$O(2^{2n})$.

The number of different constraints of the form $\inc s C$, $\univinc 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\times n\times 2^{2n}$, that is $O(2^{3n})$.

The number of constraints of the form $sPt$, $\DISAGREE s t$ is bounded by
$(2^{2n})^2 = 2^{4n}$, and each constraint has constant size.

In conclusion, we have that the size of $S$ is $O(2^{4n})$. 
\qed

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
$2^{3n}$.

\begin{theorem}[Decidability]
Given an $\ALCNR$-knowledge base $\Sigma$, checking whether $\Sigma$ is
satisfiable is a decidable problem.
\end{theorem}
\proof  
This follows from Theorems \ref{correctness} and \ref{termination}
and the fact that $\Sigma$ is satisfiable if and only if
$S_\Sigma$ is satisfiable.
\qed

We can refine the above theorem, by giving tighter bounds on the time
required  to decide satisfiability.

\begin{theorem}[Time complexity]
Given an $\ALCNR$-knowledge base $\Sigma$, checking \linebreak whether $\Sigma$ is
satisfiable can be done in nondeterministic exponential time.
\end{theorem}
\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~\ref{termination}) and
each rule, but the $\rtatmost$-rule, adds new constraints to the \cs, it follows
that all such rules are applied at most an exponential number of times.
Regarding the  $\rtatmost$-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.  
\qed


A lower bound of the complexity of KB-satisfiability is obtained 
exploiting previous results about the language $\ALC$, which is 
a sublanguage of $\ALCNR$ that does not include number restrictions and 
role conjunction.
We know from \citeB{McAl91}, and (independently) from an observation by
\citeB{Nutt92} that KB-satisfiability in $\ALC$-knowledge bases is
EXPTIME-hard (see \cite[page 183]{GaJo79} for a definition) and hence it is hard
for $\ALCNR$-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 \cite[Sec.4]{BuDS93b},
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 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
$\sigma(\cdot,\cdot)$, in different \cs s. This could be avoided if we allow a
variable to be blocked by a witness that is in a {\em previously analyzed} \cs.
This technique would be similar to the one used in \cite{Prat78}, and to the
tree-automata technique used in \cite{VaWo86}, improving on simple tableaux
methods for variants of propositional dynamic logics. Since our calculus
considers only one \cs\ 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 
$\domS$ is always finite, we have also implicitly proved that 
$\ALCNR$-knowledge bases have the {\em finite model property},
i.e., any satisfiable knowledge base has a finite model.
This property has been extensively studied in modal 
logics \cite{HuCr84} and dynamic 
logics \cite{Hare84}.
In particular, a technique, called {\em 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 $\rtatleast$-rule). Nevertheless,
they can have the same direct successors, as stated in point
4.(b) of the definition of canonical interpretation on page
\pageref{can-int}.
This would correspond to grouping variables of an infinite model
in such a way that separations are preserved.
\section{Relation to previous work}\label{sec-prevwork}

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.

\subsection{Reasoning Techniques}\label{reasoning-techniques}
As mentioned in the introduction, previous results were obtained by
\citeB{BBHN90},
\citeB{Baad90b,Baad90},
\citeB{Nebe90b,Nebe91},
\citeB{Schi91} and 
\citeB{DiMO92,DiMO93}.

\citeB[Chapter 5]{Nebe90b} considers the language ${\cal TF}$, 
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 ${\cal TF}$-concepts w.r.t.\ a TBox is decidable.  However, the
argument he uses is non-constructive: He shows that it is sufficient to
consider finite interpretations of a size bounded by the size of the TBox in
order to decide subsumption.

In \cite{Baad90} the effect of the three types of semantics---descriptive,
greatest fixpoint and least fixpoint semantics---for the language
${\cal FL}_0$, containing concept conjunction and universal quantification,
is described with the help of {\em finite automata}.
Baader reduces subsumption of ${\cal FL}_0$-concepts w.r.t.\ a TBox containing
(possibly cyclic) definitions of the form $A\deq 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 {\em B\"uchi automata}.
Using results from \cite{Baad90}, in \cite{Nebe91} 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 \cite{BBHN90} 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=\top$, where $C$ is an $\ALC$-concept.
This problem, called the {\em universal satisfiability problem}, is shown 
to be equivalent to checking the satisfiability of an $\ALC$-TBox (see
Proposition~\ref{c=top}).

In \cite{Baad90b}, an extension of $\ALC$, called $\ALC_{reg}$, 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 $\inclc A D$ with equivalent acyclic ones.
The problem of checking the satisfiability of an
$\ALC_{reg}$-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=\set{\inclc {C_1}{D_1},\dots,\inclc{C_n}{D_n}}$ 
into the concept satisfiability problem in $\ALC_{reg}$ (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 \cite{BBHN90}.

The technique exploited in \cite{BBHN90} and \cite{Baad90b} is based on the notion of
{\em 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 \cs\ is generated
from the \cs\ $\set{\inc x C}$.
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 \cs s is immediate,
provided that additional features have a counterpart in First Order Logic.

In \cite{Schi91} some results more general than those in \cite{Baad90b} are
obtained by considering languages more expressive than $\ALC_{reg}$ 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).

Recently, an algebraic approach to cycles has been proposed in \cite{DiMO92},
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 \cite{DiMO93} 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 {\sc k-rep}, and contains conjunction and existential-universal
quantifications combined into one construct (hence it is similar to ${\cal
FL}_0$). 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 \cs\ technique, even though it was 
conceived for TBox-reasoning, can be easily extended to ABox-reasoning, 
as also shown in \cite{Holl90,BaHo91,DLNS93}.

\subsection{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 ~\dot\leq~ D$ and $A\deq D$. 

Unlike \cite{Baad90b} and \cite{Schi91}, 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=\langle\A,\T\rangle$, where $\T$ is a set of inclusion
statements, can be reduced to the satisfiability of a knowledge base
$\Sigma'=\langle\A',\T'\rangle$ such that $\T'$ is a set of
concept introductions. The other direction, from concept
introductions to inclusions, is trivial since 
introductions of the form $A\deq D$ can be expressed by the pair of inclusions
$\inclc A D$ and $\inclc D A$, while  a concept name specification
$A ~\dot\leq~ D$ can be rewritten as the inclusion $\inclc A D$
(as already mentioned in Section~\ref{sec-preliminaries}).

As a notation, given a TBox $\T=\set{\inclc
{C_1}{D_1},\dots,\inclc{C_n}{D_n}}$, we define the concept $C_\T$ as 
$C_{\T}=(\NOT C_1\OR D_1)\AND\cdots\AND(\NOT C_n\OR D_n)$.
As pointed out in \cite{Baad90b} for $\ALC$, an interpretation satisfies a TBox
$\T$ if and only if it satisfies the equation $C_{\T}=\top$. This result easily
extends to $\ALCNR$, as stated in the following proposition.

\begin{proposition}\label{c=top}
Given an $\ALCNR$-TBox  $\T=\set{\inclc {C_1}{D_1},\dots,\inclc{C_n}{D_n}}$,
an interpretation $\I$ satisfies $\T$ if and only if it satisfies the equation
$C_\T=\top$.
\end{proposition}
\proof
An interpretation $\I$ satisfies an inclusion $\inclc C
D$ if and only if it satisfies  the equation $\NOT C\OR D =\top$; $\I$ satisfies the set of
equations $\NOT C_1\OR D_1=\top$,\dots, $\NOT C_n\OR D_n=\top$
if and only if $\I$ satisfies $(\NOT C_1\OR D_1)\AND\cdots\AND (\NOT C_n\OR D_n)=\top$. The claim follows.
\qed

Given a knowledge base $\Sigma=\langle\A,\T\rangle$ and
a concept $A$ not appearing in $\Sigma$, we define the knowledge base
$\Sigma'=\langle\A',\T'\rangle$ as follows: 
\begin{eqnarray*} 
\A'	&=&	\A\cup\set{A(b) \mid \mbox{$b$ is an individual in $\Sigma$}}\\
\T'	&=& \set{A ~\dot\leq~ {C_\T\AND\ALL {P_1} A \AND\cdots \AND\ALL{P_n} A}}
\end{eqnarray*}
where $P_1,P_2,\dots,P_n$ are all the role names appearing in
$\Sigma$. Note that $\T'$ has a single inclusion, which could be also thought of
as one primitive concept specification.


\begin{theorem}
$\Sigma=\langle\A,\T\rangle$ is satisfiable if and only if
$\Sigma'=\langle\A',\T'\rangle$ 
is satisfiable.
\end{theorem}
%
\proof
In order to simplify the machinery of the proof, we will use for $\T'$ the
following (logically equivalent) form: $$\T' = \set{\inclc A {C_\T}, \inclc
A {\ALL {P_1} A},\dots,\inclc A {\ALL {P_n} A}}$$ (Note that we use the symbol
`$\sqsubseteq$' instead of `$\dot\leq$' because now the
concept name $A$ appears as the left-hand side of many statements, we must
consider these statements as inclusions).

\Onlyif
Suppose $\Sigma=\langle\A,\T\rangle$ satisfiable. From
Theorem~\ref{correctness},  there exists a complete \cs\ $S$ without clash,
which defines a canonical interpretation $\IS$ which is a model of $\Sigma$.
Define the \cs\ $S'$ as follows:
	$$S'=S\cup\set{\inc w A \mid \mbox{$w$ is an object in $S$}}$$ 
and call $\I_{S'}$ the canonical interpretation associated to $S'$. We prove that $\I_{S'}$
is a model of $\Sigma'$. 

First observe that every assertion in $\A$ is satisfied by $\I_{S'}$
since $\I_{S'}$ is equal to $\IS$ except for the interpretation of
$A$, and $A$ does not appear in $\A$. Therefore, 
every assertion in $\A'$ is also satisfied by $\I_{S'}$, either because it is an
assertion of $\A$, or (if it is an assertion of the form $A(b)$) by definition of $S'$. 

Regarding $\T'$,
note that by definition of $S'$, we have
$A^{\I_{S'}}=\Delta^{\I_{S'}}=\domS$; therefore both sides of the inclusions of the form $\inclc A
{\ALL {P_i} A}$ ($i=1,\dots,n$) are
interpreted as $\Delta^{\I_{S'}}$, hence they are satisfied by $\I_{S'}$.
Since $A$ does not appear in $C_\T$, we have that
$(C_\T)^{\I_{S'}}=(C_\T)^{\I_{S}}$.
Moreover, since $\IS$ satisfies $\T$, we also have, by Proposition \ref{c=top}, that $\INTS{C_{\T}}=\domS$,
therefore $(C_\T)^{\I_{S'}}=(C_\T)^{\I_S}=\domS=\Delta^{\I_{S'}}$.
It follows that also both sides of the inclusion $\inclc A
{C_\T}$ are interpreted as $\Delta^{\I_{S'}}$. In conclusion, $\I_{S'}$ satisfies $\T'$.

\If
Suppose $\Sigma'=\langle\A',\T'\rangle$ satisfiable.  
Again, because of Theorem~\ref{correctness},  there exists a complete \cs\ $S'$
without clash, which defines a canonical interpretation $\I_{S'}$ which is a
model of $\Sigma'$. We show that $\I_{S'}$ is also a model of $\Sigma$.

First of all, the assertions in $\A$ are satisfied because $\A \incl \A'$, and
$\I_{S'}$ satisfies every assertion in $\A'$. To prove that $\I_{S'}$ satisfies
$\T$, we first prove the following equation:
\begin{equation}
A^{\I_{S'}}=\Delta^{\I_{S'}}\label{a=dom}
\end{equation}
Equation \ref{a=dom} is proved by showing that, for every object
$s\in\Delta^{\I_{S'}}$, $s$ is in $A^{\I_{S'}}$.  In order to do that, observe
a general property of \cs s: Every variable in $S'$ is a successor of an
individual. This comes from the definition of the generating rules, which add
variables to the \cs\ only as direct successors of existing objects, and at the
beginning $S_{\Sigma'}$ contains only individuals.

Then, Equation~\ref{a=dom} is proved by observing the following three facts:
\begin{enumerate}

   \item for every individual $b$ in $\Delta^{\I_{S'}}$, $b\in A^{\I_{S'}}$;

   \item if an object $s$ is in $A^{\I_{S'}}$, then because $\I_{S'}$ satisfies 
the inclusions $A^{\I_{S'}} \subseteq (\ALL {P_1}A)^{\I_{S'}},\ldots,$\\
$A^{\I_{S'}} \subseteq (\ALL
{P_n}A)^{\I_{S'}}$, every direct successor of $s$ is in $A^{\I_{S'}}$;

   \item the successor relation is closed under the direct successor relation

\end{enumerate}

From the Fundamental Theorem on Induction \cite<see e.g.,>[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<as shown in>{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}