\documentstyle[jair,twoside,11pt,theapa]{article}
%\documentstyle[jair,twoside,11pt]{article}

\vbadness=2000

\ShortHeadings{Subsumption in CLASSIC}{Borgida \& Patel-Schneider}
\jairheading{1}{1994}{277--308}{3/94}{6/94}
\firstpageno{277}


\title{A Semantics and Complete Algorithm for\\
    Subsumption in the CLASSIC Description Logic}
\author{\name Alex Borgida \email borgida@cs.rutgers.edu\\
	\addr Department of Computer Science\\
		Rutgers University\\
		New Brunswick, NJ~~08904 U. S. A.
	\AND
	\name Peter F. Patel-Schneider \email pfps@research.att.com\\
	\addr AT\&T Bell Laboratories\\
		600 Mountain Avenue\\
		Murray Hill, NJ~~07974 U. S. A.
  }

%%%START of terminological.sty
\newcommand{\notationdefs}{
%
	\def\thing{\top}
	\def\bottom{\bot}
	\def\identity{\imath}
%
	\def\And{\sqcap}
	\def\AND{\;\sqcap\;}
	\def\Or{\sqcup}
	\def\OR{\;\sqcup\;}
	\def\Not{\neg}
	\def\NOT{\neg\:}
%
	\def\all##1##2{\forall ##1 {:} ##2}
	\def\All##1##2{\forall \, ##1 : ##2}
	\def\some##1{\exists ##1}
	\def\Some##1{\exists \, ##1}
	\def\atmost##1##2{{\leq}##1 \, ##2}
	\def\Atmost##1##2{{\leq}##1 \: ##2}
	\def\atleast##1##2{{\geq}##1 \, ##2}
	\def\Atleast##1##2{{\geq}##1 \: ##2}
	\def\equal##1##2{{=}##1 \, ##2}
	\def\Equal##1##2{{=}##1 \: ##2}
%
	\def\qsome##1##2{\exists ##1 {:} ##2}
	\def\Qsome##1##2{\exists \, ##1 : ##2}
	\def\qatmost##1##2##3{{\leq}##1 \, ##2 {:} ##3}
	\def\Qatmost##1##2##3{{\leq}##1 \: ##2 : ##3}
	\def\qatleast##1##2##3{{\geq}##1 \, ##2 {:} ##3}
	\def\Qatleast##1##2##3{{\geq}##1 \: ##2 : ##3}
	\def\qequal##1##2##3{{=}##1 \, ##2 {:} ##3}
	\def\Qequal##1##2##3{{=}##1 \: ##2 : ##3}
%
	\def\same##1##2{##1 \,{=}\, ##2}
	\def\Same##1##2{##1 = ##2}
	\def\notsame##1##2{##1 \,{\neq}\, ##2}
	\def\Notsame##1##2{##1 \neq ##2}
	\def\subset##1##2{##1 \,{\subseteq}\, ##2}
	\def\Subset##1##2{##1 \subseteq ##2}
	\def\asame##1##2{##1 \,{\stackrel{\downarrow}{\raisebox{0ex}[0.7ex][0ex]{=}}}\, ##2}
	\def\Asame##1##2{##1 \stackrel{\downarrow}{\raisebox{0ex}[0.7ex][0ex]{=}} ##2}
	\def\anotsame##1##2{##1 \,{\stackrel{\downarrow}{\raisebox{0ex}[0.7ex][0ex]{$\neq$}}}\, ##2}
	\def\Anotsame##1##2{##1 \stackrel{\downarrow}{\raisebox{0ex}[0.7ex][0ex]{$\neq$}} ##2}
%
	\def\fills##1##2{##1 \,{:}\, ##2}
	\def\Fills##1##2{##1 : ##2}
	\def\less##1##2{##1 \,{<}\, ##2}
	\def\Less##1##2{##1 < ##2}
	\def\greater##1##2{##1 \,{>}\, ##2}
	\def\Greater##1##2{##1 > ##2}
	\def\set##1{\{ ##1 \}}
	\def\Set##1{\{ \; ##1 \; \}}
%
	\def\inverse##1{##1^{-1}}
	\def\Inverse##1{##1{}^{-1}}
	\def\restrict##1##2{##1 \,{\mid} ##2}
	\def\Restrict##1##2{##1 \mid\! ##2}
	\def\compose{{\circ}}
	\def\Compose{\circ}
	\def\product##1##2{##1 {\times} ##2}
	\def\Product##1##2{##1 \times ##2}
	\def\trans##1{##1^+}
	\def\Trans##1{##1{}^+}
	\def\transref##1{##1^*}
	\def\Transref##1{##1{}^*}
%
	\def\define##1##2{##1 \doteq ##2}
	\def\Define##1##2{##1 \;\;\doteq\;\; ##2}
	\def\defineprim##1##2{##1 \sqsubseteq ##2}
	\def\Defineprim##1##2{##1 \;\;\sqsubseteq\;\; ##2}
	\def\definedisjprim##1##2##3{##1 \sqsubseteq_{##2} ##3}
	\def\Definedisjprim##1##2##3{##1 \;\;\sqsubseteq_{##2}\;\; ##3}
%
	\def\instance##1##2{##1 \in ##2}
	\def\Instance##1##2{##1 \;\;\in\;\; ##2}
	\def\related##1##2##3{\langle ##1, ##2 \rangle \in ##3}
	\def\Related##1##2##3{\langle ##1, ##2 \rangle \;\;\in\;\; ##3}
%
	\def\rule##1##2{##1 \rightarrow ##2}
	\def\Rule##1##2{##1 \;\;\rightarrow\;\; ##2}
	\def\fulldefault##1##2##3{##1/##2 \leadsto ##3}
	\def\Fulldefault##1##2##3{##1 \;\;/\;\; ##2 \;\;\leadsto\;\; ##3}
	\def\default##1##2{##1 \leadsto ##2}
	\def\Default##1##2{##1 \;\;\leadsto\;\; ##2}
	\def\close##1##2{##1 \bigcirc ##2}
	\def\Close##1##2{##1 \;\;\bigcirc\;\; ##2}
%
	\def\test##1{##1}
	\def\prim##1##2{\sqsubseteq_{##1} ##2}
	\def\disjprim##1##2##3{\sqsubseteq_{##1,##2} ##3}
	\def\closed##1{\bigcirc ##1}
%
	\def\max##1{{\leq}##1}
	\def\min##1{{\geq}##1}
}


\def\M#1{\relax\ifmmode #1\else$#1$\fi}

\newcommand{\notationfont}{\sf}

\newenvironment{notation}{\relax \ifmmode \def\@notation{\relax}\else \def\@notation{\end{math}}\begin{math}\fi\notationfont\notationdefs}{\@notation{}}

\newenvironment{displaynotation}{\begin{quote}$\notationfont\notationdefs}{$\end{quote}}

