%\documentstyle[11pt,alex]{article}
\documentstyle[alex1,jair,twoside,11pt,theapa]{article}
%\documentclass{article}
%\usepackage[]{alex,jair}


\renewcommand{\vbar}{\mbox{$\;\mid\;$}}
\newcommand{\kbee}{\mbox{$KB\:\vdash\:$}}
\newcommand{\EE}{\mbox{$~\vdash\~$}}
\newcommand{\entails}{\mbox{$\:\models\:$}}
\newcommand{\kbent}{\mbox{$KB\:\models\:$}}
\newcommand{\hasfiller}[3]{ #1 \isin {\bf fills}(#2,#3)}
\newcommand{\hasclosed}[3]{ #1 \isin {\bf closedFillers}(#2,#3)}
\newcommand{\closed}[3]{ #1:{\bf allFillersKnown}(#2,#3)}
\newcommand{\notisin}{\mbox{$ \;\not\longrightarrow\; $}}
\renewcommand{\isin}{\mbox{$ \;\longrightarrow\; $}}

   \small\tt \hyphenchar\the\font=45
   \normalsize\tt \hyphenchar\the\font=45
   \small\sf \hyphenchar\the\font=45
   \normalsize\sf \hyphenchar\the\font=45



\newcommand{\myitem}[1]{\smallskip 

\noindent {\large {\bf (#1)\ }} }
\def\dotleq{\:\dot{\leq}\:}
\renewcommand{\I}{\mbox{${\cal I}$}}
\renewcommand{\domain}{\mbox{$\Delta^{{\cal I}}$}} 
\renewcommand{\Int}[1]{\mbox{$#1^{{\cal I}}$}}              % 
%\renewcommand{\IntNoMath}[1]{\mbox{#1^{{\cal I}}}}              % 
\newcommand{\ab}[1]{{\Large #1}}
\newcommand{\shortkind}[1]{
%	\parbox{.8in}{\footnotesize{#1}}
{\footnotesize #1}
}
\def\alt{{\tt\bf altern}}
\def\seq{{\tt\bf seq}}
\def\sloop{{\tt\bf loop}}
\def\sing{{\tt\bf single}}
\def\plan{{\tt\bf plan}}
\def\act{{\tt\bf act}}
\def\topexp{\mbox{{\tt\bf top-plan-exp}}}

\def\lessthan{\mbox{$<$}}
\newcommand{\calig}[1]{\mbox{${\cal #1}$}}


\newcommand{\breakit}[1]{
  \begin{tabular}{l} %{c} 
  #1
  \end{tabular}
}

\newcommand{\cbreakit}[1]{
  \begin{tabular}{c} 
  #1
  \end{tabular}
}

\newcommand{\hilite}[1]{#1} %{\underline{#1}}

%\renewcommand{\myfrac}[2]{\mbox{$\frac{\mbox{\normalsize #1}}{\mbox{\normalsize #2}}$}}


\newcommand{\myfractwo}[2]{\mbox{$\frac{\mbox{\small #1}}{\mbox{\small
#2}}$}}
\renewcommand{\myfrac}[2]{\mbox{$\frac{\mbox{\small #1}}{\mbox{\small #2}}$}}



\def\descr{\mbox{\cd{Descriptor}}}


\newcommand{\reclink}[2]{#1\ $\overrightarrow{\mbox{{\tiny 
RecognizeDependsOnMe}}}$\ #2}



\newcommand{\conslink}[2]{#1\ $\overrightarrow{\mbox{{\tiny
ConsistentDependsOnMe}}}$\ #2}

\newcommand{\inflink}[2]{#1\ $\overrightarrow{{\mbox{{\tiny
InferDependsOnMe}}}}$\ #2}


\def\anydate{{\sc any-date}}

\def\dlt{\mbox{$\ \precurlyeq\ $}}
\def\dlt{\mbox{$\ \preceq\ $}}
\def\begintime{BeginTime}
\def\endtime{EndTime}

\def\dl0{DL0}
\newcommand{\opc}[1]{{\sc #1}}
\newcommand{\mycite}[1]{\cite{#1}} 
\def\lang{\mbox{$<$}}
\def\rang{\mbox{$>$}}


\newcommand{\listset}[1]{\{#1\}}
\newcommand{\rules}[3]{
\mbox{#1}&#2&
\parbox{1.5in}{\footnotesize{#3}}    \\
  \\
}
\newcommand{\dom}{\mbox{$\Delta^{\I}$}}     % Domain
\newcommand{\implies}{\mbox{$\:\Rightarrow\:$}}

\newcommand{\db}[1]{}

\def\aline{
\vspace{.1in}
}

\newcommand{\sx}[1]{\cc{#1}}
\newcommand{\cd}[1]{{\tt #1}}
%\newcommand{\cd}[1]{{\sf #1}}
\def\incx{\cd{IncoherentExn}}
\def\incnx{\cd{InconsistentExcn}}
\def\redundx{RedundantExn}





\def\Isa{\mbox{$\:\Longrightarrow\:$}}




% for Classic code: terms 


\newcommand{\signature}[1]{{\it #1}}
\newcommand{\infrule}[1]{\begin{center}  #1 \end{center}}
\def\protoc{{\sc protodl}}
\def\protodl{{\sc protodl}}
\def\classic{{\sc classic}}
\def\clasp{{\sc clasp}}
\def\kandor{{\sc kandor}}
\def\K{{\small\bf Q}}
\def\kk{{\small\bf Q}}
\def\DD{{\small\bf DATE}}

\def\drng{{\tt\bf dateRange}}
\def\prd{{\tt\bf period}}
\def\cand{{\tt\bf and}}
\def\cor{{\tt\bf or}}
\def\cnot{{\tt\bf not}}
\def\prim{{\tt\bf prim}}
\def\range{{\tt\bf range}}
\def\cor{{\tt\bf or}}
\def\all{{\tt\bf all}}
\def\known{{\tt\bf known}}
\def\ALL{{\tt\bf All}}
\def\some{{\tt\bf some}}
\def\anyobject{\mbox{{\bf\sc any-object}}}
\def\thing{{\bf\sc thing}}
\def\nothing{{\bf\sc nothing}}
\def\atleast{\mbox{{\tt\bf at-least}}}
\def\atmost{\mbox{{\tt\bf at-most}}}
\def\sameas{\mbox{{\tt\bf same-as}}}
\def\containedIn{{\tt\bf subset-of}}
\def\oneof{{\tt\bf one-of}}
\def\avr{{\tt\bf at-least-vr}}
\def\fills{{\tt\bf fills}}

\newcommand{\issame}{\mbox{$\:\:\equiv\:\:$}}
\newcommand{\ident}{\mbox{$\:\:\equiv\:\:$}}

\jairheading{10}{1999}{399-434}{10/98}{6/99}
\ShortHeadings{Extensible DL Representation and Reasoning}
{Borgida}
\firstpageno{399}

\title{ Extensible Knowledge Representation:
the Case of Description Reasoners}
\author{
 \name Alex Borgida
 \email borgida@cs.rutgers.edu\\
 \addr Dept. of Computer Science\\Rutgers University
}


\begin{document}
\date{}
\maketitle

\begin{abstract}
 This paper offers an approach to { extensible knowledge
 representation and reasoning}, for a family of formalisms known as
 Description Logics. The approach is based on the notion of adding new
 concept constructors, and includes a heuristic methodology for {
 specifying} the desired extensions, as well as a { modularized
 software architecture} that supports implementing extensions.
The architecture detailed here falls in  the normalize-compared paradigm,
and
 supports both intentional reasoning
(subsumption) involving concepts, and  extensional  reasoning
involving individuals after { incremental} updates to the knowledge
base.

The resulting approach can be used to extend the reasoner  with specialized notions that are motivated by specific
problems or application areas, such as reasoning about dates, plans,
etc. In addition, it provides an opportunity to implement constructors
that are not currently yet sufficiently well understood theoretically,
but are needed in practice. Also, for constructors that are provably
hard to reason with (e.g., ones whose presence would lead to
undecidability), it allows the implementation of incomplete reasoners
where the incompleteness is tailored to be acceptable for the
application at hand.

\end{abstract}

%\noindent {\bf Keywords:} Description logics, knowledge
%representation, extensible reasoning, extensible architecture,
%subsumption, recognizer.


\section{Introduction and Motivation}

Description Logics (DLs) are a family of object-centered formalisms
for representing knowledge about and reasoning with individuals
grouped into classes (here called  {\em concepts}) and related by binary
relations (here called {\em roles}). Descriptions usually have a term-like
notation that uses concept constructors and identifiers to build
definitions of more complex concepts from simpler ones.
For example, the description in Figure~\ref{fig1} is supposed to
capture the noun phrase ``{\em
%\fbox{\parbox[t]{5.5in}{
A collection of objects that are books and that are written  by two or
more authors, who are all Venusians}''.

%\noindent
\begin{figure}[hb]
\begin{display} \cc{
			\cand(
			   BOOK                            
			   \atleast(2,authoredBy)
			   \all(authoredBy, VENUSIAN) )
	   %                \fills(writtenIn, English) )
}\end{display}
\caption{An example description.}\label{fig1}
\end{figure} 

\noindent This is accomplished by using the concept constructor \cand\ to
conjoin terms that represent component notions:
\begin{description}
\item[\cc{BOOK}:]  objects that are  books --- a concept declared
elsewhere, probably as a primitive; 

\item[\cc{\atleast(2,authoredBy)}:] objects that are related to at
least 2 other objects by the \cc{authoredBy} role; the concept
constructor is \atleast\ here;

\item[\cc{\all(authoredBy, VENUSIAN)}:] objects 
that are related by the \cc{authoredBy} role only to objects that
are in the concept  \cc{VENUSIAN}; the concept constructor here is \all.
\end{description}
\noindent
The concept  \cc{VENUSIAN} might itself be defined as a being
whose address includes the planet value Venus: 
\cc{\cand(BEING,} \cc{\all(address,} \cc{\fills(planet,
Venus)))}. (Note that descriptions can be nested.) A more precise
introduction to DLs is presented in Section~\ref{dls}. 

Description logics reason both about intensional notions such as
concepts, and about extensional  aspects having to do with individuals
that can be ascribed descriptions and participate in specific
relationships. DLs 
have found a variety of applications in areas such as data management
\mycite{tkde}, software engineering \mycite{prem:jones}, configuration
management \shortcite{config}, as well as general AI.


A particular description language is characterized, among others,
 by the choice of term constructors in it, and 
 the significant features of DLs are clear, precise
semantics and terminating reasoning algorithms for tasks such as
determining whether a concept is coherent, or whether it is more
general than another one.

A common difficulty faced both by designers and users of
knowledge-base management systems (KBMSs) based on DLs (or any other
logic, for that matter) is that many applications need to keep
information about specialized kinds of data, including strings, dates,
pictures, sequences of values of various kinds, etc., and it is
practically impossible to anticipate all of these as part of language
design.  

A related problem is that if reasoning is to be complete and
efficient, or even decidable, then what can be expressed in the
language must be limited.  For example, if in Figure~\ref{fig1} we
also wanted to say that the authors speak the language in which the
book is written, there is a concept constructor already discussed in
the literature, called \containedIn, with which one could express such
a constraint as  \cc{\containedIn( [writtenIn]
[authoredBy,speaks] )}.  Unfortunately, reasoning in a language that
supports constructors \cand, \all\ and \containedIn\ is known to be
undecidable \mycite{undecide-sameas}.  This means that the selection
of concept constructors in the language is a matter of very careful
consideration for the system designer, who is faced with several
choices: (a)  Select a particular subset of constructors for which a
sound and complete reasoning algorithm is known; if the language is
sufficiently limited, this procedure is guaranteed to be ``fast''
(e.g., in polynomial time); otherwise, its worst case complexity is
non-polynomial, though in practice the algorithm may behave
well. Living with ``limited languages'' is however not always easy
\mycite{doyle:patil}.  (b) Choose a larger set of constructors
(possibly one which is even undecidable), and implement an incomplete
reasoner; this however requires having to explain to the user which
inferences will or will not be made.  Both alternatives have
different shortcomings, but, from our viewpoint, a  significant common
problem is that  in all cases it is the { designer} of the DL system who
makes these decisions {\em 
ahead of time}, leaving the user to sort out the consequences later
on.
\comment{
The hypothesis of this paper is that this is not just a
temporary problem, but that in fact it will never be possible to
design a ``perfect'' DL that will meet every user's expressive needs
while preserving effectiveness and predictability of reasoning.
}

We propose to attack the above problems by starting with a relatively
small, kernel language and system, and then providing facilities to
{\em extend it by adding new concept constructors}. Such extensions
are not to be undertaken lightly, since they provide opportunities for
errors.  Some of the extensions will be standard DL constructors for
which complete reasoning can be implemented. Such extensions could be
readily available in a library\footnote{It is important to clarify
from the beginning that the addition of constructors is often not a
simple incremental process: some constructors may behave well
independently, but cause problems when brought into the same
language.}  . Other extensions will involve standard DL constructors
which are known to be hard to reason with, and for which only an
incomplete reasoning algorithm is provided, because, for example, the
problem is undecidable or because the only algorithms currently known
involve combinatorial search.  In this second case, consultation with
the user may help determine which inferences the implementation should
make. For example, in \classic, for the sake of a clearer semantics
the system designers chose to draw no inferences about an individual
based on its presence in a concept \mycite{jair}, although {\em some}
of these inferences are not hard to implement.  Finally, new concept
constructors can be added for notions that are either domain specific
(e,g,. plans, time), or which are of great practical utility but whose
interaction with the full spectrum of DL constructors is not yet fully
understood theoretically; such notions include keys/unique identifiers
\mycite{borgida:weddell} and part-whole relationships
\mycite{lambrix}.



\comment{
The following are some  reasons to start with a  small core language:
 (i) even if not used in some application, extraneous constructors may
carry an overhead in data structure space and in time spent looking
for them in  internal representations;
 (ii) if all constructors are added according to the extensibility
paradigm presented here, then their implementation is  easier to alter 
when new constructors are added, which interact with old ones.
}

To support this, we develop a {well-modularized architecture} for
DL-KBMSs that are implemented using the ``normalize-compare'' approach
(see Section~\ref{implem}); this architecture expects a set of
procedures to be filled in for each new concept constructor extending
the original language. In addition, we propose methodological
heuristics for specifying what these procedures need to do. Note that
our goal is to obtain close to the same efficiency as would have been
offered by a custom-built DL reasoner.

\comment{
Our approach is openly pragmatic: we believe that although it is
clearly preferable to have a totally correct reasoner, in the not
infrequent cases where the user will want more (including features
that would make the language undecidable), it is better to provide for
a procedural way of extending the reasoning with a declarative
representation, then to turn the user away or force the user to encode
the entire rest of the knowledge and reasoning within an impenetrable
program.  
}

Of course, the approach presented here is not a panacea for knowledge
representation and reasoning. First of all, to the extent that
normalize-compare algorithms are unable to reason in a {\em complete}
manner with DL constructors involving incomplete knowledge such as
disjunction, the present system is also likely to suffer the same
deficiencies.  Second, the present work has not yet addressed DL
notions such as role constructors, recursive concepts, and general
constraints (to be described later). Finally, there are many other
notions in knowledge representation, such as the full spectrum of
epistemic and other non-monotonic reasoning, abduction, case-based
reasoning, etc., which are likely to require a thorough overhaul of the
entire reasoning architecture, and hence are likely not to be
accommodated properly by the present approach.


\medskip 

The outline of the rest of the paper is as follows: Section~\ref{dls}
 provides an introduction to DLs, their syntax and semantic
description, and the services
provided by KBMSs concerning reasoning with concepts, especially the
``subsumption'' relationship. 
  Section~\ref{conc-reason} introduces the architecture of the
proposed \protodl\ approach to DL reasoning, provides an overview of the
methodology for extending it, and illustrates it with constructors
involving { dates}; it terminates by discussing successes and
limitations of the proposed \protodl\ approach to extension, an its
relationship to one particular other approach that is directly relevant.

In Sections~\ref{ind-reason} and \ref{indkb} we repeat the above
process, but considering this time reasoning about individuals, and
focusing  on how to support efficiently {\em incremental}
updates to the knowledge base.

We conclude by discussing relevant related work and summarizing the
contributions and limitations of the \protodl\ approach.


\section{Description Logics: An Introduction}\label{dls}

DLs are used to describe situations using various kinds of {\em
individuals}, related by {\em roles}, and grouped into {\em
concepts}\comment{In our examples, we follow the convention that
concepts are written in capital letters, roles in lower-case, and
individual's names have their first letters in capitals.}. Roles that
are restricted to be (partial) functions are distinguished, and are
called {\em attributes}. 

In this section we present the syntax and semantics of DLs, as well as
outlining the interaction with a typical DL-based KBMS, and some
implementation strategies.

\subsection{Syntax and Semantics}

 As illustrated in Figure~\ref{fig1}, DLs
provide a { compositional} and { structured} language for talking
about these kinds of things. Composite concepts are obtained
according to the syntax presented in Table~\ref{syntax}, which
includes the concept constructors mentioned  in this paper.
 The meta-symbols have the following referents: $CN$
is a concept name, $p$ is an atomic role (including an attribute), $f$
is an attribute, $C$ and $D$ are  general concepts, $b$ is an 
individual, while $n$ is an integer; subscripts may
occasionally be added to the above.
\begin{table}[hbt]








\begin{display}        $RoleChain$ ::= \cc{[$p_1,\ \ldots ,p_n$]}
        $AttributeChain$ ::= \cc{[$f_1,\ \ldots ,f_n$]}
        $C$ ::= \thing  \vbar \nothing \vbar $CN$ 
              \vbar \cand( $C_1, \ldots, C_n$ ) \vbar \atleast($n$,$p$) \vbar \atmost($n$,$p$)  
              \vbar \all($p$,$C$) \vbar \some($p$,$C$) \vbar \fills($p$,$b$) \vbar \oneof($b_1, \ldots b_n$)
              \vbar \sameas($AttributeChain_1$, $AttributeChain_2$) 
              \vbar \containedIn($RoleChain_1$, $RoleChain_2$)
\end{display}
\comment{

	\vbar \nothing 
%	\vbar \cc{STRING}
%	\vbar \cc{INTEGER}
	\vbar $CN$ 
	\vbar \cand( $C_1, \ldots, C_n$ ) 
	\vbar \atleast($n$,$p$) 
	\vbar \atmost($n$,$p$)  
        \vbar \all($p$,$C$) 
        \vbar \some($p$,$C$) 
	\vbar \fills($p$,$b$)  
        \vbar \oneof($b_1, \ldots b_n$)
	\vbar \sameas($AttributeChain_1$, $AttributeChain_2$)
	\vbar \containedIn($RoleChain_1$, $RoleChain_2$)
}%cmt
\caption{Syntax of Concept Constructors Used.}\label{syntax}
\end{table}

 To give meaning to the above syntactic terms, one can
give descriptions a denotational semantics using an interpretation
\I=(\domain,\Int{\cdot}). \I\ starts by assigning to each concept
name a subset of the domain \domain, to each role a subset of \domain
$\times$ \domain, to each attribute an element of $\domain \times
\domain$ restricted to be functional, and to each individual some
element of \domain. The interpretation is then extended to composite
terms as follows.  First, role chains (resp. attribute chains) are
interpreted as mappings resulting from relation composition:
\[\Int{[p_1,\cdots ,p_n]} 
=
\{ x \mapsto S_x \ \mid \ S_x=\{ y \mid \exists z_1,...,z_{n+1}.\ 
 z_1=x \wedge z_{n+1}=y \wedge \bigwedge_{i=1}^{n} (z_i,z_{i+1})\in
\Int{p_i}\} \}
\] 
Table~\ref{densem} then presents the interpretation of complex terms
using the interpretation of their components.

\begin{table}[h]
%\begingroup
%\scriptsize\tabcolsep=.5\tabcolsep
%\leavevmode\kern-.3in
%\begin{tabular}{|lll|}
\begin{center}
\begin{tabular}{|ll|}
\hline
 {\bf TERM}
   & {\bf INTERPRETATION}
%			    & {\bf TRANSLATION TO FOL}
\\
\hline
\hline
\thing
   &  $\domain$ 
%	& $   True$
\\
\hline
\nothing
   &  $\emptyset$ 
%	& $   False$
\\
\hline
 \cand( $C_1, \ldots, C_n$ ) 
   &  $ \Int{C_1} \cap \ldots \cap \Int{C_n}$ 
%	& $	C(\xx) \wedge D(\xx)$
\\
\hline
%\cor(C,D)
%   &  $ \Int{C} \cup \Int{D}$ 
%	& $	C(\xx) \vee D(\xx)$
%\\
%\hline
%\cnot(C)
%   & $ \domain \setminus \Int{C}$ 
%	& $	\neg C(\xx)$
%\\
%\hline
\atleast($n,p$)
   & $\set{ d \in \domain \mid \card{\Int{p}(d)} \geq n}$  
%	& $	\exists z_1,...,\exists z_n \ R(\xx,z_1) \wedge \ldots \wedge R(\xx,z_n) \wedge z_i\not=z_j$
\\
\hline
\atmost($n,p$)
   & $\set{ d \in \domain \mid \card{\Int{p}(d)} \leq n}$  
%	& $\begin{array}[t]{l}	\forall z_1,...,z_n,\forall z_{n+1} \ (R(\xx,z_1) \wedge \ldots 
%\wedge R(\xx,z_{n+1}) \implies \\
%(z_1=z_2 \vee \ldots \vee z_n=z_{n+1}) \end{array}$
\\
\hline
\all($p,C$)
   & $\set{ d \in \domain \mid \Int{p}(d) \subseteq \Int{C}}$  
%	& $	\forall z\ R(\xx,z) \implies C(z)$
\\
\hline
\some($p,C$)
   & $\set{ d \in \domain \mid \Int{p}(d) \cap \Int{C} \neq \emptyset}$  
%	& $ \exists z\ R(\xx,z) \wedge C(z)$
\\
\hline
\fills($p,b$)
   & $\set{ d \in \domain \mid \Int{b} \in \Int{p}(d)  }$  
%	& $	R(\xx,b)$
\\
\hline
\oneof(b$_1$,...,b$_m$)
   & $\set{\Int{b_1}, \ldots, \Int{b_m}}$
%	& $	\xx=b_1 \vee \ldots \vee \xx=b_m$
\\
\hline
\sameas($FC_1,FC_2$)
   & $\set{ d \in \domain \mid \Int{FC_1}(d) = \Int{FC_2}(d) \wedge
\Int{FC_1}(d)\neq \emptyset}$  
%	& $	\forall z\ R(\xx,z) \iff q(\xx,z)$
\\
\hline
\containedIn($RC_1,RC_2$)
   & $\set{ d \in \domain \mid \Int{RC_1}(d) \subseteq \Int{RC_2}(d)}$  
%	& $	\forall z\ R(\xx,z) \implies q(\xx,z)$
\\
\hline
\end{tabular}
\end{center}
\caption{Interpretation of DL Constructors.}\label{densem}
\end{table}


  Alternatively, by noting that concepts are like unary predicates,
and roles are like binary predicates, we can offer translation schemes
from descriptions to Predicate Calculus.  For example,
\cc{\cand(AMERICAN,OLD)} corresponds to the formula
\cc{AMERICAN}$(\gamma) \wedge $\cc{OLD}$(\gamma)$, where $\gamma$
is a free variable, while \cc{\all(authoredBy,VENUSIAN)} corresponds
to $\forall y.{\tt authoredBy}(\gamma,y) \implies\ $  {\tt VENUSIAN}$(y)$. 


The connection between these two kinds of specifications is that
interpretations can be applied to both predicate calculus formulas as
well as concepts~\mycite{baader:equivalence,borgida:aij}: given a
description $C$, with corresponding logical formula $\Psi_C(\gamma)$,
  and an interpretation \I, the denotation 
\Int{C} is identical to the set of values $d\in\domain$ for which
\Int{\Psi_C(\gamma)} is true, when \I\ is extended to map $\gamma$ to
$d$. 

\smallskip

 Finally, we remark that many DLs also allow {\em role
constructors}; for example, \cc{isAuthorOf} can be defined as
the converse of the \cc{authoredBy} relation, by writing
\inverse({\tt authoredBy}). In this paper we do not consider role
constructors (hence equating roles with role names).

\subsection{Subsumption Reasoning with Concepts}
The real significance of DLs is that one can {\em reason} about
descriptions. Traditionally, the standard
question one asks is whether one description is more general than ({\em subsumes})
another. For example, we would expect that the description in
Figure~\ref{fig1} subsumes the following description, which requires
in addition that the books be published in at most the four countries
enumerated, and that  there be at least three (rather than two) authors,
who are to be married to earthlings:
\begin{display} \cc{
             \cand(
                BOOK                            
                \all(publishedIn, \oneof(Usa,France,Germany,Italy))
                \atleast(3,authoredBy)
                \all(authoredBy, \cand( VENUSIAN,
                                           \all(marriedTo, TERRESTRIAL)))
                )
}\end{display}
Formally, subsumption between concepts $C$ and $D$, written as
$C$ \isa $D$, holds iff $\Int{C} \subseteq \Int{D}$ for all
 interpretations \I. 
\comment{
  (If we translated concepts to predicate logic formulas,
  subsumption corresponds to the validity of the formula
   $\forall \gamma.\Psi_C(\gamma) \implies \Psi_D(\gamma)$.)
 }%cmt
In addition, we say that a description $C$ is {\em incoherent} iff
its denotation \Int{C} is the empty set in all interpretations \I.
Note that this is the case iff $C \Isa \nothing$.

The semantics of concept constructors, and especially the deductions
performed by a particular system can also be specified using proof
theory.  A proof-theoretic specification in the ``natural semantics''
style \mycite{axiomatics}, would
indicate, among others, that greater bounds on the number of role
fillers for role $p$ lead to more specialized concepts:
\[
{\large
\myfrac{ $m \geq n$
}{
 $\atleast(m,p) \isa \atleast(n,p)$}
}
\]
This rule can be paraphrased as
 {\em ``IF one can prove $m\geq n$ THEN
 one can write as the next line of a proof that $\atleast(m,p) \isa
 \atleast(n,p)$.''}
 Such a rule allows us to prove that\\
 \cc{\atleast(2,authoredBy)} \isa \cc{\atleast(1,authoredBy)}.

As usual, it is possible (and desirable) to demonstrate   that the
rules of inference are sound and complete with respect to the
denotational semantics.  Rules
of inference are useful in characterizing reasoners that are
incomplete with respect to the standard denotational semantics, by
describing either the inferences performed, or the ones missing.
Also,
as we shall argue below, rules of inference can form a good starting point for
developing implementations.

\subsection{ DL Concept KBMS}
A concept knowledge base CKB (also known as a T-box) records
constraints on concept names, including {\em definitions} (such as the
concept \cc{VENUSIAN} mentioned in our examples) and {\em necessary
conditions for primitive concepts} (e.g., a \cc{BOOK} would be required
to have at least one author). In some DLs it is possible to state
general subsumption constraints between arbitrary descriptions, but
this will not be permitted in this paper.

Formally, CKB  is a tuple $({\cal
R,F,C,O,N,D})$ where ${\cal R,F,C,O}$ are respectively the sets of
role, attribute, concept and individual object identifiers declared. Concept names are either {\em
primitive/atomic concept names}, $PN$, which have associated a
necessary condition $PN \dotleq C$ in the set ${\cal N}$ of
necessary conditions; or {\em defined concept names},
$DN$, which have associated a definition $DN \doteq C$ in the set
${\cal D}$ of definitions.
An interpretation \I\ is a model of $PN \dotleq C$ iff $\Int{PN}
\subseteq \Int{C}$, and is a model of $DN \doteq C$ iff $\Int{DN} =
\Int{C}$. An interpretation is a model of CKB if it is a model of all
conditions in ${\cal N}$ and ${\cal D}$.

$C$ is said to subsume $D$ in the presence of a knowledge base CKB
(written CKB \entails $C \isa D$), iff $\Int{C}\subseteq\Int{D}$ for all
models \I\ of CKB.

In this paper we are restricting ourselves to
non-recursive knowledge bases, where definitions and necessary conditions
are given at the same time as the name is declared, and they can 
only involve previously declared identifiers.

\medskip

A DL-based {\em knowledge base management system}
supports certain update operations, which affect the CKB
 (${\cal R,F,C,O,N,D} $) as follows:\\

\smallskip
\begin{tabular}{|ll|}
\hline
Operation & Effect
\\ 
\hline
\hline
\opc{declare-primitive-role}($p$)
 & $p$ is added to \calig{R}
\\ 
\hline
\opc{declare-primitive-attribute}($f$)
 & $f$ is added to \calig{F}
\\
\hline
\opc{declare-individual}($b$)
 & $b$ is added to \calig{O}
\\
\hline
\opc{declare-primitive-concept}($PN$,$D$)
 & $PN$ is added to \calig{C},
 and $PN \dotleq D$ to \calig{N }
\\ 
\hline
\opc{declare-defined-concept}($CN$,$D$)
 & $CN$ is added to \calig{C}, and $CN \doteq D$ to \calig{D}
\\
\hline
\end{tabular}

 \bigskip

\noindent In return, we expect the KBMS to respond to inquiries, which include
retrieving the declarations entered and at least the following
operations:

\bigskip

\begin{tabular}{|lll|}
\hline
Question  & Answer type &Response
\\
\hline
\hline
\opc{ask-subsumes?}($C,D$)
 & Boolean
 & true iff CKB\entails$C \isa D$
\\
\hline
\opc{ask-ancestors}($C$)
 & SET(ConceptName) 
 & \{$CN\in$\calig{C} \vbar  CKB\entails$C \isa CN$\} 
\\
\hline
\opc{ask-is-incoherent?}($C$)
 & Boolean
 & true iff CKB\entails$C$ \isa \nothing
\\
\hline
%\opc{ask-least-common-subsumer}($C_1,C_2$)
% & Description
% & $D$ such that $C_i \isa D$, and $D \isa C$ for any\\
% & & $C$ such that $C_i \isa C$ 
\end{tabular}

\bigskip

A number of other operations on concepts have been found to
be useful, including  (i) computing the least common subsumer of two
concepts \mycite{cohen:lcs} (useful for machine learning), (ii) matching
concepts against patterns \mycite{match:kr96} (useful in large KBs for
viewing only relevant aspects of concepts), (iii) finding what {\em
additional} information has been deduced about a concept or especially
an individual  given the information in the KB (see Section~\ref{ind-kbms}).

\medskip

To facilitate answering the above questions, and others like them, the
 DL-KBMS almost always performs {\em concept classification}: named
 concepts (``classes'') are organized into the so-called IsA
 hierarchy, finding for each class the most specific other classes
 that subsume it.  The classification algorithm relies on the \isa\
 relationships,  treating it as a subroutine, and as such is
 largely DL-independent. Interesting previous work in this area has
 been reported by Baader et al~\shortcite{empirical}.


The KBMS is also charged with a number of clerical tasks, including
keeping a symbol table of the  declarations,
maintaining and accessing efficiently the precomputed IsA hierarchy,
signaling definitions/declarations that are redundant (i.e., a concept
which is equivalent to a previously defined one) or are incoherent.

DL-KBMS perform inferences on individuals, as well as concepts. The
operations involved will be described in Section~\ref{indkb}.

\subsection{Reasoning Strategies}\label{implem}

There are two general approaches to answering the fundamental subsumption
question underlying the DL-KBMS operations.
 
  One approach is based on theorem proving techniques specially
 adapted for descriptions, particularly variants of tableau techniques
 that determine the subsumption A\Isa~B by checking for the
 unsatisfiability of $A\wedge \neg B$; systems such as {\sc kris}
 \shortcite{empirical},{\sc crack} \cite{franconi}, {\sc FaCT}
\mycite{horrocks} and {\sc  DLP} \mycite{dlp} follow this approach. Such systems have the
 advantage of being  provably
 complete. Although the worst-case complexity bounds of the
subsumption problems  are sometimes quite high (EXPTIME
 complete), recent empirical evidence  shows that their performance
for computing subsumption on large realistic KBs is quite effective
\mycite{dl:comparison}.
\comment{
Unfortunately, such languages would seem to have problems with 
some of the more recent notions such as least common subsumer
(which is trivialized if disjunction is present, and disjunction seems
necessary whenever negating concepts) and finding the ``completion''
of concepts (everything that is inferable about the concept). 
Also, it
it is not yet know how to extend these
techniques to deal with some concept constructors that are not
intractable (e.g., \sameas\ on attribute chains).

But probably the biggest issue is that the efficient technology is
relatively recent, and no real KBMS, dealing with large sets of
individuals, has yet been fielded. However, in time this technology
may well take over, and the question of  making it  extensible is
definitely an interesting and important one. (See Section!\ref{related}.)
 }%cmt


All the implemented DL KBMS systems that have had wide distribution
and use, such as \back~\shortcite{back}, \classic~\shortcite{classic}, and \loom~\mycite{loom}, follow a so-called ``normalize-compare'' paradigm, where
most of the reasoning work is performed in an initial
``normalization'' phase, whose goal is to find a normal form for
concepts which explicates implicit facts, eliminates redundancies and
detects incoherencies. Once this is done, when, for example, it
comes to comparing two concepts for subsumption, it is often (but not always) a
matter of comparing only ``structurally similar'' elements -- ones
built with the {\em same} constructor. For example, since the descriptions
\cc{\all(pet,\nothing)} and \cc{\atmost(0,pet)} are equivalent
(subsume each other), in a normal form both would appear, so that
subsumption comparison with \cc{\all(pet,DOG)} would only require
looking at \cc{\all(pet,\nothing)}, while comparison with
\cc{\atmost(3,pet)} would locate \cc{\atmost(0,pet)}.

The present work was carried out over a period of several years within
this ``normalize-compare'' paradigm. The original reasons for this
choice included the following features, which were only available for
this paradigm: having a sizable  user base; supporting
additional KBMS operations, such as least common subsumer, pattern matching,
explanation; reasoning with large knowledge bases of individuals, and
especially doing so incrementally in an environment where one needs the
``logical completion'' of an individual. 

We remark that the tableau technology has recently become competitive
on sizable knowledge bases of concepts.  The promise of provably
complete and effective reasoners for expressive languages is very
enticing, and therefore the study of extensibility in tableaux
approaches \mycite{baader:concrete,franconi} is of great interest.

\section{Concept Reasoning in \protodl} \label{conc-reason}

Our approach to extensible KBMSs is based on the idea that in a case
when the current KBMS does not meet the users' representation and
reasoning needs, one can extend it by adding one or more new
description constructors -- what would be considered logical
connectives.


Although this approach is clearly restrictive, it has the
advantage of being very specific and directed; it allows us to develop
an implementation architecture and accompanying methodology to support
the process of extension. The approach is also supported by empirical
evidence from the use of the \classic\ system in many applications:
the  test-defined concepts of \classic\ have been crucial
in escaping the expressive limitations of the basic language, and each
such test function acts essentially as a new concept
constructor\footnote{ Note however that  reasoning with
test-concepts in \classic\ was minimal: no subsumption
reasoning other than identity checking was performed, and individual
reasoning was limited to recognition.  }.

\subsection{The Modularized Implementation Architecture}
As previously described, the concept reasoning services of our DL-KBMS are
delivered by operations which rely on the \isa\ relationship, to be
computed by the function {\cd{Subsumes?}}.  In our implementation
paradigm, this function takes as arguments two {\em normalized
concepts}. Hence we need some way to take input and convert it into
normalized concepts. This means parsing the concept (function
\cd{Parse}) and normalizing it (function \cd{Normalize}).

Because of the uniform prefix nature of DL syntax, parsing is easily
performed by recursive descent with a single token look-ahead; so 
we associate with every concept constructor \K, a function
\cd{\K::Parse}.

 After examining earlier implementations and applications, a key
decision underlying the \protodl\ implementation is that a normalized concept 
is viewed as the {\em conjunction} of a collection of component
concepts, which are either concept identifiers or are normalized terms
built with concept constructors \K\ other than \cand. Therefore, it is
possible to view a normalized concept as a data abstraction that
encapsulates the way in which the various components are stored and
accessed thru a set of functions \cd{put\_\K(value)} and
\cd{get\_\K()} --- one for each concept constructor \K. For example,
the \cd{put\_\oneof} operation stores a set of individuals \cd{S},
while \cd{get\_\oneof} returns this set\footnote{
The type of a parameter will be
indicated by enclosing it in angle-brackets. Thus, we would have
referred to \cd{put\_\oneof(s: $<$SET(Individual)$>$)}.}.
On the other hand, for the constructor \fills, the (normalized) value
stored is a set of terms of type \cd{\lang Role $\times$ SET(Individual)\rang}, since
for each role, we need to store the set of current fillers.
 For constructors such as \fills, which are associated with a single
role, we overload the \cd{put} and \cd{get} functions so they accept a
separate role argument, allowing us to access each value independently
(e.g., \cd{get\_\fills(p:\lang Role\rang) returns \lang
SET(Individual)\rang}). In fact, for such constructors it is more
efficient to group them by the role identifier, but to simplify the
exposition we shall not pursue this distinction in the rest of this
section.


As mentioned earlier, the ideal normalized concept would have the
property that subsumption could be determined by comparing, using
\cd{\K::Subsumes?},  only
components built with the same constructor. In other words,
\cd{Subsumes?} would have the pseudo-code
\medskip
 \begin{display} \cd{
    Subsumes?(hiNC, lowNC: $<$NormalizedConcept$>$) returns $<$Bool$>$
        ;; structural subsumption
        \{For every \K(T) in getComponents(hiNC) do
	      \{ lowComponent := get\_\K(lowNC);
                 if not \K::Subsumes?(T,lowComponent) 
                    return false; \}
         return true; \}
}  \end{display} 


As we shall see in Section~\ref{dates}, this is  too restrictive however,
so we will  pass as parameter the entire
normalized lower concept, \cd{lowNC}, rather than just the \cd{lowComponent}. 
Therefore, for every constructor \K\ we expect a  function 

\medskip

\fbox{\cd{\K::Subsumes?($<$Normalized\K-term$>$,$<$NormalizedConcept$>$)}}.

\smallskip
\noindent In order to normalize a concept, we will normalize each component
separately, and then combine them. Since a normalized concept
represents a conjunction, the combinator function will be named
\cd{Conjoin}. Here are then the remaining functions that are provided
ahead of time by the core implementation:
\begin{display}\cd{

    \cd{Normalize}(pC : $<$ParsedConcept$>$ )   returns $<$NormalizedConcept$>$
                                           throws \incx;
         {\em /* Start ND to be a data structure having no constraints -- i.e.like \thing */}
           ND := copy of NormalForm\thing; 
      \{ {\em /* Normalize each component and conjoin it onto ND */}
              For every \K(T) in pC do \{
                 T\_norm := \K::Normalize(T); 
                 \K::Conjoin(T\_norm,ND); \}   
         {\em /* Replace  concept ids by  normalized form  (saved by \opc{declare} ) */}
               For every concept identifier N in pC do \{
                  N\_norm := {\rm look up normalized form of} N;
                  Conjoin(N\_norm,ND); \}
              
       {\em /* if any Normalize or  Conjoin detects an incoherence, propagate it up, 
                 since the whole conjunct is incoherent. */}
       \}     catch \incx\ \{ throw \incx \} 
       return ND; 
       
                
    \cd{Conjoin}(fromNC, ontoNC: $<$NormalizedConcept$>$) throws \incx
        {\em /* Take each component of {\em fromNC} and conjoin it to {\em ontoNC};  
           modifies ontoNC. */}
        \{For every  \K(T) in getComponents(fromNC) do
             \{\K::Conjoin( T, ontoNC)
             \} catch \incx \{throw \incx \} 
        \}
}\end{display}

\smallskip

\noindent
Therefore, for every constructor \K, we also expect corresponding
functions \fbox{\cd{\K::Normalize}} and \fbox{\cd{\K::Conjoin}}.
Note that the software architecture treats incoherent concepts (ones
equivalent to \nothing) in a special
manner: whenever they are encountered, a special exception \incx\ is 
raised. Conjunction propagates these exceptions, but other
constructors may trap them and handle them in their own way. For example, 
\cd{\all::Normalize} accepts the restriction
being incoherent, but must ensure that 
\atmost(0) is also added to the normalized concept for the same role.


In retrospect, the above three functions (\cd{Subsumes?, Normalize} and
\cd{Conjoin}) really represent the semantics of the constructor \cand\
(and hence can be appropriately called \cd{\cand::Subsumes?}, etc.) 
%%\cand::Normalize, \cand::Conjoin}), 
as well as the expansion of necessary conditions/definitions for named
concepts (``inheritance''), and parts of the  meaning of the
built-in concepts \nothing\ 
%(since conjunction with it yields the \nothing\ again)
and \thing. 
%(since it is the identity for conjunction). 
To make this more complete, we can add to the beginning of the
%\cd{Subsumes?} function the statement\\
%\rule[-.15in]{0in}{.3in}{\small \cc{if equal(hiNC,NormalForm\thing) or
%equal(lowNC,NormalForm\nothing) then return true;}}
\cd{Subsumes?} function the statement: 
{\small {\tt if equal(hiNC,NormalForm\thing)} {\tt or} 
{\tt equal(lowNC,NormalForm}\-} \nothing {\tt) then return true;}}


  In this sense,  \protodl\  starts from a minimal,
core language specified by the syntax 
\[
 C ::= \thing \vbar \nothing \vbar CN \vbar (\cand\ C_1, \ldots,
C_n)
\]
%  Its rules of inference can be found  in \mycite{axiomatics}. 

\smallskip

\noindent
This is not to say that everyone must start from this minimalist
language, which is hardly useful. But it will have the advantage that
all constructors (even the most useful ones, like \all, \atleast,
etc.) will be implemented as extensions, according to the same uniform
paradigm as the more esoteric extensions. This will be essential if we
are to be able to easily {\em modify} the implementation of standard
constructors (like \all) when called upon to implement non-standard
ones (like dates), which may interact with them.


\subsection{An Overview of the Process of Extension.}\label{overview}
Suppose we want to extend the system at some particular stage with a
new concept constructor. The following is a suggested methodology for
accomplishing this, illustrated with a  familiar concept
constructor, \all.


\myitem{1} {\em Determine a syntax for the extension.}
If concepts will have a LISP-like syntax (as in \classic\ and \loom), the constructor \all\ might  be given the syntax \cc{(:all \
$Role$\ $Concept$)}.
 The terms following the
constructor are called its {\em arguments}, and a version of them will
eventually be stored in the internal representation of our normalized
concepts. One can now implement the function \cd{\all::Parse}, which
in this case would invoke \cd{Role::parse} and \cd{Concept::parse}.

\myitem{2} {\em Determine a semantics for the new concept
constructor.}\\ First, this requires settling on a domain of values
from which its denotation will come. This might be the set of ordinary
objects with unique intrinsic identity 
%(which are interpreted as elements of \domain); 
--- instances of a special  class \anyobject,
which is a built-in direct subclass of \thing. The denotation might
also be some new kind of value (e.g., triples for dates, or lists of
objects), in which case it is necessary to introduce (possibly as a
new concept constructor, which takes no argument) a top class for
these kinds of values (e.g., \anydate\ for dates).

It is now time to clarify the intended meaning of the new constructors.
One alternative, not explored here, is to express the semantics using
First Order Predicate Calculus. Another is to assign a denotation of
values to concepts built with the new constructor.  For \all,
this is just the usual interpretation 
\[
\Int{\all(p,C)}= \set{ d \in
\domain \mid \Int{p}(d) \subseteq \Int{C}}
\]

Rather than move on to implementation right away,  our experience
indicates that it is easier to first describe 
the deductions to be performed in a more concise manner: through rules
of inference. Based on empirical evidence, we see these rules of
inference as being naturally grouped into several
categories\footnote{In each case, we give a general description of
what is desired for a new constructor \K, and then illustrate it with
the specific constructor \all.} 
 \begin{itemize} \item
 %1
{\em Rules dealing with just one constructor, \K. }
\begin{itemize}
 \item {\em Normalizing the arguments of \K }, if these are  themselves
composite objects. 
\[
{\large
\myfrac{  $C \ident D$
}{
$ \all(p,C) \ident \all(p,D)$ }
}\]

 \item
        {\em Reasoning only with concepts of the form \K(args).}
        \begin{itemize}
          \item When is such a concept incoherent {\em by itself}?    
        \[ \all(p,C) {\rm\ is\ never\ incoherent}. \]


          \item When is such a concept equivalent to the entire domain of values?
\[ \all(p,\thing) \ident \anyobject
\]

          \item When does \K(arg1) subsume \K(arg2) in terms of arg1 and
                        arg2? (The so-called  structural subsumption
relationship.) 
\[
{\large
\myfrac{  $C \isa D$
}{
$ \all(p,C) \isa \all(p,D)$}
}\]

        \item When does \K(arg) entail some description built with some
other constructor?
\[ \all(p,\nothing) \ident \atmost(0,p) \]
        \end{itemize}
 \item {\em Reasoning with conjunctions of descriptions built with \K\ 
{\em only}.}
This usually results in a normal-form that either combines the arguments into a single one, or
keeps the arguments as a list, set or multi-set.
\[\cand(\all(p,C),\all(p,D)) \ident \all(p,\ \cand(C,D))
\]
\end{itemize}

%2
\item {\em Rules of inference dealing with combinations of several concept constructors.}
These rules can be grouped into similar families as above, except that they
will involve two or more kinds of constructors.

Since there is no such rule involving \all, we offer an alternative example:
\[
\cand(\atmost(n,p),\atleast(m,p)) \ident \nothing {\em \ \ if \ \ } n \lessthan m
 \]
\end{itemize}

\comment{Obviously, the set of inference rules depends on the set of concept
constructors already existing in the language. Moreover, inference
rules involving more than one kind of constructor belong to 
}
The augmented set of inference rules should be proven sound and
complete with respect to the semantics specified earlier. As with any
logic, soundness is relatively easy to show, but completeness is much
harder. Royer and Quantz propose one approach \mycite{royer} for
generating inference rules that are complete, based on translation to
First Order Logic, but the technique is not easy to apply.

\myitem{3} {\em Extend the implementation.}  This requires first
determining an appropriate normal form for the argument of constructor
\K, declaring a data structure to hold the information, and completing
the \cd{put\_\K} and \cd{get\_\K} procedures to access them from a
normalized concept. For simplicity, we will not address detailed data
structure issues here; instead, we use a simple notation based on
terms in the style of Prolog to represent data structures.  In the case of \all, the
representation is just a pair
\cd{\all($<$Role$>$,$<$NormalizedConcept$>$)}. We note that if we
wanted to keep track of the original form of the concept (so it can be
printed out to users as entered), this could be added as an extra
field of the data structure. We emphasize that the normalized form of
the description (e.g., a finite automaton) might not even resemble the
original syntax (e.g., a regular expression), though in our examples
this will not be the case.


Next, we need to implement the three procedures:
{\cd{\K::Normalize}},{\cd{\K::Conjoin}}, and {\cd{\K::Sub\-sumes?}}, whose
invocation is orchestrated by the corresponding functions for the
\cand\ constructor.


By analyzing the normalization algorithms for numerous
constructors, we have arrived at a more refined understanding of the
{\em prototypical} 
\cd{\K::Conjoin} procedure. This is presented in the Appendix A as 
 Figure~\ref{conj}, and uses  the following other, smaller functions


\fbox{\cd{\K::Universal?}},
\fbox{\cd{\K::Incoherent?}},
\fbox{\cd{\K::SubsumesSame?}}, 
\fbox{\cd{\K::ConjoinToSame}},

\fbox{\cd{\K::IncoherentWDifferent?}}, 
\fbox{\cd{\K::Subsumes\-Different?}}, 
\fbox{\cd{\K::Conjoin\-ToDifferent}},

\fbox{\cd{\K::FindOtherImplications}}.

\noindent These functions correspond to the
categories of inference rules we have mentioned above. 
When this decomposition can be applied, it provides 
two advantages: improved chances of correct implementation by making
smaller, specialized modules; and independent reuse, as in

\smallskip

{\samepage
\begin{display}\cd{
   \K::Subsumes?(T:$<$Normalized\K-Term$>$, lower:$<$NormalizedConcept$>$)
                                                      returns $<$Bool$>$
	  \{if not \hilite{\K::SubsumesSame?}(T,get\_\K(lower)) then return false;
	   if not \hilite{\K::SubsumesDifferent?}(T,lower) then return false;
	   return true; \}
}\end{display}
}

Of course, if a specific constructor does not need to implement some of these
sub-procedures, the corresponding lines from the generic implementations are
omitted, in order to avoid the cost of useless function invocations.

\medskip

{\sloppy
For our simple example, when \K=\all,
\cd{\all::Normalize(\all(role,vr))} returns
\cd{\all(role,} \cd{\cand::Normalize(vr))}.

If the only other constructor is \atmost, 
 the following functions used by \cd{\all:Conjoin} and
\cd{\all::Subsumes?} are needed:
\begin{itemize}
\item \cd{\K::Universal?(T)}: {\it Is \cc{T} equivalent to the
top of the hierarchy for that set of values?}\\
\cd{\all::Universal?(\all(role,vr))} returns true when \cd{vr} is
\cd{NormalForm\thing}. 

\item \cd{\K::SubsumesSame?(T,OldTs)}: {\it Is \cc{T}  implied by
the  \K-constructed terms already seen in oldTs?} 
This is basically the ``structural subsumption'' algorithm.\\
 \cd{\all::SubsumesSame?(\all(role,vr1),\all(role,vr2))} would
return true iff\\ \cd{\cand::Subsumes?(vr1,vr2)} returns true.

\item \cd{\K::ConjoinToSame(T,OldTs)}: {\it  Merge \cc{T} with any preceding
terms built with \K.} \\
\cd{\all::ConjoinToSame(\all(role,vr1),\all(role,vr2))} returns\\
\cd{\all(role,\cand::Conjoin(vr1,vr2))}.

\item \cd{\K::FindOtherImplications(T,This,ImplicationsToDoList)}:
{\it If any additional  constructors have to be added
because of \K, put them onto the \cd{ImplicationsToDoList}. }\\
\cd{\all::FindOtherImplications} adds to \cd{ImplicationsToDoList} the
description\\ \cd{\atmost(0,role)} if its first argument is
\cd{\all(role,\nothing)}. 
\end{itemize}
}
Once the \cd{Conjoin, Normalize} and \cd{Subsumes?} functions are
implemented for the new constructor \K, the corresponding functions
for \cand\ need to have lines added to invoke them according to the
pattern presented in the preceding section (unless the programming
language is highly polymorphic).

Next, we use reasoning about dates, an extension desired in some
\classic\ applications, to give a more complex example of the 
methodology for building extensions of \protodl.


\subsection{Dates: An Example Concept-Level Extension}\label{dates}
We imagine an application where there will be individual dates as
values of attributes or even roles, and that concepts will describe
collections of dates, specified in various ways (e.g., as ranges or periods).


To begin with, it is important to clarify what the {\em individuals}
look like about which information will be kept.  In the case of dates,
we know that we wish to treat them as temporal points, which have
associated information about the year, month and day when that date
occurs.
 Given a date $d$, the above components will be referred to 
as year($d$), month($d$), day($d$).  
 There are two different ways of thinking of a date: as  an abstract
mathematical value (e.g., a triple of integers) or as an
individual object with  attributes for \cc{year, month,
day.} The last approach has the disadvantage that we need to develop a
separate theory of identity for dates (two dates are supposed to be
identical if they have the same components), although it has the
advantage of allowing incomplete information about the exact
occurrence of a time point. Since this feature is not desired, we will
adopt the first approach, for convenience writing
date individuals as 1996/7/25.  In addition, we will have the usual
total (reflexive) order \dlt\ on dates,
as well as two special date constants, \begintime\ and \endtime, such
that \begintime \dlt\ $d$ \dlt\ \endtime\ for all dates $d$.


We are now ready to introduce concept-forming operators for dates
which are useful for our application.  First, when introducing a new
{\em kind} of value, it is useful to define a top concept, which will
contain all such values. In our case, let us call it {\anydate}.

 One obvious  grouping of dates is by ranges:
``between June 1st and August 31, 1996''. We might thus propose a
concept constructor
{\drng}, which takes as argument a pair of dates, denoting the ends of the
range, e.g., \cc{\drng(1996/6/1,1996/8/31)}. But since the base language
does not support disjunction, and we want to allow descriptions such as ``the
summers of 1995 and 1996'', we will in fact have \drng\ take as argument a
set of date pairs, as in
\cc{\drng(\listset{(1995/6/1,1995/8/31) , (1996/6/1,1996/8/31)})}.

\medskip

Having established the syntax of the concept constructors, and
then implemented \cd{{\tt\bf date\-Range}::}\-\cc{Parse}, we present its
denotational semantics:
\[
\Int{\drng(SD)} = \set{d \mid \exists b,e. (b,e)\in SD\ such\ that\
        b\dlt\ d\dlt e}
\]


Next, we look for inference rules describing the desired reasoning for 
 \drng. Following the heuristics in Section~\ref{overview}, we come up
with Table~\ref{dateRules}.

To implement the inferences for \drng, we must find a normal form and write
functions \cd{\drng::Normalize, \drng::Conjoin} and
\cd{\drng::Subsumes?}, or their components.

\begin{table}[hbt]
\begin{center}
{\small
\begin{tabular}{|l|c|}
\hline

\shortkind{Universal} \rule{0in}{.2in} &
{ %\fbox{
\drng(\listset{(\begintime,\endtime)}) \issame\ \anydate 
}
 \\[.12in]  \hline 


\shortkind{Incoherent}   \rule{0in}{.2in} &
{ %\fbox{
\drng(\listset{}) \issame\ \nothing 
}
\\[.12in]  \hline

\shortkind{Subsumption}  \rule{0in}{.3in}&
{ %\fbox{
\myfrac{
b1 \dlt b2 \dlt e2 \dlt e1
}{
\drng(\listset{(b2,e2)}) \isa \drng(\listset{(b1,e1)}) 
}
}
\\[0.2in]  
  %nothing here
 &
{ %\fbox{
\myfrac{
 \breakit{
	\drng($\alpha 1$ ) \isa \drng($\alpha 2$) \\
	 \drng($\beta 1$) \isa \drng($\beta 2$ )
 }
}{
\drng($\alpha 1 \cup \beta 1$) \isa \drng($\alpha 2 \cup \beta 2$) 
}
}
\\[0.2in]  \hline
\shortkind{Conjunction}  \rule{0in}{.3in}&
{ %\fbox{
\breakit{
	\cand(\drng(\listset{(b2,e2)}), \drng(\listset{(b1,e1)})) \issame\\
	\drng(\listset{ ($max$(b1,b2),$min$(e1,e2))})
}
}
\\[0.2in]
  &

\myfrac{
 \breakit{
   \cand(\drng($\alpha$),\drng($\beta 1$)) \issame \drng($\gamma 1$)
\\    \cand(\drng($\alpha$),\drng($\beta 2$)) \issame \drng($\gamma 2$)
  }
}{
 \cand( \drng($\alpha$),\ \drng($\beta 1 \cup \beta 2$)) 
 \issame\ \drng($\gamma 1 \cup \gamma 2$)
}
\\[0.2in]   \hline 
\shortkind{Normalize}  \rule{0in}{.3in}&
{ %\fbox{
\myfrac{e \dlt (b + 1 day)
}{\drng(\listset{(b,e),$\alpha$}) \ident \drng(\listset{$\alpha$})
}
}
\\[0.2in]
 &
{ % \fbox{  
\myfrac{
b1 \dlt  b2 \dlt (e1\ +\ 1\ day) \dlt e2
}{
\drng(\listset{(b1,e1),(b2,e2)}) \issame 
 \drng(\listset{(b1,e2)})
}
}
\\[0.2in] \hline
\end{tabular}
}
\end{center}

\caption{Inference rules for \drng.}\label{dateRules}
\end{table}


It is useful to determine first the structural subsumption function,
\cd{\drng::\-Subsumes\-Same?}, since this drives the requirements for
the others.  In our case, the obvious representation works fine: a
date is some data structure, such as a list of three values or a record
with three fields; a single date-pair is a list of two values or a
record with two fields; and the set of date-pairs making up the
disjunction is just a list of date-pairs. It is best to encapsulate
the above implementation choices using abstract data types for
\cd{Date, DatePair} and \cd{DateRange}, with appropriate accessor
functions and constructors. We must also extend the representation
of normalized concepts to implement \cd{put\_\drng} and \cd{get\_\drng}.


Returning to \cd{\drng::\-Subsumes\-Same?}, this function now simply
implements the subsumption inference rules above
% (which are essentially structural subsumption rules)

\medskip

\begin{display}\cd{
\drng::SubsumesSame?(high,low : $<$SET(Date$\times$Date)$>$ ): returns $<$Bool$>$
       \{for every (b,e) in low
          find (b',e') in high such that b'\dlt b\dlt e\dlt e';
       \}
}\end{display} 

\medskip

\cd{\drng::Normalize} verifies (if not already done so) that the dates
b and e in each pair (b,e) are valid according to our usual calendar,
and that b\dlt e. Any pairs not satisfying these conditions are
eliminated. It also needs to merge overlapping or adjacent intervals
into maximally long ones, since otherwise  the above  subsumption algorithm will not
recognize that \cc{\drng(\listset{(1996/1/2,1996/1/4),
(1996/1/5,1996/1/6)})} subsumes 
\cc{\drng(\listset{1996/1/2, 1996/1/6})}.

The function \cd{\drng::Conjoin} has the standard implementation (see
Appendix A), but only 
 functions \cd{\drng::\-Universal?},
\cd{\drng::\-Inco\-herent?}, 
\cd{\drng\- ::\-Conjoin}\-\cd{To\-Same} and \cd{\drng::\-Subsumes\-Same?} need to be implemented,
 performing exactly the actions specified by the rules of inference.


\medskip

Consider now adding another concept constructor for dates, to help
represent {\em periodic} time, such as ``every summer'' or ``every
Christmas''. A single period is just a range constraint on the
possible values for the components of a date, other than
\cc{year}. So, ``summer days'' would be represented by [(6 . 8) (1
. 31)], while ``Christmas'' would be [(12 . 12) (25 . 25)].  For the
sake of brevity, this new \fbox{\prd}\ constructor will take as argument
only a single period (rather than a set of them, interpreted
disjunctively) and we will only sketch the implementation
extensions. Also not presented here, is a very useful extension to
periods allowing constraints on the days of the week, such as ``every
Saturday to Sunday'', or even ``every 3rd Sunday''.


The denotation of \prd\ terms is also quite simple:
\[
\Int{\prd([(m1 . m2) (d1 . d2)])} = \{e \mid m1 \leq month(e) \leq
m2,\ d1 \leq day(e) \leq d2 \}
\]

The rules of inference for reasoning about \prd\ concepts alone,
presented in Table~\ref{periodRules} are also
straightforward.
\begin{table}
\begin{center}
{\small
\begin{tabular}{|l|c|}
\hline
\shortkind{Universal}  \rule{0in}{.2in} & \prd([(1 . 12)\ (1 . 31)]) \issame \anydate
\\[0.2in] \hline 

\shortkind{Incoherent}  \rule{0in}{.3in}&
\myfrac{ {\em not}( bm \mbox{$\leq$} em {\em\  and\  }bd \mbox{$\leq$}
ed )
}{
\prd([(bm.em)\ (bd.ed)]) \issame \nothing
} 
\\[0.2in] \hline 
\shortkind{Subsumption}  \rule{0in}{.3in}&
\myfrac{
 bm1 $\leq$ bm2 $\leq$ em2 $\leq$ em1 {\em \  and \
 \ }bd1 $\leq$ bd2 $\leq$ ed2 $\leq$ ed1
}{
\prd([(bm2.em2)(bd2.ed2)]) \isa \prd([(bm1.em1)(bd1.ed1)]) 
}
\\[0.2in] \hline 
\shortkind{Conjunction}  \rule{0in}{.3in}&
\cbreakit{
\cand(\prd([(bm1.em1)(bd1.ed1)]), 
\ \ \ \prd([(bm2.em2)(bd2.ed2)])) \\
\issame \\
\breakit{
\prd([($max$(bm1,bm2)\ .\ $min$(em1,em2))\ \\
\ \ \ \ \ \  ($max$(bd1,bd2)\ .\ $min$(ed1,ed2))])
}} 
\\[0.2in] \hline 
\end{tabular}
}
\end{center}
\caption{Inference rules for \prd.}\label{periodRules}
\end{table}
The implementation of most functions follows immediately from the rules of
inference.
\comment{
 \cd{\prd::SubsumesSame?} is simply the check of the
range bounds; \cd{\prd::Normalize} just invokes macros for
\cd{\prd::Universal?}
and \cd{\prd::Incoherent?}, which check the appropriate conditions specified by
the rules of inference; and \cd{\prd::ConjoinToSame} is also obvious from
the final rule of inference.
}%cmt

The interesting reasoning  involves the conjunction of ranges with
periods. These rules, appearing in Figure~\ref{prd:rng:rules},
can be expressed most succinctly by showing how certain
periods are either eliminated or retained unchanged, and then relying on 
the \drng\ normalization rule, 
applied {\em in reverse}, to cut up a range into appropriate strips.
\begin{table}
\begin{center}
{\small \begin{tabular}{|c|}
\hline
\,    \rule{0in}{.4in}
\cbreakit{
$\cand(\drng(\alpha \cup \beta), \prd(\delta)) $
\\
\issame \\
$\cand(\cand(\drng(\alpha),\prd(\delta)),\
\cand(\drng(\beta),\prd(\delta)))$  } 
\\[0.2in] \hline
\  \rule{0in}{.5in}
 \myfractwo{
  \breakit{
bm $\leq$ month(dt1) = month(dt2) $\leq$ em \ {\em and} \\
bd $\leq$ day(dt1) $\leq$  day(dt2) $\leq$ ed 
  }
}{
 \cbreakit{
\cand(\ \drng(\set{(dt1,dt2)})\ , \ \prd([(bm.em),(bd.ed)]) ) \\
\issame\ \\
 \drng(\set{(dt1,dt2)}) 
}
}
\\[0.2in] \hline
\  \rule{0in}{.45in}
\myfrac{
 \breakit{
month(dt1)=month(dt2) {\em \ and} \\ 
{\em not\ } (bm $\leq$ month(dt1) $\leq$ em \ {\em and\ } \
bd $\leq$ day(dt1) $\leq$ day(dt2) $\leq$ ed )
}
}{
\cand(\ \drng(\{(dt1,dt2)\})\ , \  \prd([(bm.em),(bd.ed)]) ) \issame\ \nothing
}
\\[0.2in]  \hline
 \end{tabular}
}\end{center}
\caption{Inference rules for conjoining \prd\ and \drng.}\label{prd:rng:rules}
\end{table}
These inference rules imply that we need to also implement 
\cd{\prd::ConjoinToDifferent} \cd{(p:$<$Period$>$,} \cd{other:$<$NormalizedConcept$>$)},
 which basically uses the period as a ``cookie cutter'' to create the
sub-interval ranges that satisfy the period's restriction.  Of
course, this will be done procedurally in a manner more efficient than
suggested by the rules of inference.  Moreover, we must now revisit
the implementation of \drng, to put in a similar
\cd{\drng::ConjoinToDifferent} function, since  a
concept with a range may be conjoined onto one that already has a
period in it.


Finally, in the presence of both \drng\ and \prd\ constructors, structural
subsumption is not enough, since we want \cc{\prd([(4 . 4) (1 . 31)])} to subsume 
\cc{\drng((1988/4/1, 1988/4/21))}, but not \cc{\drng((1990/4/1, 1992/4/1))},
and there is no finite normal form which would list all the ranges satisfying a period. So
we need to also write the function
 \cd{\prd::}\-\cc{Subsumes}\- \cc{Different?(p:$<$Period$>$,
lower:$<$Norma\-lized\-Concept$>$)}, which checks every interval \cd{(b,e)} in
\cd{get\_\drng(lower)} to make sure that \cd{year(b)=year(e)} and that
the month and day meet the conditions of the period.

\comment{
But suppose we have an interval which is semi-infinite, because one of its
end points is the constant \begintime\ or \endtime. Then we have a problem
with D1 \issame \cand( \drng((\begintime,1996/6/2))\ , \ 
\prd([(4 . 4) (1 . 31)]))
 since this is supposed to subsume \drng((88/4/1 , 88/4/21)), but not
\drng((90/4/1 , 92/4/1)). This is one example where the normalization
algorithm itself cannot find the desired normal form a priori, and we must
have the 
function, to verify that each interval in r satisfies the period restriction.
}%cmt


An interesting complication arises because dates are discrete, and
hence one can count the number of dates in a \drng. If \drng\
can  appear as the value restriction of general roles, as in
\cc{\all(freeForMeeting,} \cc{\drng(\listset{(1995/6/1,1996/6/5)}))}
attributes, there is no problem. Otherwise, we can however infer
cardinality constraints on the number of fillers: 
\cc{\drng(\listset{(1995/6/1,1996/6/5)})} allows only 5 different values.
In a language that supports constructor \atmost, we would therefore
have to conclude \cc{\atmost(5,freeForMeeting)}. The implementation
achieves this by  introducing a helper function
\cd{\drng::countDays}, which can be applied to a normalized \drng\
object; then, function
\cd{\all::FindOtherImplications} needs to be modified, so that it
invokes \cd{\drng::countDays} on its 
value restriction if it is of date type,
and a  normalized \atmost\ restriction is posted for that role
 on the \cd{ImplicationsToDoList}. Later processing of that list
will remove the \atmost\ constraint and
conjoin it onto the concept.
% Similar actions need to be taken in \cd{\all::Normalize}.

\subsection{Experience with Extensions}\label{experience}
As part of the development of the above architecture, we have
considered extending the original core with the constructors  of
\classic\ (\all, \atleast, \atmost, \fills, \oneof, integer ranges),
as well as  primitive concept negation, and the negation of \fills.
In these cases we have reproduced the inferences of \classic\, and
almost exactly the internal actions of the \classic\ implementation;
i.e., we perform only a few more checks despite the fact that our
implementation is made up of ``standard'' modules for each
constructor.


Two kinds of concept constructors seem difficult to add to a
normalize-compare algorithm in a way that preserves completeness of
reasoning {\em and} the architecture of the system. Disjunction  would
most naturally be handled if there was a disjunctive normal form,
where each disjunct is purely conjunctive. This is difficult to
achieve with nested disjunctions (inside \all\ restrictions say). Note
that we had no problem with the one-level disjunction in
\drng.

A second kind of construct that is difficult to add  efficiently
and completely is \sameas. The reason here is that \sameas\ interacts
with \all\ in a way that generates a potentially infinite number of
\all\ restrictions; therefore, the implementation of \sameas\ is best
combined with that of \all, resulting in a non-tree data structure \mycite{jair}. A
speculative way to preserve structural subsumption might be to allow
\all\ to apply to chains of a attributes represented by regular
expressions. (In general, the complications of implementing \sameas\
are the reason it does not appear in C-\classic\ and {\sc
neo-classic}.)

Finally, as mentioned earlier, we do not currently cover role
constructors and 
recursive concept constraints. Furthermore,
constructors that require entirely new deductive mechanism (e.g.,
epistemic reasoning, defaults, forward-chaining rules) will also have difficulty being integrated
properly into this framework. 

On the positive side, we have considered  extensions
supporting  strings  \cite{borgida:dl96},
 and most elaborately, a
reconstruction of the {\sc clasp} reasoner about actions and plans \mycite{borgida:kr92}. To summarize this ``success'' briefly, {\sc
clasp} \mycite{clasp} was a system built on top of \classic\ for
reasoning about actions (which were represented in propositional
STRIPS-style, having concepts for pre- and post-conditions, as well as
add and delete lists);  plans were represented by regular
expressions of actions, as illustrated below.
\comment{, and plan instances
(called scenarios) were sequences of action instances.}
Our goal was to apply the \protodl\ approach to 
{\clasp}, hoping to be 
able to reproduce the original, custom-made implementation discussed
by Devanbu and Litman \mycite{clasp}.  First, we introduced a concept
constructor for actions, \cc{\act($PreC,PostC,AddC,DeleteC$)}, with the
expected logical properties expressed as rules of inference in the
various categories (e.g., if $PreC$ was incoherent, then the
action was also incoherent).  The implementation then followed
immediately.

The more interesting problem was dealing with plans. The constructors
\sing, \seq, \sloop, and \alt\ can be used to build complex plans from
actions, as in  {\seq( \sing(\cc{DIAL}), \sloop(\sing(\cc{RING})))}.
These
plans denote {\em sequences of action instances} (e.g., in the above
example, a dialing action followed by any number of rings). Although
we provided rules of inference for plans too, it turns out that
there is no normal form for regular expressions! Instead, in the
implementation, \cd{Normalize} for \seq, \alt\ and \sloop\ built a
non-deterministic finite automaton, which then had to be made
deterministic, and in which certain chains of arcs had to be removed
(if the post-condition of the action on the incoming edge was
inconsistent with the pre-condition of the action on the outgoing
edge). Moreover, the containment algorithm for these finite automata
had to take into account the fact that actions on transitions (e.g.,
\cc{MOVE}) may represent generalizations of others (e.g.,
\cc{MOVE-FAST}). This implementation was achieved in \protodl\ by introducing a
``hidden'' concept constructor, \topexp, which enclosed the top plan.
It was then \cd{\topexp::Normalize} that made the automaton
deterministic and removed some transitions, and
\cd{\topexp::Subsumes?} that implemented the special subsumption
algorithm. Moreover, the requirement to implement
\cd{\topexp::Conjoin}, which was not present in  the original \clasp\
system, made
us realize that without this, {\sc clasp} plans could
not appear in other  concepts,
because expressions like \cc{\cand(\all(p,PLAN1), \all(p,PLAN2))}
could not be normalized.  As a result we believe we reconstructed and
improved the original {\sc clasp} proposal,
by characterizing  the inferences performed through
rules of inference, and by allowing plans to be first-class values,
which could appear in ordinary roles.


\subsection{Relationship to ``Concrete Domain'' Extensions}\label{concrete}

Although we shall address general work on extensible KR\&R in the
conclusion, there is one specific approach involving description
logics that deserves closer scrutiny at this stage, while the details
of the present work are still fresh.


Baader and Hanschke's proposal \mycite{baader:concrete} for extending DLs with
``concrete domains'' allows concepts to consist of arbitrary
predicates involving values from some domain other than ordinary
objects (i.e., other than elements of \domain), as long as these
values are fillers of {\em attributes} of ordinary
objects. For example, suppose the concrete domain is that of dates; as
above, we have predicates like $BEFORE$, corresponding to \dlt; then,
if we had two date-valued attributes \cc{arrival} and \cc{departure},
we could define the concept \cc{BEFORE(arrival,departure)}, denoting
ordinary objects (not sets of dates!)  whose attributes have
appropriately related date values.

In order to keep reasoning decidable, this mechanism requires the
concrete domain to be {\em ``admissible''}: (i) there must be a
predicate denoting the universe of all values in that concrete domain;
(ii) the set of predicates must be closed under negation; and (iii) it
must be possible to decide the satisfiability of any finite
conjunction of such predicates.  It is interesting to note that these
requirements match in part our heuristics for new concept
constructors: we also argued for the need to add a top concept to the
hierarchy of new values (and its negation, the bottom of this
hierarchy), and for the need to be able to compute the conjunction of
descriptions.

The admissibility of a concrete domain ensures that the \protodl\
approach can implement any such extension as follows: Syntactically, a
domain corresponds to a concept constructor. Therefore, a concept like
\cc{BEFORE(arrival,departure)} in the domain \DD, would be represented
in \protodl\ as \DD\cc{('BEFORE',arrival,departure)}. Then, the
necessary \protodl\ functions are programmed as follows:
\cd{\DD::Normalize} tests that the predication is satisfiable
(otherwise signaling \incx), and creates a singleton list containing
the predication; \cd{\DD::Conjoin} concatenates the list of
predications of its arguments, checking for the consistency of their
conjunction; \cd{\DD::Subsumes?(C,D)} creates the conjunction of all
the predicates in \cc{C}, and their negation in \cd{D}, and returns
true if the result is unsatisfiable.

Conversely, Baader and Hanschke's approach could well be applied to date ranges,
since these are essentially closed under negation. And since it is
offered in the context of the tableau theorem-proving technique
mentioned in Section~\ref{implem}, this continues to have the advantages
of elegance and complete reasoning, as long as the concrete domain
reasoner is proven complete. In our case, the entire system would have
to be proven complete.

We believe though that \protodl\ is somewhat more general, since it
allows concrete domains to be value of roles, not just attributes
(see our earlier discussion of dates as values of roles). Also, there
is some advantage to being able to deal with non-admissible
domains in cases when negation is not absolutely needed, but
its addition would cause an increase in computational complexity; for
example,
adding negation/complement to regular expressions makes the
containment problem non-elementary \mycite{stockmeyer}.

\section{Processing of Individuals in DLs: An Introduction }\label{ind-reason}
Concept descriptions, as introduced above, are intensional objects,
suited for capturing generic information about a domain, such as the
ontology of terms. DL-KBMSs must also manage extensional/factual
information about  individual objects --- the so-called A-box\footnote{
The most thorough theoretical investigation of individual reasoning
has been presented in Andrea Schaerf's PhD thesis and derived publications
\mycite{schaerf-ind}. We note however that for some of the most
expressive DLs proposed recently, individual reasoning has not yet been addressed.}.

\subsection{Inferences Involving Individuals}
 Normally, one can assert information such as the
fact that some object \cc{Anni} is known to be an instance of a concept \cc{CHILD}
(written as \cc{Anni:CHILD}), or that it has some other object,
\cc{Lego} as a filler for its \cc{hasToys} role (written as \cc{(Anni,Lego):hasToys}).  Based on this information,
the KBMS can deduce information about the individual's membership in
other descriptions (written using \isin); for example, in this case we
know \cc{Anni \isin \atleast(1,hasToys)}. Because DL-KBMS usually do
not make the closed-world assumption, it is also necessary to record
when some set of fillers is complete for  an individual's role. This is
done using an (auto-epistemic) assertion like\\
\cc{\closed{Anni}{hasToys}{\{Lego,Barbie\}}}. As a result of such
an assertion, we can then deduce that \cc{Anni \isin
\atmost(2,hasToys)}. (Note that we 
have distinguished the  three kinds of {\em assertions} in ${\cal A}$,
namely $b:C, (b,e):p, \closed{b}{p}{S}$,  from the
corresponding judgements that can be deduced in the logic:
 $b \isin C$, \hasfiller{b}{p}{e}, \hasclosed{b}{p}{S}.)

Information about fillers and roles being closed (i.e., all
fillers being known) can also be deduced, as in the case of 
the KB that contains
\calig{A}=\{\cc{Lori:\all(hasToys,\oneof(Lego45)),
Lori:\atleast(1, hasToys)}\}, from which we can conclude
that \cc{Lego45} is a toy owned by Lori (written as
\hasfiller{\cc{Lori}}{\cc{hasToys}}{\cc{Lego45}}) and that the complete set of 
fillers for \cc{hasToys} is \cc{\set{Lego45}} (written
as \hasclosed{\cc{Lori}}{\cc{hasToys}}{\set{\cc{Lego45}}}).
  We note that an elegant formalization of these
notions has been obtained by adding an epistemic modal constructor {\bf
K} to DLs \shortcite{epistemic}. This constructor has a number of other
uses, but to shorten the presentation we have not introduced it here
explicitly. 

Formally, we define a knowledge base KB to be a concept
knowledge base CKB, extended with a set
\calig{A} of {\em assertions} of the form $b:C$, $(b,e):p$ and
$\closed{b}{p}{S}$, where $S$ is some set of individuals.
An interpretation \I\ is said to be a model for $b:C$ if
$\Int{b} \in \Int{C}$, a model for $(b,e):p$ if $\Int{e} \in
\Int{p}(\Int{b})$, and a model for 
$\closed{b}{p}{S}$ if ($\Int{e} \in \Int{p}(\Int{b}) \ \iff\ e
\in S$)\footnote{As usual, we make the unique-name assumption, and in
fact include named individuals in the domain}.

{\sloppy
The judgment $\kbent b \isin C$ holds iff for every model \I\ of
KB, $\Int{b}\in\Int{C}$; the judgement 
$\kbent \hasfiller{b}{p}{e}$ holds iff for every model \I\ of KB,
	$(\Int{b},\Int{e}) \in\Int{p}$;  finally,
$\kbent \hasclosed{b}{p}{S}$ holds iff $\kbent \hasfiller{b}{p}{b_i}$ for every
$b_i\in S$, and for every other individual $e$ not in $S$, there is
some interpretation \I\ of KB such that 
 $\not\kbent \hasfiller{b}{p}{e}$
}.
Because our concept language may not have negation, and because we
have the open world assumption, we also need to be able to talk about
non-membership in a concept: $b \notisin C$; naturally,
$\kbent b \notisin C$ iff for some model   \I\ of KB,
$\Int{b}\not\in\Int{C}$. 
As usual, a KB will be called {\em inconsistent} iff it has no models.


The specification of reasoning about individuals can again be
represented by inference rules \mycite{axiomatics}. For example, for
the constructor \all, we proffer the following three rules of
inference, which describe the ``structural membership/non-membership''
rules, as well as a kind of inference called ``propagation'', where
information about some individual $b$ results in new information being
deduced about {\em another} individual $e$:\\
\begin{displaymath}\begin{array}{c}
\myfrac{
 \kbee \hasclosed{b}{p}{S} \ \ \ \ \kbee $b_i$ \isin C
}{
\kbee b \isin \all(p,C)
}
\;\; S=\{b_1,\cdots,b_n\}, \ n\geq 0
\\[0.2in]
\myfrac{
\kbee \hasfiller{b}{p}{e} \ \ \ \ \kbee e \notisin C
}{
\kbee b \notisin \all(p,C)
}
\\[0.2in]
\myfrac{
\kbee b \isin \all(p,C) \ \ \ \ \kbee \hasfiller{b}{p}{e}
}{
\kbee e \isin C
}
\end{array} \end{displaymath}

Note that for an inconsistent KB, we can have $\kbee b \isin
\nothing$, or  we can deduce information from fillers (e.g.,
\kbee b \isin \cc{\atleast(3,pets)}) that contradicts information
asserted or deduced from descriptors (e.g., \kbee b \isin
\cc{\atmost(2,pets)}).

 
\subsection{DL-KBMS Operations on Individuals}\label{ind-kbms}
 The point of living with the open-world assumption is to allow
information to be accumulated incrementally, as in the case of
designing some artifact (one of the most successful applications of
\classic).

From the functional point of view, the DL-KBMS  therefore supports the
following update operations for incrementally adding information
about individuals:\\

\smallskip
\begin{tabular}{|ll|}
\hline
Operation & Effect
\\ \hline
\hline
%\opc{create-individual}($b$)
% & $b$ is added to 
%\\ \hline
\opc{assert-member}($b,C$)
 & $b:C$ is added to \calig{A}
\\ \hline
\opc{assert-fills}($b,p,b_1$)
 & $(b,b_1):p$ is added to \calig{A}
\\ \hline
\opc{assert-closed}($b,p$)
 & \breakit{\closed{b}{p}{S} is added to \calig{A}, where $S$ is
\\ the set of individuals returned in the current KB by the
\\ operation \opc{ask-for-fillers}($b,p$), defined below.}
\\ \hline
\end{tabular}

\medskip
If as a result of the update, the KB is inconsistent, then the update
is rejected and the state of the KB is supposed to remain unchanged.

At any point, the KBMS is able to respond to inquiry operations
about relationships involving individuals:\\

\smallskip
\begin{tabular}{|lll|}
\hline
Question  & Answer type &Response
\\
\hline
\hline
\opc{ask-member?}($b,C$)
 & Boolean
 & true iff $\kbent b \isin C$
\\ \hline
\opc{ask-non-member?}($b,C$)
 & Boolean
 & true iff $\kbent b \notisin C$
\\ \hline
\opc{ask-for-fillers}($b,p$)
 & SET(Individual)
 & \set{$e \mid \kbent \hasfiller{b}{p}{e}$}
\\ \hline
\opc{ask-closed?}($b,p$)
 & Boolean
 & \breakit{ true iff   for some set $S$
	\\ $\kbent \hasclosed{b}{p}{S}$}
\\ \hline
\end{tabular}

\medskip

As with concepts, many DL-KBMS pre-compute the $b \isin C$ judgment,
for all individual and concept names, by finding the most specific
named descriptions to which the individual $b$ provably belongs. Similarly,
the DL-KBMS pre-computes and caches the fillers and closed information for each
individual's roles. This is done in order to  detect inconsistencies
at the time of the update,  to decrease the amortized cost in 
case  queries are much more frequent than updates, and to support
queries of the form ``What additional information can you deduce about
$v$?''. The utility of such queries has been shown, among others, in
applications involving information discovery in software development
\mycite{prem:thesis}.


\section{Individuals in \protodl}\label{indkb}

Reasoning about individuals 
The goal of our implementation is to support efficiently the update
operations, {\em which are incremental}, so that most of the inferences
are precomputed: for each individual, we know the least classes it is
an instance of, all the fillers it can have for each role, and whether
the role is closed or not for that individual. The architecture below
describes an extension and rationalization of the individual
processing that is usually carried out in normalize-compare DL-KBMS
such as \classic. The novelty will be the systematic separation of the
interaction between various kinds of updates and various kinds of
inferences, and the concomitant use of truth-maintenance links.

\subsection{The Basic Architecture of Individual Reasoning}
In some systems, one can try to reduce individual reasoning to concept
reasoning by associating some single, maximally complete description
with each individual. However, this is not always possible, as shown
by Schaerf \mycite{schaerf-ind}.

Instead, our data structure for every individual includes both a
concept description (to be called \descr), which may be an existing
class or an unnamed complex description, and {\em individual
role-filler information} recording the specific values assigned so
far, and whether the role is closed or not. (This information is
accessed with built-in functions
\cd{add\_filler}, \cd{put\_closed}, \cd{get\_fillers} and
\cd{is\_closed?}.)


In processing an update about some individual $b$, we must therefore
 resort to two kinds of reasoning: (i) subsumption/incoherence
 reasoning involving only the description \descr($b$) and other concepts;
 (ii) reasoning specific to the individual and especially its role
 fillers. 

The former kind of reasoning is motivated by general inference rules
connecting membership and subsumption (e.g., if $b\isin C$ and $C\Isa D$
then $b\isin D$). Since subsumption and its extensibility has
 been described in the preceding section,
 henceforth we concentrate on the second aspect of individual reasoning.
\comment{ A crucial
 property of individual processing that needs to be remembered is is
 that {\em the acquisition of information about individuals is assumed
 to be \underline{incremental}}: in contrast to the definition of a
 concept, which is stable (i.e., cannot be modified), one can
 frequently add new information about an individual, since the open
 world assumption holds unless explicitly removed by role closing. }

To understand the tasks involved, let us illustrate what kinds of
reasoning need to be performed whenever any fact is asserted (or
inferred) about an individual $b$ 
\begin{itemize}
\item {\em The KB may become inconsistent}, because of a
conflict between the individual descriptor and the filler information
either on $b$ or some other individual.  For example, more fillers
might be added to a role than permitted by an \atmost\
restriction. This requires  the entire update to be rejected. Note
that an update may result in several individuals with inconsistent
information on them. The system is only required to detect one of
them, before rejecting the update.

\item {\em The individual $b$ may end up being re-classified.}
 In a monotonic system,
such as the present one, this means that the individual may now belong
to some more specialized class(es) in the hierarchy.


\item {\em New information about the roles of individual $b$
can be inferred.} For example, learning that a role is closed allows
us to now count its fillers and hence obtain an exact upper bound
recordable by \atmost.

\item {\em New assertions can be inferred about other individuals,
usually ones related to $b$ via roles.} For
example, if an \cc{\all(friends,HAPPY)} description applies to some
individual $x$, and now $y$ is asserted to be a \cc{friends}-filler
for $x$, then we can infer that $y$ is an instance of \cc{HAPPY}.
\end{itemize}

To support the first task above, \protodl\ might use the function
\cd{ConsistentW?}\footnote{Later, when we introduce incremental reasoning,
we will identify a number of variants of this function.}, which returns true to indicate that information to
be added to an individual is consistent.
For the second task, we use function \cd{Recognizes?}.
\comment{ Again, note that
  \cd{Recognizes?(b,C)} returns $true$ when it is certain that $b$ is an
    instance of $C$, and false otherwise. Thus,
   Note that the three valued nature of the
  relationship between an individual and a concept can only be revealed
  by calls to two functions: \cd{Recognizes?} and \cd{ConsistentW?}.
  }
For the third and fourth tasks, which involve individuals other than
the one on which the update has occured, we use function
\cd{InferFrom}.

These functions are used to implement the various {\sc assert} KBMS
operations, as well as the \cd{ClassifyIndividual} function, which is
used by \protodl\ to find the lowest classes in the hierarchy to which
this individual belongs.

As in the case of concept reasoning, we use the \cand\ constructor to
drive the processing, and we modularize the implementation so each
kind of constructor \K\ has its own set of functions: 
\comment{
  \indent
  \cd{\K::Recognizes?($<$Individual$>$,$<$\K termRep$>$)}\\ \indent
  \cd{\K::ConsistentW?(Individual,\K termRep)}\\ \indent
  \cd{\K::InferFrom(Individual,\K termRep)}\\ 
  }
\fbox{\cd{\K::Recognizes?}}, \fbox{\cd{\K::ConsistentW?}},
\fbox{\cd{\K::InferFrom}}. It now becomes more important to
distinguish  constructors, like \all\ and \atmost,
that have an associated single role, in contrast to generic constructors
such as \oneof\ (which has no roles associated) and \sameas\ (which
has many roles, none of which is special). For the former, so called 
{\em branch constructors},
the above functions will have  arguments that include not
just the individual and the normalized representation of \K-terms, 
but also the fillers and closed information about the role. (This is
done to prevent repeated retrieval of these values by each
such constructor.) Therefore, the general form
of \cd{\cand::Recognizes?}, provided in \protodl, is
\begin{display}
 \cd{
 \cand::Recognizes?(b:$<$Individual$>$,NC:$<$NormalizedConcept$>$)returns $<$Bool$>$
       \{ For every \K(T) in getNonbranchComponents(NC) do
            if not \K::Recognizes?(b,\K(T)) then return false;

          For every role p in  getRestrictedRoles(NC) do
            \{F:= get\_fillers(b,p);
              clsd? := is\_closed?(b,p);
              For every  \K(T) in getBranchComponents(NC,p)
                \{if not \K::Recognizes?(b,\K(T),F,clsd?) 
                  then return false\};\};
          return true;  \}
}\end{display}
\noindent
\comment{
  Note that if there is a way of writing the above code in a
  generic/parametric way, then this program need not be modified when a
  functions for a new constructor, \K, are added. Otherwise, appropriate
  explicit calls must be inserted.
}


The functions \cd{\cand::ConsistentW?} and \cd{\cand::InferFrom} are
similar in structure, and are not presented due to space limitations.
It is important to note that the \cc{ConsistentW?} functions return
false only to indicate that they are unable to prove {\em
conclusively} that the individual is consistent or inconsistent; if an
inconsistency is found, an \incnx\ is raised. Also, after an update
there may be 
several individuals about which incompatible information will be
asserted. The system only guarantees to find {\em one} such case, and
then rejects the update.

\smallskip
 
The following is an example of a specialized function for the case 
\K=\all, which implements the  first inference rule presented earlier
\begin{display}{\small \cd{

  \all::Recognizes?(b:$<$Individual$>$, \all(r:$<$Role$>$,vr:$<$NormalizedConcept$>$),
               fillers:$<$SET(Individual)$>$, clsd?:$<$Bool$>$)  returns $<$Bool$>$
       \{if not clsd? then return false {\rm {\em /*More fillers might come later*/}}
        else for every f in fillers do
               \{if not \cand::Recognizes?(f,vr)
                then return false;\}
        return true \}
}}\end{display}

\subsection{Reasoning with Incremental Updates }
Since updates to individuals are incremental in nature, in order to improve
efficiency we want to take into account the fact that the KBMS had already
performed all the inferences up to, but not including,
the current update. For example, if some
individual \cc{Tintin} has been asserted to be an instance of
\cc{\all(pet,DOG)}, and  already has pet-fillers \cc{d1} and \cd{d2},
then if the current update is  
\cc{\opc{assert-fills}(Tintin,pet,Fido)}, then we only need to
propagate the information that pet-fillers are \cc{DOG}s to \cc{Fido}, since
the others would have been processed earlier. And, if the current
update is \cc{\opc{assert-closed}(Tintin,pet)}, then no new role-filler
information can be inferred from this because of the \all\
restriction, so we should not even bother calling \cd{\all::InferFrom}.
We will therefore distinguish the following three variants of
\cd{\K::InferFrom}:\\

\medskip

\noindent
\fbox{\cd{\K::InferFromFilling($<$Individual$>$,$<$Normalized\K-term$>$,$<$Role$>$,$<$Individual$>$)}} \\ 
\fbox{\cd{\K::InferFromClosing($<$Individual$>$,$<$Normalized\K-term$>$,$<$Role$>$)}}, and\\ 
\fbox{\cd{\K::InferFromAsserting($<$Individual$>$,$<$Normalized\K-Term$>$)}} \\

\smallskip

\noindent plus similar variants of \cd{\K::ConsistentW?}.
For example
\begin{itemize}
\item \cd{\all:ConsistentWFilling?(ind, \all(r,vr), r, newfiller)} 
invokes \cd{\cand::Consis\-tentW}\cd{Asserting?}\-\cd{(newfiller,vr)} to
 check that the new filler does not contradict the role restriction
\cd{vr};

\item \cd{\all::ConsistentWClosing?(ind,\all(r,vr),r)}
 just returns true, and hence is hopefully eliminated by the
compiler;

\item \cd{\all::ConsistentWAsserting?(ind,\all(r,vr))}
 verifies that all r-fillers \cd{y} of \cd{ind} are consistent with \cd{vr} by
 invoking \cd{\cand::ConsistentW\-Asserting?(y,vr)}.
\end{itemize}
\comment{
We note that in both cases there is an implicit assumption (born out
by empirical evidence with attempted extensions) that inferences about
individuals from the conjunction of C and D, can be usually obtained
from the union of the inferences from C and those from D. (This is not
always the case, so we must view these decompositions as heuristic.)
}

One might also consider variants of \cd{\K::Recognizes?}, but, as we
shall see, in our case these are of limited use since we do not
propose to keep information on which parts of the recognition test had
succeeded already, and therefore we need to start from the beginning.


\subsection{Dependency Links} 

Clearly, the results of function calls, such as \cd{Recognizes?}, on
some individual \cc{Bob} might change after an update to \cc{Bob} itself.
However, the membership of \cc{Bob}  in a class or \cc{Bob}'s 
consistency may depend on facts asserted about {\em other} individuals
in the database. For example, if all of \cc{Bob}'s friends are known
(i.e., the role \cc{friends} is closed), and all but one of them was
\cc{MARRIED}, and now that holdout, \cc{Larry}, is also asserted or
inferred to be \cc{MARRIED}, then  \cc{Bob} itself can be reclassified
as an instance of \cc{\all(friends,MARRIED)}.  

This means that without some special data structure, after  every update
of some individual an unsophisticated implementation has to
reconsider {\em every} other individual in the KB.

One alternative, used in {\sc loom} \mycite{loom}, is to
keep track of all  questions asked about an individual as part
of the previous processing (``hits'' and ``misses''), and if answers
to these do not change as a result of the update then no {\em
\underline{re}-processing} is needed. 
Another alternative is to use an elaborate truth-maintenance system
(as available in {\sc kl-two} \mycite{vilain:ijcai85}),
for each kind of judgment. In our opinion, both these approaches
might however become very expensive in terms
of space and often computation time, because they maintain too many details.

We follow an intermediate stance, first suggested by Peter
Patel-Schneider for the \classic\ implementation, which is intended to
reduce needless re-testing while incurring relatively less
``dependency maintenance'' overhead.  Essentially, we have a
``coarse-grained'' dependency structure, where one individual $e$ may
point to another, $b$, if the result of a decision about the latter
may change as a result of {\em some} (unspecified) additional
information being added to the former.  For example, in the presence
of the definition \cc{CanineLover}$\doteq$\cc{\all(pet,DOG)}, if \cc{Tintin}
has \cc{Fido} as a \cc{pet} filler, and neither \cd{
Recognizes?(\cc{Fido,DOG})} nor \cd{{\bf not}
ConsistentW?(\cc{Fido,DOG})} return true, then we add a link of the
form: \reclink{Fido}{Tintin}. Thereafter, any change of status of
\cc{Fido} will cause \cc{Tintin}'s classification (with respect to
\cc{CanineLover}, as well as other pending classes) to be re-done.
Similarly, we will have \conslink{}{} and \inflink{}{} links between
objects.

Note that when following such dependency links back, we do know
that only properties of the fillers of some role might have changed, so that
once again we could have variants  \cd{\cand::Recheck\-ConsistentW?} and
\cd{\cand::RedoInferFrom}, which perform less work by omitting the
checks involving constructors that are known not to be affected by
such aspects (e.g., \atmost\ only cares about the count of the
fillers, not their properties).

In order to set dependency links, every function such as
\cd{\K::Recognizes?} 
%and \cd{\K::ConsistentW?}
 needs to keep track of
the list of individuals whose modification might change the result of
the function.  These values must eventually be appropriately linked
with dependencies either by the functions themselves or by the calling
environment.


\subsection{Coordinating the Components}\label{topLevel} 

As should be clear from the above examples, the task of the top-level
KBMS update operations (\opc{assert}s) will include not just invoking
the appropriate functions {\em on the individual being updated}, but
also setting appropriate dependency links, gathering into queues other
objects whose dependency links have been ``tickled'' by the latest
update, and then repeating these operations on the other individuals
brought into focus by inferences or dependency links.

An appropriate software architecture for representing this processing
seems to be a blackboard model, where we have 5 lists to which
functions can post tasks to be carried out:
\begin{itemize}
\item Two lists, \cd{ToRecheckConsistencyList, ToRedoInferFromList},
for objects that are reached from individual $x$ via a corresponding kind of
dependency link as a result of a change to $x$. 

\item A list, \cd{ToPerformUpdateList}, which collects the additional
inferences to be made that are found by the \cd{InferFrom} and
\cd{RedoInferFrom} function calls.  For simplicity, these are
recorded as additional calls to versions of the three kinds of \opc{assert}
functions.

\item A list, \cd{ToReclassifyList}, which receives objects that need to be
checked in case they can be classified further down the hierarchy; these
objects come not just from dependency links but also from any additional
\opc{assert}s that had been triggered.

\item Finally, a list \cd{ToAddDependencyList}, that keeps track of dependency
links that need to be added to the knowledge base;  this list is
augmented by the various functions, as mentioned in the previous section.

\end{itemize}
Because, for example, re-classification may cause new inferences,
which may cause re-classification due to some other constructor, there
is no linear order in which these lists can be
processed. We may therefore have a loop where a ``demon''
removes an arbitrary object from a list, invokes the required
function, and then repeat the process. The only requirement is that
dependencies on  \cc{ToAddDependencyList}  be also considered as
having been installed,
whenever chasing objects that may have been affected by an update.
Note that, 
not surprisingly, it is hard to make any general statements about the
termination of the above algorithm skeleton, since the various
functions, especially \cd{InferFrom}. are free to do whatever they
want, including increasingly longer descriptions..


Several policies can help the performance of the system:
\begin{itemize}
\item  In all
cases, it is helpful to eliminate duplicates from the lists.

\item Locality of context may improve performance; therefore grouping
 together operations to be performed on one object is advisable (e.g.,
gather together all the dependencies from object $y$ on
\cc{ToAddDependencyList}).  

\item If we expect inconsistencies to arise
infrequently, then the \cd{ToRecheckConsistencyList} can be processed at the end.
\end{itemize}

\noindent Figure~\ref{assert-fills} contains the pseudo-code for
\opc{assert-fills}, which is offered by \protodl.
\begin{figure}[htb]
\begin{display} {\small  \cd{ 
        \opc{assert-fills}(ind, role, filler)
             \{if { redundant information} then signal \redundx;
               add\_filler(ind,role,filler);  /*{\em this may be rolled back by an error} */
              initialize the blackboard lists to empty; 

              ind-descr := \descr(ind);
              {\em /* deal with consistency issues involving ind */}
                    \cand::ConsistentWFilling?(ind, ind-descr, role, filler); 
                      {\em /* the preceding function will post dependencies if
                        the answer is not a definite TRUE  */}
                    ToRecheckConsistencyList += getConsistentDependsOnMe(ind);
                      {\em /* this puts up for reconsideration objects
                                dependent on ind */ }
              {\em /* check for inferences */}
                    \cand::InferFromFilling(ind,ind-descr,role,filler);
                          {\em /* this may post new updates and/or dependencies */}
                    ToRedoInferFromList += getInferDependsOnMe(ind)
              {\em /* reclassify at least this individual */}
                    Reclassify(ind);
                    ToReclassifyList += getRecognizeDependsOnMe(ind);
              {\em /* Process tasks left on the blackboard */}
                    ProcessBlackBoard;
             \}
                catch \incnx\ 
                    \{roll back update; print error msg; \}
}}\end{display}	 

\caption{\protodl\ pseudo-code for \opc{assert-fills}.} \label{assert-fills}
\end{figure}
Notice the advantage in the above program of using exception handling
 and propagation up the {\em dynamic} function call hierarchy as a way
 of dealing with inconsistency: wherever it is detected
 by \cd{ConsistentW?}, the exception passes up through levels of
 function calls, all of which are interrupted, until a handler is
 encountered --- usually by an external or internal \opc{assert}
 operation; this issues appropriate error messages, resets local
 changes made, and then re-raises/propagates the exception further up,
 until the top level is reached. 


\subsection{Extending Individual Reasoning --  An Example}
 Let us consider the extensions needed for a rather complex new concept
constructor: \sameas. The semantics of \sameas(\cc{[$f_1, \cdots
,f_n$],[$g_1, \cdots ,g_m$]}), as introduced earlier, is that it denotes individuals for which
the two attribute chains [$f_1, \cdots ,f_n$] and
[$g_1, \cdots ,g_m$]
have the same known filler. (The attributes must each have exactly one
filler.)

This constructor is very useful in representing the relationship
between actions and sub-actions. For example, suppose we try to define
the action of \cc{BUY}ing in terms of
two \cc{GIVE}s: we would assert that \cc{BUY} is subsumed by 
\cc{\cand (\all (giving1,GIVE),\all (giving2,GIVE))}, and then
add further constraints about the attributes of \cc{BUY} (such as
\cc{buyer} and \cc{seller}) and those of \cc{GIVE} (such as \cc{giver}
and \cc{receiver}), including
 \cc{\sameas([buyer],[giving1 giver])} and  \sameas( \cc{[seller]},\cc{[giving1
receiver]}).



The procedures that need to be written to extend the implementation
are: \cd{ \sameas::\-Recognize,
\sameas::\-InferFromFilling, 
\sameas::\-InferFromClosing,
\sameas::\-InferFromAsserting,
\sameas::\-ConsistentWFilling?, 
\sameas::\-ConsistentW\-} \cd{Closing?,} and \cd{
\sameas::\-ConsistentW\-}\cd{Asserting?}. In addition, some previously written
procedures may need to be augmented. 


Rules of inference for \isin\ and \notisin\ can be presented as a way
of describing the tasks performed by the above functions. However, in
this case, the functions also need to worry about dependency pointers,
so the mapping is less direct.


The following inference rule describes the standard recognition
procedure for individuals (there are additional rules for subsumption
of course):
\[
\frac{
\begin{array}{c}
 \kbee \hasfiller{b}{[f_1,\cdots,f_n]}{e} \\
 \kbee \hasfiller{b}{[g_1,\cdots,g_m]}{e}
\end{array}
}{
\kbee b \isin \sameas([f_1,\cdots,f_n],[g_1,\cdots , g_m])
}
\]
If the recognition function can only follow a chain up to an
individual $e$, which is missing the filler of the next attribute in
the chain, then a dependency from  $e$ must be recorded.

\smallskip

\begin{display}\cd{
  {\sameas::Recognizes?}(b, \sameas(chain1,chain2))
      \{ (e1,p') := {  follow} chain1 { from} b, { returning the furthest
	     individual} e1 { reached, and the  remainder of the chain} p'
	     { which was not possible to follow};
	 if not(p'=nil) 
	    then \{ { post dependency \reclink{e1}{b}}; return false;\}
	 (e2,q') := { follow} chain2 { from} b, { as above;}
	 if not(q'=nil) 
	    then \{ { post dependency \reclink{e2}{b}}; return false;\}
	 if (e1=e2) \& p'=q' then  return true else return false.
       \} }  \end{display}

\noindent  This function will be called from inside
\cd{\cand::Recognizes?(b,C)} as follows: 
\begin{display}\cd{
        ...
      for every \sameas(chn1,chn2) in get\_sameas(C)
	 if not \sameas::Subsumes?(\sameas(chn1,chn2), \descr(b))
	 then if not  \sameas::Recognizes?(b,\sameas(chn1,chn2))
	      then return false.
	  ...
}\end{display}

Reasoning with \sameas\ concerning individuals is actually
more complex, because there are additional rule of inference, such as
\[ \frac{
\begin{array}{c}
\kbee \hasfiller{b}{chain1}{e} \\
\kbee b\isin \sameas(chain1,chain2) \\
\kbee e\isin \sameas(chain3,chain4)
\end{array}
}{
\kbee b \isin \sameas( chain1\circ chain3 , chain2 \circ chain4 )
}
\]
\noindent
Applying this rule straightforwardly to verify whether some 
$b \isin \sameas([f_1,\cdots,f_n],$ $ [g_1,\cdots,g_m])$
requires one to try all possible ways of dividing up the  chain
$[f_1,\cdots,f_n]$ into subchains, and for each, one needs to try to derive the
subchain equalities alternately from individual fillers along the chain, or
from explicit assertions of \sameas\ descriptions on
individuals. In this cases, the implementor, in consultation with
the knowledge engineer who is to use the extended system, would make a
judgment on the necessity of implementing this more expensive
inference. The rules of inference can be used to describe the deductions that
have been implemented and those that have not.


\medskip

\noindent In order to check consistency, we need to consider the three
kinds of updates: assertions, fillers, and closings. When an equality
is first asserted of an individual, we would invoke:

\smallskip
\begin{display} \cd{
   \sameas:: ConsistentWAsserting?(ind, \sameas(chain1,chain2))
      \{ (e1,p') := { follow chain1 from ind;}
	 if not(p'=nil) 
	    then \{ { post dependency \conslink{e1}{ind}}; return true;\}
	 (e2,q') := { follow chain2 from ind;}
	 if not(q'=nil) 
	    then \{ { post dependency \conslink{e2}{ind}}; return true;\}
	 if e1=e2 then  return true else signal \incnx;
	 \}  }
\end{display}

\smallskip
Since the attributes can have at most one value, these attributes get closed
automatically when a filler is provided, so there is usually no explicit
closing of the role that can affect \sameas, and there is no need
for \cd{\sameas::ConsistentWClosing?}. 

Finally, if \cc{C} includes as a conjunct \cc{\sameas(chain1,chain2)}, then
 \cd{\cand::ConsistentW\-Filling?\-(ind,C,p,newfiller)} will have to
invoke 

\begin{display} \cd{
     \sameas::ConsistentWFilling?(ind,\sameas(chain1,chain2),p,newfiller)
	  \{if (member(p,chain1) OR member(p,chain2) )
	    then \sameas:ConsistentWAsserting?(ind,\sameas(chain1,chain2))\}
}\end{display}


Equalities can lead to inferences when one of the chains is completely known,
and all values but that of the last attribute on the second chain are
known, as illustrated by the following example:
\[
\set{a:\sameas([q]\; ,\;[p,r]), \ \   (a,e):q,\ \ (a,b):p} \ \models \
b \isin \fills(r,e)
\]
This inference requires us to set up \inflink{}{} links to watch for
cases when we have sufficient information to make the
inference.
\comment{
\begin{display}
function \sameas::InferFromAsserting(ind, \sameas(chain1,chain2))
   \{(e1,p') := follow chain1 from ind;
    (e2,q') := follow chain2 from ind;
    (cond    
        (p'==nil) ==$>$  if length(q')=1 then post assert-filler(e2,q',e1)
                        else post \inflink{e2}{ind}
        (q'==nil) ==>  if length(p')=1 then post assert-filler(e1,p',e2)
                        else post \inflink{e1}{ind}
        (length(p') $\geq$ 2)  ==>  post \inflink{e1}{ind}
        (length(q') $\geq$ 2)  ==>  post \inflink{e2}{ind}
        (length(p')=length(q')=1) ==> post \inflink{e1}{ind} and \inflink{e1}{ind}
    )\}
\end{display}
}%cmt

We point out that \sameas\ presents one example of a situation
where a performance penalty is paid for separating out consistency
checking, recognition and inference: each of these functions attempts
to traverse the individuals along the two chains of the equality in an
effort to reach the ends. This price is negligible
if there are relatively few individuals with
\sameas\ conditions attached, or if the chains are usually only one or
two attributes long, as is the case for the
application of \sameas\ illustrated earlier.
Otherwise, we can introduce caching to speed up the code: associate
with every equality  and individual $b$ two pairs ($e_1$,$r_1$) and
($e_2$,$r_2$) representing the 
ends $e_i$ reached on each chain, and the remainder of the chains $r_i$
left to be traversed. (So if the chain is completely known, $r=nil$.)
A final alternative is to add the code for \cd{\sameas::InferFrom}
into \cd{\sameas::ConsistentW?} function, so the latter performs
all the deductions involving \sameas. The disadvantage of this
approach, as of many optimizations, is the loss of modularity.

\comment{The above discussion should make clear that the \protodl\ approach
offers quite a variety of implementation alternatives, which would
likely not be considered by an automatic approach that started only
from the inference rules.
}

\smallskip

Finally, we mention that other extensions of reasoning at the
individual level that we have considered include ``database aggregate
functions'' like $sum$ (e.g., \cc{{\tt\bf sum}([departments budget],
totalBudget)} can be used to model that \cc{totalBudget} is the sum of
the values for \cc{budget} fillers for all department fillers); and
epistemic constructors that allow one to query the
state of knowledge \shortcite{epistemic} (e.g.,
\cc{\known-\all(friends, \known-\atmost(1,pets))} recognizes
individuals all of whose {\em known} \cc{friend} fillers have at most
one pet recorded in the KB, without having to have the roles be
closed).


\section{Conclusions}

We began from the hypothesis that no ``perfect'' DL will ever be
built, because of the need for application-specific reasoning, and 
potential incompleteness of reasoning due to the
expressiveness-(tractability/decidability) trade-off.
 We argued that some of these issues are best attacked on a per-application basis.
To resolve this problem, we proposed the use of an {\em extensible}
DL-KBMS, where one tries to go as far as possible with an initial set of 
well-understood concept constructors, and then, when encountering
unsolvable expressiveness problems \mycite{doyle:patil}, add new
concept constructors to overcome them.
\comment{  This has the advantage that
  the language user tries to use the efficient features to their fullest
  extent before turning to more esoteric/expensive constructs; and that
  the resulting reasoner does not have ``unnecessary baggage'' -- unused
  constructors, which extract a performance penalty even if not used
  (e.g., by claiming possible space in data structures, or by constantly
  checking for the occurrence of unused constructors).
}

We have also pointed out the limitations of this approach, which
include not being conducive to including new forms of reasoning such
as abduction, contexts, etc., and having difficulties with complete
inferences for useful concept constructors that require reasoning by
contradiction, and  are best handled in the alternative DL reasoning
paradigm -- tableaux. 

\subsection{Implementation Status}
Prototype implementations of aspects of both concept and individual
reasoning in \protodl\ have been carried out at Rutgers. However,
experience with all  fielded  systems indicates that there is an order
of magnitude more work to be done in making a system usable by others than
their developers. For this reason, our goal is to add the results of the
\protodl\ research to an existing DL-reasoner. In fact, several ideas 
 have been transfered, with the collaboration of Charles Isbell, to
the newest version of the \classic\ system released by AT\&T
Research. In particular, \classic\ supports {\em test-defined}
concepts -- ones which allow the recognition of individuals through
the use of an arbitrary LISP function. (This function can be seen
as the combination of the \cd{Recognizes?} and \cd{ConsistentW?}
functions discussed in the present paper.) In the newest version of
\classic, one can simulate the addition of new concept constructors by
using them after the keyword {\bf test-c}. For example, the 
concept \cc{\all(vacation,\drng(1996/6/1,1996/8/31))} would be
represented as\\ \indent \cc{({\bf test-concept} dateRange vacation '(
(1996 6 1) (1996 8 31)) ) }

 Although not all aspects of the \protodl\ system have
been implemented, the current extensions \mycite{borgida:dl96} allow
significant subsumption reasoning to be done for test extensions, and
thus provide \classic\ with the bases for extensible reasoning.


\subsection{Related Work}

In order to incorporate new concept constructors into a reasoner, we
need to extend the implementation. One approach to this  would be
to offer some form of ``declarative description'' of the inferences to be
performed, and then have a meta-interpreter which executes them.
In fact, such approaches have been tried in the past for other kinds
of representation formalisms \mycite{grein:rll,gene:mrs}.
Except for {\sc cycl}~\mycite{cyc}, which allows the
addition of new forms of inference rule schemas in First Order
Predicate Calculus, we see little evidence that such a meta-interpreter
has a chance of being nearly as efficient as custom-built
implementations, so we have opted for a different approach.


 Joshua \mycite{joshua} is also an effort at providing extensible
reasoning, which allows the user (knowledge system engineer) the
ability to change at compile-time the implementation of any or all of
the elements of the {\it protocol of inference}, which describes the
reasoning of the system.  Joshua is close in spirit to our work in the
sense that it tries to maintain a uniform ``knowledge level'' view of
the system, and because it identifies, in the ``protocol of
inference'', the specific aspects of the system that can be customized
through (re)programming of Lisp functions. Our efforts differ from
Joshua in that we are interested in DLs (Joshua's protocol was
concerned mostly with rule triggering and truth maintenance), we wish
to support incrementing the syntax of the knowledge-level interface,
and we also care about the semantics of the extension.


Gaines has also advocated the utility of a declarative specification
and of a clean, extensible modularization for a DL-reasoner
\mycite{gaines}.   At the concept level, one difference between our
approaches seems to be that \protodl\ only assumes that the concepts
will form an upper-semilattice (the \cand\ constructor is built-in),
so that a wider variety of inferences can be implemented for new
constructors.  At the individual-reasoning level, \protodl\ starts
from a much more restricted basis, and uses its extensibility to deal
with such aspects as ``propagations'' (e.g., our example dealing with
\sameas\ reasoning appears to be built-in in KRSn). On the other hand,
KRSn has built-in support for rules and exceptions to them, which are
an important component for any knowledge-based environment.

Finally, it has been suggested 
that the tableau-based approach, such as that of  {\sc crack}, is 
essentially extensible through the
addition of new ``completion'' rules \cite{franconi}, which are traditionally used to
build a model of a certain knowledge base, or prove its
inconsistency.  These tableau completion rules 
%are usually closely
%related to the denotational semantics of the concept constructors,
%and one 
can also implement incomplete reasoners
by using only a subset of the inferences. As with concrete
domain extensions (Section~\ref{concrete}), the advantages of
extensible tableau techniques lie in a
clean formalism that can lead to complete reasoning, while the
disadvantages involve language extensions that do not have negation
(e.g., \clasp\ -- see Section~\ref{experience}), and, for the moment,
the lack of experience with large A-boxes and incremental updates. 
One of the most exciting  (though very likely difficult) future
prospects is combining the two implementation paradigms, and their
extensibility features.


\subsection{Summary}
We have advocated an approach to extensible DL reasoning and
implementation, for the normalize-compare paradigm, which has two
components: a declarative specification and a modularized
implementation framework.
\comment{
Such a dual approach ought to make it easier to integrate extensions
into a ``universal'' language for communicating between knowledge
bases, such as the Generic Frame Protocol \mycite{gfp}.
}
The specification is offered using rules of inference in the ``natural
semantics'' style, and a heuristic methodology suggests various
categories of rules to be looked for. These rules often correlate well
with the implementations of the various functions, but \protodl\
offers the implementor the opportunity to use a very different
implementation. The later is needed in the case of
constructors whose argument is for example some regular expression --
as in the case of plans or strings, when the implementation needs to
use some kind of finite automaton representation, since regular
expressions have no ``normal form''.

We have modularized the software architecture of \protodl\ reasoner,
so that for every new concept constructor added to the language, there
is a well-defined set of functions that need to be implemented.
These, in turn, sometime have detailed skeletons composed of other,
smaller functions, which we have abstracted after analyzing a variety
of implementations. The invocation of these functions is organized by
the built-in functions of \protodl, usually involving the constructor
\cand. We have paid particular attention to supporting efficient
implementations, by offering the implementor
quite a lot of freedom within the confines of our major
functions. For individual reasoning, this is the first paper to
consider the need to be efficient in the face of incremental updates
of DL-KBMSs, which live with the open-world assumption, and which use
concept descriptions to infer new properties, rather than just verify
the correctness of individual facts. Our solutions involved proposing
function variants based on the form of the update, and the use of
various kinds of associated dependency links.

The major open areas involve adding to this framework role
constructors, epistemic rules (like those in \classic, characterized
by Donini et al \mycite{epistemic}), 
 the ability to express at least simple recursive
declarations for primitive concepts (e.g., ``the parents of a person
are persons''), and connections with the tableau-based
implementations for DL reasoning.

\acks{
I am very grateful to Ron Brachman, who, among others,
joined me in the initial explorations of the \protodl\ idea; to Daniel Kudenko,
who implemented a significant part of the individual reasoning;  to
Charles Isbell, who implemented the extensibility features of
\classic\ 2.3; and to Peter Patel-Schneider, for years of discussion
on the subtleties of the \classic\ language and implementation.
Extremely useful comments on the presentation and organization were provided
by Peter Clark and the anonymous reviewers.

This work was supported in part by NSF grants IRI-91-19310 and
IRI-9619979.
}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\appendix
\section*{Appendix A. A Generic Conjunction Function.} 

{\sloppy
The following pseudo-code for \cd{\K::Conjoin} shows how one can
construct this function from several, smaller functions. 

\begin{figure}[h]
\begin{display}\cd{
/*{\em Conjoin the new term \K(T) onto the already-normalized description This}*/

\K::Conjoin(T:$<$Normalized\K-term$>$,This:$<$NormalizedConcept$>$)\{

    old :=  get\_\K(This) /*{\em find the part of This dealing with constructor \K}*/
    if not(old=nil) 
    then if  \hilite{\K::SubsumesSame?}(T,old)
	 then signal \redundx;
     T := { \K::ConjoinToSame}(T,old); /*{\em  combine T with old}*/

    if { \K::SubsumesDifferent?}(T,This) /*{\em T is implied by other constructors }*/
    then signal \redundx;

    T:= { \K::ConjoinToDifferent}(T,This) /*{\em obtain a possibly stronger T}*/
    if (type(T) $\neq$ \K) /*{\em the stronger description might use another constructor}*/
	then \{post T to ImplicationsToDoList; /*{\em for later processing}*/
              return; \}
    {\K::ConsistentWithDifferent?}(T,This) /*{\em Check if T is coherent with the rest
                                        of This;  if not, an exception is raised.}*/
    
    put\_\K(T,This) /*{\em add the description to the normalized descriptor This}*/
    {\K::FindOtherImplications}(T,This,ImplicationsToDoList) 
		/* {\em add any additional constructors implied by T and This */} }
\end{display}
\caption{Pseudo-code of a generic conjunction function.}\label{conj}
\end{figure}

\noindent Before we consider the individual functions introduced
above, we remark that if the constructor \K\ implies terms built with
other constructors (i.e., it adds entries to the
\cd{ImplicationsToDoList}), then the \cd{\cand::Conjoin} function needs
to be augmented with a loop at the end, which conjoins to \cd{ontoNC} all the 
normalized terms on the \cd{ImplicationsToDoList}:
\begin{display}\cd{      while notEmpty(ImplicationsToDoList)
	 \{ another := removeAnElement(ImplicationsToDoList);
	    {\rm suppose} type(another)=\K;
	    \K::conjoin(another,ontoNC) 
}\end{display}
Note that this processing may itself add new entries to the
\cd{ImplicationsToDoList}. In the case that there are many additions being done to the 
ImplicationsToDoList, a  useful  optimization might be to test for and
remove redundancies from ImplicationsToDoList. If there are very few constructors making
additions,  a different optimization might be applied:
add the above code only to the end of the corresponding
constructor's \cd{Conjoin} program.

\medskip

 The following is the intended purpose of the component
functions used in the \cd{\K::Conjoin} function in
Figure~\ref{conj}. Note that for any particular constructor (e.g.,
\all), not every such function needs to be implemented. When using a
good optimizing compiler, default programs for these could be
provided, which return constant values. Otherwise, \cd{Conjoin} itself
should be edited.
\begin{itemize}
\item \cd{\K::Universal?(T)}: {\it Is \cc{T} equivalent to the
top of the hierarchy for that set of values?} For example,
\cd{\atleast::Universal?} returns true when processing \cc{\atleast(0,players)}. This is used to eliminate unnecessary
constructs from the normal form.

\item \cd{\K::Incoherent?(T)}: {\it Is \cc{T} incoherent by
itself?} \\ For example,  \cc{\some(players\ ,\nothing)} is  incoherent since
\nothing\ has no instances.

\item \cd{\K::IncoherentWithDifferent(T,This)}: {\em Is there an inconsistency
if we consider conjoining with other constructors?} 
For example, when \K=\atleast, conjoining \cc{\atleast(3,players)} to a
concept already containing \cc{\atmost(1,players)} would lead to
inconsistency.


\item \cd{\K::SubsumesSame?(T,oldTs)}: {\it Is \cc{T}  implied by
the  \K-constructed terms already seen in oldTs?} 
This is basically the ``structural subsumption'' part.
For example, if \K=\atleast, and \cc{oldTs} has
\cc{\atleast(4,players)}, then  \cc{\atleast(3,players)} is
redundant


\item \cd{\K::SubsumesDifferent?(T,This)}: {\it Is \cc{T} implied by other
constructors?} 
For example, \cc{\atleast(1,players)} is implied by \cc{\some(players,
OLD)}.

\item \cd{\K::ConjoinToSame(T,OldTs)}: {\it  Merge \cc{T} with any preceding
terms built with \cc{K}.} 
For example, when  we combine
 \cc{ \all(players,GENTLEMAN)} with \cc{ \all(players,SCHOLAR)}, we
obtain \cc{\all(players,\cand(GENTLEMAN, SCHOLAR))}\@.

\item \cd{\K::ConjoinToDifferent(T,This)}: {\it Produce a stronger \cc{T} by
using information from other constructors.}
For example, if we are processing  \cc{\some(player, TALL)},then if the concept \cd{This} already has 
 \cc{ \all(player,OLD)}, then \cd{\some::ConjoinToDifferent} returns the
description of \cc{\some(players,\cand(TALL,OLD))}.

\item \cd{\K::FindOtherImplications(T,This,ImplicationsToDoList)}:
{\it Add constructors which are implied because of \K(T), possibly in
conjunction with the rest of the concept, \cd{This}.}  
For example, when adding \cc{\all(players,TALL)} to a concept with
 \cc{ \atleast(3,players)},
\cd{\all::FindOtherImplications} would 
add  \cc{\some(players,TALL)} to the list of  constructors
to be conjoined to \cd{This}.
\end{itemize}
}

\vskip 0.2in
\bibliography{bibi-final} 
\bibliographystyle{theapa}
\end{document}
