%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Time-stamp: "1999-09-03 19:17:45 calvanes"
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\documentclass[11pt,twoside]{article}

\usepackage{epic}
\usepackage{eepic}
\usepackage{epsfig}
\usepackage{jair}
\usepackage{theapa}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\jairheading{11}{1999}{199-240}{7/98}{9/99}
\ShortHeadings{Unifying Class-Based Representation Formalisms}
{Calvanese, Lenzerini, \& Nardi}
\firstpageno{199}

\title{Unifying Class-Based Representation Formalisms}

\author{\name Diego Calvanese \email calvanese@dis.uniroma1.it\\
 \name Maurizio Lenzerini     \email lenzerini@dis.uniroma1.it\\
 \name Daniele Nardi          \email nardi@dis.uniroma1.it\\
 \addr Dipartimento di Informatica e Sistemistica\\
 Universit\`a di Roma ``La Sapienza''\\
 Via Salaria 113, I-00198 Roma, Italy
 }

\date{}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%\input{environments}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%% ENVIRONMENTS and THEOREMS

\newtheorem{theorem}{Theorem}[section]
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition} 
\newtheorem{lemma}[theorem]{Lemma} 

\newtheorem{definitionAux}[theorem]{Definition} 
\newenvironment{definition}{\begin{definitionAux}\rm}{\end{definitionAux}}

\newtheorem{claimAux}{Claim} 
\newenvironment{claim}{\begin{claimAux}\rm}{\end{claimAux}}

\newtheorem{exampleAux}[theorem]{Example} 
\newenvironment{example}{\begin{exampleAux}\rm}{\end{exampleAux}}
\newenvironment{exampleCont}[1]{\trivlist
  \item[\hskip \labelsep{\textbf{Example~#1 (cont.)}}]}{\endtrivlist}

\newtheorem{examplesAux}[theorem]{Examples} 
\newenvironment{examples}{\begin{examplesAux}\rm}{\end{examplesAux}}

\newtheorem{constructionAux}[theorem]{Construction} 
\newenvironment{construction}{\begin{constructionAux}\rm}
                             {\end{constructionAux}}

\newenvironment{proof}{\noindent\textsl{Proof.\ }}{\qed}
\newenvironment{proofsk}{\noindent\textsl{Proof (sketch).\ }}{\qed}

\def\Proof{\textsl{Proof.\ }}
\def\Proofsk{\textsl{Proof (sketch).\ }}


\def\qed{{\unskip\nobreak\hfil\penalty50    % qed with empty box
   \hskip2em\hbox{}\nobreak\hfil
   \qedboxempty
   \parfillskip=0pt \finalhyphendemerits=0
   \goodbreak\noindent}}
\def\qedboxempty{\vbox{\hrule\hbox{\vrule\kern3pt
                 \vbox{\kern3pt\kern3pt}\kern3pt\vrule}\hrule}}


\def\qedfull{{\unskip\nobreak\hfil\penalty50    % qed with full box
   \hskip2em\hbox{}\nobreak\hfil
   \qedboxfull
   \parfillskip=0pt \finalhyphendemerits=0
    \goodbreak\noindent}}
\def\qedboxfull{\vrule height 4pt width 4pt depth 0pt}

\def\endmarkfull{\qedfull}
\def\endmarkempty{\qed}

\def\If{\lq\lq$\Leftarrow$\rq\rq\ \ }           % 1st direction of iff-proof
\def\OnlyIf{\lq\lq$\Rightarrow$\rq\rq\ \ }      % 2nd direction of iff-proof

%%%%%%%%%%%%%%%%%%%%%%%%%%% BOXES

\newcommand{\fpbox}[3]{\framebox[#1]{\parbox{#2}{#3}}}
\newcommand{\boxtext}[1]{\fpbox{\textwidth}{0.95\textwidth}{#1}}
\newcommand{\boxcolumn}[1]{\fpbox{\columnwidth}{0.95\columnwidth}{#1}}
\newcommand{\boxformula}[1]{%
  \vspace{\abovedisplayskip}
  \boxtext{\vspace{-\abovedisplayskip} #1 \vspace{-\abovedisplayskip}}
  \vspace{\abovedisplayskip}}

%%%%%%%%%%%%%%%%%%%%%%%%%%% OTHERS

\def\incolumn#1{\begin{tabular}[c]{c} #1 \end{tabular}}
\def\incolumnmath#1{\begin{array}[c]{c} #1 \end{array}}
  % note: "x \atop y" may be more convenient

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%\input{newmacros}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%% General Math

\def\A{\mathcal{A}} \def\B{\mathcal{B}} \def\C{\mathcal{C}} \def\D{\mathcal{D}}
\def\E{\mathcal{E}} \def\F{\mathcal{F}} \def\G{\mathcal{G}} \def\H{\mathcal{H}}
\def\I{\mathcal{I}} \def\J{\mathcal{J}} \def\K{\mathcal{K}} \def\L{\mathcal{L}}
\def\M{\mathcal{M}} \def\N{\mathcal{N}} \def\O{\mathcal{O}} \def\P{\mathcal{P}}
\def\Q{\mathcal{Q}} \def\R{\mathcal{R}} \def\S{\mathcal{S}} \def\T{\mathcal{T}}
\def\U{\mathcal{U}} \def\V{\mathcal{V}} \def\W{\mathcal{W}} \def\X{\mathcal{X}}
\def\Y{\mathcal{Y}} \def\Z{\mathcal{Z}}

%%%%%%%%%%%%%%%%%%%%%%%%%% Abbreviations

\newcommand{\setone}[2][1]{\set{#1\cld #2}}
\def\eset{\emptyset}
\def\col{\colon}
\def\ol#1{\overline{#1}}                % overline
\def\ul#1{\underline{#1}}               % underline
\def\uls#1{\underline{\raisebox{0pt}[0pt][0.45ex]{}#1}} % underline with space
\def\iff{if and only if}

\def\ra{\rightarrow}
\def\Ra{\Rightarrow}
\def\la{\leftarrow}
\def\La{\Leftarrow}
\def\lra{\leftrightarrow}
\def\Lra{\Leftrightarrow}
\def\lora{\longrightarrow}
\def\Lora{\Longrightarrow}
\def\lola{\longleftarrow}
\def\Lola{\Longleftarrow}
\def\lolra{\longleftrightarrow}
\def\Lolra{\Longleftrightarrow}
\def\ua{\uparrow}
\def\da{\downarrow}
\def\uda{\updownarrow}
\def\Ua{\Uparrow}
\def\Da{\Downarrow}
\def\Uda{\Updownarrow}

%%%%%%%%%%%%%%%%%%%%%%%%%% Relations

\def\incl{\subseteq}
\def\imp{\rightarrow}
\def\deq{\doteq}
\def\dleq{\dot{\leq}}                   % dotted less equal

%%%%%%%%%%%%%%%%%%%%%%%%%% Spaces

\def\asp{\makebox[3pt]{}}       % arrow space, put before and after arrows
\def\osp{\hskip1pt}             % operator space, put before and after ops
\def\asps#1{{\asp#1\asp}}
\def\osps#1{{\osp{#1}\osp}}
\def\qland{\;\;\land\;\;}

\def\con{\asp\asp\&\asp}

\def\per{\mbox{\bf .}}                  % period

\def\cld{,\ldots,}                      % ,...,
\def\ld#1{#1 \ldots #1}                 % #1 ... #1
\def\cd#1{#1 \cdots #1}                 % #1 ... #1
\def\lds#1{\, #1 \; \ldots \; #1 \,}    % _#1_..._#1_
\def\cds#1{\, #1 \; \cdots \; #1 \,}    % _#1_..._#1_

\def\dd#1#2{#1_1,\ldots,#1_{#2}}        % x1,...,xn (da da)
\def\ddd#1#2#3{#1_{#2_1},\ldots,#1_{#2_{#3}}}    % xi1,...,xin (da da down)
\def\dddd#1#2#3{#1_{11}\cld #1_{1#3_{1}}\cld #1_{#21}\cld #1_{#2#3_{#2}}}
                                % x_11,...,x_1n,...,x_m1,...,x_mn_m

\def\ldop#1#2#3{#1_1 \ld{#3} #1_{#2}}   % x1 #3...#3 xn
\def\cdop#1#2#3{#1_1 \cd{#3} #1_{#2}}   % x1 #3...#3 xn
\def\ldsop#1#2#3{#1_1 \lds{#3} #1_{#2}} % x1 _#3_..._#3_ xn
\def\cdsop#1#2#3{#1_1 \cds{#3} #1_{#2}} % x1 _#3_..._#3_ xn

%%%%%%%%%%%%%%%%%%%%%%%%%% Delimiters

\def\quotes#1{{\lq\lq#1\rq\rq}}         % quote
\def\braces#1{$\{$ #1 $\}$}             % braces
\def\set#1{\{#1\}}                      % set
\def\Set#1{\left\{ #1 \right\}}
\def\bigset#1{ \Bigl\{ #1 \Bigr\} }
\def\bigmid{\ \Big|\ }                  % mid
\def\card#1{|{#1}|}                     % cardinality of a set
\def\Card#1{\left| #1 \right|}
\def\cards#1{\sharp #1}
\def\sub#1{[#1]}                        % [ #1 ]
\def\tup#1{\langle #1 \rangle}          % tuple < #1 >
\def\Tup#1{\left\langle #1 \right\rangle}

%%%%%%%%%%%%%%%%%%%%%%%%%% Constraints

\def\relc#1#2#3{#1#2#3}
%\def\inc#1#2{#1 \!:#2}
\def\inc#1#2{#1\col#2}

%%%%%%%%%%%%%%%%%%%%%%%%%% General Commands

%%%%%%%%%%%%%%%%%%%%%%%%%% Complexity Classes

\def\PTIME{\mbox{\textbf{PTIME}}}
\def\NP{\textbf{NP}}
\def\coNP{\mbox{\textbf{coNP}}}
\def\PSPACE{\mbox{\textbf{PSPACE}}}
\def\ETIME{\mbox{\textbf{ETIME}}}
\def\EXPTIME{\mbox{\textbf{EXPTIME}}}
\def\TIME#1{\textbf{TIME}(#1)}

%%%%%%%%%%%%%%%%%%%%%%%%%% Interpretation

\newcommand{\inter}[1][\I]{(\dom[#1],\Int[#1]{\cdot})}   % (dom^I,.^I)

\newcommand{\dom}[1][\I]{\Delta^{#1}}  % delta^I (domain of interpretation \I)
\newcommand{\Int}[2][\I]{#2^{#1}}      % #2^I    (interpretation function)
\newcommand{\INT}[2][\I]{(#2)^{#1}}    % (#2)^I  (interpretation function)

%%%%%%%%%%%%%%%%%%%%%%%%%% Concept forming operators

\def\AND{\sqcap}
\def\OR{\sqcup}
\def\NOT{\neg}
\def\ALL#1#2{\forall #1 \per #2}
\def\SOME#1#2{\exists #1 \per #2}
\def\SOMET#1{\exists #1}
\def\ALLRC{\ALL R C}
\def\SOMERC{\SOME R C}
\def\SOMERT{\SOMET R}
%%\def\ATLEAST#1#2{(\geq #1 \, #2)}
%%\def\ATMOST#1#2{(\leq #1 \, #2)}
%%\def\EXACTLY#1#2{(= #1 \, #2)}
%%\def\INV#1{#1^{-1}}

%%%%%%%%%%%%%%%%%%%%%%%%%% PDL forming operators

\def\True{\top}
\def\False{\bot}
\def\Not{\neg}
\def\And{\wedge}
\def\Or{\vee}
\def\Implies{\rightarrow}
\def\Diam#1#2{\langle #1 \rangle #2}
\def\DiamT#1{\langle #1 \rangle \True}
\def\Boxx#1#2{[#1]#2}
\def\Repeat#1{\Delta(#1)}
\def\Inv#1{#1^{-}}
\def\Star#1{#1^{\ast}}
\def\Comp{;}
\def\Choice{\cup}
\def\Test#1{#1?}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%\input{macros-l}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%% Abbreviations

\newcommand{\kb}{knowledge base}
\newcommand{\kbs}{knowledge bases}
\newcommand{\db}{database}
\newcommand{\dbs}{databases}
\newcommand{\oo}{object-oriented}

%%%%%%%%%%%%%%%%%%%%%%%%%% Languages

\newcommand{\ALUNI}{\mathcal{ALUNI}}
\newcommand{\aluni}{{\mdseries\textsc{aluni}}}
\newcommand{\alui}{{\mdseries\textsc{alui}}}
\newcommand{\ALUI}{\mathcal{ALUI}}
\newcommand{\CPDL}{\textsc{cpdl}}
\newcommand{\CPDLm}{\textsc{cpdl}^{-}}

%%%%%%%%%%%%%%%%%%%%%%%%%% Systems

\newcommand{\klone}{\textsc{kl-one}}

%%%%%%%%%%%%%%%%%%%%%%%%%% Relations

\newcommand{\ISA}{\mathrel{\dot\preceq}}	% <=
\newcommand{\ISAs}{\mathrel{~\dot\preceq~}}     % ~<=~

\newcommand{\mto}{\ra}
\newcommand{\x}{\times}
\newcommand{\cross}{\mathord{\times}}
\newcommand{\mul}{\mathop{\cdot}}
\newcommand{\mult}{\mathord{\cdot}}
\newcommand{\suchthat}{\,\per\;}

\newcommand{\defas}{=}

\newcommand{\geqt}{\mbox{\tiny $\geq$}}
\newcommand{\leqt}{\mbox{\tiny $\leq$}}

%%%%%%%%%%%%%%%%%%%%%%%%%% Special Notation

\newcommand{\lablist}[3]{\inc{#1_1}{#2_1}\cld\inc{#1_{#3}}{#2_{#3}}}
                                % U1:E1,...,Uk:Ek
                                % 1  2       3
\newcommand{\tuple}[3]{[\lablist{#1}{#2}{#3}]}
                                % [U1:E1,...Uk:Ek]
                                %  1  2      3

%%%%%%%%%%%%%%%%%%%%%%%%%% General

\newcommand{\size}[1]{|#1|}
\newcommand{\Schema}{(\A,\P,\T)}

%%%%%%%%%%%%%%%%%%%%%%%%%% Language Operators

\newcommand{\EATLEAST}[2]{\exists^{\geqt #1} #2}
\newcommand{\EATMOST}[2]{\exists^{\leqt #1} #2}
\newcommand{\EEXACTLY}[2]{\exists^{= #1} #2}
\newcommand{\INV}[1]{#1^{-}}

%%%%%%%%%%%%%%%%%%%%%%%%%% Reasoning Services

\newcommand{\cons}[2][]{#2 \not\models_{#1}}
\newcommand{\classcons}[3][]{#2 \not\models_{#1} #3 \preceq\bot}
\newcommand{\subs}[4][]{#2 \models_{#1} #3 \preceq #4}
%%\newcommand{\equival}[4][]{#2 \models_{#1} #3 \equiv #4}

\newcommand{\notcons}[2][]{#2 \models_{#1}}
\newcommand{\notclasscons}[3][]{#2 \models_{#1} #3 \preceq\bot}
\newcommand{\notsubs}[4][]{#2 \not\models_{#1} #3 \preceq #4}
%%\newcommand{\notequival}[4][]{#2 \not\models_{#1} #3 \equiv #4}

%%%%%%%%%%%%%%%%%%%%%%%%%% Mapping from frame based systems

\newcommand{\Frame}[2]{\textbf{Frame}:~#1~\textbf{in KB}~#2~~~}
\newcommand{\Subclasses}{\textbf{SubClasses}:~}
\newcommand{\Superclasses}{\textbf{SuperClasses}:~}
\newcommand{\Slot}{\textbf{MemberSlot}:~}
\newcommand{\Value}{\textbf{ValueClass}:~}
\newcommand{\Cardmin}{\textbf{Cardinality.Min}:~}
\newcommand{\Cardmax}{\textbf{Cardinality.Max}:~}

\newcommand{\KEEinter}[2]{(\textrm{INTERSECTION} ~ #1 ~ #2)}
\newcommand{\KEEunion}[2]{(\textrm{UNION} ~ #1 ~ #2)}
\newcommand{\KEEneg}[1]{(\textrm{NOT} ~ #1)}          

\newcommand{\KEEmaprel}{\theta}            % mapping from frames to LUNI
\newcommand{\KEEmap}[1]{\KEEmaprel(#1)}    % mapping from frames to LUNI

%%%%%%%%%%%%%%%%%%%%%%%%%% Mapping from ER-model

\newcommand{\ERschema}[1][\S]{(\L_{#1},{\ERisa[#1]},\ERatt[#1],
                               \ERrel[#1],\ERccon[#1])}

\newcommand{\LS}{\L_\S}
\newcommand{\ES}{\E_\S}
\newcommand{\AS}{\A_\S}
\newcommand{\US}{\U_\S}
\newcommand{\RS}{\R_\S}
\newcommand{\DS}{\D_\S}

\newcommand{\ERisa}[1][\S]{\mathrel{\preceq_{#1}}}	        % <=
\newcommand{\ERisat}[1][\S]{\mathrel{\preceq^{\ast}_{#1}}}	% <=*
\newcommand{\ERatt}[1][\S]{\mathit{att}_{#1}}	                % att_S
\newcommand{\ERrel}[1][\S]{\mathit{rel}_{#1}}	                % rel_S
\newcommand{\ERccon}[1][\S]{\mathit{card}_{#1}}	                % card_S
\newcommand{\ERcmin}[1][\S]{\mathit{cmin}_{#1}}	                % cmin_S
\newcommand{\ERcmax}[1][\S]{\mathit{cmax}_{#1}}	                % cmax_S

\newcommand{\Nat}{{\rm I\kern-.23em N}}         % Natural numbers

\newcommand{\BD}{{\B_\D}}
\newcommand{\IntB}[1]{\Int[\B]{#1}}
\newcommand{\domB}{\dom[\B]}
\newcommand{\DactB}{\domB_{\mathit{act}}}

\newcommand{\Integer}{\texttt{Integer}}
\newcommand{\String}{\texttt{String}}
\newcommand{\Boolean}{\texttt{Boolean}}

\newcommand{\INTEGER}{\textbf{I}}
\newcommand{\STRING}{\textbf{S}}
\newcommand{\BOOLEAN}{\textbf{B}}

\newcommand{\ERmaprel}{\phi}	        % mapping from ER to ALUNI
\newcommand{\ERmap}[1]{\ERmaprel(#1)}	% mapping from ER to ALUNI
\newcommand{\ERS}{\ERmap{\S}}      % ALUNI-schema corresponding to an ER-schema

\newcommand{\Conf}{\mathit{Conf}}

\newcommand{\alphaS}{\alpha_\S}
\newcommand{\betaS}{\beta_\S}
\newcommand{\betaD}{\beta_{\Delta}}

%%%%%%%%%%%%%%%%%%%%%%%%%% Mapping from OO-model

\newcommand{\OOschema}[1][\S]{(\C_{#1},\A_{#1},\D_{#1})}

\newcommand{\CS}{\C_\S}
%% \newcommand{\AS}{\A_\S}
%% \newcommand{\DS}{\D_\S}

\newcommand{\OOclass}{\underline{\textrm{Class}}}
\newcommand{\OOisa}{\underline{\textrm{is-a}}}
\newcommand{\OOtypeis}{\underline{\textrm{type-is}}}
\newcommand{\OOrecord}{\underline{\textrm{Record}}}
\newcommand{\OOsetof}{\underline{\textrm{Set-of}}}
\newcommand{\OOunion}{\underline{\textrm{Union}}}
\newcommand{\OOend}{\underline{\textrm{End}}}

\newcommand{\Tisa}[3]{\OOclass\ #1\ \OOisa\ #2\ \OOtypeis\ #3}
\newcommand{\Tunion}[2]{\OOunion\ \dd{#1}{#2}\ \OOend}
\newcommand{\Trecord}[3]{\OOrecord\ \lablist{#1}{#2}{#3}\ \OOend} 
\newcommand{\Tset}[1]{\OOsetof\ #1}

\newcommand{\OOset}[1]{\mathopen{\{\mkern-3mu |} #1 \mathclose{|\mkern-3mu \}}}
\newcommand{\OOtup}[1]{\mathopen{[\mkern-2mu [} #1 \mathclose{]\mkern-2mu ]}}
\newcommand{\OOtuple}[3]{\OOtup{\lablist{#1}{#2}{#3}}}
                                % [U1:E1,...Uk:Ek]
                                %  1  2      3

\newcommand{\VO}{\V_\O}

\newcommand{\Oid}[1][\J]{\O^{#1}}  % O^J  (domain of interpretation \J)
\newcommand{\Values}{\V_{\O^{\J}}}
\newcommand{\Vact}[1][\J]{\V_{#1}}

\newcommand{\IntJ}[1]{\Int[\J]{#1}}

\newcommand{\piJ}{\pi^{\J}}
\newcommand{\rhoJ}{\rho^{\J}}

\newcommand{\AbstractClass}{\texttt{AbstractClass}}
\newcommand{\RecType}{\texttt{RecType}}
\newcommand{\SetType}{\texttt{SetType}}

\newcommand{\OOmember}{\texttt{member}}
\newcommand{\OOvalue}{\texttt{value}}

\newcommand{\OOmaprel}{\psi}	        % mapping from OO to ALUNI
\newcommand{\OOmap}[1]{\OOmaprel(#1)}	% mapping from OO to ALUNI
\newcommand{\OOS}{\OOmap{\S}}      % ALUNI-schema corresponding to an OO-schema

\newcommand{\depth}{\mathit{depth}}

\newcommand{\alphaV}{\alpha_{\V}}
\newcommand{\betaV}{\beta_{\V}}

\newcommand{\domm}{\dom[\I_{|m}]}
\newcommand{\Intm}[1]{\Int[\I_{|m}]{#1}}
\newcommand{\INTm}[1]{\INT[\I_{|m}]{#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%\input{macros-e}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%% Introduction

\newcommand{\Male}{\texttt{Male}}
\newcommand{\Person}{\texttt{Person}}
\newcommand{\child}{\texttt{child}}

%%%%%%%%%%%%%%%%%%%%%%%%%% ALUNI

\newcommand{\AdvCourse}{\texttt{AdvCourse}}
\newcommand{\Professor}{\texttt{Professor}}
\newcommand{\Student}{\texttt{Student}}
\newcommand{\GradStud}{\texttt{GradStudent}}
\newcommand{\teaches}{\texttt{teaches}}
\newcommand{\enrolls}{\texttt{enrolls}}

%%%%%%%%%%%%%%%%%%%%%%%%%% ALUNI - reasoning

\newcommand{\FirstGuard}{\texttt{FirstGuard}}
\newcommand{\Guard}{\texttt{Guard}}
\newcommand{\shields}{\texttt{shields}}

\newcommand{\Keven}{\K_\mathit{even}}
\newcommand{\Number}{\texttt{Number}}
\newcommand{\Even}{\texttt{Even}}
\newcommand{\doubles}{\texttt{doubles}}

%%%%%%%%%%%%%%%%%%%%%%%%%% Correspondence

\newcommand{\University}{\texttt{University}}
\newcommand{\Teacher}{\texttt{Teacher}}
\newcommand{\Undergrad}{\texttt{Undergrad}}
\newcommand{\Course}{\texttt{Course}}
\newcommand{\BasCourse}{\texttt{BasCourse}}
\newcommand{\taughtby}{\texttt{taughtby}}
\newcommand{\degree}{\texttt{degree}}

\newcommand{\TEACHING}{\texttt{TEACHING}}
\newcommand{\ENROLLING}{\texttt{ENROLLING}}
\newcommand{\Tof}{\texttt{Tof}}
\newcommand{\Tby}{\texttt{Tby}}
\newcommand{\Ein}{\texttt{Ein}}
\newcommand{\Eof}{\texttt{Eof}}

\newcommand{\Setstud}{\texttt{SetStud}}

\newcommand{\DOUBLES}{\texttt{DOUBLES}}

%%%%%%%%%%%%%%%%%%%%%%%%%% Unrestricted model reasoning

\newcommand{\Root}{\texttt{Root}}
\newcommand{\OtherNode}{\texttt{OtherNode}}
\newcommand{\Node}{\texttt{Node}}
\newcommand{\RootOrNode}{\texttt{RootOrNode}}
\newcommand{\edge}{\texttt{edge}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

\sloppy
\maketitle

\begin{abstract}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%\input{0-abstract}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
The notion of class is ubiquitous in computer science and is central in many
formalisms for the representation of structured knowledge used both in
knowledge representation and in databases.  In this paper we study the basic
issues underlying such representation formalisms and single out both their
common characteristics and their distinguishing features.  Such investigation
leads us to propose a unifying framework in which we are able to capture the
fundamental aspects of several representation languages used in different
contexts.  The proposed formalism is expressed in the style of description
logics, which have been introduced in knowledge representation as a means to
provide a semantically well-founded basis for the structural aspects of
knowledge representation systems. The description logic considered in this
paper is a subset of first order logic with nice computational characteristics.
It is quite expressive and features a novel combination of constructs that has
not been studied before.  The distinguishing constructs are number
restrictions, which generalize existence and functional dependencies, inverse
roles, which allow one to refer to the inverse of a relationship, and possibly
cyclic assertions, which are necessary for capturing real world domains.  We
are able to show that it is precisely such combination of constructs that makes
our logic powerful enough to model the essential set of features for defining
class structures that are common to frame systems, object-oriented database
languages, and semantic data models.  As a consequence of the established
correspondences, several significant extensions of each of the above formalisms
become available. The high expressiveness of the logic we propose and the need
for capturing the reasoning in different contexts forces us to distinguish
between unrestricted and finite model reasoning.  A notable feature of our
proposal is that reasoning in both cases is decidable.  We argue that, by
virtue of the high expressive power and of the associated reasoning
capabilities on both unrestricted and finite models, our logic provides a
common core for class-based representation formalisms.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{abstract}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%\input{1-introduction}
\section{Introduction}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

In many fields of computer science we find formalisms for the representation of
objects and classes \cite{MoMy92}. Generally speaking, an object denotes an
element of the domain of interest, and a \emph{class} denotes a set of objects
with common characteristics. We use the term ``class-based representation
formalism'' to refer to a formalism that allows one to express several kinds of
relationships and constraints (e.g., subclass constraints) holding among the
classes that are meaningful in a set of applications. Moreover, class-based
formalisms aim at taking advantage of the class structure in order to provide
various information, such as whether a class is consistent, i.e., it admits at
least one object, whether a class is a subclass of another class, and more
generally, whether a given constraint holds between a given set of classes.
From the above characterization, it should be clear that the formalisms
referred to in this paper deal only with the structural aspects of objects and
classes, and do not include any features for the specification of behavioral
properties of objects.

Three main families of class-based formalisms are identified in this paper.
The first one comes from knowledge representation and in particular from the
work on semantic networks and frames \cite<see for example>{Lehm92,Sowa91}.
The second one originates in the field of databases and in particular from the
work on semantic data models \cite<see for example>{HuKi87}. The third one
arises from the work on types in programming languages and object-oriented
systems \cite<see for example>{KiLo89}.

In the past there have been several attempts to establish relationships among
the various families of class-based formalisms (see Section~\ref{sec-related}
for a brief survey).  The proposed solutions are not fully general and a
formalism capturing both the modeling constructs and the reasoning techniques
for all the above families is still missing. In this paper we address this
problem by proposing a class-based representation formalism, based on
description logics \cite{BrLe84,ScSm91,DLNS96}, and by using it for comparing
other formalisms.

In description logics, structured knowledge is described by means of so called
\emph{concepts} and \emph{roles}, which denote unary and binary predicates,
respectively. Starting from a set of atomic symbols one can build complex
concept and role expressions by applying suitable constructors which
characterize a description logic.  Formally, concepts are interpreted as
subsets of a domain and roles as binary relations over that domain, and all
constructs are equipped with a precise set-theoretic semantics.  The most
common constructs include boolean operations on concepts, and quantification
over roles. For example, the concept $\Person\AND\ALL{\child}{\Male}$, denotes
the set of individuals that are instances of the concept $\Person$ and are
connected through the role $\child$ only to instances of the concept $\Male$,
while the concept $\SOMET{\child}$ denotes all individuals that are connected
through the role $\child$ to some individual. Further constructs that have been
considered important include more general forms of quantification, number
restrictions, which allow one to state limits on the number of connections that
an individual may have via a certain role, and constructs on roles, such as
intersection, concatenation and inverse.
%%
A description logic knowledge base, expressing the intensional knowledge about
the modeled domain, is built by stating inclusion assertions between concepts,
which have to be satisfied by the models of the knowledge base.  The assertions
are used to specify necessary and/or necessary and sufficient conditions for
individuals to be instances of certain concepts.
%%
Reasoning on such knowledge bases includes the detection of inconsistencies in
the knowledge base itself, determining whether a concept can be populated in a
model of the knowledge base, and checking subsumption, i.e., whether all
instances of a concept are necessarily also instances of another concept in all
models of the knowledge base.

In this paper we propose a description logic called \aluni, which is quite
expressive and includes a novel combination of constructs, including number
restrictions, inverse roles, and inclusion assertions with no restrictions on
cycles. Such features make \aluni\ powerful enough to provide a unified
framework for frame systems, object-oriented languages, and semantic data
models.  We show this by establishing a precise correspondence with a
frame-based language in the style of the one proposed by \citeA{FiKe85}, with
the Entity-Relationship model \cite{Chen76}, and with an object-oriented
language in the style of the one introduced by \citeA{AbKa89}.  More
specifically, we identify the most relevant features to model classes in each
of the cited settings and show that a specification in any of those class-based
formalisms can be equivalently expressed as a knowledge base in \aluni.  In
this way, we are able to identify which are the commonalities among the
families and which are the specificities of each family.  Therefore, even
though there are specific features of every family that are not addressed by
\aluni, we are able to show that the formalism proposed in this paper provides
important features that are currently missing in each family, although their
relevance has often been stressed.  In this sense, our unifying framework
points out possible developments for the languages belonging to all the three
families.

One fundamental reason for regarding \aluni\ as a unifying framework for
class-based representation formalisms is that reasoning in \aluni\ is hard, but
nonetheless decidable, as shown by \citeA{CaLN94,Calv96}.  Consequently, the
language features arising from different frameworks to build class-based
representations are not just given a common semantic account, but are combined
in a more expressive setting where one retains the capability of solving
reasoning tasks.  The combination of constructs included in the language makes
it necessary to distinguish between reasoning with respect to finite models,
i.e., models with a finite domain, and reasoning with respect to unrestricted
models. \citeA{Calv96} devises suitable techniques for both unrestricted and
finite model reasoning, that enable for reasoning in the different contexts
arising from assuming a finite domain, as it is often the case in the field of
databases, or assuming that a domain can also be infinite.  In the paper, we
discuss the results on reasoning in \aluni, and compare them with other results
on reasoning in class-based representation formalisms.

Summarizing, our framework provides an adequate expressive power to account for
the most significant features of the major families of class-based formalisms.
Moreover, it is equipped with suitable techniques for reasoning in both finite
and unrestricted models. Therefore, we believe that \aluni\ captures the
essential core of the class-based representation formalisms belonging to all
three families mentioned above.

The paper is organized as follows.  In the next section we present our
formalism and in Sections~\ref{sec-frames},~\ref{sec-sdm}, and~\ref{sec-oom} we
discuss three families of class-based formalisms, namely, frame languages,
semantic data models, and object-oriented data models, showing that their basic
features are captured by knowledge bases in \aluni. The final sections contain
a review of related work, including a discussion of reasoning in \aluni\ and
class-based formalism, and some concluding remarks.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%\input{2-ALUNI}
\section{A Unifying Class-Based Representation Language}
\label{sec-ALUNI}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

In this section, we present \aluni, a class-based formalism in the style of
\emph{description logics} (DLs) \cite{BrLe84,ScSm91,DLNS96,DLNN97}.  In DLs the
domain of interest is modeled by means of \emph{concepts} and \emph{roles},
which denote classes and binary relations, respectively.  Generally speaking, a
DL is formed by three basic components:
\begin{itemize}
\item A \emph{description language}, which specifies how to construct complex
  concept and role expressions (also called simply concepts and roles), by
  starting from a set of atomic symbols and by applying suitable constructors.
  It is the set of allowed constructs that characterizes the description
  language.
\item A \emph{knowledge specification mechanism}, which specifies how to
  construct a DL knowledge base, in which properties of concepts and roles
  are asserted.
\item A set of \emph{basic reasoning tasks} provided by the DL.
\end{itemize}
In the rest of the section we describe the specific form that these three
components assume in \aluni.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{The Description Language of \aluni}
\label{sec-ALUNI-language}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{table}[tb]
  \centering
  %%\hspace*{-1cm}
  \renewcommand{\arraystretch}{1.2}
  \begin{tabular}{||l|c|c||} \hline\hline
    \textbf{Construct} & \textbf{Syntax} & \textbf{Semantics}\\ \hline\hline
    atomic concept  & $A$           & $\Int{A}\incl\dom$\\ \hline
    atomic negation & $\NOT A$      & $\dom\setminus\Int{A}$\\ \hline
    conjunction     & $C_1\AND C_2$ & $\Int{C_1}\cap\Int{C_2}$\\ \hline
    disjunction     & $C_1\OR C_2$  & $\Int{C_1}\cup\Int{C_2}$\\ \hline
    universal quantification & $\ALL{R}{C}$ & $\set{o \mid
     \forall o'\suchthat (o,o')\in\Int{R} \imp o'\in\Int{C}}$\\ \hline
    number restrictions & $\EATLEAST{n}{R}$ & $\set{o \mid
     \cards{\set{o'\mid (o,o')\in\Int{R}} \geq n}}$\footnotemark\\ \cline{2-3}
                        & $\EATMOST{n}{R}$  & $\set{o \mid
     \cards{\set{o'\mid (o,o')\in\Int{R}} \leq n}}$\\ \hline\hline
    atomic role  & $P$       & $\Int{P}\incl\dom\x\dom$\\ \hline
    inverse role & $\Inv{P}$ & $\set{(o,o')\mid(o',o)\in\Int{P}}$\\\hline\hline
  \end{tabular}
  \caption{Syntax and semantics of $\ALUNI$}
  \label{tab-ALUNI}
\end{table}
\footnotetext{$\cards{S}$ denotes the cardinality of a set $S$.}

In the description language of \aluni, called $\ALUNI$, \emph{concepts} and
\emph{roles} are formed according to the syntax shown in Table~\ref{tab-ALUNI},
where $A$ denotes an atomic concept, $P$ an atomic role, $C$ an arbitrary
concept expression, $R$ an arbitrary role expression, and $n$ a nonnegative
integer.
%%
To increase readability of concept expressions, we also introduce the following
abbreviations:
\begin{eqnarray*}
  \top      &\equiv& A\OR\NOT A,  \quad\textrm{for some atomic concept } A\\
  \bot      &\equiv& A\AND\NOT A, \quad\textrm{for some atomic concept } A\\
  \SOMET{R} &\equiv& \EATLEAST{1}{R}\\
  \EEXACTLY{n}{R} &\equiv& \EATMOST{n}{R}\AND\EATLEAST{n}{R}
\end{eqnarray*}

Concepts are interpreted as subsets of a domain and roles as binary relations
over that domain.  Intuitively, $\NOT A$ represents the \emph{negation} of an
atomic concept, and is interpreted as the complement with respect to the domain
of interpretation.  $C_1\AND C_2$ represents the \emph{conjunction} of two
concepts and is interpreted as set intersection, while $C_1\OR C_2$ represents
\emph{disjunction} and is interpreted as set union.  Consequently, $\top$
represents the whole domain, and $\bot$ the empty set.  $\ALLRC$ is called
\emph{universal quantification over roles} and is used to denote those elements
of the interpretation domain that are connected through role $R$ only to
instances of the concept $C$. $\EATLEAST{n}{R}$ and $\EATMOST{n}{R}$ are called
\emph{number restrictions}, and impose on their instances restrictions on the
minimum and maximum number of objects they are connected to through role $R$.
$\Inv{P}$, called the \emph{inverse} of role $P$, represents the inverse of the
binary relation denoted by $P$.

More formally, an interpretation $\I\defas\inter$ consists of an
\emph{interpretation domain} $\dom$ and an \emph{interpretation
 function}~$\Int{\cdot}$ that maps every concept $C$ to a subset $\Int{C}$ of
$\dom$ and every role $R$ to a subset $\Int{R}$ of $\dom\x\dom$ according to
the semantic rules specified in Table~\ref{tab-ALUNI}.  The sets $\Int{C}$ and
$\Int{R}$ are called the \emph{extensions} of $C$ and $R$ respectively.

\begin{example} \label{example-ALUNI}
Consider the concept expression
\[
  \begin{array}[t]{@{}l}
    \ALL{\enrolls}{\Student} \AND
    \EATLEAST{2}{\enrolls} \AND \EATMOST{30}{\enrolls} \AND{}\\
    \ALL{\Inv{\teaches}}{(\Professor\OR\GradStud)} \AND
    \EEXACTLY{1}{\Inv{\teaches}} \AND{}\\
    \NOT\AdvCourse
  \end{array}
\]
specifying the constraints for an object to be a university course. The
expression reflects the fact that each course enrolls only students, and
restrictions on the minimum and maximum number of enrolled students.  By
using the role \teaches\ and the inverse constructor we can state the
property that each course is taught by exactly one individual, who is either
a professor or a graduate student.  Finally, negation is used to express
disjointness from the concept denoting advanced courses.
%%
\endmarkfull
\end{example}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Knowledge Bases in \aluni}
\label{sec-ALUNI-kbs}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

An \aluni\ \emph{\kb}, which expresses the knowledge about classes and
relations of the modeled domain, is formally defined as a triple
$\K\defas\Schema$, where $\A$ is a finite set of atomic concepts, $\P$ is a
finite set of atomic roles, and $\T$ is a finite set of so called
\emph{inclusion assertions}.  Each such assertion has the form
\[A \ISAs C\]
where $A$ is an atomic concept and $C$ an arbitrary concept expression.  Such
an inclusion assertion states by means of the concept $C$ necessary properties
for an element of the domain in order to be an instance of the atomic concept
$A$.  Formally, an interpretation $\I$ \emph{satisfies} the inclusion assertion
$A \ISA C$ if $\Int{A}\incl\Int{C}$.  An interpretation $\I$ is a \emph{model}
of a \kb\ $\K$ if it satisfies all inclusion assertions in $\K$.  A
\emph{finite model} is a model with finite domain.

\begin{exampleCont}{\ref{example-ALUNI}}
The assertion
\[\Course ~\ISA~ \begin{array}[t]{@{}l}
                   \ALL{\enrolls}{\Student} \AND
                   \EATLEAST{2}{\enrolls} \AND
                   \EATMOST{30}{\enrolls} \AND{} \\
                   \ALL{\Inv{\teaches}}{(\Professor \OR \GradStud)} \AND
                   \EEXACTLY{1}{\Inv{\teaches}}
                 \end{array}
\]
makes use of a complex concept expression to state necessary conditions for an
object to be an instance of the concept \Course.
%%
\endmarkfull
\end{exampleCont}

In \aluni\ no restrictions are imposed on the form that the inclusion
assertions may assume.  In particular we do not rule out \emph{cyclic
 assertions}, i.e., assertions in which the concept expression on the right
hand side refers, either directly or indirectly via other assertions, to the
atomic concept on the left hand side.  In the presence of cyclic assertions
different semantics may be adopted \cite{Nebe91}.  The one defined above,
called \emph{descriptive semantics}, accepts all interpretations that satisfy
the assertions in the knowledge base, and hence interprets assertions as
constraints on the domain to be modeled.  For inclusion assertions, descriptive
semantics has been claimed to provide the most intuitive results \cite{BDNS98}.
Alternative semantics which have been proposed are based on fixpoint
constructions \cite{Nebe91,Schi94,DeLe94b}, and hence allow to define in a
unique way the interpretation of concepts.

In general, cycles in the knowledge base increase the complexity of reasoning
\cite{Nebe91,Baad96b,Calv96c} and require a special treatment by reasoning
procedures \cite{Baad91,BuDS93c}.  For this reason, many DL based systems
assume the knowledge base to be acyclic \cite{BMPAB91,BrFT95}.  However, this
assumption is unrealistic in practice, and cycles are definitely necessary for
a correct modeling in many application domains.  Indeed, the use of cycles is
allowed in all data models used in databases, and, as shown in the following
sections, in order to capture their semantics in \aluni\ the possibility of
using cyclic assertions is fundamental.

Besides inclusion assertions, some DL based systems also make use of
equivalence assertions \cite{BuDS93c}, which express both necessary and
sufficient conditions for an object to be an instance of a concept.  Although
this possibility is ruled out in \aluni, this does not limit its ability of
capturing both frame based systems and database models, where the constraints
that can be expressed correspond naturally to inclusion assertions.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Reasoning in \aluni}
\label{sec-ALUNI-reasoning}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

The basic tasks we consider when reasoning over an \aluni\ \kb\ are
concept consistency and concept subsumption:
\begin{itemize}
\item \emph{Concept consistency} is the problem of deciding whether a concept
  $C$ is \emph{consistent} in a \kb\ $\K$ (written as $\classcons{\K}{C}$),
  i.e., whether $\K$ admits a model $\I$ such that $\Int{C}\neq\eset$.
\item \emph{Concept subsumption} is the problem of deciding whether a concept
  $C_1$ \emph{is subsumed by} a concept $C_2$ in a \kb\ $\K$ (written as
  $\subs{\K}{C_1}{C_2}$), i.e., whether $\Int{C_1}\incl\Int{C_2}$ for each
  model $\I$ of $\K$.
\end{itemize}

The inclusion of number restrictions and inverse roles in $\ALUNI$ and the
ability in \aluni\ of using arbitrary, possibly cyclic inclusion assertions
allows one to construct a \kb\ in which a certain concept is consistent but has
necessarily an empty extension in all finite models of the \kb.  Similarly, a
subsumption relation between two concepts may hold only if infinite models of
the \kb\ are ruled out and only finite models are considered.

\begin{figure}[tb!]
  \boxtext{\small
   \vspace{-\abovedisplayskip}
   \begin{tabbing}
     $\Keven$\=$\A$ \=\kill
     $\Keven\defas\Schema$, where\\[1mm]
     \>$\A$ \> $\defas\{$\=$\Number,\Even\}$,\\[1mm]
     \>$\P$ \> $\defas\{$\>$\doubles\}$,\\[1mm]
     \>and the set $\T$ of assertions consists of:
   \end{tabbing}
   \vspace*{-\abovedisplayskip}
   \begin{eqnarray*}
     \Number &\ISA& \SOMET{\Inv{\doubles}} \AND
                    \ALL{\Inv{\doubles}}{\Even}\\
     \Even   &\ISA& \Number \AND \EATMOST{1}{\doubles} \AND
                    \ALL{\doubles}{\Number}
   \end{eqnarray*}
   \par\vspace{-\belowdisplayshortskip}
   }
  \caption{An \aluni\ \kb\ with two concepts that are equivalent in all finite
   models}
  \label{fig-example-finite-unrestricted-even}
\end{figure}

\begin{example} \label{example-finite-unrestricted-even}
Let $\Keven$ be the \kb\ shown in
Figure~\ref{fig-example-finite-unrestricted-even}.  Intuitively, the assertions
in $\Keven$ state that for each number there is an even number which doubles
it, and that all numbers which double it are even.  Each even number is a
number, doubles at most one number, and doubles only numbers.  Observe that for
any model $\I$ of $\Keven$, the universal quantifications together with the
functionality of \doubles\ in the assertions imply that
$\cards{\Int{\Even}}\geq\cards{\Int{\Number}}$, while the direct inclusion
assertion between \Even\ and \Number\ implies that
$\cards{\Int{\Even}}\leq\cards{\Int{\Number}}$.  Therefore, the two concepts
have the same cardinality, and since one is a sub-concept of the other, if the
domain is finite, their extensions coincide.  This does not necessarily hold
for infinite domains.  In fact, the names we have chosen suggest already an
infinite model of the \kb\ in which \Number\ and \Even\ are interpreted
differently.  The model is obtained by taking the natural numbers as domain,
and interpreting \Number\ as the whole domain, \Even\ as the even numbers, and
\doubles\ as the set $\set{(2n,n) \mid n\geq 0}$.
\endmarkfull
\end{example}

The example above shows that \aluni\ does not have the \emph{finite model
 property}, which states that if a concept is consistent in a knowledge base
then the knowledge base admits a \emph{finite} model in which the concept has a
nonempty extension.  Therefore, it is important to distinguish between
reasoning with respect to unrestricted models and reasoning with respect to
finite models.  We call \emph{(unrestricted) concept consistency} (written as
$\classcons[u]{\K}{C}$) and \emph{(unrestricted) concept subsumption} (written
as $\subs[u]{\K}{A}{C}$) the reasoning tasks as described above, i.e., carried
out without restricting the attention to finite models.  The corresponding
reasoning tasks carried out by considering finite models only, are called
\emph{finite concept consistency} (written as $\classcons[f]{\K}{C}$) and
\emph{finite concept subsumption} (written as $\subs[f]{\K}{A}{C}$).

\begin{exampleCont}{\ref{example-finite-unrestricted-even}}
Summing up the previous considerations, we can say that $\Number$ is not
subsumed by $\Even$ in $\Keven$, i.e., $\notsubs[u]{\Keven}{\Number}{\Even}$,
but is finitely subsumed, i.e., $\subs[f]{\Keven}{\Number}{\Even}$.
Equivalently $\Number\AND\NOT\Even$ is consistent in $\Keven$,
i.e., $\classcons[u]{\Keven}{\Number\AND\NOT\Even}$, but is not finitely
consistent, i.e., $\notclasscons[f]{\Keven}{\Number\AND\NOT\Even}$.
\endmarkfull
\end{exampleCont}

A distinguishing feature of \aluni\ is that reasoning both in the finite and in
the unrestricted case is decidable.  In particular, unrestricted concept
satisfiability and concept subsumption are decidable in deterministic
exponential time \cite{DeLe94,CaLN94}, and since reasoning in strict
sublanguages of \aluni\ is already EXPTIME-hard \cite{Calv96}, the known
algorithms are computationally optimal.  Finite concept consistency in \aluni\ 
is also decidable in deterministic exponential time while finite concept
subsumption (in the general case) is decidable in deterministic double
exponential time \cite{Calv96}.  A more precise discussion on the methods for
reasoning in \aluni\ is provided in Section~\ref{sec-reasoning}, while a
detailed account of the adopted algorithms and an analysis of their
computational complexity is presented by \citeA{Calv96}.

In the next sections we show how the two forms of reasoning with respect to
unrestricted and finite models, capture the reasoning tasks that are typically
considered in different formalisms for the structured representation of
knowledge.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%\input{3-frames}
\section{Frame Based Systems}
\label{sec-frames}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Frame languages are based on the idea of expressing knowledge by means of
\emph{frames}, which are structures representing classes of objects in terms of
the properties that their instances must satisfy. Such properties are defined
by the frame \emph{slots}, that constitute the items of a frame definition.
Since the 70s a large number of frame systems have been developed, with
different goals and different features.  DLs bear a close relationship with the
\klone\ family of frame systems \cite{WoSc92}.  However, here we would like to
consider frame systems from a more general perspective, as discussed for
example by \citeA{Karp92,KaMG95}, and establish the correspondence with \aluni\
knowledge bases in this context.

We remark that we are restricting our attention to those aspects that are
related to the taxonomic structure.  Moreover, as discussed below, we consider
assertional knowledge bases, where intensional knowledge is characterized in
terms of inclusion assertions rather than definitions.  In addition, we do not
consider those features that cannot be captured in a first-order framework,
such as default values in the slots, attached procedures, and the specification
of overriding inheritance policies. Some of the issues concerning the modeling
of these aspects in DLs are addressed by \citeA{DLNNS94,DoNR95}, within a modal
nonmonotonic extension of DLs.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Syntax of Frame Based Systems}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

To make the correspondence precise, we need to fix syntax and semantics for the
frame systems we consider. Unfortunately, there is no accepted standard and we
have chosen to use here basically the notation adopted by \citeA{FiKe85}, which
is used also in the KEE%
\footnote{KEE is a trademark of Intellicorp. Note that a KEE user does not
 directly specify her \kb\ in this notation, but is allowed to define frames
 interactively via the graphical system interface.} %
system.

\begin{definition} \label{def-frames-syntax}
  A \emph{frame \kb}, denoted by $\F$, is formed by a set of \emph{frame} and
  \emph{slot names}, and is constituted by a set of \emph{frame definitions} of
  the following form:
  \[\Frame{F}{\F} E,\]
  where $E$ is a \emph{frame expression}, i.e., an expression formed according
  to the following syntax:
  \[E ~\lora~\begin{array}[t]{@{}l}
               \Superclasses \dd{F}{h}\\
               \Slot S_1 \\
               ~~~\Value H_1\\
               ~~~\Cardmin m_1\\
               ~~~\Cardmax n_1\\
               \cdots\\
               \Slot S_k \\
               ~~~\Value H_k\\
               ~~~\Cardmin m_k\\
               ~~~\Cardmax n_k
             \end{array}
  \]
  $F$ and $S$ denote frame and slot names, respectively, $m$ and $n$ denote
  positive integers, and $H$ denotes \emph{slot constraint}, which can be
  specified as follows:
  \[H ~\lora~ \begin{array}[t]{@{}l}
                F \mid\\
                \KEEinter{H_1}{H_2}  \mid \\
                \KEEunion{H_1}{H_2} \mid \\
                \KEEneg H
              \end{array}
  \]
  
  \vspace{-\abovedisplayskip} %
  \endmarkfull
\end{definition}

For readers that are familiar with the KEE system, we point out that we omit
the specification of the sub-classes for a frame present in KEE, since it can
be directly derived from the specification of the super-classes.

\begin{figure}[tb!]
  \boxtext{\small
   %% \hspace*{\stretch{0.2}}
   \begin{minipage}[t]{6cm}
     \begin{tabbing}
       xx\=xx\= \kill
       \Frame{\Course}{\University} \\
       %%\> \Superclasses \\
       %%\> \Subclasses \AdvCourse, \BasCourse \\
       \> \Slot \enrolls \\
       \> \> \Value \Student \\
       \> \> \Cardmin 2 \\
       \> \> \Cardmax 30 \\
       \> \Slot \taughtby \\
       \> \> \Value (UNION \=\GradStud \\
       \> \>               \>\Professor) \\
       \> \> \Cardmin 1 \\
       \> \> \Cardmax 1 \\[3mm]
       \Frame{\AdvCourse}{\University} \\
       \> \Superclasses \Course \\
       %%\> \Subclasses \\
       \> \Slot \enrolls \\
       \> \> \Value (\=INTERSECTION\\
       \> \>         \>\GradStud \\
       \> \>         \>(NOT \Undergrad)) \\
       \> \> \Cardmax 20
     \end{tabbing}
   \end{minipage}
   \hspace{5mm}
   \begin{minipage}[t]{6cm}
     \begin{tabbing}
       xx\=xx\= \kill
       \Frame{\BasCourse}{\University} \\
       \> \Superclasses \Course \\
       %%\> \Subclasses \\
       \> \Slot \taughtby \\
       \> \> \Value \= \Professor\ \\[3mm]
       \Frame{\Professor}{\University} \\[3mm]
       %%\> \Superclasses \\
       %%\> \Subclasses
       \Frame{\Student}{\University} \\[3mm]
       %%\> \Superclasses \\
       %%\> \Subclasses \GradStud, \Undergrad \\[3mm]
       \Frame{\GradStud}{\University} \\
       \> \Superclasses \Student \\
       %%\> \Subclasses \\
       \> \Slot \degree \\
       \> \> \Value \String \\
       \> \> \Cardmin 1 \\
       \> \> \Cardmax 1 \\[3mm]
       \Frame{\Undergrad}{\University} \\
       \> \Superclasses \Student
       %%\> \Subclasses
     \end{tabbing}
   \end{minipage}
   %% \hspace*{\stretch{0.2}}
   } %\end boxtext
  \caption{A KEE \kb}
  \label{fig-frames-example}
\end{figure}

\begin{example} \label{example-frames-KEE-kb}
Figure~\ref{fig-frames-example} shows a simple example of a \kb\ modeling the
situation at an university expressed in the frame language we have presented.
The frame \Course\ represents courses which enroll students and are taught
either by graduate students or professors. Cardinality restrictions are used to
impose a minimum and maximum number of students that may be enrolled in a
course, and to express that each course is taught by exactly one individual.
The frame \AdvCourse\ represents courses which enroll only graduate students,
i.e., students who already have a degree. Basic courses, on the other hand, may
be taught only by professors.
%%
\endmarkfull
\end{example}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Semantics of Frame Based Systems}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

To give semantics to a set of frame definitions we resort to their
interpretation in terms of first-order predicate calculus \cite{Haye79}.
According to such interpretation, frame names are treated as unary predicates,
while slots are considered binary predicates.

A frame expression $E$ is interpreted as a predicate logic formula $E(x)$,
which has one free variable, and consists of the conjunction of sentences,
obtained from the super-class specification and from each slot specification.
In particular, for the super-classes $\dd{F}{h}$ we have:
\[F_1(x) \land \ldots \land F_h(x)\]
and for a slot specification
\[
  \begin{array}{l}
    \Slot S \\
    ~~~\Value H\\
    ~~~\Cardmin m\\
    ~~~\Cardmax n
  \end{array}
\]  
we have
\[
  \begin{array}{l}
    \forall y\per\,(S(x,y) \imp H(y))\ \land\\
    \exists \dd{y}{m}\per\,((\bigwedge_{i\neq j} y_i \neq y_j) \land
                            S(x,y_{1}) \land \cdots \land S(x,y_{m}))\ \land\\
    \forall \dd{y}{n+1}\per\,((S(x,y_1) \land \cdots \land S(x,y_{n+1})) \imp
                              \bigvee_{i\neq j} y_i=y_j),
  \end{array}
\]
under the assumption that within one frame definition the occurrences of $x$
refer to the same free variable.  Finally the constraints on the slots are
interpreted as conjunction, disjunction and negation, respectively, i.e.:
\[
  \begin{array}{lll}
    \KEEinter{H_1}{H_2} &\textrm{ is interpreted as }& H_1(x) \land H_2(x)\\
    \KEEunion{H_1}{H_2} &\textrm{ is interpreted as }& H_1(x) \lor H_2(x)\\
    \KEEneg{H}          &\textrm{ is interpreted as }& \neg H(x)
  \end{array}
\]
%% Note that equality between variables is needed to express number
%% restrictions, while classes without number restrictions can be translated
%% into equality-free formulas.
A frame definition
\[\Frame{F}{\F} E\]
is then considered as the universally quantified sentence of the form
\[\forall x \per (F(x) \ra E(x)).\]
The whole frame \kb\ $\F$ is considered as the conjunction of all first-order
sentences corresponding to the frame definitions in $\F$.

Here we regard frame definitions as necessary conditions, which is commonplace
in the frame systems known as \emph{assertional} frame systems, as opposed to
\emph{definitional} systems, where frame definitions are interpreted as
necessary and sufficient conditions.

In order to enable the comparison with our formalisms for representing
structured knowledge we restrict our attention to the reasoning tasks that
involve the frame \kb, independently of the assertional knowledge, i.e., the
frames instances.  \citeA{FiKe85} mention several reasoning services associated
with frames, such as:
\begin{itemize}
\item \emph{Consistency checking}, which amounts to verifying whether a frame
  $F$ is satisfiable in a \kb.  In particular, this involves both reasoning on
  cardinalities and checking whether the filler of a given slot belongs to a
  certain frame.
\item \emph{Inheritance}, which, in our case, amounts to the ability of
  identifying which of the frames are more general than a given frame,
  sometimes called \emph{all-super-of} \cite{KaMG95}.  All the properties of
  the more general frames are then inherited by the more specific one.  Such a
  reasoning is therefore based on the more general ability to check the mutual
  relationhips between frame descriptions in the \kb.
\end{itemize}

These reasoning services are formalized in the first-order semantics as
follows.
\begin{definition} \label{def-frames-semantics}
  Let $\F$ be a frame \kb\ and $F$ a frame in $\F$.  We say that $F$ is
  \emph{consistent in} $\F$ if the first-order sentence
  $\F\land\exists x\per F(x)$ is satisfiable. %
  Moreover, we say that a frame description $E$ is \emph{more general} than $F$
  in $\F$ if $\F \models \forall x\per (F(x)\imp E(x))$.
  %%
  \endmarkfull
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Relationship between Frame Based Systems and \aluni}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

The first-order semantics given above allows us to establish a straightforward
relationship between frame languages and \aluni.  Indeed, we now present a
translation from frame \kbs\ to \aluni\ \kbs.

We first define the function $\KEEmaprel$ that maps each frame expression into
an $\ALUNI$ concept expression as follows:
\begin{itemize} \itemsep 0cm
\item Every frame name $F$ is mapped into an atomic concept $\KEEmap{F}$.
\item Every slot name $S$ is mapped into an atomic role $\KEEmap{S}$.
\item Every slot constraint is mapped as follows
  \[
    \begin{array}[t]{lll}
\KEEunion{H_1}{H_2} &\textrm{ is mapped into }& \KEEmap{H_1}\OR\KEEmap{H_2}.\\
\KEEinter{H_1}{H_2} &\textrm{ is mapped into }& \KEEmap{H_1}\AND\KEEmap{H_2}.\\
\KEEneg{H}          &\textrm{ is mapped into }& \NOT\KEEmap{H}.
    \end{array}
  \]
\item Every frame expression of the form
  \[
    \begin{array}[t]{l}
      \Superclasses \dd{F}{h}\\
      \Slot S_1 \\
      ~~~\Value H_1\\
      ~~~\Cardmin m_1\\
      ~~~\Cardmax n_1\\
      \cdots\\
      \Slot S_k \\
      ~~~\Value H_k\\
      ~~~\Cardmin m_k\\
      ~~~\Cardmax n_k
    \end{array}
  \]
  is mapped into the class expression
  \[
    \begin{array}{l}
      \KEEmap{F_1} \cd{\AND} \KEEmap{F_h}\ \AND\\
      \ALL{\KEEmap{S_1}}{\KEEmap{H_1}} \AND
      \EATLEAST{m_1}{\KEEmap{S_1}} \AND
        \EATMOST{n_1}{\KEEmap{S_1}}\ \AND\\
      \cdots\\
      \ALL{\KEEmap{S_k}}{\KEEmap{H_k}} \AND
        \EATLEAST{m_k}{\KEEmap{S_k}} \AND
        \EATMOST{n_k}{\KEEmap{S_k}}.
    \end{array}
  \]  
\end{itemize}
This mapping allows us to translate a frame \kb\ into an \aluni\ \kb, as
specified in the following definition.

\begin{definition} \label{def-frames-mapping}
  The \aluni\ \kb\ $\KEEmap{\F}\defas\Schema$ corresponding to a frame \kb\
  $\F$ is obtained as follows:
  \begin{itemize} \itemsep 0cm
  \item $\A$ consists of one atomic concept $\KEEmap{F}$ for each frame name
    $F$ in $\F$.
  \item $\P$ consists of one atomic role $\KEEmap{S}$ for each slot name $S$ in
    $\F$.
  \item $\T$ consists of an inclusion assertion
    \[\KEEmap{F} \ISAs \KEEmap{E}\]
    for each frame definition
    \[\Frame{F}{\F} E\]
    in $\F$.
  %%
  \endmarkfull
  \end{itemize}
\end{definition}

\begin{figure}[tb!]
  \boxtext{\small
   \vspace*{-\abovedisplayskip}
   \begin{tabbing}
     $\K$\=$\A$ \=\kill
     $\K\defas\Schema$, where\\[1mm]
     \>$\A$ \> $\defas\{$\=$\Course,\AdvCourse,\BasCourse,\Professor,
                            \Student,\GradStud,\Undergrad,\String\}$,\\[1mm]
     \>$\P$ \> $\defas\{$\>$\enrolls,\taughtby,\degree\}$,\\[1mm]
     \>and the set $\T$ of assertions consists of:
   \end{tabbing}
   \vspace*{-\abovedisplayskip}
   \begin{eqnarray*}
     \Course    &\ISA& \begin{array}[t]{@{}l}
                         \ALL{\enrolls}{\Student} \AND
                         \EATLEAST{2}{\enrolls} \AND
                         \EATMOST{30}{\enrolls}\ \AND \\
                         \ALL{\taughtby}{(\Professor \OR \GradStud)} \AND
                         \EEXACTLY{1}{\taughtby}
                       \end{array}\\
     \AdvCourse &\ISA& \Course \AND
                       \ALL{\enrolls}{(\GradStud \AND \NOT \Undergrad)} \AND
                       \EATMOST{20}{\enrolls}\\
     \BasCourse &\ISA& \Course \AND
                       \ALL{\taughtby}{\Professor}\\
     \GradStud  &\ISA& \Student \AND \ALL{\degree}{\String} \AND
                       \EEXACTLY{1}{\degree}\\
     \Undergrad &\ISA& \Student
   \end{eqnarray*}
   \par\vspace{-\belowdisplayshortskip}
   }
  \caption{The \aluni\ \kb\ corresponding to the KEE \kb\ in
   Figure~\protect{\ref{fig-frames-example}}}
  \label{fig-frames-example-kb}
\end{figure}

\begin{exampleCont}{\ref{example-frames-KEE-kb}}
We illustrate the translation on the frame \kb\ in
Figure~\ref{fig-frames-example}.  The corresponding \aluni\ \kb\ is shown in
Figure~\ref{fig-frames-example-kb}.
%%
\endmarkfull
\end{exampleCont}

The correctness of the translation follows from the correspondence between the
set-theoretic semantics of \aluni\ and the first-order interpretation of frames
\cite<see for example>{Haye79,Borg96,DLNS96}.  We can observe that inverse
roles are in fact not necessary for the formalization of frames.  Indeed, the
possibility of referring to the inverse of a slot has been rarely considered in
frame knowledge representation systems \cite<Some exceptions are reported
in>{Karp92}.  Due to the absence of inverse roles the distinction between
reasoning in finite and unrestricted models is not necessary%
\footnote{If we eliminate from $\ALUNI$ inverse roles, then the resulting
 DL has the finite model property.}. %
Consequently, all the above mentioned forms of reasoning are captured by
unrestricted concept consistency and concept subsumption in \aluni\ \kbs.  This
is summarized in the following theorem.

\begin{theorem} \label{thm-frames-correspondence}
  Let $\F$ be a frame knowledge-base, $F$ be a frame in $\F$, $E$ be a frame
  description, and $\KEEmap{\F}$, $\KEEmap{F}$, and $\KEEmap{E}$ be their
  translations in \aluni.  Then the following hold:
  \begin{itemize}
  \item $F$ is consistent in $\F$ if and only if
    $\classcons[u]{\KEEmap{\F}}{\KEEmap{F}}$.
  \item $E$ is more general than $F$ in $\F$ if and only if
    $\subs[u]{\KEEmap{\F}}{\KEEmap{F}}{\KEEmap{E}}$. %
  \end{itemize}
\end{theorem}

\begin{proof}
The claim directly follows from the semantics of frame knowledge bases and the
translation into DLs that we have adopted.
\end{proof}

By Theorem~\ref{thm-frames-correspondence} it becomes possible to exploit the
methods for unrestricted reasoning on \aluni\ knowledge bases in order to
reason on frame knowledge bases.  Since the problem of reasoning, e.g., in KEE
is already EXPTIME-complete, we do not pay in terms of computational complexity
for the expressiveness added by the constructs of \aluni.  In fact, by
resorting to the correspondence with \aluni\ it becomes possible to add to
frame systems useful features, such as the possibility of specifying the
inverse of a slot \cite{Karp92}, and still retain the ability to reason in
EXPTIME.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%\input{4-sdm}
\section{Semantic Data Models}
\label{sec-sdm}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Semantic data models were introduced primarily as formalisms for \db\ schema
design. They provide a means to model \dbs\ in a much richer way than
traditional data models supported by Database Management Systems, and are
becoming more and more important because they are adopted in most of the recent
\db\ design methodologies and Computer Aided Software Engineering tools.

The most widespread semantic data model is the Entity-Relationship (ER) model
introduced by \citeA{Chen76}.  It has by now become a standard, extensively
used in the design phase of commercial applications. In the commonly accepted
ER notation, classes are called \emph{entities} and are represented as boxes,
whereas relationships between entities are represented as diamonds. Arrows
between entities, called \emph{ISA} relationships, represent inclusion
assertions. The links between entities and relationships represent the
ER-\emph{roles}, to which number restrictions are associated. Dashed links are
used whenever such restrictions are refined for more specific entities.
Finally, elementary properties of entities are modeled by \emph{attributes},
whose values belong to one of several predefined domains, such as \Integer,
\String, or \Boolean.

The ER model does not provide constructs for expressing explicit disjointness
or disjunction of entities, but extensions of the model allow for the use of
generalization hierarchies which represent a combination of these two
constructs.  In order to keep the presentation simple, we do not consider
generalization hierarchies in the formalization we provide, although their
addition would be straightforward.  Similarly, we omit attributes of relations.

We now show that all relevant aspects of the ER model can be captured in
\aluni, and thus that reasoning on an ER schema can be reduced to reasoning on
the corresponding \aluni\ \kb.  Since \aluni\ is equipped with capabilities to
reason on \kbs, both with respect to finite and unrestricted models
(see~Section~\ref{sec-reasoning}), the reduction shows that reasoning on the ER
model, and more generally on semantic data models, is decidable.

As in the case of frame-based systems, we restrict our attention to those
aspects that constitute the core of the ER model. For this reason we do not
consider some features, such as keys and weak entities, that have been
introduced in the literature \cite{Chen76}, but appear only in some of the
formalizations of the ER model and the methodologies for conceptual modeling
based on the model.  A proposal for the treatment of keys in description logics
is presented by \citeA{BoWe97}.

In order to establish the correspondence between the ER model and \aluni, we
present formal syntax and semantics of ER schemata.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Syntax of the Entity-Relationship Model}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Although the ER model has by now become an industrial standard, several
variants and extensions have been introduced, which differ in minor aspects in
expressiveness and in notation \cite{Chen76,Teor89,BaCN92,Thal92,Thal93}.
Also, ER schemata are usually defined using a graphical notation which is
particularly useful for an easy visualization of the data dependencies, but
which is not well suited for our purposes. Therefore we have chosen a
formalization of the ER model which abstracts with respect to the most
important characteristics and allows us to develop the correspondence to
\aluni.

In the following, for two finite sets $X$ and $Y$ we call a function from a
subset of $X$ to $Y$ an \emph{$X$-labeled tuple over $Y$}.  The labeled tuple
$T$ that maps $x_i\in X$ to $y_i\in Y$, for $i\in\setone{k}$, is denoted
$\tuple{x}{y}{k}$. We also write $T[x_i]$ to denote $y_i$.

\begin{definition} \label{def-sdm-syntax}
  An \emph{ER schema} is a tuple $\S\defas\ERschema$, where
  \begin{itemize}
  \item $\LS$ is a finite alphabet partitioned into a set $\ES$ of
    \emph{entity} symbols, a set $\AS$ of \emph{attribute} symbols, a set $\US$
    of \emph{role} symbols, a set $\RS$ of \emph{relationship} symbols, and a
    set $\DS$ of \emph{domain} symbols; each domain symbol $D$ has an
    associated predefined basic domain $\Int[\BD]{D}$, and we assume the
    various basic domains to be pairwise disjoint.
  \item $\ERisa \incl \ES\x\ES$ is a binary relation over $\ES$.
  \item $\ERatt$ is a function that maps each entity symbol in $\ES$ to an
    $\AS$-labeled tuple over $\DS$.
  \item $\ERrel$ is a function that maps each relationship symbol in $\RS$ to
    an $\US$-labeled tuple over $\E_S$. We assume without loss of generality
    that:
    \begin{itemize}
    \item Each role is specific to exactly one relationship, i.e., for two
      relationships $R,R'\in\RS$ with $R\neq R'$, if
      $\ERrel(R)\defas\tuple{U}{E}{k}$ and
      $\ERrel(R')\defas\tuple{U'}{E'}{k'}$, then $\set{\dd{U}{k}}$ and
      $\set{\dd{U'}{k'}}$ are disjoint.
    \item For each role $U\in\US$ there is a relationship $R$ and an entity $E$
      such that $\ERrel(R)\defas[\ldots,\inc{U}{E},\ldots]$.
    \end{itemize}
  \item \sloppy $\ERccon$ is a function from $\ES\x\RS\x\US$ to
    $\Nat_0\x(\Nat_0\cup\set{\infty})$ that satisfies the following condition:
    for a relationship $R\in\RS$ such that $\ERrel(R)\defas\tuple{U}{E}{k}$,
    $\ERccon(E,R,U)$ is defined only if $U=U_i$ for some $i \in \set{1 \cld
     k}$, and if $E\ERisat E_i$ (where $\ERisat$ denotes the reflexive
    transitive closure of $\ERisa$).  The first component of $\ERccon(E,R,U)$
    is denoted with $\ERcmin(E,R,U)$ and the second component with
    $\ERcmax(E,R,U)$.  If not stated otherwise, $\ERcmin(E,R,U)$ is assumed to
    be $0$ and $\ERcmax(E,R,U)$ is assumed to be $\infty$.
  %%
  \endmarkfull
  \end{itemize}
\end{definition}

Before specifying the formal semantics of ER schemata we give an intuitive
description of the components of a schema.
%%
The relation $\ERisa$ models the ISA-relationship between entities. We do not
need to make any special assumption on the form of $\ERisa$ such as acyclicity
or injectivity.
%%
The function $\ERatt$ is used to model attributes of entities.  If for example
$\ERatt$ associates the $\AS$-labeled tuple
$[\inc{A_1}{\Integer},\inc{A_2}{\String}]$ to an entity $E$, then $E$ has two
attributes $A_1,A_2$ whose values are integers and strings respectively.  For
simplicity we assume attributes to be single-valued and mandatory, but we could
easily handle also multi-valued attributes with associated cardinalities.
%%
The function $\ERrel$ associates a set of roles to each relationship symbol
$R$, determining implicitly also the arity of $R$, and for each role $U$ in
such set a distinguished entity, called the \emph{primary entity for $U$ in
 $R$}.  In a \db\ satisfying the schema only instances of the primary entity
are allowed to participate in the relationship via the role $U$.
%%
The function $\ERccon$ specifies \emph{cardinality constraints}, i.e.,
constraints on the minimum and maximum number of times an instance of an entity
may participate in a relationship via some role.  Since such constraints are
meaningful only if the entity can effectively participate in the relationship,
the function is defined only for the sub-entities of the primary entity.  The
special value $\infty$ is used when no restriction is posed on the maximum
cardinality.  Such constraints can be used to specify both existence
dependencies and functionality of relations \cite{CoKa86}.  They are often used
only in a restricted form, where the minimum cardinality is either $0$ or $1$
and the maximum cardinality is either $1$ or $\infty$.  Cardinality constraints
in the form considered here have been introduced already by \citeA{Abri74} and
subsequently studied by \citeA{GrMi84,LeNo90,Ferg91,YePS94,Thal92}.
%% \citeA{Thal92} formalizes a very general form of cardinality constraints for
%% the ER model and studies deduction for restricted cases.

\begin{figure}[tbp]
  \centering
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  \input{er-schema}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
{\setlength{\unitlength}{1.1pt}
\begin{small}
\begin{picture}(280,150)
\thinlines

\put(0,0){\framebox(60,20){\AdvCourse}}
\put(0,60){\framebox(60,20){\Course}}
\put(220,120){\framebox(60,20){\Teacher}}
\put(220,60){\framebox(60,20){\Student}}
\put(220,0){\framebox(60,20){\GradStud}}
  \put(220,10){\line(-1,0){15}}
  \put(203,10){\circle{5}}
  \put(120,0){\makebox(80,20){\degree/\String}}

\put(100,50){\setlength{\unitlength}{0.8\unitlength}%
\begin{picture}(100,50)
  \put(0,0){\makebox(100,50){\ENROLLING}}
  \put(0,25){\line(2,1){50}}
  \put(0,25){\line(2,-1){50}}
  \put(100,25){\line(-2,1){50}}
  \put(100,25){\line(-2,-1){50}}
\end{picture}}

  \put(100,70){\line(-1,0){40}}
    \put(70,57){\makebox(20,10){(2,30)}}
    \put(70,73){\makebox(20,10){\Ein}}
  \put(180,70){\line(1,0){40}}
    \put(190,57){\makebox(20,10){(4,6)}}
    \put(190,73){\makebox(20,10){\Eof}}

\put(100,110){\setlength{\unitlength}{0.8\unitlength}%
\begin{picture}(100,50)
  \put(0,0){\makebox(100,50){\TEACHING}}
  \put(0,25){\line(2,1){50}}
  \put(0,25){\line(2,-1){50}}
  \put(100,25){\line(-2,1){50}}
  \put(100,25){\line(-2,-1){50}}
\end{picture}}

  \put(100,130){\line(-1,0){70}}
    \put(70,117){\makebox(20,10){(1,1)}}
    \put(70,133){\makebox(20,10){\Tof}}
  \put(180,130){\line(1,0){40}}
    \put(190,117){\makebox(20,10){(0,$\infty$)}}
    \put(190,133){\makebox(20,10){\Tby}}
  \put(30,130){\line(0,-1){50}}

  \dashline{8}(100,70)(60,10)
    \put(80,30){(2,20)}

\thicklines
  \put(30,20){\vector(0,1){40}}
  \put(250,20){\vector(0,1){40}}
\end{picture}
\end{small}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \caption{An ER schema}
  \label{fig-sdm-example}
\end{figure}

\begin{example} \label{example-sdm-er-schema}
Figure~\ref{fig-sdm-example} shows a simple ER schema modeling a state of
affairs similar to the one represented by the KEE \kb\ in
Figure~\ref{fig-frames-example}.  We have used the standard graphic notation
for ER schemata, except for the dashed link, which represents the refinement of
a cardinality constraint for the participation of a sub-entity (in our case
\AdvCourse) in a relationship (in our case \ENROLLING).
%%
\endmarkfull
\end{example}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Semantics of the Entity-Relationship Model}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

The semantics of an ER schema can be given by specifying which \db\ states are
consistent with the information structure represented by the schema. Formally,
a \db\ state $\B$ corresponding to an ER schema $\S\defas\ERschema$ is
constituted by a nonempty \emph{finite} set~$\domB$, assumed to be disjoint
from all basic domains, and a function~$\IntB{\cdot}$ that maps
\begin{itemize} \itemsep 0cm
\item every domain symbol $D \in \DS$ to the corresponding basic domain
  $\Int[\BD]{D}$,
\item every entity $E \in \ES$ to a subset $\IntB{E}$ of $\domB$,
\item every attribute $A \in \AS$ to a set
  $\IntB{A}\incl\domB\x\bigcup_{D\in\DS}\Int[\BD]{D}$, and
\item every relationship $R \in \RS$ to a set $\IntB{R}$ of $\US$-labeled
  tuples over $\domB$.
\end{itemize}
The elements of $\IntB{E}$, $\IntB{A}$, and $\IntB{R}$ are called
\emph{instances} of $E$, $A$, and $R$ respectively.

A \db\ state is considered acceptable if it satisfies all integrity constraints
that are part of the schema. This is captured by the definition of legal \db\ 
state.

\begin{definition} \label{def-sdm-semantics}
  A \db\ state $\B$ is said to be \emph{legal for} an ER schema
  $\S\defas\ERschema$, if it satisfies the following conditions:
  \begin{itemize} \itemsep 0cm
  \item For each pair of entities $E_1,E_2 \in \ES$ such that $E_1 \ERisa E_2$,
    it holds that $\IntB{E_1} \incl \IntB{E_2}$.
  \item For each entity $E \in \ES$, if $\ERatt(E)\defas\tuple{A}{D}{h}$, then
    for each instance $e \in \IntB{E}$ and for each $i\in\setone{h}$ the
    following holds:
    \begin{itemize}
    \item there is exactly one element $a_i \in \IntB{A_i}$ whose first
      component is $e$, and
    \item the second component of $a_i$ is an element of $\Int[\BD]{D_i}$.
    \end{itemize}
  \item For each relationship $R\in\RS$ such that
    $\ERrel(R)\defas\tuple{U}{E}{k}$, all instances of $R$ are of the form
    $\tuple{U}{e}{k}$, where $e_i \in \IntB{E_i}$, $i\in\setone{k}$.
  \item For each relationship $R\in\RS$ such that
    $\ERrel(R)\defas\tuple{U}{E}{k}$, for each $i\in\setone{k}$, for each
    entity $E\in\ES$ such that $E\ERisat E_i$ and for each instance $e$ of
    $E$ in $\I$, it holds that
    \[\ERcmin(E,R,U_i) \leq 
      \cards{\set{r \in \IntB{R} \mid r[U_i]=e}} \leq
      \ERcmax(E,R,U_i).
    \]
  \par\vspace{-\belowdisplayskip}
  \endmarkfull
  \end{itemize}
\end{definition}

Notice that the definition of \db\ state reflects the usual assumption in \dbs\
that \db\ states are finite structures \cite<see also>{CoKV90}.  In fact, the
basic domains are not required to be finite, but for each legal \db\ state for
a schema, only a finite set of values from the basic domains are actually of
interest.  We define the \emph{active domain} $\DactB$ of a \db\ state $\B$ as
the set of all elements of the basic domains $D^\BD$, $D \in \DS$, that
effectively appear as values of attributes in $\B$.  More formally:
\[\DactB \defas \set{d \in D^\BD \mid D\in\DS \land\exists A\in\AS, e\in\domB
                                  \suchthat (e,d)\in\IntB{A}}.
\]
Since $\domB$ is finite and $\AS$ contains only a finite number of attributes,
which are functional by definition, also $\DactB$ is finite.

Reasoning in the ER model includes verifying entity satisfiability and deducing
inheritance.  \emph{Entity satisfiability} amounts to checking whether a given
entity can be populated in some legal \db\ state \cite{AtPa86,LeNo90,DiLe93},
and corresponds to the notion of concept consistency in DLs.  Deducing
\emph{inheritance} amounts to verifying whether in all \dbs\ that are legal for
the schema, every instance of an entity is also an instance of another entity.
Such implied ISA relationships can arise for different reasons. Either
trivially, through the transitive closure of the explicit ISA relationships
present in the schema, or in more subtle ways, through specific patterns of
cardinality restrictions along cycles in the schema and the requirement of the
\db\ state to be finite \cite{LeNo90,CoKV90}.

\begin{figure}[tbp]
  \centering
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  \input{er-schema-even}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
{\setlength{\unitlength}{1pt}
\begin{small}
\begin{picture}(180,80)
\thinlines

\put(0,0){\framebox(60,20){\Even}}
\put(0,60){\framebox(60,20){\Number}}

\put(100,20){\setlength{\unitlength}{0.8\unitlength}%
\begin{picture}(100,50)
  \put(0,0){\makebox(100,50){\DOUBLES}}
  \put(0,25){\line(2,1){50}}
  \put(0,25){\line(2,-1){50}}
  \put(100,25){\line(-2,1){50}}
  \put(100,25){\line(-2,-1){50}}
\end{picture}}

\put(60,70){\line(1,0){80}}
\put(140,70){\line(0,-1){10}}
  \put(80,73){\makebox(20,10){(1,$\infty$)}}

\put(60,10){\line(1,0){80}}
\put(140,10){\line(0,1){10}}
  \put(80,13){\makebox(20,10){(0,1)}}

\thicklines
  \put(30,20){\vector(0,1){40}}
\end{picture}
\end{small}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \caption{The ER schema corresponding to
           Example~\ref{example-finite-unrestricted-even}}
  \label{fig-sdm-finite-unrestricted-even}
\end{figure}

\begin{example} \label{example-sdm-finite-unrestricted-even}
Figure~\ref{fig-sdm-finite-unrestricted-even} shows an ER schema modeling the
same situation as the \kb\ of Example~\ref{example-finite-unrestricted-even}.
Arguing exactly as in that example we can conclude that the two entities
\Number\ and \Even\ denote the same set of elements in every finite \db\ legal
for the schema, although the ISA relation from \Number\ to \Even\ is not stated
explicitly. It is implied, however, due to the cycle involving the relationship
and the two entities and due to the particular form of cardinality constraints.
%%
\endmarkfull
\end{example}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Relationship between Entity-Relationship Schemata and \aluni}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We now show that the different forms of reasoning on ER schemata are captured
by finite concept consistency and finite concept subsumption in \aluni.  The
correspondence between the two formalisms is established by defining a
translation $\ERmaprel$ from ER schemata to \aluni\ \kbs, and then proving
that there is a correspondence between legal \db\ states and finite models of
the derived \kb.

\begin{definition} \label{def-sdm-mapping}
  Let $\S\defas\ERschema$ be an ER schema. The \aluni\ \kb\
  $\ERS\defas\Schema$ is defined as follows:\\
  %%
  The set $\A$ of atomic concepts of $\ERS$ contains the following elements:
  \begin{itemize} \itemsep 0cm
  \item for each domain symbol $D\in\DS$, an atomic concept $\ERmap{D}$;
  \item for each entity $E\in\ES$, an atomic concept $\ERmap{E}$;
  \item for each relationship $R\in\RS$, an atomic concept $\ERmap{R}$.
  \end{itemize}
  %%
  The set $\P$ of atomic roles of $\ERS$ contains the following elements:
  \begin{itemize} \itemsep 0cm
  \item for each attribute $A\in\AS$, an atomic role $\ERmap{A}$;
  \item for each relationship $R\in\RS$ such that
    $\ERrel(R)\defas\tuple{U}{E}{k}$, $k$ atomic roles
    $\ERmap{U_1}\cld\ERmap{U_k}$.
  \end{itemize}
  %%
  The set $\T$ of assertions of $\ERS$ contains the following elements:
  \begin{itemize}
  \item for each pair of entities $E_1,E_2\in\ES$ such that $E_1\ERisa E_2$,
    the assertion
    \begin{equation} \label{eqn-sdm-mapping-inclusion}
      \ERmap{E_1} \ISAs \ERmap{E_2}
    \end{equation}
  \item for each entity $E\in\ES$ such that $\ERatt(E)\defas\tuple{A}{D}{h}$,
    the assertion
    \begin{equation} \label{eqn-sdm-mapping-attributes}
      \ERmap{E} \ISAs
        \ALL{\ERmap{A_1}}{\ERmap{D_1}} \cd{\AND}
        \ALL{\ERmap{A_h}}{\ERmap{D_h}} \AND
        \EEXACTLY{1}{\ERmap{A_1}} \cd{\AND} \EEXACTLY{1}{\ERmap{A_h}}
    \end{equation}
  \item for each relationship $R\in\RS$ such that
    $\ERrel(R)\defas\tuple{U}{E}{k}$, the assertions
    \begin{eqnarray}
      \ERmap{R}   &\ISA&
        \ALL{\ERmap{U_1}}{\ERmap{E_1}} \cd{\AND}
        \ALL{\ERmap{U_k}}{\ERmap{E_k}} \AND
        \EEXACTLY{1}{\ERmap{U_1}} \cd{\AND} \EEXACTLY{1}{\ERmap{U_k}}
        \label{eqn-sdm-mapping-relationship}\\
      \ERmap{E_i} &\ISA& \ALL{\INV{(\ERmap{U_i})}}{\ERmap{R}}, \qquad
        i\in\setone{k} \label{eqn-sdm-mapping-relationship-inv}
    \end{eqnarray}
  \item for each relationship $R\in\RS$ such that
    $\ERrel(R)\defas\tuple{U}{E}{k}$,
    for $i\in\setone{k}$, and %
    for each entity $E \in \ES$ such that $E \ERisat E_i$,
    \begin{itemize}
    \item if $m\defas\ERcmin(E,R,U_i) \neq 0$, the assertion
      \begin{equation} \label{eqn-sdm-mapping-cardinality-min}
        \ERmap{E} \ISAs
        \EATLEAST{m}{\INV{(\ERmap{U_i})}}.
      \end{equation}
    \item if $n\defas\ERcmax(E,R,U_i) \neq \infty$, the assertion
      \begin{equation} \label{eqn-sdm-mapping-cardinality-max}
        \ERmap{E} \ISAs \EATMOST{n}{\INV{(\ERmap{U_i})}}.
      \end{equation}
    \end{itemize}
  \item for each pair of symbols $X_1,X_2 \in \ES \cup \RS \cup \DS$ such that
    $X_1\neq X_2$ and $X_1 \in \RS\cup\DS$, the assertion
    \begin{equation} \label{eqn-sdm-mapping-disjointness}
      \ERmap{X_1} \ISAs \NOT\ERmap{X_2}.
    \end{equation}
  \par\vspace{-\belowdisplayskip}
  \endmarkfull
  \end{itemize}
\end{definition}

\begin{figure}[tb!]
  \boxtext{\small
   \vspace{-\abovedisplayskip}
   \begin{tabbing}
     $\K$\=$\A$ \=\kill
     $\K\defas\Schema$, where\\[1mm]
     \>$\A$ \> $\defas\{$\=$\Course,\AdvCourse,\Teacher,\Student,
                            \GradStud,\TEACHING,\ENROLLING,\String\}$,\\[1mm]
     \>$\P$ \> $\defas\{$\>$\Tof,\Tby,\Ein,\Eof,\degree\}$,\\[1mm]
     \>and the set $\T$ of assertions consists of:
   \end{tabbing}
   \vspace{-\abovedisplayskip}
   \begin{eqnarray*}
     \TEACHING  &\ISA& \begin{array}[t]{@{}l}
                         \ALL{\Tof}{\Course} \AND \EEXACTLY{1}{\Tof}\ \AND \\
                         \ALL{\Tby}{\Teacher} \AND \EEXACTLY{1}{\Tby}
                       \end{array} \\
     \ENROLLING &\ISA& \begin{array}[t]{@{}l}
                         \ALL{\Ein}{\Course} \AND \EEXACTLY{1}{\Ein}\ \AND \\
                         \ALL{\Eof}{\Student} \AND \EEXACTLY{1}{\Eof}
                       \end{array} \\
     \Course    &\ISA& \begin{array}[t]{@{}l}
                         \ALL{\Inv{\Tof}}{\TEACHING} \AND
                         \EEXACTLY{1}{\Inv{\Tof}}\ \AND \\
                         \ALL{\Inv{\Ein}}{\ENROLLING} \AND
                         \EATLEAST{2}{\Inv{\Ein}} \AND
                         \EATMOST{30}{\Inv{\Ein}}
                       \end{array} \\
     \AdvCourse &\ISA& \Course \AND \EATMOST{20}{\Inv{\Ein}} \\
     \Teacher   &\ISA& \ALL{\Inv{\Tby}}{\TEACHING} \\
     \Student   &\ISA& \ALL{\Inv{\Eof}}{\ENROLLING} \AND
                       \EATLEAST{4}{\Inv{\Eof}} \AND
                       \EATMOST{6}{\Inv {\Eof}}\\
     \GradStud  &\ISA& \Student \AND \ALL{\degree}{\String} \AND
                       \EEXACTLY{1}{\degree}.
   \end{eqnarray*}
   \par\vspace{-\belowdisplayshortskip}
   }
  \caption{The \aluni\ \kb\ corresponding to the ER schema in
   Figure~\protect{\ref{fig-sdm-example}}}
  \label{fig-sdm-example-kb}
\end{figure}

\begin{exampleCont}{\ref{example-sdm-er-schema}}
We illustrate the translation on the ER schema of Figure~\ref{fig-sdm-example}.
The \aluni\ \kb\ that captures exactly its semantics is shown in
Figure~\ref{fig-sdm-example-kb}, where for brevity the disjointness
assertions~(\ref{eqn-sdm-mapping-disjointness}) are omitted, and assertions
with the same concept on the left hand side are collapsed.
%%
\endmarkfull
\end{exampleCont}

The translation makes use of both inverse attributes and number restrictions to
capture the semantics of ER schemata.  We observe that, by means of the inverse
constructor, a binary relationship could be treated in a simpler way by
choosing a traversal direction and mapping the relationship directly to a role.
Notice also that the assumption of acyclicity of the resulting \kb\ is
unrealistic in this case, and in order to exploit the correspondence for
reasoning in the ER model, we need techniques that can deal with inverse
attributes, number restrictions, and cycles together.  As shown in
Example~\ref{example-finite-unrestricted-even}, the combination of these
factors causes the finite model property to fail to hold, and we need to resort
to reasoning methods for finite models.

In fact, we can reduce reasoning in the ER model to finite model reasoning in
\aluni\ \kbs.  For this purpose we define a mapping between \db\ states
corresponding to an ER schema and finite interpretations of the \kb\ derived
from it.  Due to the possible presence of relations with arity greater than 2,
this mapping is however not one-to-one and we first need to characterize those
interpretations of the \kb\ that directly correspond to \db\ states.

\begin{definition} \label{def-sdm-relation-descriptive-model}
  Let $\S\defas\ERschema$ be an ER schema and $\ERS$ be defined as above. An
  interpretation $\I$ of $\ERS$ is \emph{relation-descriptive}, if for every
  relationship $R\in\RS$, with $\ERrel(R)\defas\tuple{U}{E}{k}$, for every
  $d,d'\in\INT{\ERmap{R}}$, we have that
  \begin{equation} \label{eqn-sdm-relation-descriptive-model}
    (\bigwedge_{1\leq i\leq k} \forall d''\in\dom\suchthat
    ((d,d'')\in\INT{\ERmap{U_i}} \lra (d',d'')\in\INT{\ERmap{U_i}}))\imp d=d'.
  \end{equation}
  \par\vspace{-\belowdisplayskip}
  \endmarkfull
\end{definition}

Intuitively, the extension of a relationship in a \db\ state is a \emph{set}
of labeled tuples, and such a set does not contain the same element twice.
Therefore it is implicit in the semantics of the ER model that there cannot
be two labeled tuples connected through all roles of the relationship to
exactly the same elements of the domain. In a model of the \aluni\ \kb\ 
corresponding to the ER schema, on the other hand, each tuple is represented
by a new individual, and the above condition is not implicit anymore. It also
cannot be imposed in \aluni\ by suitable assertions.  The following lemma,
however, shows that we do not need such an explicit condition, when we are
interested in reasoning on an \aluni\ \kb\ corresponding to an ER schema.
This is due to the fact that we can always restrict ourselves to considering
only relation-descriptive models.

\begin{lemma} \label{lem-sdm-relation-descriptive-model}
  Let $\S$ be an ER schema, $\ERS$ be the \aluni\ \kb\ obtained from $\S$
  according to Definition~\ref{def-sdm-mapping}, and $C$ be a concept
  expression of $\ERS$.  If $C$ is finitely consistent in $\ERS$, then there is
  a finite relation-descriptive model $\I$ of $\ERS$ such that
  $\Int{C}\neq\eset$.
\end{lemma}

\begin{proof}
Let $\I_0$ be a finite model of $\ERS$ such that $\Int{C}\neq\eset$.  We can
build a finite relation-descriptive model $\I'$ by starting from $\I_0$ and
applying the following construction once for each relationship in $\RS$.

Let $\I$ be the model obtained in the previous step and let $R\in\RS$ with
$\ERrel(R)\defas\tuple{U}{E}{k}$ be the next relationship to which we apply the
construction.  We construct from $\I$ a model $\I_R$ such that
condition~\ref{eqn-sdm-relation-descriptive-model} is satisfied for
relationship $R$.

Given an individual $r\in\INT{\ERmap{R}}$, we denote by $U_i(d)$,
$i\in\setone{k}$ the (unique) individual $e$ such that
$(r,e)\in\INT{\ERmap{U_i}}$.
%%
For $e_i\in\INT{\ERmap{E_i}}$, $i\in\setone{k}$ we define
$X_{(\lablist{U}{e}{k})}\defas\set{r\in\INT{\ERmap{R}}\mid U_i(d)=e_i,
\textrm{ for } i\in\setone{k}}$.  We call \emph{conflict-set} a set
$X_{(\lablist{U}{e}{k})}$ with more than one element.
%%
From each conflict-set $X_{(\lablist{U}{e}{k})}$ we randomly choose one
individual $r$, and we say that the others \emph{induce a conflict on}
$(\lablist{U}{e}{k})$.  We call $\Conf$ the (finite) set of all objects
inducing a conflict on some $(\lablist{U}{e}{k})$.

We define an interpretation $\I_{2^{\Conf}}$ as the disjoint union of
$2^{\cards\Conf}$ copies of $\I$, one copy, denoted by $\I_\Z$, for every
set $\Z\in 2^{\Conf}$.  We denote by $d_\Z$ the copy in $\I_\Z$ of the
individual $d$ in $\I$. Since the disjoint union of two models of an \aluni\
\kb\ is again a model, $\I_{2^{\Conf}}$ is a model of $\ERS$.
%%
Let $\I_\Z$ and $\I_{\Z'}$ be two copies of $\I$ in $\I_{2^{\Conf}}$.  We call
\emph{exchanging $U_k(r_\Z)$ with $U_k(r_{\Z'})$} the operation on
$\I_{2^{\Conf}}$ consisting of replacing in $\INT[\I_\Z]{\ERmap{U_k}}$ the
pair $(r_\Z,U_k(r_\Z))$ with $(r_\Z,U_k(r_{\Z'}))$ and, at the same time,
replacing in $\INT[\I_{\Z'}]{\ERmap{U_k}}$ the pair $(r_{\Z'},U_k(r_{\Z'}))$
with $(r_{\Z'},U_k(r_\Z))$.  Intuitively, by exchanging $U_k(r_\Z)$ with
$U_k(r_{\Z'})$, the individuals $r_\Z$ and $r_{\Z'}$ do not induce conflicts
anymore.

We construct now from $\I_{2^{\Conf}}$ an interpretation $\I_R$ as follows:
For each $r\in\Conf$ and for each $\Z\in 2^{\Conf}$ such that $r\in\Z$, we
exchange $U_k(r_\Z)$ with $U_k(r_{\Z\setminus\set{r}})$.  It is possible to
show that all conflicts are thus eliminated while no new conflict is created.
Hence, in $\I_R$, condition~\ref{eqn-sdm-relation-descriptive-model} for $R$ is
satisfied.
%%
We still have to show that $\I_R$ is a model of $\ERS$ in which
$\Int[\I_R]{C}\neq\eset$.  Indeed, it is straightforward to check by induction
that for every concept expression $C'$ appearing in $\ERS$, for all $\Z\in
2^{\Conf}$, $d\in\Int{C'}$ if and only if $d_{\Z}\in\Int[\I_R]{C'}$.  Thus all
assertions of $\ERS$ are still satisfied in $\I_R$ and
$\Int[\I_R]{C}\neq\eset$.
\end{proof}

With this result, the following correspondence between legal \db\ states for an
ER schema and relation-descriptive models of the resulting \aluni\ \kb\
can be established.

\begin{proposition}  \label{prop-sdm-correspondence}
  For every ER schema $\S\defas\ERschema$ there exist two mappings $\alphaS$,
  from \db\ states corresponding to $\S$ to finite interpretations of its
  translation $\ERS$, and $\betaS$, from finite relation-descriptive
  interpretations of $\ERS$ to \db\ states corresponding to $\S$, such that:
  \begin{enumerate}
  \item For each legal \db\ state $\B$ for $\S$, $\alphaS(\B)$ is a finite
    model of $\ERS$, and for each symbol $X\in\ES\cup\AS\cup\RS\cup\DS$,
    $\IntB{X}=\INT[\alphaS(\B)]{\ERmap{X}}$.
  \item For each finite relation-descriptive model $\I$ of $\ERS$, $\betaS(\I)$
    is a legal \db\ state for $\S$, for each entity $E\in\ES$,
    $\INT{\ERmap{E}}=\Int[\betaS(\I)]{E}$, and for each symbol
    $X\in\AS\cup\RS\cup\DS$,
    $\cards{\Int[\I]{\ERmap{X}}}=\cards{\Int[\betaS(\I)]{X}}$.
    %%, and $\betaS(\INT{\ERmap{X}})=\Int[\betaS(\I)]{X}$.
  \end{enumerate}
\end{proposition}

\begin{proof}
(1) Given a \db\ state $\B$, we define the interpretation $\I\defas\alphaS(\B)$
of $\ERS$ as follows:
\begin{itemize}
\item $\dom \defas \domB \cup \DactB \cup \bigcup_{R\in\RS} \IntB{R}$.
\item For each symbol $X\in\ES\cup\AS\cup\RS\cup\DS$,
  \begin{equation} \label{eqn-sdm-mapping-extension-concept}
    \INT{\ERmap{X}}\defas\IntB{X}.
  \end{equation}
\item For each relationship $R\in\RS$ such that
  $\ERrel(R)\defas\tuple{U}{E}{k}$,
  \begin{equation} \label{eqn-sdm-mapping-extension-role}
    \INT{\ERmap{U_i}} \defas \set{(r,e) \in \dom\x\dom \mid r\in\IntB{R},
                             \textrm{ and } r[U_i]=e},\quad i\in\setone{k}.
  \end{equation}
\end{itemize}
Let $\B$ be a legal \db\ state.  To prove claim (1) it is sufficient to show
that $\I$ satisfies every assertion in $\ERS$.
%%
Assertions~\ref{eqn-sdm-mapping-inclusion} are satisfied since $\B$
satisfies the set inclusion between the extensions of the corresponding
entities.
%%
With respect to assertions~\ref{eqn-sdm-mapping-attributes}, let $E\in\ES$ be
an entity such that $\ERatt(E)\defas\tuple{A}{D}{h}$, and consider an instance
$e\in\INT{\ERmap{E}}$. We have to show that for each $i\in\setone{h}$, there is
exactly one element $e_i\in\dom$ such that $(e,e_i)\in\INT{\ERmap{A_i}}$, and
moreover that $e_i\in\INT{\ERmap{D_i}}$.
By~\ref{eqn-sdm-mapping-extension-concept}, $e\in\IntB{E}$, and by definition
of legal \db\ state there is exactly one element
$a_i\in\IntB{A_i}=\INT{\ERmap{A_i}}$ whose first component is $e$.  Moreover,
the second component $e_i$ of $a_i$ is an element of
$\Int[\BD]{D_i}=\INT{\ERmap{D_i}}$.
%%
With respect to assertions~\ref{eqn-sdm-mapping-relationship}, let $R\in\RS$ be
a relationship such that $\ERrel(R)\defas\tuple{U}{E}{k}$, and consider an
instance $r\in\INT{\ERmap{R}}$. We have to show that for each $i\in\setone{k}$
there is exactly one element $e_i\in\dom$ such that
$(r,e_i)\in\INT{\ERmap{U_i}}$, and that moreover $e_i\in\INT{\ERmap{E_i}}$.
By~\ref{eqn-sdm-mapping-extension-concept}, $r\in\IntB{R}$, and by definition
of legal \db\ state, $r$ is a labeled tuple of the form $\tuple{U}{e'}{k}$,
where $e'_i\in\IntB{E_i}$, $i\in\setone{k}$.  Therefore $r$ is a function
defined on $\set{\dd{U}{k}}$, and by~\ref{eqn-sdm-mapping-extension-role},
$e_i$ is unique and equal to $e'_i$.  Moreover, again
by~\ref{eqn-sdm-mapping-extension-concept},
$e_i\in\INT{\ERmap{E_i}}=\IntB{E_i}$.
%%
Assertions~\ref{eqn-sdm-mapping-relationship-inv} are satisfied, since
by~\ref{eqn-sdm-mapping-extension-role} the first component of each element of
$\INT{\ERmap{U_i}}$ is always an element of $\IntB{R}=\INT{\ERmap{R}}$.
%%
With respect to assertions~\ref{eqn-sdm-mapping-cardinality-min}, let
$R\in\RS$ be a relationship such that $\ERrel(R)\defas\tuple{U}{E}{k}$, let
$E\in\ES$ be an entity such that $E \ERisa E_i$, for some $i\in\setone{k}$,
and such that $m\defas\ERcmin(E,R,U_i)\neq0$.  Consider an instance
$e\in\INT{\ERmap{E}}$.  We have to show that there are at least $m$ pairs in
$\INT{\ERmap{U_i}}$ that have $e$ as their second component. Since
assertions~\ref{eqn-sdm-mapping-relationship-inv} are satisfied we
know that the first component of all such pairs is an instance of $\ERmap{R}$.
By~\ref{eqn-sdm-mapping-extension-concept} and by definition of legal
\db\ state, there are at least $m$ labeled tuples in $\IntB{R}$ whose $U_i$
component is equal to $e$.
By~\ref{eqn-sdm-mapping-extension-role}, $\INT{\ERmap{U_i}}$
contains at least $m$ pairs whose second component is equal to $e$.
%%
With respect to assertions~\ref{eqn-sdm-mapping-cardinality-max} we
can proceed in a similar way.
%%
Finally, assertions~\ref{eqn-sdm-mapping-disjointness} are satisfied
since first, by definition the basic domains are pairwise disjoint and disjoint
from $\domB$ and from the set of labeled tuples, second, no element of $\domB$
is a labeled tuple, and third, labeled tuples corresponding to different
relationships cannot be equal since they are defined over different sets of
roles.

(2) Let $\I$ be a finite relation-descriptive interpretation of $\ERS$.  For
each basic domain $D\in\DS$, let $\betaD^D$ be a function from $\dom$ to
$\Int[\BD]{D}$ that is one-to-one and onto.  Since $\dom$ is finite and each
basic domain contains a countable number of elements, such a function always
exists.  In order to define $\betaS(\I)$ we first specify a mapping $\betaD$
that associates to each individual $d\in\dom$ an element as follows:
\begin{itemize}
\item If $d\in\INT{\ERmap{E}}$ for some entity $E\in\ES$, then
  $\betaD(d)\defas d$.
\item \sloppy If $d\in\INT{\ERmap{R}}$ for some relationship $R\in\RS$ with
  $\ERrel(R)\defas\tuple{U}{E}{k}$, and there are individuals
  $\dd{d}{k}\in\dom$ such that $(d,d_i)\in\INT{\ERmap{U_i}}$, for
  $i\in\setone{k}$, then $\betaD(d)\defas\tuple{U}{d}{k}$.
\item If $d\in\INT{\ERmap{D}}$ for some basic domain $D\in\DS$, then
  $\betaD(d)\defas\betaD^D(d)$.
\item Otherwise $\betaD(d)\defas d$.
\end{itemize}
For a pair of individuals $(d_1,d_2)\in\dom\x\dom$,
$\betaD((d_1,d_2))\defas(\betaD(d_1),\betaD(d_2))$, and for a set $X$,
$\betaD(X)\defas\set{\betaD(x) \mid x\in X}$.

If $\I$ is a model of $\ERS$ the above rules define $\betaD(d)$ for every
$d\in\dom$. Indeed, by assertions~\ref{eqn-sdm-mapping-disjointness}, each
$d\in\dom$ can be an instance of at most one atomic concept corresponding to a
relationship or basic domain, and if this is the case it is not an instance of
any atomic concept corresponding to an entity.  Moreover, if
$d\in\INT{\ERmap{R}}$ for some relationship $R\in\RS$ with
$\ERrel(R)\defas\tuple{U}{E}{k}$, then by
assertions~\ref{eqn-sdm-mapping-relationship}, for each $i\in\setone{k}$ there
is exactly one element $d_i\in\dom$ such that $(d,d_i)\in\INT{\ERmap{U_i}}$.
%%
If $\I$ is not a model of $\ERS$ and for some $d\in\dom$, $\betaD(d)$ is not
uniquely determined, then we choose nondeterministically one possible value.

We can now define the \db\ state $\B\defas\betaS(\I)$ corresponding to $\I$:
\begin{itemize}
\item $\domB \defas \dom \setminus \left(\bigcup_{R\in\RS}\INT{\ERmap{R}} \cup
  \bigcup_{D\in\DS}\INT{\ERmap{D}}\right)$.
\item For each symbol $X\in\ES\cup\AS\cup\RS\cup\DS$,
  $\IntB{X}\defas\betaD(\INT{\ERmap{X}})$.
\end{itemize}
It is not difficult to see, that if $\I$ is a model of $\ERS$, then $\B$
defined in such a way is a legal \db\ state for $\S$ with active domain
$\bigcup_{D\in\DS}\INT{\ERmap{D}}$.
\end{proof}

The following theorem allows us to reduce reasoning on ER schemata to finite
model reasoning on \aluni\ \kbs.

\begin{theorem} \label{thm-sdm-correspondence}
  Let $\S$ be an ER schema, $E,E'$ be two entities in $\S$, and $\ERS$ be the
  translation of $\S$.  Then the following holds:
  \begin{enumerate}
  \item $E$ is satisfiable in $\S$ if and only if
    $\classcons[f]{\ERS}{\ERmap{E}}$.
  \item $E$ inherits from $E'$ in $\S$ if and only if
    $\subs[f]{\ERS}{\ERmap{E}}{\ERmap{E'}}$.
  \end{enumerate}
\end{theorem}

\begin{proof}
(1) \OnlyIf %
Let $\B$ be a legal \db\ state with $\IntB{E}\neq\eset$. By part~1 of
Proposition~\ref{prop-sdm-correspondence}, $\alphaS(\B)$ is a finite
model of $\ERS$ in which $\INT[\alphaS(\B)]{\ERmap{E}}\neq\eset$.

\If %
Let $\ERmap{E}$ be finitely consistent in $\ERS$. %
By Lemma~\ref{lem-sdm-relation-descriptive-model} there is a finite
relation-descriptive model $\I$ of $\ERS$ with $\Int{\ERmap{E}}\neq\eset$. %
By part~2 of Proposition~\ref{prop-sdm-correspondence}, $\betaS(\I)$
is a \db\ state legal for $\S$ in which $\IntB{E}\neq\eset$.

(2) \OnlyIf %
Let $\notsubs[f]{\ERS}{\ERmap{E}}{\ERmap{E'}}$. %
Then $\ERmap{E}\AND\NOT\ERmap{E'}$ is finitely consistent in $\ERS$.  %
By Lemma~\ref{lem-sdm-relation-descriptive-model} there is a finite
relation-descriptive model $\I$ of $\ERS$ with $d\in\INT{\ERmap{E}}$ and
$d\not\in\INT{\ERmap{E'}}$, for some $d\in\dom$. %
By part~2 of Proposition~\ref{prop-sdm-correspondence}, $\betaS(\I)$ is a \db\ 
state legal for $\S$ in which $d\in\IntB{E}$ and $d\not\in\IntB{E'}$.
Therefore $E$ does not inherit from $E'$.

\If %
Assume $E$ does not inherit from $E'$. %
Then there is a \db\ state $\B$ legal for $\S$ where for an instance
$e\in\IntB{E}$ we have $e\not\in\IntB{E'}$. %
By part~1 of Proposition~\ref{prop-sdm-correspondence}, $\alphaS(\B)$ is a
finite model of $\ERS$ in which $e\in\INT[\alphaS(\B)]{\ERmap{E}}$ and
$e\not\in\INT[\alphaS(\B)]{\ERmap{E'}}$. %
Therefore $\notsubs[f]{\ERS}{\ERmap{E}}{\ERmap{E'}}$.
\end{proof}

Theorem~\ref{thm-sdm-correspondence} allows us to effectively exploit the
reasoning methods that have been developed for \aluni\ in order to reason on ER
schemas.  The complexity of the resulting method for reasoning on ER schemata
is exponential.  Observe however, that the known algorithms for reasoning on ER
schemata are also exponential \cite{CaLe94}, and that the precise computational
complexity of the problem is still open.

Moreover, by exploiting the correspondence with \aluni, it becomes possible to
add to the ER model (and more in general to semantic data models) several
features and modeling primitives that are currently missing, and which have
been considered important, and fully take them into account when reasoning over
schemata.  Such additional features include for example the possibility to
specify and use arbitrary boolean combinations of entities, and to refine
properties of entities along ISA hierarchies.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%\input{5-oodm}
\section{Object-Oriented Data Models}
\label{sec-oom}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Object-oriented data models have been proposed with the goal of devising \db\ 
formalisms that could be integrated with \oo\ programming systems \cite{Kim90}.
They are the subject of an active area of research in the database field, and
are based on the following features:
\begin{itemize}
\item They rely on the notion of object identifier at the extensional level (as
  opposed to traditional data models which are value-oriented) and on the
  notion of class at the intensional level.
\item The structure of the classes is specified by means of typing and
  inheritance.
\end{itemize}

As in the previous section, we present the common basis of \oo\ data models
with other class-based formalisms by introducing a language for specifying \oo\
schemata and show that such schemata can be correctly represented as \aluni\ 
\kbs. In our analysis, we concentrate our attention on the structural aspects
of object-oriented data models. One of the characteristics of the
object-oriented approach is to provide mechanisms for specifying also the
dynamic properties of classes and objects, typically through the definition of
methods associated to the classes. Those aspects are outside the scope of our
investigations.  Nevertheless, we argue that general techniques for schema
level reasoning, in particular, type consistency and type inference, can be
profitably exploited for restricted forms of reasoning on methods
\cite{AKRW92}.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Syntax of an Object-Oriented Model}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Below we define a simple \oo\ language in the style of most popular models
featuring complex objects and object identity.  Although we do not refer to any
specific formalism, our model is inspired by the ones presented by
\citeA{AbKa89,HuKi87}.

\begin{definition} \label{def-oom-syntax}
  An \emph{\oo\ schema} is a tuple $\S\defas\OOschema$, where:
  \begin{itemize} \itemsep 0cm
  \item $\CS$ is a finite set of \emph{class names}, denoted by the letter $C$.
  \item $\AS$ is a finite set of \emph{attribute names}, denoted by the letter
    $A$.
  \item $\DS$ is a finite set of \emph{class declarations} of the form
    \[\Tisa{C}{\dd{C}{k}}{T},\]
    in which $T$ denotes a \emph{type expression} built according to the
    following syntax:
    \begin{eqnarray*}
      T &\lora& C             \mid\\
        &     & \Tunion{T}{k} \mid\\
        &     & \Tset{T}      \mid\\
        &     & \Trecord{A}{T}{k}.
    \end{eqnarray*}
    $\DS$ contains exactly one such declaration for each class $C\in\CS$.
    %%
    \endmarkfull
  \end{itemize}
\end{definition}

\begin{figure}[tb!]
  \boxtext{\small
   \hspace*{\stretch{0.5}}
   \begin{minipage}[t]{7cm}
     \begin{tabbing}
       xx\=xx\=\kill
       \OOclass\ \Teacher\ \OOtypeis\\
       \> \OOunion\ \Professor, \GradStud\\
       \> \OOend\\[3mm]
       \OOclass\ \GradStud\ \OOisa\ \Student\ \OOtypeis\\
       \> \OOrecord\\
       \> \> \degree: \String\\
       \> \OOend
     \end{tabbing}
   \end{minipage}
   \hfill
   \begin{minipage}[t]{7cm}
     \begin{tabbing}
       xx\=xx\=\kill
       \OOclass\ \Course\ \OOtypeis\\
       \> \OOrecord\\
       \> \> \enrolls: \OOsetof\ \Student,\\
       \> \> \taughtby: \Teacher\\
       \> \OOend
     \end{tabbing}
   \end{minipage}
   \hspace*{\stretch{0.5}}
   } %\end{boxtext}
  \caption{An \oo\ schema}
  \label{fig-oom-example}
\end{figure}

\begin{example} \label{example-oom-oo-schema}
Figure~\ref{fig-oom-example} shows a fragment of the \oo\ schema corresponding
to the KEE \kb\ of Figure~\ref{fig-frames-example}.
%%
\endmarkfull
\end{example}

Each class declaration imposes constraints on the instances of the class it
refers to.  The \OOisa\ part of a class declaration allows one to specify
inclusion between the sets of instances of the involved classes, while the
\OOtypeis\ part specifies through a type expression the structure assigned to
the objects that are instances of the class.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Semantics of an Object-Oriented Model}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

The meaning of an \oo\ schema is given by specifying the characteristics of an
instance of the schema. The definition of instance makes use of the notions of
object identifier and value.

Let us first characterize the set of values that can be constructed from a set
of symbols, called \emph{object identifiers}.  Given a finite set $\O$ of
symbols denoting real world objects, the set $\VO$ of \emph{values} over $\O$
is inductively defined as follows:
\begin{itemize} \itemsep 0cm
\item $\O\incl\VO$.
\item If $\dd{v}{k} \in \VO$ then $\OOset{\dd{v}{k}} \in \VO$.
\item If $\dd{v}{k} \in \VO$ then $\OOtuple{A}{v}{k} \in \VO$.
\item Nothing else is in $\VO$.
\end{itemize}
%%
A \emph{\db\ instance} $\J$ of a schema $\S\defas\OOschema$ is constituted by
\begin{itemize} \itemsep 0cm
\item a \emph{finite} set $\Oid$ of object identifiers;
\item a mapping $\piJ$ assigning to each class in $\CS$ a subset of $\Oid$;
\item a mapping $\rhoJ$ assigning a value in $\Values$ to each object in
  $\Oid$.
\end{itemize}
%%
Although the set $\Values$ of values that can be constructed from a set $\Oid$
of object identifiers is infinite, for a \db\ instance one needs only to
consider a finite subset of $\Values$.

\begin{definition} \label{def-oom-values}
  Given an \oo\ schema $\S$ and an instance $\J$ of $\S$, the set $\Vact$ of
  \emph{active values} with respect to $\J$ is constituted by:
  \begin{itemize} \itemsep 0cm
  \item the set $\Oid$  of object identifiers.
  \item the set of values assigned by $\IntJ{\rho}$ to the elements of $\Oid$,
    including those values that are not explicitly associated with object
    identifiers, but are used to form other values.
  %%
  \endmarkfull
  \end{itemize}
\end{definition}

The interpretation of type expressions in $\J$ is defined through an
\emph{interpretation function}~$\IntJ{\cdot}$ that assigns to each type
expression a subset of $\Values$ such that the following conditions are
satisfied:
\begin{eqnarray*}
  \IntJ{C}                    &=& \piJ(C) \\
  \INT[\J]{\Tunion{T}{k}}     &=& \IntJ{T_1} \cds{\cup} \IntJ{T_k} \\
  \INT[\J]{\Tset{T}}          &=& \{\OOset{\dd{v}{k}} \mid k \geq 0,
    v_i\in\IntJ{T},\textrm{ for } i\in\setone{k}\}\\[1mm]
  \INT[\J]{\Trecord{A}{T}{k}} &=&
    \begin{array}[t]{@{}l}
      \{\OOtuple{A}{v}{h} \mid h\geq k,\\
      \qquad v_i\in\IntJ{T_i},\textrm{ for } i\in\setone{k},\\
      \qquad v_j\in\Values,\textrm{ for } j\in\set{k+1\cld h}\}.
    \end{array}
\end{eqnarray*}
%%
Notice that the instances of type record may have more components than those
specified in the type of the class.  Thus we are using an open semantics for
records, which is typical of \oo\ data models \cite{AbKa89}.

In order to characterize \oo\ data models we consider the instances that are
admissible for the schema.

\begin{definition} \label{def-oom-semantics}
  Let $\S\defas\OOschema$ be an \oo\ schema. A \db\ instance $\J$ of $\S$ is
  said to be \emph{legal} (with respect to $\S$) if for each declaration
  \[\Tisa{C}{\dd{C}{n}}{T}\]
  in $\DS$, it holds that $\IntJ{C}\incl\IntJ{C_i}$ for each $i\in\setone{n}$,
  and that $\rhoJ(\IntJ{C})\incl\IntJ{T}$.
  %%
  \endmarkfull
\end{definition}

Therefore, for a legal \db\ instance, the type expressions that are present in
the schema determine the (finite) set of active values that must be considered.
The construction of such values is limited by the depth of type expressions.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Relationship between Object-Oriented Schemata and \aluni}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We establish now a relationship between \aluni\ and the \oo\ language
presented above.  This is done by providing a mapping from \oo\ schemata into
\aluni\ \kbs.  Since the interpretation domain for \aluni\ \kbs\ consists of
atomic objects, whereas each instance of an \oo\ schema is assigned a possibly
structured value (see the definition of $\VO$), we need to explicitly represent
some of the notions that underlie the \oo\ language.  In particular, while
there is a correspondence between concepts and classes, one must explicitly
account for the type structure of each class.  This can be accomplished by
introducing in \aluni\ concepts \AbstractClass, to represent the classes, and
\RecType\ and \SetType\ to represent the corresponding types.  The associations
between classes and types induced by the class declarations, as well as the
basic characteristics of types, are modeled by means of roles: the (functional)
role \OOvalue\ models the association between classes and types, and the role
\OOmember\ is used for specifying the type of the elements of a set. Moreover,
the concepts representing types are assumed to be mutually disjoint, and
disjoint from the concepts representing classes.  These constraints are
expressed by adequate inclusion assertions that will be part of the \kb\ we are
going to define.

We first define the function $\OOmaprel$ that maps each type expression into an
$\ALUNI$ concept expression as follows:
\begin{itemize}
\item Every class $C$ is mapped into an atomic concept $\OOmap{C}$.
\item Every type expression $\Tunion{T}{k}$ is mapped into
  $\OOmap{T_1}\cds{\OR}\OOmap{T_k}$.
\item Every type expression $\Tset{T}$ is mapped into
  $\SetType\AND\ALL{\OOmember}{\OOmap{T}}$.
\item \sloppy Every attribute $A$ is mapped into an atomic role $\OOmap{A}$,
  and every type expression $\Trecord{A}{T}{k}$ is mapped into
  \[
    \begin{array}{r@{}l}
      \RecType \;\AND\; & \ALL{\OOmap{A_1}}{\OOmap{T_1}} \AND
                          \EEXACTLY 1 {\OOmap{A_1}} \cd{\AND} \\
                        & \ALL{\OOmap{A_k}}{\OOmap{T_k}} \AND
                          \EEXACTLY 1 {\OOmap{A_k}}.
    \end{array}
  \]
\end{itemize}

Using $\OOmaprel$ we define the \aluni\ \kb\ corresponding to an \oo\ schema.

\begin{definition} \label{def-oom-mapping}
  The \aluni\ \kb\ $\OOS\defas\Schema$ corresponding to the \oo\ schema
  $\S\defas\OOschema$ is obtained as follows:
  \begin{itemize}
  \item $\A\defas\set{\AbstractClass,\,\RecType,\,\SetType} \cup
    \set{\OOmap{C} \mid C\in\CS}$.
  \item $\P\defas\set{\OOvalue,\OOmember} \cup \set{\OOmap{A} \mid A\in\AS}$.
  \item $\T$ consists of the following assertions:
    \[
      \begin{array}{rcl}
        \AbstractClass &\ISA& \EEXACTLY{1}{\OOvalue}\\
        \RecType       &\ISA& \ALL{\OOvalue}{\bot}\\
        \SetType       &\ISA& \ALL{\OOvalue}{\bot} \AND \NOT\RecType
      \end{array}
    \]
    and for each class declaration
    \[\Tisa{C}{\dd{C}{n}}{T}\]
    in $\DS$, an inclusion assertion
    \[
      \OOmap{C} \ISAs \AbstractClass \AND
                      \OOmap{C_1} \cds{\AND} \OOmap{C_n} \AND
                      \ALL{\OOvalue}{\OOmap{T}}.
    \]
    \par\vspace{-2\belowdisplayskip}
    \endmarkfull
  \end{itemize}
\end{definition}

From the above translation we can observe that inverse roles are not necessary
for the formalization of \oo\ data models. Indeed, the possibility of referring
to the inverse of an attribute is generally ruled out in such models.  However,
this strongly limits the expressive power of the data model, as pointed out in
recent papers \cite<see for example>{AlGO91,Catt94}.  Note also that the use of
number restrictions is limited to the value~1, which corresponds to existence
constraints and functionality, whereas union is used in a more general form
than for example in the KEE system.

\begin{figure}[tb!]
  \boxtext{\small
   \vspace{-\abovedisplayskip}
   \begin{tabbing}
     $\K$\=$\A$ \=\kill
     $\K\defas\Schema$, where\\[1mm]
     \>$\A$ \> $\defas\{$\=$\AbstractClass,\RecType,\SetType,\String,$\\
     \>     \> \>$\Course,\Teacher,\Professor,\Student,\GradStud\}$,\\[1mm]
     \>$\P$ \> $\defas\{$\>$\OOvalue,\OOmember,
                            \enrolls,\taughtby,\degree\}$,\\[1mm]
     \>and the set $\T$ of assertions consists of:
   \end{tabbing}
   \vspace{-\abovedisplayskip}
   \begin{eqnarray*}
     \Course  &\ISA&
       \begin{array}[t]{@{}l}
         \AbstractClass \AND{}\\
         \ALL{\OOvalue}{(
           \begin{array}[t]{@{}l}
             \RecType \AND \EEXACTLY{1}{\enrolls} \AND
             \EEXACTLY{1}{\taughtby}\ \AND\\
             \ALL{\enrolls}{(\SetType\AND\ALL{\OOmember}{\Student})} \AND
             \ALL{\taughtby}{\Teacher})
           \end{array}}
       \end{array}\\
     \Teacher  &\ISA&
       \AbstractClass \AND \ALL{\OOvalue}{(\GradStud \OR \Professor)}\\
     \GradStud &\ISA&
       \begin{array}[t]{@{}l}
         \AbstractClass \AND \Student \AND{}\\
         \ALL{\OOvalue}{(\RecType \AND \ALL{\degree}{\String} \AND
                         \EEXACTLY{1}{\degree})}
       \end{array}\\
     \AbstractClass &\ISA& \EEXACTLY{1}{\OOvalue}\\
     \RecType       &\ISA& \ALL{\OOvalue}{\bot}\\
     \SetType       &\ISA& \ALL{\OOvalue}{\bot} \AND \NOT\RecType
   \end{eqnarray*}
   \par\vspace{-\belowdisplayshortskip}
   } % \end{boxtext}
  \caption{The \aluni\ \kb\ corresponding to the \oo\ schema in
   Figure~\protect{\ref{fig-oom-example}}}
  \label{fig-oom-example-kb}
\end{figure}

\begin{exampleCont}{\ref{example-oom-oo-schema}}
We illustrate the translation on the fragment of \oo\ schema in
Figure~\ref{fig-oom-example}.  The corresponding \aluni\ \kb\ is shown in
Figure~\ref{fig-oom-example-kb}.
%%
\endmarkfull
\end{exampleCont}

Below we discuss the effectiveness of the translation $\OOmaprel$.  First of
all observe that the \aluni\ \kb\ $\OOS$ resulting from the translation
of an \oo\ schema $\S$ may admit models that do not have a direct counterpart
among legal \db\ instances of $\S$.
%%
More precisely, both an interpretation of $\OOS$ and a \db\ instance of $\S$
can be viewed as a directed labeled graph: In the case of an interpretation,
the nodes are domain individuals and the arcs are labeled with roles.  In the
case of a \db\ instance, the nodes are either object identifiers or active
values, and an arc either connects an object identifier to its associated value
(in which case it is labeled with \OOvalue), or is part of the sub-structure
representing a set or record value (in which case it is labeled with \OOmember\
or with an attribute, in accordance with the type of the value).
%%
In a legal database instance of $\S$, a value $v$ is represented by a
sub-structure that has the form of a finite tree with $v$ as root, set and
record values as intermediate nodes, and objects identifiers as leaves.
Clearly, such a substructure does not contain cycles.
%%
Conversely, in a model of $\OOS$, there may be cycles involving only nodes that
are instances of \SetType\ and \RecType\ and in which all roles are different
from \OOvalue.  We call such cycles \emph{bad}.  A model containing bad cycles
cannot be put directly in correspondence with a legal database instance. Also,
due to the open semantics of records one cannot adopt a different translation
for which bad cycles in the model are ruled out.

\begin{figure}[tbp]
  \centering
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  \input{cyclic-model.pstex_t}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{picture}(0,0)%
\epsfig{file=cyclic-model.pstex}%
\end{picture}%
\setlength{\unitlength}{0.00087500in}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(4715,1785)(708,-1489)
\put(901, 74){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$o_1$}}}
\put(1801, 74){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$v_1$}}}
\put(2701, 74){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$v_2$}}}
\put(2251,-826){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$o_2$}}}
\put(3151,-826){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$v_3$}}}
\put(4051,-826){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$v_4$}}}
\put(4951,-826){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$v_5$}}}
\put(2251,-1186){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$C$}}}
\put(901,-286){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$C$}}}
\put(1486,-241){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\RecType}}}
\put(3151,-1141){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\RecType}}}
\put(4051,-1141){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\RecType}}}
\put(5131,-1141){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\RecType}}}
\put(2881,-241){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\RecType}}}
\put(2251,164){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_1$}}}
\put(3601,-736){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_1$}}}
\put(2251,-376){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_2$}}}
\put(4501,-736){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_2$}}}
\put(3601,-1456){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_3$}}}
\put(1891,-691){\makebox(0,0)[rb]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_3$}}}
\put(1351,164){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\OOvalue}}}
\put(2701,-736){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\OOvalue}}}
\end{picture}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \caption{A model containing cycles}
  \label{fig-oom-cyclic-model}
\end{figure}

\begin{example} \label{example-oom-cyclic-model}
Consider the \oo\ schema $\S$, containing a single class declaration
\[
\OOclass\ C\ \OOtypeis\
  \OOrecord\ a_1: \OOrecord\ a_2: \OOrecord\ a_3:C\ \OOend\ \OOend\ \OOend
\]
which is translated to
\[
  C \ISAs 
    \begin{array}[t]{@{}l}
      \AbstractClass\ \AND\\
      \ALL{\OOvalue}{(\RecType \AND \EEXACTLY{1}{a_1} \AND
       \ALL{a_1}{(\RecType \AND \EEXACTLY{1}{a_2} \AND
        \ALL{a_2}{(\RecType \AND \EEXACTLY{1}{a_3} \AND \ALL{a_3}{C})})})}.
    \end{array}
\]
%%
Figure~\ref{fig-oom-cyclic-model} shows a model of $\OOS$ represented as a
graph. For clarity, we have named the instances of $C$, and hence of
\AbstractClass, with $o$ and the instances of \RecType\ with $v$.  Observe the
two different types of cycles in the graph.  The cycle involving individuals
$o_2, v_3, v_4$, and $v_5$ does not cause any problems since it contains an arc
labeled with \OOvalue, which is not part of the structure constituting a
complex value.  In fact, $v_3$ represents the record value
$\OOtup{\inc{a_1}{\OOtup{\inc{a_2}{\OOtup{\inc{a_3}{o_2}}}}}}$. On the other
hand, due to the bad cycle involving $v_1$ and $v_2$, individual $v1$
represents (together with $o_2$ connected via $a_3$ to $v_1$) a record of
infinite depth.
%%
\endmarkfull
\end{example}

We can nevertheless establish a correspondence from finite models of $\OOS$
possibly containing bad cycles to legal instances of the \oo\ schema $\S$.
This can be achieved by unfolding the bad cycles in a model of $\OOS$ to
infinite trees. Obviously, the unfolding of a cycle into an infinite tree,
generates an infinite number of nodes, which would correspond to an infinite
database state.  However, we can restrict the duplication of individuals to
those that represent set and record values, and thus are instances of \SetType\ 
and \RecType. The instances of \AbstractClass, instead, are not duplicated in
the process of unfolding, and therefore their number remains finite.  Moreover,
since the set of possible active values associated with each object identifier
is bound by the depth of the schema, we can in fact block the unfolding of bad
cycles to the finite tree of depth equal to the depth of the schema.

Let us first formally define the \emph{depth} of an \oo\ schema $\S$.

\begin{definition}
  For a type expression $T$ we define $\depth(T)$ inductively as follows:
  \[\depth(T) \defas
    \cases{%
     0,                                     &if $T=C$.\cr
     \max_{1\leq i\leq k}(\depth(T_i)),     &if $T=\Tunion{T}{k}$.\cr
     1 + \depth(T'),                        &if $T=\Tset{T'}$.\cr
     1 + \max_{1\leq i\leq k}(\depth(T_i)), &if $T=\Trecord{A}{T}{k}$.}
  \]
  The \emph{depth} of an \oo\ schema $\S$ is defined as the maximum of
  $\depth(T)$ for a type expression $T$ in $\S$.
  %%
  \endmarkfull
\end{definition}

We can now introduce the notion of unfolding of an \aluni\ interpretation.
\begin{definition}
  Let $\S$ be an \oo\ schema, $\OOS$ its translation in \aluni\ and $\I$ a
  finite interpretation of $\OOS$.  We call \emph{unfolded version} of $\I$ the
  interpretation obtained from $\I$ as follows: For each individual $v$ that is
  part of a bad cycle,
  %% and that has an incoming arc labeled with \OOvalue,
  unfold the bad cycle into an (infinite) tree having $v$ as root, by
  generating new individuals only for the instances of \RecType\ and \SetType.
  %%
  For a nonnegative integer $m$, we call \emph{$m$-unfolded version} of $\I$,
  denoted as $\I_{|m}$, the interpretation obtained by truncating at depth $m$
  each infinite tree generated in the process of unfolding.
  %%
  \endmarkfull
\end{definition}

\begin{figure}[tbp]
  \centering
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  \input{tree-model.pstex_t}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{picture}(0,0)%
\epsfig{file=tree-model.pstex}%
\end{picture}%
\setlength{\unitlength}{0.00087500in}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(5593,2235)(708,-1939)
\put(901, 74){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$o_1$}}}
\put(901,-286){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$C$}}}
\put(1486,-241){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\RecType}}}
\put(1891,-691){\makebox(0,0)[rb]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_3$}}}
\put(1351,164){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\OOvalue}}}
\put(2701, 74){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$v_2^0$}}}
\put(4051,164){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_1$}}}
\put(5851,164){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_1$}}}
\put(2251,164){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_1$}}}
\put(2701,-241){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\RecType}}}
\put(3151,164){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_2$}}}
\put(4951,164){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_2$}}}
\put(3151,-1276){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$v_3$}}}
\put(4051,-1276){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$v_4$}}}
\put(4951,-1276){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$v_5$}}}
\put(2251,-1636){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$C$}}}
\put(3151,-1591){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\RecType}}}
\put(4051,-1591){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\RecType}}}
\put(5131,-1591){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\RecType}}}
\put(3601,-1186){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_1$}}}
\put(4501,-1186){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_2$}}}
\put(3601,-1906){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_3$}}}
\put(3601,-241){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\RecType}}}
\put(6301,-61){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$\ldots$}}}
\put(4366,-241){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\RecType}}}
\put(1801, 74){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$v_1^0$}}}
\put(3601, 74){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$v_1^1$}}}
\put(4501, 74){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$v_2^1$}}}
\put(5401, 74){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$v_1^2$}}}
\put(5536,-241){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\RecType}}}
\put(3331,-691){\makebox(0,0)[rb]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_3$}}}
\put(2476,-691){\makebox(0,0)[rb]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$a_3$}}}
\put(2836,-1186){\makebox(0,0)[b]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\OOvalue}}}
\put(2116,-1456){\makebox(0,0)[rb]{\smash{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}$o_2$}}}
\end{picture}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \caption{The unfolded version of the model in
   Figure~\protect{\ref{fig-oom-cyclic-model}}}
  \label{fig-oom-tree-model}
\end{figure}

\begin{exampleCont}{\ref{example-oom-cyclic-model}}
Figure~\ref{fig-oom-tree-model} shows the unfolded version of the model in
Figure~\ref{fig-oom-cyclic-model}. Notice that only the bad cycle has been
unfolded to an infinite tree, and that all arcs labeled with $a_3$ lead to
$o_2$, which is an instance of \AbstractClass\ and has not been duplicated.
%%
\endmarkfull
\end{exampleCont}

The correctness of $\OOS$ is sanctioned by the following proposition.

\begin{proposition} \label{prop-oom-correspondence}
  For every \oo\ schema $\S$ of depth $m$, there exist mappings:
  \begin{enumerate}
  \item $\alphaS$ from instances of $\S$ into finite interpretations of $\OOS$
    and $\alphaV$ from active values of instances of $\S$ into domain elements
    of the finite interpretations of $\OOS$ such that:
    %%
    For each legal instance $\J$ of $\S$, $\alphaS(\J)$ is a finite model
    of $\OOS$, and for each type expression $T$ of $\S$ and each $v\in\Vact$,
    $v\in\IntJ{T}$ if and only if
    $\alphaV(v)\in\INT[\alphaS(\J)]{\OOmap{T}}$.
  \item $\betaS$ from finite interpretations of $\OOS$ into instances of $\S$
    and $\betaV$ from domain elements of the $m$-unfolded versions of the
    finite interpretations of $\OOS$ into active values of instances of $\S$,
    such that:
    %%
    For each finite model $\I$ of $\OOS$, $\betaS(\I)$ is a legal instance of
    $\S$, and for each concept $\OOmap{T}$, which is the translation of a type
    expression $T$ of $\S$ and each $d\in\domm$, $d\in\INTm{\OOmap{T}}$ if and
    only if $\betaV(d)\in\Int[\betaS(\I)]{T}$.
  \end{enumerate}
\end{proposition}

\begin{proof} %
(1) Given a database instance $\J$ we define an interpretation $\alphaS(\J)$ of
$\OOS$ as follows:
\begin{itemize} \itemsep 0cm
\item $\alphaV$ is a function mapping every element of $\Vact$ into a distinct
  element of $\dom[\alphaS(\J)]$.  Therefore $\dom[\alphaS(\J)]$ is defined as
  the set of elements $\alphaV(v)$ such that $v\in\Vact$. %
  Moreover we denote with $\Delta_{id}$, $\Delta_{rec}$, and $\Delta_{set}$ the
  elements of $\dom[\alphaS(\J)]$ corresponding to object identifiers, record
  and set values, respectively.
\item The interpretation of atomic concepts is defined as follows:
  \[
    \begin{array}{@{}rcl@{}}
      \INT[\alphaS(\J)]{\OOmap{C}} &\defas& \set{\alphaV(o)\mid o\in\piJ(C)},\\
      &&\quad\mbox{for every $\OOmap{C}$ corresponding to a class name $C$ in
                   $\S$}\\
      \Int[\alphaS(\J)]{\AbstractClass} &\defas& \Delta_{id}\\
      \Int[\alphaS(\J)]{\RecType} &\defas& \Delta_{rec}\\
      \Int[\alphaS(\J)]{\SetType} &\defas& \Delta_{set}\\
    \end{array}
  \]
\item The interpretation of atomic roles is defined as follows:
  \[
    \begin{array}{@{}rcl@{}}
      \INT[\alphaS(\J)]{\OOmap{A}} &\defas&
        \set{(d_1,d_2) \mid d_1\in\Delta_{rec} \mbox{ and }
        \alphaV^{-1}(d_1)=\OOtup{\ldots,\inc{A}{\alphaV^{-1}(d_2)},\ldots}},\\
      &&\quad\mbox{for every $\OOmap{A}$ corresponding to an attribute name $A$
                   in $\S$}\\
      \Int[\alphaS(\J)]{\OOmember} &\defas&
        \set{(d_1,d_2) \mid d_1\in\Delta_{set} \mbox{ and }
         \alphaV^{-1}(d_1)=\OOset{\ldots,\alphaV^{-1}(d_2),\ldots}}\\
      \Int[\alphaS(\J)]{\OOvalue} &\defas&
        \set{(d_1,d_2) \mid (\alphaV^{-1}(d_1),\alphaV^{-1}(d_2))\in\rhoJ}
    \end{array}
  \]
\end{itemize}

We prove that for each type $T$ and each $v\in\Vact$, $v\in\IntJ{T}$ if and
only if $\alphaV(v)\in\INT[\alphaS(\J)]{\OOmap{T}}$.  The first part of the
thesis then follows from the definition of $\alphaS(\J)$.  The proof is by
induction on the structure of the type expression.

Base case: $T=C$ (i.e., $T$ is a class name). %
If $o\in\IntJ{C}$ then $\alphaV(o)\in\INT[\alphaS(\J)]{\OOmap{C}}$, and
vice-versa if $d\in\INT[\alphaS(\J)]{\OOmap{C}}$ then
$\alphaV^{-1}(d)\in\IntJ{C}$.

Inductive case: $T=\Trecord{A}{T}{k}$ and $\OOmap{T}=\RecType \AND
\ALL{\OOmap{A_1}}{\OOmap{T_1}} \AND \EEXACTLY{1}{\OOmap{A_1}} \cd{\AND}
\ALL{\OOmap{A_k}}{\OOmap{T_k}} \AND \EEXACTLY{1}{\OOmap{A_k}}$. 
%%
We assume that $v\in\IntJ{T_i}$ iff
$\alphaV(v)\in\INT[\alphaS(\J)]{\OOmap{T_i}}$, for $i\in\setone{k}$, and show
that $v\in\IntJ{T}$ iff $\alphaV(v)\in\INT[\alphaS(\J)]{\OOmap{T}}$.

Suppose that $v\in\IntJ{T}$, i.e., $v=\OOtuple{A}{v}{h}$ with $h\geq k$ and
$v_i\in\IntJ{T_i}$ for $i\in\setone{k}$.  By induction hypothesis
$\alphaV(v_i)\in\INT[\alphaS(\J)]{\OOmap{T_i}}$, for $i\in\setone{k}$, and by
definition of $\alphaS$, $\alphaV(v)\in\Int[\alphaS(\J)]{\RecType}$,
$(\alphaV(v),\alphaV(v_i))\in\INT[\alphaS(\J)]{\OOmap{A_i}}$ for
$i\in\setone{k}$, and all roles $\OOmap{A}$ corresponding to attribute names
are functional.  Therefore, $\alphaV(v)\in\INT[\alphaS(\J)]{\OOmap{T}}$.

Conversely, suppose that $d=\alphaV(v)\in\INT[\alphaS(\J)]{\OOmap{T}}$.  Then,
for each $i\in\setone{k}$ there is exactly one $d_i\in\dom[\alphaS(\J)]$ such
that $(d,d_i)\in\INT[\alphaS(\J)]{\OOmap{A_i}}$, and moreover
$d_i\in\INT[\alphaS(\J)]{\OOmap{T_i}}$.  By definition of $\alphaS$ we have
$v=\OOtuple{A}{v}{h}$, with $h\geq k$ and $v_i=\alphaV^{-1}(d_i)$, for
$i\in\setone{k}$.  By induction hypothesis $v_i\in\IntJ{T_i}$, for
$i\in\setone{k}$, and therefore $v\in\INT[\J]{\Trecord{A}{T}{k}}$.

The cases for $T=\Tunion{T}{k}$ and $T=\Tset{T'}$ can be treated analogously.

\vspace{\baselineskip}
(2) Given a finite model $\I$ of $\OOS$ of depth $m$, we define a legal \db\ 
instance $\betaS(\I)$ as follows:
\begin{itemize}
\item $\betaV$ is a function mapping every element of $\domm$
  into a distinct element of $\Vact[\betaS(\I)]$ such that the following
  conditions are satisfied:
  \begin{itemize}
  \item $\Oid[\betaS(\I)]\incl\Vact[\betaS(\I)]$ is the set of elements
    $\betaV(d)$ such that $d\in\Intm{\AbstractClass}$.
  \item If $d\in\Intm{\RecType}$, $(d,d_i)\in\INTm{\OOmap{A_i}}$, for
    $i\in\setone{k}$, and there is no other individual $d'\in\domm$ and
    attribute $A'$ such that $(d,d')\in\INTm{\OOmap{A'}}$, then
    $\betaV(d)=\OOtup{\inc{A_1}{\betaV(d_1)}\cld\inc{A_k}{\betaV(d_k)}}$.
  \item If $d\in\Intm{\SetType}$, $(d,d_i)\in\Intm{\OOmember}$, for
    $i\in\setone{k}$, and there is no other individual $d'\in\domm$ such that
    $(d,d')\in\INTm{\OOmember}$, then
    $\betaV(d)=\set{\betaV(d_1)\cld\betaV(d_k)}$.
  \end{itemize}
\item For every class name $C$,
  $\pi^{\betaS(\I)}(C)\defas\set{\betaV(d)\mid d\in\INTm{\OOmap{C}}}$.
\item $\rho^{\betaS(\I)} \defas
  \set{(o,v)\mid\betaV(d_1)=o,\betaV(d_2)=v,\textrm{ and }
   (d_1,d_2)\in\Intm{\OOvalue}}$.
\end{itemize}

We first prove that for each concept $\OOmap{T}$, which is the translation of a
type expression $T$ of $\S$, and each $d\in\domm$, $d\in\INTm{\OOmap{T}}$ if
and only if $\betaV(d)\in\Int[\betaS(\I)]{T}$.  The proof is by induction on
the structure of the concept expression.  Again for the inductive part we
restrict our attention to the case of record types.

Base case: $T=C$ (i.e., $\OOmap{T}$ is an atomic concept). %
If $d\in\INTm{\OOmap{C}}$ then $\betaV(d)\in\Int[\betaS(\I)]{C}$, and
vice-versa if $o\in\Int[\betaS(\I)]{C}$ then
$\betaV^{-1}(o)\in\INTm{\OOmap{C}}$.

Inductive case: $\OOmap{T}=\RecType \AND \ALL{\OOmap{A_1}}{\OOmap{T_1}} \AND
\EEXACTLY{1}{\OOmap{A_1}} \cd{\AND} \ALL{\OOmap{A_k}}{\OOmap{T_k}} \AND
\EEXACTLY{1}{\OOmap{A_k}}$ and $T=\Trecord{A}{T}{k}$.
%%
We assume that $d\in\INTm{\OOmap{T_i}}$ iff
$\betaV(d)\in\Int[\betaS(\I)]{T_i}$, for $i\in\setone{k}$, and show that
$d\in\INTm{\OOmap{T}}$ iff $\betaV(d)\in\Int[\betaS(\I)]{T}$.

Suppose that $d\in\INTm{\OOmap{T}}$.  Then $d\in\Intm{\RecType}$ and for each
$i\in\setone{k}$ there is an individual $d_i$ such that
$d_i\in\INTm{\OOmap{T_i}}$ and $(d,d_i)\in\INTm{\OOmap{A_i}}$.  By construction
$\betaV(d)=\OOtuple{A}{v}{h}$ for some $h\geq k$.  Moreover, by induction
hypothesis $\betaV(d_i)\in\Int[\betaS(\I)]{T_i}$ and therefore
$\betaV(d)\in\Int[\betaS(\I)]{T}$.

Conversely, suppose that $\betaV(d)\in\Int[\betaS(\I)]{T}$, i.e.,
$\betaV(d)=\OOtuple{A}{v}{h}$ with $h\geq k$ and $v_i\in\Int[\betaS(\I)]{T_i}$
for $i\in\setone{k}$.  By induction hypothesis
$d_i=\betaV^{-1}(v_i)\in\INTm{\OOmap{T_i}}$, for $i\in\setone{k}$, and by
definition of $\betaV$, $d\in\Intm{\RecType}$ and
$(d,d_i)\in\INTm{\OOmap{A_i}}$, for $i\in\setone{k}$.  Since all roles
$\OOmap{A}$ corresponding to attribute names are functional,
$d\in\INTm{\OOmap{T}}$.

It remains to show that for each declaration
\[\Tisa{C}{\dd{C}{n}}{T}\]
in $\DS$, (a)~$\Int[\betaS(\I)]{C}\incl\Int[\betaS(\I)]{C_i}$ for each
$i\in\setone{n}$, and
(b)~$\rho^{\betaS(\I)}(\Int[\betaS(\I)]{C})\incl\Int[\betaS(\I)]{T}$.

(a)~follows from the fact that $\OOS$ contains the assertion
$\OOmap{C}\ISA\OOmap{C_1}\cd{\AND}\OOmap{C_n}$ and from the definition of
$\pi^{\betaS(\I)}$.

(b)~follows from what we have shown above and from the fact that $\I_{|m}$
still satisfies the assertion
$\OOmap{C}\ISA\AbstractClass\AND\ALL{\OOvalue}{\OOmap{T}}$.
%%
In fact, for some $d\in\INT{\OOmap{C}}$ let $d'$ be the unique individual such
that $(d,d')\in\Int{\OOvalue}$. Since $\I$ is a model of $\OOS$,
$d'\in\INT{\OOmap{T}}$.  We argue that also $d'\in\INTm{\OOmap{T}}$.
%%
If $d'$ is not part of a bad cycle in $\I$, then $\I$ and $\I_{|m}$ coincide on
the sub-structure rooted at $d'$ and formed by the individuals reached via
$\OOmember$ and roles corresponding to attributes, and we are done.
%%
Otherwise, in $\I_{|m}$ such sub-structure is expanded into a finite tree.
Since by construction the depth of this tree is at least $\depth(T)$, and the
connections between individuals in $\I$ are preserved in $\I_{|m}$, it follows
that $d'\in\INTm{\OOmap{T}}$.
\end{proof}

The basic reasoning services considered in \oo\ \dbs\ are subtyping (check
whether a type denotes a subset of another type in every legal instance) and
type consistency (check whether a type is consistent in a legal instance).
Based on Proposition~\ref{prop-oom-correspondence}, we can show that these
forms of reasoning are fully captured by finite concept consistency and finite
concept subsumption in \aluni\ \kbs.

\begin{theorem} \label{thm-oom-correspondence}
  Let $\S$ be an \oo\ schema, $T,T'$ two type expressions in $\S$, and $\OOS$
  the translation of $\S$.  Then the following holds:
  \begin{enumerate}
  \item $T$ is consistent in $\S$ if and only if
    $\classcons[f]{\OOS}{\OOmap{T}}$.
  \item $T$ is a subtype of $T'$ in $\S$ if and only if
    $\subs[f]{\OOS}{\OOmap{T}}{\OOmap{T'}}$.
  \end{enumerate}
\end{theorem}

\begin{proof}
The proof is analogous to the proof of Theorem~\ref{thm-sdm-correspondence},
but it makes use of Proposition~\ref{prop-oom-correspondence} instead of
Proposition~\ref{prop-sdm-correspondence}.
\end{proof}

Again, the correspondence with \aluni\ established by
Theorem~\ref{thm-oom-correspondence} allows us to make use of the reasoning
techniques developed for \aluni\ to reason on object-oriented schemas.
%%
Observe that reasoning in object-oriented models is already
PSPACE-hard \cite{BeNe94} and thus the known algorithms are exponential.
%%
However, by resorting to \aluni, it becomes possible to take into account for
reasoning also various extensions of the object-oriented formalism.  Such
extensions are useful for conceptual modeling and have already been proposed in
the literature \cite{CaBa97}.  First of all, the same considerations developed
for the ER model with regard to the use of arbitrary boolean constructs on
classes can be applied also in the object-oriented setting, which provides
disjunction but does not admit any form of negation.  Additional features that
can be added to object oriented models are inverses of attributes, cardinality
constraints on set-valued attributes, and more general forms of restrictions on
the values of attributes.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%\input{6-related}
\section{Related Work}
\label{sec-related}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

In this section we briefly discuss recent results on the correspondence between
class-based formalisms and on techniques for reasoning in \aluni\ and in
class-based representation formalisms.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Relationships among Class-Based Formalisms}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

In the past there have been several attempts to establish relationships among
class-based formalisms.  \citeA{BlHR90,LeNS91} carry out a comparative analysis
of class-based languages and attempt to provide a unified view.  The analysis
makes it clear that several difficulties arise in identifying a common
framework for the formalisms developed in different areas.  Some recent papers
address this problem.  For example, an analysis of the relationships between
frame-based languages and types in programming languages has been carried out
by \citeA{Borg92}, while \citeA{BeSa92,PiSS92} use frame-based languages to
enrich the deductive capabilities of semantic and object-oriented data models.

\citeA{ArCS96} study reasoning in object-oriented data models by presenting a
translation to DLs in the style of the one discussed in Section~\ref{sec-oom}.
However, the proposed translation is applicable only in the case where the
shema contains no recursive class declarations.  This limitation is not present
in the work by \citeA{BeNe94}, where a formalism derived from DLs is used to
model complex objects and an algorithm for computing subsumption between
classes is provided.

A recent survey on the application of DLs to the problem of data management has
been presented by \citeA{Borg95} .  The application to the task of data
modeling of reasoning techniques derived from the correspondences presented in
Sections~\ref{sec-sdm} and~\ref{sec-oom} is discussed in more detail by
\citeA{CaLN98}.

Recently, there have also been proposals to integrate the object-oriented and
the logic programming paradigms \cite{KiWu93,KiLW95}.  These proposals are
however not directly related to the present work, since they aim at providing
mechanisms for computing with structured objects, rather than means for
reasoning over a conceptual (object-oriented) representation of the domain of
interest.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Reasoning in \aluni\ and in Class-Based Representation Formalisms}
\label{sec-reasoning}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\aluni\ is equipped with techniques to reason both with respect to unrestricted
and with respect to finite models.  We briefly sketch the main ideas underlying
reasoning in both contexts.  A detailed account of the reasoning techniques has
been carried out by \citeA{Calv96}.

\subsubsection{Unrestricted Model Reasoning}

We remind that reasoning on a knowledge base with respect to unrestricted
models amounts to check either concept consistency, i.e., determine whether the
knowledge base admits a (possibly infinite) model in which a given concept has
a nonempty extension, or concept subsumption, i.e., determine whether the
extension of one concept is contained in the extension of another concept in
every model (including the infinite ones) of the knowledge base.

The method to reason in \aluni\ with respect to unrestricted models exploits a
well known correspondence between DLs and Propositional Dynamic Logics (PDLs)
\cite{KoTi90}, which are a class of logics specifically designed to reason
about programs.  The correspondence, which has first been pointed out by
\citeA{Schi91}, relies on a substantial similarity of the interpretative
structures of both formalisms, and allows one to exploit the reasoning
techniques developed for PDLs to reason in the corresponding DLs.  In
particular, since $\ALUNI$, the description language of \aluni, includes the
construct for inverse roles, for the correspondence one has to resort to
\emph{converse-PDL}, a variant of PDL that includes converse programs
\cite{KoTi90}.  However, because of the presence of number restrictions in
$\ALUNI$ which have no direct correspondence in PDLs, we cannot rely on
traditional techniques for reasoning in PDLs.  Recently, encoding techniques
have been developed, which allow one to eliminate number restrictions from a
knowledge base while preserving concept consistency and concept subsumption
\cite{DeLe94}.  The encoding is applicable to knowledge bases formulated in
expressive variants of DLs, and in particular it can be used to reduce
unrestricted model reasoning on \aluni\ knowledge bases (both concept
consistency and concept subsumption) to deciding satisfiability of a formula of
converse-PDL.  Reasoning in converse-PDL is decidable in EXPTIME \cite{KoTi90},
and since the encoding is polynomial \cite{DeLe94} we obtain an EXPTIME
decision procedure for unrestricted concept consistency and concept subsumption
in \aluni\ knowledge bases.  A simplified form of the encoding, which can be
applied to decide unrestricted concept consistency in \aluni\ has also been
presented by \citeA{CaLN94}.

\subsubsection{Finite Model Reasoning}

We remind that reasoning on a knowledge base with respect to finite models
amounts to check either finite concept consistency or finite concept
subsumption, for which only the \emph{finite} models of the knowledge base must
be considered.

%% We remind that reasoning on a knowledge base with respect to finite models
%% amounts to check either finite concept consistency, i.e., determine whether
%% the knowledge base admits a finite model in which the concept has a nonempty
%% extension, or finite concept subsumption, i.e., determine whether the
%% extension of one concept is contained in the extension of another concept in
%% every finite model of the knowledge base.

For finite model reasoning, the techniques based on a reduction to reasoning in
PDLs are not applicable.  Indeed, the PDL formula corresponding to an \aluni\ 
knowledge base contains constructs both for converse programs (corresponding to
inverse roles) and for functionality of direct and inverse programs, and thus
is a formula of a variant of PDL which does not have the finite model
property \cite{Vard85}.  However, after encoding functionality, one obtains a
converse-PDL formula, and since converse-PDL has the finite model
property \cite{FiLa79}, this formula is satisfiable if and only if it is
finitely satisfiable.  This shows that the encoding of number restrictions (and
in particular the encoding of functionality), while preserving unrestricted
satisfiability does not preserve finite satisfiability \cite{DeLe94}.

For finite model reasoning in \aluni\ one can adopt a different technique,
which is based on the idea of separating the reasoning process in two distinct
phases \cite<see>[for full details]{Calv96}.  The first phase deals with all
constructs except number restrictions, and builds an ``expanded knowledge
base'' in which these constructs are embedded implicitly in the concepts and
roles.  In the second phase the assertions involving number restrictions are
used to derive from this expanded knowledge base a system of linear
inequalities. The system is defined in such a way that its solutions of a
certain type (acceptable solutions) are directly related to the finite models
of the original knowledge base.  In particular, from each acceptable solution
one can directly deduce the cardinalities of the extensions of all concepts and
roles in a possible finite model.  The proposed method allows one to establish
for \aluni\ EXPTIME decidability for finite concept consistency and for special
cases of finite concept subsumption.  By resorting to a more complicated
encoding one can obtain a 2EXPTIME decision procedure for finite concept
subsumption in \aluni\ in general \cite{Calv96d,Calv96}.

Reasoning with respect to finite models has also been investigated in the
context of dependency theory in \dbs.  As shown by \citeA{CaFP84} for the
relational model, when functional and inclusion dependencies interact, the
dependency implication problem in the finite case differs from the one in the
unrestricted case.  While the implication problem for arbitrary functional and
inclusion dependencies is undecidable \cite{ChVa85,Mitc83}, for functional and
unary inclusion dependencies it is solvable in polynomial time, both in the
finite and the unrestricted case \cite{CoKV90}.

Consistency with respect to finite models of schemata expressed in an enriched
Entity-Relationship model with cardinality constraints has been shown decidable
in polynomial time by \citeA{LeNo90}.  \citeA{CaLe94} extend the decidability
result to include also ISA relationships, and \citeA{CaLe94b} show EXPTIME
decidability of reasoning in an expressive object-oriented model.  An algorithm
for computing a refinement ordering for types (the analogue to a concept
hierarchy) in the framework of the O$_2$ object oriented model in discussed
by \citeA{LeRi89}.

Reasoning in the strict sublanguage of \aluni\ obtained by omitting inverse
roles and number restrictions is already EXPTIME-hard \cite{Calv96c}.
Therefore, the known algorithms for deciding unrestricted concept consistency
and subsumption and finite concept consistency are essentially optimal.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%\input{7-conclusions}
\section{Conclusions}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We have presented a unified framework for representing information about class
structures and reasoning about them.  We have pursued this goal by looking at
various class-based formalisms proposed in different fields of computer
science, namely frame based systems used in knowledge representation, and
semantic and \oo\ data models used in databases, and rephrasing them in the
framework of description logics.  The resulting description logic, called
\aluni\ includes a combination of constructs that was not addressed before,
although all of the constructs had previously been considered separately.

The major achievement of the paper is the demonstration that class-based
formalisms can be given a precise characterization by means of a powerful
fragment of first-order logic, which thus can be regarded as the essential core
of the class-based representation formalisms belonging to all three families
mentioned above. This has several consequences.

First of all, any of the formalisms considered in the paper can be enriched
with constructs originating from other formalisms and treated in the general
framework. In this sense, the work reported here not only provides a common
powerful representation formalism, but may also contribute to significant
developments for the languages belonging to all the three families.  For
example, the usage of inverse roles in concept languages greatly enhances the
expressivity of roles, while the combination of ISA, number restrictions, and
union enriches the reasoning capabilities available in semantic data models.

Secondly, the comparison of class-based formalisms from the fields of knowledge
representation and conceptual data modeling makes it feasible to address the
development of reasoning tools to support conceptual modeling \cite{CaLN98}. In
fact, reasoning capabilities become especially important in complex scenarios
such as those arising in heterogenous database applications and Data
Warehousing.  This line of work was among the motivations for developing
systems based on expressive description logics \cite{Horr98,HoPa99}, and has
lead to further extending the language of description logics to support
Information Integration and, more specifically, the conceptual modeling of Data
Warehouses \cite{CDLNR98}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%\bibliographystyle{theapa}
%%\bibliography{main-bib}
\begin{thebibliography}{}

\bibitem[\protect\BCAY{Abiteboul, Kanellakis, Ramaswamy, \BBA\
  Waller}{Abiteboul et~al.}{1992}]{AKRW92}
Abiteboul, S., Kanellakis, P., Ramaswamy, S., \BBA\ Waller, E. \BBOP1992\BBCP.
\newblock \BBOQ Method schemas\BBCQ\
\newblock \BTR\ CS-92-33, Brown University.
\newblock An earlier version appeared in {\sl Proc.\ of the 9th Symp.\ on
  Principles of Database Systems PODS-90}.

\bibitem[\protect\BCAY{Abiteboul \BBA\ Kanellakis}{Abiteboul \BBA\
  Kanellakis}{1989}]{AbKa89}
Abiteboul, S.\BBACOMMA\  \BBA\ Kanellakis, P. \BBOP1989\BBCP.
\newblock \BBOQ Object identity as a query language primitive\BBCQ\
\newblock In {\Bem Proceedings of the ACM SIGMOD International Conference on
  Management of Data}, \BPGS\ 159--173.

\bibitem[\protect\BCAY{Abrial}{Abrial}{1974}]{Abri74}
Abrial, J.~R. \BBOP1974\BBCP.
\newblock \BBOQ Data semantics\BBCQ\
\newblock In Klimbie, J.~W.\BBACOMMA\  \BBA\ Koffeman, K.~L.\BEDS, {\Bem Data
  Base Management}, \BPGS\ 1--59. North-Holland Publ.\ Co., Amsterdam.

\bibitem[\protect\BCAY{Albano, Ghelli, \BBA\ Orsini}{Albano
  et~al.}{1991}]{AlGO91}
Albano, A., Ghelli, G., \BBA\ Orsini, R. \BBOP1991\BBCP.
\newblock \BBOQ A relationship mechanism for strongly typed {O}bject-{O}riented
  database programming languages\BBCQ\
\newblock In {\Bem Proceedings of the Seventeenth International Conference on
  Very Large Data Bases (VLDB'91)}, \BPGS\ 565--575\ Barcelona.

\bibitem[\protect\BCAY{Artale, Cesarini, \BBA\ Soda}{Artale
  et~al.}{1996}]{ArCS96}
Artale, A., Cesarini, F., \BBA\ Soda, G. \BBOP1996\BBCP.
\newblock \BBOQ Describing database objects in a concept language
  environment\BBCQ\
\newblock {\Bem {IEEE} Transactions on Knowledge and Data Engineering}, {\Bem
  8\/}(2), 345--351.

\bibitem[\protect\BCAY{Atzeni \BBA\ {Parker Jr.}}{Atzeni \BBA\ {Parker
  Jr.}}{1986}]{AtPa86}
Atzeni, P.\BBACOMMA\  \BBA\ {Parker Jr.}, D.~S. \BBOP1986\BBCP.
\newblock \BBOQ Formal properties of net-based knowledge representation
  schemes\BBCQ\
\newblock In {\Bem Proceedings of the Second IEEE International Conference on
  Data Engineering (ICDE'86)}, \BPGS\ 700--706\ Los Angeles.

\bibitem[\protect\BCAY{Baader}{Baader}{1991}]{Baad91}
Baader, F. \BBOP1991\BBCP.
\newblock \BBOQ Augmenting concept languages by transitive closure of roles: An
  alternative to terminological cycles\BBCQ\
\newblock In {\Bem Proceedings of the Twelfth International Joint Conference on
  Artificial Intelligence (IJCAI'91)}\ Sydney, Australia.

\bibitem[\protect\BCAY{Baader}{Baader}{1996}]{Baad96b}
Baader, F. \BBOP1996\BBCP.
\newblock \BBOQ Using automata theory for characterizing the semantics of
  terminological cycles\BBCQ\
\newblock {\Bem Annals of Mathematics and Artificial Intelligence}, {\Bem 18},
  175--219.

\bibitem[\protect\BCAY{Batini, Ceri, \BBA\ Navathe}{Batini
  et~al.}{1992}]{BaCN92}
Batini, C., Ceri, S., \BBA\ Navathe, S.~B. \BBOP1992\BBCP.
\newblock {\Bem Conceptual Database Design, an {E}ntity-{R}elationship
  Approach}.
\newblock Benjamin and Cummings Publ.\ Co., Menlo Park, California.

\bibitem[\protect\BCAY{Bergamaschi \BBA\ Nebel}{Bergamaschi \BBA\
  Nebel}{1994}]{BeNe94}
Bergamaschi, S.\BBACOMMA\  \BBA\ Nebel, B. \BBOP1994\BBCP.
\newblock \BBOQ Acquisition and validation of complex object database schemata
  supporting multiple inheritance\BBCQ\
\newblock {\Bem Applied Intelligence}, {\Bem 4\/}(2), 185--203.

\bibitem[\protect\BCAY{Bergamaschi \BBA\ Sartori}{Bergamaschi \BBA\
  Sartori}{1992}]{BeSa92}
Bergamaschi, S.\BBACOMMA\  \BBA\ Sartori, C. \BBOP1992\BBCP.
\newblock \BBOQ On taxonomic reasoning in conceptual design\BBCQ\
\newblock {\Bem {ACM} Transactions on Database Systems}, {\Bem 17\/}(3),
  385--422.

\bibitem[\protect\BCAY{Bl{\"a}sius, Hedst{\"u}ck, \BBA\ Rollinger}{Bl{\"a}sius
  et~al.}{1990}]{BlHR90}
Bl{\"a}sius, K.~H., Hedst{\"u}ck, U., \BBA\ Rollinger, C.-R.\BEDS.
  \BBOP1990\BBCP.
\newblock {\Bem Sorts and Types in Artificial Intelligence}, \lowercase{\BVOL}\
  418 of {\Bem Lecture Notes in Artificial Intelligence}.
\newblock Springer-Verlag.

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

\bibitem[\protect\BCAY{Borgida}{Borgida}{1995}]{Borg95}
Borgida, A. \BBOP1995\BBCP.
\newblock \BBOQ Description logics in data management\BBCQ\
\newblock {\Bem {IEEE} Transactions on Knowledge and Data Engineering}, {\Bem
  7\/}(5), 671--682.

\bibitem[\protect\BCAY{Borgida}{Borgida}{1996}]{Borg96}
Borgida, A. \BBOP1996\BBCP.
\newblock \BBOQ On the relative expressiveness of description logics and
  predicate logics\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 82}, 353--367.

\bibitem[\protect\BCAY{Borgida \BBA\ Weddell}{Borgida \BBA\
  Weddell}{1997}]{BoWe97}
Borgida, A.\BBACOMMA\  \BBA\ Weddell, G.~E. \BBOP1997\BBCP.
\newblock \BBOQ Adding functional dependencies to description logics\BBCQ\
\newblock In {\Bem Proceedings of the Fifth International Conference on
  Deductive and Object-Oriented Databases (DOOD'97)}.

\bibitem[\protect\BCAY{Brachman \BBA\ Levesque}{Brachman \BBA\
  Levesque}{1984}]{BrLe84}
Brachman, R.~J.\BBACOMMA\  \BBA\ Levesque, H.~J. \BBOP1984\BBCP.
\newblock \BBOQ The tractability of subsumption in frame-based description
  languages\BBCQ\
\newblock In {\Bem Proceedings of the Fourth National Conference on Artificial
  Intelligence (AAAI'84)}, \BPGS\ 34--37.

\bibitem[\protect\BCAY{Brachman \BBA\ Levesque}{Brachman \BBA\
  Levesque}{1985}]{BrLe85}
Brachman, R.~J.\BBACOMMA\  \BBA\ Levesque, H.~J.\BEDS. \BBOP1985\BBCP.
\newblock {\Bem Readings in Knowledge Representation}.
\newblock Morgan Kaufmann, Los Altos.

\bibitem[\protect\BCAY{Brachman, McGuinness, Patel-Schneider, Alperin~Resnick,
  \BBA\ Borgida}{Brachman et~al.}{1991}]{BMPAB91}
Brachman, R.~J., McGuinness, D.~L., Patel-Schneider, P.~F., Alperin~Resnick,
  L., \BBA\ Borgida, A. \BBOP1991\BBCP.
\newblock \BBOQ Living with {CLASSIC}: When and how to use a {KL-ONE}-like
  language\BBCQ\
\newblock In Sowa, J.~F.\BED, {\Bem Principles of Semantic Networks}, \BPGS\
  401--456. Morgan Kaufmann, Los Altos.

\bibitem[\protect\BCAY{Bresciani, Franconi, \BBA\ Tessaris}{Bresciani
  et~al.}{1995}]{BrFT95}
Bresciani, P., Franconi, E., \BBA\ Tessaris, S. \BBOP1995\BBCP.
\newblock \BBOQ Implementing and testing expressive description logics:
  Preliminary report\BBCQ\
\newblock In Borgida, A., Lenzerini, M., Nardi, D., \BBA\ Nebel, B.\BEDS, {\Bem
  Working Notes of the 1995 Description Logics Workshop}, Technical Report, RAP
  07.95, Dipartimento di Informatica e Sistemistica, Universit{\`a} di Roma
  ``La Sapienza'', \BPGS\ 131--139\ Rome (Italy).

\bibitem[\protect\BCAY{Buchheit, Donini, Nutt, \BBA\ Schaerf}{Buchheit
  et~al.}{1998}]{BDNS98}
Buchheit, M., Donini, F.~M., Nutt, W., \BBA\ Schaerf, A. \BBOP1998\BBCP.
\newblock \BBOQ A refined architecture for terminological systems:
  {T}erminology = schema + views\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 99\/}(2), 209--260.

\bibitem[\protect\BCAY{Buchheit, Donini, \BBA\ Schaerf}{Buchheit
  et~al.}{1993}]{BuDS93c}
Buchheit, M., Donini, F.~M., \BBA\ Schaerf, A. \BBOP1993\BBCP.
\newblock \BBOQ Decidable reasoning in terminological knowledge representation
  systems\BBCQ\
\newblock {\Bem Journal of Artificial Intelligence Research}, {\Bem 1},
  109--138.

\bibitem[\protect\BCAY{Calvanese}{Calvanese}{1996a}]{Calv96d}
Calvanese, D. \BBOP1996a\BBCP.
\newblock \BBOQ Finite model reasoning in description logics\BBCQ\
\newblock In Aiello, L.~C., Doyle, J., \BBA\ Shapiro, S.~C.\BEDS, {\Bem
  Proceedings of the Fifth International Conference on the Principles of
  Knowledge Representation and Reasoning (KR'96)}, \BPGS\ 292--303. Morgan
  Kaufmann, Los Altos.

\bibitem[\protect\BCAY{Calvanese}{Calvanese}{1996b}]{Calv96c}
Calvanese, D. \BBOP1996b\BBCP.
\newblock \BBOQ Reasoning with inclusion axioms in description logics:
  Algorithms and complexity\BBCQ\
\newblock In Wahlster, W.\BED, {\Bem Proceedings of the Twelfth European
  Conference on Artificial Intelligence (ECAI'96)}, \BPGS\ 303--307. John Wiley
  \& Sons.

\bibitem[\protect\BCAY{Calvanese}{Calvanese}{1996c}]{Calv96}
Calvanese, D. \BBOP1996c\BBCP.
\newblock {\Bem Unrestricted and Finite Model Reasoning in Class-Based
  Representation Formalisms}.
\newblock Ph.D.\ thesis, Dipartimento di Informatica e Sistemistica,
  Universit{\`a} di Roma ``La Sapienza''.
\newblock Available at {\tt
  http://www.dis.uniroma1.it/pub/calvanes/thesis.ps.gz}.

\bibitem[\protect\BCAY{Calvanese, De~Giacomo, Lenzerini, Nardi, \BBA\
  Rosati}{Calvanese et~al.}{1998}]{CDLNR98}
Calvanese, D., De~Giacomo, G., Lenzerini, M., Nardi, D., \BBA\ Rosati, R.
  \BBOP1998\BBCP.
\newblock \BBOQ Description logic framework for information integration\BBCQ\
\newblock In {\Bem Proceedings of the Sixth International Conference on
  Principles of Knowledge Representation and Reasoning (KR'98)}, \BPGS\ 2--13.

\bibitem[\protect\BCAY{Calvanese \BBA\ Lenzerini}{Calvanese \BBA\
  Lenzerini}{1994a}]{CaLe94b}
Calvanese, D.\BBACOMMA\  \BBA\ Lenzerini, M. \BBOP1994a\BBCP.
\newblock \BBOQ Making object-oriented schemas more expressive\BBCQ\
\newblock In {\Bem Proceedings of the Thirteenth ACM SIGACT SIGMOD SIGART
  Symposium on Principles of Database Systems (PODS'94)}, \BPGS\ 243--254\
  Minneapolis. {ACM} Press and Addison Wesley.

\bibitem[\protect\BCAY{Calvanese \BBA\ Lenzerini}{Calvanese \BBA\
  Lenzerini}{1994b}]{CaLe94}
Calvanese, D.\BBACOMMA\  \BBA\ Lenzerini, M. \BBOP1994b\BBCP.
\newblock \BBOQ On the interaction between {ISA} and cardinality
  constraints\BBCQ\
\newblock In {\Bem Proceedings of the Tenth IEEE International Conference on
  Data Engineering (ICDE'94)}, \BPGS\ 204--213\ Houston (Texas). IEEE Computer
  Society Press.

\bibitem[\protect\BCAY{Calvanese, Lenzerini, \BBA\ Nardi}{Calvanese
  et~al.}{1994}]{CaLN94}
Calvanese, D., Lenzerini, M., \BBA\ Nardi, D. \BBOP1994\BBCP.
\newblock \BBOQ A unified framework for class based representation
  formalisms\BBCQ\
\newblock In Doyle, J., Sandewall, E., \BBA\ Torasso, P.\BEDS, {\Bem
  Proceedings of the Fourth International Conference on the Principles of
  Knowledge Representation and Reasoning (KR'94)}, \BPGS\ 109--120\ Bonn.
  Morgan Kaufmann, Los Altos.

\bibitem[\protect\BCAY{Calvanese, Lenzerini, \BBA\ Nardi}{Calvanese
  et~al.}{1998}]{CaLN98}
Calvanese, D., Lenzerini, M., \BBA\ Nardi, D. \BBOP1998\BBCP.
\newblock \BBOQ Description logics for conceptual data modeling\BBCQ\
\newblock In Chomicki, J.\BBACOMMA\  \BBA\ Saake, G.\BEDS, {\Bem Logics for
  Databases and Information Systems}, \BPGS\ 229--264. Kluwer Academic
  Publisher.

\bibitem[\protect\BCAY{Casanova, Fagin, \BBA\ Papadimitriou}{Casanova
  et~al.}{1984}]{CaFP84}
Casanova, M.~A., Fagin, R., \BBA\ Papadimitriou, C.~H. \BBOP1984\BBCP.
\newblock \BBOQ Inclusion dependencies and their interaction with functional
  dependencies\BBCQ\
\newblock {\Bem Journal of Computer and System Sciences}, {\Bem 28\/}(1),
  29--59.

\bibitem[\protect\BCAY{Cattell}{Cattell}{1994}]{Catt94}
Cattell, R. G.~G.\BED. \BBOP1994\BBCP.
\newblock {\Bem The Object Database Standard: {ODMG}-93}.
\newblock Morgan Kaufmann, Los Altos.
\newblock Release 1.1.

\bibitem[\protect\BCAY{Cattell \BBA\ Barry}{Cattell \BBA\ Barry}{1997}]{CaBa97}
Cattell, R. G.~G.\BBACOMMA\  \BBA\ Barry, D.~K.\BEDS. \BBOP1997\BBCP.
\newblock {\Bem The Object Database Standard: {ODMG} 2.0}.
\newblock Morgan Kaufmann, Los Altos.

\bibitem[\protect\BCAY{Chandra \BBA\ Vardi}{Chandra \BBA\ Vardi}{1985}]{ChVa85}
Chandra, A.~K.\BBACOMMA\  \BBA\ Vardi, M.~Y. \BBOP1985\BBCP.
\newblock \BBOQ The implication problem for functional and inclusion
  dependencies is undecidable\BBCQ\
\newblock {\Bem {SIAM} Journal on Computing}, {\Bem 14\/}(3), 671--677.

\bibitem[\protect\BCAY{Chen}{Chen}{1976}]{Chen76}
Chen, P.~P. \BBOP1976\BBCP.
\newblock \BBOQ The {E}ntity-{R}elationship model: {T}oward a unified view of
  data\BBCQ\
\newblock {\Bem {ACM} Transactions on Database Systems}, {\Bem 1\/}(1), 9--36.

\bibitem[\protect\BCAY{Cosmadakis \BBA\ Kanellakis}{Cosmadakis \BBA\
  Kanellakis}{1986}]{CoKa86}
Cosmadakis, S.~S.\BBACOMMA\  \BBA\ Kanellakis, P.~C. \BBOP1986\BBCP.
\newblock \BBOQ Functional and inclusion dependencies - {A} graph theoretical
  approach\BBCQ\
\newblock In Kanellakis, P.~C.\BBACOMMA\  \BBA\ Preparata, F.~P.\BEDS, {\Bem
  Advances in Computing Research, Vol.\ 3}, \BPGS\ 163--184. {JAI} Press.

\bibitem[\protect\BCAY{Cosmadakis, Kanellakis, \BBA\ Vardi}{Cosmadakis
  et~al.}{1990}]{CoKV90}
Cosmadakis, S.~S., Kanellakis, P.~C., \BBA\ Vardi, M. \BBOP1990\BBCP.
\newblock \BBOQ Polynomial-time implication problems for unary inclusion
  dependencies\BBCQ\
\newblock {\Bem Journal of the ACM}, {\Bem 37\/}(1), 15--46.

\bibitem[\protect\BCAY{De~Giacomo \BBA\ Lenzerini}{De~Giacomo \BBA\
  Lenzerini}{1994a}]{DeLe94}
De~Giacomo, G.\BBACOMMA\  \BBA\ Lenzerini, M. \BBOP1994a\BBCP.
\newblock \BBOQ Boosting the correspondence between description logics and
  propositional dynamic logics\BBCQ\
\newblock In {\Bem Proceedings of the Twelfth National Conference on Artificial
  Intelligence (AAAI'94)}, \BPGS\ 205--212. {AAAI} Press/The {MIT} Press.

\bibitem[\protect\BCAY{De~Giacomo \BBA\ Lenzerini}{De~Giacomo \BBA\
  Lenzerini}{1994b}]{DeLe94b}
De~Giacomo, G.\BBACOMMA\  \BBA\ Lenzerini, M. \BBOP1994b\BBCP.
\newblock \BBOQ Concept language with number restrictions and fixpoints, and
  its relationship with $\mu$-calculus\BBCQ\
\newblock In {\Bem Proceedings of the Eleventh European Conference on
  Artificial Intelligence (ECAI'94)}, \BPGS\ 411--415.

\bibitem[\protect\BCAY{{Di Battista} \BBA\ Lenzerini}{{Di Battista} \BBA\
  Lenzerini}{1993}]{DiLe93}
{Di Battista}, G.\BBACOMMA\  \BBA\ Lenzerini, M. \BBOP1993\BBCP.
\newblock \BBOQ Deductive entity-relationship modeling\BBCQ\
\newblock {\Bem {IEEE} Transactions on Knowledge and Data Engineering}, {\Bem
  5\/}(3), 439--450.

\bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, \BBA\ Nutt}{Donini
  et~al.}{1997}]{DLNN97}
Donini, F.~M., Lenzerini, M., Nardi, D., \BBA\ Nutt, W. \BBOP1997\BBCP.
\newblock \BBOQ The complexity of concept languages\BBCQ\
\newblock {\Bem Information and Computation}, {\Bem 134}, 1--58.

\bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, Nutt, \BBA\ Schaerf}{Donini
  et~al.}{1994}]{DLNNS94}
Donini, F.~M., Lenzerini, M., Nardi, D., Nutt, W., \BBA\ Schaerf, A.
  \BBOP1994\BBCP.
\newblock \BBOQ Queries, rules and definitions\BBCQ\
\newblock In {\Bem Foundations of Knowledge Representation and Reasoning}.
  Springer-Verlag.

\bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, \BBA\ Schaerf}{Donini
  et~al.}{1996}]{DLNS96}
Donini, F.~M., Lenzerini, M., Nardi, D., \BBA\ Schaerf, A. \BBOP1996\BBCP.
\newblock \BBOQ Reasoning in description logics\BBCQ\
\newblock In Brewka, G.\BED, {\Bem Principles of Knowledge Representation},
  Studies in Logic, Language and Information, \BPGS\ 193--238. {CSLI}
  Publications.

\bibitem[\protect\BCAY{Donini, Nardi, \BBA\ Rosati}{Donini
  et~al.}{1995}]{DoNR95}
Donini, F.~M., Nardi, D., \BBA\ Rosati, R. \BBOP1995\BBCP.
\newblock \BBOQ Non-first-order features in concept languages\BBCQ\
\newblock In Gori, M.\BBACOMMA\  \BBA\ Soda, G.\BEDS, {\Bem Proceedings of the
  Fourth Conference of the Italian Association for Artificial Intelligence
  (AI*IA'95)}, \lowercase{\BVOL}\ 992 of {\Bem Lecture Notes in Artificial
  Intelligence}, \BPGS\ 91--102. Springer-Verlag.

\bibitem[\protect\BCAY{Ferg}{Ferg}{1991}]{Ferg91}
Ferg, S. \BBOP1991\BBCP.
\newblock \BBOQ Cardinality concepts in entity-relationship modeling\BBCQ\
\newblock In {\Bem Proceedings of the Tenth International Conference on the
  Entity-Rela\-tion\-ship Approach (ER'91)}, \BPGS\ 1--30.

\bibitem[\protect\BCAY{Fikes \BBA\ Kehler}{Fikes \BBA\ Kehler}{1985}]{FiKe85}
Fikes, R.\BBACOMMA\  \BBA\ Kehler, T. \BBOP1985\BBCP.
\newblock \BBOQ The role of frame-based representation in reasoning\BBCQ\
\newblock {\Bem Communications of the ACM}, {\Bem 28\/}(9), 904--920.

\bibitem[\protect\BCAY{Fischer \BBA\ Ladner}{Fischer \BBA\
  Ladner}{1979}]{FiLa79}
Fischer, M.~J.\BBACOMMA\  \BBA\ Ladner, R.~E. \BBOP1979\BBCP.
\newblock \BBOQ Propositional dynamic logic of regular programs\BBCQ\
\newblock {\Bem Journal of Computer and System Sciences}, {\Bem 18}, 194--211.

\bibitem[\protect\BCAY{Grant \BBA\ Minker}{Grant \BBA\ Minker}{1984}]{GrMi84}
Grant, J.\BBACOMMA\  \BBA\ Minker, J. \BBOP1984\BBCP.
\newblock \BBOQ Numerical dependencies\BBCQ\
\newblock In Gallaire, H., Minker, J., \BBA\ Nicolas, J.-M.\BEDS, {\Bem
  Advances in Database Theory II}. Plenum Publ.\ Co., New York.

\bibitem[\protect\BCAY{Hayes}{Hayes}{1979}]{Haye79}
Hayes, P.~J. \BBOP1979\BBCP.
\newblock \BBOQ The logic of frames\BBCQ\
\newblock In Metzing, D.\BED, {\Bem Frame Conceptions and Text Understanding},
  \BPGS\ 46--61. Walter de Gruyter and Co.
\newblock Republished in \cite{BrLe85}.

\bibitem[\protect\BCAY{Horrocks}{Horrocks}{1998}]{Horr98}
Horrocks, I. \BBOP1998\BBCP.
\newblock \BBOQ Using an expressive description logic: {FaCT} or fiction?\BBCQ\
\newblock In {\Bem Proceedings of the Sixth International Conference on
  Principles of Knowledge Representation and Reasoning (KR'98)}, \BPGS\
  636--647.

\bibitem[\protect\BCAY{Horrocks \BBA\ Patel-Schneider}{Horrocks \BBA\
  Patel-Schneider}{1999}]{HoPa99}
Horrocks, I.\BBACOMMA\  \BBA\ Patel-Schneider, P.~F. \BBOP1999\BBCP.
\newblock \BBOQ Optimizing description logic subsumption\BBCQ\
\newblock {\Bem Journal of Logic and Computation}, {\Bem 9\/}(3), 267--293.

\bibitem[\protect\BCAY{Hull \BBA\ King}{Hull \BBA\ King}{1987}]{HuKi87}
Hull, R.~B.\BBACOMMA\  \BBA\ King, R. \BBOP1987\BBCP.
\newblock \BBOQ Semantic database modelling: Survey, applications and research
  issues\BBCQ\
\newblock {\Bem ACM Computing Surveys}, {\Bem 19\/}(3), 201--260.

\bibitem[\protect\BCAY{Karp}{Karp}{1992}]{Karp92}
Karp, P.~D. \BBOP1992\BBCP.
\newblock \BBOQ The design space of knowledge representation systems\BBCQ\
\newblock \BTR\ SRI AI Technical Note 520, SRI International, Menlo Park, CA.

\bibitem[\protect\BCAY{Karp, Myers, \BBA\ Gruber}{Karp et~al.}{1995}]{KaMG95}
Karp, P.~D., Myers, K.~L., \BBA\ Gruber, T. \BBOP1995\BBCP.
\newblock \BBOQ The generic frame protocol\BBCQ\
\newblock In {\Bem Proceedings of the Fourteenth International Joint Conference
  on Artificial Intelligence (IJCAI'95)}, \lowercase{\BVOL}~A, \BPGS\ 768--774\
  Montreal, Canada.

\bibitem[\protect\BCAY{Kifer, Lausen, \BBA\ Wu}{Kifer et~al.}{1995}]{KiLW95}
Kifer, M., Lausen, G., \BBA\ Wu, J. \BBOP1995\BBCP.
\newblock \BBOQ Logical foundations of {O}bject-{O}riented and frame-based
  languages\BBCQ\
\newblock {\Bem Journal of the ACM}, {\Bem 42\/}(4), 741--843.

\bibitem[\protect\BCAY{Kifer \BBA\ Wu}{Kifer \BBA\ Wu}{1993}]{KiWu93}
Kifer, M.\BBACOMMA\  \BBA\ Wu, J. \BBOP1993\BBCP.
\newblock \BBOQ A logic for programming with complex objects\BBCQ\
\newblock {\Bem Journal of Computer and System Sciences}, {\Bem 47}, 77--120.

\bibitem[\protect\BCAY{Kim}{Kim}{1990}]{Kim90}
Kim, W. \BBOP1990\BBCP.
\newblock {\Bem Introduction to {O}bject-{O}riented Databases}.
\newblock The {MIT} Press.

\bibitem[\protect\BCAY{Kim \BBA\ Lochovsky}{Kim \BBA\ Lochovsky}{1989}]{KiLo89}
Kim, W.\BBACOMMA\  \BBA\ Lochovsky, F.~H.\BEDS. \BBOP1989\BBCP.
\newblock {\Bem {O}bject-{O}riented Concepts, Databases, and Applications}.
\newblock {ACM} Press and Addison Wesley, New York.

\bibitem[\protect\BCAY{Kozen \BBA\ Tiuryn}{Kozen \BBA\ Tiuryn}{1990}]{KoTi90}
Kozen, D.\BBACOMMA\  \BBA\ Tiuryn, J. \BBOP1990\BBCP.
\newblock \BBOQ Logics of programs\BBCQ\
\newblock In van Leeuwen, J.\BED, {\Bem Handbook of Theoretical {C}omputer
  {S}cience -- Formal Models and Semantics}, \BPGS\ 789--840. Elsevier Science
  Publishers (North-Holland), Amsterdam.

\bibitem[\protect\BCAY{Lecluse \BBA\ Richard}{Lecluse \BBA\
  Richard}{1989}]{LeRi89}
Lecluse, C.\BBACOMMA\  \BBA\ Richard, P. \BBOP1989\BBCP.
\newblock \BBOQ Modeling complex structures in object-oriented databases\BBCQ\
\newblock In {\Bem Proceedings of the Eighth ACM SIGACT SIGMOD SIGART Symposium
  on Principles of Database Systems (PODS'89)}, \BPGS\ 362--369.

\bibitem[\protect\BCAY{Lehmann}{Lehmann}{1992}]{Lehm92}
Lehmann, F.\BED. \BBOP1992\BBCP.
\newblock {\Bem Semantic Networks in {A}rtificial {I}ntelligence}.
\newblock Pergamon Press, Oxford.

\bibitem[\protect\BCAY{Lenzerini, Nardi, \BBA\ Simi}{Lenzerini
  et~al.}{1991}]{LeNS91}
Lenzerini, M., Nardi, D., \BBA\ Simi, M.\BEDS. \BBOP1991\BBCP.
\newblock {\Bem Inheritance Hierarchies in Knowledge Representation and
  Programming Languages}.
\newblock John Wiley \& Sons, Chichester.

\bibitem[\protect\BCAY{Lenzerini \BBA\ Nobili}{Lenzerini \BBA\
  Nobili}{1990}]{LeNo90}
Lenzerini, M.\BBACOMMA\  \BBA\ Nobili, P. \BBOP1990\BBCP.
\newblock \BBOQ On the satisfiability of dependency constraints in
  entity-relationship schemata\BBCQ\
\newblock {\Bem Information Systems}, {\Bem 15\/}(4), 453--461.

\bibitem[\protect\BCAY{Mitchell}{Mitchell}{1983}]{Mitc83}
Mitchell, J.~C. \BBOP1983\BBCP.
\newblock \BBOQ The implication problem for functional and inclusion
  dependencies\BBCQ\
\newblock {\Bem Information and Control}, {\Bem 56}, 154--173.

\bibitem[\protect\BCAY{{Motschnig-Pitrik} \BBA\ Mylopoulous}{{Motschnig-Pitrik}
  \BBA\ Mylopoulous}{1992}]{MoMy92}
{Motschnig-Pitrik}, R.\BBACOMMA\  \BBA\ Mylopoulous, J. \BBOP1992\BBCP.
\newblock \BBOQ Classes and instances\BBCQ\
\newblock {\Bem Journal of Intelligent and Cooperative Information Systems},
  {\Bem 1\/}(1).

\bibitem[\protect\BCAY{Nebel}{Nebel}{1991}]{Nebe91}
Nebel, B. \BBOP1991\BBCP.
\newblock \BBOQ Terminological cycles: Semantics and computational
  properties\BBCQ\
\newblock In Sowa, J.~F.\BED, {\Bem Principles of Semantic Networks}, \BPGS\
  331--361. Morgan Kaufmann, Los Altos.

\bibitem[\protect\BCAY{Piza, Schewe, \BBA\ Schmidt}{Piza et~al.}{1992}]{PiSS92}
Piza, B., Schewe, K.-D., \BBA\ Schmidt, J.~W. \BBOP1992\BBCP.
\newblock \BBOQ Term subsumption with type constructors\BBCQ\
\newblock In Yesha, Y.\BED, {\Bem Proceedings of the International Conference
  on Information and Knowledge Management (CIKM'92)}, \BPGS\ 449--456\
  Baltimore.

\bibitem[\protect\BCAY{Schild}{Schild}{1991}]{Schi91}
Schild, K. \BBOP1991\BBCP.
\newblock \BBOQ A correspondence theory for terminological logics: Preliminary
  report\BBCQ\
\newblock In {\Bem Proceedings of the Twelfth International Joint Conference on
  Artificial Intelligence (IJCAI'91)}, \BPGS\ 466--471\ Sydney, Australia.

\bibitem[\protect\BCAY{Schild}{Schild}{1994}]{Schi94}
Schild, K. \BBOP1994\BBCP.
\newblock \BBOQ Terminological cycles and the propositional
  $\mu$-calculus\BBCQ\
\newblock In Doyle, J., Sandewall, E., \BBA\ Torasso, P.\BEDS, {\Bem
  Proceedings of the Fourth International Conference on the Principles of
  Knowledge Representation and Reasoning (KR'94)}, \BPGS\ 509--520\ Bonn.
  Morgan Kaufmann, Los Altos.

\bibitem[\protect\BCAY{{Schmidt-Schau{\ss}} \BBA\ Smolka}{{Schmidt-Schau{\ss}}
  \BBA\ Smolka}{1991}]{ScSm91}
{Schmidt-Schau{\ss}}, M.\BBACOMMA\  \BBA\ Smolka, G. \BBOP1991\BBCP.
\newblock \BBOQ Attributive concept descriptions with complements\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 48\/}(1), 1--26.

\bibitem[\protect\BCAY{Sowa}{Sowa}{1991}]{Sowa91}
Sowa, J.~F.\BED. \BBOP1991\BBCP.
\newblock {\Bem Principles of Semantic Networks}.
\newblock Morgan Kaufmann, Los Altos.

\bibitem[\protect\BCAY{Teorey}{Teorey}{1989}]{Teor89}
Teorey, T.~J. \BBOP1989\BBCP.
\newblock {\Bem Database Modeling and Design: {T}he Entity-Relationship
  Approach}.
\newblock Morgan Kaufmann, Los Altos.

\bibitem[\protect\BCAY{Thalheim}{Thalheim}{1992}]{Thal92}
Thalheim, B. \BBOP1992\BBCP.
\newblock \BBOQ Fundamentals of cardinality constraints\BBCQ\
\newblock In Pernoul, G.\BBACOMMA\  \BBA\ Tjoa, A.~M.\BEDS, {\Bem Proceedings
  of the Eleventh International Conference on the Entity-Rela\-tion\-ship
  Approach (ER'92)}, \BPGS\ 7--23. Springer-Verlag.

\bibitem[\protect\BCAY{Thalheim}{Thalheim}{1993}]{Thal93}
Thalheim, B. \BBOP1993\BBCP.
\newblock {\Bem Fundamentals of the Entity Relationship Model}.
\newblock Springer-Verlag.

\bibitem[\protect\BCAY{Vardi}{Vardi}{1985}]{Vard85}
Vardi, M.~Y. \BBOP1985\BBCP.
\newblock \BBOQ The taming of converse: Reasoning about two-way
  computations\BBCQ\
\newblock In Parikh, R.\BED, {\Bem Proc.\ of the 4th Workshop on Logics of
  Programs}, \lowercase{\BVOL}\ 193 of {\Bem Lecture Notes in Computer
  Science}, \BPGS\ 413--424. Springer-Verlag.

\bibitem[\protect\BCAY{Woods \BBA\ Schmolze}{Woods \BBA\
  Schmolze}{1992}]{WoSc92}
Woods, W.~A.\BBACOMMA\  \BBA\ Schmolze, J.~G. \BBOP1992\BBCP.
\newblock \BBOQ The {KL-ONE} family\BBCQ\
\newblock In Lehmann, F.~W.\BED, {\Bem Semantic Networks in Artificial
  Intelligence}, \BPGS\ 133--178. Pergamon Press.
\newblock Published as a special issue of {\it Computers \& Mathematics with
  Applications}, Volume 23, Number 2--9.

\bibitem[\protect\BCAY{Ye, Parent, \BBA\ Spaccapietra}{Ye
  et~al.}{1994}]{YePS94}
Ye, X., Parent, C., \BBA\ Spaccapietra, S. \BBOP1994\BBCP.
\newblock \BBOQ Cardinality consistency of derived objects in {DOOD}
  systems\BBCQ\
\newblock In Loucopoulos, P.\BED, {\Bem Proceedings of the Thirteenth
  International Conference on the Entity-Rela\-tion\-ship Approach (ER'94)},
  \lowercase{\BVOL}\ 881 of {\Bem Lecture Notes in Computer Science}, \BPGS\
  278--295\ Manchester (UK). Springer-Verlag.

\end{thebibliography}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% save-place: t
%%% End: 
