\documentclass[letterpaper,jair,twoside,11pt]{article}

\usepackage{theapa}
\usepackage{jair}
\usepackage{latexsym}  
\usepackage{epsfig,boxedminipage}
\usepackage{amssymb,amsthm,amsmath,bbm}
%\usepackage{amssymb,amsmath}
\usepackage{pifont}
\usepackage{xspace}

%\voffset=-.5in \hoffset=-.35in
%\textwidth=14.5cm \textheight=22.5cm

\bibliographystyle{theapa}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{example}[theorem]{Example}
\newtheorem{observation}[theorem]{Observation}
\newtheorem{claim}[theorem]{Claim}
\newtheorem{fact}[theorem]{Fact} 

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\newcommand{\auf}{\left\langle}
\newcommand{\zu}{\right\rangle}
\newcommand{\U}{{\sf U}}
\newcommand{\geqn}{\exists_{\geq n}}
\newlength{\indxlength}
\setlength{\indxlength}{4mm}
\newcommand{\ind}[1]{\hspace*{#1\indxlength}}

\def\endmark{\hskip 2em\begin{picture}(8,10)
\put(0,0){\ding{111}}
%\put(2,0){\rule{1.9mm}{0.3mm}}
%\put(6.5,0){\rule{0.3mm}{1.9mm}}
\end{picture}
\par}
\def\proof{\trivlist \item[\hskip \labelsep{\bf Proof.\ }]}
\def\endproof{\null\hfill\endmark\endtrivlist}
\def\proofsketch{\trivlist \item[\hskip \labelsep{\em Proof sketch.\ }]}
\def\endproofsketch{\null\hfill\endmark\endtrivlist}

\def\BBN{{\mathbb N}}
\def\BBZ{{\mathbb Z}}
\def\BBQ{{\mathbb Q}}
\def\BBR{{\mathbb R}}
\markboth{\today}{\today}
\def\nb #1{\marginpar{\footnotesize #1}}
\def\c #1{{\cal #1}}
\def\b #1{{\bar{#1}}}
\def\g #1{{\mathfrak #1}}
\def\wh #1{\widehat{#1}}
\def\mon{monodic}

\def\bigop#1{\mathop{\mathchoice
{\vcenter{\hbox{\huge$#1$}}}
{\vcenter{\hbox{\Large$#1$}}}
{\vcenter{\hbox{\large$#1$}}}
{\vcenter{\hbox{$\scriptstyle #1$}}}}
\displaylimits}
\def\Forall{\bigop{\forall}}
\def\Exists{\bigop{\exists}}

\font\msam=msam10
\def\Bx{\mbox{\msam\char"04}}
\def\Dm{\mbox{\msam\char"07}}


%\def\funny#1#2#3{\hbox to 0pt{$\displaystyle #1_{{#2}}^{{#3}}$}
%\phantom{\displaystyle #1}}



\def\rt{{\it right}}
\def\lt{{\it left}}
\def\up{{\it up}}
\def\down{{\it down}}

\newcommand{\defn}[1]{\emph{#1}}
\newcommand{\AL}{\ensuremath{\mathcal{AL}}\xspace}
\newcommand{\ALC}{\ensuremath{\mathcal{ALC}}\xspace}
\newcommand{\ALCD}{\ensuremath{\mathcal{ALC(D)}}\xspace}
\newcommand{\ALCF}{\ensuremath{\mathcal{ALCF}}\xspace}
\newcommand{\ALCQ}{\ensuremath{\mathcal{ALCQ}}\xspace}
\newcommand{\ALCN}{\ensuremath{\mathcal{ALCN}}\xspace}
\newcommand{\ALCH}{\ensuremath{\mathcal{ALC_H}}\xspace}
\newcommand{\ALCO}{\ensuremath{\mathcal{ALCO}}\xspace}
\newcommand{\SHIQ}{\ensuremath{\mathcal{SHIQ}}\xspace}
\newcommand{\Amc}{\ensuremath{\mathcal{A}}\xspace}
\newcommand{\Bmc}{\ensuremath{\mathcal{B}}\xspace}
\newcommand{\Cmc}{\ensuremath{\mathcal{C}}\xspace}
\newcommand{\Dmc}{\ensuremath{\mathcal{D}}\xspace}
\newcommand{\Fmc}{\ensuremath{\mathcal{F}}\xspace}
\newcommand{\Gmc}{\ensuremath{\mathcal{G}}\xspace}
\newcommand{\Hmc}{\ensuremath{\mathcal{H}}\xspace}
\newcommand{\Imc}{\ensuremath{\mathcal{I}}\xspace}
\newcommand{\Lmc}{\ensuremath{\mathcal{L}}\xspace}
\newcommand{\Mmc}{\ensuremath{\mathcal{M}}\xspace}
\newcommand{\Nmc}{\ensuremath{\mathcal{N}}\xspace}
\newcommand{\Qmc}{\ensuremath{\mathcal{Q}}\xspace}
\newcommand{\Rmc}{\ensuremath{\mathcal{R}}\xspace}
\newcommand{\Smc}{\ensuremath{\mathcal{S}}\xspace}
\newcommand{\Tmc}{\ensuremath{\mathcal{T}}\xspace}

\newcommand{\Lmf}{\ensuremath{\mathfrak{W}}\xspace}
\newcommand{\Vmf}{\ensuremath{\mathfrak{V}}\xspace}
\newcommand{\Wmf}{\ensuremath{\mathfrak{W}}\xspace}
\newcommand{\Fmf}{\ensuremath{\mathfrak{F}}\xspace}

\newcommand{\mn}[1]{\ensuremath{\text{{\it #1}}}}

\newcommand{\rec}{\mn{sur}}

\newcount\XXXoption\XXXoption=0
\def\pdfimgs{\XXXoption=1}
\def\nopdfimgs{\XXXoption=0}
\long\def\inclimg#1{\hbox{}\ifnum\XXXoption>0\includegraphics{#1.pdf}\else\includegraphics{#1.pstex}\fi}

%
% Choose here \pdfimgs for pdflatex and \nopdfimgs for latex
% Also make sure that, inside .pstex_t files, \inclimg is used
% instead of \include
%
% see also the 'fig2pdf' shellscript
%
\pdfimgs

\author{Franz Baader${}^1$ \and Carsten Lutz${}^1$ \and Holger Sturm${}^2$ \and Frank Wolter${}^3$}

\date{}

\jairheading{16}{2002}{1-58}{7/01}{1/02}
\ShortHeadings{Fusions of Description Logics and Abstract Description Systems}
{Baader, Lutz, Sturm, \& Wolter}
\firstpageno{1}

\begin{document}

\title{Fusions of Description Logics and \\  Abstract Description Systems}

\author{\name Franz Baader \email baader@cs.rwth-aachen.de \\
       \name Carsten Lutz \email lutz@cs.rwth-aachen.de \\
       \addr Teaching and Research Area for Theoretical Computer
       Science, \\
       RWTH Aachen, 
       Ahornstra{\ss}e 55, 52074 Aachen, Germany
       \AND
       \name Holger Sturm \email holger.sturm@uni-konstanz.de \\
       \addr Fachbereich Philosophie, Universit{\"a}t Konstanz, \\
       78457 Konstanz, Germany
       \AND
       \name Frank Wolter \email wolter@informatik.uni-leipzig.de \\
       \addr Institut f{\"u}r Informatik, Universit{\"a}t Leipzig, \\
       Augustus-Platz 10-11, 04109 Leipzig, Germany}

\maketitle

\begin{abstract}
Fusions are a simple way of combining logics. For normal modal logics,
fusions have been investigated in detail. In particular, it is known that,
under certain conditions, decidability transfers from the component logics to their fusion.
Though description logics are closely related to modal logics, they
are not necessarily normal. In addition, ABox reasoning in description logics
is not covered by the results from modal logics.

In this paper, we extend the decidability transfer results from normal modal logics to a large
class of description logics. To cover different description logics in a uniform
way, we introduce abstract description systems, which can be seen as a common
generalization of description and modal logics, and show the transfer
results in this general setting.
\end{abstract}

\section{Introduction}
%
Knowledge representation systems based on description logics (DL)
can be used to represent the  knowledge
of an application domain in a structured and formally well-understood way
\cite{BrSc85,BaHo91,BMPAB91,WoSc92,Borg95,Horr98}.
In such systems, the important notions of the domain
can be described by \emph{concept descriptions}, i.e., expressions that
are built from atomic concepts (unary predicates) and atomic roles
(binary predicates) using the concept constructors provided by the
description logic employed by the system.
The atomic concepts and the concept descriptions represent sets
of individuals, whereas roles represent binary relations between individuals.
For example, using the atomic concepts $\mathsf{Woman}$ and $\mathsf{Human}$,
and the atomic role $\mathsf{child}$, the concept of all \emph{women having
only daughters} (i.e., women such that all their children are again
women) can be represented by the description
%\[
$\mathsf{Woman}\sqcap\forall \mathsf{child}.\mathsf{Woman}$,
%\]
and the concept of all \emph{mothers} by the description
%\[
$\mathsf{Woman}\sqcap\exists \mathsf{child}.\mathsf{Human}$.
%\]  
In this example, we have used the constructors concept conjunction ($\sqcap$),
value restriction ($\forall R.C$), and existential restriction ($\exists R.C$).
In the DL literature, also various other constructors have 
been considered. A prominent example
are so-called number restrictions, which are available in almost all DL systems.
For example, using number restrictions the concept of all 
\emph{women having exactly two children}
can be represented by the concept description
\[
\mathsf{Woman}\sqcap({\leq}\,2\mathsf{child})\sqcap({\geq}\,2\mathsf{child}).
\]         
%
The knowledge base of a DL system consists of a \emph{terminological
  component} (TBox) and an \emph{assertional component} (ABox). In its
simplest form, the TBox consists of concept definitions, which assign names
(abbreviations) to complex descriptions.  More general TBox formalisms allow
for so-called \emph{general concept inclusion} axioms (GCIs) between complex
descriptions. For example, the concept inclusion
$$\mathsf{Human}\sqcap({\geq}\,3\mathsf{child})\sqsubseteq\exists \mathsf{entitled}.\mathsf{Taxbreak}$$
states that people having at least three children are entitled to a tax break.
The ABox formalism consists of concept assertions
(stating that an individual belongs to a concept) and role assertions (stating that 
two individuals are related by a role). For example, the assertions
$\mathsf{Woman}(\mathsf{MARY}), \mathsf{child}(\mathsf{MARY},\mathsf{TOM}),
\mathsf{Human}(\mathsf{TOM})$ state that Mary is a woman, who has a child, Tom, who
is a human.

DL systems
provide their users with various inference capabilities that allow them
to deduce implicit knowledge from the explicitly represented knowledge.
%For instance, the \emph{subsumption} algorithm allows one to determine
%subconcept-superconcept relationships: $C$ is subsumed by $D$
%($C\sqsubseteq D$) if, and only if, all instances of $C$ are also instances of $D$,
%i.e., the first description is always interpreted as a
%subset of the second description.
For instance, the \emph{subsumption} problem is concerned with
subconcept-superconcept relationships: $C$ is subsumed by $D$
($C\sqsubseteq D$) if, and only if, all instances of $C$ are also instances of $D$,
i.e., the first description is always interpreted as a
subset of the second description.
For example, the concept
description $\mathsf{Woman}$ obviously subsumes the concept description
$\mathsf{Woman}\sqcap\forall \mathsf{child}.\mathsf{Woman}$.
The concept description $C$ is \emph{satisfiable} iff it is non-contradictory,
i.e., it can be interpreted by a nonempty set.  
In DLs allowing for conjunction and negation of concepts, subsumption can be reduced
to (un)satisfiability: $C\sqsubseteq D$ iff $C\sqcap\neg D$ is unsatisfiable.
The \emph{instance} checking problem consists of deciding whether a given individual
is an instance of a given concept. For example, w.r.t.\ the assertions from
above, $\mathsf{MARY}$ is an instance of the concept description
$\mathsf{Woman}\sqcap\exists \mathsf{child}.\mathsf{Human}$.
The ABox $\mathcal{A}$ is \emph{consistent} iff it is non-contradictory,
i.e., it has a model.  
In DLs allowing for negation of concepts, the instance problem can be reduced
to (in)consistency of ABoxes: $i$ is an instance of $C$ w.r.t.\ the ABox
$\mathcal{A}$ iff $\mathcal{A}\cup\{\neg C(i)\}$ is inconsistent.

In order to ensure a reasonable and predictable
behavior of a DL system, reasoning in the DL employed
by the system should at least be decidable, and preferably of low
complexity. Consequently, the expressive power of the DL in question
must be restricted in an appropriate way. If the imposed restrictions
are too severe, however, then the important notions of the application
domain can no longer be expressed. Investigating this trade-off
between the expressivity of DLs and the complexity of their inference
problems has thus been one of the most important issues in DL research
(see, e.g., \citeR{LeBr87,Nebe88,Schm89,%
ScSm91,Nebe90,DLNN91b,DLNN97,% 
DHLM92,Scha93,DLNS94,%
DeLe94,DeLe94b,DeLe95b,CaDL99,Lutz99b,HoST00}).   

This paper investigates an approach for extending the expressivity of
DLs that (in many cases) guarantees that reasoning remains decidable: the fusion of DLs. 
In order to explain the difference between the usual union and the fusion
of DLs, let us consider a simple example. Assume that the DL $\mathcal{D}_1$
is $\mathcal{ALC}$, i.e., it provides for the Boolean operators $\sqcap$, $\sqcup$,
$\neg$ and the additional concept constructors value restriction $\forall R.C$
and existential restriction $\exists R.C$, and that the DL $\mathcal{D}_2$
provides for the Boolean operators and number restrictions $({\leq}\,nR)$ and
$({\geq}\,nR)$. If an application requires concept constructors from both
DLs for expressing its relevant concepts, then one would usually consider
the \emph{union} $\mathcal{D}_1\cup\mathcal{D}_2$ of 
$\mathcal{D}_1$ and $\mathcal{D}_2$, which allows for the unrestricted
use of all constructors. For example, the concept description
$C_1 := (\exists R.A)\sqcap(\exists R.\neg A)\sqcap({\leq}\,1R)$ is a legal
$\mathcal{D}_1\cup\mathcal{D}_2$ description. Note that this description is
unsatisfiable, due to the interaction between constructors of $\mathcal{D}_1$ 
and $\mathcal{D}_2$. The \emph{fusion} $\mathcal{D}_1\otimes\mathcal{D}_2$ of 
$\mathcal{D}_1$ and $\mathcal{D}_2$ prevents such interactions by imposing the
following restriction: one assumes that the set of all role names is partitioned
into two sets, one that can be used in constructors of $\mathcal{D}_1$, and
another one that can be used in constructors of $\mathcal{D}_2$. Thus, the
description $C_1$ from above is not a legal $\mathcal{D}_1\otimes\mathcal{D}_2$
description since it uses the same role $R$ both in the existential restrictions
(which are $\mathcal{D}_1$-constructors) and in the number restriction
(which is a $\mathcal{D}_2$-constructor). In contrast, the descriptions
$(\exists R_1.A)\sqcap(\exists R_1.\neg A)\sqcap({\leq}\,1R_2)$ and
$(\exists R_1.({\leq}\,1R_2))$ are admissible in $\mathcal{D}_1\otimes\mathcal{D}_2$
since they employ different roles in the $\mathcal{D}_1$- and $\mathcal{D}_2$-constructors.
If the concepts that must be expressed are such that they require both
constructors from $\mathcal{D}_1$ and $\mathcal{D}_2$, but the ones from  $\mathcal{D}_1$
for other roles than the ones from $\mathcal{D}_2$, then one does not really
need the union of $\mathcal{D}_1$ and $\mathcal{D}_2$; the fusion would be sufficient.

What is the advantage of taking the fusion instead of the union? 
Basically, for the union of two DLs one must design new reasoning methods, whereas
reasoning in the fusion can be reduced to reasoning in the component DLs.
Indeed, reasoning in the union may even be undecidable whereas reasoning in the fusion
is still decidable. As an example, we consider the DLs
%
(i)  $\mathcal{ALCF}$, which extends the basic
     DL $\mathcal{ALC}$ by functional roles (features) and the same-as
     constructor (agreement) on chains of functional roles \cite{HoNu90,BBNNS93}; and 
%
(ii) $\mathcal{ALC}^{{+},{\circ},{\sqcup}}$, which extends $\mathcal{ALC}$
     by transitive closure, composition, and union of roles \cite{Baad91,Schi91}. 
%
For both DLs, subsumption of concept descriptions is known to be decidable
\cite{HoNu90,Schi91,Baad91}. However, their \emph{union}
$\mathcal{ALCF}^{{+},{\circ},{\sqcup}}$ has an undecidable subsumption problem
\cite{BBNNS93}. This undecidability result
depends on the fact that, in $\mathcal{ALCF}^{{+},{\circ},{\sqcup}}$,
the role constructors transitive closure, composition, and union
can be applied to functional roles that also appear within the same-as constructor.
This is not allowed in the fusion $\mathcal{ALCF}\otimes\mathcal{ALC}^{{+},{\circ},{\sqcup}}$.
Of course, failure of a certain undecidability proof does not make the fusion
decidable.

Why do we know that the fusion of decidable DLs is again decidable?  Actually,
in general we don't, and this was our main reason for writing this paper.  The
notion ``fusion'' was introduced and investigated in modal logic, basically to
transfer results like finite axiomatizability, decidability, finite model
property, etc.\ from uni-modal logics (with one pair of box and diamond
operators) to multi-modal logics (with several such pairs, possibly satisfying
different axioms). This has led to rather general transfer results (see, e.g.,
\citeR{Wolt98,KrWo91,FiSc96,Spaa93,Gabb99} for results that concern
decidability), which are sometimes restricted to so-called \emph{normal} modal
logics \cite{Che80}.  Since there is a close relationship between modal logics
and DLs \cite{Schi91}, it is clear that these transfer results also apply to
some DLs.  The question is, however, to which DLs exactly and to which
inference problems. First, some DLs allow for constructors that are not
considered in modal logics (e.g., the same-as constructor mentioned above).
Second, some DL constructors that have been considered in modal logics, such
as qualified number restrictions $({\leq}\,nR.C)$, $({\geq}\,nR.C)$
\cite{HoBa91}, which correspond to graded modalities \cite{HoRi95}, can
easily be shown to be non-normal.  Third, the transfer results for
decidability are concerned with the satisfiability problem (with or without
general inclusion axioms). ABoxes and the related inference problems are not
considered. ABoxes can be simulated in modal logics allowing for so-called
nominals, i.e., names for individuals, within formulae
\cite{Prio67,GaGo93,Areces-et-al-00}.  However, as we will see below, the
general transfer results do not apply to modal logics with nominals.

The purpose of this paper is to clarify for which DLs decidability of the
component DLs transfers to their fusion. To this purpose, we introduce
so-called \emph{abstract description systems} (ADSs), which can be seen as a
common generalization of description and modal logics.  We define the fusion
of ADSs, and state four theorems that say under which conditions decidability
transfers from the component ADSs to their fusion. Two of these theorems are
concerned with inference w.r.t.\ general concept inclusion axioms and two with
inference without TBox axioms. In both cases, we first formulate and prove the
results for the consistency problem of ABoxes (more precisely, the
corresponding problem for ADSs) and then establish analogous results for the
satisfiability problem of concepts.

From the DL point of view, the four theorems shown in this paper
are concerned with the following four \emph{decision problems}: 
\begin{itemize}
\item[(i)] decidability of consistency of ABoxes w.r.t.\ TBox axioms
      (Theorem~\ref{transfer}); 
\item[(ii)] decidability of satisfiability of concepts w.r.t.\ TBox axioms;
      (Corollary~\ref{transfer:term}); 

\item[(iii)] decidability of consistency of ABoxes without TBox axioms
      (Theorem~\ref{transfer2}); and
\item[(iv)] decidability of satisfiability of concepts without TBox axioms
      (Corollary~\ref{transfer2:term}).
\end{itemize}
These theorems imply that decidability of the consistency problem and the
satisfiability problem transfers to the fusion for most DLs considered in the
literature.  The \emph{main exceptions} (which do not satisfy the
prerequisites of the theorems) are
\begin{itemize}
\item[(a)] DLs that are not propositionally closed, i.e., do not contain all Boolean connectives;
\item[(b)] DLs allowing for individuals (called nominals in modal logic) in concept descriptions; and 
\item[(c)] DLs explicitly allowing for the universal role or for negation of roles.
\end{itemize} 
Results from modal logic for problem (iv) usually require the
component modal logics to be normal. Our Theorem~\ref{transfer2} is less restrictive,
and thus also applies to DLs allowing for constructors like qualified number restrictions.



\section{Description logics}
\label{sect:DLs}

Before defining abstract description systems in the next section, we introduce the main 
features of DLs that must be covered by this definition. To this purpose, we 
first introduce \ALC, the basic DL containing
all Boolean connectives, and the relevant inference problems. Then, we 
consider different possibilities for extending \ALC to more expressive DLs.
%
\begin{definition}[\ALC Syntax]
  \label{def:syntax}
  Let $N_C$, $N_R$, and $N_I$ be countable and pairwise disjoint sets of
  concept, role, and individual names, respectively.  The set of \ALC concept
  descriptions is the smallest set such that
  %
  \begin{enumerate}
  \item every concept name is a concept description, 
  \item if $C$ and $D$ are concept descriptions and $R$ is a role name, then the following
    expressions are also concept descriptions:
  %
  \begin{itemize}
  \item $\neg C$ (negation), $C \sqcap D$ (conjunction), $C \sqcup D$
    (disjunction),
  \item $\exists R . C$ (existential restriction), and $\forall R .C$
    (value restriction).
  \end{itemize}
  \end{enumerate}
  %
  We use $\top$ as an abbreviation of $A \sqcup \neg A$ and
  $\bot$ as an abbreviation for $A \sqcap \neg A$ (where $A$ is an 
  arbitrary concept name). 

  Let $C$ and $D$ be concept descriptions. Then $C \sqsubseteq D$ is a \defn{general
  concept inclusion axiom} (GCI). A finite set of such axioms is called a
  \defn{TBox}. 

  Let $C$ be a concept description, $R$ a role name, and $i, j$ individual names. 
  Then $C(i)$ is a \emph{concept assertion} and $R(i,j)$ a \emph{role assertion}.
  A finite set of such assertions is called an ABox.
\end{definition}

The meaning of \ALC-concept descriptions, TBoxes, and ABoxes can be defined
with the help of a set-theoretic semantics.

\begin{definition}[\ALC Semantics]
  \label{def:semantics}
  An \ALC-\defn{interpretation} $\mathcal{I}$ is a pair $(\Delta^\Imc,
  \cdot^\Imc)$, where $\Delta^\Imc$ is a nonempty set, the \defn{domain} of
  the interpretation, and $\cdot^\Imc$ is 
  the \defn{interpretation function}. The interpretation function maps
  %
  \begin{itemize}
    \item each concept name $A$ to a subset $A^\Imc$ of $\Delta^\Imc$, 
    \item each role name $R$ to a subset $R^\Imc$ of $\Delta^\Imc \times
          \Delta^\Imc$,
    \item each individual name $i$ to an element $i^\Imc$ of $\Delta^\Imc$
          such that different names are mapped to different elements
          (unique name assumption).
  \end{itemize}
  %
  For a role name $R$ and an element $a\in \Delta^\Imc$ we define
  $R^\Imc(a) := \{ b \mid (a,b) \in R^\Imc\}$.
  The interpretation function can inductively be extended to complex 
  concepts as follows:
  %
  \begin{gather*}
    \begin{split}
      (\neg C)^\Imc &:= \Delta^\Imc \setminus C^\Imc \\
      (C \sqcap D)^\Imc &:= C^\Imc \cap D^\Imc \\
      (C \sqcup D)^\Imc &:= C^\Imc \cup D^\Imc \\
      (\exists R.C)^\Imc &:= \{ a \in \Delta^\Imc \mid R^\Imc(a) \cap C^\Imc \neq \emptyset\} \\
      (\forall R.C)^\Imc &:= \{ a \in \Delta^\Imc \mid R^\Imc(a) \subseteq C^\Imc\}
    \end{split}
  \end{gather*}
  %
  An interpretation \Imc is a \defn{model of the TBox} \Tmc iff it satisfies
  $C^\Imc \subseteq D^\Imc$ for all GCIs $C \sqsubseteq D$ in \Tmc. 
  It is a \defn{model of the ABox} \Amc iff it satisfies $i^\Imc\in C^\Imc$
  for all concept assertions $C(i)\in \Amc$ and $(i^\Imc,j^\Imc)\in R^\Imc$
  for all role assertions $R(i,j)\in \Amc$.
  Finally, \Imc is a \defn{model of an ABox relative to a TBox} iff it is
  a model of both the ABox and the TBox.
  %An
  %interpretation \Imc is a \defn{model of a concept $C$} iff it satisfies
  %$C^\Imc \neq \emptyset$. 
  %An interpretation \Imc is a \defn{model of a
  %  concept $C$ w.r.t.\ a TBox \Tmc} iff it is a model of both $C$ and \Tmc.
\end{definition}


Given this semantics, we can now formally define the relevant inference
problems.

\begin{definition}[Inferences]
\label{DL:inf:def}
  Let $C$ and $D$ be concept descriptions, $i$ an individual name,
  \Tmc a TBox, and \Amc an ABox.
  We say that $C$ \defn{subsumes} $D$ \defn{relative to the TBox~\Tmc{}}
  ($D \sqsubseteq_\Tmc C$) iff 
  $D^\Imc \subseteq C^\Imc$ for all models \Imc of \Tmc.
%
  The concept description $C$ is \defn{satisfiable relative to the TBox \Tmc{}}
  iff there exists a model \Imc of \Tmc such that $C^\Imc\neq\emptyset$.
%
  The individual $i$ is an \defn{instance} of $C$ in the ABox \Amc \defn{relative to the TBox \Tmc{}}
  iff $i^\Imc\in C^\Imc$ for all models of \Amc relative to \Tmc.
%
  The ABox \Amc is \defn{consistent relative to the TBox \Tmc{}} iff there exists
  a model of \Amc relative to \Tmc.

  These three inferences can also be considered without reference to a TBox:
  $C$ \defn{subsumes} $D$ ($C$ is satisfiable) iff $C$ subsumes $D$ ($C$ is satisfiable)
  relative to the empty TBox, and 
  $i$ is an \defn{instance} of $C$ in \Amc (\Amc is \defn{consistent}) iff
  $i$ is an instance of $C$ in \Amc (\Amc is consistent) relative to the empty TBox.
\end{definition}
%
%Note that it would be more precise to speak of subsumption \defn{in a
%  description logic $L$} since there may obviously be concepts $C, D$ and
%description logics $L_1, L_2$ such that $C \sqsubseteq D$ in $L_1$ but $C
%\not\sqsubseteq D$ in $L_2$. However, since the description logic considered
%is usually clear from the context, we do not mention it explicitly when
%talking about subsumption.

%As mentioned in the introduction, 
We restrict our attention to DLs that are propositionally closed (i.e., allow
for the Boolean operators conjunction, disjunction, and negation).
Consequently, subsumption can be reduced to (un)satisfiability since $C
\sqsubseteq_\Tmc D$ iff $C\sqcap\neg D$ is unsatisfiable relative to \Tmc.
Conversely, (un)\-satis\-fi\-ability can be reduced to subsumption since $C$
is unsatisfiable relative to \Tmc iff $C \sqsubseteq_\Tmc \bot$. For this
reason, it is irrelevant whether we consider the subsumption or the
satisfiability problem in our results concerning the transfer of decidability
of these problems from component DLs to their fusion (informally called
\emph{transfer results} in the following).

Similarly, the instance problem can be reduced to the (in)consistency problem and vice versa:
$i$ is an instance of $C$ in \Amc relative to \Tmc iff $\Amc \cup\{\neg
C(i)\}$ is inconsistent relative to \Tmc;
and \Amc is inconsistent relative to \Tmc iff $i$ is an instance of $\bot$ in \Amc relative to \Tmc,
where $i$ is an arbitrary individual name. Consequently, it is irrelevant whether we consider the 
instance problem or the consistency problem in our transfer results.

Finally, the satisfiability problem can be reduced to the consistency problem:
$C$ is satisfiable relative to \Tmc iff the ABox $\{ C(i)\}$ is consistent relative to \Tmc,
where $i$ is an arbitrary individual name. However, the converse need not be
true.  It should be obvious that this implies that a transfer result for the
satisfiability problem does not yield the corresponding transfer result for
the consistency problem: from decidability of the consistency problem for the
component DLs we can only deduce decidability of the satisfiability problem in
their fusion.  What might be less obvious is that a transfer result for the
consistency problem need not imply the corresponding transfer result for the
satisfiability problem: if the satisfiability problems in the component DLs
are decidable, then the transfer result for the consistency problem can just
not be applied (since the %component DLs need not satisfy the stronger
prerequisite of this transfer result, namely, decidability of the \emph{consistency}
problem in the component DLs, need not be satisfied). 
However, we will show that the method used to show the transfer
result for the consistency problem also applies to the satisfiability problem.


\subsection{More expressive DLs}

There are several possibilities for extending \ALC in order to obtain a more
expressive DL. The three most prominent are adding additional
concept constructors, adding role constructors, and formulating restrictions on
role interpretations. In addition to giving examples for such extensions, we
also introduce a naming scheme for the obtained DLs. Additional concept constructors
are indicated by appending caligraphic letters to the language name, role constructors
by symbols in superscript, and restrictions on roles by letters in subscript.

We start with introducing restrictions on role interpretations, since we 
need to refer to such restrictions when defining certain concept constructors.


\subsubsection{Restrictions on role interpretations}

These restrictions enforce the interpretations of roles to satisfy
certain properties, such as functionality, transitivity, etc. We
consider three prominent examples:
%
\begin{enumerate}
%
\item {\bf Functional roles.}
  Here one considers a subset $N_F$ of the set of role names $N_R$,
  whose elements are called \defn{features}. An interpretation
  must map features $f\in N_F$ to functional binary
  relations $f^\Imc\subseteq\Delta^\Imc \times \Delta^\Imc$, i.e.,
  relations satisfying $\forall a,b,c. f^\Imc(a,b)\wedge f^\Imc(a,c)\rightarrow b=c$.
  We will sometimes treat functional relations as partial functions,
  and write $f^\Imc(a) = b$ rather than $f^\Imc(a,b)$.
  $\ALC$ extended with features is denoted by $\ALC_f$.
%
\item {\bf Transitive roles.}
  Here one considers a subset $N_{R^+}$ of $N_R$. Role names $R \in
  N_{R^+}$ are called \defn{transitive roles}.  
  An interpretation must map transitive roles $R \in N_{R^+}$ to transitive binary
  relations $R^\Imc\subseteq\Delta^\Imc \times \Delta^\Imc$.
  \ALC extended with transitive roles is
  denoted by $\mathcal{ALC}_{R^+}$. 
%
\item {\bf Role hierarchies.} A \defn{role inclusion axiom} is an expression of the
  form $R \sqsubseteq S$ with $R,S \in N_R$. A finite set $H$ of role inclusion
  axioms is called a \defn{role hierarchy}. 
  An  interpretation must satisfy $R^\Imc \subseteq S^\Imc$ for all $R \sqsubseteq S \in H$. 
  \ALC extended with a role hierarchy $H$ is
  denoted by $\ALC_{\mathcal{H}(H)}$.  If $H$ is clear from the context or
  irrelevant, we write $\ALCH$ instead of
  $\ALC_{\mathcal{H}(H)}$.
%
\end{enumerate}
%
The above restrictions can also be combined with each other.
For example, $\ALC_{\mathcal{H} \! R^+}$ is \ALC with a
role hierarchy and transitive roles. 

Transitive roles in DLs were first investigated by \citeA{Satt96}.
Features were introduced in DLs by \citeA{HoNu90} and (under the name ``attributes'')
in the CLASSIC system \cite{BMPAB91}, in both cases in conjunction with feature
agreements and disagreements (see concept constructors below). Features without 
agreements and disagreements are, e.g., used in the DL $\mathcal{SHIF}$ \cite{HoSa99},
albeit in a more expressive ``local'' way, where functionality can be asserted
to hold at certain individuals, but not necessarily on the whole model. According to
our naming scheme, we indicate the presence of features in a DL by the letter
$f$ in subscript.\footnote{%
Note that some authors (e.g., \citeR{HoSa99}) use an appended $\mathcal{F}$ to
denote local features. Following \citeA{HoNu90}, we will use $\mathcal{F}$ to denote
a DL that allows for feature agreements (see below).
}

A remark on role hierarchies is also in order: in our definition, if $H_1$ and $H_2$ are
different role hierarchies, then $\ALC_{\mathcal{H}(H_1)}$ and
$\ALC_{\mathcal{H}(H_2)}$ are different DLs. In the DL
literature, usually only one logic $\ALCH$ is defined and role hierarchies are
treated like TBoxes, i.e., satisfiability and subsumption are defined relative to
TBoxes \defn{and} role hierarchies (see, e.g., \citeR{Horr98}). For our
purposes, however, it is more convenient to define one DL per
role hierarchy since distinct role hierarchies impose distinct restrictions on
the interpretation of roles. The advantages of this approach will become clear
later on when frames and abstract description systems are introduced.


%
\begin{figure}
%  \begin{center}
  \small
\hspace*{\fill}
\renewcommand{\arraystretch}{1.2}
    \begin{tabular}{|l|l|l|c|}
      \hline
      Name & Syntax & Semantics & Symbol \\
      \hline
      Unqualified & ${\geq} n R$ & $\{ a \in \Delta^\Imc \mid 
      | R^\Imc(a) | \geq n \}$ & 
      $\mathcal{N}$
      \\
      number restrictions & ${\leq} n R$ & $\{ a \in \Delta^\Imc \mid 
      | R^\Imc(a) | \leq n \}$ & 
      \\
      \hline
      Qualified & ${\geq} n R . C$ & $\{ a \in \Delta^\Imc \mid 
      | R^\Imc(a) \cap C^\Imc| \geq n \}$ & 
      $\mathcal{Q}$
      \\
      number restrictions & ${\leq} n R . C$ & $\{ a \in \Delta^\Imc \mid 
      | R^\Imc(a) \cap C^\Imc| \leq n \}$ & 
      \\
      \hline
      Nominals & $I$ & $I^\Imc \subseteq \Delta^\Imc \text{ with } |I^\Imc| = 1$ & $\mathcal{O}$
      \\
     \hline
      Feature agreement & $u_1 {\downarrow} u_2$ & $\{ a \in \Delta^\Imc \mid
       \exists b \in \Delta^\Imc.\ u_1^\Imc(a) = b = u_2^\Imc(a) \}$& 
      \\
      and disagreement & $u_1 {\uparrow} u_2$ & $\{ a \in \Delta^\Imc \mid
       \exists b_1,b_2 \in \Delta^\Imc .$ & $\mathcal{F}$ \\
       && \hspace*{2cm} $u_1^\Imc(a) = b_1 \neq b_2 =
       u_2^\Imc(b_1) \}$& 
      \\
      \hline
    \end{tabular}
\renewcommand{\arraystretch}{1}
\hspace*{\fill}
%  \end{center}
  %
  \caption{Some description logic concept constructors.}
  \label{fig:constructors}
\end{figure}
%


\subsubsection{Concept constructors}

Concept constructors take concept and/or role descriptions and transform them
into more complex concept descriptions. In addition to the constructors
available in \ALC, various other concept constructors are considered in the DL
literature.  A small collection of such constructors can be found in
Figure~\ref{fig:constructors}, where $|S|$ denotes the cardinality of a set
$S$.  The symbols in the rightmost column indicate the naming scheme for the
resulting DL. %In contrast to the case of restrictions on role interpretations,
As mentioned above
the name modifiers for concept constructors are not written in subscript,
they are appended to the language name. For
example, $\ALC_{\mathcal{H} \! R^+}$ extended with qualified number
restrictions is called $\mathcal{ALCQ}_{\mathcal{H} \!  R^+}$. The syntax of
the extended DLs is as expected, i.e., the constructors may be arbitrarily
combined. The semantics is obtained by augmenting the semantics of \ALC with
the appropriate conditions, which can be found in the third column in
Figure~\ref{fig:constructors}.  Nominals and feature (dis)agreements need some
more explanation:
%
\begin{itemize}
\item {\bf Nominals.} We consider a set $N_O$ of (names for) \defn{nominals},
  which is pairwise disjoint to the sets $N_C$, $N_R$, and $N_I$.
  Elements from $N_O$ are often denoted by $I$ (possibly with index). 
  An interpretation must map nominals to singleton subsets of $\Delta^\Imc$.
  %From an intensional point of view, 
  The intention underlying nominals is that they stand for elements of $\Delta$,
  just like individual names. However, since we want to use the nominal $I\in N_O$
  as a (nullary) concept constructor, $\Imc$ must interpret them by a set,
  namely the singleton set consisting of the individual that $I$ denotes.
\item {\bf Feature (dis)agreements.} \ALCF is the extension of $\ALC_f$ with
  feature agreements and disagreements. Beside the additional concept constructors, \ALCF
  uses 
  %features and 
  feature chains as part of the (dis)agreement constructor. 
  A \defn{feature chain} is an
  expression of the form $u = f_1 \circ \cdots \circ f_n$. The interpretation
  $u^\Imc$ of such a feature chain is just the composition of the partial
  functions $f_1^\Imc, \dots, f_n^\Imc$, where composition is to be read
  from left to right.
\end{itemize}
%
DLs including nominals or feature (dis)agreements and additional
concept constructors or restrictions on role interpretations are defined 
(and named) in the obvious way.

Number restriction are available in almost all DL systems. The DL \ALCN (i.e.,
\ALC{} extended with number restrictions) was first treated by \citeA{HoNu90},
as was \ALCF. The DL \ALCQ was first investigated by \citeA{HoBa91}, and
\ALCO by \citeA{Scha94}.


\subsubsection{Role constructors}

Role constructors allow us to build complex role
descriptions. A collection of role constructors can be found in
Figure~\ref{fig:rconstr}. Again, the rightmost column indicates the naming
scheme, where name modifiers for role constructors are written in superscript
and separated by commas.  For example, $\mathcal{ALCQ}$ with inverse roles and
transitive closure is called $\mathcal{ALCQ}^{+,{-1}}$.  In DLs
admitting role constructors, the set of role descriptions is defined inductively,
analogously to the set of concept descriptions. The semantics of role constructors
is given in the third column of Figure~\ref{fig:rconstr}. As with concept descriptions,
it can be used to extend the interpretation function from role names to 
role descriptions.
%We exemplarily do this for
%$\mathcal{ALC}^{\overline{\cdot},\sqcap,\sqcup}$, i.e., \ALC with role
%complement, conjunction and disjunction.
%
%\begin{definition}[$\mathcal{ALC}^{\overline{\cdot},\sqcap,\sqcup}$ roles]
%  The set of $\mathcal{ALC}^{\overline{\cdot},\sqcap,\sqcup}$ roles
%  is defined inductively as follows:
%  %
%  \begin{enumerate}
%  \item every role name is a role and
%  \item if $R_1$ and $R_2$ are roles, then the following expressions are also
%    roles: \\ $\overline{R_1}$, $R_1 \sqcap R_2$, and $R_1 \sqcup R_2$.
%  \end{enumerate}
%\end{definition}

In a DL with role constructors, role descriptions can be used wherever role names may be
used in the corresponding DLs without role constructors. For example,
$$\exists (R_1\sqcap R_3) . C \sqcap \forall (R_2 \sqcup \overline{R}_2) . \neg C$$ 
is an $\mathcal{ALC}^{\overline{\cdot},\sqcap,\sqcup}$-concept description.
This concept description is unsatisfiable since $R_2 \sqcup \overline{R}_2$ is
equivalent to the universal role.
Note that role descriptions can also be used within role assertions in an ABox.
%The semantics of 
%complex roles is defined inductively. We exemplarily define the semantics
%of complex $\mathcal{ALC}^{\overline{\cdot},\sqcap,\sqcup}$ roles.
%%
%\begin{definition}[$\mathcal{ALC}^{\overline{\cdot},\sqcap,\sqcup}$ role
%semantics]
%\end{definition}
%%
%The semantics of role constructors can be read off from the third column
%of Figure~\ref{fig:rconstr}.
%
\begin{figure}
%  \begin{center}
   \small
\hspace*{\fill}
\renewcommand{\arraystretch}{1.2}
    \begin{tabular}{|l|l|l|c|}
      \hline
      Name & Syntax & Semantics & Symbol \\
      \hline
      Role composition & $R_1 \circ R_2$ & $\{ (a,b) \in \Delta^\Imc \times 
      \Delta^\Imc \mid$ & $\circ$ \\
      && \hspace*{1cm} $\exists c \in \Delta^\Imc.\ (a,c) \in R_1^\Imc 
      \wedge (c,b) \in R_2^\Imc \}$ & 
      \\
\hline
      Role complement & $\overline{R}$ & $\{ (a,b) \in \Delta^\Imc \times 
      \Delta^\Imc \mid (a,b) \notin R^\Imc \}$ & 
      $\overline{\cdot}$
      \\
\hline
      Role conjunction & $R_1 \sqcap R_2$ & $\{ (a,b) \in \Delta^\Imc \times 
      \Delta^\Imc \mid (a,b) \in R_1^\Imc \wedge (a,b) \in R_2^\Imc \}$ & 
      $\sqcap$
      \\
\hline
      Role disjunction & $R_1 \sqcup R_2$ & $\{ (a,b) \in \Delta^\Imc \times 
      \Delta^\Imc \mid (a,b) \in R_1^\Imc \vee (a,b) \in R_2^\Imc \}$ & 
      $\sqcup$
      \\
\hline
      Inverse roles & $R^{-1}$ & $\{ (a,b) \in \Delta^\Imc \times 
      \Delta^\Imc \mid (b,a) \in R^\Imc \}$ & 
      $-1$
      \\
\hline
      Transitive closure & $R^+$ & $\{ (a,b) \in \Delta^\Imc \times 
      \Delta^\Imc \mid (a,b) \in (R^\Imc)^+ \}$ & 
      $+$
      \\
\hline
      Universal role & $U$ & $\Delta^\Imc \times 
      \Delta^\Imc$ & $U$
      \\
      \hline
    \end{tabular}
\renewcommand{\arraystretch}{1}
\hspace*{\fill}\\
\hspace*{\fill}
    For a binary relation $R$, $R^+$ denotes the transitive closure of $R$.
\hspace*{\fill}
%  \end{center}
  %
  \caption{Some description logic role constructors.} 
  \label{fig:rconstr}
\end{figure}
%

The DL $\ALC^{{\circ},{\sqcup},{+}}$ was first treated by \citeA{Baad91}
(under the name $\ALC_{trans}$);
\citeA{Schi91} has shown that this DL is a notational variant of
propositional dynamic logic (PDL). DLs with Boolean operators on roles
were investigated by \citeA{LuSa00}. The inverse operator was available in
the system CRACK \cite{BrFT95}, and reasoning in DLs with inverse roles was, for example,
investigated by Calvanese et al.\ \citeyear{CaDR98} and \citeA{HoST00}.
The universal role can be expressed
using DLs with Boolean operators on roles (see the above example), and it
can in turn be used to simulate general concept inclusion axioms within
concept descriptions.
 

\subsection{Restricting the syntax}

\enlargethispage*{-2mm}
Until now, constructors could be combined arbitrarily.
Sometimes it makes sense to restrict the interaction
between constructors since reasoning in the restricted  DL
may be easier than reasoning in the unrestricted DL.
We will consider DLs imposing certain restrictions on
%
\begin{enumerate}
\item which roles may be used inside certain concept constructors,
\item which roles may be used inside certain role constructors,
\item the combination of role constructors, and
\item the role constructors that may be used inside certain concept
  constructors.
\end{enumerate}
%
As an example for the first case, consider the fragment of
$\mathcal{ALCQ}_{R^+}$ in which transitive roles may be used in existential
and universal restrictions, but not in number restrictions (see, e.g.,
\citeR{HoST00}). 

As the result of taking the fusion of two DLs, we will obtain DLs
whose set of roles $N_R$ is partitioned. For example, the fusion of \ALCQ with
$\ALC^{-1}$ yields a fragment of $\ALCQ^{-1}$ where $N_R$ is partitioned in two sets,
say $N_{R_1}$ and $N_{R_2}$. In this fragment,
the inverse role constructor and roles from $N_{R_2}$ may not be used
within qualified number restrictions, while
roles from $N_{R_1}$ may not be used inside the inverse role constructor.%
\footnote{This will become clearer once we have given a formal definition of the
fusion.}
%
Thus, this DL is an example for the first, the second, and the fourth
case.

Now consider the DL \ALCF introduced above, which does not only extend
$\ALC_f$ with feature (dis)agreement as a concept constructor, but also
provides the role composition constructor. However, the role chains built
using composition have to be comprised exclusively of features and
non-functional roles may not appear inside feature (dis)agreement. Hence,
\ALCF is also an example for the first, second, and fourth case.

As an example for the third case, the fragment of
$\mathcal{ALC}^{\overline{\cdot},\sqcap}$ in which role conjunction may not be used inside
the role complement constructor is considered by \citeA{LuSa00}. 

%Regarding the fourth case, consider the fragment
%of $\mathcal{ALCQ}^+$ where the transitive closure constructor must not be
%used inside qualified number restrictions. 

For these restricted DLs, we
do not introduce an explicit naming scheme.  Note that, in this paper, we do \emph{not}
deal with DLs in which the combinability of concept constructors with
each other is restricted since these DLs would not fit into the
framework of abstract description systems introduced
in the next section. An example of such a DL would be one with atomic negation
of concepts, i.e., where negation may only be applied to concept names (e.g.,
the DL \AL discussed by 
\citeR{DLNN97}).




\section{Abstract description systems}
\label{sect:ads}

%In this section, we introduce abstract description systems (ADSs) and show
%that, for every description logic introduced in Section~\ref{sect:DLs}, there
%exists a corresponding abstract description system. Here, ``corresponding''
%means that every DL concept $C$ can be translated into a term $t_C$ of the
%corresponding ADS and that subsumption of two DL concepts $C$ and $D$ can then
%be decided by deciding subsumption of the terms $t_C$ and $t_D$. 
%
%\subsection{Abstract Description Systems}
%\label{sect:ads2}

In order to define the fusion of DLs and prove general results for fusions
of DLs, one needs a formal definition of what are ``description logics''.
Since there exists a wide variety of DLs with very different characteristics, we
introduce a very general formalization, which should cover all of the DLs considered
in the literature, but also includes logics that would usually not be
subsumed under the name DL.

\subsection{Syntax and semantics}

The \emph{syntax} of an abstract description system is given by its
\emph{abstract description language}, which determines a set of terms, term
assertions, and object assertions.
%
In this setting, concept descriptions are represented by terms that are 
built using the abstract description language. General inclusion axioms in DLs
are represented by term assertions and ABox assertions in DLs 
are represented by object assertions.        
%
\begin{definition}[Abstract description language]
\label{ADL:def}
  An \emph{abstract description language} (ADL) is determined by a countably
  infinite set $V$ of set variables,  a countably infinite set ${\cal X}$ of 
  object variables, a (possibly infinite) countable set $\Rmc$
  of relation symbols of arity two,\footnote{%
To keep things simpler, we restrict our attention to the case of binary predicates,
i.e., roles in DL. However, the results can easily be extended to $n$-ary predicates.} 
  and a (possibly infinite) countable set
  $\Fmc$ of functions symbols $f$, which are equipped with arities
   $n_f$. All these sets have to be pairwise disjoint.

  The \emph{terms} $t_j$ of this ADL are built using the
  follow syntax rules:
$$
t_j \ \ 
         \longrightarrow \ \ x,\
                         \neg t_{1},\ t_{1}\wedge t_{2},\ t_{1}\vee t_{2},\
                         f(t_{1},\ldots,t_{n_f}),
$$
where $x\in V$, $f\in \Fmc$, and the Boolean operators 
$\neg, \wedge, \vee$ are different from all function symbols in $\Fmc$.
For a term $t$, we denote by 
$\mn{var}(t)$ the set of set variables used in 
$t$.
The symbol $\top$ is used as an 
abbreviation of $x \vee \neg x$ and $\bot$
as an abbreviation for $x \wedge \neg x$ (where $x$ is a set variable).

The \emph{term assertions} of this ADL are
\begin{itemize}
\item $t_{1} \sqsubseteq t_{2}$, for all terms $t_{1},t_{2}$,
\end{itemize}               
%
and the \emph{object assertions} are
\begin{itemize}
\item $R(a,b)$, for $a,b\in {\cal X}$ and $R \in {\cal R}$;
\item $(a:t)$, for $a \in {\cal X}$ and $t$ a term.
\end{itemize}
The sets of term and object assertions together form
the set of \emph{assertions} of the ADL. 
%
\end{definition}
%
From the DL point of view, the set variables correspond to concept names,
object variables to individual names, relation symbols to roles, and the
Boolean operators as well as the function symbols correspond to concept
constructors. Thus, terms correspond to concept descriptions.  As an example,
let us view concept descriptions of the DL $\mathcal{ALCN}^\sqcap$, i.e., \ALC
extended with number restrictions and conjunction of roles, as terms of an
ADL. Value restrictions and existential restrictions can be seen as unary
function symbols: for each role description $R$, we have the function symbols
$f_{\forall R}$ and $f_{\exists R}$, which take a term $t_C$ (corresponding to
the concept description $C$) and transform it into the more complex terms
$f_{\forall R}(t_C)$ and $f_{\exists R}(t_C)$ (corresponding to the concept
descriptions $\forall R.C$ and $\exists R.C$).  Similarly, number restrictions
can be seen as nullary function symbols: for each role description $R$ and
each $n \in \mathbb{N}$, we have the function symbols $f_{\geq n R}$ and
$f_{\leq n R}$. Hence, the $\mathcal{ALCN}^\sqcap$-concept description $A
\sqcap \forall (R_1 \sqcap R_2) . \neg (B \sqcap (\geq 2 R_1))$
%, with $A$ and $B$ concept names and $r_1$ and $r_2$ role names,
corresponds to the term $x_A \wedge f_{\forall (R_1 \sqcap R_2)}(\neg (x_B
\wedge f_{(\geq 2 R_1)}))$.  
%
We will analyze the connection between ADLs
and DLs more formally later on.


The \emph{semantics} of abstract description systems is defined based on
\emph{abstract description models}. These models are the general semantic
structures in which the terms of the ADL are interpreted. It should already
be noted here, however, that an abstract description system usually does not
take into account all abstract description models available for the language: 
it allows only for a \emph{selected subclass} of these models. This subclass
determines the semantics of the system.
%
\begin{definition}
  Let $L$ be an ADL as in Definition~\ref{ADL:def}.
  An \emph{abstract description model} (ADM) for $L$ is of the form $${\mathfrak W} =
  \auf W, \Fmc^{\mathfrak W} = \{f^{{\mathfrak W}}\mid f\in \Fmc\},
\Rmc^{\mathfrak W}= \{R^{{\mathfrak W}}\mid R\in {\cal R}\}\zu,
$$ 
where $W$ is
  a nonempty set, the $f^{{\mathfrak W}}$ are functions mapping every
  sequence $\auf X_{1},\ldots,X_{n_f}\zu$ of subsets of $W$ to a subset of
  $W$, and
  the $R^{{\mathfrak W}}$ are binary relations on $W$.

\end{definition}
%
Since ADMs do not interpret variables, we need an assignment that
assigns a subset of $W$ to each set variable, 
before we can evaluate terms in an
ADM. To evaluate object assertions, we need an additional assignment
that assigns an element of $W$ to each object variable.
%
\begin{definition}
  Let \Lmc be an ADL and $\Wmf=\auf W, \Fmc^\Wmf, \Rmc^\Wmf \zu$ be an ADM for \Lmc.  
  An
  \defn{assignment} for \Wmf is a pair $\Amc = ({\cal A}_{1},
  {\cal A}_{2})$ such that ${\cal A}_{1}$ is a mapping from the set of 
  set variables $V$ into $2^W$,
  and ${\cal A}_{2}$ is an injective%
\footnote{This corresponds to the unique name assumption.} 
  mapping from the set
  of object variables ${\cal X}$ into 
  $W$.
%  The value the assignment $\Amc$ assigns to a variable $x\in V$ is denoted
%  by $x^\Amc$ (or, sometimes, by $x^{{\cal A}_{1}}$). 
  Let \Wmf be an ADM and $\Amc = ({\cal A}_{1},{\cal A}_{2})$ be an assignment for \Wmf.  
  With each \Lmc-term $t$, we inductively associate a value $t^{\Wmf,\Amc}$ in
  $2^W$ as follows:
  %
%
\begin{itemize}
\item $x^{\Wmf,\Amc} := \Amc_1(x)$ for all variables $x\in V$,
\item $(\neg t)^{\Wmf,\Amc} := W \setminus (t)^{\Wmf,\Amc}$,
      $(t_1 \wedge t_2)^{\Wmf,\Amc} := t_1^{\Wmf,\Amc} \cap t_2^{\Wmf,\Amc}$,
      $(t_1 \vee t_2)^{\Wmf,\Amc} := t_1^{\Wmf,\Amc} \cup t_2^{\Wmf,\Amc}$,
\item $f(t_1,\dots,t_{n_f})^{\Wmf,\Amc} := f^\Wmf(t_1^{\Wmf,\Amc},\dots,t_{n_f}^{\Wmf,\Amc})$.
\end{itemize}
%
If $x_1,\ldots, x_n$ are the set variables occurring in $t$, then we often
write  $t^\Wmf(X_1,\dots,X_n)$ as 
shorthand for $t^{\Wmf, \Amc}$, where $\Amc$ is an assignment with $x_i^\Amc =
X_i$ for $1 \leq i \leq n$.

The truth-relation $\models$ between $\auf {\mathfrak W},{\cal A}\zu$
and assertions is defined as follows:
\begin{itemize}
\item $\auf {\mathfrak W},{\cal A}\zu \models R(a,b)$ iff
${\cal A}_{2}(a) R^{\mathfrak W} {\cal A}_{2}(b)$,
\item $\auf {\mathfrak W},{\cal A}\zu \models a:t$ iff
${\cal A}_{2}(a)\in t^{{\mathfrak W},{\cal A}}$,
\item $\auf {\mathfrak W},{\cal A}\zu \models t_{1}\sqsubseteq t_{2}$
iff $t_{1}^{{\mathfrak W},{\cal A}}\subseteq t_{2}^{{\mathfrak W},{\cal A}}$. 
\end{itemize}
In this case we say that the assertion is satisfied in $\auf {\mathfrak
  W},{\cal A}\zu$. If, for an ADM \Wmf and a set of assertions $\Gamma$, there
exists an assignment \Amc for \Wmf such that each assertion in $\Gamma$ is
satisfied in $\auf {\mathfrak W},{\cal A}\zu$, then \Wmf is a \emph{model for
  $\Gamma$}.
\end{definition}

There are two differences between ADMs and DL interpretations.
First, in a DL interpretation, the
interpretation of the role names fixes the interpretation of the function
symbols corresponding to concept constructors that involve roles (like value
restrictions, number restrictions, etc.). The interpretation of the concept
names corresponds to an assignment. Thus, a DL model is an ADM together with
an assignment, whereas an ADM alone corresponds to what is called frame in
modal logics. 
%Since individuals in DLs correspond to nullary function symbols,
%their interpretation must also be fixed in the ADM.  We will call a non-empty
%domain together with an interpretation of the role names and (if any)
%individual names a \emph{DL frame}. We introduce abstract description systems
%before giving examples of ADMs.       
Second, in DL the roles used in concept constructors may, of course, also
occur in role assertions. In contrast, the definition of ADMs per se does not 
enforce any connection between the interpretation of the function symbols
and the interpretation of the relation symbols. Such connections can, however,
be enforced by restricting the attention to a subclass of all possible ADMs
for the ADL. 
%
\begin{definition}
An \emph{abstract description system} (ADS) is a pair $({\cal L},{\cal M})$,
where ${\cal L}$ is an ADL and ${\cal M}$ is a class of ADMs for ${\cal L}$
that is closed under isomorphic copies.\footnote{%
Intuitively, this means that, if an ADM ${\mathfrak W}$ belongs to ${\cal M}$, 
then all ADMs that differ from it only w.r.t.\ the names of the elements in its 
domain $W$ also belong to $\Mmc$.}
\end{definition}
%
From the DL point of view, the choice of the class ${\cal M}$ defines the
semantics of the concept and role constructors, and it allows us, e.g., to
incorporate restrictions on role interpretations. In this sense, the ADS 
can be viewed as determining a (description) logic.

To be more concrete, in a DL interpretation the interpretation of the function
symbols is determined by the interpretation of the role names. Thus one can,
for example, restrict the class of models to ADMs that interpret a certain
role as a transitive relation or as the composition of two other roles.
Another restriction that can be realized by the choice of ${\cal M}$ is that
nominals (corresponding to nullary function symbols) must be interpreted as
singleton sets.

Let us now define reasoning problems for abstract description systems. 
We will introduce satisfiability of sets of assertions
(with or without term assertions), which corresponds to consistency of
ABoxes (with or without GCIs), and satisfiability of terms (with or without term assertions),
which corresponds to satisfiability of concept descriptions (with or without GCIs). 

\begin{definition}
Given an ADS $(\Lmc, \Mmc)$, a finite set of assertions $\Gamma$
is called \emph{satisfiable} in $({\cal L},{\cal M})$
iff 
there exists an ADM ${\mathfrak W}\in {\cal M}$ and an
assignment $\Amc$ for \Wmf such that $\auf {\mathfrak W},{\cal A}\zu$
satisfies all assertions in $\Gamma$.
The \emph{term} $t$ is called \emph{satisfiable} in $(\Lmc, \Mmc)$
iff $\{ a:t\}$ is satisfiable in $(\Lmc, \Mmc)$, where
$a$ is an arbitrary object variable.                        
%
\begin{itemize}
\item
The \emph{satisfiability problem} for $(\Lmc, \Mmc)$ is concerned with the following
question: given a finite set of \emph{object} assertions $\Gamma$ of $\Lmc$, 
is $\Gamma$ is satisfiable in $({\cal L},{\cal M})$.
\item
The \emph{relativized satisfiability problem} for $(\Lmc, \Mmc)$ 
is concerned with the following question: 
given a finite set of assertions $\Gamma$ of $\Lmc$, 
is $\Gamma$ is satisfiable in $({\cal L},{\cal M})$.
%
\item
The \emph{term satisfiability problem} for $(\Lmc, \Mmc)$ is concerned with the following
question: given a term $t$ of $\Lmc$, is $t$ satisfiable in $(\Lmc, \Mmc)$.
\item
The \emph{relativized term satisfiability problem} for $(\Lmc, \Mmc)$ is concerned with the 
following question: given a term $t$ and a set of \emph{term} assertions $\Gamma$ of $\Lmc$, 
is $\{ a:t\}\cup \Gamma$ satisfiable in $(\Lmc,\Mmc)$.
\end{itemize}
\end{definition}

In the next section, we will define the fusion of two ADSs, and show that
(relativized) satisfiability is decidable in the fusion if (relativized) satisfiability
in the component ADSs is decidable.
For these transfer results to hold, we must restrict ourselves to so-called
local ADSs.
%
%\enlargethispage*{-15mm}
\begin{definition}
Given a family $({\mathfrak W}_{p})_{p\in P}$ of ADMs 
${\mathfrak W}_{p}= \auf W_{p},\Fmc^{{\mathfrak W}_{p}}, \Rmc^{{\mathfrak W}_{p}}\zu$
over pairwise disjoint domains $W_p$, 
we say that
$
{\mathfrak W}= \auf W, \Fmc^{\mathfrak W},
\Rmc^{{\mathfrak W}}\zu
$
is the {\em disjoint union} of 
$({\mathfrak W}_{p})_{p\in P}$
iff
\begin{itemize}
\item
$W = \bigcup_{p\in P} W_p$,
\item
$f^{{\mathfrak W}}(X_{1},\ldots,X_{n_f})
= \bigcup_{p\in P} f^{{\mathfrak W}_{p}}(X_{1}\cap W_{p},\ldots,X_{n_f}\cap W_{p})$
for all $f\in \Fmc$ and \\ $X_{1},\ldots,X_{n_f}\subseteq W$,
\item
$R^{\mathfrak W}= \bigcup_{p\in P} R^{{\mathfrak W}_{p}}$
for all $R \in {\cal R}$.
\end{itemize}       
%
%Given two ADMs 
%$
%{\mathfrak W}_{1}=
%\auf W_{1},F^{{\mathfrak W}_{1}},
%R^{{\mathfrak W}_{1}}\zu
%$
%and
%$
%{\mathfrak W}_{2} = \auf W_{2}, F^{{\mathfrak W}_{2}},
%R^{{\mathfrak W}_{2}}\zu
%$
%with $W_{1}\cap W_{2} =\emptyset$,
%we say that 
%$
%{\mathfrak W}= \auf W, F^{\mathfrak W},
%R^{{\mathfrak W}}\zu
%$
%is the {\em disjoint union} of ${\mathfrak W}_{1}$ and ${\mathfrak W}_{2}$
%iff 
%\begin{itemize}
%\item
%$W = W_{1}\cup W_{2}$,
%\item
%$
%f_i^{{\mathfrak W}}(X_{1},\ldots,X_{n_i})
%= f_i^{{\mathfrak W}_{1}}(X_{1}\cap W_{1},\ldots,X_{n_i}\cap W_{1})
%\cup
%f_i^{{\mathfrak W}_{2}}(X_{1}\cap W_{2},\ldots,X_{n_i}\cap W_{2})
%$
%for all $X_{1},\ldots,X_{n_i}\subseteq W$ and $i\in I$, and
%\item
%$
%%R_{i}^{\mathfrak W}= R_{i}^{{\mathfrak W}_{1}} \cup R_{i}^{{\mathfrak W}_{2}}
%$
%for all $i \in {\cal R}$.
%\end{itemize} 
An ADS
$S=(\Lmc,\Mmc)$ is called \emph{local} iff \Mmc is closed under
disjoint unions.
\end{definition}

In the remainder of this section, we first analyze the connection between ADSs and DLs
in more detail, and then comment on the relationship to modal logics. 

\subsection{Correspondence to description logics}
\label{sect:adsdl}

We will show that the DLs introduced in
Section~\ref{sect:DLs} correspond to ADSs. In
order to do this, we first need to introduce frames, a notion well-known from
modal logic. Let $L$ be one of the DLs introduced in
Section~\ref{sect:DLs}.
%
\begin{definition}[Frames]
  An $L$-frame \Fmf is a pair $(\Delta^\Fmf, \cdot^\Fmf)$, where $\Delta^\Fmf$ is
  a nonempty set,
  called the \defn{domain} of $\Fmf$, and $\cdot^\Fmf$ is the \defn{interpretation function},
  which maps
  %
  \begin{itemize}
  \item each nominal $I$ to a singleton subset $I^\Fmf$ of $\Delta^\Fmf$, and
  \item each role name $R$ to a subset $R^\Fmf$ of $\Delta^\Fmf \times
    \Delta^\Fmf$ such that the restrictions for role interpretations in $L$
    are satisfied. For example, in $\ALC_{R^+}$, each $R \in N_{R^+}$ is
    mapped to a transitive binary relation.
  \end{itemize}
  %
  The interpretation function $\cdot^\Fmf$ can inductively be extended to complex roles in
  the obvious way, i.e., by interpreting the role constructors in $L$
  according to their semantics as given in Figure~\ref{fig:rconstr}.

  %If $L$ does not provide nominals, we assume that $N_O = \emptyset$. 
  An
  interpretation \Imc is \defn{based} on a frame \Fmf iff $\Delta^\Imc =
  \Delta^\Fmf$, $R^\Imc = R^\Fmf$ for all roles $R \in N_R$, and $I^\Imc = I^\Fmf$
  for all nominals $I \in N_O$.

\end{definition}
%
A frame can be viewed as an interpretation that is partial in the sense that
the interpretation of individual and concept names is not fixed.  Note that
(in contrast to the case of concept and individual names) the interpretation
of nominals is already fixed in the frame. The reason for this is that, if we
do not interpret nominals in the frame, then we have to treat them as set
variables on the ADS side. These would, however, have to be variables to which
only singleton sets may be assigned. Since such a restriction is not possible
in the framework of ADSs as defined above, we interpret nominals in the frame.
The consequence is that they correspond to functions of arity 0 on the ADS
side.


Now, we define the abstract description system $S=(\Lmc, \Mmc)$ corresponding
to a DL $L$. It is straightforward to translate the syntax of $L$ into an abstract
description language \Lmc. 

%\enlargethispage*{-2mm}
\begin{definition}[Corresponding ADL]
Let $L$ be a DL with concept and role constructors as well as
restrictions on role interpretations as introduced in Section~\ref{sect:DLs}.
The \emph{corresponding abstract description language} \Lmc is defined as follows.
For every concept name $A$ in $L$, there exists a set variable $x_A$ in \Lmc,
and for every individual name $i$ in $L$ there exists an object variable $a_i$  in \Lmc. 
Let $\Rmc$ be the set of (possibly complex) role descriptions of $L$.
The set of relation symbols of \Lmc is $\Rmc$, and
the set of function symbols of \Lmc is the smallest set containing
%
\begin{enumerate}
%\item a unary function symbol $f_\neg$,
%\item binary function symbols $f_\sqcap$ and $f_\sqcup$,
\item for every role description $R \in \Rmc$, unary function symbols $f_{\exists R}$
  and $f_{\forall R}$,
\item if $L$ provides unqualified number restrictions, then, for every $n \in
  \mathbb{N}$ and every role description $R \in \Rmc$, function symbols $f_{{\geq} n R}$
  and $f_{{\leq} n R}$ of arity 0,
\item if $L$ provides qualified number restrictions, then, for every $n \in
  \mathbb{N}$ and every role $R \in \Rmc$, unary function symbols
  $f_{\dot{\geq} n R}$ and $f_{\dot{\leq} n R}$,
\item if $L$ provides nominals, then, for every $I \in N_O$, a function symbol
  $f_I$ of arity 0,
\item if $L$ provides feature agreement and disagreement, then, for every pair
  of feature chains $(u_1,u_2)$, two function symbols $f_{u_1 {\downarrow}
    u_2}$ and $f_{u_1 {\uparrow} u_2}$ of arity 0.
\end{enumerate}
\end{definition}


For an $L$-concept description $C$, let $t_C$ denote the representation of $C$ as an
\Lmc-term, which is defined in the obvious way: concept names $A$ are
translated into set variables $x_A$, the concept constructors $\neg$, $\sqcap$, and
$\sqcup$ are mapped to $\neg$, $\wedge$, and $\vee$, respectively, and all
other concept constructors are translated to the corresponding function
symbols.                                         
Obviously, both the sets of function and relation symbols of \Lmc may be infinite.
%Note that, by definition of terms in abstract description languages, \Lmc
%is automatically equipped with the Boolean operators.

An example of the translation of concept descriptions into terms of an ADL
was already given above:
% (see remark below Definition~\ref{ADL:def}).
the $\mathcal{ALCN}^\sqcap$-concept description $A
\sqcap \forall (R_1 \sqcap R_2) . \neg (B \sqcap (\geq 2 R_1))$
%, with $A$ and $B$ concept names and $r_1$ and $r_2$ role names,
corresponds to the term $x_A \wedge f_{\forall (R_1 \sqcap R_2)}(\neg (x_B
\wedge f_{(\geq 2 R_1)}))$.                        


We now define the set of abstract description models \Mmc corresponding
to the DL $L$. For every $L$-frame, \Mmc contains a corresponding ADM.
%
\begin{definition}[Corresponding ADM]
\label{cor:adm:def}
  Let $\Fmf=(\Delta^\Fmf, \cdot^\Fmf)$ be a frame. The \defn{corresponding
  abstract description model} $\Wmf = \auf W, \Fmc^\Wmf, \Rmc^\Wmf \zu$ has domain
  $W := \Delta^\Fmf$. 
%
  The relation symbols of $\Lmc$ are just the role descriptions of $L$, and
  thus they are interpreted in the frame $\Fmf$. For each relation symbol $R\in \Rmc$ 
  we can hence define $R^\Wmf := R^\Fmf$.

  To define $\Fmc^\Wmf$, we need to define $f^\Wmf$
  for every nullary function symbol $f$ in \Lmc, and $f^\Wmf(X)$ for every
  unary function symbol $f$ in \Lmc and every $X \subseteq \Delta^\Imc$. 
  Let $A$ be an arbitrary concept name. For each $X\subseteq \Delta^\Fmf$, let 
  $\Imc_X$ be the interpretation based on
  \Fmf mapping the concept name $A$ to $X$ and every other concept name to
  $\emptyset$.\footnote{Taking the empty set here is arbitrary.}
  To define $f^\Wmf$, we make a case distinction according to the type of~$f$:
%
\begin{enumerate}
\item 
% $f_\neg^\Wmf(X_1) = (\neg A_1)^{\Imc_1}$, \\
% $f_\sqcap^\Wmf(X_1, X_2) = (A_1 \sqcap A_2)^{\Imc_2}$,
% $f_\sqcup^\Wmf(X_1, X_2) = (A_1 \sqcup A_2)^{\Imc_2}$,\\ 
 $f_{\exists R}^\Wmf(X) := (\exists R . A)^{\Imc_X}$, \ \  \
 $f_{\forall R}^\Wmf(X) := (\forall R . A)^{\Imc_X}$,
\item  $f_{{\geq} n R}^\Wmf := ({\geq} n R)^{\Imc_\emptyset}$,\ \  \
  $f_{{\leq} n R}^\Wmf := ({\leq} n R)^{\Imc_\emptyset}$,
\item  $f_{\dot{\geq} n R}^\Wmf(X) := ({\geq} n R . A)^{\Imc_X}$,\ \  \
  $f_{\dot{\leq} n R}^\Wmf(X) := ({\leq} n R . A)^{\Imc_X}$,
\item  $f_I^\Wmf := I^{\Imc_\emptyset}$,
\item  $f_{u_1 {\downarrow} u_2}^\Wmf = (u_1 {\downarrow} u_2)^{\Imc_\emptyset}$,\ \  \
  $f_{u_1 {\uparrow} u_2}^\Wmf = (u_1 {\uparrow} u_2)^{\Imc_\emptyset}$.
\end{enumerate}
\end{definition}

The class of ADMs \Mmc thus obtained from a DL $L$
is obviously closed under isomorphic copies since this also holds for the
set of $L$-frames (independently of which DL $L$ we consider).  Hence,
the tuple $S=(\Lmc, \Mmc)$ corresponding to a DL $L$ is indeed an ADS.  

As an example, let us view the DL $\mathcal{ALCN}^\sqcap$ as an
ADS. The ADL \Lmc corresponding to $\mathcal{ALCN}^\sqcap$ has already been discussed.
Thus, we concentrate on the class of ADMs \Mmc induced by the frames
of $\mathcal{ALCN}^\sqcap$.
Assume that $\Fmf$ is such a frame, i.e., $\Fmf$ consists of a nonempty domain
and interpretations $R^{\Fmf}$ of the role names $R$. The ADM
${\mathfrak W} = \auf W, \Fmc^{\mathfrak W}, \Rmc^{\mathfrak W} \zu$ induced by $\Fmf$ is 
defined as follows. The set $W$ is identical to the domain of $\Fmf$. 
Each role description yields a relation symbol, which is interpreted in ${\mathfrak W}$
just as in the frame. For example, $(R_1 \sqcap R_2)^{\mathfrak W} = R_1^{\Fmf}\cap
R_2^{\Fmf}$.  It remains to define the interpretation
of the function symbols. We illustrate this on two examples.
First, consider the (unary) function symbol $f_{\forall (R_1 \sqcap R_2)}$. Given
a subset $X$ of $W$, the function $f_{\forall (R_1 \sqcap R_2)}^{\mathfrak W}$
maps $X$ to
%
$$f_{\forall (R_1 \sqcap R_2)}^{\mathfrak W}(X) :=
  \{ w\in W \mid v\in X\ \mbox{for all $v$ with $(w,v)\in R_1^\Fmf\cap R_2^\Fmf$}\}, $$
i.e., the interpretation of the concept description $\forall (R_1 \sqcap R_2) . A$
in the interpretations based on $\Fmf$ interpreting $A$ by $X$.
Accordingly, the value of the constant symbol $f_{(\geq 2 R)}$ in ${\mathfrak W}$
is given by the interpretation of $(\geq 2 R)$ in the interpretations based on $\Fmf$.  




It is easy to show that the interpretation of concept descriptions in $L$ 
coincides with the interpretation of the corresponding terms in $S=(\Lmc, \Mmc)$.

%
\begin{lemma}
  \label{lem:tcequiv}
  Let \Fmf be a frame, $\Wmf = \auf W, \Fmc^\Wmf, \Rmc^\Wmf \zu$ be the ADM corresponding to
  \Fmf, $\Amc = (\Amc_1,\Amc_2)$ be an assignment for \Wmf, 
  $C$ be a concept description, and let the concept
  names used in $C$ be among $A_1,\dots,A_k$. For all interpretations \Imc
  based on \Fmf with $A_i^\Imc = \Amc_1(x_{A_i})$ for all $1 \leq i \leq k$, we
  have that 
$$
C^\Imc = t_C^{\Wmf,\Amc}.
$$
\end{lemma}
%
%\begin{proof}
%  The proof of the lemma is by induction over the structure of $t_C$. The
%  induction start ($t_C$ is a variable or function of arity 0) follows from
%  the definition of ADMs corresponding to frames. For the induction step, we
%  make a case distinction according to the topmost function symbol $f$ in
%  $t_C$.  We exemplarily treat the case $f=\wedge$. Assume $t_C =
%  f_\wedge(t_D,t_E)$.  By induction, we have that $t_D^{\Wmf,\Amc} = D^\Imc$
%  and $t_E^{\Wmf,\Amc} = E^\Imc$.  By definition of term semantics and
%  description logics semantics, we conclude that $t_C^{\Wmf,\Amc} = C^\Imc$.
%\end{proof}
%

As an easy consequence of this lemma, there is a close connection between reasoning
in a DL $L$ and reasoning in the corresponding ADS.
Given a TBox $\Tmc$ and an ABox $\Amc$ of the DL $L$, we define the corresponding
set $S(\Tmc,\Amc)$ of assertions of the corresponding ADL $(\Lmc,\Mmc)$
in the obvious way, i.e., each GCI $C\sqsubseteq D$ in $\Tmc$ yields a term assertion
$t_C\sqsubseteq t_D$, each role assertion $R(i,j)$ in $\Amc$ yields an
object assertion $R(a_i,a_j)$, and each concept assertion $C(i)$ yields
an object assertion $a_i:t_C$.

%
\begin{proposition}
\label{prop:subseq}
The ABox $\Amc$ is consistent relative to the TBox $\Tmc$ in $L$
iff $S(\Tmc,\Amc)$ is satisfiable in the corresponding ADS.
\end{proposition}

We do not treat non-relativized consistency explicitly since it is the special
case of relativized consistency where the TBox is empty. 

As already mentioned above, our transfer results require the component ADSs to be local.
We call a DL $L$ \emph{local} iff the ADS $(\Lmc,\Mmc)$ corresponding to $L$ is local.
It turns out that not all DLs introduced in Section~\ref{sect:DLs} are local.
%
\begin{proposition}
\label{prop:local}
  Let $L$ be one of the DLs introduced in
  Section~\ref{sect:DLs}. %and let $S=(\Lmc,\Mmc)$ be the corresponding ADS. 
  Then, $L$ is local iff $L$ does not include any of the following constructors:
  nominals, role complement, universal role.
\end{proposition}
%
%\begin{proof}
\noindent
{\bf Proof.\ }
We start with  the ``only if'' direction, which is more interesting
since it shows \defn{why} ADSs corresponding to DLs with
nominals, role complement, or the universal role are not local. We make a case
distinction according to which of these constructors $L$ contains.
%
\begin{itemize}
\item {\bf Nominals. }
  Consider the disjoint union $\Wmf$ of the ADMs $\Wmf_1$ and $\Wmf_2$,
  and assume that $\Wmf_1$ and $\Wmf_2$ correspond to frames of a DL with nominals.
  By definition of the disjoint union, we know that $\Delta^{\Wmf_1} \cap
  \Delta^{\Wmf_2} = \emptyset$. If $I \in N_O$ is a nominal,
  then the definition of the disjoint union implies that
  $f_I^\Wmf = f_I^{\Wmf_1}\cup f_I^{\Wmf_2}$. Since nominals are interpreted
  by singleton sets in $\Wmf_1$ and $\Wmf_2$, and since the domains of $\Wmf_1$ and $\Wmf_2$
  are disjoint, this implies that $f_I^\Wmf$ is a set of cardinality $2$.
  Consequently, $\Wmf$ cannot correspond to an ADM induced by a frame for a DL with
  nominals, since such frames interpret nominals by singleton sets.
%  
\item {\bf Universal role.}
  Again, consider the disjoint union $\Wmf$ of the ADMs $\Wmf_1$ and $\Wmf_2$,
  and assume that $\Wmf_1$ and $\Wmf_2$ correspond to frames of a DL with the universal role.
  Let $U$ denote the universal role, i.e., a role name for which the interpretation
  is restricted to the binary relation relating each pair of individuals of
  the domain. By the definition of the disjoint union,
  we have $U^\Wmf = U^{\Wmf_1} \cup U^{\Wmf_2} = \Delta^{\Wmf_1}\times\Delta^{\Wmf_1}\cup
  \Delta^{\Wmf_2}\times\Delta^{\Wmf_2} \neq \Delta^{\Wmf}\times\Delta^{\Wmf}$.
  Consequently, $\Wmf$ cannot correspond to an ADM induced by a frame for a DL with
  universal role,
  since such a frame would interpret $U$ by
  $\Delta^{\Wmf}\times\Delta^{\Wmf}$.
  
\item {\bf Role complement.} 
  Again, consider the disjoint union $\Wmf$ of the ADMs $\Wmf_1$ and $\Wmf_2$,
  and assume that $\Wmf_1$ and $\Wmf_2$ correspond to frames of a DL with role negation.
  For an arbitrary role name $R$, 
  we have $\overline{R}^\Wmf = \overline{R}^{\Wmf_1} \cup \overline{R}^{\Wmf_2} = 
  (\Delta^{\Wmf_1}\times\Delta^{\Wmf_1}\setminus R^{\Wmf_1})\cup (\Delta^{\Wmf_2}\times\Delta^{\Wmf_2}
  \setminus R^{\Wmf_2})\neq
  (\Delta^{\Wmf_1}\cup\Delta^{\Wmf_2})\setminus (R^{\Wmf_1}\cup R^{\Wmf_2}) =
  \Delta^{\Wmf}\setminus R^{\Wmf}$.
\end{itemize}

It remains to prove the ``if'' direction. Assume that $L$ is one of the DLs introduced in
Section~\ref{sect:DLs} that does not allow for nominals, role complements, and the universal role.
Let $(\Fmf_p)_{p\in P}$ be a family of $L$-frames $\Fmf_p=(\Delta^{\Fmf_p}, \cdot^{\Fmf_p})$ 
and let $\Wmf_p = \auf W_p, \Fmc^{\Wmf_p}, \Rmc^{\Wmf_p} \zu$ be the ADMs corresponding to them.
By definition, $\Delta^{\Fmf_p} = W_p$ for all $p\in P$.
Assume that the domains $(W_p)_{p\in P}$ are pairwise disjoint. We must show that the disjoint union
of $(\Wmf_p)_{p\in P}$ also corresponds to an $L$-frame.
%
To this purpose, we define the frame $\Fmf=(\Delta^{\Fmf}, \cdot^{\Fmf})$ as follows:
%
\begin{itemize}
\item $\Delta^{\Fmf} := \bigcup_{p\in P}\Delta^{\Fmf_p}$ and
\item $R^\Fmf  := \bigcup_{p\in P}R^{\Fmf_p}$ for all $R \in N_R$.
\end{itemize}
%
Let $\Wmf = \auf W, \Fmc^\Wmf, \Rmc^\Wmf \zu \in \Mmc$ be the ADM corresponding to \Fmf. 
By Definition~\ref{cor:adm:def} (corresponding ADM), we have $W = \bigcup_{p\in P}W_p$
and $R^\Wmf  = \bigcup_{p\in P}R^{\Wmf_p}$ for all $R\in N_R$.
By induction on the structure of complex roles, it is easy to show that this
also holds for all $R\in \Rmc$, i.e., all complex role descriptions.
For example, consider the role description $R_1\circ R_2$. By induction, we know
that $R_1^\Wmf  = \bigcup_{p\in P}R_1^{\Wmf_p}$ and $R_2^\Wmf  = \bigcup_{p\in P}R_2^{\Wmf_p}$.
Since the sets $(W_p)_{p\in P}$ are pairwise disjoint, 
$$
(R_1\circ R_2)^\Wmf =
R_1^\Wmf\circ R_2^\Wmf =
\bigcup_{p\in P}R_1^{\Wmf_p}\circ\bigcup_{p\in P}R_2^{\Wmf_p} =
\bigcup_{p\in P}R_1^{\Wmf_p}\circ R_2^{\Wmf_p} =
\bigcup_{p\in P}(R_1\circ R_2)^{\Wmf_p}.
$$

Since $R^{\Wmf_p} = R^{\Fmf_p}$ for all $R\in \Rmc$ and $p\in P$, we obtain the following fact:
%\begin{fact}
%\label{roleclaim}
\begin{itemize}
\item[$(\ast)$\ ]
For all $p \in P$, $a \in \Delta^{\Fmf_p}$, and
role descriptions $R \in \Rmc$, the following
holds: $R^\Fmf(a) = R^{\Fmf_p}(a)$;
in particular, $R^\Fmf(a)\subseteq \Delta^{\Fmf_p}$.
\end{itemize}
%\end{fact}
%
It remains to
show that, for all $n\geq 0$, all $X_{1},\ldots,X_{n}\subseteq W$, and all function symbols
$f$ of arity $n$, we have
$$
f^{{\mathfrak W}}(X_{1},\ldots,X_{n})
= \bigcup_{p\in P}f^{{\mathfrak W}_{p}}(X_{1}\cap W_{p},\ldots,X_{n}\cap W_{p}).
$$
This can be proved by making a case distinction according to the 
type of $f$. We treat two cases exemplarily.                              
\begin{itemize}
\item $f = f_{u_1 {\downarrow} u_2}$.  Since $W = \bigcup_{p\in P}W_p$ and the sets
    $W_p$ are pairwise disjoint, $f_{u_1 {\downarrow}
    u_2}^\Wmf$ is the disjoint union of the sets $f_{u_1 {\downarrow} u_2}^{\Wmf} \cap W_p$
    for $p\in P$.
    It remains to show that $f_{u_1
    {\downarrow} u_2}^{\Wmf} \cap W_p = f_{u_1 {\downarrow} u_2}^{\Wmf_p}$ ($p \in P$).
  By definition of $f_{u_1 {\downarrow} u_2}^{\Wmf_p}$, we know that $a \in
  f_{u_1 {\downarrow} u_2}^{\Wmf_p}$ iff $a \in \Delta^{\Fmf_p}$, both $u_1^{\Fmf_p}(a)$ and
  $u_2^{\Fmf_p}(a)$ are defined, and $u_1^{\Fmf_p}(a) = u_2^{\Fmf_p}(a)$. By
  %Fact~\ref{roleclaim}, 
  $(\ast)$, this is the case iff $a \in \Delta^{\Fmf_p}$, both $u_1^{\Fmf}(a)$ and
  $u_2^{\Fmf}(a)$ are defined and $u_1^{\Fmf}(a) = u_2^{\Fmf}(a)$, which is equivalent to
  $a \in f_{u_1 {\downarrow} u_2}^{\Wmf} \cap W_p$.
 
\item $f = f_{\dot{\geq} n R }$. Since $W = \bigcup_{p\in P}W_p$ and the sets
    $W_p$ are pairwise disjoint, 
   $f_{ \dot{\geq} n R }^\Wmf(X)$ is the disjoint union
   of the sets $f_{ \dot{\geq} n R }^{\Wmf}(X) \cap W_p$ for $p\in P$.
    It remains to show that $f_{ \dot{\geq} n
    R}^{\Wmf}(X) \cap W_p = f_{ \dot{\geq} n R}^{\Wmf_p}(X \cap W_p)$ ($p \in P$).
  By definition of $f_{ \dot{\geq} n R}^{\Wmf_p}$, we know that $a
  \in f_{ \dot{\geq} n R}^{\Wmf_p}(X \cap W_p)$ iff $a \in \Delta^{\Fmf_p}$ and
  $|R^{\Fmf_p}(a) \cap (X \cap W_p)| \geq n$. By $(\ast)$, %Fact~\ref{roleclaim}, 
  this is the case iff $|R^{\Fmf}(a) \cap (X \cap W_p)| \geq n$ iff
  $|R^{\Fmf}(a) \cap X| \geq n$, and hence iff $a \in f_{ \dot{\geq} n
    R}^{\Wmf}(X) \cap W_p$.    \hspace*{\fill}\endmark
\end{itemize} 
%\end{proof}

It should be noted that arguments similar to the ones used in the proof of the
``only if'' direction show that, in the presence of the universal role or of
role negation, function symbols (e.g., $f_{\forall U}$) may also violate the
locality condition.

The transfer results for decidability that are
developed in this paper only apply to fusions of local ADSs.  Hence,
the ``only if'' direction of the proposition implies that our results are not
applicable to fusions of ADSs corresponding to DLs that incorporate nominals,
role complement, or the universal role. 
%In a succeeding section, we will show
%that this is not a defficieny of our approach but that the mentioned transfer
%results do not hold for ADSs / DLs including any of these three operators.

\subsection{Correspondence to modal logics}
\label{sect:adsmodal} 

In this paper our concern are fusions of description logics and not
modal logics. Nevertheless, 
it is useful to have a brief look at the relationship
between ADSs and modal logic.
Standard modal languages can be regarded as ADLs without
relation symbols and object variables (just identify
propositional formulas with terms).
Given such an ADL ${\cal L}$, a set $L$ of ${\cal L}$-terms is
called a {\em classical modal logic} iff is contains all 
tautologies of classical propositional logic 
and is closed under modus ponens, substitutions, and the regularity rule
%
\begin{equation*}
\frac{x_{1}\leftrightarrow y_{1},\ldots,x_{n_{f}}\leftrightarrow y_{n_{f}}}
{f(x_{1},\ldots,x_{n_{f}})\leftrightarrow f(y_{1},\ldots,y_{n_{f}})}
\end{equation*}
%
for all function symbols $f$ of ${\cal L}$.
The minimal classical modal logic in the language with
one unary 
function symbol is known as the logic {\bf E} (see \citeR{Che80}).

Any ADS $({\cal L},{\cal M})$ based on ${\cal L}$ 
determines a classical modal logic $L$ by taking the valid terms, i.e., by defining
$$
t\in L\ \ \mbox{iff}\ \ t^{{\mathfrak W},{\cal A}}=W\ \mbox{for all
${\mathfrak W}\in {\cal M}$ and assignments 
${\cal A}$ in ${\mathfrak W}$}.
$$
The logic ${\bf E}$ is determined by 
the ADS with precisely one unary operator whose class of ADMs 
consists of all models. Chellas formulates
this completeness result (Theorem 9.8 in \citeR{Che80}) for so-called minimal models 
(alias neighborhood-frames),
which are, however, just a notational variant of abstract description models
with one unary operator \cite{Dose88}.
If the classical modal logic $L$ is determined by an ADS with decidable term
satisfiability problem, then $L$ is decidable since $t\in L$ iff $\neg t$ is unsatisfiable.

A classical modal logic $L$ 
is called \emph{normal} iff it additionally contains
%(for $\top= x\vee \neg x$ and $\bot=x \wedge \neg x$)
\begin{eqnarray*}
f(x_{1},\ldots,x_{j-1},x_{j}\wedge y_{j},x_{j+1},\ldots,x_{n_{f}})
&\leftrightarrow &
f(x_{1},\ldots,x_{j-1},x_{j},x_{j+1},\ldots,x_{n_{f}})
\wedge \mbox{} \\ & &
f(x_{1},\ldots,x_{j-1},y_{j},x_{j+1},\ldots,x_{n_{f}})
\end{eqnarray*}
and
$$
f(\top,\bot,\ldots,\bot),\;\;
f(\bot,\top,\bot,\ldots,\bot),\;\ldots, 
f(\bot,\ldots,\bot,\top),
$$
for all function symbols $f$ and all $j$ with $1\leq j\leq n_{f}$ \cite{JoTa51,JoTa52,Gold89}. 
This definition of normal modal logics assumes that the formulas (terms)
are built using only necessity (box) operators.\footnote{%
Note that some authors define
normal modal logics using possibility (diamond) operators, in which case the definitions are the duals
of what we have introduced and thus at first sight look quite different.}
We will work here
only with necessity operators; the corresponding
possibility-operators are definable by putting
$$
f^{\Diamond}(x_{1},\ldots,x_{n_{f}})=
\neg f(\neg x_{1},\ldots,\neg x_{n_{f}}).
$$
The minimal normal modal logic in the language with
one unary operator is known as~{\bf K} \cite{Che80}.

We call a function $F: W^n \rightarrow W$ 
\emph{normal}
iff for all $1\leq j\leq n$ and $X_{1},\ldots,X_{n},Y_{j}\subseteq W$
\begin{eqnarray*}
F(X_{1},\ldots,X_{j-1},X_{j}\cap Y_{j},X_{j+1},\ldots,X_{n})
&=&
F(X_{1},\ldots,X_{j-1},X_{j},X_{j+1},\ldots,X_{n})
\cap \mbox{}\\ & &
F(X_{1},\ldots,X_{j-1},Y_{j},X_{j+1},\ldots,X_{n}))
\end{eqnarray*}
and
\begin{equation*}
F(W,\emptyset,\ldots,\emptyset)=
F(\emptyset,W,\emptyset,\ldots,\emptyset)=
\cdots =
F(\emptyset,\ldots,\emptyset,W)=W.
\end{equation*}
Note that a unary function $F$ is normal iff $F(W)=W$
and 
$F(X\cap Y) = F(X)\cap F(Y)$,
for any $X,Y\subseteq W$.
%
A function symbol $f$ is called \emph{normal} in
an ADS $({\cal L},{\cal M})$
iff the functions $f^{\mathfrak W}$
are normal for all ${\mathfrak W}\in {\cal M}$.

For any role $R$ of some DL, the function symbol $f_{\forall R}$ is normal
in the corresponding ADS. To the contrary, it is readily checked that neither
$f_{\dot{\geq} n R}$ and $f_{\dot{\leq} n R}$
nor their duals
$f_{\dot{\geq} n R}^{\Diamond}$ and 
$f_{\dot{\leq} n R}^{\Diamond}$ are normal.
 
Obviously, an ADS $({\cal L},{\cal M})$ determines a normal modal logic iff
all function symbols of ${\cal L}$ are normal in $({\cal L},{\cal M})$.
Completeness of {\bf K} with respect to Kripke semantics \cite{Che80} implies
that the logic {\bf K} is determined by the ADS with one unary operator whose
class of ADMs consists of all models interpreting this operator by a normal
function.
%(Note, however, that not all normal
%modal logics are determined by ADSs. 
%But one can show that even all classical modal logics are determined by 
%generalized ADS when we allow for
%restrictions of the assignments to certain subalgebras of the
%full powerset-algebra \cite{Gold89}.)


\section{Fusions of abstract description systems}
\label{sect:adsfusions}

In this section, we define the fusion of abstract description systems and
prove two transfer theorems for decidability, one concerning satisfiability and 
the other one concerning relativized satisfiability. 
%
%
\begin{definition}
The \emph{fusion} $S_1 \otimes S_2 = ({\cal L}_{1}\otimes{\cal L}_{2}, {\cal M}_{1}\otimes{\cal M}_{2})$ 
of two abstract description systems $S_1=({\cal L}_{1},{\cal M}_{1})$ and 
$S_2=({\cal L}_{2},{\cal M}_{2})$ over 
\begin{itemize}
\item disjoint sets of function symbols $\Fmc$ of $\Lmc_1$ 
and $\Gmc$ of $\Lmc_2$,
\item disjoint sets of relation symbols $\Rmc$ of $\Lmc_1$
and $\Qmc$ of $\Lmc_2$, and
\item the same sets of set and object variables

\end{itemize}
is defined as follows: 
${\cal L}_{1}\otimes{\cal L}_{2}$ is the ADL based on 
\begin{itemize}
\item 
the union $\Fmc\cup \Gmc$ of the function symbols of 
${\cal L}_{1}$ and ${\cal L}_{2}$, and 
\item
the union $\Rmc\cup \Qmc$ of the relation symbols of ${\cal L}_{1}$ and
${\cal L}_{2}$,
\end{itemize}
and ${\cal M}_{1}\otimes{\cal M}_{2}$ is defined as
%
%\vspace*{-3mm}
%\begin{eqnarray*}
%\lefteqn{%
%{\cal M}_{1}\otimes{\cal M}_{2} :=
% \{ \auf W,\Fmc^{{\mathfrak W}} \cup \Gmc^{{\mathfrak W}},
%           \Rmc^{{\mathfrak W}} \cup \Qmc^{{\mathfrak W}}\zu\mid}
%\hspace{3.5cm}\\[.3em] 
% & &
% \auf W,\Fmc^{{\mathfrak W}},\Rmc^{{\mathfrak W}} \zu\in {\cal M}_{1}\ \mbox{and}\ 
% \auf W, \Gmc^{{\mathfrak W}}, \Qmc^{{\mathfrak W}}\zu  \in {\cal M}_{2}\}.
%\end{eqnarray*}
%
$$
%\begin{eqnarray*}
%\lefteqn{%
%{\cal M}_{1}\otimes{\cal M}_{2} :=
 \{ \auf W,\Fmc^{{\mathfrak W}} \cup \Gmc^{{\mathfrak W}},
           \Rmc^{{\mathfrak W}} \cup \Qmc^{{\mathfrak W}}\zu %\mid }
%\hspace{3.5cm}\\[.3em]
 \mid 
 \auf W,\Fmc^{{\mathfrak W}},\Rmc^{{\mathfrak W}} \zu\in {\cal M}_{1}\ \mbox{and}\
 \auf W, \Gmc^{{\mathfrak W}}, \Qmc^{{\mathfrak W}}\zu  \in {\cal M}_{2}\}.
%\end{eqnarray*}         
$$
\end{definition}

As an example, consider the ADSs $S_1$ and $S_2$ corresponding to the DLs $\mathcal{ALCF}$ and
$\mathcal{ALC}^{{+},{\circ},{\sqcup}}$ introduced in Section~\ref{sect:DLs}. We concentrate
on the function symbols provided by their fusion. In the following, 
we assume that the set of role names employed by
$\mathcal{ALCF}$ and $\mathcal{ALC}^{{+},{\circ},{\sqcup}}$ are disjoint.
\begin{itemize}
\item
The ADS $S_1$ is based on the following function symbols:
(i) unary functions symbol $f_{\forall R}$ and $f_{\exists R}$ for every role name $R$ of
   $\mathcal{ALCF}$,
(ii) nullary functions symbols corresponding to the same-as constructor for every
     pair of chains of functional roles of $\mathcal{ALCF}$.
\item
The ADS $S_2$ is based on the following function symbols:
(iii) unary functions symbol $f_{\forall Q}$ and $f_{\exists Q}$ for every role description
$Q$ built from role names of $\mathcal{ALC}^{{+},{\circ},{\sqcup}}$
using union, composition, and transitive closure.
\end{itemize}
Since we assumed that the set of role names employed by $\mathcal{ALCF}$ and
$\mathcal{ALC}^{{+},{\circ},{\sqcup}}$ are disjoint, these sets of
function symbols are also disjoint. The union of these sets provides us both with
the symbols for the same-as constructor and with the symbols for value and existential
restrictions on role descriptions involving union, composition, and transitive closure.
However, the role descriptions contain only role names from
$\mathcal{ALC}^{{+},{\circ},{\sqcup}}$, and thus none of the functional roles of
$\mathcal{ALCF}$ occurs in such descriptions.
Thus, the fusion of $\mathcal{ALCF}$ and $\mathcal{ALC}^{{+},{\circ},{\sqcup}}$
yields a strict fragment of their union $\mathcal{ALCF}^{{+},{\circ},{\sqcup}}$.
 

\subsection{Relativized satisfiability}

We prove a transfer result for decidability of the relativized satisfiability
problem, show that this also yields a corresponding transfer result for the
relativized \emph{term} satisfiability problem, and investigate how these
transfer results can be extended to ADSs that correspond to DLs providing for
the universal role.

\subsubsection{The transfer result}

This section is concerned with establishing the following transfer theorem:
%
\begin{theorem}
  \label{transfer}
  Let $S_1$ and $S_2$ be local ADSs, and
  suppose that the relativized satisfiability problems for $S_1$ and
  $S_2$ are decidable. Then the relativized satisfiability problem for $S_1
  \otimes S_2$ is also decidable.
\end{theorem}      

The idea underlying the proof of this theorem is to translate a given
set of assertions $\Gamma$ of $S_1 \otimes S_2$ into a set of assertions
$\Gamma_1$ of $S_1$ and a set of assertions $\Gamma_2$ of $S_2$ such that
$\Gamma$ is satisfiable in $S_1 \otimes S_2$ iff $\Gamma_1$ is satisfiable
in $S_1$ and $\Gamma_2$ is satisfiable in $S_2$. The first (naive) idea for 
how to obtain the set $\Gamma_i$ ($i = 1, 2$) is to 
replace in $\Gamma$ alien terms
(i.e., subterms starting with function symbols not belonging to $S_i$) 
by new set variables (the surrogate variables introduced below). 
With this approach, satisfiability of $\Gamma$ would in fact imply
satisfiability of the sets $\Gamma_i$, but the converse would not be true.
The difficulty arises when trying to combine the models of $\Gamma_1$ and
$\Gamma_2$ into one for $\Gamma$. To ensure that the two models can
indeed be combined, the sets $\Gamma_i$ must contain additional assertions
that make sure that the surrogate variables in one model and the corresponding
alien subterms in the other model are interpreted in a ``compatible'' way.
To be more precise, there are (finitely many) different ways of adding such
assertions, and one must try which of them (if any) leads to a satisfiable
pair $\Gamma_1$ and $\Gamma_2$.


For the proof of Theorem~\ref{transfer}, we fix two local ADSs 
$S_i = ({\cal L}_{i},{\cal M}_{i})$, $i\in \{1,2\}$, in
which ${\cal L}_{1}$ is based on the set of function symbols 
$\Fmc$ and relation symbols $\Rmc$,
and ${\cal L}_{2}$ is based on $\Gmc$ and 
$\Qmc$.
Let ${\cal L}= {\cal L}_{1} \otimes {\cal L}_{2}$ and 
${\cal M}= {\cal M}_{1} \otimes {\cal M}_{2}$.                            

In what follows, we use the following notation:
for a set of assertions $\Gamma$,
denote by $\mn{term}(\Gamma)$ and $\mn{obj}(\Gamma)$
the set of terms and
object names in $\Gamma$, respectively.      

We start with explaining how alien subterms in the set $\Gamma$
can be replaced by new set variables.
For each \Lmc-term $t$ of the form
$h(t_{1},\ldots ,t_{n})$, $h\in \Fmc\cup \Gmc$,
we reserve a new variable $x_{t}$,
which will be called the \emph{surrogate} of $t$.
We assume that the set of surrogate variables is disjoint to the
original sets of variables. As sketched above, the idea underlying the introduction
of surrogate variables is that the decision procedure for $S_1$ ($S_2$)
cannot deal with terms containing function symbols from $\Gmc$ ($\Fmc$).
Thus, these ``alien'' function symbols must be replaced before
applying the procedure. To be more precise, we replace the whole
alien subterm starting with the alien function symbol by its surrogate.
For example, if the unary symbol $f$ belongs to $\Fmc$, and the unary symbol $g$ 
belongs to $\Gmc$, then $f(g(f(x)))$ is a ``mixed'' \Lmc-term. To obtain a
term of $\Lmc_1$, we replace the subterm $g(f(x))$ by its surrogate,
which yields $f(x_{g(f(x))})$. Analogously, to obtain a
term of $\Lmc_2$, we replace the whole term by its surrogate,
which yields $x_{f(g(f(x)))}$.
%
We now define this replacement process more formally.

\begin{definition}
For an \Lmc-term $t$ without surrogate variables,
denote by $\rec_{1}(t)$ the ${\cal L}_{1}$-term 
resulting from $t$ when all occurrences of
terms
$g(t_{1},\ldots,t_{n})$, $g\in \Gmc$,
that are not within the scope of some $g'\in \Gmc$ are replaced by
their surrogate variable $x_{g(t_{1},\ldots, t_{n})}$.
For a set $\Theta$ of terms, put
$\rec_{1}(\Theta) := \{ \rec_{1}(t)\mid t \in \Theta\}$
and define $\rec_{2}(t)$ as well as
$\rec_{2}(\Theta)$ accordingly.

Denote by $\mn{sub}(\Theta)$ the set of subterms of terms in
$\Theta$,
and by $\mn{sub}^{1}(\Theta)$ the variables occurring
in $\Theta$ as well as the subterms of alien terms (i.e., terms
starting with a symbol from $\Gmc$) in $\Theta$.
More formally, we can define
$$
\mn{sub}^{1}(\Theta) := \mn{sub}\{ t \mid x_{t} \in var
(\rec_{1}(\Theta))\} \cup \mn{var}(\Theta).
$$
Define $\mn{sub}^{2}(\Theta)$ accordingly.                   
\end{definition}

For example, let $f\in \Fmc$ be unary and $g\in \Gmc$ be binary.
If $t = f(g(x,f(g(x,y))))$, then
$\rec_{1}(t) = f(x_{g(x,f(g(x,y)))})$. Note that the restriction
``not within the scope of some $g'\in G$'' is there to clarify that
only the top-most alien subterms are to be replaced.
For the term $t$ of this example, we have
$\mn{sub}^{1}(\{t\}) = \{ g(x,f(g(x,y))), f(g(x,y)), g(x,y), x, y\}$.
%Intuitively, $\mn{sub}^{1}(\Theta)$ consists of the variables occurring
%in $\Theta$ as well as the subterms of alien terms (i.e., terms
%starting with a symbol from $\Gmc$) in $\Theta$.

Note that the Boolean operators occurring in terms are ``shared'' function
symbols in the sense that they are alien to neither ${\cal L}_{1}$ nor ${\cal L}_{2}$.
Thus, $\rec_{1}(f(x)\wedge g(x,y)) = f(x)\wedge x_{g(x,y)}$ and
$\rec_{2}(f(x)\wedge g(x,y)) = x_{f(x)}\wedge g(x,y)$.

Of course, when replacing whole terms by variables, some information
is lost. For example, consider the (inconsistent) assertion
$(\exists R_1.(({\leq}1\,R_2)\sqcap ({\geq}2\,R_2)))(i)$ and assume that
$R_1$ is a role of one component of a fusion, and $R_2$ a role of the other
component. Translated into abstract description language syntax, the concept
description $\exists R_1.(({\leq}1\,R_2)\sqcap ({\geq}2\,R_2))$ yields the term
$t := f_{\exists R_1}(f_{({\leq}1\,R_2)}\wedge f_{({\geq}2\,R_2)})$,
where $f_{\exists R_1}$ is a function symbol of $\Lmc_1$ and
the other two function symbols belong to $\Lmc_2$.
Now, $\rec_{1}(t) = f_{\exists R_1}(x\wedge y)$, where $x$ is the surrogate
for $f_{({\leq}1\,R_2)}$ and $y$ is the surrogate for $f_{({\geq}2\,R_2)}$.
If the decision procedure for the first ADS only sees $f_{\exists R_1}(x\wedge y)$,
it has no way to know that the conjunction of the alien subterms corresponding
to $x$ and $y$ is unsatisfiable. In fact,
for this procedure $x$ and $y$ are arbitrary set variables, and thus $x\wedge y$
is satisfiable. To avoid this problem, we introduce so-called consistency set consisting
of ``types'', where a type says for each ``relevant'' formula whether the formula itself
or its negation is supposed to hold. The sets $\Gamma_1$ and $\Gamma_2$ will then
contain additional information that basically ensures that their models satisfy
the same types. This will allow us to merge these models into one for $\Gamma$.
%Thus, we need some way to check satisfiability of certain Boolean
%combinations of surrogated subterms. 


\begin{definition}
%The {\em consistency set} ${\cal C}(\Gamma)$
%of $\Gamma$ is defined as
%$
%{\cal C}(\Gamma) := \{ t_{c} \mid c \subseteq term(\Gamma) \},
%$
%where, for $c\subseteq term(\Gamma)$,
Given a finite set $\Theta$ of \Lmc-terms, we define
the {\em consistency set} ${\cal C}(\Theta)$ of $\Theta$ as
${\cal C}(\Theta) := \{ t_{c} \mid c \subseteq \Theta\}$, where the \emph{type}
$t_c$ determined by $c\subseteq \Theta$ is defined as
$$
t_{c} := \bigwedge \{ \chi \mid \chi \in c \} \wedge
\bigwedge
\{ \neg \chi \mid \chi \in \Theta\setminus c \}.
$$
Given a finite set $\Gamma$ of assertions in ${\cal L}$,
we define $\mn{sub}^{i}(\Gamma) := \mn{sub}^{i}(\mn{term}(\Gamma))$.
We abbreviate ${\cal C}^{i}(\Gamma) :=
{\cal C}(sub^{i}(\Gamma))$,
for $i\in \{1,2\}$.                     
\end{definition}

In the example above, we have 
$$\mn{sub}^{1}(f_{\exists R_1}(f_{({\leq}1\,R_2)}\wedge f_{({\geq}2\,R_2)}) =
\{  f_{({\leq}1\,R_2)}, f_{({\geq}2\,R_2)}\},$$
and thus
${\cal C}^{1}(\{a_i : f_{\exists R_1}(f_{({\leq}1\,R_2)}\wedge f_{({\geq}2\,R_2)})\})$
consists of the $4$ terms
$$
\begin{array}{rcl}
f_{({\leq}1\,R_2)}& \wedge & f_{({\geq}2\,R_2)},
\\[.2em]
f_{({\leq}1\,R_2)}& \wedge & 
\neg f_{({\geq}2\,R_2)}, \\[.2em]
\neg f_{({\leq}1\,R_2)}&  
\wedge & f_{({\geq}2\,R_2)}, \text{ and}
\\[.2em]
\neg f_{({\leq}1\,R_2)}&  
\wedge & \neg f_{({\geq}2\,R_2)}.
\end{array}
$$
%
Given a set of terms $\Theta$, an element $t_c$ of its consistency set ${\cal C}(\Theta)$ can 
indeed be considered as the ``type'' of an element $e$ of the domain of an ADM w.r.t.\ 
$\Theta$. Any such element $e$ belongs to the interpretations of some of the terms
in $\Theta$, and to the complements of the interpretations of the other terms.
Thus, if $c$ is the set of terms of $\Theta$ to which $e$ belongs,
then $e$ also belongs to the interpretation of $t_c$ and it does not belong to
the interpretation of any of the other terms in ${\cal C}(\Theta)$. In this case we say
that $e$ \emph{realizes} the type $t_c$.

We are now ready to formulate the theorem that reduces the relativized satisfiability problem
in a fusion of two local ADSs to relativized satisfiability in the component
ADSs. A proof of this theorem can be found in the appendix.
%From this Theorem~\ref{transfer} follows immediately.
 
\begin{theorem}\label{criterion}
Let
$S_i = ({\cal L}_{i},{\cal M}_{i})$, $i\in \{1,2\}$, be 
two local ADSs in
which ${\cal L}_{1}$ is based on the set of function symbols
$\Fmc$ and relation symbols $\Rmc$,
and ${\cal L}_{2}$ is based on $\Gmc$ and
$\Qmc$, and let ${\cal L}= {\cal L}_{1} \otimes {\cal L}_{2}$ and
${\cal M}= {\cal M}_{1} \otimes {\cal M}_{2}$.           
If $\Gamma$ is a finite set of assertions from ${\cal L}$,
then the following are equivalent:
\begin{enumerate}
\item
\label{cond:one:criterion}
$\Gamma$ is satisfiable in $({\cal L},{\cal M})$.
\item
\label{cond:two:criterion}
There exist
\begin{enumerate}
\item\label{a} 
  a set $D\subseteq {\cal C}^{1}(\Gamma)$,
\item\label{b} 
  for every term $t\in D$ an object variable $a_{t}\not\in \mn{obj}(\Gamma)$,
\item\label{c}
   for every $a\in \mn{obj}(\Gamma)$ a term $t_{a}\in D$,
%such that every $s$ with $(a:s)\in \Gamma$ is a conjunct of $t_{a}$,
\end{enumerate}
%
such that the union $\Gamma_{1}$ of the following sets of
assertions in $\Lmc_1$ is satisfiable in $({\cal L}_{1},{\cal M}_{1})$:
%
\begin{enumerate}
\addtocounter{enumii}{3}
\item\label{d}
  $\{a_{t}:\mn{sur}_{1}(t) \mid t\in D\}\cup \{ \top\sqsubseteq \mn{sur}_{1}(\bigvee D)\}$,
%\item\label{e}
%  $\{ \top\sqsubseteq \mn{sur}_{1}(\bigvee D)\}$,
\item\label{e}
  $\{a:\mn{sur}_{1}(t_{a}) \mid a \in \mn{obj}(\Gamma)\}$,
\item\label{f} 
  $\{R(a,b) \mid R(a,b) \in \Gamma, R\in {\cal R}\}$,
\item\label{g}
  $\{ \mn{sur}_{1}(t_{1})\sqsubseteq \mn{sur}_{1}(t_{2}) \mid t_{1}\sqsubseteq t_{2}\in \Gamma\}
   \cup \{a:\mn{sur}_{1}(s)\mid (a:s)\in \Gamma\}$;

\end{enumerate}
%
and the union $\Gamma_{2}$ of the following sets of
assertions in $\Lmc_2$ is satisfiable in $({\cal L}_{2},{\cal M}_{2})$:
%
\begin{enumerate}
\addtocounter{enumii}{7}
\item\label{h}
  $\{a_{t}:\mn{sur}_{2}(t) \mid t\in D\}\cup \{ \top\sqsubseteq \mn{sur}_{2}(\bigvee D)\}$,
\item\label{i}
  $\{a:\mn{sur}_{2}(t_{a}) \mid a \in \mn{obj}(\Gamma)\}$,
\item\label{j}
 $\{Q(a,b) \mid Q(a,b) \in \Gamma, Q\in {\cal Q}\}$.
%\cup \{a:\mn{sur}_{2}(s)\mid (a:s)\in \Gamma\}$
%\item\label{l}
%  $\{ \top\sqsubseteq \mn{sur}_{2}(\bigvee D)\}$.
\end{enumerate}
%
\end{enumerate}
\end{theorem}                                                  

Intuitively, (\ref{a})  ``guesses'' a set $D$ of types (i.e., elements of
the consistency set). The idea is that these are exactly the types that
are realized in the model of $\Gamma$ (to be constructed when showing
$(\ref{cond:two:criterion}\rightarrow\ref{cond:one:criterion})$ and given when
showing $(\ref{cond:one:criterion}\rightarrow\ref{cond:two:criterion})$). 
Condition~(\ref{b}) introduces for every type in $D$ a name for an object realizing
this type, and (\ref{c}) ``guesses'' for every object variable occurring in
$\Gamma$ a type from $D$.

Regarding (\ref{d}) and (\ref{h}), one should note that the set of assertions
$\{a_{t}:t \mid t\in D\}\cup \{ \top\sqsubseteq \bigvee D\}$ states that
every type in $D$ is realized (i.e., there is an object in the model having this type)
and that every object has one of the types in $D$. The sets of assertions
(\ref{d}) and (\ref{h}) are obtained from this set through surrogation to make it
digestible by the decision procedures of the component logics.

The assertions in (\ref{e}) and (\ref{i}) state (again in surrogated versions)
that the object interpreting the variable $a$ has type $t_a$. This ensures that,
in the models of $\Gamma_1$ and $\Gamma_2$ (given when showing
$(\ref{cond:two:criterion}\rightarrow\ref{cond:one:criterion})$), the objects interpreting $a$ have the
same type $t_a$ from $D$. Otherwise, these models could not be combined into a common one
for $\Gamma$.

The sets (\ref{f}) and (\ref{j}) are obtained from $\Gamma$ by distributing
its relationship assertions between $\Gamma_1$ and $\Gamma_2$,
depending on the relation symbol used in the assertion.

The set (\ref{g}) contains (in surrogated version) the term assertions of the form $t_1\sqsubseteq t_2$
and the membership assertions of the form $a:s$ of $\Gamma$.

Condition~\ref{cond:two:criterion} is
asymmetric in two respects. First, it guesses a subset of ${\cal C}^{1}(\Gamma)$
rather than a subset of ${\cal C}^{2}(\Gamma)$. Of course this is arbitrary, we could
also have chosen index $2$ instead of $1$ here. 
Second, the set
$\Gamma_2$ neither contains the assertions
$\{ \mn{sur}_{2}(t_{1})\sqsubseteq \mn{sur}_{2}
(t_{2}) \mid t_{1}\sqsubseteq t_{2}\in \Gamma\}$ nor
$\{a:\mn{sur}_{2}(s)\mid (a:s)\in \Gamma\}$.
If we added these assertions, 
the theorem would still be true, but this
would unnecessarily increase the amount of work 
to be done by the combined decision procedure.
In fact, since the other assertions in $\Gamma_1$ and $\Gamma_2$ enforce a tight coordination
between the models of $\Gamma_1$ and $\Gamma_2$, the fact that the membership assertions
and term assertions of $\Gamma$ are satisfied in the models of $\Gamma_1$ implies
that they are also satisfied in the models of $\Gamma_2$ (see the appendix for details).

To prove Theorem~\ref{transfer}, we must show how Theorem~\ref{criterion}
can be used to construct a decision procedure for relativized satisfiability
in $S_1\otimes S_2$ from such decision procedures for the component systems
$S_1$ and $S_2$. For a given finite set of assertions $\Gamma$ of $S_1\otimes S_2$,
the set ${\cal C}^{1}(\Gamma)$ is also finite, and thus there are finitely many
sets $D$ in (\ref{a}) and choices of types for object variables in (\ref{c}). Consequently,
we can enumerate all of them and check whether one of these choices leads to
satisfiable sets $\Gamma_1$ and $\Gamma_2$. 
%
By definition of the sets $\Gamma_i$ and of the functions $\mn{sur}_i$, the
assertions in $\Gamma_i$ are indeed assertions of $\Lmc_i$, and thus
the satisfiability algorithm for $({\cal L}_{i},{\cal M}_{i})$ can be
applied to $\Gamma_i$. This proves Theorem~\ref{transfer}.

Regarding the complexity of the obtained decision procedure, the
costly step is guessing the right set $D$. Since the cardinality
of the set $\mn{sub}^1(\Gamma)$ is linear in the size of $\Gamma$,
the cardinality of ${\cal C}^{1}(\Gamma)$ is exponential in the size of
$\Gamma$ (and each element of it has size quadratic in $\Gamma$).
Thus, there are doubly exponentially many different subsets to be chosen
from. Since the cardinality of the chosen set $D$ may be exponential in the
size of $\Gamma$, also the size of $\Gamma_1$ and $\Gamma_2$ may be exponential
in $\Gamma$ (because of the big disjunction over $D$).
From this, the following corollary follows.

\begin{corollary}
  Let $S_1$ and $S_2$ be local ADSs, and
  suppose that the relativized satisfiability problems for $S_1$ and
  $S_2$ are decidable in {\sc ExpTime} ({\sc PSpace}). Then the relativized 
  satisfiability problem for $S_1\otimes S_2$ is decidable in 
  {\sc 2ExpTime} ({\sc ExpSpace}).
\end{corollary}

\begin{proof}
Assume that $\Gamma$ has size $n$. Then we must consider $2^{2^{p_1(n)}}$ (for some polynomial
$p_1$) different sets $D$ in (\ref{a}). Each such set has size $2^{p_1(n)}$ and thus we 
have of $2^{2^{p_2(n)}}$ choices in (\ref{c}) (for some polynomial $p_2$). 
Overall, this still leaves us with doubly exponentially many choices. 
Now assume that the relativized satisfiability problems for $S_1$ and
$S_2$ are decidable in {\sc ExpTime}. Since each call of these procedures is applied
to a set of assertions of exponential size, it may take double exponential time,
say $2^{2^{p_3(n)}}$ and $2^{2^{p_4(n)}}$ (for polynomials $p_3$ and $p_4$).
Overall, we thus have a time complexity of 
$$2^{2^{p_1(n)}}\cdot 2^{2^{p_2(n)}} \cdot (2^{2^{p_3(n)}} + 2^{2^{p_4(n)}}),$$ 
which can clearly be majorized by $2^{2^{p(n)}}$ for an appropriate
polynomial $p$. This shows membership in {\sc 2ExpTime}.

The argument regarding the space complexity is similar. Here one must additionally
take into account that doubly exponentially many choices can be enumerated using an 
exponentially large counter.
\end{proof}

\subsubsection{The relativized term satisfiability problem}

The statement of Theorem~\ref{transfer} itself does not imply a transfer
result for the relativized term satisfiability problem. The problem is that
decidability of the relativized \emph{term} satisfiability problem in $S_1$
and $S_2$ does not necessarily imply decidability of the relativized satisfiability 
problem in these ADSs, and thus the prerequisite for the theorem to apply is not
satisfied. However, if we consider the statement of Theorem~\ref{criterion},
then it is easy to see that this theorem also yields a transfer result
for the relativized \emph{term} satisfiability problem.

\begin{corollary}
  \label{transfer:term}
  Let $S_1$ and $S_2$ be local ADSs, and
  suppose that the relativized term satisfiability problems for $S_1$ and
  $S_2$ are decidable. Then the relativized \emph{term} satisfiability problem for $S_1
  \otimes S_2$ is also decidable.
\end{corollary}   

\begin{proof}
Consider the satisfiability criterion in Theorem~\ref{criterion}. If
we are interested in relativized term satisfiability, then
$\Gamma$ is of the form $\{a:t\}\cup \Gamma'$, where $\Gamma'$
is a set of term assertions. In this case, the sets of assertions
$\Gamma_1$ and $\Gamma_2$ do not contain object assertions involving
relations. Now, assume that $\Gamma_i$ is of the form
$\{a_1:t_1,\ldots,a_n:t_n\}\cup \Gamma_i'$, where $\Gamma_i'$
is a set of term assertions. 
Since two assertions
of the form $b:s_1, b:s_2$ are equivalent to one assertion $b:s_1\wedge s_2$,
we may assume that the $a_i$ are distinct from each other.
Since $S_i$ is local, it is easy to see that the following are equivalent:
%
\begin{enumerate}
\item
  $\{a_1:t_1,\ldots,a_n:t_n\}\cup \Gamma_i'$ is satisfiable in $S_i$.
\item
  $\{a_j:t_j\}\cup \Gamma_i'$ is satisfiable in $S_i$ for all $j = 1,\ldots,n$.
\end{enumerate}
%
Since $(1\rightarrow 2)$ is trivial, it is enough to show $(2\rightarrow 1)$.
Given models $\Wmf_j\in \Mmc_i$ of $\{a_j:t_j\}\cup \Gamma_i'$ ($j = 1,\ldots,n$),
their disjoint union also belongs to $\Mmc_i$, and it is clearly a model of
$\{a_1:t_1,\ldots,a_n:t_n\}\cup \Gamma_i'$.

The second condition can now be checked by applying the term satisfiability test
in $S_i$ $n$ times.
\end{proof}

\subsubsection{Dealing with the universal role}

As stated above (Proposition~\ref{prop:local}), ADSs corresponding to
DLs with the universal role are not local, and thus Theorem~\ref{transfer}
cannot be applied directly. Nevertheless, in some cases this theorem
can also be used to obtain a decidability result for fusions of DLs
with the universal role, provided that both of them provide for a universal role.
(We will comment on the usefulness of this approach in more detail in
Section~\ref{sect:nominals}). 

\begin{definition}
Given an ADS $S=(\Lmc,\Mmc)$, we denote by $S^U$
the ADS obtained from $S$ by
%
\begin{enumerate}
\item extending \Lmc with two function symbols $f_{\exists U_S}$ and
  $f_{\forall U_S}$, and
\item extending every ADM $\Wmf=\auf W,\Fmc^\Wmf,\Rmc^\Wmf\zu \in \Mmc$ with the unary
  functions $f_{\exists U_S}^\Wmf$ and $f_{\forall U_S}^\Wmf$,
  where
  \begin{itemize}
  \item
   $f_{\exists U_S}^\Wmf(X)=\emptyset$ if $X=\emptyset$, and 
   $f_{\exists U_S}^\Wmf(X)=W$ otherwise; 
  \item
   $f_{\forall U_S}^\Wmf(X)=W$ if $X=W$, and $f_{\forall U_S}^\Wmf(X)=\emptyset$ otherwise.
  \end{itemize}
\end{enumerate}
\end{definition}
%
For ADSs $S$ corresponding to a DL $L$, the ADS $S^U$
corresponds to the extension of $L$ with the universal role, where
the universal role can only be used within value and existential
restrictions.\footnote{%
Note that it is not necessary to add the universal role $U$ to the set of
relation symbols since an assertion of the form $U(a,b)$ is trivially true.
However, the use of the universal role within (qualified) number restrictions
is not covered by this extension.} There is a close connection between
the relativized satisfiability problem in $S$ and the satisfiability problem
in $S^U$.

\begin{proposition}
\label{universal:prop}
If $S$ is a local ADS, then the following conditions are equivalent:
\begin{enumerate}
\item\label{universal:prop:1}
  the relativized (term) satisfiability problem for $S$ is decidable,
\item\label{universal:prop:2}
  the (term) satisfiability problem for $S^{U}$ is decidable,
\item\label{universal:prop:3}
  the relativized (term) satisfiability problem for $S^{U}$ is decidable.
\end{enumerate}
\end{proposition}
%
\begin{proof}
We restrict our attention to the term satisfiability problem
since the equivalences for the satisfiability problem can be proved similarly.

The implication $(\ref{universal:prop:3}\rightarrow\ref{universal:prop:2})$
is trivial, and $(\ref{universal:prop:2}\rightarrow\ref{universal:prop:1})$
is easy to show. In fact, $t$ is satisfiable in $S$ relative to the
term assertions $\{ s_1\sqsubseteq t_1,\ldots, s_n\sqsubseteq t_n\}$
iff $t\wedge f_{\forall U_S}.((\neg t_1\vee s_1)\wedge \ldots\wedge(\neg t_n\vee s_n))$
is satisfiable in $S^U$.

To show $(\ref{universal:prop:1}\rightarrow\ref{universal:prop:3})$, we
assume that the relativized term satisfiability problem for $S$ is
decidable.
Let $S=({\cal L},{\cal M})$ and $S^{U}=({\cal L}^{U},{\cal M}^{U})$.
In the following, we use $f_{U}$ as an abbreviation for $f_{\forall U_{S}}$. 
Since we can replace equivalently in any term the function symbol
$f_{\exists U_{S}}$ by $\neg f_{U} \neg$,
we may assume without loss of generality that 
$f_{\exists U_{S}}$ does not occur in terms of ${\cal L}^{U}$.

Suppose a set $\Sigma=\{a:s\} \cup \Gamma$ from ${\cal L}^{U}$ is given, where $\Gamma$
is a set of term assertions. We want to decide whether $\Sigma$
is satisfiable in some model ${\mathfrak W}\in {\cal M}^{U}$.
To this purpose, we transform $\Sigma$ into a set of assertions not containing
$f_{U}$. The idea underlying this transformation is that, given a model
${\mathfrak W}\in {\cal M}^{U}$, we have $f_U(t)^{\Wmf} \in \{W, \emptyset\}$,
depending on whether $t^{\Wmf} = W$ or not. Consequently, if we replace
$f_U(t)$ accordingly by $\top$ or $\bot$, the evaluation of this term
in $\Wmf$ does not change. However, in the satisfiability test we do not have 
the model $\Wmf$ (we are trying to decide whether one exists), and thus we 
must \emph{guess} the right replacement. 

A term $t$ from ${\cal L}^{U}$ is called a $U$-{\em term} iff it starts with
$f_{U}$. The set of $U$-terms that occur (possibly as subterms) in $\Sigma$
is denoted by $\Sigma^{U}$. Set, inductively, for any function 
$\sigma: \Sigma^{U} \rightarrow \{\bot,\top\}$ and all subterms of terms in $\Sigma$:
\begin{eqnarray*}
x^{\sigma} & := & x,\\
(t_{1}\wedge t_{2})^{\sigma} & := & t_{1}^{\sigma}\wedge t_{2}^{\sigma},\\
(t_{1}\vee t_{2})^{\sigma} & := & t_{1}^{\sigma}\vee t_{2}^{\sigma},\\ 
(\neg t)^{\sigma} & := & \neg t^{\sigma},\\
(f(t_{1},\ldots,t_{n}))^{\sigma} & := & f(t_{1}^{\sigma},\ldots,t_{n}^{\sigma})\ \
\mbox{for $f\neq f_{U}$ of arity $n$},\\
(f_{U}(t))^{\sigma} & := & \sigma(f_{U}(t)).
\end{eqnarray*}
Thus, $t^{\sigma}$ is obtained from $t$ by replacing all occurrences of
$U$-terms in $t$ by their image under $\sigma$, i.e., by $\bot$ or $\top$.
Define, for any such function $\sigma$, 
\begin{eqnarray*}
\Sigma^{\sigma} & := & 
        \{ t_{1}^{\sigma}\sqsubseteq t_{2}^{\sigma} \mid t_{1}\sqsubseteq t_{2}
              \in \Gamma\}\cup \{a:s^{\sigma}\} \cup\mbox{}\\
     & & \{ \top\sqsubseteq t^{\sigma} \mid f_{U}(t)\in \Sigma^{U}\ \mbox{and}\ \sigma(f_{U}(t))=\top\}
     \cup\mbox{}\\
     & & \{ a_{t} : \neg t^{\sigma} \mid f_{U}(t)\in \Sigma^{U}\ \mbox{and}\ \sigma(f_{U}(t)) = \bot\},
\end{eqnarray*}
where the $a_{t}$ are mutually distinct new object variables.  Note that
$\Sigma^{\sigma}$ does not contain the function symbol $f_{U}$, and thus it
can be viewed as a set of assertions of $S$.  In addition, though it contains
more than one membership assertion, it does not contain assertions involving
relation symbols. Consequently, the satisfiability of $\Sigma^{\sigma}$ in $S$
can be checked using the term satisfiability test for $S$ (see the proof of
Corollary~\ref{transfer:term} above).  Decidability of the relativized term
satisfiability problem for $S^{U}$ then follows from the following claim:

\medskip
\noindent
{\bf Claim.}
\emph{$\Sigma$ is satisfiable in a member of ${\cal M}^{U}$ iff
there exists a mapping $\sigma:\Sigma^{U} \rightarrow \{\bot,\top\}$ 
such that $\Sigma^{\sigma}$ is satisfiable in
a member of ${\cal M}$. }

\medskip
To prove this claim, first suppose that $\Sigma$ is satisfied under an assignment
${\cal A}$ in a member ${\mathfrak W}=\auf W,\Fmc^{\mathfrak W}\cup\{f_{U}^{\mathfrak W}\},
\Rmc^{\mathfrak W}\zu$
of ${\cal M}^{U}$. Define $\sigma$ by setting
$\sigma(f_{U}(t)) = \top$ if $(f_{U}(t))^{{\mathfrak W},{\cal A}}=W$,
and $\sigma(f_{U}(t)) = \bot$ otherwise. Obviously, this implies that $\Sigma^{\sigma}$ is
satisfied under the assignment ${\cal A}$ in $\auf W,\Fmc^{\mathfrak W}, \Rmc^{\mathfrak W}\zu$,
which is a member of ${\cal M}$. 

Conversely, suppose $\Sigma^{\sigma}$ is satisfiable for
some mapping $\sigma$. Take a member ${\mathfrak W}=\auf W,\Fmc^{\mathfrak W},\Rmc^{\mathfrak W}\zu$
of ${\cal M}$ and an assignment ${\cal A}$ such such that 
$\auf {\mathfrak W},{\cal A}\zu\models \Sigma^{\sigma}$. 
Set ${\mathfrak W}':=\auf W,\Fmc^{\mathfrak W}\cup\{f_{U}^{\mathfrak W}\},\Rmc^{\mathfrak W} \zu$,
and prove, by induction, for all
terms $t$ that occur in $\Sigma$:
$$
(*)\ \ \ \  t^{{\mathfrak W}',{\cal A}} = (t^{\sigma})^{{\mathfrak W},{\cal A}}.
$$
The only critical case is the one where $t = f_U(s)$. First, assume that
$\sigma(f_U(s)) = (f_U(s))^\sigma = \top$. Then $\Sigma^\sigma$ contains $\top\sqsubseteq s^{\sigma}$,
and thus $W = (s^{\sigma})^{{\mathfrak W},{\cal A}} = s^{{\mathfrak W}',{\cal A}}$, where
the second identity holds by induction. However, $s^{{\mathfrak W}',{\cal A}} = W$ implies
$(f_U(s))^{{\mathfrak W}',{\cal A}} = W = \top^{{\mathfrak W},{\cal A}}$.
The case where $\sigma(f_U(s)) = (f_U(s))^\sigma =\bot$ can be treated similarly. Here the
term assertion $a_s:\neg s^\sigma$ ensures that $s^\sigma$ (and thus by induction $s$)
is not interpreted as the whole domain. Consequently, applying $f_U$ to it yields the
empty set. 

Since $\auf {\mathfrak W},{\cal A}\zu\models \Sigma^{\sigma}$, the identity
$(*)$ implies that $\auf {\mathfrak W}',{\cal A}\zu\models \Sigma$.  This
completes the proof of the claim, and thus also of the proposition.
\end{proof}

For normal modal logics, the result stated in this proposition was already
shown by \citeA{GoPa92}. The proof technique used there can, however, not be
transfered to our more general situation since it strongly depends on the
normality of the modal operators.

Using Proposition~\ref{universal:prop}, we obtain the following
corollary to our first transfer theorem.
%
\begin{corollary}
  \label{corollary}
  Let $S_{1}$, $S_{2}$ be local ADSs and assume that, for $i \in \{1,2\}$,
  the relativized (term) satisfiability problem for $S_{i}$ is decidable.  Then the
  relativized (term) satisfiability problem for $S_{1}^{U} \otimes S_{2}^{U}$ is
  decidable.
\end{corollary}
%
\begin{proof}
We know by
Theorem~\ref{transfer} (Corollary~\ref{transfer:term}) that the relativized (term) satisfiability
problem for $S_{1}\otimes S_{2}$ is decidable. Hence, 
Proposition~\ref{universal:prop} yields that the relativized (term) satisfiability problem
for $(S_{1}\otimes S_{2})^{U}$ is decidable. But $S_{1}^{U} \otimes S_{2}^{U}$
is just a notational variant of $(S_{1} \otimes S_{2})^{U}$: the function
symbols $f_{\exists U_{S_1}}$ and $f_{\exists U_{S_2}}$ can be replaced by
$f_{\exists U_{S_{1}\otimes S_{2}}}$ (and analogously for $f_{\forall
  U_{S_{1}\otimes S_{2}}}$) since all three have identical semantics.
\end{proof}

\subsection{Satisfiability}

Note that Theorem~\ref{transfer} does not yield a transfer result for the unrelativized
satisfiability problem. Of course, if the relativized satisfiability problems for $S_1$ and
$S_2$ are decidable, then the theorem implies that the satisfiability problem for
$S_1 \otimes S_2$ is also decidable (since it is a special case of the
relativized satisfiability problem). However, to be able to apply the theorem
to obtain decidability of the satisfiability problem in the fusion, the component ADSs
must satisfy the stronger requirement that the relativized satisfiability problem is decidable.
Indeed, the set $\Gamma_i$ in Theorem~\ref{criterion} contains a term assertion
(namely $\top\sqsubseteq \mn{sur}_{i}(\bigvee D)$) even if $\Gamma$ does not contain
any term assertions.

There are cases where the relativized satisfiability problem is undecidable whereas the
satisfiability problem is still decidable.  For example,
Theorem~\ref{transfer} cannot be applied for the fusion of
$\mathcal{ALCF}$ and $\mathcal{ALC}^{{+},{\circ},{\sqcup}}$
since the relativized satisfiability problem for $\mathcal{ALCF}$ is already undecidable
\cite{BBNNS93}.
However, the satisfiability problem is decidable for both DLs. 

\subsubsection{Covering normal terms}

Before we can formulate
a transfer result for the satisfiability problem, we need to introduce an additional
notion, which generalizes the notion of a normal modal logic. 

\begin{definition}[Covering normal terms]
\label{def:covnt}
Let $({\cal L},{\cal M})$ be an ADS and $f$ be a function symbol of \Lmc
of arity $n$. The term $t_f(x)$ (with one variable $x$) is a \emph{covering normal term}
for $f$ iff the following holds for all ${\mathfrak W}\in {\cal M}$:
\begin{itemize}
\item $t_{f}^{\mathfrak W}(W) = W$
\item
for all $X,Y\subseteq W$,
$
t_{f}^{\mathfrak W}(X \cap Y) = t_{f}^{\mathfrak W}(X) \cap
t_{f}^{\mathfrak W}(Y),
$ and
\item for all $X, X_{1},\ldots,%X_{n},Y_{1},\ldots,
Y_{n}\subseteq W$:
$X \cap X_{i} = X \cap Y_{i} \text{ for $1\leq i\leq n$ implies}$\\
$$
t_{f}^{\mathfrak W}(X) \cap f^{\mathfrak W}(X_{1},
\ldots,X_{n}) = t_{f}^{\mathfrak W}(X) \cap
f^{\mathfrak W}(Y_{1},\ldots,Y_{n}).
$$
\end{itemize}
An ADS $({\cal L},{\cal M})$ is said to
\emph{have covering normal terms} iff one can effectively determine a
covering normal term $t_f$ for every function symbol $f$ of \Lmc.                   
\end{definition}
%
Intuitively, the first two conditions state that the covering normal term
behaves like a value restriction (or box operator). Consider the term 
$f_{\forall R}(x)$, where $f_{\forall R}$ is the function symbol corresponding 
to the value restriction constructor for the role $R$. 
Then $f_{\forall R}(x)$ obviously satisfies the
first two requirements for covering normal terms. 
Note that the second condition implies that the function induced by
$t_{f}$ is monotonic, i.e., $X\subseteq Y$ implies 
$t_{f}^{\mathfrak W}(X)\subseteq t_{f}^{\mathfrak W}(Y)$.
The third condition specifies the connection between the covering normal term
and the function symbol it covers. With respect to elements of $t_{f}^{\mathfrak W}(X)$,
the values of the functions $f^{\mathfrak W}(X_{1}, \ldots,X_{n})$ and 
$f^{\mathfrak W}(Y_{1}, \ldots,Y_{n})$ agree provided that their arguments agree on $X$.
It is easy to see
that $f_{\forall R}(x)$ is a covering normal term for the function symbols
corresponding to the value, existential, and (qualified)
number restrictions on the role $R$ (see Proposition~\ref{DL:covering:nt:prop} below).      

Given covering normal terms $t_f$ for the function symbols $f$ of a finite
set of function symbols $E$, one can construct a term $t_E$ that is
a covering normal term for all the elements of $E$.

\begin{lemma}
\label{cntexist}
Suppose the ADS $({\cal L},{\cal M})$ has covering normal terms and
$\Lmc$ is based on a set of function symbols $F$. Denote by $t_f$ the
covering normal term for the function symbol $f$, for all $f \in F$.
Then, for every finite set $E\subseteq F$ of function symbols, the term
$$
t_{E}(x) := \bigwedge_{f \in E} t_{f}(x)
$$
is a covering normal term for all $f\in E$.
\end{lemma}                                      

\subsubsection{Correspondence to normal modal logics}


The following result shows that any ADS in
which every function symbol is normal has covering normal terms.
Hence, the notion of covering normal terms generalizes the
notion of normality in modal logics.

\begin{proposition}
Let $({\cal L},{\cal M})$ be an ADS, and assume that 
$f$ is a normal function symbol in $({\cal L},{\cal M})$. Then
$$
t_{f}(x) := 
f(x,\bot,\ldots,\bot) \wedge f(\bot,x,\ldots,\bot) \wedge \cdots \wedge 
f(\bot,\ldots,\bot,x)
$$
is a covering normal term for $f$.
In particular, if $f$ is nullary (unary), then $t_{f}(x) = \top$
($t_{f}(x) = f(x)$) is a covering normal term for $f$.
\end{proposition}
\begin{proof}
The first two conditions in the definition of covering normal
terms immediately follow from the definition of normal function symbols. 
Thus, we concentrate on the third condition.
Assume, for simplicity, that $f$ is binary.
Suppose ${\mathfrak W}\in {\cal M}$ and
$X,X_{1},X_{2},Y_{1},Y_{2}\subseteq W$ with
$X\cap X_{i}=X\cap Y_{i}$ for $i=1,2$, and
set $F := f^{\mathfrak W}$.
%Firstly, observe that any normal
%is monotonic, i.e. for$X_{1}\subseteq X_{2}$ and $Y_{1}
%\subseteq Y_{2}$ implies
%$$
%f^{\mathfrak W}(X_{1},Y_{1})\subseteq f^{\mathfrak W}
%(X_{2},Y_{2})
%$$
Then 
$F(X\cap X_{1},X\cap X_{2})=
F(X\cap Y_{1},X\cap Y_{2})$.
Since $F$ is normal, we know that
\begin{eqnarray*}
F(X\cap X_{1},X\cap X_{2}) &=&
F(X,X)\cap F(X,X_{2})\cap F(X_{1},X)\cap F(X_{1},X_{2}),\\
F(X\cap Y_{1},X\cap Y_{2}) &=&
F(X,X)\cap F(X,Y_{2})\cap F(Y_{1},X)\cap F(Y_{1},Y_{2}),
\end{eqnarray*}
and thus
\begin{eqnarray*}
F(X,X)\cap F(X,X_{2})\cap F(X_{1},X)\cap F(X_{1},X_{2})
=~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\\
F(X,X)\cap F(X,Y_{2})\cap F(Y_{1},X)\cap F(Y_{1},Y_{2}).
\end{eqnarray*}
Since, by normality of $F$,
\begin{eqnarray*}
F(X,X)\cap F(X,X_{2})\cap F(X_{1},X) &\supseteq& t_{f}^{\mathfrak W}(X),\\
F(X,X)\cap F(X,Y_{2})\cap F(Y_{1},X) &\supseteq& t_{f}^{\mathfrak W}(X),
\end{eqnarray*}
this implies
$t_{f}^{\mathfrak W}(X) \cap F(X_{1},X_{2})
= 
t_{f}^{\mathfrak W}(X) \cap F(Y_{1},Y_{2})$.
\end{proof}


\subsubsection{The transfer result}

Using covering normal terms, 
we can now formulate the second transfer theorem,
which is concerned with the transfer of decidability of (non-relativized)
satisfiability.
%
\begin{theorem}
  \label{transfer2}
  Let $S_1$ and $S_2$ be local ADSs having covering normal terms, and
  suppose that the satisfiability problems for $S_1$ and
  $S_2$ are decidable. Then the satisfiability problem for $S_1
  \otimes S_2$ is also decidable.              
\end{theorem}

%Note that all theorems and corollaries in this section can be generalized to
%the fusion of $n$ ADSs (instead of $2$). This is obvious for
%Theorem~\ref{transfer} since the fusion of two ADSs is again an ADS. For
%Corollary~\ref{corollary}, we may first apply Theorem~\ref{transfer} $n-1$
%times and then use an argument as in the proof of the corollary. Since, if two
%ADSs $S_1$ and $S_2$ have covering normal terms, then $S_1 \otimes, S_2$
%obviously also has covering normal terms, Theorem~\ref{transfer2} also
%generalizes to the fusion of $n$ ADSs.

As in the proof of Theorem~\ref{transfer}, 
we fix two local ADSs
$S_i = ({\cal L}_{i},{\cal M}_{i})$, $i\in \{1,2\}$, in
which ${\cal L}_{1}$ is based on the set of function symbols
$\Fmc$ and relation symbols 
$\Rmc$,
and ${\cal L}_{2}$ is based on $\Gmc$ and
$\Qmc$.
Let ${\cal L}= {\cal L}_{1} \otimes {\cal L}_{2}$ and
${\cal M}= {\cal M}_{1} \otimes {\cal M}_{2}$.                  

The proof of Theorem~\ref{transfer2} follows the same general ideas as the proof of
Theorem~\ref{transfer}. There are, however, notable differences in the
way satisfiability in $S_1 \otimes S_2$ is reduced to satisfiability
in $S_1$ and $S_2$. In Theorem~\ref{criterion} we had to 
``guess'' a set $D$ of types, and then based on this set and some additional guesses,
a pair of satisfiability problems $\Gamma_1$ and $\Gamma_2$ in $S_1$ and $S_2$, respectively,
was generated. In the proof of Theorem~\ref{transfer2}, we do not need to guess $D$.
Instead, we can compute the right set. However, this computation requires
us to solve additional satisfiability problems in the fusion $S_1 \otimes S_2$. 
Nevertheless, this yields a reduction since the alternation depth (i.e., number
of alternations between function symbols of $S_1$ and $S_2$) decreases when going from
the input set $\Gamma$ to these additional mixed satisfiability problems. 


Before we can describe this reduction in more detail, we must introduce some new notation.
In the case of relativized satisfiability, term assertions of the form
$\top\sqsubseteq \mn{sur}_{i}(\bigvee D)$ were used to assert that
all elements of the domain belong to $\mn{sur}_{i}(\bigvee D)$.
Now, we use covering normal terms to ``propagate'' $\mn{sur}_{i}(\bigvee D)$ into
terms up to a certain depth.
For a set of function symbols $E$, define the $E$-depth $d_{E}(t)$ of
a term $t$ inductively:
%
\begin{eqnarray*}
d_{E}(x_{i}) & = & 0\\
d_{E}(\neg t) & = & d_{E}(t)\\
d_{E}(t_{1}\vee t_{2}) = d_{E}(t_{1}\wedge t_{2}) & = & max\{d_{E}(t_{1}),d_{E}(t_{2})\}\\
d_{E}(f(t_{1},\ldots,t_{n})) & = & max\{d_{E}(t_{1}),\ldots,d_{E}(t_{n})\} +1\ \ \mbox{if}\ \ 
f\in E\\
d_{E}(f(t_{1},\ldots,t_{n})) & = & max\{d_{E}(t_{1}),\ldots,d_{E}(t_{n})\}\ \ \mbox{if}\ \ 
f\not\in E
\end{eqnarray*}
% 
If $\Gamma$ is a finite set of assertions, then
$$
d_E(\Gamma) := \mn{max}\{ d_E(t) \mid t\in \mn{term}(\Gamma)\}.
$$
%
Put, for a term $t(x)$ with one variable $x$, $t^{0}(x) := x$, $t^{m+1}(x)
:= t(t^{m}(x))$, $t^{\leq 0}(x) := x$, and
$t^{\leq m+1}(x) := t^{m+1}(x) \wedge t^{\leq m}(x)$.     

%Let $\Gamma$ be a set of object assertions in ${\cal L}$.
%For $i\in \{1,2\}$, denote by
%$\Sigma_{i}(\Gamma)$ the set of
%all $s\in {\cal C}^{i}(\Gamma)$ such that the term $s$ is
%satisfiable in  $({\cal L},{\cal M})$.\footnote{%
%Recall that this is the case iff %equivalent to saying that
%$\{a:s\}$ is satisfiable in $({\cal L},{\cal M})$ for an arbitrary 
%object variable $a$.}
%Since in the following the set $\Gamma$ will be fixed, 
%we will mostly write $\Sigma_{i}$ instead of
%$\Sigma_{i}(\Gamma)$.
We are now in the position to formulate the result that reduces
satisfiability in the fusion %$({\cal L},{\cal M})$.
of two local ADSs with covering normal terms to satisfiability in the
component ADSs.
 
\begin{theorem}
\label{critsecond}
Let
$S_i = ({\cal L}_{i},{\cal M}_{i})$, $i\in \{1,2\}$, be
two local ADSs having covering normal terms in
which ${\cal L}_{1}$ is based on the set of function symbols
$\Fmc$ and relation symbols $\Rmc$,
and ${\cal L}_{2}$ is based on $\Gmc$ and
$\Qmc$, and let ${\cal L}= {\cal L}_{1} \otimes {\cal L}_{2}$ and
${\cal M}= {\cal M}_{1} \otimes {\cal M}_{2}$. 
%
Let $\Gamma$ be a finite set of object assertions from ${\cal L}$.
Put $m:=d_\Fmc(\Gamma)$, $r:=d_\Gmc(\Gamma)$, and let $c(x)$ ($d(x)$) be a
covering normal term for all function symbols in $\Gamma$ that
are in $\Fmc$ ($\Gmc$).

For $i\in \{1,2\}$, denote by
$\Sigma_{i}$ the set of
all $s\in {\cal C}^{i}(\Gamma)$ such that the term $s$ is
satisfiable in  $({\cal L},{\cal M})$. %\footnote{%
%Recall that this is the case iff %equivalent to saying that
%$\{a:s\}$ is satisfiable in $({\cal L},{\cal M})$ for an arbitrary
%object variable $a$.}                      
Then the following three conditions are equivalent:
%
\begin{enumerate}
\item $\Gamma$ is satisfiable in $({\cal L},{\cal M})$.
\item There exist
\begin{itemize}
\item for every $t\in \Sigma_{1}$
      an object variable $a_{t}\not\in \mn{obj}(\Gamma)$
\item for every $a\in \mn{obj}(\Gamma)$ a term $t_{a}\in \Sigma_{1}$
      %which contains the conjunct $s$ whenever $(a:s)\in \Gamma$ and
\end{itemize}
%
such that the union $\Gamma_{1}$
of the following sets of object assertions is
satisfiable in $({\cal L}_{1},{\cal M}_{1})$:
%
\begin{itemize}
\item $\{a_{t}: \rec_{1}(t \wedge c^{\leq m}(\rec_{1}(\bigvee \Sigma_{1}))
       \mid
       t \in \Sigma_{1}\}$,
\item $\{a: \rec_{1}(t_{a} \wedge c^{\leq m}(\rec_{1}(\bigvee \Sigma_{1})) \mid
       a \in \mn{obj}(\Gamma)\}$, %\cup
       %\{ a: \rec_{1}(s) \mid (a : s) \in \Gamma\}$, 
\item $\{R(a,b) \mid R(a,b) \in \Gamma, R\in {\cal R}\}$,
\item $\{ a: \rec_{1}(s) \mid (a : s) \in \Gamma\}$;
\end{itemize}
%
and the union $\Gamma_{2}$ of the following sets of object assertions is
satisfiable in $({\cal L}_{2},{\cal M}_{2})$:
%
\begin{itemize}
\item $\{a_{t}: \rec_{2}(t \wedge d^{\leq r}
      (\rec_{2}(\bigvee \Sigma_{1})) \mid
       t \in \Sigma_{1}\}$,
\item $\{a: \rec_{2}(t_{a} \wedge d^{\leq r}(\rec_{2}(\bigvee \Sigma_{1}))
       \mid
       a \in \mn{obj}(\Gamma)\}$,
\item $\{Q(a,b) \mid Q(a,b) \in \Gamma, Q\in {\cal Q}\}$.
\end{itemize}
%
\item The same condition  as in (2) above, with $\Sigma_{1}$ replaced by $\Sigma_{2}$.
%
\end{enumerate}
% 
\end{theorem}              

The sets $\Gamma_i$ in the above theorem are very similar to the ones in
Theorem~\ref{criterion}. The main difference is that the
term assertion $\top\sqsubseteq \mn{sur}_{i}(\bigvee D)$ is no longer
there. Instead, the disjunction $\rec_{i}(\bigvee \Sigma_{1})$ is directly
``inserted'' into the terms using the covering normals terms.
As already mentioned above,
another difference is that the set $D$, which had to be guessed in
Theorem~\ref{criterion}, is replaced by the set $\Sigma_1$ in (2)
and $\Sigma_2$ in (3). Actually, guessing the set $D$ is no longer
possible in this case. In the proof of Theorem~\ref{critsecond} 
we need to know that $\top\sqsubseteq \mn{sur}_{i}(\bigvee D)$
is satisfiable in $S_i$ (i.e., holds in at least one model in $\Mmc_i$). 
But we have no way to check this effectively
since we do not have an algorithm for relativized satisfiability in $S_i$.
Taking the set $\Sigma_i$ ensures that this property is satisfied
(see the proof in the appendix for details).

By definition, $\Sigma_{i}$ % = \Sigma_{i}(\Gamma)$ 
is the set of all $s\in {\cal C}^{i}(\Gamma)$ such that the term $s$ is
satisfiable in  $({\cal L},{\cal M})$. Recall that the term $s$ is satisfiable
iff $\{a:s\}$ is satisfiable in $({\cal L},{\cal M})$ for an arbitrary
object variable $a$. Since the elements of ${\cal C}^{i}(\Gamma)$ are still
mixed terms (i.e., terms of the fusion), computing the set $\Sigma_{i}$ actually
needs a recursive call to the decision procedure for satisfiability
in $({\cal L},{\cal M})$. This recursion is well-founded since 
the alternation depth decreases. 

\begin{definition}
For a term $s$ of ${\cal L}$, denote by $a_{1}(s)$ and $a_{2}(s)$
the $1$-alternation and the $2$-alternation depth of $s$,
respectively. That is to say,
$a_{1}(s)$ is the length of the longest sequence of the form
$(g_{{1}},f_{{2}},g_{{3}},\ldots)$ such that
$$
g_{{1}}(\ldots(f_{{2}}\ldots(g_{{3}}\ldots)))
$$
with $g_{{j}}\in \Gmc$ and $f_{{j}}\in \Fmc$ appears
in $s$. The $2$-alternation depth $a_{2}(s)$ is defined by exchanging the 
roles of $\Fmc$ and $\Gmc$. Put $a(s) := a_{1}(s) + a_{2}(s)$, and call this
the \emph{alternation depth}. 
For a finite set $\Theta$ of terms, $a(\Theta)$ is the maximum of all
$a(s)$ with $s\in \Theta$.
\end{definition}

Thus, $a_1(s)$ counts the maximal number of changes between symbols from the
first and the second ADS, starting with the first symbol from $S_2$ (i.e.,
the first symbol from $S_2$ counts as a change, even if it does not occur
inside the scope of a symbol from $S_2$). The $2$-alternation depth
is defined accordingly. The alternation depth sums up the $1$- and the
$2$-alternation depth. 

\begin{lemma}
\label{terminate}
If $a({\mn term}(\Gamma)) > 0$, 
then $a(\Cmc^{1}(\Gamma)) < a({\mn term}(\Gamma))$ or 
$a(\Cmc^{2}(\Gamma)) < a({\mn term}(\Gamma))$.
\end{lemma}        
%
\begin{proof}
  We show that, if $a({\mn term}(\Gamma)) > 0$, then we have
  $a(\mn{sub}^{1}(\Gamma)) < a({\mn term}(\Gamma))$ or
  $a(\mn{sub}^{2}(\Gamma)) < a({\mn term}(\Gamma))$, which, by definition of
  $\Cmc^i$, clearly implies the lemma. First note that, by definition of 
  $\mn{sub}^i$, we have 
  \begin{equation*}
    a_i(\mn{sub}^j(\Gamma)) \leq a_i(\mn{term}(\Gamma)) \text{ for all } i,j.
  \tag{$*$}
  \end{equation*}
  We now make a case distinction as follows:
  %
  \begin{enumerate}
    
  \item $a_1({\mn term}(\Gamma)) \geq a_2({\mn term}(\Gamma))$. We want to
    show that $a_1(\mn{sub}^2(\Gamma)) < a_1({\mn term}(\Gamma))$, since, by
    ($*$), this implies $a(\mn{sub}^2(\Gamma)) < a({\mn term}(\Gamma))$.
    Assume to the contrary that $a_1(\mn{sub}^2(\Gamma)) \geq a_1({\mn
      term}(\Gamma))$. Then ($*$) implies $a_1(\mn{sub}^2(\Gamma)) = a_1({\mn
      term}(\Gamma))$. Hence, there exists a term $s \in \mn{sub}^2(\Gamma)$
    and a sequence $(g_1,f_2,g_3,\dots)$ of function symbols $g_i \in \Gmc,
    f_i \in \Fmc$ of length $a_1({\mn term}(\Gamma))$ such that
    $g_{{1}}(\ldots(f_{{2}}\ldots(g_{{3}}\ldots)))$ occurs in $s$. By
    definition of $\mn{sub}^2$, this implies the existence of a term $t \in
    \mn{term}(\Gamma)$ and a function symbol $f \in \Fmc$ such that $f (
    \ldots g_{{1}}(\ldots(f_{{2}}\ldots(g_{{3}}\ldots))))$ occurs in $t$.
    Since the length of $(g_1,f_2,g_3,\dots)$ is $a_1({\mn term}(\Gamma))$,
    this obviously yields $a_2(\mn{term}(\Gamma)) > a_1({\mn term}(\Gamma))$
    which is a contradiction.

  \item $a_1({\mn term}(\Gamma)) \leq a_2({\mn term}(\Gamma))$. Similar to the
    previous case: just exchange the roles of $a_1$ and $a_2$, \Fmc and \Gmc,
    and $\mn{sub}^1$ and $\mn{sub}^2$.
  \end{enumerate}
\vspace*{-8mm}
\end{proof}

To prove Theorem~\ref{transfer2}, we must show how Theorem~\ref{critsecond}
can be used to construct a decision procedure for satisfiability
in $S_1\otimes S_2$ from such decision procedures for the component systems
$S_1$ and $S_2$. Let us first consider the problem of computing
the sets $\Sigma_1$ and $\Sigma_2$.
%
If $a(({\mn term}(\Gamma)) = 0$, then $\Gamma$ consists of Boolean combinations
of set variables. In this case, $\Cmc^{i}(\Gamma)$ consists of set variables,
and $\Sigma_i, i = 1, 2$, can be computed using Boolean reasoning.
If $a({\mn term}(\Gamma)) > 0$, then Lemma~\ref{terminate} states that there
is an $i\in \{1, 2\}$ such that $a(\Cmc^{i}(\Gamma)) < a({\mn term}(\Gamma))$.
By induction we can thus assume that
$\Sigma_i$ can effectively be computed. 
Consequently, it remains to check Condition~($i+1$) of Theorem~\ref{critsecond}
for $i\in \{1, 2\}$. Since $\Sigma_i$ is finite, we can guess for every
object variable $a$ occurring in $\Gamma$ a type $t_a$ in $\Sigma_i$.
The sets $\Gamma_1$ and $\Gamma_2$ obtained this way are indeed sets of
assertions of $\Lmc_1$ and $\Lmc_2$, respectively. Thus, their satisfiability
can effectively be checked using the decision procedures for $S_1$ and $S_2$. 
This proves Theorem~\ref{transfer2}.

The argument used above also shows why in Theorem~\ref{critsecond} it
was not sufficient to state equivalence of (1) and (2) (as in Theorem~\ref{criterion}).
In fact, the induction argument used above does not necessarily always apply to
the computation of $\Sigma_1$. In some cases, the alternation depth may not
decreases for $\Sigma_1$, but only for $\Sigma_2$. It should be noted that
Theorem~\ref{criterion} could also have been formulated in this symmetric way.
We have not done this since it was not necessary for proving Theorem~\ref{transfer}.

Regarding the complexity of the combined decision procedure, 
we must in principle also consider the complexity of
computing covering normal terms and the size of these terms. In the examples
from DL, these terms are just value restrictions, and thus their size and the
complexity of computing them is linear. Here, we assume a polynomial bound on
both.  Under this assumption, we obtain the same complexity results as for the
case of relativized satisfiability. In fact, the complexity of testing
Condition (2) and (3) of Theorem~\ref{critsecond} agrees with the complexity
of testing Condition (2) of Theorem~\ref{criterion}: it adds one exponential
to the complexity of the decision procedure for the single ADSs.  In order to
compute $\Sigma_i$, we need exponentially many recursive calls to the
procedure.  Since the recursion depth is linear in the size of $\Gamma$, we
end up with at most exponentially many tests of Condition (2) and (3).

\begin{corollary}
  Let $S_1$ and $S_2$ be local ADSs having covering normal terms,
  and assume that these  covering normal terms can be computed in polynomial time.
  If the satisfiability problems for $S_1$ and
  $S_2$ are decidable in {\sc ExpTime} ({\sc PSpace}), then the 
  satisfiability problem for $S_1\otimes S_2$ is decidable in
  {\sc 2ExpTime} ({\sc ExpSpace}).
\end{corollary}    

With the same argument as in the case of relativized satisfiability,
we can extend the transfer result also to \emph{term} satisfiability.

\begin{corollary}
  \label{transfer2:term}
  Let $S_1$ and $S_2$ be local ADSs having covering normal terms, and
  suppose that the term satisfiability problems for $S_1$ and
  $S_2$ are decidable. Then the \emph{term} satisfiability problem for $S_1
  \otimes S_2$ is also decidable.
\end{corollary}        


\section{Fusions of description logics}

Given two DLs $L_1$ and $L_2$,  their fusion is defined as follows. We translate
them into the corresponding ADSs $S_1$ and $S_2$, and then build the fusion
$S_1\otimes S_2$. The fusion $L_1\otimes L_2$ of $L_1$ and $L_2$ is the DL that
corresponds to $S_1\otimes S_2$. Since the definition of the fusion of ADSs
requires their sets of function symbols to be disjoint, we must ensure that
the ADSs corresponding to $L_1$ and $L_2$ are built over disjoint sets of function symbols.
For the DLs introduced in Section~\ref{sect:DLs}, this can be achieved by
assuming that the sets of role names of $L_1$ and $L_2$ are disjoint and the sets
of nominals of $L_1$ and $L_2$ are disjoint. 
%
The DL $L_1\otimes L_2$ then allows the use of the concept and role constructors
of both DLs, but in a restricted way. Role descriptions are either role descriptions
of $L_1$ or of $L_2$. There are no role descriptions involving constructors or
names of both DLs. Concept descriptions may contain concept constructors of
both DLs; however, a constructor of $L_i$ may only use a role description of
$L_i$ ($i = 1, 2$).

Let us illustrate these restrictions by two simple examples.
The fusion $\ALC^+ \otimes \ALC^{-1}$ of the two DLs $\ALC^+$ and $\ALC^{-1}$ is the
fragment of $\ALC^{+,{-1}}$ whose set of role names is partitioned into two sets
$N_{R_1}$ and $N_{R_2}$ such that 
%
\begin{itemize}
\item the transitive closure operator may only be applied to names from $N_{R_1}$;
\item the inverse operator may only be applied to names from $N_{R_2}$.
\end{itemize}
%
For example, if $A$ is a concept name, $R\in N_{R_1}$ and $Q\in N_{R_2}$, then 
$\exists R^{+}.A\sqcap \forall Q^{-1}.\neg A$ is a concept description of
$\ALC^+ \otimes \ALC^{-1}$, but 
$\exists R^{+}.A\sqcap \forall R^{-1}.\neg A$ and
$\exists (Q^{-1})^{+}. A$ are not.
Note that, although the two source DLs have disjoint sets of role names, in
$\ALC^+ \otimes \ALC^{-1}$ role names from both sets may be used inside
existential and value restrictions since these concept constructors are
available in both DLs.

%The fusion $\ALCQ \otimes \ALC_f$ of the two DLs \ALCQ and $\ALC_f$
%is the fragment of $\mathcal{ALCQ}_f$ whose set of role names $N_R$ (with
%feature names $N_F \subseteq N_R$) is partitioned into two sets
%$N_{R_1}$ and $N_{R_2}$ with $N_F \subseteq N_{R_2}$ such
%that, inside qualifying number restrictions, only role names from
%$N_{R_1}$ may be used. In particular, this means that feature names
%cannot occur within qualified number restrictions.
The fusion $\ALCQ \otimes \ALC_{R^{+}}$ of the two DLs \ALCQ and $\ALC_{R^{+}}$
is the fragment of $\mathcal{ALCQ}_{R^{+}}$ whose set of role names $N_R$ (with
transitive roles $N_{R^{+}} \subseteq N_R$) is partitioned into two sets
$N_{R_1}$ and $N_{R_2}$ with $N_{R^{+}} \subseteq N_{R_2}$ such
that, inside qualifying number restrictions, only role names from
$N_{R_1}$ may be used. In particular, this means that transitive roles
cannot occur within qualified number restrictions. 

In the following, we give examples that illustrate the usefulness of the
transfer results proved in the previous section. First, we will give
an example for the case of satisfiability and then for relativized
satisfiability. Subsequently, we will consider a more complex example
involving so-called concrete domains. Here, our general transfer result
can be used to prove a decidability result that has only recently been
proved by designing a specialized algorithm for the fusion. Finally,
we will give an example that demonstrates that the restriction
to local ADSs is really necessary. 


\subsection{Decidability transfer for satisfiability}
\label{subsect:DLtransfersat}

In this subsection, we will give an example for an application of
Theorem~\ref{transfer2} where the decidability result could not be obtained
using Theorem~\ref{transfer}.

Theorem~\ref{transfer2} requires the ADSs to have covering normal terms.
This is, however, satisfied by all the DLs that yield local ADSs.
%
\begin{proposition}\label{DL:covering:nt:prop}
  Let $L$ be one of the DLs introduced in
  Section~\ref{sect:DLs}, and let the corresponding ADS $S=(\Lmc,\Mmc)$ be
  local.  Then $S$ has covering normal terms, and these terms can
  be computed in linear time.
\end{proposition}
%
\begin{proof} 
  For all function symbols $f$ in \Lmc, the term $t_f$ has the form
  $f_{\forall R}(x)$ for some role description $R$.
  The semantics of value restrictions implies that terms of this form
  satisfy the first two properties of Definition~\ref{def:covnt}. 
  This completes the proof for all function symbols $f$ of arity 0 since
  for these the third condition of Definition~\ref{def:covnt} is trivially
  satisfied. Thus, for nullary function symbols, $f_{\forall R}(x)$ for an
  arbitrary role name $R$ does the job.

  It remains to
  show that, for every unary function symbol $f\in \{f_{\exists R}, 
  f_{\forall R}, f_{\dot{\geq} n R}, f_{\dot{\leq} n R}\}$, the term 
  $f_{\forall R}(x)$ also satisfies the third property. 
  %Again, this is an easy consequence of the semantics of these concept constructors.
  This is an immediate consequence of the fact that, for these function symbols
  $f$, we have $f_{\forall R}^{\Wmf}(X)\cap f^\Wmf(Y) = f_{\forall R}^{\Wmf}(X)\cap f^\Wmf(X\cap Y)$
  for all models $\Wmf\in \Mmc$ and $X, Y\subseteq W$.
\end{proof}
%

In the following, we
consider the two description logics \ALCF and $\ALC^{+,\circ,\sqcup}$. 
\citeA{HoNu90} show that satisfiability of \ALCF-concept descriptions
is decidable. The same is true for consistency of \ALCF-ABoxes \cite{Lutz99b}.
Note, however, that relativized satisfiability of \ALCF-concept descriptions and thus
also relativized ABox consistency in \ALCF is undecidable \cite{BBNNS93}.
For $\ALC^{+,\circ,\sqcup}$, decidability of satisfiability is
shown by \citeA{Baad91} and \citeA{Schi91}.\footnote{%
Note that $\ALC^{+,\circ,\sqcup}$ is a notational variant of test-free propositional dynamic logic
(PDL)~\cite{FiLa79}.}
Decidability of ABox consistency in $\ALC^{+,\circ,\sqcup}$ %follows from the results
is shown in Chapter~7 of \cite{Degi95}.

The unrestricted combination $\ALCF^{+,\circ,\sqcup}$ of the two DLs
is undecidable. To be more precise, %the results in \cite{BBNNS93} imply that
satisfiability of $\ALCF^{+,\circ,\sqcup}$-concept descriptions (and thus also
consistency of $\ALCF^{+,\circ,\sqcup}$-ABoxes) is undecidable.
This follows from the undecidability of relativized satisfiability of \ALCF-concept descriptions
and the fact that the role operators in $\ALCF^{+,\circ,\sqcup}$ can be used
to internalize TBoxes \cite{Schi91,BBNNS93}.
In contrast to the undecidability of $\ALCF^{+,\circ,\sqcup}$, 
Theorem~\ref{transfer2} immediately implies that satisfiability
of concept descriptions in the  fusion of \ALCF and $\ALC^{+,\circ,\sqcup}$ is decidable.

\begin{theorem}
\label{fus1}
Satisfiability of concept descriptions and consistency of ABoxes is decidable
in $\mathcal{ALCF} \otimes \ALC^{+,\circ,\sqcup}$, whereas satisfiability of 
$\ALCF^{+,\circ,\sqcup}$-concept descriptions is already undecidable.
\end{theorem}
%
Taking the fusion thus yields a decidable combination of two DLs
whose unrestricted combination is undecidable. The price one has
to pay is that the fusion offers less expressivity than the unrestricted combination.
The concept $f_1 {\downarrow} f_2 \sqcap \forall
f_1^+ . C$ is an example of a concept description of $\ALCF^{+,\circ,\sqcup}$ 
that is not allowed in the fusion $\mathcal{ALCF} \otimes \ALC^{+,\circ,\sqcup}$.

\subsection{Decidability transfer for relativized satisfiability}
\label{subsect:DLtransferrelsat} 

As an example for the application of Corollary~\ref{transfer:term} (and thus of
Theorem~\ref{transfer}), we consider the 
DL $\mathcal{ALC}_f^{+,\circ,\sqcap,\sqcup}$. For this DL, satisfiability of
concept descriptions is undecidable. However, an expressive fragment with 
a decidable relativized satisfiability problem can be obtained by building the fusion 
of the two sublanguages $\mathcal{ALC}_f^{+,\circ,\sqcup}$ and
$\mathcal{ALC}^{+,\circ,\sqcup,\sqcap}$.

\begin{theorem}
  Satisfiability of $\mathcal{ALC}_f^{+,\circ,\sqcap,\sqcup}$-concept descriptions 
  is undecidable.
\end{theorem}
%
Undecidability can %easily 
be shown by a reduction of the domino problem
\cite{Berg66,Knut73} (see, e.g., \citeR{BaSa99}, for undecidability proofs of
DLs using such a reduction). The main tasks to solve in such a reduction is
that one can express the $\mathbbm{N} \times \mathbbm{N}$ grid and that one
can access all points on the grid.  One square of the grid can be expressed by
a description of the form $\exists (x \circ y \sqcap y \circ x) . \top$, where
$x, y$ are features.  In fact, this description expresses that the ``points''
belonging to it have both an $x \circ y$ and a $y \circ x$ successor, and that
these two successors coincide.  Accessing all point on the grid can then be
achieved by using the role description $(x \sqcup y)^+$.

Note that this undecidability result is also closely related to the known undecidability
of IDPDL, i.e., deterministic propositional dynamic logic with intersection
\cite{Hare84}. However, the undecidability proof for IDPDL by \citeA{Hare84}
uses the test construct, which is not available in $\mathcal{ALC}_f^{+,\circ,\sqcap,\sqcup}$.

Next, we show that relativized satisfiability in two rather expressive
sublanguages of $\mathcal{ALC}_f^{+,\circ,\sqcap,\sqcup}$ is decidable.

\begin{theorem}
  Relativized satisfiability of concept descriptions
  is decidable in 
  $\mathcal{ALC}_f^{+,\circ,\sqcup}$ and $\mathcal{ALC}^{+,\circ,\sqcup,\sqcap}$.
\end{theorem}
%
\begin{proofsketch}
In both cases, TBoxes can be internalized as described by
\citeA{Schi91} and \citeA{BBNNS93}. Thus, it is sufficient to show decidability of
(unrelativized) satisfiability.

For $\mathcal{ALC}_f^{+,\circ,\sqcup}$, this follows from decidability of
DPDL \cite{BeHP82}, the known correspondence between PDL and
$\mathcal{ALC}^{+,\circ,\sqcup}$ \cite{Schi91}, and the fact that
non-functional roles can be simulated by functional ones in the presence
of composition and transitive closure \cite{Pari80}.

For $\mathcal{ALC}^{+,\circ,\sqcup,\sqcap}$, decidability of satisfiability
follows from decidability of IPDL, i.e., PDL with intersection \cite{Dane84}.
\end{proofsketch} 

Given this theorem, Corollary~\ref{transfer:term} now yields the following decidability result.
%
\begin{corollary}
  Relativized satisfiability of concept descriptions
  is decidable in the fusion 
  $\mathcal{ALC}_f^{+,\circ,\sqcup} \otimes \mathcal{ALC}^{+,\circ,\sqcup,\sqcap}$.
\end{corollary}
%



%\begin{theorem}
%  Subsumption of $\ALC_f^\sqcap$ concepts w.r.t.\ TBoxes is decidable.
%\end{theorem}
%{\em Proof sketch:} It is easy to see that $\ALC_f^\sqcap$ concepts and TBoxes
%can be translated to $C^2$ formulae, i.e., formulae of first-order logic with
%two variables and counting. Since satisfiability of $C^2$ formulae is
%decidable \cite{Graedel-et-al-97}, subsumption of $\ALC_f^\sqcap$ concepts is
%also decidable.  \hfill\endmark
%%
%As in the previous examples, we can use fusion to define a fragment of
%$\mathcal{ALC}_f^{+,\circ,\sqcap,\sqcup}$ which contains the same set of
%constructors as the original logic and for which concept subsumption w.r.t.\ 
%TBoxes is decidable.
%%
%\begin{theorem}
%  Subsumption of $\mathcal{ALC}_f^{+,\circ,\sqcup} \otimes \ALC_f^\sqcap$
%  concepts w.r.t.\ TBoxes is decidable.
%\end{theorem}
%%
%Note that it would also be interesting to consider the fusion
%$\mathcal{ALC}_f^{+,\circ,\sqcup} \otimes
%\mathcal{ALC}^{+,\circ,\sqcup,\sqcap}$. However, it seems to be currently
%unknown whether subsumption of $\mathcal{ALC}^{+,\circ,\sqcup,\sqcap}$
%concepts (corresponds to test-free PDL with program intersection
%\cite{Harel-84}) is decidable.

\subsection{A ``concrete'' example}
\label{subsect:concdom}

Description logics with concrete domains were introduced by \citeA{BaHa91}
in order to allow for the reference to concrete objects like numbers, time intervals,
spatial regions, etc.\ when defining concepts. To be more precise, \citeA{BaHa91}
define the extension $\ALC(\Dmc)$ of $\ALC$, where $\Dmc$ is a concrete domain
(see below). Under suitable assumptions on $\Dmc$, they show that satisfiability in
$\ALC(\Dmc)$ is decidable. One of the main problems with this extension of DLs is that relativized 
satisfiability (and satisfiability in DLs where TBoxes can be internalized)
is usually undecidable \cite{BaHa92}
(though there are exceptions, see \citeR{Lutz01}).
For this reason, Haarslev et al.\ \citeyear{HaMW01} introduce a restricted way of extending
DLs by concrete domains, and show that the corresponding extension of 
$\ALCN_{\Hmc\Rmc^+}$ has a decidable relativized satisfiability problem.\footnote{%
%
To be more precise, they even show that relativized ABox consistency is decidable in
their restricted extension of $\ALCN_{\Hmc\Rmc^+}$ by concrete domains. Here, we restrict
ourself to satisfiability of concepts since the ABoxes introduced by Haarslev
et al.\ \citeyear{HaMW01}
also allow for the use of concrete individuals and for predicate assertions on these
individuals, which is not covered by the object assertions for ADSs introduced in the
present paper.}
%
In the following, we show that this result
can also be obtained as an easy consequence of our Theorem~\ref{transfer}. Moreover,
$\ALCN_{\Hmc\Rmc^+}$ can be replaced by an arbitrary local DL with a decidable relativized
satisfiability problem. 

%
\begin{definition}[Concrete Domain]
  \label{def:concrete-domain}
  A \defn{concrete domain} \Dmc is a pair $(\Delta_\Dmc,\Phi_\Dmc)$, where
  $\Delta_\Dmc$ is a nonempty set called the domain, and $\Phi_\Dmc$ is a set of
  predicate names.  Each predicate name $P \in \Phi_\Dmc$ is associated with
  an arity $n$ and an $n$-ary predicate $P^\Dmc \subseteq \Delta_\Dmc^n$. A
  concrete domain \Dmc is called \defn{admissible} iff (1) the set of its
  predicate names is closed under negation and contains a name $\top_\Dmc$ for
  $\Delta_\Dmc$, and (2) the satisfiability problem for finite conjunctions of
  predicates is decidable.
\end{definition}
%
Given a concrete domain \Dmc and one of the predicates $P \in \Phi_\Dmc$ (of arity $n$),
one can define a new concept constructor $\exists f_1, \dots, f_n . P$ (predicate restriction), 
where $f_1,\ldots, f_n$ are concrete features.\footnote{%
Note that the general framework introduced by \citeA{BaHa91} allows
for feature chains in predicate restrictions. Considering only feature chains of
length one is the main restriction introduced by \citeA{HaMW01}.
} 
In contrast to the abstract features considered
until now, concrete features are interpreted by partial functions from the
abstract domain $\Delta^\Imc$ into the concrete domain $\Delta_\Dmc$. We consider
the basic DL that allows for Boolean operators and these new concept constructors
only.

\begin{definition}[$\Bmc(\Dmc)$]
Let $N_C$ be a set of concept names and $N_{F_c}$ be a set of names for concrete features 
disjoint from $N_C$, and let \Dmc be an admissible concrete domain. 
Concepts descriptions of $\Bmc(\Dmc)$ are Boolean combinations of concept names and
\emph{predicate restrictions}, i.e., expressions of the form
$\exists f_1, \dots, f_n . P$ where $P$ is an $n$-ary predicate in $\Phi_\Dmc$
and $f_1, \ldots, f_n \in N_{F_c}$.

The semantics of $\Bmc(\Dmc)$ is defined as follows. We consider an interpretation
$\Imc$, which has a nonempty domain $\Delta^\Imc$,  and interprets concept names as subsets of
$\Delta^\Imc$ and concrete features as partial functions from $\Delta^\Imc$ into $\Delta_\Dmc$. 
The Boolean operators are interpreted as usual, and
$$
\begin{array}{r@{\ }c@{\ }l}
    (\exists f_1, \dots, f_n . P)^\Imc = \{a \in \Delta^\Imc &\mid& 
         \exists x_1,\dots,x_n \in \Delta_\Dmc .\\[.5em]
    & & f_i^\Imc(a) = x_i \text{ for all $1 \leq i \leq n$ and } (x_1,\dots,x_n) \in P^\Dmc\}.
\end{array}
$$
\end{definition}
%
Note that concept descriptions are interpreted as subsets of $\Delta^\Imc$ and
not of $\Delta^\Imc\cup \Delta_\Dmc$. Thus, if we go to the ADS corresponding
to $\Bmc(\Dmc)$,
the concrete domain is not an explicit part of the corresponding ADMs. %It is hidden in the
It is only used to define the
interpretation of the function symbols corresponding to predicate restrictions.
%
The predicate restriction constructor is translated into a function symbol
$f_{\exists f_1, \dots, f_n .  P}$ of arity 0, and, for an ADM \Wmf
corresponding to a frame \Fmf, $f^\Wmf_{\exists f_1, \dots, f_n .  P}$ is
defined as $(\exists f_1,\dots, f_n .  P)^{\Imc_\emptyset}$, where
$\Imc_\emptyset$ is the interpretation based on \Fmf that maps all concept
names to the empty set.
%
\begin{theorem}
  Let \Dmc be an admissible concrete domain. Then,
  $\Bmc(\Dmc)$ is local and the relativized satisfiability problem for $\Bmc(\Dmc)$-concept
  descriptions is decidable.
\end{theorem}
%
\begin{proof}
Given the family $(\Wmf_i)_{i\in I}$ of ADMs $\Wmf_i$ corresponding to the frames 
$\Fmf_i$ over pairwise
disjoint domains $\Delta^{\Fmf_i}$ $(i\in I)$, we first build the union $\Fmf$ of the frames:
the domain of $\Fmf$ is $\bigcup_{i\in I}\Delta^{\Fmf_i}$ and it interprets the concrete features 
in the obvious way, i.e., 
$f^\Fmf(x) := f^{\Fmf_i}(x)$ if $x\in \Delta^{\Fmf_i}$. 
%$$
%\left\{ \begin{array}{ll}f^{\Fmc_1}(x) & \mbox{if $x\in \Delta_1$},\\[.5em]
%                                     f^{\Fmc_2}(x) & \mbox{if $x\in \Delta_2$}.
%                    \end{array}\right.
%$$
Let $\Wmf$ be the ADM induced by $\Fmf$. 
%It is easy to show that $\Wmf$ is in
%fact the disjoint union of $(\Wmf_p)_{p\in P}$.
To prove that $\Wmf$ is in fact the disjoint union of $(\Wmf_i)_{i\in I}$,
it remains to show that
$f_{\exists f_1, \dots, f_n .  P}^\Wmf = \bigcup_{i\in I} f_{\exists f_1, \dots, f_n .  P}^{\Wmf_i}$.
This is an easy consequence of the semantics of the predicate restriction constructor,
the interpretation of the concrete features in $\Fmf$, 
and the fact that the domains $\Delta^{\Fmf_i}$ are pairwise disjoint.

Decidability of the unrelativized satisfiability problem is an immediate consequence
of the decidability results for $\ALC(\Dmc)$ given by \citeA{BaHa91}.
Since $\Bmc(\Dmc)$ is a very simple DL that does not contain any concept constructors
requiring the generation of abstract individuals, it is easy to see that a $\Bmc(\Dmc)$-concept
description $C_0$ is satisfiable relative to the TBox $C_1\sqsubseteq D_1,\ldots, C_n\sqsubseteq D_n$
iff it is satisfiable in a one-element interpretation. But then the TBox can be
internalized in a very simple way:
$C_0$ is satisfiable relative to the TBox $C_1\sqsubseteq D_1,\ldots, C_n\sqsubseteq D_n$
iff $C_0\sqcap (\neg C_1\sqcup D_1)\sqcap \ldots\sqcap (\neg C_n\sqcup D_n)$ is satisfiable.
\end{proof}

Given this theorem, Corollary~\ref{transfer:term} now yields the following
transfer result, which shows that concrete domains with the restricted form of
predicate restrictions introduced above can be integrated into any local DL
with a decidable relativized satisfiability problem without losing
decidability.

\begin{corollary}
Let \Dmc be an admissible concrete domain and $L$ be a local DL for which
relativized satisfiability of concept descriptions is decidable. Then,
relativized satisfiability of concept descriptions in 
$\Bmc(\Dmc)\otimes L$ is also decidable.
\end{corollary}


\subsection{Non-local DLs}
\label{sect:nominals}

By Proposition~\ref{prop:local}, DLs allowing for
nominals, the universal role, or role negation are not local. 
It follows that the decidability transfer theorems are not applicable 
to fusions of such DLs. In the following, we try to clarify the reasons
for this restricted applicability of the theorems.

First, we show that there are DLs with decidable satisfiability problem
such that their fusion has an undecidable satisfiability problem. The
culprit in this case is the universal role (or role negation).

\begin{theorem}
Satisfiability of concept descriptions is decidable in $\ALC^U$
and $\ALCF$, but undecidable in their fusion
$\ALC^U\otimes\ALCF$.
\end{theorem}

\begin{proof}
  Decidability of \ALCF was shown by \citeA{HoNu90} and of
  $\ALC^U$ by Baader et al.\ \citeyear{BBHN90} and \citeA{GoPa92}.
  Undecidability of $\ALC^U \otimes \ALCF$ (which is identical to $\ALCF^U$) 
  follows from the results by Baader et al.\ \citeyear{BBNNS93} and the %well-known 
  fact that the universal role can be used to simulate TBoxes (see
  Proposition~\ref{universal:prop}).
\end{proof}

Note that role negation can be used to simulate the universal role: just
replace $\forall U.C$ by $\forall R.C\sqcap \forall \overline{R}.C$ and
$\exists U.C$ by $\exists R.C\sqcup \exists\overline{R}.C$.  In addition,
decidability of $\ALC^{\overline{\cdot}}$ is known to be decidable
\cite{LuSa00}. Consequently, the theorem also holds if we replace
$\ALC^U$ by $\ALC^{\overline{\cdot}}$.

It should be noted that the example given in the above theorem depends on the fact
that one of the two DLs allows for the universal role and the other becomes undecidable
if the universal role is added. In fact, Corollary~\ref{corollary} shows that decidability
does transfer if both DLs already provide for the universal role.

Concerning nominals, we do not have a counterexample to the transfer of decidability
in their presence. However, we think that it is very unlikely that there can be a
general transfer result in this case. In fact, note that
for each DL $L$ without nominals introduced in Section~\ref{sect:DLs}, its fusion with 
$\ALCO$ is identical to $L$ extended with nominals. Since (relativized) satisfiability
in $\ALCO$ is decidable, a general transfer result in this case would imply that
this extension is decidable provided that $L$ is decidable. Consequently, this would
yield a general transfer result for adding nominals. 
%Though we do not know of
%a counterexample, this result would, for example, imply that the DL
%\SHIQ \cite{HoST00} extended with nominals is decidable. However, this
%an open research problem that is considered to be quite hard. 


\section{Conclusion}

Regarding related work,
the work that is most closely related to the one presented here is
\cite{Wolt98}. There, analogs of our Theorems~\ref{criterion} and~\ref{critsecond}
are proved for normal modal logics within an algebraic framework.
The present results extend the ones from \citeA{Wolt98} in two directions.
First, we have added object assertions, and thus can also prove transfer results
for ABox  reasoning. Second, we can show transfer results for satisfiability
in non-normal modal logics as long as we have covering normal terms. This
allows us to handle non-normal concept constructors like qualified number
restrictions (graded modalities) in our framework.

We also think that the introduction of abstract description systems (ADSs) is a 
contribution in its own right. ADSs abstract from the internal structure of
concept constructors and thus allow us to treat a vast range of such constructors
in a uniform way. Nevertheless, the model theoretic semantics provided by
ADSs is less abstract than the algebraic semantics employed by \citeA{Wolt98}.
It is closer to the usual semantics of DLs, and thus easier to comprehend for
people used to this semantics. The results in this paper show that ADSs in fact yield a
good level of abstraction for proving general results on description logics.
%Interestingly, the same notion also turned out to be very useful in the context of combining
%tableau algorithms for modal and description logics \cite{What?}.
Recently, the same notion has been used for
proving general results about so-called E-connections
of representation formalisms like description
logics, modal spatial logics, and temporal logics
\cite{KR-Paper}.
In contrast to fusions, in an E-connection the
two domains are not merged but connected by means
of relations.    

Regarding complexity, our transfer results yield only upper bounds. Basically,
they show that the complexity of the algorithm for the fusion is at most one exponent
higher than of the ones for the components. We believe that the complexity of satisfiability 
in the fusion of ADSs can indeed be exponentially higher than the complexity of satisfiability
in the component ADSs.
%
However, we do not yet have matching lower bounds,
i.e., we know of no example where this exponential increase in the complexity really happens.

Note that Spaan's results \citeyear{Spaa93} on the transfer of NP and {\sc
  PSpace} decidability from the component modal logics to their fusion are
restricted to normal modal logics, and that they make additional assumptions
on the algorithms used to solve the satisfiability problem in the component
logics. Nevertheless, for many {\sc PSpace}-complete description logics it is
easy to see that their fusion is also {\sc PSpace}-complete. In this sense,
the general techniques for reasoning in the fusion of descriptions logics
developed in this paper give only a rough complexity estimate.

%Anyway, from a practical point of view it may be more interesting to find good optimizations
%of the combined decision procedures. However, it is likely that such optimizations will
%also depend on additional requirements on the component algorithms: optimizations may require
%these algorithm to yield more information than just ``decidable'' or ``undecidable.''

\newpage

\appendix

\section{Proofs}

In this appendix, we give detailed proofs of 
criteria for (relativized) satisfiability in the
fusion of local ADSs. Recall that, from these criteria, the
transfer theorems for decidability easily follow.
We have deferred the proofs of these theorems to the appendix
since they are rather technical.

\subsection{Proof of Theorem~\ref{criterion}}

Before we can prove this theorem, we need a technical lemma.  In the proof of
Theorem~\ref{criterion}, we are going to merge models ${\mathfrak W}_{1}\in
{\cal M}_{1}$ and ${\mathfrak W}_{2}\in {\cal M}_{2}$ by means of a bijective
function $b$ from the domain $W_{1}$ of ${\mathfrak W}_{1}$ onto the domain
$W_{2}$ of ${\mathfrak W}_{2}$ in such a way that the surrogates $sur_{i}(t)$,
$t\in {\cal C}^{1}(\Gamma)$, are respected by $b$ in the sense that
$$
w\in sur_{1}(t)^{{\mathfrak W}_{1},{\cal A}^{1}}
\Leftrightarrow b(w)\in sur_{2}(t)^{{\mathfrak W}_{2},{\cal A}^{2}}
$$
for all $w\in W_{1}$ and $t\in {\cal C}^{1}(\Gamma)$.  The existence of
such a bijection is equivalent to the condition that the cardinalities
$|sur_{1}(t)^{{\mathfrak W}_{1},{\cal A}^{1}}|$ of $sur_{1}(t)^{{\mathfrak
    W}_{1},{\cal A}^{1}}$ and $|sur_{2}(t)^{{\mathfrak W}_{2},{\cal A}^{2}}|$
of $sur_{2}(t)^{{\mathfrak W}_{2},{\cal A}^{2}}$ coincide for all $t\in {\cal
  C}^{1}(\Gamma)$: if $t\not=t'$ for $t,t' \in \Cmc^1(\Gamma)$, then $t$
contains a conjunct which is (equivalent to) the negation of a conjunct of
$t'$; hence, for all such $t,t'$, we have $sur_{i}(t)^{{\mathfrak W}_{i},{\cal
    A}^{i}} \cap sur_{i}(t')^{{\mathfrak W}_{i},{\cal A}^{i}}=\emptyset$ for
$i \in \{1,2\}$, which clearly yields the above equivalence.  The following
lemma will be used to choose models in such a way that this cardinality
condition is satisfied.  (We refer the reader to, e.g., \citeR{Grae79} for
information about cardinals.)
%
\begin{lemma}\label{cardinality}
  Let $({\cal L},{\cal M})$ be a local ADS and $\Gamma$ a set of assertions
  satisfiable in $({\cal L},{\cal M})$.  Then there exists a cardinal $\kappa$
  such that, for all cardinals $\kappa' \geq \kappa$, there exists a model
  ${\mathfrak W} = \auf W,{\cal F}^{\mathfrak W},{\cal R}^{\mathfrak W}
  \zu\in {\cal M}$ with
  $|W|=\kappa'$ and an assignment ${\cal A}$ with $\auf {\mathfrak W},{\cal
    A}\zu\models \Gamma$ and $|s^{{\mathfrak W},{\cal A}} | \in \{0,\kappa'\}$
  for all terms $s$.
\end{lemma}
%
\begin{proof}
By assumption, there exists an ADM
${\mathfrak W}_{0} = \auf W_{0},
{\cal F}^{{\mathfrak W}_{0}},{\cal R}^{{\mathfrak W}_{0}}
\zu\in {\cal M}$
and an assignment ${\cal B}=\auf {\cal B}_{1},{\cal B}_{2}\zu$ in it 
such that $\auf {\mathfrak W}_{0},{\cal B}\zu\models \Gamma$.
Let $\kappa= \max\{\aleph_{0},|W_{0}|\}$.
We show that $\kappa$ is as required. Let $\kappa'\geq
\kappa$. Take $\kappa'$ disjoint isomorphic copies 
$\auf {\mathfrak W}_{\rho},
{\cal B}^{\rho}_{1}\zu$, ${\mathfrak W}_{\rho}=\auf W_{\rho},
{\cal F}^{{\mathfrak W}_{\rho}},{\cal R}^{{\mathfrak W}_{\rho}}\zu$,
$\rho< \kappa'$, of $\auf {\mathfrak W}_{0},{\cal B}_{1}\zu$.
(The first member of the list coincides with ${\mathfrak W}_{0}$.)
Let ${\mathfrak W}=\auf W,\Fmc^\Wmf,\Rmc^\Wmf \zu$ be the disjoint
union of the ${\mathfrak W}_{\rho}$,
$\rho<\kappa'$, and define
$\auf {\mathfrak W},{\cal A}=
\auf {\cal A}_{1},{\cal A}_{2}\zu\zu$ 
by putting ${\cal A}_{2}(a) = {\cal B}_{2}(a)$, for all $a
\in {\cal X}$, and
$$
{\cal A}_{1}(x) = \bigcup_{\rho<\kappa'} {\cal B}_{1}^{\rho}(x),
$$
for all $x \in V$.
Note that all object variables are interpreted in $W_{0}$.
It follows from the definitions of term semantics and disjoint unions
that
\begin{equation*}
s^{{\mathfrak W},{\cal A}} = \bigcup_{\rho<\kappa'} s^{{\mathfrak W}_{\rho},
{\cal B}_{\rho}},
\tag{$*$}
\end{equation*}
for all terms $s$. Hence $|W|=\kappa'$ and $\auf {\mathfrak W},{\cal
  A}\zu\models \Gamma$.  It remains to show that \mbox{$|s^{{\mathfrak
      W},{\cal A}}| \in \{0,\kappa'\}$} for every term $s$. Suppose
$|s^{{\mathfrak W},{\cal A}}|\not=0$. Then, by ($*$), $\kappa' \leq
|s^{{\mathfrak W},{\cal A}}| \leq \kappa \times \kappa'=\kappa'$, which means
$\kappa' = |s^{{\mathfrak W},{\cal A}}|$.
\end{proof}

As noted above, the disjointness of the sets $sur_{i}(t)^{{\mathfrak
    W}_{i},{\cal A}^{i}}$ and $sur_{i}(t')^{{\mathfrak W}_{i},{\cal A}^{i}}$
(for $t\not=t'$) is required in order to ensure the existence of the bijection
$b$. More precisely, in order to merge models $\Wmf_1,\Wmf_2$, the sets
$sur_{i}(t)^{{\mathfrak W}_{i},{\cal A}^{i}}$ for $t$ member of some
``relevant'' subset of $\Cmc^1(\Gamma)$ must form a partition of $\Wmf_i$'s
domain that satisfies a certain cardinality condition. This is formalized by
the following definition:
%
\begin{definition}
\label{partition}
  Let $\kappa$ be a cardinal. A set $\{X_{1},\ldots,X_{n}\}$ is called a
  $\kappa$-partition of a set $W$ iff
\begin{enumerate}
\item $|X_{i}|=\kappa$, for all $1\leq i \leq n$,
\item $X_{i}\cap X_{j} = \emptyset$ whenever $i\not=j$, and
\item $W = \bigcup_{1 \leq i \leq n} X_{i}$.
\end{enumerate}
$\{X_{1},\ldots,X_{n}\}$ is a $\kappa$-partition of
an ADM ${\mathfrak W}$ with domain $W$ iff it is a $\kappa$-partition
of~$W$.
\end{definition}
%
In the proof, we will enforce that Properties~1 and~3 hold by
appropriate constructions, while Property~2 holds by definition of ${\cal
  C}^{1}(\Gamma)$.

Before proving Theorem~\ref{criterion}, we repeat its formulation.\\
%We fix two local ADSs
%$S_i = ({\cal L}_{i},{\cal M}_{i})$, $i\in \{1,2\}$, in
%which ${\cal L}_{1}$ is based on the set of function symbols
%${\cal F}$ and relation symbols 
%${\cal R}$
%and ${\cal L}_{2}$ is based on ${\cal G}$ and
%${\cal Q}$.
%Let ${\cal L}= {\cal L}_{1} \otimes {\cal L}_{2}$ and
%${\cal M}= {\cal M}_{1} \otimes {\cal M}_{2}$.\\

%\begin{theorem} \label{criterion}
\noindent
{\bf Theorem~\ref{criterion}.\ }
{\em 
Let
$S_i = ({\cal L}_{i},{\cal M}_{i})$, $i\in \{1,2\}$, be 
two local ADSs in
which ${\cal L}_{1}$ is based on the set of function symbols
$\Fmc$ and relation symbols $\Rmc$,
and ${\cal L}_{2}$ is based on $\Gmc$ and
$\Qmc$, and let ${\cal L}= {\cal L}_{1} \otimes {\cal L}_{2}$ and
${\cal M}= {\cal M}_{1} \otimes {\cal M}_{2}$.           
If $\Gamma$ is a finite set of assertions from ${\cal L}$,
then the following are equivalent:
\begin{enumerate}
\item
$\Gamma$ is satisfiable in $({\cal L},{\cal M})$.
\item
There exist
\begin{enumerate}
\item %\label{a} 
  a set $D\subseteq {\cal C}^{1}(\Gamma)$,
\item %\label{b} 
  for every term $t\in D$ an object variable $a_{t}\not\in \mn{obj}(\Gamma)$,
\item %\label{c}
   for every $a\in \mn{obj}(\Gamma)$ a term $t_{a}\in D$,
%such that every $s$ with $(a:s)\in \Gamma$ is a conjunct of $t_{a}$,
\end{enumerate}
%
such that the union $\Gamma_{1}$ of the following sets of
assertions in $\Lmc_1$ is satisfiable in $({\cal L}_{1},{\cal M}_{1})$:
%
\begin{enumerate}
\addtocounter{enumii}{3}
\item %\label{d}
  $\{a_{t}:\mn{sur}_{1}(t) \mid t\in D\}\cup \{ \top\sqsubseteq \mn{sur}_{1}(\bigvee D)\}$,
%\item %\label{e}
%  $\{ \top\sqsubseteq \mn{sur}_{1}(\bigvee D)\}$,
\item %\label{e}
  $\{a:\mn{sur}_{1}(t_{a}) \mid a \in \mn{obj}(\Gamma)\}$,
\item %\label{f} 
  $\{R(a,b) \mid R(a,b) \in \Gamma, R\in {\cal R}\}$,
\item %\label{g}
  $\{ \mn{sur}_{1}(t_{1})\sqsubseteq \mn{sur}_{1}(t_{2}) \mid t_{1}\sqsubseteq t_{2}\in \Gamma\}
   \cup \{a:\mn{sur}_{1}(s)\mid (a:s)\in \Gamma\}$;

\end{enumerate}
%
and the union $\Gamma_{2}$ of the following sets of
assertions in $\Lmc_2$ is satisfiable in $({\cal L}_{2},{\cal M}_{2})$:
%
\begin{enumerate}
\addtocounter{enumii}{7}
\item %\label{h}
  $\{a_{t}:\mn{sur}_{2}(t) \mid t\in D\}\cup \{ \top\sqsubseteq \mn{sur}_{2}(\bigvee D)\}$,
\item %\label{i}
  $\{a:\mn{sur}_{2}(t_{a}) \mid a \in \mn{obj}(\Gamma)\}$,
\item %\label{j}
 $\{Q(a,b) \mid Q(a,b) \in \Gamma, Q\in {\cal Q}\}$.
%\cup \{a:\mn{sur}_{2}(s)\mid (a:s)\in \Gamma\}$
%\item\label{l}
%  $\{ \top\sqsubseteq \mn{sur}_{2}(\bigvee D)\}$.
\end{enumerate}
%
\end{enumerate}}
%\end{theorem}                                                  


\begin{proof}
  We start with the direction from (2) to (1).  Take a set $D\subseteq {\cal
    C}^{1}(\Gamma)$ satisfying the properties listed in the theorem.  Take
  cardinals $\kappa_{i}$, $i\in \{1,2\}$ as in Lemma~\ref{cardinality} for
  $({\cal L}_{i},{\cal M}_{i})$, put $\kappa = max\{ \kappa_{1},\kappa_{2}\}$,
  and take $\auf {\mathfrak W}_{1},{\cal A}^{1}=\auf {\cal A}_{1}^{1}, {\cal
    A}_{2}^{1}\zu\zu$ and $\auf {\mathfrak W}_{2},{\cal A}^{2}=\auf {\cal
    A}_{1}^{2}, {\cal A}_{2}^{2}\zu\zu$ with ${\mathfrak W}_i \in {\cal M}_i$
  such that $\auf {\mathfrak W}_{i},{\cal A}^{i}\zu \models \Gamma_{i}$ for
  $i\in \{1,2\}$. By Lemma~\ref{cardinality}, for $i \in \{1,2\}$ we can
  assume $|W_i|=\kappa$ and, $|\mn{sur}_i(s)^{{\mathfrak W}_i,{\cal A}^i} |
  \in \{0,\kappa\}$ for all $s \in D$.
  
  The sets $\{ \rec_{i}(s)^{{\mathfrak W}_{i},{\cal A}^{i}} : s \in D\}$ are
  $\kappa$-partitions of $W_{i}$ for $i\in \{0,1\}$ since (i) for each $s\in
  D$, we have $(a_{s}:\mn{sur}_{i}(s)) \in \Gamma_{i}$, (ii) $\auf {\mathfrak
    W}_{i},{\cal A}^{i}\zu \models \top \sqsubseteq \mn{sur}_{i}(\bigvee D) $,
  and (iii) $s,s' \in D$ and $s \neq s'$ implies $\mn{sur}_i(s)^{{\mathfrak
      W}_{i},{\cal A}^{i}} \cap \mn{sur}_i(s')^{{\mathfrak W}_{i},{\cal
      A}^{i}}$ by definition of $D$ and ${\mathcal C}^1$. Moreover,
  $\mn{obj}(\Gamma_{1})=\mn{obj}(\Gamma_{2})$ and, for all $a \in
  \mn{obj}(\Gamma_{1})$ and $s\in D$, we have ${\cal A}_{2}^{1}(a) \in
  \rec_{1}(s)^{{\mathfrak W}_{1},{\cal A}^{1}}$ iff ${\cal A}_{2}^{2}(a) \in
  \rec_{2}(s)^{{\mathfrak W}_{2},{\cal A}^{2}}$.

Together with the fact that ${\mathcal A}^1_2$ and ${\mathcal A}^2_2$ are
injective, this implies the existence of a bijection $b$ from
$W_{1}$ onto $W_{2}$ such that
$$
\{ b(w) : w \in \rec_{1}(t)^{{\mathfrak W}_{1},{\cal A}^{1}}\} = 
\rec_{2}(t)^{{\mathfrak W}_{2},{\cal A}^{2}},
$$
for all $t\in D$, and
$$
b({\cal A}_{2}^{1}(a)) = {\cal A}_{2}^{2}(a),
$$
for all $a \in \mn{obj}(\Gamma_{1})$. 
Figure~\ref{fig:bild1},
in which it is assumed that
$D = \{s_{1},\ldots,s_{k}\}$,
illustrates the mapping $b$.

\begin{figure}
  \begin{center}
    \framebox[1\textwidth]{\input{bild1.pstex_t}}
    \caption{The mapping $b$.}
    \label{fig:bild1}
  \end{center}
\end{figure}

Define a model ${\mathfrak W} = \auf W, ({\cal F}\cup
{\cal G})^{\mathfrak W}, ({\cal R} \cup {\cal Q})^{\mathfrak W}\zu 
\in {\cal M}$ by putting
\begin{itemize}
\item
$W = W_{1}$,
\item
$f^{\mathfrak W} = 
f^{{\mathfrak W}_{1}}$, for $f\in {\cal F}$,
\item
for all $g\in {\cal G}$ of arity $n$ and
all $Z_{1},\ldots,Z_{n} \subseteq W$,
$$
g^{\mathfrak W}(Z_{1},\ldots,Z_{n}) = 
b^{-1}(g^{{\mathfrak W}_{2}}(b(Z_{1}),\ldots,b(Z_{n}))),
$$
where $b(Z) = \{b(z) : z\in Z\}$,
\item $R^{\mathfrak W}=R^{{\mathfrak W}_{1}}$, for all $R\in {\cal R}$, 
\item $Q^{\mathfrak W}(x,y)$ iff 
$Q^{{\mathfrak W}_{2}}(b(x),b(y))$, for all $Q\in {\cal Q}$.
\end{itemize}
Since $\Mmc_2$ is closed under isomorphic copies, it is not hard to see
that  ${\mathfrak W}\in {\cal M}_{1}\otimes {\cal M}_{2}$.
Let ${\cal A}= {\cal A}^{1}$.
To prove the implication from (2) to (1) of the theorem it remains to show that
$\auf {\mathfrak W},{\cal A}\zu\models \Gamma$.
To this end it suffices to prove the following claim:
\\[2mm]
{\bf Claim.} For all terms $t\in \mn{sub}^{1}(\Gamma)$, we have
$$
t^{{\mathfrak W},{\cal A}} = \rec_{1}(t)^{{\mathfrak W}_{1},{\cal A}^{1}}
= b^{-1}(\rec_{2}(t)^{{\mathfrak W}_{2},{\cal A}^{2}}).
$$
%
Before we prove this claim, let us show that it implies $\auf {\mathfrak
  W},{\cal A}\zu\models \Gamma$. First note that, from the claim, we obtain
%
\begin{equation}
\label{termequality}
t^{{\mathfrak W},{\cal A}} = \rec_{1}(t)^{{\mathfrak W}_{1},{\cal A}^{1}}
\text{ for all } t\in \mn{term}(\Gamma).
\end{equation}
%
This may be proved by induction on the construction of $t\in
\mn{term}(\Gamma)$ from terms in $\mn{sub}^{1}(\Gamma)$ using the booleans and
function symbols from ${\cal L}_{1}$, only.  The basis of induction (i.e., the
equality for members of $\mn{sub}^{1}(\Gamma)$) is stated in the claim and the
induction step is straightforward.

\smallskip

We now show that $\auf {\mathfrak W},{\cal A}\zu\models \Gamma$ is a
consequence of (\ref{termequality}). Suppose $R(a,b)\in \Gamma$.  Then
$R(a,b) \in \Gamma_{1}$ and thus $\auf {\mathfrak W},{\cal A}\zu \models
R(a,b)$.  Similarly, $Q(a,b)\in \Gamma$ implies $Q(a,b)\in \Gamma_{2}$ and
$\auf {\mathfrak W},{\cal A}\zu \models Q(a,b)$.  Suppose $(a:t)\in \Gamma$.
Then $(a: \mn{sur}_{1}(t)) \in \Gamma_{1}$ and so ${\cal A}^{1}_{2}(a) \in
\rec_{1}(t)^{{\mathfrak W}_{1},{\cal A}^{1}}$ which implies, by
(\ref{termequality}), ${\cal A}_{2}^1(a) \in t^{{\mathfrak W},{\cal A}}$.
Hence $\auf {\mathfrak W},{\cal A}\zu \models (a:t)$.  If $t_{1}\sqsubseteq
t_{2}\in \Gamma$, then $\mn{sur}_{1}(t_{1}) \sqsubseteq \mn{sur}_{1}(t_{2})\in
\Gamma_{1}$ and so, by (\ref{termequality}), $t_{1}^{{\mathfrak W},{\cal
    A}}\subseteq t_{2}^{{\mathfrak W},{\cal A}}$.  Hence $\auf {\mathfrak
  W},{\cal A}\zu\models t_{1}\sqsubseteq t_{2}$.

\medskip

We come to the proof of the claim.  It is proved by induction on the
structure of~$t$. Due to the following equalities holding for all $t\in
\mn{sub}^{1}(\Gamma)$, it suffices to show that $t^{\Wmf,\Amc} =
\rec_1(t)^{\Wmf_1,\Amc^1}$.
%
\begin{eqnarray*}
\rec_{1}(t)^{{\mathfrak W}_{1},{\cal A}^{1}} 
& = & 
\bigcup \{ \rec_{1}(s)^{{\mathfrak W}_{1},{\cal A}^{1}}
 : s \in D,
t \mbox{ is a conjunct of } s \}\\
& = &
\bigcup \{ b^{-1}(\rec_{2}(s)^{{\mathfrak W}_{2},{\cal A}^{2}})
: s \in D,
t \mbox{ is a conjunct of } s \}\\
& = &
b^{-1}(\rec_{2}(t)^{{\mathfrak W}_{2},{\cal A}^{2}})
\end{eqnarray*}
%
The first equality holds since $\rec_1(\bigvee D)^{\Wmf_1,\Amc^1}=W_1$ and,
for all $s \in D$, either $t$ or $\neg t$ is a conjunct of $s$.  The second
equality is true by definition of $b$ and the validity of the third equality
can be seen analogously to the validity of the first one by considering that
$\rec_2(\bigvee D)^{{\mathfrak W}_{2},{\cal A}^{2}}=W_{2}$.
\\[2mm]
Hence let us show $t^{\Wmf,\Amc} = \rec_1(t)^{\Wmf_1,\Amc^1}$.  For the
induction start, let $t$ be a variable.  The equation $t^{\Wmf,\Amc} =
\rec_1(t)^{\Wmf_1,\Amc^1}$ is an immediate consequence of the fact that $\Amc
= \Amc^1$.  For the induction step, we distinguish several cases:
%
\begin{itemize}

\item $t=\neg t_1$. By induction hypothesis, $t_1^{\Wmf,\Amc} =
  \rec_1(t_1)^{\Wmf_1,\Amc_1}$. Hence, $t^{\Wmf,\Amc} = W \setminus
  t_1^{\Wmf,\Amc} = W \setminus \rec_1(t_1)^{\Wmf_1,\Amc^1} =
  \rec_1(t)^{\Wmf_1,\Amc^1}$ (since $W=W_1$).

\item $t=t_1 \wedge t_2$. By induction hypothesis, $t_i^{\Wmf,\Amc} =
  \rec_1(t_i)^{\Wmf_1,\Amc_1}$ for $i \in \{1,2\}$. Hence, $t^{\Wmf,\Amc}
  = t_1^{\Wmf,\Amc} \cap t_2^{\Wmf,\Amc} = \rec_1(t_1)^{\Wmf_1,\Amc^1} \cap
  \rec_1(t_2)^{\Wmf_1,\Amc^1} = \rec_1(t)^{\Wmf_1,\Amc^1}$.

\item $t=t_1 \vee t_2$. Similar to the above case.
  
\item $t=f(t_1,\dots,t_n)$. By induction hypothesis, $t_i^{\Wmf,\Amc} =
  \rec_1(t_i)^{\Wmf_1,\Amc^1}$ for $1 \leq i \leq n$.  Hence, $t^{\Wmf,\Amc} =
  f^\Wmf(t_1^{\Wmf,\Amc}, \dots, t_n^{\Wmf,\Amc}) =
  f^\Wmf(\rec_1(t_1)^{\Wmf_1,\Amc^1},\dots,\rec_1(t_n)^{\Wmf_1,\Amc^1}) =
  \rec_1(t)^{\Wmf_1,\Amc^1}$ (since $f^\Wmf = f^{\Wmf_1}$).
  
\item $t=g(t_1,\dots,t_n)$. In this case, $t^{\Wmf,\Amc} =
  b^{-1}(g^{\Wmf_2}(b(t_1^{\Wmf,\Amc}),\dots, b(t_n^{\Wmf,\Amc})))$.
  Since, by the above equalities, $\rec_1(t)^{\Wmf_1,\Amc^1} =
  b^{-1}(\rec_2(t)^{\Wmf_2,\Amc^{2}})$, it remains to show that
  $\rec_2(t)^{\Wmf_{2},\Amc^2} =
  g^{\Wmf_2}(b(t_1^{\Wmf,\Amc}),\dots,b(t_n^{\Wmf,\Amc}))$.  Since
  we have $\rec_2(t)^{\Wmf_2,\Amc^2}=g^{\Wmf_2}(\rec_2(t_1)^{\Wmf_2,\Amc^2},
  \dots,\rec_2(t_n)^{\Wmf_2,\Amc^2})$, this amounts to showing that
  $b(t_i^{\Wmf,\Amc})=\rec_2(t_i)^{\Wmf_2,\Amc^2}$ for $1 \leq i \leq n$.
  This, however, follows by induction hypothesis together with the above
  equations.
\end{itemize}
%
This concludes the proof of the direction from (2) to (1). 

\medskip
It remains to prove
the direction from (1) to (2).  
Suppose $\auf {\mathfrak W},{\cal A}\zu \models \Gamma$, for
some ${\mathfrak W}\in 
{\cal M}$ and ${\cal A} = \auf {\cal A}_1, {\cal A}_2 \zu$.
Put
$$
D = \{ s \in {\cal C}^{1}(\Gamma): s^{{\mathfrak W},{\cal A}} \not=\emptyset\}.
$$
Note that the fusion of local ADLs is a local ADL again. Hence
$({\cal L},{\cal M})$ is local
and we may assume, by Lemma~\ref{cardinality}, that the sets
$s^{{\mathfrak W},{\cal A}}$ are infinite.

Take a new object name $a_{s}\not\in \mn{obj}(\Gamma)$ for every $s\in D$
and let, for $a\in \mn{obj}(\Gamma)$,
$$
t_{a}= \bigwedge\{t\in \mn{sub}^{1}(\Gamma): {\cal A}_{2}(a)\in
t^{{\mathfrak W},{\cal A}}\}
\wedge  \bigwedge 
\{\neg t : t \in \mn{sub}^{1}(\Gamma), {\cal A}_{2}(a)\not\in
t^{{\mathfrak W},{\cal A}}\}.
$$
We prove that set of assertions
$\Gamma_{1}$ based on $D$, $t_{a}$, $a\in \mn{obj}(\Gamma)$,
and $a_{s}$, $s \in D$, is satisfiable in $({\cal L}_{1},{\cal M}_{1})$.

Let ${\cal F}^\Wmf$ denote the restriction of $({\cal F} \cup {\cal G})^\Wmf$ 
to the symbols in
${\cal F}$.  Similarly, ${\cal R}^\Wmf$ is the restriction
of $({\cal R}\cup {\cal Q})^\Wmf$ to the
symbols in ${\cal R}$.  
Set $\Wmf_1 = \auf W,{\cal F}^\Wmf,{\cal R}^\Wmf \zu \in \Mmc_1$, ${\cal
  A}^{1}=\auf {\cal A}_{1}^{1},{\cal A}_{2}^{1}\zu$, where
%
$$
\Amc_{1}^{1}
= \Amc_{1} 
\cup \{ x_t \mapsto t^{\Wmf,\Amc} : t=g(t_{1},\ldots,t_{k}) \in \mn{sub}^1(\Gamma)\},
$$
$\Amc_{2}^{1}(a) = \Amc_{2}(a)$, for $a\in \mn{obj}(\Gamma)$,
and $\Amc_{2}^{1}(a_{s}) \in s^{{\mathfrak W},{\cal A}}$,
for all $s\in D$.
Note that we can choose an injective function ${\cal A}^{1}_{2}$
because the $s^{{\mathfrak W},{\cal A}}$ are infinite.
We show by induction that
%
\begin{equation}
\label{termeq2}
\rec_1(t)^{\Wmf_1,\Amc_1}=t^{\Wmf,\Amc} \text{ for all } 
t \in \mn{term}(\Gamma).
\end{equation}
Let $t=x$ be a variable. 
Then $x$ is not a surrogate, and so
${\cal A}^{1}_{1}(x)={\cal A}_{1}(x)$.
For the induction step, we distinguish several cases:
%
\begin{itemize}

%\item $t=\neg t_1$. By induction hypothesis, $t_1^{\Wmf,\Amc} =
%  \rec_1(t_1)^{\Wmf_1,\Amc_1}$. Hence, $t^{\Wmf,\Amc} = W \setminus
%  t_1^{\Wmf,\Amc} = W \setminus \rec_1(t_1)^{\Wmf_1,\Amc^1} =
%  \rec_1(t)^{\Wmf_1,\Amc^1}$.
  
\item The inductive steps for $t=\neg t_1$, $t=t_1 \wedge t_2$, $t=t_1 \vee t_2$, and
  $t=f(t_1,\dots,t_n)$, $f\in {\cal F}$, are identical to the corresponding
  cases in the proof of Equation~\ref{termequality}, which occurs in the direction that (2)
  implies (1) above.

\item $t=g(t_1,\dots,t_n)$, where $g\in {\cal G}$.
      Then $sur_{1}(t)=x_{t}$. Hence
    ${\cal A}_{1}^{1}(x_{t})= t^{{\mathfrak W},{\cal A}}$
    and the equation is proved.
\end{itemize}
From Equation~\ref{termeq2}, we obtain 
$\auf {\mathfrak W}_{1},{\cal A}^{1}\zu
\models \Gamma_{1}$: we prove $\auf {\mathfrak W}_{1},{\cal A}^{1}\zu
\models R(a,b)$ whenever $R(a,b)\in \Gamma_{1}$
and $\auf {\mathfrak W}_{1},{\cal A}^{1}\zu\models
sur_{1}(t_{1})\sqsubseteq sur_{1}(t_{2})$ whenever
$sur_{1}(t_{1})\sqsubseteq sur_{1}(t_{2})\in \Gamma_{1}$. The remaining formulas
from $\Gamma_{1}$ are left to the reader.
Suppose $R(a,b)\in \Gamma_{1}$.
Then $R(a,b)\in \Gamma$ and so 
$\auf {\mathfrak W},{\cal A}\zu
\models R(a,b)$. Hence $\auf {\mathfrak W}_{1},{\cal A}^{1}\zu
\models R(a,b)$. 
Suppose
$sur_{1}(t_{1})\sqsubseteq sur_{1}(t_{2})\in \Gamma_{1}$.
Then $t_{1}\sqsubseteq t_{2}\in \Gamma$. Hence
$\auf {\mathfrak W},{\cal A}\zu\models t_{1}\sqsubseteq t_{2}$
which means $t_{1}^{{\mathfrak W},{\cal A}}\subseteq 
t_{2}^{{\mathfrak W},{\cal A}}$.
By Equation~\ref{termeq2}, $\mn{sur}_1(t_{1})^{{\mathfrak W}_{1},{\cal A}^{1}}
\subseteq \mn{sur}_1(t_{2})^{{\mathfrak W}_{1},{\cal A}^{1}}$
which means 
$\auf {\mathfrak W}_{1},{\cal A}^{1}\zu\models
sur_{1}(t_{1})\sqsubseteq sur_{1}(t_{2})$.

The construction of a model in ${\cal M}_{2}$ satisfying $\Gamma_{2}$
is similar and left to the reader.

\end{proof}


\subsection{Proof of Theorem~\ref{critsecond}}

As in the proof of Theorem~\ref{transfer},
we fix two local ADSs
$S_i = ({\cal L}_{i},{\cal M}_{i})$, $i\in \{1,2\}$, in
which ${\cal L}_{1}$ is based on the set of function symbols
${\cal F}$ and relation symbols 
${\cal R}$,
and ${\cal L}_{2}$ is based on 
${\cal G}$
and ${\cal Q}$.
Let ${\cal L}= {\cal L}_{1} \otimes {\cal L}_{2}$ and
${\cal M}= {\cal M}_{1} \otimes {\cal M}_{2}$.                              
We assume that $S_1$ and $S_2$ have
covering normal terms.

\smallskip

Similarly to what was done in the previous section, we will merge models by
means of bijections which map points in sets $sur_{1}(t)^{{\mathfrak
    W}_{1},{\cal A}^{1}}$ to points in the corresponding sets
$sur_{2}(t)^{{\mathfrak W}_{2},{\cal A}^{2}}$. For a finite set of object
assertions $\Gamma$ of \Lmc, let $\Sigma_{i}(\Gamma)$ denote the set of all
$s\in {\cal C}^{i}(\Gamma)$ such that the term $s$ is satisfiable in $({\cal
  L},{\cal M})$ (for $i\in \{1,2\}$). To ensure that the merging of models
succeeds, we must enforce that the elements of $\Sigma_1(\Gamma)$ and
$\Sigma_2(\Gamma)$ form $\kappa$-partitions (for some appropriate $\kappa$) of
the models to be merged. For $\Sigma_1(\Gamma)$, this is captured by the
following lemma.  Explicitly stating a dual of this lemma for
$\Sigma_2(\Gamma)$ is omitted for brevity.
\begin{lemma}
\label{partitionexists}
Let $\Gamma$ be a finite set of object assertions of \Lmc, $\kappa$ a cardinal
satisfying the conditions of Lemma~\ref{cardinality} for $({\cal L},{\cal M})$
and $\Gamma$, and $\Sigma_{1}=\Sigma_{1}(\Gamma)$.  If $\kappa'\geq \kappa$,
then
\begin{enumerate}
\item 
there exists a model ${\mathfrak W}\in {\cal M}_{1}$ 
and an assignment ${\cal A}$ such that
$$
\{ \rec_1(s)^{{\mathfrak W},{\cal A}} \mid s\in \Sigma_{1}\}
$$ 
is a $\kappa'$-partition of ${\mathfrak W}$; and

\item
there exists a model ${\mathfrak W}\in {\cal M}_{2}$ 
and an assignment ${\cal A}$ such that
$$
\{ \rec_2(s)^{{\mathfrak W},{\cal A}} \mid s\in \Sigma_{1}\}
$$ 
is a $\kappa'$-partition of ${\mathfrak W}$. 
\end{enumerate}
\end{lemma}
%
\begin{proof}
  1.  By definition of $\Sigma_{1}$, for each $s \in \Sigma_1$, we find a
  model ${\mathfrak W}_s \in \Mmc $ and an assignment $\Amc_s$
%=\auf W_s,({\cal F}\cup {\cal G})^{{\mathfrak W}_s},
%({\cal R}\cup {\cal Q})^{{\mathfrak W}_s}\zu\in {\cal M}$
  such that $s^{{\mathfrak W}_s,{\cal A}_s}\not=\emptyset$. Since the fusion
  of two local ADSs is again local, the set of models \Mmc is closed under
  disjoint unions. Hence, there exists a model $\Wmf_{\Sigma_1}$ and an
  assignment $\Amc_{\Sigma_1}$ such that $s^{{\mathfrak W}_{\Sigma_1},{\cal
      A}_{\Sigma_1}}\not=\emptyset$ for all $s\in \Sigma_{1}$. It follows that
  the set $\Gamma_1 := \{ a_s:s \mid s \in \Sigma_1 \}$ is satisfiable in
  $(\Lmc,\Mmc)$. By Lemma~\ref{cardinality}, there thus exists a model
  ${\mathfrak W}'=\auf W',({\cal F}\cup {\cal G})^{{\mathfrak W}'}, ({\cal
    R}\cup {\cal Q})^{{\mathfrak W}'}\zu\in {\cal M}$ and an assignment ${\cal
    A}'$ such that $\Wmf',\Amc' \models \Gamma_1$ and
$
\{ s^{{\mathfrak W}',{\cal A}'} \mid s \in \Sigma_{1}\}
$
is a $\kappa'$-partition of $W'$.
Now let ${\mathfrak W}$ denote the restriction of ${\mathfrak W}'$
to ${\cal L}_{1}$ and define
$$
\Amc_{1}
= \Amc_{1}' 
\cup \{ x_t \mapsto t^{\Wmf',\Amc'} \mid
t=g(t_{1},\ldots,t_{k}) \in \mn{sub}^1(\Gamma)\}.
$$
Then $\auf {\mathfrak W},{\cal A}\zu$ is as required.
To prove this note that
$\rec_1(t)^{\Wmf,\Amc}=t^{{\mathfrak W}',{\cal A}'}$
for all
\mbox{$t \in \mn{term}(\Gamma)$}.

2.\ is similar and left to the reader.
\end{proof}


We repeat the formulation of the theorem to be proved.\\

%\begin{theorem}
%\label{critsecond}
\noindent
{\bf Theorem~\ref{critsecond}.\ }
{\em 
Let
$S_i = ({\cal L}_{i},{\cal M}_{i})$, $i\in \{1,2\}$, be
two local ADSs having covering normal terms in
which ${\cal L}_{1}$ is based on the set of function symbols
$\Fmc$ and relation symbols $\Rmc$,
and ${\cal L}_{2}$ is based on $\Gmc$ and
$\Qmc$, and let ${\cal L}= {\cal L}_{1} \otimes {\cal L}_{2}$ and
${\cal M}= {\cal M}_{1} \otimes {\cal M}_{2}$. 
%
Let $\Gamma$ be a finite set of object assertions from ${\cal L}$.
Put $m:=d_F(\Gamma)$, $r:=d_G(\Gamma)$, and let $c(x)$ ($d(x)$) be a
covering normal term for all function symbols in $\Gamma$ that
are in $F$ ($G$).

For $i\in \{1,2\}$, denote by
$\Sigma_{i}$ the set of
all $s\in {\cal C}^{i}(\Gamma)$ such that the term $s$ is
satisfiable in  $({\cal L},{\cal M})$. %\footnote{%
%Recall that this is the case iff %equivalent to saying that
%$\{a:s\}$ is satisfiable in $({\cal L},{\cal M})$ for an arbitrary
%object variable $a$.}                      
Then the following three conditions are equivalent:
%
\begin{enumerate}
\item $\Gamma$ is satisfiable in $({\cal L},{\cal M})$.
\item There exist
\begin{itemize}
\item for every $t\in \Sigma_{1}$
      an object variable $a_{t}\not\in \mn{obj}(\Gamma)$
\item for every $a\in \mn{obj}(\Gamma)$ a term $t_{a}\in \Sigma_{1}$
      %which contains the conjunct $s$ whenever $(a:s)\in \Gamma$ and
\end{itemize}
%
such that the union $\Gamma_{1}$
of the following sets of object assertions is
satisfiable in $({\cal L}_{1},{\cal M}_{1})$:
%
\begin{itemize}
\item $\{a_{t}: \rec_{1}(t \wedge c^{\leq m}(\rec_{1}(\bigvee \Sigma_{1}))
       \mid
       t \in \Sigma_{1}\}$,
\item $\{a: \rec_{1}(t_{a} \wedge c^{\leq m}(\rec_{1}(\bigvee \Sigma_{1})) \mid
       a \in \mn{obj}(\Gamma)\}$, %\cup
       %\{ a: \rec_{1}(s) \mid (a : s) \in \Gamma\}$, 
\item $\{R(a,b) \mid R(a,b) \in \Gamma, R\in {\cal R}\}$,
\item $\{ a: \rec_{1}(s) \mid (a : s) \in \Gamma\}$;
\end{itemize}
%
and the union $\Gamma_{2}$ of the following sets of object assertions is
satisfiable in $({\cal L}_{2},{\cal M}_{2})$:
%
\begin{itemize}
\item $\{a_{t}: \rec_{2}(t \wedge d^{\leq r}
      (\rec_{2}(\bigvee \Sigma_{1})) \mid
       t \in \Sigma_{1}\}$,
\item $\{a: \rec_{2}(t_{a} \wedge d^{\leq r}(\rec_{2}(\bigvee \Sigma_{1}))
       \mid
       a \in \mn{obj}(\Gamma)\}$,
\item $\{Q(a,b) \mid Q(a,b) \in \Gamma, Q\in {\cal Q}\}$.
\end{itemize}
%
\item The same condition  as in (2) above, with $\Sigma_{1}$ replaced by $\Sigma_{2}$.
%
\end{enumerate}}
% 
% 
%\end{theorem}              
 
%
We start the proof with the direction from (1) to (2) and (1) to (3).  The
proofs are dual to each other, so we only give a proof for (1) $\Rightarrow$
(2). Suppose $\auf {\mathfrak W},{\cal A}\zu \models \Gamma$, where
${\mathfrak W}=\auf W,({\cal F}\cup {\cal G})^{\mathfrak W}, ({\cal R}\cup
{\cal Q})^{\mathfrak W}\zu$.  By Lemma~\ref{cardinality}, we can assume that
that, for every $t\in \Sigma_{1}$, $|t^{{\mathfrak W},{\cal A}}|$ is infinite.
Take a new object name $a_{s}\not\in \mn{obj}(\Gamma)$ for every $s\in
\Sigma_{1}$ and let, for $a\in \mn{obj}(\Gamma)$,
$$
t_{a}= \bigwedge\{t\in \mn{sub}^{1}(\Gamma): {\cal A}_{2}(a)\in
t^{{\mathfrak W},{\cal A}}\}
\wedge  \bigwedge 
\{\neg t : t \in \mn{sub}^{1}(\Gamma), {\cal A}_{2}(a)\not\in
t^{{\mathfrak W},{\cal A}}\}.
$$
We prove that the set $\Gamma_{1}$ of assertions based on $t_{a}$, $a\in
\mn{obj}(\Gamma)$, and $a_{s}$, $s \in \Sigma_{1}$, is satisfiable in $({\cal
  L}_{1},{\cal M}_{1})$ (the proof is rather similar to the proof of the
direction from (1) to (2) in the proof of Theorem~\ref{criterion}).  Let
${\cal F}^\Wmf$ (resp.\ ${\cal G}^\Wmf$) denote the restriction of $({\cal F}
\cup {\cal G})^\Wmf$ to the symbols in ${\cal F}$ (resp.\ ${\cal G}$).
Similarly, ${\cal R}^\Wmf$ and ${\cal Q}^{\Wmf}$ are the restrictions of
$({\cal R}\cup {\cal Q})^\Wmf$ to the symbols in ${\cal R}$ and ${\cal Q}$,
respectively.  Set $\Wmf_1 = \auf W,{\cal F}^\Wmf,{\cal R}^\Wmf \zu \in
\Mmc_1$, ${\cal A}^{1}=\auf {\cal A}_{1}^{1},{\cal A}_{2}^{1}\zu$, where
%
$$
\Amc_{1}^{1}
= \Amc_{1} 
\cup \{ x_t \mapsto t^{\Wmf,\Amc} \mid
t=g(t_{1},\ldots,t_{k}) \in \mn{sub}^1(\Gamma)\},
$$
$\Amc_{2}^{1}(a) = \Amc_{2}(a)$, for $a\in \mn{obj}(\Gamma)$,
and $\Amc_{2}^{1}(a_{t}) \in t^{{\mathfrak W},{\cal A}}$,
for all $t\in \Sigma_{1}$ (we can choose an injective function for 
$\Amc^1_2$ since the sets $t^{\Wmf,\Amc}$ are infinite).

As in the corresponding part of the proof of Theorem~\ref{criterion}, it can
show by induction that
%
$$
\rec_1(t)^{\Wmf_1,\Amc_1}=t^{\Wmf,\Amc} \text{ for all } 
t \in \mn{term}(\Gamma).
$$
Let us see now why
$\auf {\mathfrak W}_{1},{\cal A}^{1}\zu\models \Gamma_{1}$
follows from this equation.
For $R(a,b)\in \Gamma_{1}$ we have $R(a,b)\in \Gamma$ and
so $\auf {\mathfrak W},{\cal A}\zu\models R(a,b)$.
Hence $\auf {\mathfrak W}_{1},{\cal A}^{1}\zu\models R(a,b)$.
We have $\auf {\mathfrak W},{\cal A}\zu \models 
(\bigvee \Sigma_{1}) = \top$ (by the definition of $\Sigma_{1}$).
Hence 
$\auf {\mathfrak W}_{1},{\cal A}^{1}\zu\models
sur_{1}(\bigvee \Sigma_{1})=\top$
and so, by the definition of $c^{\leq m}$,
$\auf {\mathfrak W}_{1},{\cal A}^{1}\zu\models
(c^{\leq m}(sur_{1}(\bigvee \Sigma_{1})))=\top$.
It remains to observe that 
${\cal A}_{2}^{1}(a)\in 
sur_{1}(t_{a})^{{\mathfrak W}_{1},{\cal A}_{1}}$
for all $a\in obj(\Gamma)$,
${\cal A}_{2}^{1}(a)\in 
sur_{1}(s)^{{\mathfrak W}_{1},{\cal A}_{1}}$
whenever $(a:s)\in \Gamma$,
and 
${\cal A}_{2}^{1}(a_{t})\in 
sur_{1}(t)^{{\mathfrak W}_{1},{\cal A}_{1}}$
for all $t\in \Sigma_{1}$.

The construction of a model in ${\cal M}_{2}$ satisfying $\Gamma_{2}$
is similar and left to the reader.

\medskip

It remains to show the implications (2) $\Rightarrow$ (1) and (3)
$\Rightarrow$ (1). They are similar, so we concentrate on the first.
In the proof of Theorem~\ref{criterion} it was possible to
construct the required model for $\Gamma$ by merging 
models for $\Gamma_{1}$ and $\Gamma_{2}$.
The situation is different here. It is not possible
to merge models for $\Gamma_{1}$ and $\Gamma_{2}$ in one step,
since we do not know whether they satisfy
$sur_{1}(\bigvee \Sigma_{1})=\top$ and
$sur_{2}(\bigvee \Sigma_{1})=\top$, respectively.
We only know that they
satisfy the approximations
$a:sur_{1}(s)\wedge c^{\leq m}(sur_{1}(\bigvee \Sigma_{1}))$
and $a:sur_{2}(s)\wedge d^{\leq r}(sur_{2}(\bigvee \Sigma_{1}))$,
respectively, for $a:s\in \Gamma$.
To merge models of this type we have to
distinguish various pieces of the models and have
to add new pieces as well.
To define those pieces we need a technical claim.
As in the proof of Theorem~\ref{transfer}, take
cardinals $\kappa_{i}$, $i\in \{1,2\}$ as in Lemma~\ref{cardinality}
for $({\cal L}_{i},{\cal M}_{i})$ and put $\kappa = max\{
\kappa_{1},\kappa_{2}\}$.

\medskip 
\noindent
{\bf Claim 1}. Suppose (2) holds. 

\medskip

(a) There exist 
${\mathfrak W}_{1}=\auf W_{1},{\cal F}^{\mathfrak W},
{\cal R}^{\mathfrak W}\zu \in {\cal M}_{1}$, 
an assignment ${\cal A}=\auf {\cal A}_{1},{\cal A}_{2}\zu$ into ${\mathfrak W}_{1}$,
and a sequence $X_{0},\ldots,X_{m}$
of subsets of $W_{1}$ such that 
\begin{itemize}
\item[{[a1]}] ${\cal A}_{2}(a)\in X_{m}$,
for all $a\in \mn{obj}(\Gamma_{1})$,
\item[{[a2]}] $\auf {\mathfrak W}_{1},{\cal A}\zu \models \Gamma_{1}$,
\item[{[a3]}]
$X_{n+1} \subseteq X_{n} \cap c^{{\mathfrak W}_{1}}(X_{n})$, 
for all $0\leq n < m$,
\item[{[a4]}]
The set $\{ \rec_1(s)^{{\mathfrak W}_{1},{\cal A}} \cap X_{m}:
s\in \Sigma_{1}\}$ is a $\kappa$-partition of $X_{m}$,
\item[{[a5]}]
The sets
$$
\{ \rec_1(s)^{{\mathfrak W}_{1},{\cal A}} \cap (X_{n}-X_{n+1}) : s\in \Sigma_{1}\}
$$
are $\kappa$-partitions of $X_{n}-X_{n+1}$, for $0 \leq n < m$.
\item[{[a6]}] $|W_{1}-X_{0}| = \kappa$.
\end{itemize}

(b) There exist 
${\mathfrak W}_{2}=\auf W_{2},{\cal G}^{\mathfrak W},
{\cal Q}^{\mathfrak W}\zu \in 
{\cal M}_{2}$, an assignment ${\cal B}=\auf {\cal B}_{1},{\cal B}_{2}\zu$, 
and a sequence $Y_{0},\ldots,Y_{r}$
of subsets of $W_{2}$ such that 
\begin{itemize}
\item[{[b1]}] ${\cal B}_{2}(a)\in Y_{r}$,
for all $a\in \mn{obj}(\Gamma_{1})$,
\item[{[b2]}] $\auf {\mathfrak W}_{2},{\cal B}\zu \models \Gamma_{2}$,
\item[{[b3]}]
$Y_{n+1} \subseteq Y_{n} \cap d^{\mathfrak W_{2}}(Y_{n})$, 
for all $0\leq n < r$,
\item[{[b4]}]
The set $\{ \rec_2(s)^{{\mathfrak M},{\cal A}} \cap Y_{r}:
s\in \Sigma_{1}\}$ is a $\kappa$-partition of $Y_{r}$,
\item[{[b5]}]
The sets
$$
\{ \rec_2(s)^{{\mathfrak M},{\cal A}} \cap (Y_{n}-Y_{n+1}) : s\in \Sigma_{1}\}
$$
are $\kappa$-partitions of $Y_{n}-Y_{n+1}$, for $0 \leq n < r$.
\item[{[b6]}] $|W_{2} - Y_{0}|=\kappa$.
\end{itemize}
%
Figure~\ref{fig:bild2} illustrates the relation between the sets $X_{i}$.
(We set $A_{i}=X_{i}-X_{i+1}$ for $0\leq i < m$
and $A_{-1}= W_{1}-X_{0}$.)
%
\begin{figure}
  \begin{center}
\framebox[1\textwidth]{\input{bild2.pstex_t}}
    \caption{The sets $X_{i}$.}
    \label{fig:bild2}
  \end{center}
\end{figure}
%
Intuitively, $X_{m}$ is the set of points for which
we know that points in
$W_{1} -
sur_{1}(\bigvee \Sigma_{1})^{{\mathfrak W}_{1},{\cal A}}$
are ``very far away''. For $X_{m-1}$ they are possibly less
``far away'', for $X_{m-2}$ possibly even 
``less far'', and so on for $X_{i}$, $i<m-1$. Finally, for members of
$A_{-1}$ it is not even known whether they 
are in $sur_{1}(\bigvee \Sigma_{1})^{{\mathfrak W}_{1},{\cal A}}$ or not.
Note that all object names are interpreted in $X_{m}$.
We now come to the formal construction of the sets $X_{i}$.

\medskip

\emph{Proof of Claim~1.}
We prove (a). Part~(b) is proved similarly and left to the
reader.
By assumption and Lemma~\ref{cardinality}, 
we find an ADM ${\mathfrak W}_{a}=
\auf W_{a},F^{{\mathfrak W}_{a}},R^{{\mathfrak W}_{a}}\zu\in 
{\cal M}_{1}$ with 
$|W_{a}|=\kappa$ and an assignment 
${\cal A}^{a}=\auf {\cal A}_{1}^{a},{\cal A}_{2}^{a}\zu$
such that $\auf {\mathfrak W}_{a},{\cal A}^{a}\zu \models \Gamma_{1}$.

Let 
$$
Z_{n} = (c^{\leq n}(\rec_{1}(\bigvee 
\Sigma_{1})))^{{\mathfrak W}_{a},{\cal A}_{a}},
$$
for $0 \leq n \leq m$. 
By Lemma \ref{partitionexists} (1)
we can take for every $n$ with $-1 \leq n \leq m$ an ADM 
${\mathfrak W}_{n}=
\auf W_{n},{\cal F}^{{\mathfrak W}_{n}},{\cal R}^{{\mathfrak W}_{n}}\zu\in 
{\cal M}_{1}$ and assignments $\Amc^n$ such that
$$
\{ \rec_1(s)^{{\mathfrak W}_{n},{\cal A}^{n}} : s\in \Sigma_{1}\}
$$ 
are $\kappa$-partitions of ${\mathfrak W}_{n}$. 

Take the disjoint union ${\mathfrak W}$ (with
${\mathfrak W}= \auf W,{\cal F}^{\mathfrak W},{\cal R}^{\mathfrak W}\zu$) of the 
${\mathfrak W}_{n}$, $-1\leq n\leq m$, 
and ${\mathfrak W}_{a}$.
Define ${\cal A}=\auf {\cal A}_{1},{\cal A}_{2}\zu$ in ${\mathfrak W}$
by putting 
$$
{\cal A}_{1}(x) = 
{\cal A}^{a}_{1}(x) \cup
\bigcup_{-1 \leq i \leq m}{\cal A}^{i}_{1}(x),
$$
for all set variables $x$ and ${\cal A}_{2}(b) = {\cal A}_{2}^{a}(b)$,
for all object variables $b$.
Let, for $0 \leq n \leq m$,
$$ 
X_{n} = Z_{n} \cup
\bigcup_{n \leq i \leq m} W_{i}.  
$$
We show that $\auf \Wmf, \Amc\zu$ and the
sets $X_{n}$, $0 \leq n \leq m$, are as required.

\begin{itemize}
\item[{[a1]}] We have $\auf {\mathfrak W}_{a},{\cal A}^{a}\zu\models
\Gamma_{1}$ and so ${\cal A}_{2}(b)={\cal A}_{2}^{a}(b) \in Z_{m}$
for all $b \in obj(\Gamma_{1})$. Hence ${\cal A}_{2}(b)\in X_{m}=
Z_{m}\cup W_{m}$ for all $b\in obj(\Gamma_{1})$.
\item[{[a2]}] By the definition of disjoint unions and because
$\auf \mathfrak{W}_{a},{\cal A}^{a}\zu \models \Gamma_{1}$.
\item[{[a3]}] Firstly, we have, by the definition
of $c^{\leq n}t$ and since $c^{\mathfrak W}$ is monotone
(it distributes over intersections),
\begin{equation}
\label{eqa3}
Z_{n+1}\subseteq Z_{n}\cap c^{\mathfrak W}(Z_{n}) 
\subseteq X_{n}\cap c^{\mathfrak W}(X_{n}).
\end{equation}
Secondly, by the definition of disjoint unions,
the first property of covering normal terms,
and since $c^{\mathfrak W}$ is monotone
\begin{equation}
\label{eqa3a}
\bigcup_{n+1\leq i \leq m} W_{i}
\subseteq 
\bigcup_{n\leq i \leq m} W_{i}
\subseteq
\bigcup_{n\leq i \leq m} W_{i}
\cap c^{\mathfrak W}(\bigcup_{n\leq i \leq m} W_{i})
\subseteq
X_{n} \cap c^{\mathfrak W}X_{n}.
\end{equation}
From (\ref{eqa3}) and (\ref{eqa3a}) we obtain
\begin{equation}
X_{n+1} = Z_{n+1} \cup \bigcup_{n+1\leq i \leq m}W_{i}
\subseteq 
X_{n} \cap c^{\mathfrak W} X_{n}.
\end{equation}
\item[{[a4]}] We show that the three properties from 
Definition~\ref{partition} are satisfied. 
Since 
$$
\{
\rec_1(s)^{{\mathfrak W}_{m},{\cal A}_{m}} : s\in \Sigma_{1}\}
$$
is a
$\kappa$-partition of $W_m$, we have $|\rec_1(s)^{\Wmf_m,\Amc_m}| =
\kappa$ for all $s\in\Sigma_{1}$. This implies Property~1 since 
$\rec_1(s)^{{\mathfrak W},{\cal A}} \cap W_m = \rec_1(s)^{\Wmf_m,\Amc_m}$,
$W_m \subseteq X_m$, and $|X_{m}|\leq \kappa$.

Property~2 is an immediate consequence of the
definition of $\Sigma_1$. As for Property~3, 
we show that, for all $w \in X_m$, we have $w \in s^{\Wmf,\Amc}$ for an
$s \in \Sigma_1$. Fix a $w
\in X_m$. We distinguish two cases: firstly, assume $w \in
W_m$. Then, by the fact that $\{ \rec_1(s)^{{\mathfrak W}_{m},{\cal
A}_{m}} : s \in \Sigma_{1}\}$ is a $\kappa$-partition of $W_m$, it is
clear that there exists an $s \in \Sigma_1$ as required. Secondly,
assume $w \in Z_m = (c^{\leq m} (\rec_1(\bigvee
\Sigma_1)))^{\Wmf_a,\Amc_a}$. By definition of $c^{\leq m}t$, we have
$w \in (\rec_1(\bigvee \Sigma_1))^{\Wmf_a,\Amc_a}$
and so again $w\in \rec_{1}(s)^{{\mathfrak W},{\cal A}}$ for some $s\in
\Sigma_{1}$.
\item[{[a5]}] The proof is similar to that of Property~[a4].
\item[{[a6]}] By definition.
\end{itemize}
%
This finishes the proof of Claim~1.

\medskip

Suppose now that we have 
$$
{\mathfrak W}_{1}
=\auf W_{1},{\cal F}^{{\mathfrak W}_{1}},
{\cal R}^{{\mathfrak W}_{1}}\zu, \;{\cal A},\; 
X_{m},\ldots,X_{0} \text{ and } 
{\mathfrak W}_{2}=\auf W_{2},{\cal G}^{{\mathfrak W}_{2}},
{\cal Q}^{{\mathfrak W}_{2}}\zu, \;{\cal B},\;
Y_{r},\ldots,Y_{0}
$$
satisfying the properties listed in Claim~1.
We may assume that
$$
(W_{1}-X_{m}) \cap (W_{2}-Y_{r}) =\emptyset.
$$
Using an appropriate bijection $b$ from $X_{m}$ onto
$Y_{r}$ we may also assume that $X_{m}=Y_{r}$,
${\cal A}_{2}(a)={\cal B}_{2}(a)$
for all object variables $a\in \mn{obj}(\Gamma_{1})$,
and
\begin{equation}
\label{eqpar1}
\rec_{1}(s)^{{\mathfrak W}_{1},{\cal A}}\cap X_{m} = 
\rec_{2}(s)^{{\mathfrak W}_{2},{\cal B}}\cap X_{m}
\text{ for all } s \in \Sigma_{1}.
\end{equation}
This follows from the fact that all object variables
are mapped by ${\cal A}_{2}$ and ${\cal B}_{2}$
into $X_{m}$ and $Y_{r}$ ([a1], [b1]), respectively,
the injectivity of the mappings
${\cal A}_{2}$ and ${\cal B}_{2}$, and the conditions [a4]
and [b4] which state that
$\{ \rec_1(s)^{{\mathfrak W}_{1},{\cal A}} \cap X_{m}:
s\in \Sigma_{1}\}$ and
$\{ \rec_2(s)^{{\mathfrak W}_{2},{\cal B}} \cap Y_{r}:
s\in \Sigma_{1}\}$ both form $\kappa$-partitions of $X_{m}=Y_{r}$.
Some abbreviations are useful: set
\begin{itemize}
\item $A_{i}= X_{i}-X_{i+1}$, for $0\leq i < m$,
\item $B_{i}= Y_{i}-Y_{i+1}$, for $0 \leq i <r$,
\item $A_{-1}= W_{1}-X_{0}$, $B_{-1}= W_{2}-Y_{0}$.
\end{itemize}
So far we have merged the $X_{m}$-part of 
${\mathfrak W}_{1}$ with the $Y_{r}$-part of ${\mathfrak W}_{2}$.
It remains to take care of the sets $A_{i}$, $-1\leq i <m$,
and $B_{i}$, $-1\leq i < r$:
the sets $A_{i}$ will be merged with new models ${\mathfrak W}^{i}
\in {\cal M}_{2}$ and the sets 
$B_{i}$ will be merged with new models ${\mathfrak V}^{i}$
from ${\cal M}_{1}$. Thus, the final model will be obtained by
merging the disjoint union of ${\mathfrak W}_{1}$ and 
${\mathfrak W}^{i}$, $-1\leq i <m$ with the disjoint union
of ${\mathfrak W}_{2}$ and ${\mathfrak V}^{i}$, $-1 \leq i <r$.
Figure~\ref{fig:bild3} illustrates this merging.
In the figure, we assume that $\Sigma_{1}=\{s_{1},
\ldots,s_{k}\}$.

\begin{figure}
  \begin{center}
    \framebox[1\textwidth]{\input{bild3.pstex_t}}
    \caption{The bijection.}
    \label{fig:bild3}
  \end{center}
\end{figure}

Of course, when merging 
$A_{i}$, $i\geq 0$, with a new model ${\mathfrak W}^{i}$ we
have to respect the partition 
$$
\{sur_{1}(t)^{{\mathfrak W}_{1},{\cal A}}\cap A_{i} \mid t\in \Sigma_{1}\}
$$
of $A_{i}$. 
And when merging 
$B_{i}$, $i\geq 0$, with a new model ${\mathfrak V}^{i}$ we
have to respect the partition 
$$
\{sur_{1}(t)^{{\mathfrak W}_{1},{\cal B}}\cap B_{i} \mid t\in \Sigma_{1}\}
$$
of $B_{i}$.
Note that for $A_{-1}$ and $B_{-1}$ there is no partition to take care of.
We now proceed with the formal construction.
We find models 
${\mathfrak W}^{i}= \auf A_{i},{\cal G}^{{\mathfrak W}^{i}},
{\cal Q}^{{\mathfrak W}^{i}}\zu \in {\cal M}_{2}$
with assignments ${\cal B}^{i}=\auf {\cal B}_{1}^{i},{\cal B}_{2}^{i}\zu$,
$-1 \leq i \leq m-1$, such that, for $0 \leq i \leq m-1$,
\begin{equation}
\label{eqpar2}
\rec_{2}(s)^{{\mathfrak W}^{i},{\cal B}^{i}} = 
\rec_{1}(s)^{{\mathfrak W}_{1},{\cal A}}\cap A_{i} \text{ for all }
s \in \Sigma_{1}.
\end{equation}
This follows from [a5], [a6], and Lemma~\ref{partitionexists} (2).

We find, now using [b5], [b6],
and Lemma~\ref{partitionexists} (1), models 
${\mathfrak V}^{i}= \auf B_{i},{\cal F}^{{\mathfrak V}^{i}},
{\cal R}^{{\mathfrak V}^{i}}\zu \in {\cal M}_{1}$
with assignments ${\cal A}^{i}=\auf {\cal A}_{1}^{i},{\cal A}_{2}^{i}\zu$,
$-1 \leq i \leq r-1$, such that, for $0 \leq i \leq r-1$,
\begin{equation}
\label{eqpar3}
\rec_{1}(s)^{{\mathfrak V}^{i},{\cal A}^{i}} = 
\rec_{2}(s)^{{\mathfrak W}_{2},{\cal B}}\cap B_{i}
\text{ for all } s \in \Sigma_{1}.
\end{equation}

\medskip
Let 
$$
{\mathfrak W}_{1}'=\auf W_{1}\cup (W_{2}-Y_{r}),
{\cal F}^{{\mathfrak W}_{1}'},{\cal R}^{{\mathfrak W}_{1}'}\zu\in {\cal M}_{1}
$$
be the disjoint union of the
${\mathfrak V}^{i}$, $-1 \leq i < r$, and ${\mathfrak W}_{1}$,
and let 
$$
{\mathfrak W}_{2}'
=\auf W_{2}\cup (W_{1}-X_{m}),
{\cal G}^{{\mathfrak W}_{2}'},{\cal Q}^{{\mathfrak W}_{2}'}\zu\in {\cal M}_{2}
$$
be the disjoint union of the ${\mathfrak W}^{i}$,
$-1 \leq i < m$, and ${\mathfrak W}_{2}$.
We assume $X_{m}=Y_{r}$ and so the domain of both
ADMs is $W_{1}\cup W_{2}$.

Define a model ${\mathfrak W}=\auf W,({\cal F}\cup {\cal G})^{\mathfrak W},
({\cal R}\cup {\cal Q})^{\mathfrak W}\zu \in {\cal M}$ based on
$W = W_{1}\cup W_{2}$ by putting
\begin{itemize}
\item ${\cal R}^{\mathfrak W}= {\cal R}^{{\mathfrak W}_{1}'}$,
\item ${\cal F}^{\mathfrak W}= {\cal F}^{{\mathfrak W}_{1}'}$,
\item ${\cal Q}^{\mathfrak W}= {\cal Q}^{{\mathfrak W}_{2}'}$,
\item ${\cal G}^{\mathfrak W}= {\cal G}^{{\mathfrak W}_{2}'}$.
\end{itemize}
Define an assignment ${\cal C}=\auf {\cal C}_{1},{\cal C}_{2}\zu$ 
in ${\mathfrak W}$ by putting
\begin{itemize}
\item ${\cal C}_{2}(a) = {\cal A}_{2}(a)(={\cal B}_{2}(a))$, for all 
$a\in \mn{obj}(\Gamma_{1})$.
\item ${\cal C}_{1}(x) = {\cal A}_{1}(x) \cup \bigcup_{-1\leq i <r}
{\cal A}_{1}^{i}(x)$, for all set variables $x$
in $\mn{term}(\Gamma)$. 

Notice that ${\cal C}_{1}(x) = 
{\cal B}_{1}(x) \cup \bigcup_{-1\leq i <m}
{\cal B}_{1}^{i}(x)$, for all set variables $x\in \mn{term}(\Gamma)$. 
\item ${\cal C}_{1}(x_{t})= {\cal A}_{1}(x_{t})
\cup \bigcup_{-1\leq i <r}
{\cal A}_{1}^{i}(x_{t})$, for all $t=g(t_{1},\ldots,t_{k})
\in \mn{sub}^{1}(\Gamma)$.
\item  ${\cal C}_{1}(x_{t})= 
{\cal B}_{1}(x_{t}) \cup \bigcup_{-1\leq i <m}
{\cal B}_{1}^{i}(x_{t})$, for all $t=f(t_{1},\ldots,t_{k})\in 
\mn{sub}^{1}(\Gamma)$.
\end{itemize}
We will show that $\auf{\mathfrak W},{\cal C}\zu \models \Gamma$.
Firstly, however, we make a list of the relevant
properties of $\auf {\mathfrak W},{\cal C}\zu$:

\medskip
\noindent
{\bf Claim 2.} 
\begin{itemize}
\item[{[c1]}] ${\cal C}_{2}(a)\in X_{m}=Y_{r}$, for all $a \in \mn{obj}(\Gamma)$;
\item[{[c2]}] $\auf {\mathfrak W},{\cal C}\zu \models \Gamma_{1}\cup \Gamma_{2}$;
\item[{[c3]}] $\mn{sur}_{1}(t)^{{\mathfrak W},{\cal C}} \cap (X_{0}\cup Y_{0})
= \mn{sur}_{2}(t)^{{\mathfrak W},{\cal C}} \cap (X_{0}\cup Y_{0})$, for all 
$t\in \Sigma_{1}$;
\item[{[c4]}] $\mn{sur}_{1}(s)^{{\mathfrak W},{\cal C}} \cap (X_{0}\cup Y_{0})
= \mn{sur}_{2}(s)^{{\mathfrak W},{\cal C}} \cap (X_{0}\cup Y_{0})$, for all 
$s \in \mn{sub}^{1}(\Gamma)$;
\item[{[c5]}] $X_{n+1} \subseteq X_{n} \cap c^{\mathfrak W}(X_{n})$,
for all $0\leq n < m$;
\item[{[c6]}] $Y_{n+1} \subseteq Y_{n} \cap d^{\mathfrak W}(Y_{n})$,
for all $0\leq n <r$;
\item[{[c7]}] for all $g\in {\cal G}$ of arity $l$, $0\leq n < m$, and
all $C_{1},\ldots,C_{l}\subseteq W$:
$$
g^{\mathfrak W}(C_{1},\ldots,C_{l})
\cap X_{n} =
g^{\mathfrak W}(C_{1}\cap X_{n},\ldots,C_{l} \cap X_{n}) \cap X_n;
$$
\item[{[c8]}] 
for all $f\in {\cal F}$ of arity $l$, $0\leq n < r$, and
all $C_{1},\ldots,C_{l}\subseteq W$:
$$
f^{\mathfrak W}(C_{1},\ldots,C_{l})
\cap Y_{n} =
f^{\mathfrak W}(C_{1}\cap Y_{n},\ldots,C_{l} \cap Y_{n}) \cap Y_n. 
$$
\end{itemize}
{\em Proof of Claim 2}.
[c1] follows from [a1] and [b1] and the construction of
$\auf {\mathfrak W},{\cal C}\zu$. [c2] follows from [a2] and [b2].
[c3] follows from the construction of 
$\auf {\mathfrak W},{\cal C}\zu$ and equations (\ref{eqpar1}),
(\ref{eqpar2}), and (\ref{eqpar3}).
[c4] follows from [c3].
[c5] and [c6] follow from [a3] and [b3], respectively.
It remains to prove [c7] and [c8]. But [c7] follows from the
fact that $\auf {\mathfrak W},G^{{\mathfrak W}}\zu$ is the disjoint union
of structures based on $X_{n}$ and $W-X_{n}$, for $0 \leq n<m$,
and [c8] is dual to [c7].
Claim 2 is proved.

\medskip

We now show $\auf {\mathfrak W},{\cal C}\zu \models \Gamma$.
To this end we first show the following:

\medskip
\noindent
{\bf Claim 3.} For all $k_{1},k_{2}$ with $0 \leq k_{1} \leq m$ and
$0\leq k_{2} \leq r$ and all $s\in \mn{sub}^{1}(\Gamma)$ with $d_{F}(s)
\leq k_{1}$ and $d_{G}(s) \leq k_{2}$ we have, 
for $Z \in \{X_{k_{1}},Y_{k_{2}}\}$,
$$
Z \cap s^{{\mathfrak M},{\cal C}}
= Z \cap \mn{sur}_{1}(s)^{{\mathfrak M},{\cal C}}
= Z \cap \mn{sur}_{2}(s)^{{\mathfrak M},{\cal C}}.
$$

\medskip
\noindent
{\em Proof of Claim 3.}
By [c4] it suffices to prove the first equation.
The proof is by induction on the cardinal $k_{1}+k_{2}$.
The induction base $k_{1}=k_{2}=0$ follows 
from $\mn{sur}_{1}(s)= \mn{sur}_{2}(s)$ for $d_{F}(s)=d_{G}(s)=0$.

\medskip
Suppose the claim is proved for all $X_{k},Y_{k'}$ with 
$k\leq m$, $k'\leq r$ and $k+k'<k_{1}+k_{2}$.
We prove the claim for $X_{k_{1}},Y_{k_{2}}$.
The proof is by induction on the construction
of terms $s$ with $d_{F}(s)\leq k_{1}$
and $d_{G}(s) \leq k_{2}$. The boolean cases are trivial.

Suppose $s = f(s_{1},\ldots,s_{l})$
with $d_{F}(s)\leq k_{1}$ and $d_{G}(s)\leq k_{2}$.
We have to show the following
two statements:

\medskip
(i) 
$X_{k_{1}} \cap s^{{\mathfrak W},{\cal C}}
= X_{k_{1}} \cap \mn{sur}_{1}(s)^{{\mathfrak M},{\cal C}}$.

\medskip
(ii) 
$Y_{k_{2}} \cap s^{{\mathfrak W},{\cal C}}
= Y_{k_{2}} \cap \mn{sur}_{1}(s)^{{\mathfrak M},{\cal C}}$.

\medskip
\noindent
Consider (i) first.
The induction hypothesis yields
$$
X_{k_{1}-1} \cap s_{i}^{\Wmf, {\cal C}} = X_{k_{1}-1} \cap 
\rec_{1}(s_{i})^{\Wmf, {\cal C}}
$$
for $1 \leq i \leq l$. We have
%
\begin{eqnarray*}
X_{k_{1}-1} \cap c^{\mathfrak W}(X_{k_{1}-1}) \cap s^{\Wmf, {\cal C}}
& = &
X_{k_{1}-1} \cap c^{\mathfrak W}(X_{k_{1}-1}) \cap
f^{\mathfrak W}(s_{1}^{\Wmf, {\cal C}},\ldots,s_{l}^{\Wmf, {\cal C}})\\
& = &
X_{k_{1}-1} \cap c^{\mathfrak W}(X_{k_{1}-1}) \cap
f^{\mathfrak W}(\rec_{1}(s_{1})^{\Wmf, {\cal C}},\ldots,
\rec_{1}(s_{l})^{\Wmf, {\cal C}})\\
& = &
X_{k_{1}-1} \cap c^{\mathfrak W}(X_{k_{1}-1}) \cap
\rec_{1}(s)^{\Wmf, {\cal C}}.
\end{eqnarray*}
%
The second equation is an immediate consequence of the third property
of covering normal terms as given in Definition~\ref{def:covnt}.
Now the equation follows from [c5], i.e. $X_{k_{1}}
\subseteq X_{k_{1}-1} \cap c^{\mathfrak W}(X_{k_{1}-1})$.
(i) is proved.

\medskip

(ii)
Suppose first that $k_{2}=r$. Then $Y_{k_{2}}=X_{m}$
and the claim can be proved as above since
$X_{m}\subseteq X_{k_{1}}$ and, by induction hypothesis,
$X_{k_{1}-1} \cap s_{i}^{\Wmf, {\cal C}} = X_{k_{1}-1} \cap 
\rec_{1}(s_{i})^{\Wmf, {\cal C}}$,
for $1 \leq i \leq l$.

Assume now that $k_{2}<r$.
By induction hypothesis,
$$
Y_{k_{2}} \cap s_{i}^{\Wmf, {\cal C}} = Y_{k_{2}} 
\cap \rec_{2}(s_{i})^{\Wmf, {\cal C}},
$$
for $1 \leq i \leq l$.
Hence
$$
f^{\mathfrak W}(Y_{k_{2}} \cap s_{1}^{\Wmf, {\cal C}},\ldots,
Y_{k_{2}} \cap s_{l}^{\Wmf, {\cal C}})=
f^{\mathfrak W}(Y_{k_{2}} \cap \rec_{2}(s_{1})^{\Wmf, {\cal C}},\ldots,
Y_{k_{2}} \cap \rec_{2}(s_{l})^{\Wmf, {\cal C}}).
$$
We intersect both sides of the equation with $Y_{k_{2}}$
and derive with the help of [c8]:
$$
Y_{k_{2}} \cap
f^{\mathfrak W}(s_{1}^{\Wmf, {\cal C}},\ldots,
s_{l}^{\Wmf, {\cal C}})=
Y_{k_{2}} \cap f^{\mathfrak W}(\rec_{2}(s_{1})^{\Wmf, {\cal C}},\ldots,
\rec_{2}(s_{l})^{\Wmf, {\cal C}}).
$$
This means $Y_{k_{2}} \cap s^{\Wmf, {\cal C}} = Y_{k_{2}} 
\cap \rec_{2}(s)^{\Wmf, {\cal C}}$,
and the equation follows. 
The statements are proved.

\medskip

The case $s=g(s_{1},\ldots,s_{l})$ is dual and left to the reader.
We have proved claim 3.

\medskip

By induction (c.f.\ in the proof of Theorem~\ref{criterion} 
the proof of (\ref{termequality}) from the corresponding claim),
we obtain from Claim 3:
\begin{equation}
\label{end}
X_{m} \cap s^{\Wmf,{\cal C}} = 
X_{m} \cap \mn{sur}_{1}(s)^{{\mathfrak M},{\cal C}}
\text{ for all } s\in \mn{term}(\Gamma).
\end{equation}
Let us see how $\auf {\mathfrak W},{\cal A}\zu\models \Gamma$ 
follows from (\ref{end}).
We distinguish three cases:  
Suppose $R(a,b)\in \Gamma$.
Then $R(a,b) \in \Gamma_{1}$ and therefore
$\auf {\mathfrak W},{\cal C}\zu \models
R(a,b)$. Similarly, $Q(a,b)\in \Gamma$ implies $Q(a,b)\in \Gamma_{2}$ and
$\auf {\mathfrak W},{\cal C}\zu \models Q(a,b)$.  
Suppose $(a:t)\in \Gamma$.
Then $(a: \mn{sur}_{1}(t)) \in \Gamma_{1}$
and so, by [c2],
${\cal C}_{2}(a) \in \rec_{1}(t)^{{\mathfrak W},{\cal C}}$
which implies, by (\ref{end}),
${\cal C}_{2}(a) \in t^{{\mathfrak W},{\cal C}}$.
Hence $\auf {\mathfrak W},{\cal C}\zu \models (a:t)$.
This finishes the proof of Theorem~\ref{critsecond}.

%\newpage

\bibliography{medium-string,dl,local}

\end{document}