\newcommand{\syntax}[1]{\begin{notation}#1\end{notation}{}}

\newcommand{\name}[1]{\begin{notation}\mbox{#1}\end{notation}{}}
%%%END of terminological.sty

\def\inj{\Upsilon}
\newcommand{\pw}{\M{{\cal I}}}
\newcommand{\intr}[1]{{\M{#1^{\cal I}}}}
\newcommand{\DD}{\M{\Delta}}
\newcommand{\expl}[1]{{\em (Reason: {\small #1})}}
\newtheorem{algorithm}{Algorithm}
\newtheorem{definition}{Definition}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}

\newcommand{\proof}{\par \noindent {\bf Proof:} \rm}
\newcommand{\qed}{\vrule height1ex width1ex depth0pt}

\newcommand{\system}[1]{{\sc #1}}
\newcommand{\classic}{\system{classic}}

%STARTSTART

\begin{document}

\maketitle

\begin{abstract}
This paper analyzes the correctness of the subsumption algorithm used
in \classic{}, a description logic-based knowledge representation
system that is being used in practical applications.  In order to deal
efficiently with individuals in \classic{} descriptions, the
developers have had to use an algorithm that is incomplete with
respect to the standard, model-theoretic semantics for description
logics. We provide a variant semantics for descriptions with respect
to which the current implementation is complete, and which can be
independently motivated.  The soundness and completeness of the
polynomial-time subsumption algorithm is established using description
graphs, which are an abstracted version of the implementation
structures used in \classic{}, and are of independent interest.
\end{abstract}

\section{Introduction to Description Logics}

Data and knowledge bases are models of some part of the natural world. 
Such models are often built from individual objects that are 
inter-related by relationships and grouped into classes that capture
commonalities among their instances.
{\em Description logics} (DLs), also known as {\em terminological logics},
form a class of languages used to build and access such models; 
their distinguishing feature is that classes 
(usually called {\em concepts}) 
can be {\em defined intensionally}---in terms of descriptions that specify
the properties that objects must satisfy to belong to the concept. 
These descriptions are expressed using some language that allows the
construction of composite descriptions, including  restrictions on the
binary relationships (usually called {\em roles}) 
connecting objects.

As an example, consider the description
$$\syntax{
   GAME \AND
	\atleast{4}{participants}	\AND
	\all{participants}{ (PERSON \And
\fills{gender}{Female})}}.\footnote{The notation used for descriptions here
is the standard notation in the description logic community
\shortcite{baader-et-al:notation}.
The \classic{} notation is not used because it is more verbose.}$$
This description characterizes objects in the intersection 
(\begin{notation} \And{}{} \end{notation}) of three sub-descriptions: 
\syntax{GAME}---objects that belong to the atomic concept;
\syntax{\atleast{4}{participants}}---objects with at least four fillers for
	the \name{participants} role; 
and
\syntax{\all{participants}{(PERSON \And \fills{gender}{Female})}}---objects
all of whose \name{participants} fillers are restricted to belong to
\name{PERSON}s, which themselves have \name{gender} role filled by the
value \name{Female}. 

A key difference between DLs and the standard representation
formalisms based on First-Order Logic, e.g., relational and 
deductive databases, is that DLs provide an arena for exploring new sets of
 ``logical connectives''---the constructors used to form
composite descriptions---that are different from the standard connectives
such as conjunction, universal quantifiers, etc.. Therefore, DLs provide a new
space in which to search for expressive yet effectively computable
representation languages.  
Moreover, although it is possible to translate many aspects of DLs
currently encountered into First Order Logic, reasoning with such a
translation would be a very poor substitute because DL-based systems
reason in a way that does not resemble standard theorem proving (e.g., by
making use of imperative programming features). 

Descriptions such as the one above can be used in several ways
in a  knowledge base management system (KBMS) based on a description logic:
\begin{enumerate} 
\item {\em To state queries:} The KBMS can locate all the objects
	that satisfy the description's properties.
\item {\em To define and classify concepts}: 
	Identifiers can be attached to descriptions, in the manner of views in
	relational DBMSs. 
	The system can in addition automatically determine the ``subclass''
	relationship between pairs of such concepts based on their definitions.
	For example, a concept defined by the above description would be
	subsumed by a concept defined by
	``games with at least two participants''
	(\begin{notation} GAME  \And \atleast{2}{participants} \end{notation}).
\item {\em To provide partial information about objects}:
	It is important to understand that distinct DL descriptions can be
	ascribed to arbitrary individuals (e.g., ``today's game of
	cards---individual \name{Bgm\#467}---will have exactly two participants
	from the following set of three \ldots, all of whom like tea and rum''). 
	Note that unlike database systems, DL-based KBMSs do not require
	descriptions to be predefined.
	This provides considerable power in recording partial knowledge about
	objects.
\item {\em To detect errors}: It is possible to 
	determine whether two descriptions are disjoint,
	whether a description is incoherent or not, and whether ascribing a
	description to an individual leads to an inconsistency.
\end{enumerate}

Quite a number of KBMSs based on description logics have been built,
including \classic{} \shortcite{resnick-et-al:classic-manual}, 
\system{loom} \shortcite{macgregor-bates:loom}, 
and \system{back} \shortcite{peltason-et-al:back-users-guide}.
Such systems have been used in several practical situations, including
software information bases \shortcite{devanbu-et-al:lassie-cacm}, 
financial management \shortcite{mays-et-al:financing}, 
configuration management
\shortcite{owsnicki-klewe:configuration,wright-et-al:prose},
and data exploration. 
Additional signs that DLs are significant subjects of study are the several
recent workshops on DLs
\shortcite{dagstuhl-workshop,berlin-taxonomic-workshop,fss-92-dl}.


\subsection{On the Tractability and Completeness of DL Implementations}

The fundamental operation on descriptions is determining whether one
description is more general, or {\em subsumes}, another, in
the sense that any object satisfying the latter would also satisfy the
conditions of the former.
In parallel with the surge of work on finding tractable yet expressive
subsets of first order logic, the DL research community has been
investigating the complexity of reasoning with
various constructors. 
The first result in this area
\shortcite{levesque-brachman:tractability}
showed that even a seemingly simple addition to a  
very small language can lead to subsumption determination becoming
NP-hard. 
A more recent, striking pair of results 
\shortcite{patel-schneider:nikl-undecidable,schmidt-schauss:undecidable} 
shows that adding the
ability to represent equalities of role compositions makes the complexity
of the subsumption problem leap from quadratic to {\em undecidable}.


There are three possible responses to these intractability results:
\begin{itemize}
\item Provide an {\em incomplete implementation} of the DL reasoner, in the
sense that there are inferences sanctioned by the standard semantics of the
constructors that are not performed by the algorithm. This approach,
explicitly adopted by the \system{loom} system implementers
\shortcite{macgregor-bates:loom}, 
and advocated by some users \shortcite{doyle-patil:two-theses}, has one major
difficulty: how can 
one describe to users the inferences actually drawn by the implementation so
that systems with known properties can be implemented on top of such KBMS?
Two solutions to this problem have been suggested: alternative semantic
accounts (based on weaker, 4-valued logics, for example)
\shortcite{patel-schneider:terminological-logic},
and proof-theoretic semantics \shortcite{borgida:natural-semantics}.

\item Provide a {\em complete implementation} of a specific DL reasoner,
acknowledging that in certain circumstances it may take an inordinate
amount of time. This approach, followed in systems such as \system{kris}
\shortcite{baader-hollunder:kris}, 
has the problem of unpredictability: when will the system ``go off into the
wild blue yonder''? And of course, in some circumstances this is impossible
to even attempt since the reasoning problem is undecidable.

\item Carefully devise a {\em language of limited expressive power\/} for
which reasoning is  tractable, and then  provide a complete
implementation for it. 
This was the approach chosen by the designers of such languages as
\system{kandor} \shortcite{patel-schneider:small} 
and \system{krypton} \shortcite{brachman-et-al:krypton}, and
is close to the approach in \classic{} \shortcite{borgida-et-al:classic-sigmod}.
\end{itemize} 

A hidden difficulty in the second and third approach is to produce an
implementation that is correct (``complete'') with respect to the semantics.
This difficulty is illustrated by the discovery, several years later, that
the implementation of \system{kandor}, as well as \system{candide} \shortcite{beck-et-al:candide},
was in fact incomplete, and its subsumption 
problem is NP-hard \shortcite{nebel:back-complexity}, rather than
polynomial, as was claimed; this happened despite the
fact that 
\system{Kandor} is a very ``small'' language in comparison with other DLs, and its
implementation appeared to be evidently correct.
To avoid such problems, it is necessary to produce convincing
demonstrations that the algorithm is correct; several such proofs have
in fact  already appeared in the DL literature (e.g.,
\shortcite{patel-schneider:thesis,hollunder-nutt:subsumption-algorithms,donini-et-al:tractable}),
albeit only for languages that have not seen use in practical applications.

\subsection{Outline}


The \classic{} 1\footnote{\classic{} 1 is the first released version of
\classic{}.  A new version, \classic{} 2, with a more expressive DL, has
recently been released.} system is a reasoner based on a moderately complicated DL.
It is being used in commercial \shortcite{wright-et-al:prose} and prototype
applications at AT\&T, and
is made available to academic researchers by AT\&T Bell Laboratories.

One purpose of this paper is to provide a rigorous formal analysis of
the correctness and efficiency for the \classic{} DL subsumption
algorithm.\footnote{In empirical tests \shortcite{heinsohn-et-al:empirical}, \classic{} has
emerged as the fastest of the current DL implementations.}
We start by presenting such a result for a subset of the language,
which we call Basic \classic{}.  The subsumption algorithm relies on
the transformation of descriptions into a data structure, which we
call {\em description graphs}, and which are a generalization of
A\"\it-Kaci's psi-terms \citeyear{ait-kaci:thesis}. 
In the process of
normalizing such a graph to a canonical form, we remove obvious
redundancies and explicate certain implicit facts, encoding in
particular the infinite set of inferences that can be drawn from
so-called ``coreference constraints''.  The correctness of the
subsumption algorithm is demonstrated rigorously by showing
how to construct (inductively) a counter-model in case the algorithm
returns the answer ``no''.

Next, we explore the effect of adding individuals to descriptions.  We
show that, using individuals, one can encode disjunctive information
leading to the need to examine combinatorially many possibilities.
  The \classic{} implementation is in fact incomplete
with respect to the standard semantics. The second contribution of
this paper is then a well-motivated, understandable, and small change
to the standard semantics that alleviates this problem. We  extend
the subsumption algorithm and its proof of correctness to deal with
individuals under the modified semantics, thereby characterizing in
some sense the ``incompleteness'' of the reasoner.

This paper therefore illustrates all three paradigms described above,
albeit in a non-standard manner for the second paradigm, and does so
for the first time on a realistic language with significant practical
use.

\section{Basic {\sc CLASSIC}}\label{basic}

Descriptions in Basic \classic{} are built up from a collection of {\em
atomic} concept names, role names, and attribute names. 
Roles and attributes are always atomic but descriptions can be built up
using operators/constructors such as value restrictions and number
restrictions, as we indicate below.

Basic \classic{} incorporates objects from the host programming
language,\footnote{A general scheme for incorporating such host objects is
described in \shortcite{baader-hanschke:concrete-domains}.} 
called {\em host individuals}, which form a distinct group from {\em classic
individuals}; only the latter can have roles or attributes of their own,
the former being restricted to be role or attribute fillers.

The denotational semantics of \classic{} descriptions starts, as usual, with
a domain of values, \DD, subsets of which are extensions for descriptions,
while subsets of $\DD \times \DD$ are extensions of roles and attributes.
This domain is in fact disjointly divided into two {\em realms}, 
the {\em host realm}, $\DD_H$, containing objects corresponding to host
language individuals,  
and the {\em classic realm} $\DD_C$, containing the other objects.  
Every description, except for \name{THING}, which denotes the entire
domain has as its extension a subset of either the classic realm or
the host realm. (\name{NOTHING} denotes the empty set, which is
therefore both a classic and host concept.)
The extension of a role in a possible world is a relation from the
classic realm to the entire domain, while the extension of an attribute is a
function from the classic realm into the entire domain.

Host descriptions are relatively simple: (i) \name{HOST-THING},
denoting the entire host realm, $\DD_H$; (ii) special, pre-defined
names corresponding to the types in the host programming language; and
(iii) conjunctions of the above descriptions.  The descriptions
corresponding to the host programming language types have pre-defined
extensions and subsumption relationships, mirroring the subtype
relationship in the host programming language.  This subtype
relationship is satisfied in all possible worlds/interpretations.  
We require that 
(i) all host concepts have an extension that is either of infinite size or is empty;
(ii) that if the extensions of two host concepts overlap, then one must be subsumed
by the other, i.e., types are disjoint, unless they are subtypes of each other;
and (iii) that a host concept has an infinite number of extra instances
than each of its child concepts.
(These conditions are needed to avoid
being able to infer conclusions from the size of host descriptions.)
This allows for host concepts like
\name{INTEGER}, \name{REAL}, \name{COMPLEX}, and \name{STRING},
but not \name{BOOLEAN} or \name{NON-ZERO-INTEGER}.


Non-host (classic) descriptions in Basic \classic{} are formed according to
the following syntax:
\begin{quote}
\begin{tabular}{l@{\hspace*{1em}}l}
Syntax & Constructor Name \\[1ex]
\name{CLASSIC-THING} & \\
\syntax{E} & Atomic Concept Name\\
\syntax{C \And D} & Intersection \\
\syntax{\all{R}{C}} & Role Value Restriction \\
\syntax{\all{A}{C}} & Attribute Value Restriction \\
\syntax{\atleast{n}{R}} & Minimum Number Restriction \\
\syntax{\atmost{m}{R}} & Maximum Number Restriction \\
\syntax{\same{A_1 \compose \ldots \compose A_k}{B_1 \compose \ldots
\compose B_h}} & Equality Restriction
\end{tabular}
\end{quote}
where \name{E} is an atomic concept name;
\name{C} and \name{D} are classic descriptions;
\name{R} is a role;
\name{A}, \syntax{A_i}, and \syntax{B_j} are attributes;
\name{n,k,h} are  positive integers;
and \name{m} is a non-negative integer.
The set of constructors in Basic \classic{} was judiciously
chosen to result in a language in which subsumption is easy to compute.

The denotational semantics for descriptions in Basic \classic{} is
recursively built on the extensions assigned to atomic names by a
possible world: 
\begin{definition}\label{desc-extension}
A possible world/interpretation, $\pw$, consists of a domain, $\DD$, and
an interpretation function $\intr{.}$.
The domain is disjointly divided into a classic realm, $\DD_C$, and a host
realm, $\DD_H$.
The interpretation function assigns extensions to atomic identifiers as
follows: 
\begin{itemize}
\item  The extension of an atomic concept name \name{E} is some subset
	\intr{\name{E}} of the classic realm.
\item The extension of an atomic role name \name{R} is some subset
	\intr{\name{R}} of $\DD_C \times \DD$.
\item The extension of an atomic attribute name \name{A} is some total function
	\intr{\name{A}} from $\DD_C$ to \DD.
\end{itemize}
The extension \intr{\syntax{C}} of a non-atomic classic description
is computed as follows:
\begin{itemize}
\item $\intr{\name{CLASSIC-THING}} = \DD_C$.
\item $\intr{(\syntax{C \And D})} = \intr{\syntax{C}} \cap
	\intr{\syntax{D}}$.
\item $\intr{\syntax{(\all{p}{C})}} = 
	\{ d \in \DD_C \mid \forall x \ (d,x) \in \intr{\name{p}}\
		\Rightarrow \ x \in \intr{\name{C}}\}$, i.e.,
	those objects in  $\DD_C$
	all of whose \name{p}-role or \name{p}-attribute fillers are in the
	extension of \name{C}; 
\item $\intr{\syntax{(\atleast{n}{p})}}$ 
	(resp. $\intr{\syntax{(\atmost{n}{p})}}$)
	is those objects in $\DD_C$ with at least (resp. at most) \name{n}
	fillers for role \name{p}.
\item $\intr{\syntax{(\same{\syntax{A_1} \compose \ldots \compose
	\syntax{A_k}}{\syntax{B_1} \compose \ldots \compose \syntax{B_h}})}}
	= \{ d \in \DD_C \mid
	 \intr{\syntax{A_k}}(\ldots\intr{\syntax{A_1}}(d)) \; =\;   
         \intr{\syntax{B_h}}(\ldots \intr{\syntax{B_1}}(d))  \}$, i.e.,
 	those objects in $\DD_C$ with the property that applying the
	composition of the extension of the \syntax{A_i}s and the
	composition of the extension of the \syntax{B_j}s to the object
	both result in the same value.\footnote{Note that both attribute
chains must have a definite value, and that all but the last cannot
evaluate to host individuals, since these cannot have attributes.}
\end{itemize}
A description, $\syntax{D_1}$, is then said to {\em subsume} another,
$\syntax{D_2}$, if for all possible worlds $\pw$,  $\intr{\syntax{D_2}}
\subseteq  \intr{\syntax{D_1}}$.  

\end{definition}


Of key interest is the computation of the subsumption relationship between
descriptions in Basic \classic{}.
Subsumption computation is a multi-part process.
First, descriptions are turned into description graphs.  
Next, description graphs are put into canonical form, where certain
inferences are explicated and other redundancies are reduced by
combining nodes and edges in the graph.
Finally, subsumption is determined between a description and a
canonical description graph. 

To describe in detail the above process, we start with a
formal definition of the notion of description graph
(Definition~\ref{dg-def}), and then present techniques for
\begin{itemize}
\item translating a description to a description graph 
(Section~\ref{transl}),  which requires  merging pairs of nodes, and
pairs of graphs (Definitions~\ref{node-merge} and \ref{dg-merge}); 

\item putting a description graph into canonical form (Section~\ref{canon});

\item determining whether a description subsumes a description graph
(Algorithm~\ref{subsume}).
\end{itemize}

To prove the correctness of this approach, we need to show that
the first two steps lead us in the right direction, i.e., that the
following three questions are equivalent: ``Does description D subsume
description C?'', ``Does description D subsume graph $G_C$?'', and
``Does description D subsume graph $canonical(G_C)$?''. To do this, we
need to define the formal semantics of both descriptions and
graphs (Definitions~\ref{desc-extension} and \ref{dg-extension}), and
then prove the results (Theorems~\ref{translation lemma} and
\ref{canonical theorem}). To prove the ``completeness'' of
the subsumption algorithm, we  show that if the algorithm does not
indicate that D subsumes $canonical(G_C)$, then we can construct an
interpretation (``graphical world'') in which some object is in the
denotation of $canonical(G_C)$ but not that of D.

\subsection{Description Graphs}\label{cg-defn}


One way of developing a subsumption algorithm is to first transform
descriptions into a canonical form, and then determine subsumption
relationships between them. Canonical descriptions  can normally be
thought of as trees since descriptions are terms in a first order term
language. 
The presence of equality restrictions in \classic{} significantly
changes the handling of subsumption because they
 introduce relationships between different pieces of
the normal form. 
Most significantly, in the presence of equalities, a small description, 
such as  
\begin{notation}
\all{friend}{TALL} \And \same{friend}{friend \compose friend}
\end{notation},
can be subsumed by descriptions of arbitrary size,
such as 
$$\syntax{\all{friend}{(\all{friend}{(\ldots(\all{friend}{TALL})\ldots)})}}.$$
In order to record such sets of inferences in the canonical form, we will
resort to a graph-based representation, suggested by the
semantic-network origins of description logics, and the work of
A\"\it-Kaci \citeyear{ait-kaci:thesis}.


\medskip

Intuitively, a {\em description graph} is a labelled, directed multigraph,
with a distinguished node.
Nodes of the graph correspond to descriptions,
while edges of the graph correspond to restrictions on roles or attributes.
The edges of the graph are labelled with 
the role name and the minimum and maximum number of fillers associated with
the edge, 
or just with the attribute name.  
The nodes of the graph are labelled with concept names associated
with the node concept.  
For example, Figure~\ref{eg-graph} is a description graph, which, as we
shall see later, corresponds to the description 
\begin{notation}
 GAME \And \all{participants}{PERSON} \And
 \same{coach}{(captain \compose father)}
\end{notation}.

\begin{figure}

\begin{center}
\begin{picture}(250,80)(25,37)

\put(50,50){\circle*{5}}		% root node
\put(25,37){$\{\syntax{GAME}\}$}

\put(250,100){\circle*{5}}		% final node
\put(225,105){$\{\name{THING}\}$}

\put(100,100){\circle*{5}}		% intermediate node
\put(60,105){$\{\name{CLASSIC-THING}\}$}

\put(200,50){\circle*{5}}		% bottom node
\put(207,46){$\{\name{PERSON}\}$}

\put(50,50){\vector(4,1){193}}		% root to final
\put(160,70){\syntax{coach}}

\put(50,50){\vector(1,1){47}}		% root to intermediate
\put(44,75){\syntax{captain}}

\put(100,100){\vector(1,0){143}}	% intermediate to final
\put(175,102){\syntax{father}}

\put(50,50){\vector(1,0){147}}		% root to bottom
\put(130,53){\syntax{participants}}
\put(130,39){$[ 0 , \infty]$}

\end{picture}
\end{center}

\caption{A description graph.}\label{eg-graph}

\end{figure}

Because equality restrictions (and hence the non-tree portions of the
graph) involve only attributes, edges labelled with roles are all
cut-edges, i.e., their removal increases by one the number of
connected components of the graph. 
This restriction is important because if the graph is in tree form, there
is really no difference between a graphical and a linear notation, and a
semantics is simple to develop.  
If the graph is a general directed acyclic graph, then there is
the problem of relating the semantics generated by two different paths in
the graph that share the same beginning and ending nodes.  
If the graph contains cycles, the problem of developing a correct semantics
is even more difficult, as a simplistic semantics will be non-well-founded,
and some sort of fixed-point or model-preference semantics will be
required.  
Fortunately, any non-tree parts of our graphical notation will involve
attributes only, and because attributes are functional, our job will be
much easier.

As a result of the above restrictions, it is possible to view a description
graph as having the following recursive structure: 
(i) There is a distinguished node $r$, which has an ``island'' of nodes
connected to it by edges labelled with attributes.
(ii) Nodes in this island may have 0 or more edges labelled
with roles leaving them, pointing to distinguished nodes of other
description graphs. 
(iii) These graphs share no nodes or edges in common with
each other, nor with the islands above them. 

Because of this recursive structure, it is easier to represent description
graphs using a recursive definition, instead of the usual graph definition.
This recursive definition is similar to the recursive definition of a tree,
which states that a tree consists of some information (the information on
the root of the tree) plus a set of trees (the children of the root of the
tree).  
As description graphs are more complex than simple trees, we will have to
use a two-part definition.

\begin{definition}\label{dg-def}
A {\em description graph} is a triple, $\left<N,E,r\right>$,
consisting of a set $N$ of {\em nodes};
a bag $E$ of edges ({\em a-edges}) labelled with attribute names;
and a {\em distinguished node} $r$ in $N$.
Elements of $E$ will be written $\left<n_1,n_2,\syntax{A}\right>$
where $n_1$ and $n_2$ are nodes and \syntax{A} is an attribute name.

A {\em node} in a description graph is a pair, $\left<C,H\right>$ 
consisting of a set $C$ of concept names (the {\em atoms} of the node),
and a bag $H$ of tuples (the {\em r-edges} of the node).
An r-edge is a tuple, $\left<\syntax{R},m,M,G\right>$, of 
	a role name, $\syntax{R}$; 
 	a min, $m$, which is a non-negative integer;
	a max, $M$, which is a non-negative integer or $\infty$;
 and 	a (recursively nested) description graph $G$, representing the
restriction on the fillers of the role. 
($G$ will often be called the {\em restriction graph} of the node.)

{\em Concept names} in a description graph are atomic concept names, host
concept names, \name{THING}, \name{CLASSIC-THING}, or \name{HOST-THING}.

\end{definition}



\medskip

Descriptions graphs are provided extensions starting from the same
possible worlds $\pw$ as used for descriptions. However, in addition
we need a way of identifying the individuals to be related by
attributes, which will be given by the function $\inj$.
\begin{definition}\label{dg-extension}
Let $G = \left<N,E,r\right>$ be a description graph
and let $\pw$ be a possible world. 
Then the interpretation $\intr{G}$ of $G$, and the interpretation
$\intr{n}$ of each of the nodes in $N$, are recursively (and mutually)
defined as follows: 

An element, $d$, of $\DD$ is in $\intr{G}$,
iff
there is some function, $\inj $, from $N$ into $\DD$
such that 
\begin{enumerate}
\item $d = \inj (r)$;
\item for all $n \in N$  $\inj (n) \in \intr{n}$;
\item for all $ \left<n_1,n_2,\syntax{A}\right> \in E$ we have $
	\left<\inj (n_1),\inj (n_2)\right> \in \intr{\syntax{A}}$,
	(which is equivalent to 
	$\inj (n_2)=\intr{\syntax{A}}(\inj (n_1))$, 
	since $\intr{\syntax{A}}$ is a function).
\end{enumerate}

An element, $d$, of $\DD$ is in $\intr{n}$, 
where $n=\left< C,H\right>$,
iff
\begin{enumerate}
\item for all $\syntax{C} \in C$, we have $d \in \intr{\syntax{C}}$; 
		and
\item for all $\left<\syntax{R},m,M,G\right> \in H$,
	\begin{enumerate}
	\item there are between $m$ and $M$ elements, $d'$, of the domain 
		such that $\left<d,d'\right> \in \intr{\syntax{R}}$ and
	\item $d' \in \intr{G}$ for all $d'$ such that
		$\left<d,d'\right> \in \intr{\syntax{R}}$.
	\end{enumerate}
\end{enumerate}
\end{definition}


\subsection{Translating Descriptions to Description Graphs}\label{transl}

A Basic \classic{} description is turned into a description graph by a
recursive process, working from
the ``inside out''. 
In this process, description graphs and nodes are often merged.

\begin{definition}\label{node-merge}
The merge of two nodes, $n_1 \oplus n_2$, is a new node whose atoms are the
union of the atoms of the two nodes and whose r-edges are the
union of the r-edges of the two nodes\footnote{Note that duplicate edges,
such as ones joining $n_i$ to $n_i$, are not removed, since the edges form a bag.}.
\end{definition}

\begin{definition}\label{dg-merge}
The merge of two description graphs, $G_1 \oplus G_2$, is a
description graph whose nodes are the disjoint union\footnote{In
taking the disjoint union of two sets, elements of one may be
systematically renamed first to make sure that the sets are
non-overlapping.} of the non-distinguished nodes of $G_1$ and $G_2$
plus a new distinguished node.  The edges of the merged graph are the
union of the edges of $G_1$ and $G_2$, except that edges
touching on the distinguished nodes of $G_1$ or $G_2$ are modified to
touch the new distinguished node.  The new distinguished node is the
merge of the two distinguished nodes of $G_1$ and $G_2$.
\end{definition}
%It is easy to see that these merge operations are well-defined.


The rules for translating a description \syntax{C} in Basic
\classic{} into a description graph $G_{\syntax{C}}$ 
are as follows:
\begin{enumerate}
\item
A description that consists of a concept name
is turned into a description graph with one node and no a-edges.
The atoms of the node contains only the concept name.
The node has no r-edges.

\item
A description of the form
\syntax{\atleast{n}{\name{R}}}
is turned into a description graph with one node and no a-edges.
The node has as its atoms \name{CLASSIC-THING} and has a
single r-edge with role \name{R}, min $n$, max $\infty$,
and restriction $G_{\name{THING}}$.

\item
A description of the form
\syntax{\atmost{n}{\name{R}}}
is turned into a description graph with one node and no a-edges.
The node has as its atoms \name{CLASSIC-THING} and a
single r-edge with role \name{R}, min $0$, max $n$,
and restriction $G_{\name{THING}}$.

\item
A description of the form
\syntax{\all{\name{R}}{\syntax{C}}}, with \name{R} a role,
is turned into a description graph with one node and no a-edges.
The node has as its atoms \name{CLASSIC-THING} and has a
single r-edge with role \name{R}, min $0$, max $\infty$, and
restriction $G_{\syntax{C}}$.
 
\item
To turn a description of the form 
\syntax{C \And D}
into a description graph, 
construct $G_{\syntax{C}}$ and $G_{\syntax{D}}$
and merge them.

\item
To turn a description of the form 
\syntax{\all{\name{A}}{\syntax{C}}}, with \name{A} an attribute,
into a description graph,
first construct the description graph $\left<N_C,E_C,r_C\right>$ for
\syntax{C}. 
The description graph for \syntax{\all{\name{A}}{\syntax{C}}} is 
$\left<N_C \cup \{t\}, E_C \cup \{\left<t,r_C,\name{A}\right>\},t\right>$, 
where $t$ is the node $\left< \{ \name{CLASSIC-THING} \}, \{\} \right>$.

\item
To turn a description of the form
\syntax{\same{A_1 \compose \ldots \compose A_n}{B_1 \compose \ldots
	\compose B_m}}
into a description graph first create a distinguished node, node $r$, with
\name{CLASSIC-THING} as its atoms, 
and a node $e$, with \name{THING} as its atoms.
For $1 \leq i \leq n-1$ create a node $a_i$, 
with its atoms being \name{CLASSIC-THING}.
For $1 \leq j \leq m-1$ create a node $b_j$, 
with its atoms being \name{CLASSIC-THING}.
None of the $a_i$ or $b_j$ have r-edges.

If $n = 1$, 
create the edge $\left<r,e,\syntax{A_1}\right>$; if $n > 1$ 
then create  edges $\left<r,a_1,\syntax{A_1}\right>$, 
 $\left<a_{n-1},e,\syntax{A_n}\right>$, and 
$\left<a_{i-1},a_i,\syntax{A_i}\right>$ for $2 \leq i \leq n-1$.

Similarly,
if $m = 1$, 
create the edge $\left<r,e,\syntax{B_1}\right>$; if $m > 1$ 
then create  edges $\left<r,b_1,\syntax{B_1}\right>$, 
 $\left<b_{m-1},e,\syntax{B_m}\right>$, and 
$\left<b_{i-1},b_i,\syntax{B_i}\right>$ for $2 \leq i \leq m-1$.


This creates two disjoint paths, one for the \syntax{A_i} and one for the
\syntax{B_j}, from the distinguished node to the end node.
\end{enumerate}

Figure~\ref{eg-graph} presents a view of a description graph constructed in
this fashion from the description
\begin{notation}
\name{GAME} \AND 
\all{participants}{\name{PERSON}} \AND
\same{coach}{captain \compose father}.
\end{notation}

\medskip

Now we want to show that this process preserves extensions.
As we use the merge operations we first show that they work correctly.

\begin{lemma}\label{merge lemma}
If $n_1$ and $n_2$ are nodes then 
$\intr{(n_1 \oplus n_2)} = \intr{n_1} \cap \intr{n_2}$.
If $D_1$ and $D_2$ are description graphs then 
$\intr{(D_1 \oplus D_2)} = \intr{D_1} \cap \intr{D_2}$.
\proof{} 
Since the components (atoms and r-edges) of the merged node are
obtained by unioning the components of the respective nodes, and since
the interpretation of a node is the intersection of the interpretation of
its components, the result is obviously true for nodes.

For merging graphs, the only difference is that the root nodes are
replaced by their merger in all edges, as well as the root.
But then an element of $\intr{(D_1 \oplus D_2)}$ is clearly
 an element of both $\intr{D_1}$ and $\intr{D_2}$. Conversely,
since we take the
{\em disjoint} union of the other nodes in the two graphs, the
mapping functions $\inj_1$ and $\inj_2$ in
Definition~\ref{dg-extension} can simply be unioned, so that
an element of both $\intr{D_1}$ and $\intr{D_2}$
is an element of the merged root node, and hence of $\intr{(D_1 \oplus
D_2)}$. 
\qed
\end{lemma}

\begin{theorem} \label{translation lemma}
For all possible worlds, the extension of a description is the same as
the extension of its description graph. 
\proof{}
The proof is by structural induction on descriptions. 

The extension of concept names, cardinality restrictions, and
$\forall$-restrictions on roles can be easily seen  to agree with the
extension of description graphs formed from them.
Lemma~\ref{merge lemma} shows that conjunction is properly handled.
For $\forall$-restrictions on attributes, the construction is correct
because attributes are functional.

For equalities 
\begin{notation}
\same{\syntax{A_1} \compose \ldots \compose \syntax{A_n}}{\syntax{B_1}
\compose \ldots \compose \syntax{B_m}} 
\end{notation}
 the construction forms a description graph with two disjoint 
paths from the distinguished node to an end node, one labelled by the
\syntax{A_i}, through nodes $a_i$, and the other labelled by the
\syntax{B_j}, through nodes $b_j$.
If $$d \in 
(\syntax{\same{A_1 \compose \ldots \compose A_n}{B_1 \compose \ldots
\compose B_m}})\intr{} 
=  \{ d \in \DD_C \mid
	 \intr{\syntax{A_k}}(\ldots\intr{\syntax{A_1}}(d)) \; =\;   
         \intr{\syntax{B_h}}(\ldots \intr{\syntax{B_1}}(d))  \},$$ 
then defining $\inj(a_i) = 
	 \intr{\syntax{A_i}}(\ldots\intr{\syntax{A_1}}(d))$
and $\inj(b_j) = 
         \intr{\syntax{B_j}}(\ldots \intr{\syntax{B_1}}(d))  \}$, 
yields the mapping required by Definition~\ref{dg-extension}.
The converse is satisfied by the requirement in
Definition~\ref{dg-extension}
  that for each a-edge  $\left<n_1,n_2,\syntax{A}\right> \in E$, we have
$\inj(n_2)=\intr{\syntax{A}}(\inj(n_1))$.
\qed
\end{theorem}


\subsection{Canonical Description Graphs}\label{canon}

In the following sections we will occasionally refer to {\em ``marking
a node incoherent''}; this consists of replacing it with a special
node having no outgoing r-edges, and including in its atoms \name{NOTHING}, 
which always has the empty interpretation.  Marking a description graph as
incoherent consists of replacing it with a description graph
consisting only of an incoherent node. (Incoherent graphs are to be
thought of as representing concepts with empty extension.)

\medskip

Description graphs are transformed into canonical form by repeating the
following normalization steps whenever possible for the description graph
and all its descendants. 
\begin{enumerate}
%1
\item If some node has in its atoms a pre-defined host concept, 
	add \name{HOST-THING} to its atoms. 
	If some node has an atomic concept name in its atoms, add
	\name{CLASSIC-THING} to its atoms. 
	For each pre-defined host concept in the atoms of the node, add all
	the more-general pre-defined host concepts to its atoms.
%2
\item If some node has both \name{HOST-THING} and \name{CLASSIC-THING}
	in its atoms, mark the node incoherent.
	If some node has in its atoms a pair of  host concepts
	that are not related by the pre-defined subsumption
	relationship, mark the node incoherent, since their
	intersection will be empty.
%3
\item If any node in a description graph is marked incoherent, mark the
	description graph as incoherent. \expl{Even if the node is not a
	root, attributes must always have a value, and this value cannot
	belong to the empty set.} 
%4
\item If some r-edge in a node has its min greater than its max,
 	mark the node incoherent.
%5
\item If some r-edge in a node has its description graph marked incoherent,
	change its max to 0. \expl{It cannot have any fillers that belong
	to the empty set.} 
%6
\item If some r-edge in a node has a max of 0, 
	mark its description graph as incoherent. \expl{This normalization
step records the equivalence between 
\syntax{\atmost{0}{\name{R}}} and 
\syntax{\all{R}{NOTHING}}, and is used then to infer that a concept with  
 \syntax{\all{R}{C}} for arbitrary \syntax{C} subsumes
\syntax{\atmost{0}{\name{R}}}.}
%7
\item If some node has two r-edges labelled with the same role, merge
	the two edges, as described below.
%8
\item If some description graph has two a-edges from the same node labelled
	with the same attribute, merge the two edges.

\end{enumerate}

To {\em merge two r-edges} of a node, which have identical roles,
replace them with one r-edge.
The new r-edge has the role as its role,
the maximum of the two mins as its min,
the minimum of the two maxs as its max,
and the merge of the two description graphs as its restriction.

To {\em merge two a-edges} 
 $\left<n,n_1,\name{A}\right>$ and
$\left<n,n_2,\name{A}\right>$, replace them 
with a single new edge 
$\left<n,n',\name{A}\right>$, where $n'$ results from merging $n_1$ and
$n_2$, i.e., $n'\ = \ n_1 \oplus n_2$.  (If $n_1 = n_2$ then $n' = n_1$.)
In addition, replace $n_1$ and $n_2$ by $n'$ in all other a-edges of
this description graph.


\medskip

We need to show that the transformations to canonical form do not
change the extension of the graph.
The main difficulty is in showing that the two edge-merging processes do
not change the extension. 

\begin{lemma} \label{attribute merging extension lemma}
Let $G = \left<N,E,r\right>$ be a description graph with two mergeable
a-edges and let 
$G' = \left<N',E',r'\right>$ be the result of merging these two a-edges.
Then $\intr{G} = \intr{G'}$.
\proof{}
Let the two edges be $\left<n,n_1,\name{A}\right>$ and
$\left<n,n_2,\name{A}\right>$ and the new node $n'$ be $n_1 \oplus n_2$.

Choose $d \in \intr{G}$, and
let $\inj$ be a function from $N$ into the domain satisfying the conditions
for extensions (Definition~\ref{dg-extension}) such that $\inj(r) = d$.
Then $\inj(n_1) = \inj(n_2)$ because both are equal to
$\intr{\notation{A}}(\inj(n))$. 
Let $\inj '$ be the same as $\inj$ except that $\inj '(n') =
\inj(n_1)= \inj(n_2)$. Then $\inj '$ satisfies
Definition~\ref{dg-extension}, part 3, for $G'$, because we replace
$n_1$ and $n_2$ by $n'$ everywhere. Moreover, $\inj'(n') = \inj(n_1)\ \in\
\intr{n_1} \cap \intr{n_2}$, which, by Lemma~\ref{merge lemma}, equals
$\intr{(n_1 \oplus n_2)}$; so part 2 is satisfied too, since $n'= n_1
\oplus n_2$.  Finally, if the root is modified by the merger, i.e.,
$n_1$ or $n_2$ is $r$, say $n_1$, then $d=\inj(n_1)=\inj'(n')$, so part 1
of the definition is also satisfied.

\medskip

Conversely, given arbitrary $d \in \intr{G'}$,  let $\inj '$ be
the function stipulated by Definition~\ref{dg-extension} such that
$\inj '(r') = d$.  Let $\inj$ be the same as $\inj'$ except that
$\inj(n_1) = \inj(n')$ and $\inj(n_2) = \inj'(n')$.  Then the above
argument can be traversed in reverse to verify 
that $\inj $ satisfies Definition~\ref{dg-extension}, so that
 $d \in \intr{G}$.
\qed
\end{lemma}

\begin{lemma} \label{role merging extension lemma}
Let $n$ be a node with two mergeable r-edges
and let $n'$ be the node with these edges merged.
Then $\intr{n} = \intr{n'}$.
\proof{}
Let the two r-edges be $\left<\name{R},m_1,M_1,G_1\right>$ and
$\left<\name{R},m_2,M_2,G_2\right>$. 

Let $d \in \intr{n}$.
Then there are between $m_1$ ($m_2$) and $M_1$ ($M_2$) elements of the
domain, $d'$, such that $\left<d,d'\right> \in \intr{\syntax{R}}$.
Therefore there are between the maximum of $m_1$ and $m_2$ and 
		the minimum of $M_1$ and $M_2$ elements of the domain, $d'$,
such that $\left<d,d'\right> \in \intr{\syntax{R}}$.
Also, all $d'$ such that  $\left<d,d'\right> \in \intr{\syntax{R}}$ 
are in $\intr{G_1}$ ($\intr{G_2}$).
Therefore, all $d'$ such that  $\left<d,d'\right> \in \intr{\syntax{R}}$ 
are in $\intr{G_1} \cap \intr{G_2}$, which equals $\intr{(G_1 \oplus
G_2)}$ by Lemma~\ref{merge lemma}.
Thus $d \in \intr{n'}$.

Let $d \in \intr{n'}$.
Then there are between the maximum of $m_1$ and $m_2$ and 
		the minimum of $M_1$ and $M_2$ elements of the domain, $d'$,
such that $\left<d,d'\right> \in \intr{\syntax{R}}$.
Therefore there are between $m_1$ ($m_2$) and $M_1$ ($M_2$) elements of the
domain, $d'$, such that $\left<d,d'\right> \in \intr{\syntax{R}}$.
Also, all $d'$ such that  $\left<d,d'\right> \in \intr{\syntax{R}}$ 
are in $\intr{(G_1 \oplus G_2)} = \intr{G_1} \cap \intr{G_2}$.
Therefore, all $d'$ such that  $\left<d,d'\right> \in \intr{\syntax{R}}$ 
are in $\intr{G_1}$ ($\intr{G_2}$).
Therefore $d \in \intr{n}$.
\qed
\end{lemma}
Having dealt with the issue of merging, we can now return to our
desired result: showing that ``normalization'' does not affect the
meaning of description graphs.
\begin{theorem} \label{canonical theorem}
For all possible worlds \pw, the extension of the canonical form of a
description graph, $G$, resulting from a Basic \classic{} description
is the same as the extension of the description.
\proof{}
Steps 1 and 2 are justified since $\intr{G}$ is a subset of
either $\DD_H$ or $\DD_C$, which are disjoint.

Step 3 is justified by the fact that, by the definition of description
graphs, there must be an element of the domain in the extension of each
node in a description graph.

Steps 4, 5, and 6 are easily derived from
Definition~\ref{dg-extension}.

Steps 7 and 8 are dealt with in the preceding two lemmas.
\qed
\end{theorem}

\subsection{Subsumption Algorithm}

The final part of the subsumption process is checking to see if a
canonical description graph is subsumed by a description. It turns out
that it is possible to carry out the subsumption test  without the
expense of normalizing the candidate subsumer concept.

\begin{algorithm}\label{subsume}
{\bf (Subsumption Algorithm)}
Given a description \syntax{D} and description graph $G=\left<N,E,r\right>$,
{\em subsumes?}$( \syntax{D}, G )$ is defined to be true if and only if
any of the following conditions hold:
\begin{enumerate}

%1
\item The description graph $G$ is marked incoherent.

%2
\item \syntax{D} is equivalent to \name{THING}.
(This is determined by checking first if \syntax{D}=\name{THING}, or by 
recursively testing whether \syntax{D}  subsumes the
canonical description graph $G_{\name{THING}}$.)

%3
\item \syntax{D} is a concept name and is an element of the atoms of $r$.

%4
\item \syntax{D} is \syntax{\atleast{n}{R}}
 and some r-edge of $r$ has \syntax{R} as its role and min greater than or
 equal to \syntax{n}. 
%5

\item \syntax{D} is \syntax{\atmost{n}{R}}
 and some r-edge of $r$ has \syntax{R} as its role and max less than
or equal
 to \syntax{n}.

%6
\item \syntax{D} is \syntax{\all{R}{C}}
 and some r-edge of $r$ has \syntax{R} as its role and $G'$  as its
 restriction graph and $\mbox{{\em subsumes?}}( \syntax{C} , G')$.
%7
\item \syntax{D} is \syntax{\all{R}{C}}
 and $\mbox{subsumes?}(\syntax{C}, G_{\name{THING}})$
 and $r$ has \name{CLASSIC-THING} in its atoms. 
 \expl{\syntax{\all{R}{THING}} only requires the possibility that \name{R}
 be applicable to an object, which is absent for host values.}

%8
\item \syntax{D} is \syntax{\all{A}{C}}
 and some a-edge of $G$ is of the form $\left<r,r',\syntax{A}\right>$,
 and $\mbox{{\em subsumes?}}(\syntax{C},\left<N,E,r'\right>)$.

%9
\item \syntax{D} is \syntax{\all{A}{C}}
 and $\mbox{subsumes?}(\syntax{C},G_{\name{THING}})$
 and $r$ has \name{CLASSIC-THING} in its atoms.

%10a
\item \syntax{D} is \syntax{\same{A_1 \compose \ldots \compose A_n}{B_1
	\compose \ldots \compose B_m}}
	and the paths $\syntax{A_1}, \ldots, \syntax{A_n}$ and
 	$\syntax{B_1}, \ldots, \syntax{B_m}$ 
 	exist in $G$ starting from $r$ and end at the same node.

%10b
\item \syntax{D} is \syntax{\same{A_1 \compose \ldots \compose A_n}{B_1
	\compose \ldots \compose B_m}} 
	with \syntax{A_n} the same as \syntax{B_m} 
	and the paths $\syntax{A_1}, \ldots, \syntax{A_{n-1}}$ and 
	$\syntax{B_1}, \ldots, \syntax{B_{m-1}}$ 
 	exist in $G$ starting from $r$ and end at the same node, which
        has \name{CLASSIC-THING} in its atoms.
	\expl{If $\intr{\syntax{A_i}}(\ldots\intr{\syntax{A_1}}(d)) \; =\; 
         \intr{\syntax{B_j}}(\ldots \intr{\syntax{B_1}}(d))$
	then
	$$\intr{\syntax{F}}(\intr{\syntax{A_i}}(\ldots\intr{\syntax{A_1}}(d)))
	 \; = \;  
        \intr{\syntax{F}}(\intr{\syntax{B_j}}(\ldots \intr{\syntax{B_1}}(d)))$$
	for any attribute \syntax{F}, {\em as long as the attribute is 
	applicable} (i.e., the value is not in the host domain).}

%11
\item \syntax{D} is \syntax{C \And E}
      and both $\mbox{subsumes?}(\syntax{C},G)$ and
	$\mbox{subsumes?}(\syntax{E},G)$ are true.
\end{enumerate}
\end{algorithm}

\subsection{Correctness of Subsumption Algorithm}

The soundness of this algorithm is fairly obvious, so we shall not dwell on
it.
The completeness of the algorithm is, as usual, more difficult to
establish.  
First we have to show that for any canonical description graph or node that
is not marked as incoherent, a possible world having a non-empty extension
for the description graph or node can be constructed.
We will do this in a constructive, inductive manner, constructing a
collection of such possible worlds, called the {\em graphical} worlds of a
description graph. 
A graphical world has a distinguished domain element that is in the
extension of the description graph or node.

A common operation is to merge two possible worlds.
\begin{definition}
Let $\pw_1$ and $\pw_2$ be two possible worlds.
The {\em merge} of $\pw_1$ and $\pw_2$, $\pw_1 \oplus \pw_2$,
is a possible world with classic realm the disjoint union of the classic
realm of $\pw_1$ and the classic realm of $\pw_2$.
The extension of atomic names in $\pw_1 \oplus \pw_2$
is the disjoint union of their extensions in $\pw_1$ and $\pw_2$.
\end{definition}
It is easy to show that the extension of a description, a description
graph, or a node in $\pw_1 \oplus \pw_2$ is the union (disjoint union for
the classic realm, regular union for the host realm) of its extensions in
$\pw_1$ and $\pw_2$.

Another operation is to add new domain elements to a possible world.
These new domain elements must be in the classic realm.  
The extension of all atomic identifiers remain the same
except that the new domain elements belong to some arbitrary set of atomic
concept names and have some arbitrary set of
fillers (filler) for each role (attribute).
Again, it is easy to show that a domain element of the original world
is in an extension in the original world iff it is in the extension in the
augmented world.

\medskip

Given a node, $n$, that is not marked as incoherent, we construct the
graphical worlds for $n$ as follows:

\begin{enumerate}

\item
If the atoms of $n$ are precisely \name{THING}, then $n$ can have no
r-edges, because the only constructs that cause r-edges to be created also
add \name{CLASSIC-THING} to the atoms.
Any possible world, with any domain element the distinguished domain
element, is a graphical world for $n$.

\item
If the atoms of $n$ include \name{HOST-THING}, then $n$ can have no
r-edges.
Any possible world, with distinguished element any domain element in the
extension of all the atoms of $n$ and in no other host concepts, is a
graphical world for $n$. 
(Because of the requirements on the host domain, there are an infinite
number of these domain elements.)

\item
If the atoms of $n$ include \name{CLASSIC-THING}, 
then for each r-edge, $\left<\syntax{R},m,M,G\right>$, in $n$,
construct between $m$ and $M$ graphical worlds for $G$.
This can be done for any number between $m$ and $M$ because if $m > 0$ then
$G$ is not marked incoherent, and if $G$ is marked incoherent then $M = 0$.

No two of these graphical worlds should have the same host  domain
element as their
distinguished element. (Again, this is possible because the extension
of a host concept is either empty or infinite.) 
Now merge all the graphical worlds for each r-edge into one possible world.
Add some new domain elements such that one of them 
is in exactly the extensions of the atoms of $n$ and 
has as fillers for each \syntax{R} exactly the distinguished elements of
the appropriate graphical worlds.
This domain element will have the correct number of fillers for each
r-edge, because of the disjoint union of the classic realms in the merge
process and because of the different host domain elements picked
above; therefore it is in the extension of $n$.
Thus the resulting world is a graphical world for $n$.

\end{enumerate}

Given a description graph, $G = \left<N,E,r\right>$, 
that is not marked incoherent, we construct 
the graphical worlds for $G$ as follows:
For each node $n \in N$ construct a graphical world for $n$.  
This can be done because none of them are marked incoherent.
Merge these graphical worlds.
Modify the resulting world so  that for each
$\left<n_1,n_2,\syntax{A}\right> \in E$
the \syntax{A}-filler for the distinguished node 
of the graphical world from $n_1$ is the distinguished node of the
graphical world from $n_2$. 
It is easy to show that the distinguished node of the graphical world of
$r$ is in the extension of $G$, making this a graphical world for $G$.

\bigskip

Now we can show the final part of the result.
\begin{theorem} \label{subsumption theorem}
If the subsumption algorithm indicates that the canonical description of some
graph $G$ is not subsumed by the Basic \classic{} description \name{D}, 
then
for some possible world there is a domain element in the extension of the
graph but not in the extension of \name{D}.
Therefore $G$ is not subsumed by \name{D}.
\proof
The proof actually shows that if the subsumption algorithm indicates that
some canonical description graph, $G$, is not subsumed by some description,
\name{D}, then there are some graphical worlds for $G$ such that their
distinguished domain elements are not in the extension of \name{D}.
Remember that the subsumption algorithm indicates that 
$G$ is not subsumed by \name{D}, so $G$ must not be marked as
incoherent and thus there are graphical worlds for $G$.

The proof proceeds by structural induction on \name{D}.
Let $G = \left< N, E, r \right>$.

\begin{itemize}

\item %2 %3
If \name{D} is an atomic concept name or a pre-defined host concept, 
then \name{D} does not occur in the atoms of $r$.
By construction, in any graphical world for $G$ the distinguished domain
element will not be in the extension of \name{D}.
Similarly, if \name{D} is \name{CLASSIC-THING} or \name{HOST-THING},
then the distinguished domain elements will be in the wrong realm.
If \name{D} is \name{THING}, then it is not possible for the
subsumption algorithm to indicate a non-subsumption.
In each case any graphical world for $G$ has the property that its
distinguished domain element is not in the extension of \name{D}.

\item %11
If \name{D} is of the form \syntax{D_1 \And D_2}
then the subsumption algorithm must indicate that $G$ is not
subsumed by at least one of \syntax{D_1} or \syntax{D_2}.
By the inductive hypothesis, 
we get some graphical worlds of $G$
where the distinguished domain elements
are not in the extension of \syntax{D_1} 
or not in the extension of \syntax{D_2},
and thus are not in the extension of \name{D}.

\item %4
If \name{D} is the form \syntax{\atleast{n}{R}}
then either the r-edge from $r$ labelled with \name{R} has
min less than \syntax{n} or there is no such r-edge.

In the former case there are graphical worlds for $G$ in which the
distinguished node has  $\syntax{n}-1$ fillers for \name{R}, 
because $\syntax{n}$ is greater than the min on the r-edge for \name{R},
and thus the distinguished node is not in the extension of \name{D}.

In the latter case, there are graphical worlds for $G$ in which its
distinguished node has any number of fillers for \syntax{R}.
Those with $\syntax{n}-1$ fillers have the property that their
distinguished node is not in the extension of \syntax{D}.

\item %5
If \name{D} is of the form \syntax{\atmost{n}{R}}
then either the r-edge from $r$ labelled with \name{R} has
max greater than \syntax{n} (including $\infty$) or there is no such r-edge.

In the former case there are graphical worlds for $G$ in which the
distinguished node has  $\syntax{n}+1$ fillers for \name{R}, 
because $\syntax{n}$ is less than the max on the r-edge for \name{R},
and thus the distinguished node is not in the extension of \name{D}.

In the latter case, there are graphical worlds for $G$ in which its
distinguished node has any number of fillers for \syntax{R}.
Those with $\syntax{n}+1$ fillers have the property that their
distinguished node is not in the extension of \syntax{D}.

\item %6 %7
If \name{D} is of the form \syntax{\all{R}{C}},
where \name{R} is a role, then two cases arise.
\begin{enumerate}
\item %7
	If $\mbox{subsumes?}(\syntax{C},G_{\name{THING}})$ 
	then \name{CLASSIC-THING} is not in the atoms of $r$.
	Then there are some graphical worlds for $G$ whose distinguished
	element is in the host realm, and thus not in the extension of
	\name{D}. 
\item %6
	Otherwise, either there is an r-edge from $r$ with role \name{R}
	and description graph $H$ such that 
	$\mbox{subsumes?}(\syntax{C},H)$ is false
	or there is no r-edge from $r$ with role \name{R}.
	Note that the extension of \syntax{C} is not the entire domain, and
	thus must be a subset of either the host realm or the classic realm.

	In the former case $H$ is not marked incoherent (or else the
	subsumption could not be false) and the max on the r-edge cannot be
	$0$.   
	Thus there are graphical worlds for $H$ whose distinguished element
	is not in the extension of \syntax{C} and there are graphical
	worlds for $G$ that use these graphical worlds for $H$ as
	distinguished domain element \syntax{R}-fillers.
	In these graphical worlds for $G$ the distinguished element is not
	in the extension of \syntax{D}.

	In the latter case, pick graphical worlds for $G$ that have some
	distinguished node \syntax{R}-filler in the wrong realm.
	In these graphical worlds for $G$ the distinguished element is not
	in the extension of \syntax{D}.
\end{enumerate}

\item %8 %9
If \name{D} is of the form \syntax{\all{A}{C}}
where \name{A} is an attribute then two cases arise.
\begin{enumerate}
\item %9
	If $\mbox{subsumes?}(\syntax{C},G_{\name{THING}})$ 
	then \name{CLASSIC-THING} is not in the atoms of $r$.
	Then there are some graphical worlds for $G$ whose distinguished
	element is in the host realm, and thus not in the extension of
	\name{D}.
\item %8
	Otherwise, either there is an a-edge from $r$ with attribute
	\name{A} to some other node $r'$
	such that $\mbox{subsumes?}(\syntax{C},H)$ is false,
	where $H = \left<N,E,r'\right>$;
	or there is no a-edge from $r$ with attribute \name{A}.
	Note that the extension of \syntax{C} is not the entire domain, and
	thus must be a subset of either the host realm or the classic realm.

	In the former case $H$ is not marked incoherent, because $G$ is not
	marked incoherent.
	Thus there are graphical worlds for $H$ whose distinguished element
	is not in the extension of \syntax{C}.
	Given any graphical world for $H$, a graphical world for $G$ can be
	formed simply by changing the distinguished domain element.
	If the original graphical world's distinguished element is not in
	the extension of \syntax{C}, then the new graphical world's
	distinguished element will not be in the extension of \syntax{D},
	as required.

	In the latter case, pick graphical worlds for $G$ that have their
	distinguished node \syntax{A}-filler in the wrong realm.
	In these graphical worlds for $G$ the distinguished element is not
	in the extension of \syntax{D}.
\end{enumerate}

\item %10a 10b
If \name{D} is of the form \syntax{\same{A_1 \compose \ldots  \compose 
A_n}{B_1 \compose \ldots \compose B_m}} several cases again arise.
\begin{enumerate}
\item If one of the paths $\syntax{A_1}, \ldots, \syntax{A_{n-1}}$ 
	or $\syntax{B_1}, \ldots, \syntax{B_{m-1}}$ 
 	does not exist in $G$ starting from $r$,
	then find the end of the partial path and use graphical worlds in
	which the domain element for this node has an element of the host
	domain as its filler for the next attribute in the path.
	Then one of the full paths will have no filler.
\item If the paths $\syntax{A_1}, \ldots, \syntax{A_n}$ 
	and $\syntax{B_1}, \ldots, \syntax{B_m}$ 
 	exist in $G$ starting from $r$ but end at different nodes,
	then use graphical worlds in which the domain elements for these two
	nodes are different.
\item If one of the paths  $\syntax{A_1}, \ldots, \syntax{A_n}$ 
	and $\syntax{B_1}, \ldots, \syntax{B_m}$ does not exist in $G$
	starting from $r$ 
	but the paths $\syntax{A_1}, \ldots, \syntax{A_{n-1}}$ 
	and $\syntax{B_1}, \ldots, \syntax{B_{m-1}}$ 
 	both exist in $G$ starting from $r$ and end at the same node
	then either \name{CLASSIC-THING} is not in the atoms of this node
	or $\syntax{A_n} \neq \syntax{B_m}$.
	In the former case use graphical worlds in which the domain element
	for this node is in the host realm.
	In the latter case use graphical worlds that have different fillers
	for \syntax{A_n} and \syntax{B_m} for the domain element for this node.
	
\item  If one of the paths  $\syntax{A_1}, \ldots, \syntax{A_n}$ 
	and $\syntax{B_1}, \ldots, \syntax{B_m}$ does not exist in $G$
	starting from $r$
	but the paths $\syntax{A_1}, \ldots, \syntax{A_{n-1}}$ 
	and $\syntax{B_1}, \ldots, \syntax{B_{m-1}}$ 
 	both exist in $G$ starting from $r$ and end at different nodes
	then use graphical worlds that have different fillers for the
	domain elements of these nodes or that have the domain elements in
	the host realm.
\end{enumerate}
In all cases we have that
either one of 
$\intr{\syntax{A_n}}(\ldots\intr{\syntax{A_1}})(d)$ or
$\intr{\syntax{B_m}}(\ldots\intr{\syntax{B_1}})(d)$ does not exist or
$\intr{\syntax{A_n}}(\ldots\intr{\syntax{A_1}})(d) \neq
 \intr{\syntax{B_m}}(\ldots\intr{\syntax{B_1}})(d)$,
so the distinguished domain element is not in the extension of \syntax{D}.

\end{itemize}
\end{theorem}

\subsection{Implementing the subsumption algorithm}

In this section we provide some further comments about the actual
subsumption algorithm used by the \classic{} system, including a rough
analysis of its complexity.

As we have described it, deciding whether description C subsumes D is
accomplished in three phases:
\begin{enumerate}
\item Convert D into a description graph $G_D$.
\item Normalize $G_D$.
\item Verify whether C subsumes $G_D$.
\end{enumerate}

{\bf Step 1}:
Conversion is accomplished by a simple recursive descent parser, which
takes advantage of the fact that the syntax of description logics
(i.e., the leading term constructor) makes them amenable to predictive
parsing.  Clearly, constructing graphs for fixed sized terms (like
{\tt at-least}) is constant time (if we measure size so that an
integer is size 1 no matter how large), while the time for non-recursive
terms (like {\tt same-as}) is proportional to their length. Finally,
recursive terms (like {\tt all}, {\tt and}) only require a fixed
amount of additional work, on top of the recursive processing.
Therefore, the first stage can be accomplished in time proportional to
the size of the input description. In order to speed up later
processing, it will be useful to maintain various lists, such as the
lists of atomic concept identifiers, or roles/attributes, in sorted
order. This sorting needs to be done initially (later, ordering will
be maintained by performing list merges) and this incurs, in the worst
case a quadratic overhead in processing\footnote{We tend not to use
fancy sorting techniques since these lists are not likely to be very long.}.
In any case, the total size of the graph constructed (including the
sizes of the nodes, etc.) is proportional to the size of the original
concept description.

\medskip

{\bf Step 3:} Checking whether a description $C$ subsumes a
description graph $G_D$, can be seen to run in time proportional to
the size of the subsuming concept, modulo the cost of lookups in
various lists. Since these are sorted, the lookup costs are bounded by
the logarithm of the size of the candidate subsumee graph, so the
total cost is bounded by $O(\mid C \mid \ *\ log \mid G_D \mid)$.
\medskip

{\bf Step 2}:
Normalization is accomplished by a post-order traversal of the
description graph: in processing a description {\em graph} 
$\left< N,E,r \right>$, each node in $N$ is normalized first independently
(see details below), and afterwards the attribute edges $E$ are normalized.
This later task involves identifying multiple identically-labelled
attribute edges leaving a node (this is done in one pass since the
attribute edges are grouped by source node, and sorted by attribute
name), and ``merging'' them.  Merging two edges is quite
easy in and of itself, but when merging the nodes at their tips,
 we
must be careful because node mergers may cascade; for example, if
a concept has the form
\syntax{\same{a_1}{b_1} \And \same{a_2}{b_2} \And \ldots \And
\same{a_n}{b_n} \And \same{a_1}{a_2} \And \same{a_2}{a_3} \And \ldots
\And \same{a_{n-1}}{a_n}}
then the original graph will have $2n+1$ nodes, but $2n$ of these are
collapsed by normalization step 8. To discover this
efficiently, we use a version of A\"\it-Kaci's algorithm for unifying
$\Psi$-terms
\shortcite{ait-kaci:thesis,ait-kaci-nasr:logic}; the algorithm relies on the
UNION-FIND technique to identify nodes to be merged, and runs in time
just slightly more than linear
%\footnote{Grows with the inverse of Ackerman's function.} 
in the number of nodes in $N$.
Therefore the  cost of the non-recursive portion of graph
normalization is roughly linear in the number of nodes in it.

The merging of two description graph {\em nodes} is quite similar to
the normalization of a single node: the atomic concept identifier
lists need to sorted/merged, with duplicates eliminated on the fly.
 This can be
done in time proportional to the {\em size of the nodes} themselves,
if we make the size of the node include the size of the various lists in
it, such as atoms. The processing of role edges leaving a
node is, again, one of identifying and merging identically-labelled
edges. (But in this case the mergers of labelled edges do not
interact, so a single pass over the role-edge list is sufficient.) The
cost of non-recursive aspects of any such merger is once again
proportional to the size of the local information.

We are therefore left with the problem of bounding the {\em total
number} of procedure calls to NormalizeGraph, NormalizeNode,
MergeEdge, and MergeNode, and then bounding the sizes of the nodes
being merged.

NormalizeGraph and NormalizeNode are called exactly once on
every (sub)graph and node in the original graph, as part of the
depth-first traversal, and as argued above, on their own they
contribute at most time proportional to the total size of the original
graph, which was proportional to the size of the original description.

The number of calls to MergeEdge and MergeNode is not so simply
bounded however -- the same node may be merged several times with
others. However, these calls are paired, and each invocation of
MergeNode reduces the number of nodes in the graph by one. Therefore,
since the number of nodes is not incremented elsewhere, the total
number of calls to MergeEdge and MergeNode is bounded by the number of
nodes in the original graph. The only problem is that the
non-recursive cost of a call to MergeNode depends on the size of the
argument nodes, and each call may increase the size of the remaining
node to be the sum of the sizes of the two original nodes.

Therefore, if the original concept had size S, with the graph having $n$
nodes, each of size $v_i$, then the worst case cost would result from
the iterative summation of sizes:
\[
\begin{array}{l}
(v_{i_1}+v_{i_2}) + (v_{i_1}+v_{i_2}+v_{i_3}) + 
(v_{i_1}+v_{i_2}+v_{i_3}+v_{i_4}) + \ldots\\
= 
n*v_{i_1} + (n-1)*v_{i_2} + \ldots + 1*v_{i_n}
\end{array}
\]

Given that $n$ and all $v_j$ are  bounded by $S$, clearly the
above is in the worst case $O(S^3)$. In fact, given the constraint
that $\sum_{j=1}{n}v_j\ =\ S$, it is possible to argue that the worst
case cost will occur when $v_j = 1$ for every j, (i.e., when $n=S$),
in which case the cost is really just $O(S^2)$.

There are other theoretical improvements that could be attempted for
the algorithm (e.g., merging nodes in the correct order of increasing
size) as well as its analysis (e.g., only nodes in graphs at the same
depth in the tree can be merged).


\medskip
We remark that like all other description logics, \classic{} permits
identifiers to be associated with complex descriptions and then these
identifiers can be used in other descriptions (though no recursion is
allowed).  The expansion of identifiers is a standard operation which
can lead to exponential growth in size in certain pathological cases
\shortcite{nebel:intractable}, making the subsumption problem inherently
intractable. As with the type system of the programming language Standard ML, such
pathological cases are not encountered in practice, and the correct
algorithm is simple, straightforward and efficient in normal cases
(unlike the correct algorithm for reasoning with the set constructor,
say).

\medskip

Because users rarely
ask only whether some concept subsumes another, but rather are
interested in the relationship between pairs of concepts, \classic{}
in fact constructs the normalized description graph of any description
given to it. This suggests that it might be better to check whether
one description graph subsumes another one, rather than checking
whether a description subsumes a graph. In general, this works quite
well, except that we would have to verify that the attribute edges in
the subsumer graph form a {\em subgraph} of the subsumee's attribute
edges. Since edges are uniquely labelled after normalization, this is
not inherently hard, but it still requires a complete traversal (and
hence marking/unmarking) of the upper graph. We have therefore found
it useful to encode as part of the description graph's root the {\tt
same-as} restrictions that lead to the construction of the
corresponding a-edges; then, during subsumption testing, the only
aspect of the subsumer related to {\tt same-as} which is checked is
this list of {\tt same-as} pairs.

Also, the above description of the algorithm has tried to optimize the
cost of normalization, which dominates when checking a single
subsumption. If in the overall use of a system (e.g., processing
individuals), inquiries about the restrictions on roles/attributes are
frequent, and space usage is not a problem, then it may be practically
advantageous to maintain the r-edges and a-edges of a node in a hash
table, rather than a sorted list, in order to speed up access. (Note
that for merging r-edges, one must however still have some way of
iterating through all the values stored in the hash table.)

\section{Individuals in Descriptions}

In practical applications where DLs have been used, 
such as integrity constraint checking, 
it is often very useful to be able to specify ranges of atomic values for
roles. 
The most common examples of this involve integers, 
e.g., {\it ``the year of a student can be 1,2,3 or 4''},
or what are called enumerated types in Pascal, 
e.g., {\it ``the gender of a person is either M or F''}.  
One way to allow such constraints is to introduce a new description
constructor, a set description, which creates a description from a list of
individual names, 
and whose obvious extension is the set consisting of the extensions of
the individuals that appear in the list.
This construct could be used in terms like
\begin{notation}
\all{year}{\set{ 1\,  2\, 3\, 4}}
\end{notation}.
Another useful constructor involving individuals is 
a fills restriction,
\begin{notation} \fills{p}{I} \end{notation}, 
which denotes objects that have the extension
of the individual \begin{notation} I \end{notation} 
 as one of the fillers for the relationship denoted by
role or attribute \syntax{p}. 
(Note that for an attribute, \syntax{q},
\begin{notation} \all{q}{\set{I}} \end{notation} is the same as
\begin{notation} \fills{q}{I} \end{notation}.)

Within the paradigm of DLs, these constructors are quite useful and can in
fact be used to express new forms of incomplete information.
For example, if we only know that Ringo is in his early fifties, we can
simply assert that \name{Ringo} is described by
\begin{notation} \all{ age}{ \set{50\, 51\, 52\, 53\, 54}} \end{notation}.
The constructors can also be used to ask very useful queries.
For example, to find all the male persons it suffices to determine the
instances of \begin{notation}\fills{ gender}{M}\end{notation}.

The new constructors do interact with previous ones, such as cardinality
constraints:
clearly the size of a set is an upper cardinality bound for any role it
restricts.  
This interaction is not problematic as long as the individuals in the set
are {\em host values}, since such individuals have properties that are
fixed and known ahead of time.
However, once we allow classic individuals as members of sets, then
the properties of these individuals might themselves affect subsumption.
As a simple example, if we know that \name{Ringo} is an instance of the
concept \name{ROCK-SINGER} 
(which we shall write as 
\begin{notation}\instance{Ringo}{\name{ROCK-SINGER}}\end{notation})
then the extension of 
\begin{notation} \all{ friends}{\name{ROCK-SINGER}} \end{notation}
is always a superset of the extension of 
\begin{notation} \all{ friends}{ \set{ Ringo}}\end{notation}.

This is disturbing because then the classification hierarchy
of  definitions would change as new facts about individuals are added to
the knowledge base.
Definitions are not meant to be contingent of facts about the current
world.
Therefore, subsumption is usually defined to be independent of these
``contingent'' assertions.
As we shall see below, the use of individual properties in
description subsumption also leads to intractability.

\subsection{Complex Subsumption Reasoning: An Example}\label{eg-poles}

Traditional proofs of intractability (e.g.
\shortcite{levesque-brachman:tractability}) have occasionally left users of DLs
puzzled over the intuitive aspects of a language which make reasoning
difficult.
For this reason we present  an example that illustrates the complexity
of reasoning with the set description.

Suppose that we have the concept of \name{JADED-PERSON} as being one who
wants only to visit the Arctic and/or the  Antarctic,
wherever there are penguins:
\begin{displaynotation} 
\Define{\name{JADED-PERSON}}{\all{wantsToVisit}{(\set{ Arctic \,
Antarctic} \And \all{hasPenguins!}{\set{Yes}})}}
\end{displaynotation}
Suppose we do not remember which is the Arctic and which the
Antarctic; but we do know that the South Pole is located in one of
these two places, and that there are penguins there, while the North
Pole is located in one of these two places, and there are no penguins
there.  
Assuming that \name{isLocatedIn!} and \name{hasPenguins!} are
attributes---roles with exactly one filler, we can record
\begin{displaynotation}
\instance{Southpole}{\all{ isLocatedIn!}{(
 \set{ Arctic\, Antarctic} \And \all{hasPenguins!}{\set{Yes}})}}
 \\
\instance{Northpole}{\all{ isLocatedIn!}{(
 \set{ Arctic\, Antarctic} \And \all{hasPenguins!}{\set{No}})}}
\end{displaynotation}
We are thus unable to distinguish the exact location of the
\name{Southpole} and \name{Northpole}; however, since \name{hasPenguins!}
has a single filler, exactly one of \name{Arctic} and \name{Antarctic}
can (and in fact must) have \name{Yes} as filler for
\name{hasPenguins!}, and therefore exactly one of them is the location
of \name{Southpole}.

As a result of these facts, we know that the extension of \name{JADED-PERSON}
must be a subset of the extension of
\begin{notation} \atmost{1}{wantsToVisit} \end{notation}
in any database containing the above facts about \name{Southpole} and
\name{Northpole}.

Observe that we have here not just an occasional worse-case behavior,
but a generalized difficulty in reasoning with set descriptions.
Because subsumption ignores assertions about individuals, this does
not (yet) show that subsumption per se must perform these inferences.
A simple transformation, given in the appendix, establishes this fact,
by converting the recognition of individuals into a question about the
subsumption of two descriptions by making all the individuals involved
attribute-fillers for new dummy attributes, and their descriptions as
restrictions on these attributes. As a result, if the description is
non-empty then these attribute values must satisfy the corresponding
restrictions.


\subsection{A Modified Semantics for Individuals}\label{modif-semantics}

We have seen two problems with individuals appearing in descriptions:
(1) the effect of  ``mutable facts'' on  extensional relationships between
``immutable'' descriptions, and
(2) the computational intractability of subsumption caused by the
appearance of individuals in descriptions.

To deal with the first problem, it is reasonable to restrict the
computation of subsumption so that it cannot access ``database facts'' about
individuals, such as their role fillers, so that all individuals are treated
like host identifiers. 
This is a procedural description of some aspect of
reasoning, in the same sense as negation-by-failure is in Prolog. 
As with Prolog, it would be desirable to find a semantic account of this
phenomenon. 

A semantics that ignores mutable facts when determining subsumption is not
hard to devise---all that is required is to have two different sets of
possible worlds corresponding to a KB containing both concepts and
individuals. 
One set consists of all possible worlds that model all the information in
the KB; the second consists of all possible worlds that model only the
information about concepts (and roles and attributes).
When asking questions about individuals, the first set of possible
worlds must be considered; when asking subsumption questions, the
second, larger, set must be considered, thus ignoring any effects of the
mutable facts.

However, this semantics does not solve the computational problem with
individuals in descriptions. To deal with this problem, the semantics
of individuals are modified as follows: instead of mapping individuals
into separate elements of the domain, as is done in a standard
semantics, individuals are mapped into {\em disjoint subsets of the
domain}, intuitively representing different possible realizations of
that (Platonic) individual.

Therefore, the semantics of the set constructor is now stated as follows:
Domain value $d$ belongs to the extension of 
\begin{notation} \set{B_1\, \ldots\, B_n} \end{notation} 
iff $d$ belongs to the extension of one of the  \syntax{B_i}.
An associated change in the notion of cardinality is required---two
elements of the domain are considered {\em congruent} if they belong to the
extension of the same individual or if they are identical.  
The cardinality of a set of elements of the domain is then the size of the
set modulo this congruence relationship.
This means that occurrences of different identifiers in description(s) are
guaranteed to be unequal, but distinct occurrences of the same individual
identifier are not guaranteed to denote the same individual. 

Here are two consequences of this stance: 
\begin{enumerate}
\item
Looking at the descriptions of \name{Southpole} and \name{Northpole} in
Section~\ref{eg-poles}, the distinct occurrences of \name{Arctic} might be
satisfied by distinct domain elements, with different role fillers. 
(In greater detail: the extension of \name{Arctic} might include domain
elements $d_1$ and $d_2$, with $d_1$ satisfying condition 
\begin{notation} \fills{hasPenguins!}{Yes} \end{notation}, 
while $d_2$ satisfies
\begin{notation} \fills{hasPenguins!}{No} \end{notation}. 
If \name{Southpole} is then located in $d_1$, while \name{Northpole} is
located in $d_2$, then we still have both satisfying 
\begin{notation} \fills{isLocatedIn!}{Arctic} \end{notation}. 
Similarly for domain elements $d_3$ and $d_4$ in the extension of
\name{Antarctic}.  
Therefore one could have two places to visit where there are penguins,
$d_1$ and $d_3$.)
\item
Even though an individual may have a description that includes
\begin{displaynotation} 
\fills{isLocatedIn!}{Arctic} \AND 
	\fills{originatesIn!}{Arctic},
\end{displaynotation}
it need not satisfy the condition
\begin{notation} \same{isLocatedIn!}{originatesIn!} \end{notation}, 
since the equality restriction requires identity of domain values.
\end{enumerate}


\section{Adding Individuals to {\sc CLASSIC}}\label{add-inds}

Individuals can occur in both classic and host descriptions.
The following constructs create classic descriptions:
\begin{quote}
\begin{notation}
\fills{R}{I}\\
\fills{A}{I}\\
\set{I_1\, \ldots\, I_n}
\end{notation}
\end{quote}
where \name{A} is an attribute,
\name{R} is a role,
\name{I} is the name of a classic individual or a host value, 
collectively called individuals,
and
$\syntax{I_j}$ are names of classic individuals.
New host descriptions can be constructed using
\syntax{\set{I_1\, \ldots\, I_n}}, 
where the \syntax{I_j} are host values.

The interpretation function \intr{.} is extended to individual
identifiers, by requiring that \intr{\name{I}} be a non-empty subset
of $\DD_C$, if \name{I} is syntactically not recognized to be a host
individual, and making  \intr{\name{I}}= $\{\name{I}\}$ for host values
\name{I}. As stated earlier, the interpretations of distinct identifiers must
be non-overlapping.

The interpretation 
\intr{\syntax{C}} of non-atomic descriptions
is modified as follows:
\begin{itemize}
\item $\intr{\syntax{\fills{p}{I}}} = 
	\{ d \in \DD_C \mid \exists x \ (d,x) \in \intr{\name{p}}\
		\land \ x \in \intr{\name{I}}\}$

\item $\intr{\syntax{\set{I_1\, \ldots\, I_n}}} = \bigcup_{k}
\intr{\name{I}_k}$ if the $\name{I}_k$ are all classic individuals;
$\intr{\syntax{\set{I_1\, \ldots\, I_n}}} = \{\name{I}_1\, \ldots\,
\name{I}_n\}$ if  $\name{I}_k$ are all host individuals; empty otherwise.

\item $\intr{\syntax{(\atleast{n}{p})}}$ 
	(resp. $\intr{\syntax{(\atmost{n}{p})}}$)
	is those objects in $\DD_C$ with at least (resp. at most) \name{n}
{\em non-congruent}	fillers for role \name{p}
\end{itemize}


\medskip

The development of the subsumption algorithm in Section~\ref{basic} is
then modified to take into account the added constructs with the
modified semantics introduced earlier.

First description graphs are extended.
A node of a description graph is given a third field, 
which is either a finite set of individuals or 
a special marker denoting the ``universal'' set.
This field is often called the {\em dom} of the node.
Both a-edges and r-edges are given an extra field, called the {\em
fillers} of the edge.
This field is a finite set of individuals.
Where unspecified, as in constructions in previous sections,
the {\em dom} of a node is the universal set and the {\em fillers} of an
a-edge or an r-edge is the empty set.

The semantics of description graphs in Definition~\ref{dg-extension} are
extended to the following:
\begin{definition}\label{individual-dg-extension}
Let $G = \left<N,E,r\right>$ be a description graph
and let $\pw$ be a possible world.

An element, $d$, of $\DD$ is in $\intr{G}$,
iff
there is some function, $\inj$, from $N$ into $\DD$
such that 
\begin{enumerate}
\item $d = \inj(r)$;
\item for all $n \in N \; \inj (n) \in \intr{n}$;
\item for all $ \left<n_1,n_2,\syntax{A},F  \right> \in E$ we have $
	\left<\inj(n_1),\inj(n_2)\right> \in \intr{\syntax{A}}$, and
	 for all $\syntax{f} \in F$, $ \inj(n_2) \in \intr{\syntax{f}}$.
\end{enumerate}

An element, $d$, of $\DD$ is in $\intr{n}$, 
where $n=\left< C, H, S\right>$,
iff
\begin{enumerate}
\item for all $\syntax{C} \in C$, we have $d \in \intr{\syntax{C}}$; 
\item for all $\left<\syntax{R},m,M,G,F\right> \in H$,
	\begin{enumerate}
	\item there are between $m$ and $M$ elements, $d'$, of the domain 
		such that $\left<d,d'\right> \in \intr{\syntax{R}}$;
	\item $d' \in \intr{G}$ for all $d'$ such that
		$\left<d,d'\right> \in \intr{\syntax{R}}$;
	and
	\item for all $\syntax{f} \in F$  there is a domain element, $d'$,
		such that $\left<d,d'\right> \in \intr{\syntax{R}}$ and
			$d' \in \intr{\syntax{f}}$
	\end{enumerate}
\item If the $S$ is not the universal set then
	$\exists \syntax{f} \in S$ such that $ d \in \intr{\syntax{f}}$.
\end{enumerate}
\end{definition}

When merging nodes, the {\em dom} sets are intersected.
Merging description graphs is unchanged.
When merging a-edges and r-edges, the sets of fillers are unioned.

The translation of descriptions into description graphs is extended by
the following rules:
\begin{enumerate}
\setcounter{enumi}{7}
\item 
A description of the form 
\syntax{\fills{R}{I}}
is turned into a description graph with one node and no a-edges.
The node has as its atoms \name{CLASSIC-THING} and a
single r-edge with role \name{R}, min $0$, max $\infty$, 
and fillers $\{ \syntax{I} \}$.
The description graph restricting this r-edge is
$G_{\name{CLASSIC-THING}}$ if \syntax{I} is a classic individual, and
$G_{\name{HOST-THING}}$ otherwise.

\item 
A description of the form 
\syntax{\fills{A}{I}}
is turned into a description graph with two nodes with a single a-edge
between them. 
The distinguished node of the graph is the source of the a-edge.
It has no r-edges and has as atoms \name{CLASSIC-THING}.
The other node also has no r-edges.
It has as atoms \name{CLASSIC-THING} if \syntax{I} is a classic individual,
and \name{HOST-THING} otherwise.
The a-edge has as its single filler \syntax{I}.

\item
A description of the form
\syntax{\set{I_1\, \ldots\, I_n}}
is turned into a description graph with one node.
The node has as {\em dom} the set containing $\syntax{I_1}$ through
$\syntax{I_n}$, and no r-edges.
The atoms of the node is \name{HOST-THING} if all of the individuals
are host values, and \name{CLASSIC-THING} if all of the 
individuals are classic individual names.
(Note that the parser ensures that  individuals either must all be host values or must all be
classic individual names.)
\end{enumerate}

\smallskip

A short examination shows that
Theorem~\ref{translation lemma} is true for these graphs, i.e.,
the extension of description graphs formed using these rules is the same as
the extension of the description from which they were formed.

\smallskip

The following transformations are added to the canonicalization
algorithm:
\begin{enumerate}
\setcounter{enumi}{8}
\item If the {\em dom} of a node is empty, mark the node incoherent.
\item If a host value in the {\em dom} of a node is not in all the atoms of the
	node, remove it from the {\em dom}.
\item If an a-edge has more than one filler, then mark the description
	graph as incoherent.
\item If an a-edge has a filler and the node at its end has the universal
	{\em dom}, make the {\em dom} be the filler.
\item If the filler of an a-edge is not included in the {\em dom} of the node at
	its end, mark the description graph as incoherent.
\item If a node has only one element in its {\em dom}, make this element be the
	filler for all the a-edges pointing to it.
\item If the fillers of some r-edge are not a subset of the {\em dom}
	of the distinguished node of the restriction graph of the edge,
	mark the node of the r-edge incoherent. 
\item If the min on an r-edge is less than the cardinality of fillers on it,
	let the min be this cardinality.
\item If the max on an r-edge is greater than the cardinality of the {\em
	dom} on the distinguished node of the description graph of the r-edge, 
	make the max of this edge be the cardinality of the {\em dom}.
\item If the min on an r-edge is greater than or equal to the cardinality
	of the {\em dom} on the distinguished node of the restriction graph of
	the r-edge,  
	let the fillers of the edge be the union of its fillers and the
	{\em dom} above. (If min is greater than the cardinality, then
	steps 4 and 17 detect the inconsistency.)
\item If the max on an edge is equal to the cardinality of
	fillers on the edge, 
	let the {\em dom} on the distinguished node of the description graph of
	the r-edge be the intersection of the {\em dom} and the
	fillers. (If max is less than the cardinality, steps 18 and 4 detect
	the inconsistency.)
\end{enumerate}
Note that in the new canonical form all a-edges pointing to a single node
have the same value for their fillers, and that if this is not the empty
set, then the node has this set as the value for its {\em dom}.

The proofs of Lemmas 
\ref{role merging extension lemma}~and~\ref{attribute merging extension lemma}
also work for this extension of description graphs.  The proof of
Theorem~\ref{canonical theorem} can then be extended for these graphs.

\smallskip

The subsumption algorithm from page~\pageref{subsume} is extended as follows:
\begin{enumerate}
\setcounter{enumi}{12}
\item \syntax{D} is \syntax{\fills{R}{I}}
	 and some r-edge of $r$ has role \syntax{R} and fillers including
	\syntax{I}. 
	
\item \syntax{D} is \syntax{\fills{A}{I}}
	 and some a-edge from $r$ has attribute \syntax{A} and fillers
	including \syntax{I}. 

\item \syntax{D} is \syntax{\set{I_1\,\ldots\,I_n}}
	 and the {\em dom} of $r$ is a subset of
	\syntax{\set{I_1\,\ldots\,I_n}}. 
\end{enumerate}

Again, the soundness of the extended algorithm is fairly obvious.
The completeness proof has the following additions to the construction of
graphical worlds:
\begin{itemize}
\item The extension of classic individual names starts out empty.
\item When constructing graphical worlds for a node that includes
	\name{HOST-THING} in its atoms and has a non-universal {\em dom},
	pick only those domain elements corresponding to the elements of
	its {\em dom}.
\item When constructing graphical worlds for a node that includes
	\name{CLASSIC-THING} in its atoms and has a non-universal {\em dom},
	add the distinguished domain element to the extension of one of
	its {\em dom} elements.
\item When constructing graphical worlds for the r-edges of a node,
	ensure that each element of the fillers of the r-edge has the
	distinguished element of at least one of the graphical worlds in
	its extension by either adding them to the extension or using
	appropriate host domain elements.  
	(This can be done because the fillers must be a subset of the {\em dom}
	of the distinguished node of the graphical world and any host
	values must belong to its atoms.)
\end{itemize}
The fillers for a-edges need not be considered here because they are
``pushed'' onto the nodes in the canonicalization process.

The proof of Theorem~\ref{subsumption theorem} is then extended with the
following cases:
\begin{itemize}

\item If \name{D} is of the form \syntax{\set{I_1\,\ldots\,I_n}}
	then the {\em dom} of $r$ is not a subset of 
	$\{\syntax{I_1},\ldots,\syntax{I_n}\}$.
	Thus there are graphical worlds for $G$ in which the distinguished
	domain element is not in the extension of any of the \syntax{I_j}.

\item If \name{D} if of the form \syntax{\fills{A}{I}}
	then either the a-edge from $r$ labelled with \name{A} does not have
	filler \syntax{I} or there is no such a-edge.

	In the former case the node pointed to by the a-edge cannot have as its
	domain the singleton consisting of \syntax{I}.
	Therefore there are graphical worlds for $G$ that have their
	distinguished node \syntax{A}-filler not in the extension of
	\syntax{I}, as required.

	In the latter case, pick graphical worlds for $G$ that have their
	distinguished node \syntax{A}-filler in the wrong realm.
	In these graphical worlds for $G$ the distinguished element is not
	in the extension of \syntax{D}.

\item If \name{D} is of the form \syntax{\fills{R}{I}}
	then either the r-edge from $r$ labelled with \name{R} does not have
	filler \syntax{I} or there is no such r-edge.

	In the former case either the cardinality of the {\em dom} of the
	distinguished node of the description graph of this r-edge is
	greater than the min, \syntax{m}, of the r-edge, or the {\em dom} does
	not include \syntax{I}.  
	If the {\em dom} does not include \syntax{I}, then all graphical worlds
	for the node have their distinguished element not in the extension
	of \syntax{I}, as required.  
	If the {\em dom} does include \syntax{I}, then there are at least
	\syntax{m} elements of the {\em dom} besides \syntax{I}, and the
	fillers of the r-edge are a subset of the set of these elements.
	There are thus graphical worlds for $G$ that use only these
	elements, as required. 

	In the latter case, pick graphical worlds for $G$ that have some
	distinguished node \syntax{R}-filler in the wrong realm.
	In these graphical worlds for $G$ the distinguished element is not
	in the extension of \syntax{D}.

\end{itemize}

This shows that the subsumption algorithm given here is
sound and complete for the modified semantics presented here.


\section{Complete {\sc CLASSIC}}

We now make a final pass to deal with some less problematic aspects
of \classic{} descriptions that have not been appropriately covered so far.

\smallskip

\classic{} allows primitive descriptions of the form
\syntax{(\name{\small\bf PRIMITIVE}\ D\ T)}, where \syntax{D} is a description,
and \syntax{T} is a symbol.
The extension of this is some arbitrary subset of the extension of
\syntax{D}, but is the same as the extension of 
\syntax{(\name{\small\bf PRIMITIVE}\ E\ T)}, provided that \syntax{D} and
\syntax{E} subsume each other.
In this way one can express \syntax{EMPLOYEE},
a kind of a person who must have an employee number, as
\begin{displaynotation}
(\name{\small\bf PRIMITIVE} \; (PERSON \And \atleast{1}{employeeNr}) \; 
employee)
\end{displaynotation}
This construct can be removed by creating for
every such primitive an atomic concept (e.g., \name{EMPLOYEEHOOD}) and then
replacing the definition of the concept by the conjunction of the necessary
conditions and this atom, in this case
\begin{notation} EMPLOYEEHOOD \And (PERSON \And \atleast{1}{employeeNr})
\end{notation}.  Care has to be taken to use the same atomic concept for
equivalent primitives.

\smallskip

\classic{} permits the declaration of disjoint primitives, essentially
allowing one to state that the extensions of various atomic concepts must be
disjoint in all possible worlds. To deal with such declarations, we need
only modify the algorithm for creating canonical graphs by adding a step
that marks a node as incoherent whenever its atoms contains two
identifiers that have been declared to be disjoint.

\smallskip

To allow an approximate representation for ideas that cannot be
encoded using the constructors expressly provided, \classic{} allows the
use of {\em test-defined concepts}, using the following syntax:
\begin{displaynotation}
(\name{\small\bf TEST} \; \mbox{\it [host-language\ Boolean\ function]})
\end{displaynotation}
e.g., \name{({\small\bf TEST} Prime-Number-Testing-Function)}.\footnote{In
order to deal with the two realms, \classic{} in fact provides two
constructors: {\small\bf H-TEST} and {\small\bf C-TEST}, for host and
classic descriptions, but this does not cause any added complications
besides keeping track of the correct realm.}
For the purposes of subsumption, these are treated as ``black-boxes'', 
with semantics assigned as for atomic concepts.
(Test concepts have a real effect on reasoning at the level of individuals,
where they can perform constraint checking.)

With these simple additions, the above algorithm is a sound and complete
subsumption algorithm for descriptions in \classic{} 1, under the modified
semantics introduced in this paper.

\section{Summary, Related Work,  and Conclusions}
  We believe this paper makes two kinds of contributions:
First, the paper presents an abstracted form of the subsumption
algorithm for the \classic{} description logic, and shows that it is
efficient and correct under the modified semantics. 
This is significant because previous claims of correct and efficient
subsumption algorithms in implemented DLs such as \system{kandor}
\shortcite{patel-schneider:small} and \system{candide} \shortcite{beck-et-al:candide}
have turned out to be unfounded \shortcite{nebel:back-complexity}.

A tractability proof  for a language like Basic \classic\ 
is claimed to exist (but is not proven) in
\shortcite{donini-et-al:tractable}, and an alternate proof technique may be found
by considering a restriction of the (corrected) subsumption algorithm in
\shortcite{hollunder-nutt:subsumption-algorithms}. 

Description graphs have also turned out to be of interest because they
support further theoretical results about DLs, concerning their
learnability
\shortcite{cohen-hirsh:learning-description-logics,pitt-frazier:learning}---results
which would seem harder to obtain using the standard notation for DLs.

\smallskip

Second, this paper investigates the effect of allowing individuals
to appear in descriptions of DLs. As independently demonstrated in
\shortcite{lenzerini-schaerf:concept-query-languages}, adding a set
description introduces yet another source of intractability, and we
have provided an intuitive example illustrating the source of
difficulties.
The implementers of the \classic{} system, like others who do not use
refutation/tableaux theorem-proving techniques, chose not to perform
all inferences validated by a standard semantics, not just because of
the formal intractability result but because no obvious algorithm was
apparent, short of enumerating all possible ways of filling roles. The
subset of inferences actually performed was initially described
procedurally: ``facts'' about individuals were not taken into account
in the subsumption algorithm.  This paper provides a 
denotational semantic account for this incomplete set of
inferences. The formal proof of this being a correct account is a
corollary of the completeness proof for the subsumption algorithm in
Section~\ref{add-inds}, and the observation that the graph
construction and subsumption algorithms in that section do indeed
ignore the properties of the individuals involved. The one difference
between the original implementation of
\classic{} and the current semantics is that attribute paths ending
with the same filler were used to imply an equality condition. As noted in
Section~\ref{modif-semantics}, the modified semantics does not support
this inference, and it was taken out of the implementation of
\classic{}.  It is significant that the change to the standard
semantics is small, easy to explain to users (either procedurally or
semantically), and only affects the desired aspects of the language
(i.e., all reasoning with Basic \classic{} remains exactly as before).       
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection*{Acknowledgments} We wish to thank Ronald Brachman and
our other colleagues in the \classic{} project for their
collaboration, and the JAIR referees for their excellent suggestions
for improving the paper. In particular, one of the referees deserves a
medal for the thoroughness and care taken in locating weaknesses in
our arguments, and we are most thankful. Any remaining
errors are of course our own responsibility.



\vskip 0.2in
%%\bibliography{publications}
%%Bibliography file from BibTeX
%% Warning:  This file was manually modified to get around bugs in
%% theapa.bst!  Not all modifications are mentioned!!
\begin{thebibliography}{}

\bibitem[\protect\BCAY{A{\"\i}t-Kaci}{A{\"\i}t-Kaci}{1984}]{ait-kaci:thesis}
A{\"\i}t-Kaci, H. \BBOP 1984\BBCP.
\newblock {\Bem A Lattice Theoretic Approach to Computation Based on a Calculus
  of Partially-Ordered Type Structures}.
\newblock Ph.D.\ thesis, University of Pennsylvania.

\bibitem[\protect\BCAY{A{\"\i}t-Kaci \BBA\ Nasr}{A{\"\i}t-Kaci \BBA\
  Nasr}{1986}]{ait-kaci-nasr:logic}
A{\"\i}t-Kaci, H.\BBACOMMA\  \BBA\ Nasr, R. \BBOP 1986\BBCP.
\newblock \BBOQ {LOGIN}: A logic programming language with built-in
  inheritance\BBCQ\
\newblock {\Bem Journal of Logic Programming}, {\Bem 3}, 187--215.

\bibitem[\protect\BCAY{AAAI}{AAAI}{1992}]{fss-92-dl}
%% Manually modified to get around bug in theapa.bst
American Association for Artificial Intelligence \BBOP 1992\BBCP.
%% Manually modified to get around bug in theapa.bst
\newblock {\Bem Issues in Description Logics: Users Meet Developers}.
\newblock Working Notes of the AAAI 1992 Fall Symposium.

\bibitem[\protect\BCAY{Baader, B{\"u}rckert, Heinsohn, Hollunder, M{\"u}ller,
  Nebel, Nutt, \BBA\ Profitlich}{Baader et al.}{1991}]{baader-et-al:notation}
%% Manually modified to get around bug in theapa.bst
Baader, F., B{\"u}rckert, H.-J., Heinsohn, J., Hollunder, B., M{\"u}ller, J.,
  Nebel, B., Nutt, W., \BBA\ Profitlich, H.-J. \BBOP 1991\BBCP.
\newblock \BBOQ Terminological knowledge representation: {A} proposal for a
  terminological logic\BBCQ\
\newblock German Research Center for Artificial Intelligence (DFKI).

\bibitem[\protect\BCAY{Baader \BBA\ Hanschke}{Baader \BBA\
  Hanschke}{1991}]{baader-hanschke:concrete-domains}
Baader, F.\BBACOMMA\  \BBA\ Hanschke, P. \BBOP 1991\BBCP.
\newblock \BBOQ A scheme for integrating concrete domains into concept
  languages\BBCQ\
\newblock In {\Bem Proceedings of the Twelfth International Joint Conference on
  Artificial Intelligence}, \BPGS\ 452--457. International Joint Committee on
  Artificial Intelligence.
\newblock A long version appears as Research Report RR-91-10 from the German
  Research Center for Artificial Intelligence (DFKI), April 1991.

\bibitem[\protect\BCAY{Baader \BBA\ Hollunder}{Baader \BBA\
  Hollunder}{1991}]{baader-hollunder:kris}
Baader, F.\BBACOMMA\  \BBA\ Hollunder, B. \BBOP 1991\BBCP.
\newblock \BBOQ {KRIS}: {K}nowledge {R}epresentation and {I}nference
  {S}ystem\BBCQ\
\newblock {\Bem {SIGART} Bulletin}, {\Bem 2\/}(2), 8--15.

\bibitem[\protect\BCAY{Beck, Gala, \BBA\ Navathe}{Beck
  et~al.}{1989}]{beck-et-al:candide}
Beck, H.~W., Gala, S.~K., \BBA\ Navathe, S.~B. \BBOP 1989\BBCP.
\newblock \BBOQ Classification as a query processing technique in the {CANDIDE}
  semantic data model\BBCQ\
\newblock In {\Bem Proceedings of the Fifth International Data Engineering
  Conference}, \BPGS\ 572--581. Institute of Electric and Electronic Engineers.

\bibitem[\protect\BCAY{Borgida, Brachman, McGuinness, \BBA\ Resnick}{Borgida
  et~al.}{1989}]{borgida-et-al:classic-sigmod}
Borgida, A., Brachman, R.~J., McGuinness, D.~L., \BBA\ Resnick, L.~A. \BBOP
  1989\BBCP.
\newblock \BBOQ {CLASSIC:} {A} structural data model for objects\BBCQ\
\newblock In {\Bem Proceedings of the 1989 ACM SIGMOD International Conference
  on Mangement of Data}, \BPGS\ 59--67. Association for Computing Machinery.

\bibitem[\protect\BCAY{Borgida}{Borgida}{1992}]{borgida:natural-semantics}
Borgida, A. \BBOP 1992\BBCP.
\newblock \BBOQ From type systems to knowledge representation: {N}atural
  semantics specifications for description logics\BBCQ\
\newblock {\Bem International Journal of Intelligent and Cooperative
  Information Systems}, {\Bem 1\/}(1), 93--126.

\bibitem[\protect\BCAY{Brachman, Fikes, \BBA\ Levesque}{Brachman
  et~al.}{1983}]{brachman-et-al:krypton}
Brachman, R.~J., Fikes, R.~E., \BBA\ Levesque, H.~J. \BBOP 1983\BBCP.
\newblock \BBOQ {KRYPTON}: A functional approach to knowledge
  representation\BBCQ\
\newblock {\Bem IEEE Computer}, {\Bem 16\/}(10), 67--73.

\bibitem[\protect\BCAY{Cohen \BBA\ Hirsh}{Cohen \BBA\
  Hirsh}{1994}]{cohen-hirsh:learning-description-logics}
Cohen, W.~W.\BBACOMMA\  \BBA\ Hirsh, H. \BBOP forthcoming\BBCP.
\newblock \BBOQ Learnability of description logics with equality
  constraints\BBCQ\
\newblock {\Bem Machine Learning}.
\newblock A preliminary version appears in the {\em Proceedings of the Fourth
  Annual Workshop on Computational Learning Theory.}

\bibitem[\protect\BCAY{Devanbu, Brachman, Ballard, \BBA\ Selfridge}{Devanbu
  et~al.}{1991}]{devanbu-et-al:lassie-cacm}
Devanbu, P., Brachman, R.~J., Ballard, B., \BBA\ Selfridge, P.~G. \BBOP
  1991\BBCP.
\newblock \BBOQ {LaSSIE}: {A} knowledge-based software information system\BBCQ\
\newblock {\Bem Communications of the ACM}, {\Bem 34\/}(5), 35--49.

\bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, \BBA\ Nutt}{Donini
  et~al.}{1991}]{donini-et-al:tractable}
Donini, F.~M., Lenzerini, M., Nardi, D., \BBA\ Nutt, W. \BBOP 1991\BBCP.
\newblock \BBOQ Tractable concept languages\BBCQ\
\newblock In {\Bem Proceedings of the Twelfth International Joint Conference on
  Artificial Intelligence}, \BPGS\ 458--453. International Joint Committee on
  Artificial Intelligence.

\bibitem[\protect\BCAY{Doyle \BBA\ Patil}{Doyle \BBA\
  Patil}{1991}]{doyle-patil:two-theses}
Doyle, J.\BBACOMMA\  \BBA\ Patil, R. \BBOP 1991\BBCP.
\newblock \BBOQ Two theses of knowledge representation: {L}anguage
  restrictions, taxonomic classification, and the utility of representation
  services\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 48\/}(3), 261--297.

\bibitem[\protect\BCAY{Pitt \BBA\ Frazier}{Pitt \BBA\
  Frazier}{1994}]{pitt-frazier:learning}
Pitt, L.\BBACOMMA\  \BBA\ Frazier, M. \BBOP 1994\BBCP.
\newblock \BBOQ Classic learning\BBCQ\
\newblock In {\Bem Proceedings of the Seventh Annual ACM Conference on
  Computational Learning Theory}\ New Brunswick, NJ. ACM Press.

\bibitem[\protect\BCAY{Heinsohn, Kudenko, Nebel, \BBA\ Profitlich}{Heinsohn
  et~al.}{1992}]{heinsohn-et-al:empirical}
Heinsohn, J., Kudenko, D., Nebel, B., \BBA\ Profitlich, H.-J. \BBOP 1992\BBCP.
\newblock \BBOQ An empirical analysis of terminological representation
  systems\BBCQ\
\newblock In {\Bem Proceedings of the Tenth National Conference on Artificial
  Intelligence}, \BPGS\ 767--773. American Association
  for Artificial Intelligence.

\bibitem[\protect\BCAY{Hollunder \BBA\ Nutt}{Hollunder \BBA\
  Nutt}{1990}]{hollunder-nutt:subsumption-algorithms}
Hollunder, B.\BBACOMMA\  \BBA\ Nutt, W. \BBOP 1990\BBCP.
\newblock \BBOQ Subsumption algorithms for concept languages\BBCQ\
\newblock Research report\ RR-90-04, German Research Center for Artificial
  Intelligence (DFKI).

\bibitem[\protect\BCAY{Lenzerini \BBA\ Schaerf}{Lenzerini \BBA\
  Schaerf}{1991}]{lenzerini-schaerf:concept-query-languages}
Lenzerini, M.\BBACOMMA\  \BBA\ Schaerf, A. \BBOP 1991\BBCP.
\newblock \BBOQ Concept languages and query languages\BBCQ\
\newblock In {\Bem Proceedings of the Ninth National Conference on
Artificial Intelligence}, \BPGS\ 471--476. American Association
  for Artificial Intelligence.
\bibitem[\protect\BCAY{Levesque \BBA\ Brachman}{Levesque \BBA\
  Brachman}{1987}]{levesque-brachman:tractability}
Levesque, H.~J.\BBACOMMA\  \BBA\ Brachman, R.~J. \BBOP 1987\BBCP.
\newblock \BBOQ Expressiveness and tractability in knowledge representation and
  reasoning\BBCQ\
\newblock {\Bem Computational Intelligence}, {\Bem 3\/}(2), 78--93.

\bibitem[\protect\BCAY{MacGregor \BBA\ Bates}{MacGregor \BBA\
  Bates}{1987}]{macgregor-bates:loom}
MacGregor, R.~M.\BBACOMMA\  \BBA\ Bates, R. \BBOP 1987\BBCP.
\newblock \BBOQ The {Loom} knowledge representation language\BBCQ\
\newblock \BTR\ ISI/RS-87-188, Information Sciences Institute, University of
  Southern California.

\bibitem[\protect\BCAY{Mays, Apt{\'e}, Griesmer, \BBA\ Kastner}{Mays
  et~al.}{1987}]{mays-et-al:financing}
Mays, E., Apt{\'e}, C., Griesmer, J., \BBA\ Kastner, J. \BBOP 1987\BBCP.
\newblock \BBOQ Organizing knowledge in a complex financial domain\BBCQ\
\newblock {\Bem IEEE Expert}, {\Bem 2}, 61--70.

\bibitem[\protect\BCAY{Nebel}{Nebel}{1988}]{nebel:back-complexity}
Nebel, B. \BBOP 1988\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}]{nebel:intractable}
Nebel, B. \BBOP 1990\BBCP.
\newblock \BBOQ Terminological reasoning is inherently intractable\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 43\/}(2), 235--249.

\bibitem[\protect\BCAY{Nebel, Peltason, \BBA\ von Luck}{Nebel
  et~al.}{1991}]{dagstuhl-workshop}
Nebel, B., Peltason, C., \BBA\ von Luck, K.\BEDS. \BBOP 1991\BBCP.
\newblock {\Bem International Workshop on Terminological Logics}. 
	Document D-91-13, German Research Center for Artificial
	Intelligence (DFKI). 

\bibitem[\protect\BCAY{Owsnicki-Klewe}{Owsnicki-Klewe}{1988}]{owsnicki-klewe:c%
onfiguration}
Owsnicki-Klewe, B. \BBOP 1988\BBCP.
\newblock \BBOQ Configuration as a consistency maintenance task\BBCQ\
\newblock In Hoeppner, W.\BED, {\Bem Proceedings of GWAI-88---the 12th German
  Workshop on Artificial Intelligence}, \BPGS\ 77--87. Springer Verlag.

\bibitem[\protect\BCAY{Patel-Schneider}{Patel-Schneider}{1984}]{patel-schneide%
r:small}
Patel-Schneider, P.~F. \BBOP 1984\BBCP.
\newblock \BBOQ Small can be beautiful in knowledge representation\BBCQ\
\newblock In {\Bem Proceedings of the IEEE Workshop on Principles of
  Knowledge-Based Systems}, \BPGS\ 11--16. IEEE Computer Society.

\bibitem[\protect\BCAY{Patel-Schneider}{Patel-Schneider}{1987}]{patel-schneide%
r:thesis}
Patel-Schneider, P.~F. \BBOP 1987\BBCP.
\newblock {\Bem Decidable, Logic-Based Knowledge Representation}.
\newblock Ph.D.\ thesis, Department of Computer Science, University of Toronto.

\bibitem[\protect\BCAY{Patel-Schneider}{Patel-Schneider}{1989a}]{patel-schneid%
er:terminological-logic}
Patel-Schneider, P.~F. \BBOP 1989a\BBCP.
\newblock \BBOQ A four-valued semantics for terminological logics\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 38\/}(3), 319--351.

\bibitem[\protect\BCAY{Patel-Schneider}{Patel-Schneider}{1989b}]{patel-schneid%
er:nikl-undecidable}
Patel-Schneider, P.~F. \BBOP 1989b\BBCP.
\newblock \BBOQ Undecidability of subsumption in {NIKL}\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 39\/}(2), 263--272.

\bibitem[\protect\BCAY{Peltason, von Luck, \BBA\ Kindermann}{Peltason
  et~al.}{1991}]{berlin-taxonomic-workshop}
Peltason, C., von Luck, K., \BBA\ Kindermann, C.\BEDS. \BBOP 1991\BBCP.
\newblock {\Bem Terminological Logic Users Workshop}.
\newblock Fachbereich Informatik, Technische Universit{\"a}t Berlin.

\bibitem[\protect\BCAY{Peltason, von Luck, Nebel, \BBA\ Schmiedel}{Peltason
  et~al.}{1987}]{peltason-et-al:back-users-guide}
Peltason, C., von Luck, K., Nebel, B., \BBA\ Schmiedel, A. \BBOP 1987\BBCP.
\newblock \BBOQ The user's guide to the {BACK} system\BBCQ\
\newblock Kit-report~42, Fachbereich Informatik, Technische Universit{\"a}t
  Berlin.

\bibitem[\protect\BCAY{Resnick, Borgida, Brachman, McGuinness, \BBA\
  Patel-Schneider}{Resnick et~al.}{1992}]{resnick-et-al:classic-manual}
Resnick, L.~A., Borgida, A., Brachman, R.~J., McGuinness, D.~L., \BBA\
  Patel-Schneider, P.~F. \BBOP 1992\BBCP.
\newblock \BBOQ {CLASSIC} description and reference manual for the {COMMON
  LISP} implementation\BBCQ\
\newblock AI Principles Research Department, AT\&T Bell Laboratories.

\bibitem[\protect\BCAY{Schmidt-Schauss}{Schmidt-Schauss}{1989}]{schmidt-schaus%
s:undecidable}
Schmidt-Schauss, M. \BBOP 1989\BBCP.
\newblock \BBOQ Subsumption in {KL-ONE} is undecidable\BBCQ\
\newblock In {\Bem Proceedings of the First International Conference on
  Principles of Knowledge Representation and Reasoning}, \BPGS\ 421--431.
  Morgan Kaufmann. 

\bibitem[\protect\BCAY{Wright, Weixelbaum, Brown, Vesonder, Palmer, Berman,
  \BBA\ Moore}{Wright et~al.}{1993}]{wright-et-al:prose}
Wright, J.~R., Weixelbaum, E.~S., Brown, K., Vesonder, G.~T., Palmer, S.~R.,
  Berman, J.~I., \BBA\ Moore, H.~H. \BBOP 1993\BBCP.
\newblock \BBOQ A knowledge-based configurator that supports sales,
  engineering, and manufacturing at {AT\&T} network systems\BBCQ\
\newblock In {\Bem Proceedings of the Innovative Applications of Artificial
  Intelligence Conference}, \BPGS\ 183--193. American
  Association for Artificial Intelligence.

\end{thebibliography}
%%End of bibliography file from BibTeX
\bibliographystyle{theapa}

%ENDEND

\appendix
\section{Intractability of Reasoning with {\sc ONE-OF}}

We present here a formal proof that subsumption with set descriptions
is in fact NP-hard.\footnote{Our original result was submitted for
publication in 1990. A different, independent, proof of the same
result has since been outlined in
\shortcite{lenzerini-schaerf:concept-query-languages}.}

We will show that if a term language allows a set description
then it will need to do ``case analysis'' in order to check
whether the extension of an individual belongs to a description or
not; this is because this constructor behaves like disjunction if its
elements can be extensions of individuals whose membership in all terms is
not known a priori, i.e., non-host individuals. 
In particular, we will show how to encode the testing of {\em
unsatisfiability} of a formula in 3CNF as the question of recognizing
an individual as an instance of a description. Since this problem is known
to be NP-hard, we have strong indication of its intractability.

Start with a formula $F$, in 3CNF.
Using DeMorgan's laws, construct formula $G$, which is the negation
of $F$, and which is in 3DNF. 
Testing the validity of $G$ is equivalent to checking the unsatisfiability
of $F$.

Construct for every propositional symbol $p$ used in $F$, two
individual names \syntax{P} and \syntax{\hat{P}}.
(Here \syntax{\hat{P}} will represent the negation of $p$.)
Each individual will have attribute \name{truthValue}, with possible
fillers \name{True} and \name{False}
\begin{displaynotation}
\Instance{P, \hat{P}}{\all{truthValue}{ \set{ True\, False}}}.
\end{displaynotation}
To make sure that \name{P} and \syntax{\hat{P}} have exactly one, and
opposite, truth values, we create two more individual names, \name{Yesp} and
\name{Nop}, with additional attributes \name{approve} and \name{deny}
respectively, whose fillers need to have truth value \name{True} and
\name{False} respectively:
\begin{displaynotation}
\Instance{Yesp}{\all{approve}{(\set{ P\, \hat{P}} \And
                       \all{  truthValue}{ \set{ True}})}}
\\
\Instance{Nop}{\all{  deny}{(\set{ P\, \hat{P}} \And      
                       \all{  truthValue}{ \set{ False}})}}
\end{displaynotation}

Now, given the formula $G ~=~ C1 \vee C2 \vee \ldots \vee Cn$, create
individual names
\name{C1}, \name{C2}, \ldots, \name{Cn}, each with role \name{conjuncts}
containing the propositions that are its conjuncts.
For example, if $C1 = p \wedge \neg q \wedge \neg r$ then
\begin{displaynotation}
\Instance{C1}{\all{ conjuncts}{\set{ P\, \hat{Q}\, \hat{R}}} \And
             \atleast{3}{conjuncts}}.
\end{displaynotation}

Finally, construct individual \name{G} to have
\name{C1}, \name{C2}, \ldots, \name{Cn} as  possible 
fillers  for a new role \name{disjunctsHolding}:
\begin{displaynotation}
\Instance{G}{\all{disjunctsHolding}{\set{C1\, C2\, \ldots \, Cn}}}.
\end{displaynotation}

The formula $G$ will then be valid iff there is always at least one
disjunct that holds.
This is equivalent to membership in the concept \name{VALID-FORMULAE}
defined as 
\begin{displaynotation}
\atleast{1}{disjunctsHolding}  \And
\all{ disjunctsHolding}{(\all{conjuncts}{( \all{ truthValue}{\set{True}})})}.
\end{displaynotation}

The above shows that recognizing whether individuals are instances of
descriptions is intractable in the presence of set descriptions, minimum
number restrictions, and value restrictions.

\medskip

We can convert this into a question concerning the subsumption of two
descriptions by essentially making all the individuals involved
attribute-fillers for new dummy attributes, and their descriptions as
restrictions on these attributes. Then if the description is non-empty then
these attribute values must satisfy the corresponding restrictions.

So, define concept \name{UPPER} to be
\begin{displaynotation}
\all{formula}{\name{VALID-FORMULAE}}
\end{displaynotation}
and define concept \name{LOWER} to be
\begin{displaynotation}
\all{\name{dummy1-p}}{(\set{P} \And {\em [P's\ concept\ descriptor]})} \And\\
          \all{\name{dummy2-p}}{( \set{\hat{P}} \And
	{\em [\hat{P}'s\ concept\ descriptor]}
)} \And\\
          \all{\name{dummy3-p}}{( \set{Yesp} \And \ldots )} \And \\
          \all{\name{dummy4-p}}{( \set{Nop} \And \ldots )} \And \\
 	  \ldots\\
 	  \all{\name{dummy5-c}_i}{( \set{C_i} \And \ldots)} \And\\
      \ldots\\
      \all{formula}{ (\set{ G} \And \ldots)}
\end{displaynotation}
Then in any database state either concept \name{LOWER} has no instances, in
which case it is a subset of the extension of \name{UPPER}, or it has at least
one instance, in which case the individual names filling the various dummy
attributes must have the properties ascribed to them, whence
\name{C} will be in \name{VALID-FORMULAE} (and hence \name{UPPER} will subsume
\name{LOWER}) iff \name{C} is valid, which completes the proof.


\end{document}


