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

\jairheading{6}{1997}{87-110}{7/96}{3/97}
\ShortHeadings{Concept Definitions in Description Logics}
{De Giacomo \& Lenzerini}

\begin{document}
\firstpageno{87}
%\input{macros}
%%%%%%%%%%%%%%%%%%%%%%%%%%% MACROS %%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\A{{\cal A}} \def\B{{\cal B}} \def\C{{\cal C}} \def\D{{\cal D}}
\def\E{{\cal E}} \def\F{{\cal F}} \def\G{{\cal G}} \def\H{{\cal H}}
\def\I{{\cal I}} \def\J{{\cal J}} \def\K{{\cal K}} \def\L{{\cal L}}
\def\M{{\cal M}} \def\N{{\cal N}} \def\O{{\cal O}} \def\P{{\cal P}}
\def\Q{{\cal Q}} \def\R{{\cal R}} \def\S{{\cal S}} \def\T{{\cal T}}
\def\U{{\cal U}} \def\V{{\cal V}} \def\W{{\cal W}} \def\X{{\cal X}}
\def\Y{{\cal Y}} \def\Z{{\cal Z}}

%\def\asp{\makebox[3pt]{}}  
%\def\osp{\hskip1pt}  
%\def\asps#1{{\asp#1\asp}}
%\def\osps#1{{\osp{#1}\osp}}
%\def\eset{\emptyset}
%\def\incl{\subseteq}
%\def\qland{\;\;\land\;\;}
%\def\col{\colon}
%\def\cld{,\ldots,}

\def\imp{\Rightarrow}
\def\st{\,.\,\,}
\def\iff{\;\mbox{ iff }\;}

%\def\braces#1{$\{$ #1 $\}$}

%\def\con{\asp\asp\&\asp}
%\def\deq{\doteq}
\def\eqdef{=_{def}}
%\def\sbox{\vbox{\hrule
%                \hbox{\vrule\hskip4pt\vbox{\vskip4pt}\vrule}
%                \hrule}}

\def\per{.}   

%\def\ol#1{\overline{#1}}
%\def\dd#1#2{#1_1,\ldots,#1_{#2}}
%\def\quotes#1{\lq\lq#1\rq\rq}

%\def\set#1{\{#1\}}
%\def\bigset#1{ \Bigl\{ #1 \Bigr\} }
%\def\bigmid{\ \Big|\ }
%\def\card#1{|{#1}|}
\def\card#1{\#\{#1\}}
%\def\sub#1{[#1]}

%\def\If{\lq\lq$\Leftarrow$\rq\rq\ \ }
%\def\OnlyIf{\lq\lq$\Rightarrow$\rq\rq\ \ }

%\def\quote#1{{\lq\lq#1\rq\rq}}

\newcommand{\KLONE}{{\sc kl-one}}

\newcommand{\dom}{\Delta^\I}
\newcommand{\Int}[1]{#1^\I}
\newcommand{\INT}[1]{(#1)^\I}
\newcommand{\domp}{\Delta^{\I'}}
\newcommand{\Intp}[1]{#1^{\I'}}
\newcommand{\INTP}[1]{(#1)^{\I'}}
\newcommand{\Inta}[1]{#1_{\rho}^\I}
\newcommand{\Intax}[2]{#1_{\rho #2}^\I}
\newcommand{\INTAX}[2]{(#1)_{\rho #2}^\I}
\newcommand{\INTA}[1]{(#1)_{\rho}^\I}
\newcommand{\INTOP}[1]{\|#1\|^\I}
\newcommand{\Ass}[1]{#1_\rho}

\def\SUBD{\sqsubseteq}
\def\AND{\sqcap}
\def\OR{\sqcup}
\def\NOT{\neg}
\def\ALL#1#2{\forall #1 . #2}
\def\SOME#1#2{\exists #1 . #2}
\def\SOMET#1{\exists #1}
\def\ALLRC{\ALL R C}
\def\SOMERC{\SOME R C}
\def\SOMERT{\SOMET R}
\newcommand{\ATMOST}[2]{(\leq #1 \, #2)}
\newcommand{\ATLEAST}[2]{(\geq #1 \, #2)}

%\def\lacute{\mathopen{<}}
%\def\racute{\mathclose{>}}

\newcommand\BOX[1]{\lbrack #1 \rbrack}
\newcommand\DIAM[1]{\langle #1 \rangle}

%\def\rR{{\bf R}}
%\def\pP{{\bf P}}
%\def\Any_u{{\bf Any}_{U_1,\ldots,U_n}}
%\def\ud{<U_1:d_1,\ldots,U_n:d_n>}

%\def\any{{\bf any}}
%\def\Tau{T}
%\def\Varrho{P}

%\def\u{{\bf u}}

\newcommand{\relc}[3]{#1#2#3}
\newcommand{\inc}[2]{#1\col#2}

\newcommand{\ALN}{{\cal ALN}}
\newcommand{\ALUNR}{{\cal ALUNR}}
\newcommand{\AL}{{\cal AL}}
\newcommand{\ALC}{{\cal ALC}}
\newcommand{\ALCN}{{\cal ALCN}}
\newcommand{\ALCQ}{{\cal ALCQ}}
\newcommand{\ALE}{{\cal ALE}}
\newcommand{\ALU}{{\cal ALU}}
\newcommand{\ALEMIN}{{\cal FLE}^{-{}}}
\newcommand{\FLMIN}{{\cal FL}^{-{}}}
\newcommand{\FLEMIN}{{\cal FLE}^{-{}}}
\newcommand{\FL}{{\cal FL}}
\newcommand{\TSL}{{\cal TSL}}
\newcommand{\TSLF}{{\cal TSLF}}

\newcommand{\CF}{{\cal CF}}
\newcommand{\CFO}{{\cal CFO}}
\newcommand{\CN}{{\cal CN}}
\newcommand{\CNO}{{\cal CNO}}
\newcommand{\CI}{{\cal CI}}
\newcommand{\CIO}{{\cal CIO}}
\newcommand{\CIF}{{\cal CIF}}
\newcommand{\CIN}{{\cal CIN}}
\newcommand{\CIFR}{{\cal CIFR}}
\newcommand{\CINR}{{\cal CINR}}
\newcommand{\CINB}{{\cal CINB}}
\newcommand{\CINBR}{{\cal CINBR}}

\newcommand{\DL}{\mu{\cal ALCQ}}

\newcommand{\DF}{{\cal DF}}
\newcommand{\DFO}{{\cal DFO}}
\newcommand{\DN}{{\cal DN}}
\newcommand{\DNO}{{\cal DNO}}
\newcommand{\DIF}{{\cal DIF}}
\newcommand{\DIN}{{\cal DIN}}
\newcommand{\DIFR}{{\cal DIFR}}
\newcommand{\DINR}{{\cal DINR}}
\newcommand{\DINB}{{\cal DINB}}
\newcommand{\DINBR}{{\cal DINBR}}
\newcommand{\mucal}{\mu K_i}

\newcommand{\Moda}[1]{#1_{\rho}^\M}
\newcommand{\Modax}[2]{#1_{\rho #2}^\M}
\newcommand{\MODA}[1]{(#1)_{\rho}^\M}

\newcommand{\doms}{\Delta^{\I^s}}      
\newcommand{\Ints}[1]{#1^{\I^s}}
\newcommand{\INTS}[1]{(#1)^{\I^s}}   
\newcommand{\Intas}[1]{#1_{\rho^s}^{\I^s}}    
\newcommand{\INTAS}[1]{(#1)_{\rho^s}^{\I^s}}  
\newcommand{\Intaxs}[2]{#1_{(\rho #2)^{s}}^{\I^s}} 
\newcommand{\Intaxss}[2]{#1_{\rho^{s} #2}^{\I^s}} 
\newcommand{\INTAXS}[2]{(#1)_{(\rho #2)^{s}}^{\I^s}}
\newcommand{\Asss}[1]{#1_{\rho^s}}        
\newcommand{\ASSS}[1]{(#1)_{\rho^s}}        

%%%%%%%%%%%%%%%%%%%%%%%%% END MACROS %%%%%%%%%%%%%%%%%%%%%%%%%



%\input{commands}
%%%%%%%%%%%%%%%%%%%%%%%%%% COMMANDS %%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\sep}{\bigskip \noindent}

\newcommand{\xifx}{$\leftarrow$}

\newcommand{\leavebigvspace}{\par \addvspace{\bigskipamount}}
\newcommand{\leavemedvspace}{\par \addvspace{\medskipamount}}
\newcommand{\leavesmallvspace}{\par \addvspace{\smallskipamount}}

\newcommand{\dynamicvspace}[1]{\par \addvspace{#1}} 
% #1 = \smallskipamount, \medskipamount, \bigskipamount


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

\newenvironment{definition}{\leavebigvspace \noindent
{\bf Definition}}{$\Box$ \leavebigvspace}

\newenvironment{example}{\leavebigvspace \noindent
{\bf Example}}{$\Box$ \leavebigvspace}

\newenvironment{proof}{\leavebigvspace \noindent
{\bf Proof} $\,$}{$\Box$ \leavebigvspace}

%%%%%%%%%%%%%%%%%%%%%%%% END COMMANDS %%%%%%%%%%%%%%%%%%%%%%%%


%\begin{document}

\title{A Uniform Framework for Concept Definitions in Description Logics}

\author{\name Giuseppe De Giacomo \email degiacomo@dis.uniroma1.it\\
	\addr Universit\`{a} di Roma ``La Sapienza''\\
	Via Salaria 113, 00198 Roma, Italy
	\AND
	\name Maurizio Lenzerini \email lenzerini@dis.uniroma1.it\\
	\addr Universit\`{a} di Roma ``La Sapienza''\\
        Via Salaria 113, 00198 Roma, Italy}

%\author{Giuseppe De Giacomo and Maurizio Lenzerini\\ \\ Dipartimento di
%  Informatica e Sistemistica\\ Universit\`{a} di Roma ``La Sapienza''\\
%  Via Salaria 113, 00198 Roma, Italy\\ {\tt
%    \{degiacomo,lenzerini\}@dis.uniroma1.it}}

%\date{}

\maketitle

\begin{abstract}
  Most modern formalisms used in Databases and Artificial Intelligence for
  describing an application domain are based on the notions of class (or
  concept) and relationship among classes.  One interesting feature of such
  formalisms is the possibility of defining a class, i.e., providing a set
  of properties that precisely characterize the instances of the class.
  Many recent articles point out that there are several ways of assigning a
  meaning to a class definition containing some sort of recursion.  In this
  paper, we argue that, instead of choosing a single style of semantics, we
  achieve better results by adopting a formalism that allows for different
  semantics to coexist. We demonstrate the feasibility of our argument, by
  presenting a knowledge representation formalism, the description logic
  $\DL$, with the above characteristics.  In addition to the constructs for
  conjunction, disjunction, negation, quantifiers, and qualified number
  restrictions, $\DL$ includes special fixpoint constructs to express
  (suitably interpreted) recursive definitions.  These constructs enable
  the usual frame-based descriptions to be combined with definitions of
  recursive data structures such as directed acyclic graphs, lists,
  streams, etc.  We establish several properties of $\DL$, including the
  decidability and the computational complexity of reasoning, by
  formulating a correspondence with a particular modal logic of programs
  called the modal mu-calculus.
\end{abstract}


\section{Introduction}

Most modern formalisms used in Databases and Artificial Intelligence for
representing an application domain are based on the notions of class (or
concept) and relationship among classes.  For example, the object-oriented
and semantics data models developed in Databases describe data in terms of
classes (sometimes called entity types) and incorporate several features
for establishing various forms of relationships between classes. On the
other hand, the notion of class (often called concept or frame) and that of
link among classes are provided in all structured formalisms for Knowledge
Representation (frame-based languages, semantic networks, description
logics, etc.). Finally, this notion is also present in several type systems
of programming languages, specially those based on the object-oriented
paradigm.

There are basically two ways of using and describing classes (concepts).
In the first one, which we can call the {\em prescriptive approach}, the
description formalism allows for expressing a number of properties of a
class, thus prescribing constraints that the instances of the class must
satisfy.  In the second one, which we can call the {\em definitional
  approach}, the formalism allows for providing the {\em definition} of a
class, i.e., a set of properties that {\em precisely characterize} the
instances of the class.  While the prescriptive approach is quite well
understood and established, the definitional approach is still the subject
of an interesting debate, regarding both its nature and its semantic
foundation. In particular, it is well known that there are various ways to
assign a meaning to a class definition when it contains some sort of
recursion \cite{Baad90c,Baad91,Nebe91,BergaICDT,Beer90}.

In this paper, we are concerned with the semantic problems related to the
definitional approach, arguing that, instead of choosing a single style of
semantics for the knowledge representation formalism, we achieve better
results by allowing different semantics to coexist.

We discuss this issue in the context of Description Logics\footnote{Also
  called Concept Languages or Terminological Languages.}, which are logics
originally developed in Knowledge Representation to provide a formal
reconstruction of frame-based languages.  Description logics describe the
domain of interest in terms of concepts, which represent classes of
individuals, and roles, which are binary relations used to specify
properties or attributes of individuals as well as links with other
individuals \cite{Nebe90b}.  Starting from atomic concepts, denoted simply
by a name, more complex concepts are built by using a suitable set of
constructs.  For example, the expression $parent \AND male \AND
\ALL{child}{male}$ denotes the concept of father (male parent) whose
children are all male. The symbol $\AND$ denotes the construct for {\em
  concept conjunction}, while $\forall$ denotes {\em universal role
  quantification}.  Typically, concepts are structured into hierarchies
determined by the properties associated with them. The hierarchical
structure is defined in such a way that more specific concepts inherit the
properties of the more general ones.

We introduce a description logic, called $\DL$, which extends the
well-known description logic $\ALC$ \cite{ScSm91} by including the so
called {\em qualified number restrictions}, which are a very general form
of cardinality constraints on roles, and special {\em fixpoint constructs},
which enable us to capture the various semantics for recursive definitions
within a single formalism.  Notably, the availability of these constructs
makes it possible to combine the usual frame-based descriptions with
definitions of recursive data structures such as directed acyclic graphs,
lists, streams, etc.

We establish several properties of $\DL$, including the decidability and
the computational complexity of reasoning, by formulating a correspondence
with a particular modal logic of programs called the {\em modal
  mu-calculus}.

Recent articles, \cite<e.g.,>{Berga,Borg92}, advocate the use of
description logics as a unifying framework for several types of database
and knowledge representation formalisms.  Indeed, it is possible to show
that, depending on both the constructs and the semantics used, one can
capture several database models and programming language type systems by
using description logics. Therefore, the study presented in this paper is
not merely confined to description logics, but is also applicable to other
representation formalisms.

The paper is organized as follows. In Section~2, we present the basic
notions regarding both description logics and fixpoints. In Section~3, we
motivate our approach through a detailed discussion about the different
semantics of concept definitions that have been considered in the
literature, and we argue for a formalism in which the various semantics
coexist. In Section~4, we present one such formalism, namely the logic
$\DL$, and we discuss several of its properties.  In Section~5 we study
reasoning techniques for $\DL$ and expose the correspondence with modal
mu-calculus. Finally, in Section~6, we draw the conclusions and discuss
some open problems.


\section{Preliminaries}

In this section, we briefly present the basic notions regarding both
description logics, and fixpoints.  The interested reader is referred
to \cite{Nebe90b} and \cite{DeBa-80} for a more complete introduction to
the subjects.


\subsection{Description Logics}

Description logics allow one to represent a domain of interest in terms of
{\em concepts} and {\em roles}. Concepts model classes of individuals,
while roles model relationships between classes.  Starting with atomic
concepts (denoted by $A$) and atomic roles (denoted by $R$), which are
concepts and roles described simply by a name, complex concepts and roles
can be built by means of suitable constructs.

In this section, we concentrate on the description logic $\ALCQ$, obtained
from the well-known description logic $\ALC$ \cite{ScSm91} by including
{\em qualified number restrictions}.  These are cardinality constraints on
the role fillers of a very general form, where role fillers to which a
constraint applies are selected by means of a generic concept expression,
the {\em qualifier}.

$\ALCQ$ concepts (denoted by $C$ or $D$, possibly with a subscript)
are composed inductively according to the following {\em abstract
syntax} ($n$ denotes a natural number):

\[C ::=  A\mid\top \mid \bot \mid \NOT C\mid C_1\AND C_2 \mid C_1\OR C_2 
\mid \SOME{R}{C} \mid \ALL{R}{C} \mid \ATMOST{n}{R\per C} \mid
\ATLEAST{n}{R\per C}.\]

These constructs are not all independent. The following equalities hold:
$\top = A\OR\NOT A$, $\bot = \NOT\top$, $\ALL{R}{C} = \NOT\SOME{R}{\NOT
  C}$, and $\ATMOST{n}{R\per C} = \NOT \ATLEAST{n+1}{R\per C}$.


>From a semantic point of view, concepts are interpreted as subsets of
an abstract domain, while roles are interpreted as binary relations
over such a domain.  More precisely, an {\em interpretation} $\I
=(\dom, \Int{\cdot})$ consists of a {\em domain of interpretation}
$\dom$, and an {\em interpretation function} $\Int{\cdot}$ mapping
every atomic concept $A$ to a subset of $\dom$ and every atomic role
$R$ to a subset of $\dom\times\dom$.

The interpretation function $\Int{\cdot}$ is extended to complex
concepts of $\ALCQ$ (note that in $\ALCQ$ roles are always atomic) as
follows:
\[\begin{array}{lcl}

\Int{\top} & = & \dom\\
\Int{\bot} & = & \emptyset\\
\INT{\NOT C} & = & \dom - \Int{C}\\
\INT{C_1 \AND C_2} & = & \Int{C_1}\cap\Int{C_2}\\
\INT{C_1 \OR C_2} & = & \Int{C_1}\cup\Int{C_2}\\

\INT{\SOME{R}{C}}  & = &  \{ s \in\dom \mid\exists s'.\;
(s,s')\in \Int{R} \mbox{ and } s' \in \Int{C}\}\\

\INT{\ALL{R}{C}}  & = &   \{ s \in\dom \mid\forall s'.\;
(s,s')\in \Int{R} \mbox{ implies } s' \in \Int{C}\}\\

\Int{\ATMOST{n}{R.C}} & = & \{ s \in\dom \mid \card{s'\mid
(s,s')\in \Int{R} \mbox{ and } s' \in \Int{C}}\le n\}\\

\Int{\ATLEAST{n}{R.C}} & = & \{ s \in\dom \mid \card{s'\mid
(s,s')\in \Int{R} \mbox{ and } s' \in \Int{C}} \ge n\}

\end{array}\]
where $\# S$ denotes the cardinality of the set $S$.


A {\em concept $C$ is satisfiable} iff there exists an interpretation $\I$
such that $\Int{C}\not= \emptyset$, otherwise $C$ is {\em unsatisfiable}.
A {\em concept $C_1$ is subsumed by a concept $C_2$}, written as $C_1 \SUBD
C_1$, iff for every interpretation $\I$, $\Int{C_1} \subseteq \Int{C_2}$.

Our knowledge expressed in terms of concepts and roles is assembled into a
special knowledge base, traditionally called {\em TBox}, which consists of
a finite (possibly empty) set of assertions. In order to be as general as
possible, we assume that every assertion has the form of an {\em inclusion
  assertion} (or simply inclusion):
\[C_1 \SUBD C_2\]
without any restriction on the form of the concepts $C_1$ and $C_2$.  A
pair of inclusions of the form $\{C_1 \SUBD C_2, C_2 \SUBD C_1\}$ is often
written as $C_1 \equiv C_2$ and is called {\em equivalence assertion}.

An interpretation $\I$ {\em satisfies an inclusion} $C_1 \SUBD C_2$ iff
$\Int{C_1}\subseteq \Int{C_2}$.  An interpretation $\I$ is a {\em model of
  a TBox} $\K$ iff $\I$ satisfies all inclusions in $\K$.

Let $\K$ be a TBox. We say that a {\em concept $C$ is satisfiable in $\K$},
iff there exists a model $\I$ of $\K$ such that $\Int{C} \not=\emptyset$,
{\em unsatisfiable} otherwise.  We say that a {\em concept $C_1$ is
  subsumed by a concept $C_2$ in $\K$}, written $\K \models C_1 \SUBD C_2$,
iff for every model $\I$ of $\K$, $\Int{C_1}\subseteq \Int{C_2}$.

\subsection{Fixpoints}

We briefly recall few notions on fixpoints.  Consider the equation:
\[X=f(X)\]
where $f$ is an operator from $2^{\S}$ to $2^{\S}$ ($2^{\S}$ denotes the
set of all subsets of a set $\S$).  Every solution $\E$ of this equation is
called a {\em fixpoint} of the operator $f$ (while every set $\E$ such that
$f(\E)\subseteq\E$ is called {\em pre-fixpoint}, and every set $\E$ such
that $\E\subseteq f(\E)$ is called {\em post-fixpoint}). In general, an
equation as the one above may have either no solution, a finite number of
solutions, or an infinite number of them.  Among the various solutions, the
smallest and the greatest solutions (with respect to set-inclusion) have a
prominent position, if they exist.  A fundamental result due to Tarski
\cite{Tarski55} guarantees the existence and the uniqueness of both such
solutions in case $f$ is monotonic wrt set-inclusion ($\subseteq$), where
$f$ is {\em monotonic} wrt $\subseteq$ whenever $\E_1 \subseteq \E_2$
implies $f(\E_1)\subseteq f(\E_2)$.
\begin{theorem}[Tarski]\label{tarski}
  Let $\S$ be a set, and $f$ an operator from $2^{\S}$ to $2^{\S}$ that is
  monotonic wrt $\subseteq$.  Then:
\begin{itemize}
\item There exists a unique least fixpoint of $f$, which is given by
$\bigcap\{ \E\subseteq \S \mid \;f(\E)\subseteq\E\}$.
\item There exists a unique greatest fixpoint of $f$, which is given
by
$\bigcup\{ \E\subseteq \S \mid \;\E \subseteq f(\E)\}$.
\end{itemize}
\end{theorem}


\section{Concept Definitions as Equations}

We now analyze the notion of concept definition in detail. Let us ignore
for the moment knowledge bases as they have been introduced in the previous
section, and let us consider a different kind of assertion: the definition
statement.  Let the form of a {\em definition statement} (or simply
definition) be:
\[A \eqdef C\]
where $A$ is an atomic concept which cannot appear in the left-hand side of
other definition statements, and $C$ is a concept expression in $\ALCQ$.
In principle, $A \eqdef C$ is intended to provide an exact account for the
concept to $A$ in terms of $C$, i.e., to define $A$ as {\em the} set of the
individuals satisfying $C$.


In specifying the semantics of definitions, we need to distinguish
between two different types of atomic concepts, namely, {\em primitive
concepts} and {\em defined concepts}. Given a set of definition
statements, the primitive concepts are the atomic concepts that do not
appear in the left-hand side of any definition statement, whereas the
defined concepts are those that appear in the left-hand side of a
definition statement.

Given an interpretation $\I=(\dom, \Int\cdot)$, the interpretation
function $\Int\cdot$ directly assigns a subset of $\dom$ to primitive
concepts, but not to defined concepts. The meaning of a defined
concept $A$ is assigned through its definition statement $A \eqdef C$,
extending the interpretation function so as the following requirement
is satisfied:
\begin{equation}\label{req:def}
\Int A = \Int C.
\end{equation}

Consider, for example, the definition statement:
\[parent \eqdef \SOME{child}{\top}.\]
Note that the defined concept $parent$ does not appear in the body of
its definition statement. By (\ref{req:def}), the definition statement
provides the {\em definition} for the concept $parent$, in the
following sense: in any interpretation $\I=(\dom,\Int{\cdot})$,
$\Int{parent}$ denotes a {\em single} subset of $\dom$, exactly the
one denoted by $\INT{\SOME{child}{\top}}$, i.e., $\{s \mid \exists t .
(s,t)\in\Int{child}\}$.  In general, if a concept $A$ is defined in
terms of primitive and already defined concepts, then for every
interpretation $\I$ there exists a unique way to extend the
interpretation function to defined concepts, and hence there is no
doubt that the definition statement provides a {\em definition} of
$A$.


Now, consider the following definition statement:
\[A \eqdef \SOME{child}{A}.\]
Given an interpretation $\I=(\dom,\Int\cdot)$, by (\ref{req:def}) the
statement is interpreted as the equation:
\[\Int{A} = \{ s\in \dom \mid \exists t. (s,t)\in \Int{child} \mbox{ and
  } t \in \Int{A}\}. \] However such equation does not specify
univocally how to extend the interpretation function $\Int\cdot$ to
the defined concept $A$, since $\emptyset$ satisfies the equation as
well as any set of individuals where each member has an infinite
chain of descendants that are also members.

In general, we call {\em recursive definition
  statements}\footnote{Terminological cycles in
  \cite{Baad90c,Baad91,Nebe91}. In the present discussion, for sake of
  simplicity, we do not consider mutual recursive definitions, as
  $A\eqdef F(B)$, $B\eqdef F'(A)$. We shall come back to this point
  later on.} (or simply recursive definitions), definition statements
  of the form:
\[A\eqdef F(A)\] where $F(A)$ stands for a concept that has $A$ as a
subconcept\footnote{ A {\em subconcept} of a concept $C$ is any
  substring of $C$ (including $C$ itself) that is a concept, according
  to the syntax rules.}. According to (\ref{req:def}), the recursive
  definition $A \eqdef F(A)$ is interpreted simply as a sort of
  equation specifying that, given an interpretation $\I$, the subset
  of $\dom$ that can be tied to the defined concept $A$ must satisfy
  the equation $\Int{A} = \Int{F(A)}$, i.e., must be one of its {\em
  solutions}.  Observe that, in general, either none, one, or several
  subsets of $\dom$ may exist which are solutions of the above
  equation.

Another convenient way to consider a definition statement is to
associate to it, for every interpretation $\I$, an operator from
subsets of $\dom$ to subsets of $\dom$ instead of an equation, so that
the fixpoints of the operator correspond to the solutions of the
equation. For example, to the definition $A \eqdef \SOME{child}{A}$ we
associate the operator: 
\[\lambda S . \{ s\in\dom \mid \exists
t. (s,t)\in \Int{child} \mbox{ and } t \in S\}\] for any
interpretation $\I$. In general as either none, one or multiple
solutions exist for the equation associated with a recursive
definition, we have that either none, one or multiple fixpoints exist
for the corresponding operator.

In this situation the word ``definition'' itself seems misleading: the
body of the definition does not give a complete account of the defined
concept. An additional criterion is needed for selecting solutions of
the associated equation, or equivalently, fixpoints of the associated
operator. In other words in addition to (\ref{req:def}), a criterion
is needed to extend univocally the interpretations $\I$ to the defined
concepts. This observation has led to various semantics, each of which
interprets recursive definitions differently, by choosing, a priori
and once and for all, which solutions, or equivalently which
fixpoints, are to be assigned to the defining concept of a recursive
definition\footnote{We remark that a non-recursive definition is
interpreted by the various semantics in the same way, since, for every
$\I$, the equation associated to it has a single solution.}.

\subsection{Different Semantics for Recursive Definitions}

In the literature on description logics, three semantics for recursive
definitions have been proposed \cite<see>{Nebe91}:

\begin{itemize}

\item Descriptive Semantics

\item Least Fixpoint Semantics

\item Greatest Fixpoint Semantics

\end{itemize}
and which of these semantics is the ``right'' one is a long standing matter
of debate. Below we describe how each of the three semantics interprets
recursive definitions, and present some examples showing that the choice of
the semantics depends in fact upon the concept to be defined.  But first,
it should be stressed that only the descriptive semantics is able to assign
meaning to general inclusion assertions $C_1\SUBD C_2$ introduced in the
previous section.

According to the {\em Descriptive Semantics}, a recursive definition $A
\eqdef F(A)$ is a {\em constraint} stating that, for any $\I$, $\Int{A}$
has to be {\em a} solution of the equation $\Int{A} = \Int{F(A)}$.  Under
the descriptive semantics, $A \eqdef \SOME{child}{A}$ simply states that
the individuals in the class $A$ have a child in the class $A$, and the
individuals that have a child in the class $A$ are themselves in the class
$A$, where $A$ {\em is no better specified}. In general the descriptive
semantics is not appropriate to properly define recursive concepts, in the
sense that, given an interpretation $\I$, it is unable to assign a unique
subset of $\dom$ to the defined concept of the recursive definition.

In fact under descriptive semantics definition statements are
indistinguishable from the equivalence assertions introduced in the
previous section. In other words, the meaning assigned to $A\eqdef
F(A)$ is the same as that assigned to the equivalence assertion $A
\equiv F(A)$. Although such equivalence assertions can be used to specify
if-and-only-if constraints, they do not provide proper definitions when
recursion is involved.  For example, we can express the fact that humans are
mammals having parents that are humans, and on the converse, that
mammals having parents that are humans are humans themselves, in terms
of the equivalence assertion:
\[human \equiv mammal \AND \SOME{parent}{\top} \AND
\ALL{parent}{human}.\]  Similarly we may require  horses to satisfy an
analogous property:
\[horse \equiv mammal \AND \SOME{parent}{\top} \AND \ALL{parent}{horse}.\]
However the two equivalence assertions above do not define $human$ and
$horse$ as shown, e.g., by the fact that (correctly) they do not imply that
all humans are horses and vice-versa (in contrast to what happen when a
fixpoint semantics is used, see below).


The {\em Least Fixpoint Semantics} interprets a recursive definition
statement $A \eqdef F(A)$ by assigning to $A$ the smallest possible
extension in each interpretation $\I$, among those that satisfy $\Int A
\eqdef \Int{F(A)}$ -- i.e., the least fixpoint of the corresponding
operator.  In fact it is always assumed that the operator associated with
the definition statement is monotonic, so that Theorem~\ref{tarski} applies
and a least fixpoint exists and is unique, i.e., the corresponding equation
has a {\em unique} smallest solution. Hence under the least fixpoint
semantics the recursive definition statement $A \eqdef F(A)$ {\em defines}
the concept $A$.  It is easy to verify that in the example $A \eqdef
\SOME{child}{A}$, the least fixpoint semantics leads us to identify $A$
with $\bot$. Indeed the empty set is a solution of the equation associated
with the statement, and it is obviously the smallest solution.  Similarly
if we interpret the definition statement:
\[human \eqdef mammal \AND \SOME{parent}{\top} \AND \ALL{parent}{human}\]
with the least fixpoint semantics, we have that $\Int{human}=\emptyset$ for
any interpretation $\I$. Observe that if, as above, we adopt a similar
definition for $horse$, we get again $\Int{horse}=\emptyset$, so we can
trivially infer that $horse \equiv human$.


The least fixpoint semantics is particularly suitable for providing
{\em inductive definitions} of concepts. For example, consider the
class of a list (LIST) defined as follows:
\begin{itemize}
\item An EMPTY-LIST is a LIST.
\item A NODE that has exactly one successor that is a LIST is a LIST.
\item Nothing else is a LIST.
\end{itemize}
The first two conditions can be captured by the following recursive
definition statement\footnote{Additionally we specify that the two
concepts $emptylist$ and $node$ are disjoint.}: \[list\eqdef
emptylist\OR(node\AND \ATMOST{1}{succ.\top}\AND \SOME{succ}{list})\]
where $\ATMOST{1}{succ.\top}$ forces $succ$ to be a function. To
enforce the third condition we must assign the smallest possible
extension to $list$.  Thus, the class of LISTs can be naturally
defined by means of the above definition statement, interpreted
according to the least fixpoint semantics.

The {\em Greatest Fixpoint Semantics} interprets a recursive definition
statement $A \eqdef F(A)$ by assigning to $A$ the largest possible
extension in each interpretation $\I$, among those that satisfy $\Int A
\eqdef \Int{F(A)}$ -- i.e., the greatest fixpoint of the corresponding
operator. Again, it is assumed that such operator is monotonic in order to
guaranty the existence an the unicity of the greatest fixpoint
(Theorem~\ref{tarski}).  As for the least fixpoint semantics, under the
greatest fixpoint semantics a recursive definition statement $A \eqdef
F(A)$ {\em defines} the concept $A$. For example, considering again the
definition statement $A \eqdef \SOME{child}{A}$, the greatest fixpoint
semantics leads us to interpret $A$ as the class of {\em all} the
individuals having a child that in turn is a member of $A$.


While the least fixpoint semantics naturally captures classes defined by
induction, the greatest fixpoint semantics naturally captures classes of
individuals whose structure is {\em non-well-founded} or {\em
  co-inductive}.  An example is the class of STREAMs, modeling the
well-known linear data structure having a NODE as first element, and such
that the rest of the structure is a STREAM itself. Note that streams are
similar to lists except that while lists can be considered as finite
sequences of nodes, streams are infinite sequences of nodes.  Such a class
can be captured by the following recursive definition statement:
\[stream \eqdef node \AND \ATMOST{1}{succ.\top}\AND
\SOME{succ}{stream}\] with the proviso that the greatest possible
extension is assigned to $stream$.

Finally, consider under the greatest fixpoint semantics the recursive
definition statements:
\[human \eqdef mammal \AND \SOME{parent}{\top} \AND \ALL{parent}{human}\] 
\[horse \eqdef mammal \AND \SOME{parent}{\top} \AND \ALL{parent}{horse}.\] 
Although they do not assign the empty extension to both $human$ and $horse$
as the least fixpoint semantics does, we do have again the rather counter
intuitive consequence that $human\equiv horse$, since $\Int{human} =
\Int{horse}$ for any interpretation $\I$.  In general under both types of
fixpoint semantics the particular name used to denote a defined concept
does not have any impact on the interpretation of it, since the meaning of
the defined concept is completely specified by its definition statement.

\subsection{Least and Greatest Fixpoints as Concept Constructs}

The above considerations show that arguing about which is the ``right''
semantics for recursive definitions is not really an issue. Each of them
captures an essential use of recursive equations: the descriptive semantics
is appropriate to specify constraints on concepts and is the only one that
extends to the general inclusion assertions introduced in Section~2; the
least fixpoint semantics is appropriate to define a structure inductively;
the greatest fixpoint semantics is the appropriate to define
non-well-founded structures. Generally, we may need the three of them in
the same knowledge base, in order to model the various properties of the
different concepts.


Our proposal in this paper is exactly in the direction of reconciling
the various semantics in the same knowledge base. This is pursued by
means of a logic that incorporates two constructs, $\mu X . F(X)$ and
$\nu X . F(X)$ (the symbols $X,Y,\ldots$ stand for concept variables),
denoting, respectively, the least fixpoint and the greatest fixpoint of
the operator associated with the definition $X \eqdef F(X)$, that is,
for every $\I$, the smallest solution and the
greatest solution of the equation $\Int{X}=\Int{F(X)}$.  

In our approach, definition statements will never appear in a TBox.
Instead, a knowledge base will be simply a set of inclusion assertions
(interpreted according to the descriptive semantics) that can involve
fixpoint constructs.  For example, in order to specify the properties of
the concepts of $list$, $stream$, $human$ and $horse$ we can use the
following assertions\footnote{ We also include the assertion $emptylist
  \SUBD \NOT node$, specifying that the concepts $emptylist$ and $node$ are
  disjoint.}:
\[\begin{array}{lcl}

list & \equiv & \mu X . emptylist\OR(node\AND\ATMOST{1}
{succ\per\top}\AND \SOME{succ}{X})\\


stream & \equiv & \nu X. node \AND\ATMOST{1}{succ.\top}\AND \SOME{succ}{X}\\

human & \equiv & mammal \AND \SOME{parent}{\top} \AND \ALL{parent}{human}\\

horse & \equiv & mammal \AND \SOME{parent}{\top} \AND \ALL{parent}{horse}.

\end{array}\]
Note that, if we then add to the above knowledge base the equivalence
assertion:
\[mgm \equiv \nu X \st mammal \AND \SOME{parent}{\top} \AND
\ALL{parent}{X}\] defining the concept $mgm$ (mammal generated by
mammal), then it correctly turns out that both $human$ and $horse$ are
subsumed by $mgm$.


The availability of least and greatest fixpoint constructs, by allowing
different semantics to be used in the same TBox, makes it possible to model
not only abstract classes, but also inductively and co-inductively defined
data structures, such as lists and streams. This is particularly important
if our objective is to integrate class-based representation formalisms and
programming systems (declarative or procedural), in order to make these
formalisms more useful in practice.  Furthermore, we have the possibility
of nesting fixpoints, thus going beyond the simple equational format by
which we motivated their introduction. As an example, consider the
following one:
\begin{quotation}
Among the inhabitants of the planet ``Plonk'', a disease called
``foo'' is quite common. Such a disease manifests itself in two forms:
a ``visible'' one and a ``latent'' one, and it has a rather intricate
hereditary pattern.  Individuals that have the visible form transmit
the visible form to at least one (say the first) direct descendant
(obviously, if there is any direct descendant), these ill descendants
in turn do the same, and so on, {\em until} someone transmits the
latent form of the disease.  More precisely, along any chain of
descendants, the visible form of the disease sooner or later is
interrupted, because either an individual has no direct descendant or
an individual transmits to some descendant the latent form.  All
direct descendants (if any) of an individual that has the latent form
inherit the visible form. The pattern goes on like this, generation
after generation, {\em forever}.
\end{quotation}
The hereditary pattern ($foo\_hp$) of the above disease can be defined as
follows:
\[
\arraycolsep=0pt
\begin{array}{ll}
foo\_hp \equiv \nu X.\mu Y.(&(visible \AND (\SOME{child}{Y}\OR \ALL{child}{\bot}))
\OR \\
& (latent \AND \ALL{child}{(visible \AND X)}))
\end{array}\]
where $visible$ and $latent$ denote the visible and the latent form
respectively of the disease, and are assumed to be disjoint
($latent\SUBD\NOT visible$).


\section{The Description Logic $\DL$}

We provide a formal account of the meaning of the fixpoint constructs by
introducing a description logic, called $\DL$, which is obtained by adding
these constructs to $\ALCQ$.

We make use of the notions of scope, bound and free occurrences of
variables, closed formulae, etc.\ The definitions of these notions are the
same as the analogues in first-order logic, treating $\mu$ and $\nu$ as
quantifiers.  In addition, we use the symbol $\sigma$ as an abstraction for
either $\mu$ or $\nu$.

The primitive symbols in $\DL$ are atomic concepts, {\em (concept)
  variables} (denoted by $X,Y,\ldots$), and atomic roles which are the only
roles admitted in the logic.

Concepts in $\DL$ are formed inductively according
to the following abstract syntax:
\[\begin{array}{lcl}
C &::=& A\mid\top \mid \bot \mid \NOT C\mid C_1\AND C_2 \mid C_1\OR C_2
\mid \SOME{R}{C} \mid \ALL{R}{C}\mid \ATMOST{n}{R \per C}\mid
\ATLEAST{n}{R \per C} \mid \\
  &   & \mu X.C\mid \nu X.C \mid X
\end{array}\]
where $A$ denotes an atomic concept, $R$ an atomic role, $n$ a natural
number, and $X$ a variable, and {\em with the restriction that only a
  variable $X$ occurring positively in $C$ can be bounded by a fixpoint
  $\sigma$ in $\sigma X . C$}.  We say that a variable $X$ occurs {\em
  positively} in a concept $C$, if every free occurrence of $X$ is in the
scope of an even number of negations, considering concepts $C'$ in
$\ATMOST{n}{R.C'}$ in the scope of one negation.

The two fixpoint constructs are mutually definable: $\nu X.C = \neg \mu
X.\NOT C [X/\NOT X]$ (where $C [X/\NOT X]$ is the concept obtained
substituting all free occurrences of $X$ by the concept $\neg X$).

As before, an interpretation $\I =(\dom, \Int{\cdot})$ consists of a domain
of interpretation $\dom$, and a interpretation function $\Int{\cdot}$,
which maps every atomic concept to a subset of $\dom$, and every atomic
role to a subset of $\dom\times\dom$.  But the presence of free variables
does not allow us to extend the interpretation function $\Int{\cdot}$
directly to every concept of the logic. For this reason we introduce
valuations.  A {\em valuation} $\rho$ on an interpretation $\I$ is a
mapping from variables to subsets of $\dom$.

Given a valuation $\rho$, we denote by $\rho[X/\E]$ the valuation
identical to $\rho$ except for $\rho[X/\E](X) =
\E$. In other words, for every variable $Y$:


\[\rho[X/\E](Y) = \left\{ 
\begin{array}{ll}
\E & \mbox{ if } Y = X\\
\rho(Y) & \mbox{ if } Y\not= X
\end{array}\right.\]

Let $\I$ be an interpretation and $\rho$ a valuation on $\I$. We assign
meaning to concepts of the logic by associating to $\I$ and $\rho$ an {\em
  extension function} $\Inta{\cdot}$, mapping concepts to subsets of
$\dom$, as follows:

\[\begin{array}{lcl}

\Inta{X}  & = & \rho(X) \subseteq \dom \\

\Inta{A}  & = & \Int{A} \subseteq \dom \\

\Inta{\top} & = & \dom\\

\Inta{\bot} & = & \emptyset\\

\INTA{\NOT C} & = & \dom - \Inta{C}\\

\INTA{C_1 \AND C_2} & = & \INTA{C_1}\cap\INTA{C_2}\\

\INTA{C_1 \OR C_2} & = & \INTA{C_1}\cup\INTA{C_2}\\

\INTA{\SOME{R}{C}}  & = &  \{ s \in\dom \mid\exists s'.\;
(s,s')\in \Int{R} \mbox{ and } s' \in \Inta{C}\}\\

\INTA{\ALL{R}{C}}  & = &   \{ s \in\dom \mid\forall s'.\;
(s,s')\in \Int{R} \mbox{ implies } s' \in \Inta{C}\}\\

\Inta{\ATMOST{n}{R.C}} & = & \{ s \in\dom \mid \card{s'\mid
(s,s')\in \Int{R} \mbox{ and } s' \in \Inta{C}}\le n\}\\

\Inta{\ATLEAST{n}{R.C}} & = & \{ s \in\dom \mid \card{s'\mid
(s,s')\in \Int{R} \mbox{ and } s' \in \Inta{C}} \ge n\}\\

\INTA{\mu X.C} & = & 
\bigcap\{ \E\subseteq\dom \mid \;\;\;\;\Intax{C}{[X/\E]} \subseteq\E \;\}\\

\INTA{\nu X.C} & = & 
\bigcup\{ \E\subseteq\dom \mid  \;\;\;\;\E \subseteq \;\; \Intax{C}{[X/\E]}
\;\}

\end{array}\]

In the last two cases $\Intax{C}{[X/\E]}$ is interpreted as an operator
from subsets $\E$ of $\dom$ to subsets of $\dom$. By the syntactic
restriction enforced on variables, such an operator is guaranteed to be
monotonic wrt $\subseteq$. Notice that free variables appearing in a
concept are interpreted similarly to atomic concepts.
 
A concept $C$ is satisfiable, if there exists an interpretation $\I$ and a
valuation $\rho$ on $\I$ such that $\Inta{C} \not=\emptyset$, otherwise $C$
is unsatisfiable.  A concept $C_1$ is subsumed by a concept $C_2$, written
as $C_1\SUBD C_2$, if for every interpretation $\I$ and every valuation
$\rho$ on $\I$, $\INTA{C_1}\subseteq \INTA{C_2}$.

A $\DL$ TBox is a finite (possibly empty) set of inclusion assertions $C_1
\SUBD C_2$ where $C_1$ and $C_2$ are {\em closed} concepts of $\DL$. As
before, we use equivalence assertions of the form $C_1 \equiv C_2$ as an
abbreviation for $\{C_1 \SUBD C_2, C_2 \SUBD C_1\}$.

An interpretation $\I$  satisfies an inclusion assertion $C_1
\SUBD C_2$, if $\INTA{C_1}\subseteq \INTA{C_2}$, where $\rho$ is any
valuation on $\I$ (being $C_1$ and $C_2$ closed, and hence independent
from valuations). $\I$ is a  model of a TBox $\K$, if $\I$
satisfies all inclusion assertions in $\K$. We say that a TBox $\K$ is
satisfiable, if it has a model. Observe that inclusion assertions in
$\K$ are interpreted according to the descriptive semantics.

We say that a TBox $\K$ logically implies an inclusion assertion
$C_1\SUBD C_2$, written $\K\models C_1 \SUBD C_2$, if for every model
$\I$ of $\K$ and every valuation $\rho$ on $\I$, $\INTA{C_1}\subseteq
\INTA{C_2}$.



\subsection{Properties of the Fixpoint Constructs}\label{mu-prop}

In the following, we use the notation $C(X)$ to indicate that the variable
$X$ occurs free in the concept $C$ (other variables could occur free in $C$
as well), and the notation $C(D)$, where $D$ is a concept, as a shorthand
for $C(X)[X/D]$ (i.e., the concept obtained substituting all free
occurrences of $X$ in $C(X)$ by the concept $D$).

Let us comment briefly on some simple properties of the logic.  First, the
concept $\sigma X.C(X)$ is equivalent to the concept $\sigma Y.C(Y)$, as
long as $Y$ is free for $X$ in $C(X)$.  Second, the extension function
$\Inta{\cdot}$ assign to a closed concept a value which is independent of
the actual valuation $\rho$. Hence $\sigma X.C$, where $X$ does not occur
in $C$, is equivalent to $C$.  Third, since $\sigma X.C(X)$ is a fixpoint
we have that $C(\sigma X.C(X))$ is equivalent to $\sigma X.C(X)$.
Furthermore, we have that the concept $\mu X.C(X)$ is always subsumed by
the concept $\nu X.C(X)$.

The next property is more substantial.  Consider the class of a single
source finite directed acyclic graphs (DAGs) defined inductively as
follows\footnote{We assume that a leaf of a DAG is a NODE with all
arcs leading to a special DAG called EMPTY-DAG.  As an alternative,
one can assume that a leaf of a DAG is a NODE having no connection at
all.  In the latter case, the definition of $dag$ would simplify to
$dag \eqdef node \AND\ALL{arc}{dag}$ (in which the general form of
inductive definitions -- i.e., base case and inductive case -- is less
apparent).}:
\begin{itemize}

\item The EMPTY-DAG is a DAG (base step).

\item A NODE that has connections and all connections are DAGs, is a DAG
(inductive step).
\item Nothing else is a DAG.
\end{itemize}

Consider now a $\DL$ TBox $\K$ containing the two equivalence assertions:
\[dag\_of\_student \equiv \mu X \st emptydag \OR (student \AND
\SOME{arc}{\top} \AND \ALL{arc}{X})\]
\[dag\_of\_person \equiv \mu X \st emptydag \OR (person \AND
\SOME{arc}{\top} \AND \ALL{arc}{X})\] which define the concepts
$dag\_of\_student$ and $dag\_of\_person$ as the classes of DAGs whose nodes
are students and persons respectively.  Assuming that students are persons,
we want to be able to infer that DAGs of students are DAGs of persons as
well. That is, we want: \[\K\models student \SUBD person ~\mbox{ implies
  }~\K\models dag\_of\_student \SUBD dag\_of\_person.\]

It turns out that for $\DL$ such a property holds. To prove this, we
introduce the following two theorems.

\begin{theorem}\label{TN1}
  Let $\K$ be a $\DL$ TBox, and $C$ and $D$ two $\DL$ concepts in which a
  variable $X$ occurs free positively. Then:
\[\K\models C \SUBD D ~~\mbox{ implies }~~ \K\models \sigma X.C \SUBD \sigma X.D.\]
\end{theorem}

\begin{proof}
We proceed by contradiction\footnote{ For uniformity, we do not
distinguish if $X$ occurs free or not. Obviously if $X$ does not occur
free, the result is trivial.}. Assume that $\Inta{C} \subseteq
\Inta{D}$ holds for all models $\I$ of $\K$ and all valuations $\rho$
on $\I$. And suppose that there exists a model $\I$ of $\K$ and a
valuation $\rho$ on $\I$ such that $\INTA{\sigma X.C} \not\subseteq
\INTA{\sigma X.D}$.

First we prove the result for $\sigma =\mu$.  Let $s$ be an individual
in $\INTA{\mu X.C}$ but not in $\INTA{\mu X.D}$.  Now, we have:
\begin{equation}
s\in \INTA{\mu X.C} \iff
\forall \E\subseteq\dom \st (\Intax{C}{[X/\E]} \subseteq\E \mbox{ implies }
s\in\E) \label{eq1}
\end{equation}
\begin{equation}
s\not\in \INTA{\mu X.D} \iff
\exists \E'\subseteq\dom \st (\Intax{D}{[X/\E']} \subseteq\E' \mbox{ and }
s\not\in\E').\label{eq2}
\end{equation}
For the set $\E'$ in (\ref{eq2}), the following expression holds:
\[\Intax{C}{[X/\E']}\subseteq\Intax{D}{[X/\E']}\subseteq\E'\] 
hence by (\ref{eq1}) we have $s\in\E'$ and by (\ref{eq2}) we have
$s\not\in\E'$, which is impossible.


\bigskip
The proof for $\sigma =\nu$ is similar.
Let $s$ be an individual in $\INTA{\nu X.C}$ but not in $\INTA{\nu X.D}$.
Now, we have:
\begin{equation}
s\in \INTA{\nu X.C} \iff
\exists \E''\subseteq\dom \st ( \E'' \subseteq\Intax{C}{[X/\E'']}\mbox{
and } s\in\E'') \label{eq3}
\end{equation}
\begin{equation}
s\not\in \INTA{\nu X.D} \iff
\forall \E\subseteq\dom \st (\E \subseteq\Intax{D}{[X/\E]} \mbox{ implies }
s\not\in\E).\label{eq4}
\end{equation}
For the set $\E''$ in (\ref{eq3}), the following expression holds:
\[\E''\subseteq\Intax{C}{[X/\E'']}\subseteq\Intax{D}{[X/\E'']}\] 
hence by (\ref{eq3}) we have $s\in\E''$ and by (\ref{eq4}) we have
$s\not\in\E''$, which is impossible.
\end{proof}

Above we have defined what it means for a variable $X$ to occur positively
in a concept $C$.  Similarly we say that a variable $X$ occurs {\em
  negatively} in a concept $C$, if every free occurrence of $X$ is in the
scope of an odd number of negations, considering concepts $C'$ in
$\ATMOST{n}{R.C'}$ in the scope of one negation.

\begin{theorem}\label{TN2}
  Let $\K$ be a $\DL$ TBox, and $D(X)$ a $\DL$ concept with the variable
  $X$ as a free variable. Then, for any $\DL$ concepts $C_1$ and $C_2$:
\[\K\models C_1\SUBD C_2 \mbox{ implies }
\left\{\begin{array}{lr}
 \K\models D(C_1)\SUBD D(C_2) & \mbox{ if $X$ occurs positively in $D(X)$}\\
 \K\models D(C_2)\SUBD D(C_1) & \mbox{ if $X$ occurs negatively in $D(X)$}
\end{array}\right.\] 
\end{theorem}

\begin{proof}
  We prove the result by induction on the formation of $D(X)$. 
  
  Base case.  If $D(X) = X$, the result holds trivially.
  
  Inductive cases. If $D(X)$ has the form $\NOT D'(X)\mid
  \ATLEAST{n}{R.C'}$ , then $X$ occurs positively (negatively) in $D'(X)$
  and negatively (positively) in $D(X)$.  By induction hypothesis
  $\K\models D'(C_i)\SUBD D'(C_j)$ (where $i,j\in\{1,2\}$ and $i\not=j$)
  and hence by the semantics of the constructs $\K\models D(C_j)\SUBD
  D(C_i)$.
  
  If $D(X)$ has the form $D'_{1}(X)\AND D'_{2}(X) \mid D'_{1}(X)\OR
  D'_{2}(X) \mid \ALL{R}{D'(X)}\mid \ATLEAST{n}{R\per D'(X)}$, then $X$
  occurs positively (negatively) both in $D'(X)$ and in $D(X)$. By
  induction hypothesis $\K\models D'(C_i)\SUBD D'(C_j)$ and hence by the
  semantics of the constructs $\K\models D(C_i)\SUBD D(C_j)$.
  
  It remains to prove the result for $D(X)=\sigma Y.D'(X)$ ($Y\not=X$). In
  this case, by the syntactic restriction enforced, $Y$ occurs positively in
  $D'(X)$ and hence by Theorem~\ref{TN1} we have $\K\models D'(C_i)\SUBD
  D'(C_j)$ implies $\K\models\sigma Y.D'(C_i)\SUBD \sigma Y.D'(C_j)$, thus
  by induction hypothesis we are done.
\end{proof}


Going back to our example, we can, in fact, infer that DAGs of
students are also DAGs of persons. Indeed, by applying
Theorem~\ref{TN2} and then Theorem~\ref{TN1}, we have that $\K\models
student\SUBD person$ implies $\K\models \mu X.emptydag \OR (student
\AND \SOME{arc}{\top} \AND \ALL{arc}{X}) \SUBD \mu X.emptydag \OR
(person \AND \SOME{arc}{\top} \AND \ALL{arc}{X})$.



\subsection{Internalizing Assertions}

We now show that logical implication in $\DL$ TBoxes (thus also
satisfiability of $\DL$ TBoxes) is reducible to unsatisfiability of {\em a
  single $\DL$ concept}.  To prove this result, we introduce the notions of
generated sub-interpretation and sub-valuation\footnote{Together these
  notions play the same role as that of generated sub-model in modal
  logics.}.


Let $\I=(\dom, \Int{\cdot})$ be an interpretation, $\rho$ a valuation on
$\I$, and $s\in \dom$ an individual. We define the interpretation
$\I^s = (\doms, \Ints{\cdot})$, and the valuation $\rho^s$ on $\I^s$,
as follows:
\begin{itemize}

\item  $\doms = 
\{ s'\in \dom \mid (s,s') \in (R_{1}^{\I}\cup\ldots \cup
R_{m}^{\I})^* \}$.

\item For each atomic role $R_i$, we have $R_{i}^{\I^s} = R_{i}^{\I} \cap
(\doms\times\doms)$.

\item For each atomic concept $A$, we have $A^{\I^s} = \Int{A}\cap
\doms$.

\item For each variable $X$, we have $\rho^s(X) = \rho(X)\cap
\doms$.

\end{itemize}
We call {\em $\I^s$ the sub-interpretation of $\I$ generated by $s$},
and {\em $\rho^s$ the sub-valuation of $\rho$ generated by $s$}.


For generated sub-interpretations and sub-valuations we can state the
following lemma.


\begin{lemma}\label{TN3}
Let $C$ be a $\DL$ concept. Then for any interpretation $\I$, any
valuation $\rho$ on $\I$, and any individual $s\in \dom$, we have:
\[\forall t\in\doms.\;t\in \Inta{C} \iff t\in \Intas{C}.\]
\end{lemma}

\begin{proof}
Without loss of generality, we consider concepts formed according to the
following simplified abstract syntax: $C ::=  A\mid \bot \mid \NOT C\mid
C_1\AND C_2 \mid \SOME{R}{C} \mid \ATLEAST{n}{R\per C}\mid \mu X.C \mid X.$

We prove the result by induction on the number of nested fixpoint
constructs.  Base case. If in $C$ there are no fixpoint
constructs, the thesis can be proven by induction on the formation
of $C$.

Inductive case. We assume that the thesis holds for concepts $C$ with
$k$ nested fixpoint constructs, and we prove it for concepts $\mu X.C$
with $k+1$. We recall that, by the Tarski-Knaster Theorem on fixpoints
\cite{Tarski55}, $t\in\INTA{ \mu X.C}$ iff there exists an ordinal
$\alpha$ such that $t\in\INTA{\mu_{\alpha} X.C}$, where
$\INTA{\mu_{\alpha} X.C}$ is defined by transfinite induction as:
\begin{itemize}

\item $\INTA{\mu_0 X.C}=\emptyset$

\item $\INTA{\mu_{\alpha+1}
X.C}=\Intax{C}{[X/\INTA{\mu_{\alpha} X.C}]}$

\item $\INTA{\mu_{\lambda} X.C}=\bigcup_{\alpha < \lambda}\INTA{\mu_{\alpha}
X.C}$, if $\lambda$ is a limit ordinal. 

\end{itemize}
Hence we proceed by transfinite induction on ordinals $\alpha$.

Base case of the transfinite induction. $\mu_0 X.C$ is defined as
$\bot$, thus trivially we have $t\in\INTA{\mu_0 X.C} \iff t\in
\INTAS{\mu_0 X.C}$.

Successor case of the transfinite induction.  We want to show that
$t\in\INTA{ \mu_{\alpha+1} X.C} \iff t\in\INTAS{ \mu_{\alpha+1} X.C}$,
which reduces to:
\begin{equation}
t\in\Intax{C}{[X/\INTA{\mu_{\alpha} X.C}]}\iff 
t\in\Intaxss{C}{[X/\INTAS{\mu_{\alpha} X.C}]}. \label{TN3.eq1}
\end{equation} 

To prove this, we start by showing that:
\begin{equation}
t\in\Intaxss{C}{[X/\INTAS{\mu_{\alpha} X.C}]} \iff
t\in\Intaxs{C}{[X/\INTA{\mu_{\alpha} X.C}]}. \label{TN3.eq2}
\end{equation}
Notice that the two valuations above may differ only on the value of $X$.
If it holds that:
\begin{equation}
t\in\Intaxss{X}{[X/\INTAS{\mu_{\alpha} X.C}]} \iff
t\in\Intaxs{X}{[X/\INTA{\mu_{\alpha} X.C}]}, \label{TN3.eq3}
\end{equation}
then by straightforward induction on the formation of $C$ we have that
(\ref{TN3.eq2}) holds as well.  Let us prove (\ref{TN3.eq3}). We can
write it as:
\[t\in \rho^s[X/\INTAS{\mu_{\alpha} X.C}](X) \iff
t\in (\rho[X/\INTA{\mu_{\alpha} X.C}])^s(X),\]
and since $t\in \doms$, this reduces to 
\[t\in \INTAS{\mu_{\alpha} X.C} \iff
t\in \INTA{\mu_{\alpha} X.C}.\]
which holds by transfinite inductive hypothesis.

Now, since $C$ contains $k$ fixpoint constructs, by inductive hypothesis on
$k$, we have:
\[t\in\Intax{C}{[X/\INTA{\mu_{\alpha} X.C}]} \iff 
t\in\Intaxs{C}{[X/\INTA{\mu_{\alpha} X.C}]}.\] Hence, considering
(\ref{TN3.eq1}) and (\ref{TN3.eq2}), it follows that indeed
$t\in\INTA{\mu_{\alpha+1} X.C} \iff t\in\INTAS{\mu_{\alpha+1} X.C}$.


Limit case of the transfinite induction.  Let $\lambda$ be a limit
ordinal, then $t\in\INTA{\mu_{\lambda} X.C}$ iff there exists an
ordinal $\alpha < \lambda$ such that $t\in\INTA{\mu_{\alpha} X.C}$. By
transfinite induction hypothesis, it holds that:
$t\in\INTA{\mu_{\alpha} X.C} \iff t\in\INTAS{\mu_{\alpha} X.C}$, and
thus:
\[t\in\INTA{\mu_{\lambda} X.C} \iff t\in \INTAS{\mu_{\lambda}X.C}.\]

This completes the transfinite induction. So for all ordinals $\alpha$
it holds that: \[t\in\INTA{\mu_{\alpha} X.C} \iff
t\in\INTAS{\mu_{\alpha} X.C}.\] The induction on the nesting of
fixpoint constructs is completed as well, hence we have proven the
lemma.
\end{proof}




Now we are ready to state the result mentioned above.

\begin{theorem}\label{TN4}
Let $\K = \{C_1\SUBD D_1,\ldots, C_q\SUBD D_q\}$ be a $\DL$ TBox,
and $C$ and $D$ two $\DL$ concepts.  Then $\K\models C\SUBD D$ if
and only if the $\DL$ concept:
\begin{equation}
\nu X .(\ALL{R_1}{X} \AND \ldots \AND \ALL{R_m}{X} \AND C_\K) \AND C \AND \NOT
D \label{eq10}
\end{equation}
is unsatisfiable, where $R_1,\ldots, R_m$ are all the atomic roles
appearing in $\K$, and $C_\K = (\NOT C_1 \OR D_1) \AND \ldots\AND
(\NOT C_q \OR D_q)$.
\end{theorem}

\begin{proof}
If part. By contradiction.  Assume that (\ref{eq10}) is not
satisfiable, and suppose that $\K\not\models C\SUBD D$, i.e., there
exists an interpretation $\I$, and a valuation $\rho$ on $\I$, such
that $\I$ is a model of $\K$ and $\Inta{C}\not \subseteq \Inta{D}$.
It follows that, there exists an individual $s\in \dom$ such that
$s\in \Inta{C}$ and $s\in \INTA{\NOT D}$.  On the other hand, the fact
that $\I$ is a model of $\K$ implies that $\INTA{C_\K} = \dom$, and
thus that $\INTA{\nu X .(\ALL{R_1}{X} \AND \ldots \AND
\ALL{R_m}{X} \AND C_\K)}=\dom$.
So we have $s \in \INTA{\nu X .(\ALL{R_1}{X} \AND \ldots \AND \ALL{R_m}{X}
\AND C_\K) \AND C \AND \NOT D}$, i.e., (\ref{eq10}) is satisfiable,
contradicting the hypotheses.



Only If part. Again we proceed by contradiction.  Assume $\K\models
C\SUBD D$. And suppose that (\ref{eq10}) is satisfiable, i.e., there
exists an interpretation $\I$, a valuation $\rho$ on $\I$, and an
individual $s\in \dom$, such that $s\in\INTA{\nu X .(\ALL{R_1}{X}\AND
\ldots \AND \ALL{R_m}{X} \AND C_\K) \AND C \AND \NOT D}$.


Now consider the sub-interpretation $\I^s = (\doms, \Intas{\cdot})$
and the sub-valuation $\rho^s$ on $\I^s$ generated by $s$.  On the one
hand, we clearly have that $\INTAS{C_\K}= \doms$, hence $\I^s$ is a
model of $\K$. On the other hand by Lemma~\ref{TN3} $s\in \INTAS{\nu X
.(\ALL{R_1}{X} \AND \ldots \AND \ALL{R_m}{X} \AND C_\K) \AND C
\AND \NOT D}$, so it follows that $\I^s$ and $\rho^s$ do not
satisfy the subsumption $C\SUBD D$, contradicting the hypotheses.
\end{proof}

This result states that satisfiability of $\DL$ concepts and logical
implication in $\DL$ TBoxes (and thus of satisfiability of $\DL$ TBoxes)
are {\em not} distinct reasoning tasks. Hence in the following we will
limit our attention to concept satisfiability without loss of generality.


\section{Reasoning with Fixpoints}

In this section we concentrate on developing reasoning methods to check for
satisfiability concepts involving fixpoints. In particular, we exhibit a
correspondence between $\DL$ and a well-known logic of programs, called
{\em modal mu-calculus}
\cite{Koze-83,Koze-Pari-83,Stre-Emer-84,Stre-Emer-89}, that has been
recently investigated for expressing temporal properties of reactive and
parallel processes \cite{Stir-92,Lars-90,Clea-90,Wins-89,Dam-92}.

To get a better insight on the correspondence between the two logics,
we first study the sublanguage $\mu\ALC$ obtained from $\DL$ leaving
out qualified number restrictions\footnote{Observe that, in
Theorem~\ref{TN4} qualified number restrictions play no role. Hence
exactly the same reduction from logical implication to
unsatisfiability holds for $\mu\ALC$ as well. This allows us to
restrict our attention to satisfiability only.}. Then, we study the
full logic $\DL$.

\subsection{Reasoning in $\mu\ALC$}

Let us introduce modal mu-calculus formally.  Formulae $\Phi, \Psi, \ldots$
of modal mu-calculus are formed inductively from atomic formulae $A,\ldots$
and variables $X,\ldots$ according to the following abstract syntax:
\[\Phi,\Psi ::= A\mid\top \mid \bot \mid \neg \Phi\mid \Phi\wedge \Psi
\mid \Phi\vee \Psi \mid \DIAM{a}\Phi \mid \BOX{a}\Phi \mid \mu
X.\Phi\mid \nu X.\Phi \mid X\] where $a$ is the generic element of a
set of labels $\L$, and every bounded occurrence of every variable $X$
must be in the scope of an even number of negation signs.

The semantics of modal mu-calculus is based on the notions of (Kripke)
structure and valuation.  A {\em Kripke structure} $\M$ is a triple
$(\S,\{\R_i\mid i\in \L\},\V)$, where $\S$ is a set of states, each
$\R_i$ is a binary relation on $\S$, and $\V$ is a mapping from atomic
formulae to subsets of $\S$.  A {\em valuation} $\rho$ on $\M$ is a
mapping from variables to subsets of $\S$.  To a Kripke structure $\M$
and a valuation $\rho$ on $\M$, it is associated an extension function
$\Moda{\cdot}$ defined inductively as follows:
\[\begin{array}{lcl}

\Moda{X}  & = & \rho(X) \subseteq \S \\

\Moda{A}  & = & \V(A) \subseteq \S \\

\Moda{\top} & = & \S\\

\Moda{\bot} & = & \emptyset\\

\MODA{\NOT \Phi} & = & \S - \Moda{\Phi}\\

\MODA{\Phi \wedge \Psi} & = & \Moda{\Phi}\cap\Moda{\Psi}\\

\MODA{\Phi \vee \Psi} & = & \Moda{\Phi}\cup\Moda{\Psi}\\

\MODA{\DIAM{a}\Phi}  & = &  \{ s \in\S \mid\exists s'.\;
(s,s')\in \R_a \mbox{ and } s' \in \Moda{\Phi}\}\\

\MODA{\BOX{a}\Phi}  & = &   \{ s \in\S \mid\forall s'.\;
(s,s')\in \R_a \mbox{ implies } s' \in \Moda{\Phi}\}\\

\MODA{\mu X.\Phi} & = & 
\bigcap\{ \E\subseteq \S \mid \;\;\;\;\Modax{\Phi}{[X/\E]} \subseteq\E \;\}\\

\MODA{\nu X.\Phi} & = & 
\bigcup\{ \E\subseteq \S \mid  \;\;\;\;\E \subseteq \;\; \Modax{\Phi}{[X/\E]}
\;\}

\end{array}\]
A formula $\Phi$ is {\em satisfiable} if there exists a Kripke
structure $\M$ and a valuation $\rho$ on $\M$ such that $\Moda{\Phi}
\not= \emptyset$.


The following theorem is the basis for the correspondence between
$\mu\ALC$ and the modal mu-calculus.
 
\begin{theorem}\label{TN5}
There exists a one-to-one linear-time function $q$ mapping concepts of
$\mu\ALC$ to formulae of modal mu-calculus such that: for any
$\mu\ALC$ concept $C$, $C$ is satisfiable if and only if $q(C)$ is
satisfiable.
\end{theorem}

\begin{proof}
We can define $q$ in the following way: $q(A)=A$ (atomic concepts are
mapped to atomic formulae), $q(X)=X$, $q(\top) = \top$,
$q(\bot)=\bot$, $q(\NOT C) = \neg q(C)$, $q(\SOME{R}{C}) =
\DIAM{R}q(C)$ (atomic roles are mapped to labels), $q(\ALL{R}{C}) =
\BOX{R}q(C)$, $q(\mu X.C)= \mu X.q(C)$, and $q(\nu X.C)= \nu X.q(C)$.

An interpretation $\I=(\dom,\Int{\cdot})$ is equivalent to a Kripke
structure $\M=(\S,\{\R_i\mid i\in \L\},\V)$ such that: $\S =\dom$; $\L$ is
equal to the set of names of the atomic roles interpreted in $\I$;
$\R_R=\Int{R}$ for each atomic role $R$; and $\V(A)=\Int{A}$ for each
atomic concept $A$.  In addition, a valuation $\rho$ on $\I$ is equivalent
to a valuation $\rho'$ on $\M$.  Now both the extension function associated
with $\I$ and $\rho$ and the extension function associated with $\M$ and
$\rho'$ map, respectively, any concept $C$ and the corresponding formula
$q(C)$ to the same subset of $\dom = \S$. Hence the thesis follows.
\end{proof}



It follows that we may transfer both decidability and complexity
results for the modal mu-calculus
\cite{Koze-Pari-83,Emer-Jutl-88,Safr-88} to $\mu\ALC$.  Thus, we can
immediately state what is the complexity of reasoning with $\mu\ALC$
concepts and $\mu\ALC$ TBoxes.

\begin{theorem}
Satisfiability of $\mu\ALC$ concepts, satisfiability of $\mu\ALC$
TBoxes, and logical implication in $\mu\ALC$ TBoxes are
EXPTIME-complete problems.
\end{theorem}

\begin{proof}
  The satisfiability problem for modal mu-calculus is EXPTIME-complete
  \cite{Emer-Jutl-88}, hence by Theorem~\ref{TN5} and by Theorem~\ref{TN4}
  the thesis follows.
\end{proof}



\subsection{Reasoning in $\DL$}

Next we exhibit a mapping from $\DL$ concepts to formulae of variant of
modal mu-calculus, called {\em deterministic modal mu-calculus}, which has
the same syntax as the modal mu-calculus, but is interpreted over {\em
  deterministic Kripke structures}, that is Kripke structures
$\M=(\S,\{\R_i\mid i\in \L\},\V)$ in which the relations $\R_i$ are partial
functions \cite{Stre-Emer-84}.

Let us ignore for a moment the qualified number restriction constructs.
Formulae of $\DL$ without qualified number restrictions are, in fact,
formulae of the modal mu-calculus, as shown in the previous section.  By
using a well-known technique developed for propositional dynamic logic
\cite{Pari-81}, (nondeterministic) modal mu-calculus formulae can be
reduced to deterministic modal mu-calculus formulae \cite{Stre-Emer-84}, as
shown below.

We use the following notations for usual operations on binary
relations: $\cdot\circ\cdot$ for {\em chaining}, $\cdot^*$ for {\em
reflexive transitive closure}, $\cdot^+$ for {\em transitive closure},
and $\cdot^-$ for {\em converse}.  We also use the following
abbreviations:
\[\begin{array}{lcl}
\BOX{R^*}\phi &\mbox{ for }& \nu X.(\phi\wedge \BOX{R} X)\\

\BOX{R^+}\phi &\mbox{ for }& \BOX{R}{\BOX{R^*}{\phi}}\\

\DIAM{R^*}\phi &\mbox{ for }& \mu X.(\phi\vee \DIAM{R} X)\\

\DIAM{R^+}\phi &\mbox{ for }& \DIAM{R}{\DIAM{R^*}{\phi}}.
\end{array}\]

The reduction is as follows: in a formula $\Phi$, we recursively
replace each subformulae of the form $\BOX{R}{\phi}$ by
$\BOX{R}{\BOX{(R_{new})^*}{\phi}}$ and each subformulae of the form
$\DIAM{R}{\phi}$ by $\DIAM{R}{\DIAM{(R_{new})^*}{\phi}}$, where
$R_{new}$ is a new symbol and both $R$ and $R_{new}$ in the resulting
formula are interpreted as partial functions.  Let us call the
resulting formula $\Phi'$, we have that $\Phi$ is satisfiable if and
only if $\Phi'$ is satisfiable.


We briefly sketch the reasoning behind the proof of this statement.
The if direction is easy: it suffices to observe that if
$M^D=(\S^D,\{\R^D_i\mid i\in \L^D\},\V^D)$ is a model of $\Phi'$, then
can transform it into a model $\M=(\S,\{\R_i\mid i\in \L\},\V)$ of
$\Phi$ by defining $\S=\S^D$, $\L=\L^D-{new}$,
$\R_{R}=\R^D_{R}\circ(\R^D_{new})^*$, and $\V=\V^D$.  The only if
direction is as follows.  We recall that both nondeterministic and
deterministic modal mu-calculus have the tree model property
\cite{Stre-Emer-89,Stre-Emer-84}: if a formula has a model it has a
tree model, i.e., a model having the form of a {\em
tree}\footnote{Given a model of $\Phi$ we get a tree model simply by
``unfolding'' the original one.}. So without loss of generality we can
restrict our attention to tree models only.  Now there is a one-to-one
transformation from tree models $M^T=(\S^T,\{\R^T_i\mid i\in
\L^T\},\V^T)$ of $\Phi$ to (tree) models $M^B=(\S^B,\{\R^B_i\mid i\in
\L^B\},\V^B)$ of $\Phi'$. Indeed, we put $\S^B = \S^T$, $\V^B=\V^T$,
$\L^B=\L^T$, and given a state $x\in\S^T$ having as
$\R^T_{R}$-successors $z_1,\ldots,z_l$,\footnote{ We implicitly assume
that $M^T$ is a finite branching tree model. This can be done without
loss of generality since modal mu-calculus has the finite model
property, and hence unfolding a finite model we get a finite branching
tree model. Note however that it would suffice to assume $M^T$ to be a
countable branching tree model.} we put $(x,z_1)\in\R^B_{R}$, and
$(z_i,z_{i+1})\in\R^B_{R_{new}}$, for $i=1,\ldots,l-1$. In this way we
have $(x,z_i)\in \R^T_{R}$ if and only if $(x,z_i)\in \R^B_{R}\circ
(\R^B_{R_{new}})^*$.\footnote{Note that this construction is similar
to the one often used in programming to reduce n-ary trees to binary
trees by coding children of a node as the combination of one child and
its siblings.}

We remark that $M^T$ is required to be a tree because once we get
$M^B$ we need to recover the ``original'' $\R^T_{R}$-predecessor $x$
of a state $z_i$, namely we need $(\R^B_{R}\circ
(\R^B_{R_{new}})^*)^-$ to be {\em a partial function}, otherwise,
given a state $z_i$, we would not know which of the various
$(\R^B_{R}\circ (\R^B_{R_{new}})^*)^-$-successors is its original
$\R^T_{R}$-predecessor $x$, and therefore we would not be able to
reconstruct $M^T$ from $M^B$.

\bigskip 
By interpreting $R$ and $R_{new}$ as partial functions, it easy to
express qualified number restrictions as constraints on the chain of
$(R\circ R_{new}^*)$-successors of a state.  For example:
$\ATMOST{3}{R.\phi}$ can be expressed by
\[ \BOX{R}{\BOX{(R_{new})^*}{(\neg\phi\vee
    \BOX{(R_{new})^+}{(\neg\phi\vee \BOX{(R_{new})^+}{(\neg\phi\vee
          \BOX{(R_{new})^+}{\neg \phi})})})}}\] and can be read as
``everywhere along the chain $R\circ(R_{new})^*$ there are at most three
states where $\phi$ holds'', which corresponds exactly to the intended
meaning.  Similarly $\ATLEAST{3}{R.\phi}$ can be expressed by
\[\DIAM{R}{\DIAM{(R_{new})^*}{(\phi \wedge \DIAM{(R_{new})^+}{(\phi\wedge
\DIAM{(R_{new})^+}{\phi})})}}\] and can be read as ``somewhere along
the chain $R\circ(R_{new})^*$ there are at least three states where
$\phi$ holds'', which again corresponds exactly to the intended
meaning.


The above discussion allows us to state the following result. 

\begin{theorem}\label{TN5'}
There exists a polynomial function $t$ mapping concepts of $\DL$ to
formulae of deterministic modal mu-calculus such that: for any $\DL$
concept $C$, $C$ is satisfiable if and only if $u(C)$ is satisfiable.
\end{theorem}
\begin{proof}
The function $t$ is defined inductively as follows:
\[\begin{array}{lcl}  
u(A) &=& A\\
u(X) &=& X\\ 
u(C_1\AND C_1) &=& u(C_1)\wedge u(C_2)\\
u(C_1\OR C_2) &=& u(C_1)\vee u(C_2)\\
u(\NOT C) &=& \neg u(C)\\ 
u(\mu X.C) &=&\mu X.u(C)\\
u(\nu X.C) &=&\nu X.u(C)\\
u(\SOME{R}{C}) &=& \DIAM{R}{\DIAM{(R_{new})^*}{u(C)}}\\
u(\ALL{R}{C}) &=& \BOX{R}{\BOX{(R_{new})^*}{u(C)}}
\end{array}\]
where $R_{new}$ is a new role.  Finally, $\ATMOST{n}{R.C}$ and
$\ATLEAST{n}{R.C}$ are mapped to the following formulae:

\[\arraycolsep=0pt
\begin{array}{ll}
u(\ATMOST{n}{R.C}) = & 
\BOX{R}
\BOX{(R_{new})^*}(\neg u(C)\vee 
  \BOX{(R_{new})^+}(\neg u(C)\vee\\
& \BOX{(R_{new})^+}(\ldots 
(\neg u(C)\vee \BOX{(R_{new})^+}\neg u(C))\ldots)))
\end{array}\]
where the number of nested formulae of the form $\neg u(C)\vee
\BOX{(R_{new})^+}\Phi$ is $n$, and

\[\arraycolsep=0pt
\begin{array}{ll}
u(\ATLEAST{n}{R.C}) = & 
\DIAM{R}\DIAM{(R_{new})^*}(u(C)\wedge
\DIAM{(R_{new})^+}(u(C)\wedge\\
& \DIAM{(R_{new})^+}(\ldots (u(C) \wedge
\DIAM{(R_{new})^+}u(C))\ldots)))
\end{array}\]
where the number of nested formulae of the form $u(C) \wedge
\DIAM{(R_{new})^+}\Phi$ is $n-1$.

$u(C)$ is clearly polynomial in the size of $C$ (under the usual
assumption that numbers in $C$ coded in unary). Moreover, following
the technique in \cite{Pari-81,Stre-Emer-84} that as been exposed
above, it is easy to verify, by induction on the formation of the
concept $C$, that the mapping $t$ preserves satisfiability.
\end{proof}

It follows that we may transfer both decidability and complexity results
for the deterministic modal mu-calculus
\cite{Stre-Emer-84,Emer-Jutl-88,Safr-88} to $\DL$.  Thus, we can
immediately state what is the complexity of reasoning with $\DL$ concepts
and $\DL$ TBoxes.
\begin{theorem}
Satisfiability of $\DL$ concepts, satisfiability of $\DL$ TBoxes, and
logical implication in $\DL$ TBoxes are EXPTIME-complete problems.
\end{theorem}
\begin{proof}
  Satisfiability in deterministic modal mu-calculus is an
  EXPTIME-complete problem \cite{Stre-Emer-84,Emer-Jutl-88,Safr-88}.
  Hence by Theorem~\ref{TN5'} and Theorem~\ref{TN4} the thesis
  follows.
\end{proof}



\section{Discussion and Conclusion}

The work presented in this paper stems out from \cite{D-CNKRR-93}, where
the basic ideas of introducing explicit fixpoint was first presented, and
\cite{DL-ECAI-94}, where such idea was further elaborated and $\DL$ was
first introduced.

One of the main contributions of this work has been to devise a tight
correspondence between description logics with fixpoints and modal
mu-calculus. In this respect we remark that, while $\mu\ALC$
corresponds directly to modal mu-calculus, the full $\DL$ corresponds
to a variant of modal mu-calculus whose decidability and complexity
had not been studied.  More precisely, a notion essentially equivalent
to that of qualified number restrictions has independently emerged in
modal logics, namely that of {\em graded modalities}
\cite{VanD-DeRi-95,VanD-92,Fatt-DeCa-85,Fine-72}.  However the
combination of fixpoints and graded modalities had not been
investigated before in the setting of modal logics.  Given the tight
correspondence between $\mu\ALC$ and modal mu-calculus, $\DL$ can be
considered as {\em modal mu-calculus augmented with graded
modalities}. Hence the results in this paper apply to such a logic as
well.

\bigskip The research reported in this paper bears several similarities
with the one on the correspondence between description logics and
propositional dynamic logics
\cite{Baad91,Schi91,DL-AAAI-94,DL-IJCAI-95,D-PHDTHESIS-95}.  In fact what
characterize description logics based on propositional dynamic logics are
the role constructs for chaining, choice, test, and above all reflexive
transitive closure of roles, which is a limited form of fixpoint.  Such
role constructs can be easily expressed by using the explicit fixpoints
introduced here. It suffice to resort to the following equivalences:
\[\begin{array}{l}
\SOME{R_1\circ R_2}{C} = \SOME{R_1}{\SOME{R_2}{C}}\\
\SOME{R_1\OR R_2}{C} = \SOME{R_1}{C}\OR\SOME{R_2}{C}\\
\SOME{R^*}{C} = \mu X . (C \OR\SOME{R}{X})\\
\SOME{id(D)}{C} = C \AND D.
\end{array}\]
Note that $\ALL{R^*}{C} = \nu X . (C\AND\ALL{R}{X})$.  In
\cite{CDL-DOOD-95} a further implicit form of fixpoint has been advocated,
the so called well-founded role construct $wf(R)$. By explicit fixpoints,
$wf(R)$ is expressed simply as $\mu X.(\ALL{R}{X})$.

Our proposal of allowing for fixpoint constructs explicitly in the
formalism is shared by the study independently carried out by Schild in
\cite{Schi94}\footnote{ In \cite{Schi94} number restrictions are not
  considered.}. The main goal of that work is to study both the expressive
power and the computational complexity of subsumption and satisfiability
for TBoxes expressed in $\ALC$ (no fixpoint constructs), that allow for
{\em mutually} recursive definitions. To this end, a description logic is
defined that corresponds to a variant of the modal mu-calculus in which
{\em mutual fixpoints} are allowed but some restrictions on nested
fixpoints are enforced \cite{Vard-Wolp-84}. It is well known that mutual
fixpoints can be re-expressed by means of nested ones \cite<see, for
example,>{Park-76,DeBa-80}. As a consequence of this observation it follows
that the logic introduced in this paper, is more expressive than the one
analyzed in \cite{Schi94} since, on the one hand, it allows nesting of
fixpoints without any restriction, on the other hand it makes it possible
to state sophisticated forms of cardinality constraints on role fillers by
means of qualified number restrictions.


\bigskip

The present work can be extended along several directions.  We conclude by
outlining two of them.

We already noticed that fixpoint constructs allow for representing not
only abstract classes, but also several data structures extensively
used in software development. We believe that this characteristic is
an important step towards a satisfactory integration of description
logics with both traditional and declarative programming systems.
Indeed the description logic proposed in this paper provides powerful
mechanisms for data structure modeling. In particular, the properties
stated in Section~\ref{mu-prop} can be the base to formulate a notion
of {\em parametric concept}\footnote{ Note that parametric concepts
can be introduced also in simpler logics which do not include fixpoint
constructs.}.  For instance, the expression (named $dag\_of[Z]$) $$\mu
X \st emptydag \OR (Z \AND \SOME{arc}{\top} \AND \ALL{arc}{X})$$ where
$Z$ is a formal parameter, denotes the class of DAGs whose nodes are
left unspecified. This class can be used in several ways in the
TBox. For example, it can be instantiated by binding the formal
parameter to actual parameters, thus getting, say, $dag\_of[student]$,
$dag\_of[person]$, etc., which are concepts inheriting the properties
of $dag\_of[Z]$.


Although $\DL$ is a powerful logic, it lacks the construct for {\em inverse
  roles} which is needed for example to correctly capture the notions of
(finite) TREE, BINARY-TREE, etc.\ Indeed, to define the concept of TREE (an
EMPTY-TREE is a TREE; a NODE that has at most one parent, some children,
and all children are TREEs, is a TREE; nothing else is a TREE) we can write
$tree \equiv \mu X \st empty\_tree \OR (node\AND \ATMOST{1}{child^{-}.\top}
\AND \SOME{child}{\top} \AND \ALL{child}{X}$ where $child^-$ denotes the
inverse of $child$.  Notice that the introduction of inverse roles does not
pose any difficulty from the semantical point of view; however, its impact
on the reasoning method needs to be investigated. More generally, a wide
variety of concept constructs can be studied in conjunction with fixpoints.
The research on description logics related to propositional dynamic logics
in \cite{DL-AAAI-94,DL-IJCAI-95,CDL-DOOD-95,D-PHDTHESIS-95} may give us
hints on how to proceed along this direction.



\bibliographystyle{theapa}
%\bibliography{lop,mia,cikm.altri,medium-string,knowledge-repr}
\begin{thebibliography}{}

\bibitem[\protect\BCAY{Baader}{Baader}{1990}]{Baad90c}
Baader, F. \BBOP1990\BBCP.
\newblock \BBOQ Terminological cycles in {KL-ONE}-based knowledge
  representation languages\BBCQ\
\newblock In {\Bem Proc.\ of the 8th Nat.\ Conf.\ on Artificial Intelligence
  (AAAI-90)}, \BPGS\ 621--626\ Boston, Ma.

\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 Proc.\ of the 12th Int.\ Joint Conf.\ on Artificial
  Intelligence (IJCAI-91)}\ Sydney, Australia.

\bibitem[\protect\BCAY{Beeri}{Beeri}{1990}]{Beer90}
Beeri, C. \BBOP1990\BBCP.
\newblock \BBOQ A formal approach to object-oriented databases\BBCQ\
\newblock {\Bem Data and Knowledge Engineering}, {\Bem 5}, 353--382.

\bibitem[\protect\BCAY{Beneventano \BBA\ Bergamaschi}{Beneventano \BBA\
  Bergamaschi}{1992}]{BergaICDT}
Beneventano, D.\BBACOMMA\  \BBA\ Bergamaschi, S. \BBOP1992\BBCP.
\newblock \BBOQ Subsumption for complex object data models\BBCQ\
\newblock In {\Bem Proc.\ of the 4th Int.\ Conf.\ on Database
  Theory (ICDT-92)}, \lowercase{\BNUM}\ 646 in Lecture Notes in Computer Science, \BPGS\
  357--375. Springer-Verlag.

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

\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{Calvanese, De~Giacomo, \BBA\ Lenzerini}{Calvanese
  et~al.}{1995}]{CDL-DOOD-95}
Calvanese, D., De~Giacomo, G., \BBA\ Lenzerini, M. \BBOP1995\BBCP.
\newblock \BBOQ Structured objects: modeling and reasoning\BBCQ\
\newblock In {\Bem Proc.\ of the 4th Int.\ Conf.\ on
  Deductive and Object-Oriented Databases ({DOOD-95})}, Lecture Notes in
  Computer Science. Springer-Verlag.

\bibitem[\protect\BCAY{Cleaveland}{Cleaveland}{1990}]{Clea-90}
Cleaveland, R. \BBOP1990\BBCP.
\newblock \BBOQ Tableaux-based model checking in the propositional
  mu-calculus\BBCQ\
\newblock {\Bem Acta Informatica}, {\Bem 27}, 725--747.

\bibitem[\protect\BCAY{Dam}{Dam}{1992}]{Dam-92}
Dam, M. \BBOP1992\BBCP.
\newblock \BBOQ {CTL*} and {ECTL*} as fragments of the modal mu-calculus\BBCQ\
\newblock In {\Bem Proceeding of the Col.\ on Trees and Algebra in
  Programming}, \lowercase{\BNUM}\ 581 in Lecture Notes in Computer Science,
  \BPGS\ 145--164. Springer-Verlag.

\bibitem[\protect\BCAY{de~Bakker}{de~Bakker}{1980}]{DeBa-80}
de~Bakker, J. \BBOP1980\BBCP.
\newblock {\Bem Mathematical Theory of Program Correctness}.
\newblock Prentice-Hall.

\bibitem[\protect\BCAY{De~Giacomo}{De~Giacomo}{1993}]{D-CNKRR-93}
De~Giacomo, G. \BBOP1993\BBCP.
\newblock \BBOQ Reconciling different semantics for concept definition
  (extended abstract)\BBCQ\
\newblock In {\Bem Proc.\ of the 1st {COMPULOG} Net Meeting on Knowledge
  Representation and Reasoning Systems ({CNKRR-93})}.

\bibitem[\protect\BCAY{De~Giacomo}{De~Giacomo}{1995}]{D-PHDTHESIS-95}
De~Giacomo, G. \BBOP1995\BBCP.
\newblock {\Bem Decidability of Class-Based Knowledge Representation
  Formalisms}.
\newblock Ph.D.\ thesis, Dipartimento di Informatica e Sistemistica,
  Universit\`a di Roma {``La Sapienza''}.

\bibitem[\protect\BCAY{De~Giacomo \BBA\ Lenzerini}{De~Giacomo \BBA\
  Lenzerini}{1994a}]{DL-AAAI-94}
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 Proc.\ of the 12th Nat.\ Conf.\ 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}]{DL-ECAI-94}
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 Proc.\ of the 11th Eur.\ Conf.\ on
  Artificial Intelligence ({ECAI-94})}, \BPGS\ 411--415. John Wiley and Sons.

\bibitem[\protect\BCAY{De~Giacomo \BBA\ Lenzerini}{De~Giacomo \BBA\
  Lenzerini}{1995}]{DL-IJCAI-95}
De~Giacomo, G.\BBACOMMA\  \BBA\ Lenzerini, M. \BBOP1995\BBCP.
\newblock \BBOQ What's in an aggregate: foundation for description logics with
  tuples and set\BBCQ\
\newblock In {\Bem Proc.\ of the 14th Int.\ Conf.\ on
  Artificial Intelligence ({IJCAI-95})}.

\bibitem[\protect\BCAY{Emerson \BBA\ Jutla}{Emerson \BBA\
  Jutla}{1988}]{Emer-Jutl-88}
Emerson, E.~A.\BBACOMMA\  \BBA\ Jutla, C.~S. \BBOP1988\BBCP.
\newblock \BBOQ The complexity of tree automata and logics of programs\BBCQ\
\newblock In {\Bem Proc.\ of the 20th An.\ Symp.\ on the Foundations
  of Computer Science (FOCS-88)}, \BPGS\ 328--337.

\bibitem[\protect\BCAY{Fattorosi-Barnaba \BBA\ De~Caro}{Fattorosi-Barnaba \BBA\
  De~Caro}{1985}]{Fatt-DeCa-85}
Fattorosi-Barnaba, M.\BBACOMMA\  \BBA\ De~Caro, F. \BBOP1985\BBCP.
\newblock \BBOQ Graded modalities {I}\BBCQ\
\newblock {\Bem Studia Logica}, {\Bem 44}, 197--221.

\bibitem[\protect\BCAY{Fine}{Fine}{1972}]{Fine-72}
Fine, K. \BBOP1972\BBCP.
\newblock \BBOQ In so many possible worlds\BBCQ\
\newblock {\Bem Notre Dame Journal of Formal Logic}, {\Bem 13\/}(4), 516--520.

\bibitem[\protect\BCAY{Kozen}{Kozen}{1983}]{Koze-83}
Kozen, D. \BBOP1983\BBCP.
\newblock \BBOQ Results on the propositional mu-calculus\BBCQ\
\newblock {\Bem Theoretical Computer Science}, {\Bem 27}, 333--355.

\bibitem[\protect\BCAY{Kozen \BBA\ Parikh}{Kozen \BBA\
  Parikh}{1983}]{Koze-Pari-83}
Kozen, D.\BBACOMMA\  \BBA\ Parikh, R. \BBOP1983\BBCP.
\newblock \BBOQ A decision procedure for the propositional mu-calculus\BBCQ\
\newblock In {\Bem Proc.\ of the 2nd Work.\ on Logic of Programs},
  \lowercase{\BNUM}\ 164 in Lecture Notes in Computer Science, \BPGS\ 313--325.
  Springer-Verlag.

\bibitem[\protect\BCAY{Larsen}{Larsen}{1990}]{Lars-90}
Larsen, K.~J. \BBOP1990\BBCP.
\newblock \BBOQ Proof systems for satisfiability in {H}ennessy-{M}ilner logic
  with recursion\BBCQ\
\newblock {\Bem Theoretical Computer Science}, {\Bem 72}, 265--288.

\bibitem[\protect\BCAY{Nebel}{Nebel}{1990}]{Nebe90b}
Nebel, B. \BBOP1990\BBCP.
\newblock {\Bem Reasoning and Revision in Hybrid Representation Systems}.
\newblock \BNUM\ 422 in Lecture Notes in Artificial Intelligence.
  Springer-Verlag.

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

\bibitem[\protect\BCAY{Parikh}{Parikh}{1981}]{Pari-81}
Parikh, R. \BBOP1981\BBCP.
\newblock \BBOQ Propositional dynamic logic of programs: A survey\BBCQ\
\newblock In {\Bem Proc.\ of the 1st Work.\ on Logic of Programs},
  \lowercase{\BNUM}\ 125 in Lecture Notes in Computer Science, \BPGS\ 102--144.
  Springer-Verlag.

\bibitem[\protect\BCAY{Park}{Park}{1976}]{Park-76}
Park, D. \BBOP1976\BBCP.
\newblock \BBOQ Finiteness is mu-ineffable\BBCQ\
\newblock {\Bem Theoretical Computer Science}, {\Bem 3}, 173--181.

\bibitem[\protect\BCAY{Safra}{Safra}{1988}]{Safr-88}
Safra, S. \BBOP1988\BBCP.
\newblock \BBOQ On the complexity of $\omega$-automata\BBCQ\
\newblock In {\Bem Proc.\ of the 20th An.\ Symp.\ on the Foundations
  of Computer Science (FOCS-88)}, \BPGS\ 319--327.

\bibitem[\protect\BCAY{Schild}{Schild}{1991}]{Schi91}
Schild, K. \BBOP1991\BBCP.
\newblock \BBOQ A correspondence theory for terminological logics: Preliminary
  report\BBCQ\
\newblock In {\Bem Proc.\ of the 12th Int.\ Joint Conf.\ on Artificial
  Intelligence (IJCAI-91)}, \BPGS\ 466--471\ Sydney, 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 Proc.\ of
  the 4th Int.\ Conf.\ 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{Stirling}{Stirling}{1992}]{Stir-92}
Stirling, C. \BBOP1992\BBCP.
\newblock \BBOQ Modal and temporal logic\BBCQ\
\newblock In Abramsky, S., Gabbay, D.~M., \BBA\ Maibaum, T. S.~E.\BEDS, {\Bem
  Handbook of Logic in Computer Science}, \BPGS\ 477--563. Clarendon Press,
  Oxford.

\bibitem[\protect\BCAY{Streett \BBA\ Emerson}{Streett \BBA\
  Emerson}{1984}]{Stre-Emer-84}
Streett, R.~S.\BBACOMMA\  \BBA\ Emerson, E.~A. \BBOP1984\BBCP.
\newblock \BBOQ The propositional mu-calculus is elementary\BBCQ\
\newblock In {\Bem Proc.\ of the 6th Int.\ Col.\ on Automata,
  Languages and Programming}, \lowercase{\BNUM}\ 172 in Lecture Notes in
  Computer Science, \BPGS\ 465--472. Springer-Verlag.

\bibitem[\protect\BCAY{Streett \BBA\ Emerson}{Streett \BBA\
  Emerson}{1989}]{Stre-Emer-89}
Streett, R.~S.\BBACOMMA\  \BBA\ Emerson, E.~A. \BBOP1989\BBCP.
\newblock \BBOQ An automata theoretic decision procedure for the propositional
  mu-calculus\BBCQ\
\newblock {\Bem Information and Control}, {\Bem 81}, 249--264.

\bibitem[\protect\BCAY{Tarski}{Tarski}{1955}]{Tarski55}
Tarski, A. \BBOP1955\BBCP.
\newblock \BBOQ A lattice-theoretical fixpoint theorem and its
  applications\BBCQ\
\newblock {\Bem Pacific Journal of Mathematics}, {\Bem 5}, 285--309.

\bibitem[\protect\BCAY{Van~der Hoek}{Van~der Hoek}{1992}]{VanD-92}
Van~der Hoek, W. \BBOP1992\BBCP.
\newblock \BBOQ On the semantics of graded modalities\BBCQ\
\newblock {\Bem Journal of Applied Non-Classical Logics}, {\Bem 2\/}(1),
  81--123.

\bibitem[\protect\BCAY{Van~der Hoek \BBA\ de~Rijke}{Van~der Hoek \BBA\
  de~Rijke}{1995}]{VanD-DeRi-95}
Van~der Hoek, W.\BBACOMMA\  \BBA\ de~Rijke, M. \BBOP1995\BBCP.
\newblock \BBOQ Counting objects\BBCQ\
\newblock {\Bem Journal of Logic and Computation}, {\Bem 5\/}(3), 325--345.

\bibitem[\protect\BCAY{Vardi \BBA\ Wolper}{Vardi \BBA\
  Wolper}{1984}]{Vard-Wolp-84}
Vardi, M.~Y.\BBACOMMA\  \BBA\ Wolper, P. \BBOP1984\BBCP.
\newblock \BBOQ Automata theoretic techniques for modal logics of
  programs\BBCQ\
\newblock In {\Bem Proc.\ of the 16th An.\ Symp.\ on the Foundations
  of Computer Science (FOCS-84)}, \BPGS\ 446--456.

\bibitem[\protect\BCAY{Winsket}{Winsket}{1989}]{Wins-89}
Winsket, G. \BBOP1989\BBCP.
\newblock \BBOQ A note on model checking the modal $\nu$-calculus\BBCQ\
\newblock In {\Bem Proc.\ of the 11th Int.\ Col.\ on
  Automata, Languages and Programming}, \lowercase{\BNUM}\ 372 in Lecture Notes
  in Computer Science, \BPGS\ 761--772. Springer-Verlag.

\end{thebibliography}

\end{document}


