%----------------------------------------------------------------------------
% Title: Coherent integration of databases by abductive logic programming.
%
% Authors: Ofer Arieli, Marc Denecker, Bert Van Nuffelen, Maurice Bruynooghe.
%
% 21.01.2003 - Submission to the Journal of AI research (JAIR).
% 30.03.2003 - JAIR rejected.
% 15.07.2003 - Re-submission to JAIR.
% 19.11.2003 - JAIR accepted.
% 05.01.2004 - Final version.
% 23.02.2004 - Camera ready version.
%----------------------------------------------------------------------------

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

%\input epsf
%\usepackage{latexsym}
%\usepackage{amssymb}
%\usepackage{theapa}

 \jairheading{21}{2004}{245--286}{07/2003}{03/2004}
 \ShortHeadings{Coherent integration of databases by abductive logic programming}
               {Arieli, Denecker, Van Nuffelen, \& Bruynooghe}
 \firstpageno{245}

%----------------------------------------------------------------------------
% LaTeX style definitions
%----------------------------------------------------------------------------

\setlength{\unitlength}{1mm}

\newtheorem{definition}{Definition}
\newtheorem{notation}{Notation}
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}{Proposition}
\newtheorem{theorem}{Theorem}
\newtheorem{corollary}{Corollary}
\newtheorem{example}{Example}
\newtheorem{note}{Note}

\newcommand{\xnot}     {{\tt not} \ }
\newcommand{\xIn}      {{\mathsf Insert}}
\newcommand{\xOut}     {{\mathsf Retract}}
\newcommand{\xif}      {:\joinrel\!- \ }
\newcommand{\xCWA}     {\mathsf{CWA}}
\newcommand{\xDB}      {({\cal D},\,{\cal IC})}
\newcommand{\DB}       {{\cal DB}}
\newcommand{\UDB}      {{\cal UDB}}
\newcommand{\asystem}  {${\cal A}$\mbox{system}}

\newcommand{\specialchar}[1]{{\cal #1}}
\newcommand{\state}{\specialchar{S}}
\newcommand{\CS}{\specialchar{CS}}
\newcommand{\cs}[1]{{\CS^{#1}}}
\newcommand{\st}[1]{{ST}_{#1}}
\newcommand{\XX}{\overline{X}}
\newcommand{\YY}{\overline{Y}}
\newcommand{\ZZ}{\overline{Z}}
\newcommand{\ttt}{\overline{t}}
\newcommand{\sss}{\overline{s}}
\newcommand{\posS}[1]{{\tt Pos}(\state_{#1})}
\newcommand{\negS}[1]{{\tt Neg}(\state_{#1})}
\newcommand{\ProcALP}{{\tt Proc}_{{\tt ALP}}}
\newcommand{\G}{\specialchar{G}}
\newcommand{\goal}[1]{{\G_{#1}}}
\newcommand{\Gm}[1]{{\G^{-}_{#1}}}
\newcommand{\OR}{{\bf OR}}
\newcommand{\SELECT}{{\bf SELECT}}

\newenvironment{enumlist}%
 {\begin{list}{}%
     {\setlength{\labelwidth}{0cm}%
      \setlength{\labelsep}{0cm}%
      \setlength{\leftmargin}{0cm}%
     }%
   }%
 {\end{list}}


%----------------------------------------------------------------------------
% The Paper
%----------------------------------------------------------------------------

\begin{document}

\title  {Coherent Integration of Databases \\
         by Abductive Logic Programming}
\author {\name Ofer Arieli \email oarieli@mta.ac.il \\
         \addr Department of Computer Science,
               The Academic College of Tel-Aviv, \\
               4 Antokolski street, Tel-Aviv 61161, Israel.
         \AND
         \name Marc Denecker \email Marc.Denecker@cs.kuleuven.ac.be \\
         \name Bert Van Nuffelen \email Bert.VanNuffelen@cs.kuleuven.ac.be \\
         \name Maurice Bruynooghe \email Maurice.Bruynooghe@cs.kuleuven.ac.be \\
         \addr Department of Computer Science,
               Katholieke Universiteit Leuven, \\
               Celestijnenlaan 200A, B-3001 Heverlee, Belgium.}
\maketitle

\begin{abstract}
  We introduce an abductive method for a coherent integration of independent
  data-sources. The idea is to compute a list of data-facts that should be
  inserted to the amalgamated database or retracted from it in order to
  restore its consistency. This method is implemented by an abductive solver,
  called ${\cal A}$\mbox{system}, that applies SLDNFA-resolution
  on a meta-theory that relates different, possibly contradicting, input
  databases. We also give a pure model-theoretic analysis of the possible
  ways to `recover' consistent data from an inconsistent database in terms of
  those models of the database that exhibit as minimal inconsistent
  information as reasonably possible. This allows us to characterize the
  `recovered databases' in terms of the `preferred' (i.e., most consistent)
  models of the theory. The outcome is an abductive-based application that
  is sound and complete with respect to a corresponding model-based,
  preferential semantics, and -- to the best of our knowledge -- is more
  expressive (thus more general) than any other implementation of coherent
  integration of databases.
\end{abstract}


\section{Introduction}
\label{section:introduction}

Complex reasoning tasks often have to integrate information that
is coming from different sources. One of the major challenges
with this respect is to compose contradicting sources of
information such that what is obtained would properly reflect the
combination of the data-sources on one hand\footnote {This
property is sometimes called {\em compositionality\/}
\cite{VDD97,VDD00}.}, and would still be {\em coherent\/} (in
terms of consistency) on the other hand. There are a number of
different issues involved in this process, the most important of
which are the following:

\begin{enumerate}
\item Unification of the different ontologies and/or database schemas,
      in order to get a fixed (global) schema, and a translation of the
      integrity constraints\footnote {I.e., the rules that represent
      intentional truths of a database domain.} of each database to the
      new ontology.

\item Unification of translated integrity constraints in a single global
      set of integrity constraints. This means, in particular, elimination
      of contradictions among the translated integrity constraints, and
      inclusion of any global integrity constraint that is imposed on the
      integration process.

\item Integration of databases w.r.t. the unified set of integrity
      constraints, computed according to the previous item.
\end{enumerate}

Each one of the issues mentioned above has its own difficulties
and challenges. For instance, the first issue is considered, e.g.,
by \citeA{Ul00} and \citeA{Le01,Le02}, where questions such as
how to express the relations between the `global database schema'
and the source (local) schemas, and how this influences query
processing with respect to the global schema \cite{BCCG02}, are
dealt with\footnote {For surveys on schema matching and related
aspects, see also \cite{BLN86} and \cite{RB01}.}. \\

The second issue above is concerned with the construction of a
single, classically consistent, set of integrity constraints,
applied on the integrated data. In database context, it is common
to assume that such a set is pre-defined, and consists of global
integrity constraints that are imposed on the integration process
itself \cite{BCCG02,Le02}. In such case there is no need to
derive these constraints from the local databases. When different
integrity constraints are specified in different local databases,
it is required to integrate not only the database instances (as
specified in issue 3 above), but also the integrity constraints
themselves (issue 2). The reason for separating these two topics
is that integrity constraints represent truths that should be
valid in all situations, while a database instance exhibits an
extensional truth, i.e., an actual situation. Consequently, the
policy of resolving contradictions among integrity constraints is
often different than the one that is applied on database facts,
and often the former is applied before the latter. \\

Despite their different nature, both issues are based on some
formalisms that maintain contradictions and allow to draw
plausible conclusions from inconsistent situations. Roughly,
there are two approaches to handle this problem:
\begin{itemize}
   \item {\em Paraconsistent\/} formalisms, in which the amalgamated data
         may remain inconsistent, but the set of conclusions implied by it
         is not explosive, i.e.: not every fact follows from an
         inconsistent database, and so the inference process does not become
         trivial in the presence of contradictions. Paraconsistent procedures
         for integrating data, like those of \citeA{Su94} and \citeA{dACM02},
         are often based on a paraconsistent reasoning systems, such as LFI
         \cite{CM01}, annotated logics \cite{Su90,KL92,ABK00}, or other
         non-classical proof procedures \cite{Pr91,AA96,Av02,CM02}\footnote
         {See also \cite{De03} for a historical perspective and some
         computational remarks on this kind of formalisms.}.
   \item {\em Coherent\/} (consistency-based) methods, in which the
         amalgamated data is revised in order to restore consistency
         \cite<see, e.g.,>{BKM91,BKMS92,BDP95,ABC99,AA99,GZ00,LS00,BS02,ADvNB04}.
         In many cases the underlying formalisms of these approaches are
         closely related to the theory of belief revision \cite{AGM95,GH95}.
         In the context of database systems the idea is to consider consistent
         databases that are `as close as possible' to the original database.
         These `repaired' instances of the `spoiled' database correspond to
         plausible and compact ways of restoring consistency.
\end{itemize}

In this paper we follow the latter approach, and consider
abductive approaches that handle the third issue above, namely:
coherent methods for integrating different data-sources (with the
same ontology) w.r.t. a consistent set of integrity
constraints\footnote {In this sense, one may view this work as a
method for restoring the consistency of a single inconsistent
database. We prefer, however, to treat it as an integration
process of multiple sources, since it also has some mediating
capabilities, such as source identification, making priorities
among different data-sources, etc. (see, e.g.,
Section~\ref{subsec:specialized_information}).}. The main
difficulty in this process stems from the fact that even when
each local database is consistent, the collective information of
all the data-sources may not remain consistent anymore. In
particular, facts that are specified in a particular database may
violate some integrity constraints defined elsewhere, and so this
data might contradict some elements in the unified set of
integrity constraints. Moreover, as noted e.g. in
\cite{Le01,CCdGL02}, the ability to handle, in a plausible way,
incomplete and inconsistent data, is an inherent property of any
system for data integration with integrity constrains, no matter
which integration phase is considered. Providing proper ways
of gaining this property is a major concern here as well.  \\

Our goal is therefore to find ways to properly `repair' a
combined (unified) database, and restore its consistency. For
this, we consider a pure declarative representation of the
composition of distributed data by a meta-theory, relating a
number of different input databases (that may contradict each
other) with a consistent output database. The underlying language
of the theory is that of abductive logic programming
\cite{KKT92,DK00}. For reasoning with such theories we use an
abductive system, called \asystem\ \cite{KvND01,vNK01}, which is
an abductive solver implementing SLDNFA-resolution
\cite{DD92,DD98}. The composing system is implemented by
abductive reasoning on the meta-theory. In the context of this
work, we have extended this system with an optimizing component
that allows us to compute preferred coherent ways to restore the
consistency of a given database. The system that is obtained
induces an {\em operational semantics\/} for database
integration. In the sequel we also consider some model-theoretic
aspects of the problem, and define a {\em preferential
semantics\/} \cite{Sh88} for it. According to this semantics, the
repaired databases are characterized in terms of the preferred
models (i.e., the most-consistent valuations) of the underlying
theory. We relate these approaches by showing that the ${\cal
A}$system is sound and complete w.r.t. the model-based semantics.
It is also noted that our framework supports reasoning with
various types of special information, such as timestamps and
source identification. Some implementation issues and experimental
results are discussed as well. \\

The rest of this paper is organized as follows: in the next
section we formally define our goal, namely: a coherent way to
integrate different data-sources. In
Section~\ref{section:model_theoretic_analysis} we set up a
semantics for this goal in terms of a corresponding model theory.
Then, in Section~\ref{section:A_system} we introduce our
abductive-based application for database integration. This is the
main section of this paper, in which we also describe how a given
integration problem can be represented in terms of meta logic
programs, show how to reason with these programs by abductive
computational models, present some experimental results, consider
proper ways of reasoning with several types of special data, and
show that our application is sound and complete with respect to
the model-based semantics, considered in
Section~\ref{section:model_theoretic_analysis}.
Section~\ref{section:related_works} contains an overview of some
related works, and in Section~\ref{section:conclusion} we conclude
with some further remarks, open issues, and future
work\footnote{This is a combined and extended version of
\cite{AvNDB01} and \cite{ADvNB02}.}.


\section{Coherent Integration of Databases}
\label{section:problem_definition}

We begin with a formal definition of our goal. In this paper we
assume that we have a first-order language $L$, based on a fixed
database schema $S$, and a fixed domain $D$. Every element of $D$
has a unique name. A {\em database instance\/} ${\cal D}$
consists of atoms in the language $L$ that are instances of the
schema $S$. As such, every instance ${\cal D}$ has a finite
active domain, which is a subset of $D$.

\begin{definition}
{\rm A {\em database\/} is a pair $\xDB$, where ${\cal D}$ is a
database instance, and ${\cal IC}$, the set of {\em integrity
constraints\/}, is a finite and classically consistent set of
formulae in $L$.
} \end{definition}

Given a database $\DB \!=\! \xDB$, we apply to it the closed word
assumption, so only  the facts that are explicitly mentioned in
${\cal D}$ are considered true. The underlying semantics
corresponds, therefore, to minimal Herbrand interpretations.

\begin{definition}
\label{min_Herbrand_model}
{\rm The {\em minimal Herbrand
model\/} ${\cal H}^{\cal D}$ of a database instance ${\cal D}$ is
the model of ${\cal D}$ that assigns true to all the ground
instances of atomic formulae in ${\cal D}$, and false to all the
other atoms.
} \end{definition}

There are different views on a database. One view is that it is a
logic theory consisting of atoms and, implicitly, the closed world
assumption (CWA) that indicates that all atoms not in the
database are false. Another common view of a database is that it
is a structure that consists of a certain domain and corresponding
relations, representing the state of the world. Whenever there is
a complete knowledge and all true atoms are represented in the
database, both views coincide: the unique Herbrand model of the
theory is the intended structure. However, in the context of
independent data-sources, the assumption that each local database
represents the state of the world is obviously false. However, we
can still view a local database as an incomplete theory, and so
treating a database as a theory rather than as a structure is more
appropriate in our case.

\begin{definition}
{\rm A formula $\psi$ {\em follows\/} from a database instance
${\cal D}$ (alternatively, ${\cal D}$ {\em entails\/} $\psi$;
notation: ${\cal D} \models \psi$) if the minimal Herbrand model
of ${\cal D}$ is also a model of $\psi$.
} \end{definition}

\begin{definition}
\label{consistent_DB}
{\rm A database $\DB \!=\! \xDB$ is {\em
consistent\/} if every formula in ${\cal IC}$ follows from ${\cal
D}$ (notation: ${\cal D} \models {\cal IC}$).
} \end{definition}

Our goal is to integrate $n$ consistent local databases, $\DB_{i}
\!=\! ({\cal D}_{i},\,{\cal IC}_{i})$ ($i \!=\! 1,\ldots n$) to
one {\em consistent\/} database that contains as much information
as possible from the local databases. The idea, therefore, is to
consider the union of the distributed data, and then to restore
its consistency in such a way that as much information as
possible will be preserved.

\begin{notation}
\label{def:udb}
 {\rm Let $\DB_{i} = ({\cal D}_{i},\,{\cal IC}_{i})$, $i = 1,\ldots
 n$, and let ${\cal I}({\cal IC}_{1},\ldots,{\cal IC}_{n})$ be a
 classically consistent set of integrity constraints. We denote:
 \[ \displaystyle \UDB = (\bigcup_{i=1}^{n}{\cal D}_{i} \, , \,
        {\cal I}({\cal IC}_{1},\ldots,{\cal IC}_{n})). \]
} \end{notation}

In the notation above, ${\cal I}$ is an operator that combines the
integrity constraints and eliminates contradictions \cite<see,
e.g.,>{ALPQ00,APPP02}. As we have already noted, how to choose
this operator and how to apply it on a specific database is
beyond the scope of this paper. In cases that the union of all
the integrity constraints is classically consistent, it makes
sense to take ${\cal I}$ as the union operator.
% The assumption that the union of the integrity constraints is
% indeed classically consistent is justified in such cases by
% the nature of the integrity constrains as describing statements
% that are widely accepted, so it is less likely that integrity
% constraints would contradict each other. Contradictions between
% the data in the different databases and integrity constraints
% are more frequent, and may occur due to many different reasons.
% The examples below show some common cases. \\
Global consistency of the integrity constraints is indeed a
common assumption in the database literature
\cite{ABC99,GZ00,GGZ01,BCCG02,KPP02,Le02}, but for the discussion
here it is possible to take, instead of the union, any operator
${\cal I}$ for consistency restoration. \\

A key notion in database integration is the following:

\begin{definition}
\label{def:repair} {\rm A {\em repair\/} of a database $\DB \!=\!
\xDB$ is a pair $(\xIn,\xOut)$, such that:
\begin{enumerate}
   \item $\xIn \cap {\cal D} \!=\! \emptyset$,
   \item $\xOut \subseteq {\cal D}$\footnote {Note that by conditions (1)
         and (2) it follows that $\xIn \cap \xOut \!=\! \emptyset$.},
   \item $({\cal D} \cup \xIn \setminus \xOut,\;{\cal IC})$ is a consistent
         database.
\end{enumerate}
} \end{definition}

Intuitively, $\xIn$ is a set of elements that should be inserted
into ${\cal D}$ and $\xOut$ is a set of elements that should be
removed from ${\cal D}$ in order to have a consistent database. \\

As noted above, repair of a given database is a key notion in many
formalisms for data integration. In the context of database
systems, this notion was first introduced by \fullciteA{ABC99},
and later considered by many others
\cite<e.g.,>{GZ00,LS00,FPLPS01,BCCG02,BS02,dACM02,ABC03,ADvNB04}.
Earlier versions of repairs and inclusion-based consistency
restoration may be traced back to \citeA{Da88} and \citeA{Wi88}.

\begin{definition}
\label{def:repairedKB}
{\rm A {\em repaired database\/} of $\DB \!=\! \xDB$ is a consistent
database of the form $({\cal D} \cup \xIn \setminus \xOut \, , \, {\cal IC})$,
where $(\xIn,\xOut)$ is a repair of $\DB$.
} \end{definition}

As there may be many ways to repair an inconsistent
database\footnote{Some repairs may be trivial and/or useless,
though. For instance, one way to eliminate the inconsistency in
$\xDB = (\{p,q,r\},\{\neg p\})$ is by deleting every element in
${\cal D}$, but this is certainly not the optimal way of restoring
consistency in this case.}, it is often convenient to make
preferences among the possible repairs, and consider only the
most preferred ones. Below are two common preference criteria for
preferring a repair $(\xIn,\xOut)$ over a repair $(\xIn',\xOut')$:

\begin{definition}
\label{preference_criteria}
{\rm Let $(\xIn,\xOut)$ and $(\xIn',\xOut')$ be two repairs of a given
database.
\begin{itemize}
   \item {\em set inclusion preference criterion \/}:
         $(\xIn',\xOut') \leq_{i} (\xIn,\xOut)$, if \\
         $\xIn \subseteq \xIn'$ and $\xOut \subseteq \xOut'$.
   \item {\em minimal cardinality preference criterion\/}: $(\xIn',\xOut')
         \leq_{c} (\xIn,\xOut)$, if \\
         $|\xIn| + |\xOut| \leq |\xIn'|+ |\xOut'|$.
\end{itemize}
} \end{definition}

Set inclusion is also considered in \cite[and
others]{ABC99,GZ00,BCCG02,BS02,dACM02,ABC03,ADvNB04}, minimal
cardinality is considered, e.g., in \cite{Da88,LS00,ABC03,ADvNB04}. \\

In what follows we assume that the preference relation $\leq$ is a
fixed pre-order that represents some preference criterion on the
set of repairs (and we shall omit subscript notations in it
whenever possible). We shall also assume that if
$(\emptyset,\emptyset)$ is a valid repair, it is the $\leq$-least
(i.e., the `best') one. This corresponds to the intuition that a
database should not be repaired unless it is inconsistent.

\begin{definition}
\label{def:preferred_repairs}
 {\rm A {\em $\leq$-preferred repair\/} of  $\DB$ is a repair
 $(\xIn,\xOut)$ of $\DB$, s.t. for every repair $(\xIn',\xOut')$ of $\DB$,
 if $(\xIn,\xOut) \!\leq\! (\xIn',\xOut')$ then $(\xIn',\xOut') \!\leq\!
 (\xIn,\xOut)$. The set of all the $\leq$-preferred repairs of $\DB$ is
 denoted by $!(\DB,\leq)$.
} \end{definition}

\begin{definition}
{\rm A {\em $\leq$-repaired database\/} of $\DB$ is a repaired
database of $\DB$, constructed from a {\em $\leq$}-preferred
repair of $\DB$. The set of all the $\leq$-repaired databases
is denoted by:
\[ {\cal R}(\DB,\leq) = \{ \, ({\cal D} \cup \xIn \setminus \xOut \, ,
                           \, {\cal IC}) ~|~ (\xIn,\xOut) \in \ !(\DB,\leq)
                          \, \}. \]
} \end{definition}

Note that if $\DB$ is consistent and $\leq$ is a preference
relation, then $\DB$ is the only $\leq$-repaired database of
itself (thus, there is nothing to repair in this case, as
expected).

\begin{note}
{\rm It is usual to refer to the $\leq$-preferred databases of
$\DB$ as the consistent databases that are `as close as possible'
to $\DB$ itself \fullcite<see,
e.g.,>{ABC99,LS00,dACM02,KPP02,ABC03,ADvNB04}. Indeed, let
\[ {\tt dist}({\cal D}_{1},{\cal D}_{2}) =
        ({\cal D}_{1} \setminus {\cal D}_{2}) \cup
        ({\cal D}_{2} \setminus {\cal D}_{1}).
\]
It is easy to see that $\DB' = ({\cal D}',{\cal IC})$ is a
$\leq_{i}$-repaired database of $\DB = \xDB$, if the set
${\tt dist}({\cal D}',{\cal D})$ is minimal (w.r.t. set
inclusion) among all the sets of the form ${\tt dist}({\cal
D}'',{\cal D})$, where ${\cal D}'' \models {\cal IC}$. Similarly,
if $|S|$ denotes the size of $S$, then $\DB' = ({\cal D}',{\cal
IC})$ is a $\leq_{c}$-repaired database of $\DB = \xDB$, if
$|{\tt dist}({\cal D}',{\cal D})| = \min \{ |{\tt dist}({\cal
D}'',{\cal D})| ~|~ {\cal D}'' \models {\cal IC} \}$.  }
\end{note}

Given $n$ databases and a preference criterion $\leq$, our goal is
therefore to compute the set ${\cal R}(\UDB,\leq)$ of the
$\leq$-repaired databases of the unified database, $\UDB$
(Notation~\ref{def:udb}). The reasoner may use different
strategies to determine the consequences of this set. Among the
common approaches are the skeptical (conservative) one, that it
is based on a `consensus' among all the elements of ${\cal
R}(\UDB,\leq)$ \cite<see>{ABC99,GZ00}, a `credulous' approach, in
which entailments are determined by any element in ${\cal
R}(\UDB,\leq)$, an approach that is based on a `majority vote'
\cite{LM98,KPP02}, etc. In cases where processing time is a major
consideration, one may want to speed-up the computations by
considering {\em any\/} repaired database. In such cases it is
sufficient to find an arbitrary element in the set ${\cal R}(\UDB,\leq)$. \\

Below are some examples\footnote{See, e.g., \cite{ABC99,GZ00,BS02}
for further discussions on these examples.} of the integration
process\footnote{In all the following examples we use set
inclusion as the preference criterion, and take the operator
${\cal I}$ that combines integrity constraints (see Notation
\ref{def:udb}) to be the union operator.}.

\begin{example}
\label{example:teachers}
 {\rm Consider a relation $teaches$ of the schema
 $({\tt course\_name},{\tt teacher\_name})$, and an integrity
 constraint, stating that the same course cannot be taught by two
 different teachers: \vspace{1mm} \\
 \hspace*{18mm}
 ${\cal IC} = \{ \,
   \forall X \forall Y \forall Z \,
   (teaches(X,Y) \wedge teaches(X,Z) \, \rightarrow \,
   Y = Z ) \, \}$.
 \vspace{1mm} \\
Consider now the following two databases:
 \vspace{2mm} \\
 \hspace*{18mm}
 $\DB_{1} = ( \, \{teaches(c_{1},n_{1}), \:
                   teaches(c_{2},n_{2})\}, \, {\cal IC} \,)$, \vspace{1mm} \\
 \hspace*{18mm}
 $\DB_{2} = ( \, \{teaches(c_{2},n_{3})\}, \, {\cal IC})$. \vspace{1mm} \\
 Clearly, the unified database $\DB_{1} \cup \DB_{2}$ is inconsistent.
 It has two preferred repairs, which are
 $(\emptyset, \,\{teaches(c_{2},n_{3})\})$ and
 $(\emptyset, \,\{teaches(c_{2},n_{2})\})$.
 The corresponding repaired databases are the following: \vspace{1mm} \\
 \hspace*{18mm}
 ${\cal R}_{1} = ( \, \{teaches(c_{1},n_{1}), \: teaches(c_{2},n_{2})\},
                   \, {\cal IC} \, )$, \vspace{1mm} \\
 \hspace*{18mm}
 ${\cal R}_{2} = ( \, \{teaches(c_{1},n_{1}), \: teaches(c_{2},n_{3})\},
                   \, {\cal IC} \, )$. \vspace{1mm} \\
Thus, e.g., $teaches(c_{1},n_{1})$ is true both in the conservative
approach and the credulous approach to database integration, while
the conclusion $teaches(c_{2},n_{2})$ is supported only by credulous
reasoning.
} \end{example}

\begin{example}
\label{example:suppliers}
{\rm Consider databases with relations $class$ and $supply$,
 of schemas $({\tt item},{\tt type})$ and
 $({\tt supplier},{\tt department}, {\tt item})$, respectively.
 Let \vspace{2mm} \\
 \hspace*{18mm}
 $\DB_{1} = (\{ supply(c_{1},d_{1},i_{1}), \: class(i_{1},t_{1}) \}, \,
                {\cal IC})$, \vspace{1mm} \\
 \hspace*{18mm}
 $\DB_{2} = (\{ supply(c_{2},d_{2},i_{2}), \: class(i_{2},t_{1}) \}, \,
                \emptyset)$,
 \vspace{2mm} \\
 where ${\cal IC} = \{ \, \forall X \forall Y \forall Z \,
 (supply(X,Y,Z) \wedge class(Z,t_{1}) \rightarrow X = c_{1} ) \,\}$
 states that only supplier $c_{1}$ can supply items of type $t_{1}$.
 Again, $\DB_{1} \cup \DB_{2}$ is inconsistent, and has two preferred repairs:
 $(\emptyset, \,\{supply(c_{2},d_{2},i_{2})\})$ and $(\emptyset,
 \,\{class(i_{2},t_{1})\})$. It follows that there are two repairs
 of this database: \vspace{1mm} \\
 \hspace*{18mm} ${\cal R}_{1} =
               ( \, \{ supply(c_{1},d_{1},i_{1}), \: class(i_{1},t_{1}), \:
                       class(i_{2},t_{1}) \}, \, {\cal IC} \, )$,
               \vspace{1mm} \\
 \hspace*{18mm} ${\cal R}_{2} =
               ( \, \{ supply(c_{1},d_{1},i_{1}), \: supply(c_{2},d_{2},i_{2}),
                 \: class(i_{1},t_{1}) \}, \, {\cal IC} \, )$.
} \end{example}

\begin{example}
\label{example:set_inclusion}
{\rm Let ${\cal D}_{1} \!=\! \{p(a),
 \: p(b)\}, {\cal D}_{2} \!=\! \{q(a), \: q(c)\}$, and ${\cal IC}
 \!=\! \{ \forall X (p(X) \!\rightarrow\! q(X)) \}$. Again,
 $({\cal D}_{1}, \emptyset) \cup ({\cal D}_{2}, {\cal IC})$ is
 inconsistent. The corresponding preferred repairs are $(\{q(b)\},
 \,\emptyset)$ and $(\emptyset, \,\{p(b)\})$.
 Thus, the repaired databases are the following: \vspace{1mm} \\
 \hspace*{18mm} ${\cal R}_{1} = ( \, \{p(a), \: p(b), \: q(a), \: q(b),
                   \: q(c) \}, \, {\cal IC} \, )$, \vspace{1mm} \\
 \hspace*{18mm} ${\cal R}_{2} = ( \, \{p(a), \: q(a), \: q(c) \},
                   \, {\cal IC} \, )$. \\
 In this case, then, both the `consensus approach' and the `credulous
 approach' allow to infer, e.g., that $p(a)$ holds, while $p(b)$ is
 supported only by credulous reasoning, and $p(c)$ is not supported by
 either of these approaches.
} \end{example}


\section{Model-based Characterization of Repairs}
\label{section:model_theoretic_analysis}

In this section we set up a semantics for describing repairs and
preferred repairs in terms of a corresponding model theory. This
will allow us, in particular, to give an alternative description
of preferred repairs, this time in terms of a preferential semantics
for database theory.\\

As database semantics is usually defined in terms of two-valued
(Herbrand) models (cf. Definition~\ref{min_Herbrand_model} and
the discussion that proceeds it), it is natural to consider
two-valued semantics first. We show that arbitrary repairs can be
represented by {\em two-valued\/} models of the integrity
constraints. When a database is inconsistent, then by definition,
there is no two-valued interpretation which satisfies both its
database instance and its integrity constraints. A standard  way
to cope with this type of inconsistencies is to move to {\em
multiple-valued semantics\/} for reasoning with inconsistent and
incomplete information \fullcite<see,
e.g.,>{Su90,Su94,Me97,AA99,ABK00,dACM02}. What we will show
below, is that repairs can be characterized by three-valued
models of the whole database, that is, of the database instance
and the integrity constraints. Finally, we concentrate on the
most preferred repairs, and show that a certain subset of the
three-valued models can be used for characterizing
$\leq$-preferred repairs.

\begin{definition}
{\rm Given a valuation $\nu$ and a truth value $x$. Denote:
\vspace{1mm} \\ \hspace*{29mm}
 $ \nu^{x} = \{ p ~|~ p \mbox { is an atomic formula, and }
 \nu(p) = x \}$\footnote {Note, in particular, that in terms of
 Definition~\ref{min_Herbrand_model}, if $\nu \!=\! {\cal H}^{\cal D}$
 and $x \!=\! t$, we have that $\nu^{x} = {\cal D}$.}.
} \end{definition}

The following two propositions characterize repairs in terms of two-valued
structures.

\begin{proposition}
\label{prop:repair_0a}
 Let $\xDB$ be a database and let $M$ be a two-valued model of
 ${\cal IC}$. Let $\xIn = M^{t} \setminus {\cal D}$ and $\xOut =
 {\cal D} \setminus M^{t}$. Then $(\xIn,\xOut)$ is a repair of
 $\xDB$.
\end{proposition}

\noindent{\em Proof:} The definitions of $\xIn$ and $\xOut$
immediately imply that $\xIn \cap {\cal D} = \emptyset$ and
$\xOut \subseteq {\cal D}$. For the last condition in
Definition~\ref{def:repair}, note that ${\cal D} \cup \xIn
\setminus \xOut = {\cal D} \cup (M^{t} \setminus {\cal D})
\setminus ({\cal D} \setminus M^{t}) = M^{t}$. It follows that
$M$ is the least Herbrand model of ${\cal D} \cup \xIn \setminus
\xOut$ and it is also a model of ${\cal IC}$, therefore ${\cal D}
\cup \xIn \setminus \xOut \models {\cal IC}$. \hfill$\Box$

\begin{proposition}
\label{prop:repair_0b}
 Let $(\xIn,\xOut)$ be a repair of a database $\xDB$. Then there is a
 two-valued model $M$ of ${\cal IC}$ such that $\xIn = M^{t} \setminus
 {\cal D}$ and $\xOut = {\cal D} \setminus M^{t}$.
\end{proposition}

\noindent{\em Proof:} Consider a valuation $M$, defined for every atom $p$
as follows: \vspace{2mm} \\
\hspace*{24mm} $M(p) = \left\{ \begin{array}{ll}
      t  \ \ & \mbox{ if $p \in {\cal D} \cup \xIn \setminus \xOut$, }
               \vspace{1mm} \\
      f  \ \ & \mbox{ otherwise. } \\
\end{array} \right.$ \vspace{2mm} \\
By its definition, $M$ is a minimal Herbrand model of ${\cal D}
\cup \xIn \setminus \xOut$. Now, since $(\xIn,\xOut)$ is a repair
of $\xDB$, we have that ${\cal D} \cup \xIn \setminus \xOut
\!\models\! {\cal IC}$, thus $M$ is a (two-valued) model of
${\cal IC}$. Moreover, since $(\xIn,\xOut)$ is a repair,
necessarily $\xIn \cap {\cal D} = \emptyset$ and $\xOut \subseteq
{\cal D}$, hence we have the following: \vspace{1mm} \\
$\bullet$ $M^{t} \setminus {\cal D} =
          ({\cal D} \cup \xIn \setminus \xOut) \setminus {\cal D} = \xIn$,
          \vspace{1mm} \\
$\bullet$ ${\cal D} \setminus M^{t} =
          {\cal D} \setminus ({\cal D} \cup \xIn \setminus \xOut) =
          \xOut$. \hfill$\Box$ \\

When a database is inconsistent, it has no models that satisfy
both its integrity constraints and its database instance. One
common method to overcome such an inconsistency is to introduce
additional truth-values that intuitively represent partial
knowledge, different amounts of beliefs, etc. \cite<see,
e.g.,>{Pr89,Pr91,Su90,Fi91,Ar99,ABK00,Av02}. Here we follow this
guideline, and consider database integration in the context of a
three-valued semantics. The benefit of this is that, as we show
below, {\em any\/} database has some three-valued models, from
which it is possible to pinpoint the inconsistent
information, and accordingly construct repairs. \\

The underlying three-valued semantics considered here is induced
by the algebraic structure ${\cal THREE}$, shown in the
double-Hasse diagram of Figure~\ref{fig:three}\footnote{This
structure is used for reasoning with inconsistency by several
other three-valued formalisms, such as LFI \cite{CM01,CM02} and LP
\cite{Pr89,Pr91}.}.

\begin{figure}[hbt]
\begin{picture}(50,37)(-52,0)
\put(0,0){\vector(0,1){37}}    \put(01,35){$\leq_{k}$}
\put(0,0){\vector(1,0){50}}    \put(48,02){$\leq_{t}$}
\put(05,10){\circle*{2}}       \put(04,05){$f$}
\put(25,30){\circle*{2}}       \put(24,33){$\top$}
\put(45,10){\circle*{2}}       \put(44,05){$t$}
\put(05,10){\line(1,1){20}}    \put(25,30){\line(1,-1){20}}
\end{picture}
\caption{The structure ${\cal THREE}$}
\label{fig:three}
\end{figure}

Intuitively, the elements $t$ and $f$ in ${\cal THREE}$
correspond to the usual classical values {\tt true} and {\tt
false}, while the third element, $\top$, represents inconsistent
information (or belief). Viewed horizontally, ${\cal THREE}$ is a
complete lattice. According to this view, $f$ is the minimal
element, $t$ is the maximal one, and $\top$ is an intermediate
element. The corresponding order relation, $\leq_{t}$,
intuitively represents differences in the amount of {\em truth\/}
that each element exhibits. We denote the meet, join, and the
order reversing operation on $\leq_{t}$ by $\wedge$, $\vee$, and
$\neg$ (respectively). Viewed vertically, ${\cal THREE}$ is a
semi-upper lattice. In this view, $\top$ is the maximal element
and the two `classical values' are incomparable. This partial
order, denoted by $\leq_{k}$, may be intuitively understood as
representing differences in the amount of {\em knowledge\/} (or
information) that each element represents\footnote{See
\cite{Be77,Gi88,Fi91} for a more detailed discussion on these
orders and their intuitive meaning.}. We denote by $\oplus$ the
join operation on $\leq_{k}$\footnote{We follow here the
notations of \citeA{Fi90,Fi91}.}. \\

Various semantic notions can be defined on ${\cal THREE}$ as
natural generalizations of similar classical ones: a {\em
valuation\/} $\nu$ is a function that assigns a truth value in
${\cal THREE}$ to each atomic formula. Given a valuation $\nu$,
truth values $x_{i} \!\in\! \{t,f,\top\}$, and atomic formulae
$p_{i}$, we shall sometimes write $\nu =\{p_{i} \!:\! x_{i}\}$
instead of $\nu(p_{i}) = x_{i}$ \ ($i \!=\!1,2\ldots$). Any
valuation is extended to complex formulae in the obvious way. For
instance, $\nu(\neg\psi) = \neg\nu(\psi)$, $\nu(\psi \wedge \phi)
= \nu(\psi) \wedge \nu(\psi)$, and so forth\footnote{As usual, we
use here the same logical symbol to denote the connective that
appear on the left-hand side of an equation, and the corresponding
operator on ${\cal THREE}$ that appear on the right-hand side of
the same equation.}. The set of the {\em designated\/} truth
values in ${\cal THREE}$ (i.e., those elements in ${\cal THREE}$
that represent true assertions) consists of $t$ and $\top$. A
valuation $\nu$ {\em satisfies\/} a formula $\psi$ iff
$\nu(\psi)$ is designated. A valuation that assigns a designated
value to every formula in a theory ${\cal T}$ is a (three-valued)
{\em model\/} of ${\cal T}$.

\begin{lemma}
\label{k_lemma_1}
Let $\nu$ and $\mu$ be three-valued valuations
s.t. for every atom $p$, $\nu(p) \!\geq_{k}\! \mu(p)$. Then for
every formula $\psi$, $\nu(\psi) \!\geq_{k}\! \mu(\psi)$.
\end{lemma}

\noindent{\em Proof:} By induction on the structure of $\psi$.
\hfill$\Box$ \\

We shall write $\nu \!\geq_{k}\! \mu$, if $\nu$ and $\mu$ are
three-valued valuations, for which the condition of
Lemma~\ref{k_lemma_1} holds.

\begin{lemma}
\label{k_lemma_2}
If $\nu \!\geq_{k}\! \mu$ and $\mu$ is a model
of some theory ${\cal T}$, then $\nu$ is also a model of ${\cal
T}$.
\end{lemma}

\noindent{\em Proof:} For every formula $\psi \in {\cal T}$,
$\mu(\psi)$ is designated. Hence, by Lemma~\ref{k_lemma_1}, for
every formula $\psi \in {\cal T}$ $\nu(\psi)$ is also designated,
and so $\nu$ is a model of ${\cal T}$. \hfill$\Box$ \\

Next we characterize the repairs of a database $\DB$ by its
three-valued models:

\begin{proposition}
\label{prop:repair_1}
 Let $\xDB$ be a database and let $M$ be a two-valued model of ${\cal IC}$.
 Consider the three-valued valuation $N$, defined for every atom $p$ by
 $N(p) \!=\! {\cal H}^{\cal D}(p) \oplus M(p)$, and let $\xIn  =  N^{\top}
 \setminus {\cal D}$, $\xOut = N^{\top} \cap {\cal D}$. Then:
 \begin{enumerate}
    \item $N$ is a three-valued model of ${\cal D} \cup {\cal IC}$, and
    \item $(\xIn,\xOut)$ is a repair of $\xDB$.
 \end{enumerate}
\end{proposition}

Proposition~\ref{prop:repair_1} shows that repairs of a database
$\xDB$ may be constructed in a standard (uniform) way by
considering three-valued models that are the $\leq_{k}$-least
upper bounds of two two-valued valuations: the minimal Herbrand
model of the database instance, and a two-valued model of the
integrity constraints. Proposition~\ref{prop:repair_2} below
shows that any repair of $\xDB$ is of this form. \\

Before we give a proof for Proposition~\ref{prop:repair_1}, let's
demonstrate it by a simple example.

\begin{example}
 \label{example:M^DB}
 {\rm Let $\DB = (\{p,r\}\:,\:\{p \rightarrow q \})$. Then
 ${\cal H}^{{\cal D}} = \{p\!:\!t, \: q\!:\!f, \: r\!:\!t\}$, and
 the two-valued models of ${\cal IC} = \{p \rightarrow q \}$ are
 $\{p\!:\!t, \: q\!:\!t, \: r\!:\!t\}$,
 $\{p\!:\!t, \: q\!:\!t, \: r\!:\!f\}$,
 $\{p\!:\!f, \: q\!:\!t, \: r\!:\!t\}$,
 $\{p\!:\!f, \: q\!:\!t, \: r\!:\!f\}$,
 $\{p\!:\!f, \: q\!:\!f, \: r\!:\!t\}$,
 and $\{p\!:\!f, \: q\!:\!f, \: r\!:\!f\}$.
 Thus, the (three-valued) models of the form ${\cal H}^{\cal D} \oplus M$,
 where $M$ is a two-valued model of ${\cal IC}$, are
 $\{p\!:\!t\:, \: q\!:\!\top, \: r\!:\!t\}$,
 $\{p\!:\!t\:, \: q\!:\!\top, \: r\!:\!\top\}$,
 $\{p\!:\!\top, \: q\!:\!\top, \: r\!:\!t\}$,
 $\{p\!:\!\top, \: q\!:\!\top, \: r\!:\!\top\}$,
 $\{p\!:\!\top, \: q\!:\!f, \: r\!:\!t\}$
 and $\{p\!:\!\top, \: q\!:\!f, \: r\!:\!\top\}$.
 By Proposition~\ref{prop:repair_1}, the pairs
 $(\{q\},\{\})$, $(\{q\},\{r\})$,  $(\{q\},\{p\})$,
 $(\{q\},\{p,r\})$, $(\{\},\{p\})$, and $(\{\},\{p,r\})$,
 are repairs of $\DB$.
} \end{example}

\noindent{\em Proof of Proposition \ref{prop:repair_1}:} Since by
the definition of $N$, $N \!\geq_{k}\! {\cal H}^{\cal D}$, and
since ${\cal H}^{\cal D}$ is a model of ${\cal D}$,
Lemma~\ref{k_lemma_2} implies that $N$ is a model ${\cal D}$.
Similarly, $N \!\geq_{k}\! M$, and $M$ is a model of ${\cal IC}$,
thus by the same lemma $N$ is also a model of ${\cal IC}$.

For the second part, we observe that $\xIn = N^{\top} \setminus
{\cal D} = M^{t} \setminus {\cal D}$ and $\xOut = N^{\top} \cap
{\cal D} = M^{f} \cap {\cal D} = {\cal D} \setminus M^{t}$. Now,
$M$ is a two-valued model of ${\cal IC}$ and hence, by
Proposition~\ref{prop:repair_0a}, $(\xIn,\xOut)$ is a repair of
$\xDB$. \hfill$\Box$ \\

Note that the specific form of the three-valued valuations
considered in Proposition~\ref{prop:repair_1} is essential here,
as the proposition does not hold for {\em every\/} three-valued
model of ${\cal D} \cup {\cal IC}$. To see this consider, e.g.,
${\cal D} = \{\}$, ${\cal IC} = \{p\:,\:p\!\rightarrow\! q\}$, and
a three valued valuation $N$ that assigns $\top$ to $p$ and $t$
to $q$. Clearly, $N$ is a model of ${\cal D} \cup {\cal IC}$, but
the corresponding update, $(N^{\top} \setminus {\cal
D}\:,\:N^{\top} \cap {\cal D}) = (\{p\},\{\})$ is {\em not\/} a
repair of $\xDB$, since $(\{p\},{\cal IC})$ is not a consistent
database. \\

Again, as we have noted above, it is possible to show that the
converse of Proposition~\ref{prop:repair_1} is also true:

\begin{proposition}
\label{prop:repair_2}
Let $(\xIn,\xOut)$ be a repair of a database $\xDB$. Then there is a
three-valued model $N$ of ${\cal D} \cup {\cal IC}$, such that $\xIn  =
N^{\top} \setminus {\cal D}$ and $\xOut = N^{\top} \cap {\cal D}$.
\end{proposition}

\noindent{\em Proof:} Consider a valuation $N$, defined for every atom $p$
as follows: \vspace{2mm} \\
\hspace*{20mm} $N(p) = \left\{ \begin{array}{ll}
     \top  \ \ & \mbox{ if $p \!\in\! \xIn \cup \xOut$, }  \vspace{1mm} \\
     t     \ \ & \mbox{ if $p \!\not\in\! \xIn \cup \xOut$ but
                        $p \!\in\! {\cal D}$, }  \vspace{1mm} \\
     f     \ \ & \mbox{ otherwise. } \\
\end{array} \right.$ \vspace{2mm} \\
By the definition of $N$ and since $(\xIn,\xOut)$ is a repair of $\xDB$,
we have that $N^{\top} \setminus {\cal D} = (\xIn \cup \xOut) \setminus
{\cal D} = \xIn$ and $N^{\top} \cap {\cal D} = (\xIn \cup \xOut) \cap
{\cal D} = \xOut$.

It remains to show that $N$ is a (three-valued) model of ${\cal
D}$ and ${\cal IC}$. It is a three-valued model of ${\cal D}$
because for every $p \!\in\! {\cal D}$, $N(p) \!\in\! \{t,\top\}$.
Regarding ${\cal IC}$, $(\xIn,\xOut)$ is a repair of $\xDB$, thus
every formula in ${\cal IC}$ is true in the least Herbrand model
$M$ of ${\cal D}' = {\cal D} \cup \xIn \setminus \xOut$. In
particular, $M(q)=t$ for every $q \in {\cal D}'$. But since for
every $p \!\in\! {\cal D} \cup \xIn$ we have that $N(p) \!\in\!
\{t,\top\}$ and ${\cal D}' \subseteq {\cal D} \cup \xIn$,
necessarily $\forall q \!\in\! {\cal D}' \ N(q) \!\in\!
\{t,\top\}$.  It follows that for every $q \!\in\!{\cal D}'$,
$N(q) \!\geq_{k}\!  M(q) = t$, thus by Lemma~\ref{k_lemma_1} and
Lemma~\ref{k_lemma_2}, $N$ must also be a (three-valued) model of
${\cal D}'$. Hence $N$ is a model of ${\cal IC}$. \hfill$\Box$ \\

The last two propositions characterize the repairs of $\UDB$ in
terms of pairs that are associated with certain three-valued
models of ${\cal D} \cup {\cal IC}$. We shall denote the elements
of these pairs as follows:

\begin{notation}
{\rm Let $N$ be a three-valued model and let $\DB = \xDB$ be a
database. Denote: $\xIn^{N} = N^{\top} \setminus {\cal D}$ and
$\xOut^{N} = N^{\top} \cap {\cal D}$.
} \end{notation}

We conclude this model-based analysis by characterizing the set of
the $\leq$-preferred repairs, where $\leq$ is one of the
preference criteria considered in
Definition~\ref{preference_criteria} (i.e., set inclusion or
minimal cardinality). As the propositions below show, common
considerations on how inconsistent databases can be `properly'
recovered (e.g., keeping the amount of changes as minimal as
possible, being `as close as possible' to the original instance,
etc.) can be captured by preferential models in the context of
preferential semantics \cite{Sh88}. The idea is to define some
order relation on the set of the (three-valued) models of the
database. This relation intuitively captures some criterion for
making preferences among the relevant models. Then, only the `most
preferred' models (those that are minimal with respect to the
underlying order relation) are considered in order to determine
how the database should be repaired. Below we formalize this idea:

\begin{definition}
{\rm Given a database $\DB = \xDB$, denote: \vspace{1mm} \\
 \hspace*{25mm}
 ${\cal M}^{\DB} = \{ N ~|~ N \geq_{k} {\cal H}^{\cal D} \oplus M
                      \mbox{ for some classical model $M$ of } {\cal IC}
 \}$\footnote {Note that $N$ is a {\em three-valued\/} valuation
 and $M$ is a {\em two-valued\/} model of ${\cal IC}$. }.
} \end{definition}

\begin{example}
\label{example:M^DB_2}
 {\rm Consider again the database $\DB = (\{p,r\}\:,\:\{p \rightarrow q \})$
 of Example~\ref{example:M^DB}. As we have shown, there are six
 valuations of the form ${\cal H}^{\cal D} \oplus M$, for some
 two-valued model $M$ of ${\cal IC}$, namely:
 \begin{center}
 \begin{tabular}{lll}
 $\{p\!:\!t\:, \: q\!:\!\top, \: r\!:\!t\}$, &
 $\{p\!:\!t\:, \: q\!:\!\top, \: r\!:\!\top\}$, &
 $\{p\!:\!\top, \: q\!:\!\top, \: r\!:\!t\}$, \vspace{1mm} \\
 $\{p\!:\!\top, \: q\!:\!\top, \: r\!:\!\top\}$, &
 $\{p\!:\!\top, \: q\!:\!f, \: r\!:\!t\}$, &
 $\{p\!:\!\top, \: q\!:\!f, \: r\!:\!\top\}$. \\
 \end{tabular}
 \end{center}
 The $k$-minimal models among these models are
 $\{p\!:\!t, \: q\!:\!\top, \: r\!:\!t\}$ and
 $\{p\!:\!\top, \: q\!:\!f, \: r\!:\!t\}$, thus \vspace{1mm}
 ${\cal M}^{\DB} =
   \{ N ~|~ N(p) \geq_{k} t, \: N(q) = \top, \: N(r) \geq_{k} t \}
   \ \cup \
   \{ N ~|~ N(p) = \top, N(q) \geq_{k} f, \: N(r) \geq_{k} t \}.$
} \end{example}

Preference orders should reflect some normality considerations
applied on the relevant set of valuations (${\cal M}^{\DB}$, in
our case); $\nu$ is preferable than $\mu$, if $\nu$ describes a
situation that is more common (plausible) than the one described
by $\mu$. Hence, a natural way to define preferences in our case
is by minimizing inconsistencies. We thus get the following
definition:

\begin{definition}
{\rm Let ${\cal S}$ be a set of three-valued valuations, and
$N_{1}, N_{2} \!\in\! {\cal S}$.
\begin{itemize}
   \item $N_{1}$ is {\em $\leq_{i}$-more consistent\/} than $N_{2}$, if
         $N_{1}^{\top} \subset N_{2}^{\top}$.
   \item $N_{1}$ is {\em $\leq_{c}$-more consistent\/} than $N_{2}$, if
         $|N_{1}^{\top}| < |N_{2}^{\top}|$.
   \item $N \!\in\! {\cal S}$ is
         {\em $\leq_{i}$-maximally consistent\/} in ${\cal S}$
         (respectively, $N$ is {\em $\leq_{c}$-maximally consistent\/}
         in ${\cal S}$), if there is no $N' \!\in\! {\cal S}$ that is
         $\leq_{i}$-more consistent than $N$ (respectively, no
         $N'\!\in\! {\cal S}$ is $\leq_{c}$-more consistent than $N$).
\end{itemize}
} \end{definition}

The following propositions show that there is a close relationship
between most consistent models of ${\cal M}^{\DB}$ and the preferred
repairs of $\DB$.

\begin{proposition}
\label{prop:repair_3}
If $N$ is a $\leq_{i}$-maximally consistent
element in ${\cal M}^{\DB}$, then $(\xIn^{N},\;\xOut^{N})$ is a
$\leq_{i}$-preferred repair of $\DB$.
\end{proposition}

\noindent {\em Proof:\/} By Proposition~\ref{prop:repair_1},
$(\xIn^{N},\;\xOut^{N})$ is a repair of $\DB$. If it is not a
$\leq_{i}$-preferred repair of $\DB$, then there is a repair
$(\xIn,\;\xOut)$ s.t. $\xIn \subseteq \xIn^{N}$, $\xOut \subseteq
\xOut^{N}$, and $\xIn \cup \xOut \subset \xIn^{N} \cup
\xOut^{N}$. By Proposition~\ref{prop:repair_2} and its proof,
there is an element $N' \!\in\! {\cal M}^{\DB}$ s.t. $\xIn =
\xIn^{N'}$, $\xOut = \xOut^{N'}$, and $(N')^{\top} = \xIn^{N'}
\cup \xOut^{N'}$. It follows, then, that $(N')^{\top} \subset
N^{\top}$, and so $N$ is not a maximally consistent in ${\cal
M}^{\DB}$, but this is a contradiction to the definition of $N$.
\hfill$\Box$

\begin{proposition}
\label{prop:repair_4}
 Suppose that $(\xIn,\;\xOut)$ is a $\leq_{i}$-preferred repair
 of $\DB$. Then there is a $\leq_{i}$-maximally consistent element
 $N$ in ${\cal M}^{\DB}$ s.t. $\xIn = \xIn^{N}$ and $\xOut = \xOut^{N}$.
\end{proposition}

\noindent{\em Proof:} The pair $(\xIn,\;\xOut)$ is in particular
a repair of $\DB$, thus by Proposition~\ref{prop:repair_0b} there
is a classical model $M$ of ${\cal IC}$ such that $\xIn = M^{t}
\setminus {\cal D}$ and $\xOut = {\cal D} \setminus M^{t}$.
Consider the following valuation:
\[ N(p) = \left\{ \begin{array}{ll}
          \top \ \ & \mbox{ if  $p \!\in\! M^{t} \setminus {\cal D}$ or
                                $p \!\in\! {\cal D} \setminus M^{t}$ }
                             \vspace{1mm} \\
          M(p) \ \ & \mbox{ otherwise. } \\
\end{array} \right. \]
First we show that $N = {\cal H}^{{\cal D}} \oplus M$. This is so
since if $M(p) = {\cal H}^{{\cal D}}(p)$, then since ${\cal
H}^{{\cal D}}$ is a minimal Herbrand model of ${\cal D}$,
necessarily $p \!\not\in\! M^{t} \setminus {\cal D}$ and $p
\!\not\in\! {\cal D} \setminus M^{t}$, thus $N(p) \!=\! M(p)
\!=\! M(p) \oplus M(p) = M(p) \oplus {\cal H}^{{\cal D}}(p)$.
Otherwise, if $M(p) \neq {\cal H}^{{\cal D}}(p)$, then either
$M(p) \!=\! t$ and ${\cal H}^{{\cal D}}(p) \!=\! f$, i.e., $p
\!\in\! M^{t} \setminus {\cal D}$, or $M(p) \!=\! f$ and ${\cal
H}^{{\cal D}}(p) \!=\! t$, i.e., $p \!\in\! {\cal D} \setminus
M^{t}$. In both cases, $N(p) \!=\! \top \!=\! M(p) \oplus {\cal
H}^{{\cal D}}(p)$\footnote {Here we use the fact that $t \oplus f
\!=\! \top$.}. Thus $N = {\cal H}^{{\cal D}} \oplus M$, and so $N
\!\in\! {\cal M}^{\DB}$. Now, by Proposition~\ref{prop:repair_0b}
again, and by the definition of $N$, $\xIn^{N} = N^{\top}
\setminus {\cal D} = [(M^{t} \setminus {\cal D}) \cup ({\cal D}
\setminus M^{t})] \setminus {\cal D} = M^{t} \setminus {\cal D} =
\xIn$, and $\xOut^{N} = N^{\top} \cap {\cal D} = [(M^{t}
\setminus {\cal D}) \cup ({\cal D} \setminus M^{t})] \cap {\cal
D} = {\cal D} \setminus M^{t} = \xOut$.

It remains to show that $N$ is $\leq_{i}$-maximally consistent in
${\cal M}^{\DB}$. Suppose not. Then there is an $N' \!\in\! {\cal
M}^{\DB}$ s.t. $(N')^{\top} \subset N^{\top} = \xIn \cup \xOut$.
By Proposition~\ref{prop:repair_1}, $(\xIn^{N'},\;\xOut^{N'})$ is
also a repair of $\DB$. Moreover, \\
$\bullet$ $\xIn^{N'} \!=\! (N')^{\top} \setminus {\cal D}
          \!\subseteq\! N^{\top} \setminus {\cal D} \!=\!
          \xIn^{N} \!=\! \xIn$, \\
$\bullet$ $\xOut^{N'} \!=\! (N')^{\top} \cap {\cal D}
          \!\subseteq\! N^{\top} \cap {\cal D} \!=\! \xOut^{N}
          \!=\! \xOut$, \\
$\bullet$ $\xIn^{N'} \cup \xOut^{N'} \!=\! (N')^{\top}
          \!\subset\! N^{\top} \!=\! \xIn^{N} \cup \xOut^{N} \!=\!
          \xIn \cup \xOut$. \\
Hence $(\xIn^{N'},\;\xOut^{N'}) <_{i} (\xIn,\;\xOut)$, and so
$(\xIn,\;\xOut)$ is not a $\leq_{i}$-preferred repair of $\xDB$, a
contradiction. \hfill$\Box$ \\

Propositions~\ref{prop:repair_3} and \ref{prop:repair_4} may be
formulated in terms of $\leq_{c}$ as follows:

\begin{proposition}
\label{prop:repair_5}
If $N$ is a $\leq_{c}$-maximally consistent
element in ${\cal M}^{\DB}$, then $(\xIn^{N},\;\xOut^{N})$ is a
$\leq_{c}$-preferred repair of $\DB$.
\end{proposition}

\begin{proposition}
\label{prop:repair_6}
Suppose that $(\xIn,\;\xOut)$ is a
$\leq_{c}$-preferred repair of $\DB$. Then there is a
$\leq_{c}$-maximally consistent element $N$ in ${\cal M}^{\DB}$
s.t. $\xIn = \xIn^{N}$ and $\xOut = \xOut^{N}$.
\end{proposition}

The proofs of the last two propositions are similar to those of
Propositions~\ref{prop:repair_3} and \ref{prop:repair_4},
respectively.

\begin{example}
{\rm Consider again Example~\ref{example:set_inclusion}. We have
that: \vspace{1mm} \\ \hspace*{21mm}
 $\UDB = \xDB = ( \, \{ p(a), \:p(b), \: q(a), \: q(c) \}, \,
                \{ \forall X (p(X) \!\rightarrow\! q(X)) \} \, ).$
\vspace{1mm} \\
Thus, ${\cal H}^{{\cal D}} = \{ p(a)\!:\!t, \:p(b)\!:\!t, \:
p(c)\!:\!f, \: q(a)\!:\!t, \: q(b)\!:\!f, \: q(c)\!:\!t \}$, and
the classical models of ${\cal IC}$ are those in which either
$p(y)$ is false or $q(y)$ is true for every $y \!\in\!
\{a,b,c\}$. Now, since in ${\cal H}^{{\cal D}}$ neither $p(b)$ is
false nor $q(b)$ is true, it follows that {\em every\/} element
in ${\cal M}^{\UDB}$ must assign $\top$ either to $p(b)$ or to
$q(b)$. Hence, the $\leq_{i}$-maximally consistent elements in
${\cal M}^{\UDB}$ (which in this case are also the
$\leq_{c}$-maximally consistent elements in ${\cal M}^{\UDB}$)
are the following:
\vspace{1mm} \\
\hspace*{28mm} $M_{1} = \{ \: p(a)\!:\!t, \: p(b)\!:\!\top,
                          \: p(c)\!:\!f, \: q(a)\!:\!t, \
                          \: q(b)\!:\!f, \: q(c)\!:\!t \: \}$,
\vspace{1mm} \\
\hspace*{28mm} $M_{2} = \{ \: p(a)\!:\!t, \: p(b)\!:\!t,
                          \: p(c)\!:\!f, \: q(a)\!:\!t,
                          \: q(b)\!:\!\top, \: q(c)\!:\!t \: \}$.
\vspace{1mm} \\
By Propositions~\ref{prop:repair_3} and \ref{prop:repair_4},
then, the $\leq_{i}$-preferred repairs of $\UDB$ (which are also
its $\leq_{c}$-preferred repairs) are
$(\xIn^{M_{1}},\;\xOut^{M_{1}}) = (\emptyset,\:\{p(b)\})$ and
$(\xIn^{M_{2}},\;\xOut^{M_{2}}) = (\{q(b)\},\: \emptyset)$ (cf.
Example~\ref{example:set_inclusion}).
} \end{example}

\begin{example}
{\rm In Examples~\ref{example:M^DB} and \ref{example:M^DB_2}, the
$\leq_{i}$-maximally consistent elements (and the
$\leq_{c}$-maximally consistent elements) of ${\cal M}^{\DB}$ are
 $N_{1} = \{ \: p\!:\! t, \: q\!:\! \top, \: r \!:\!t \: \}$ and
 $N_{2} = \{ \: p\!:\! \top, q\!:\! f, \: r \!:\! t \: \}$.
It follows that the preferred repairs in this case are $(\{q\},\:
\emptyset)$ and $(\emptyset,\:\{p\})$.
} \end{example}

To summarize, in this section we have considered a model-based,
three-valued {\em preferential semantics\/} for database integration.
We have shown (Propositions \ref{prop:repair_3} -- \ref{prop:repair_6})
that common and natural criteria for making preferences among possible
repairs (i.e., set inclusion and minimal cardinality) can be expressed
by order relations on three-valued models of the database. The two ways
of making preferences (among repairs on one hand and among three-valued
models on the other hand) are thus strongly related, and induce two
alternative approaches for database integration. In the next section we
shall consider a third approach to the same problem (aimed to provide
an {\em operational semantics\/} for database integration) and relate
it to the model-based semantics, discussed above.


\section{Computing Repairs through Abduction}
\label{section:A_system}

In this section we introduce an abductive system that consistently
integrates possibly contradicting data-sources. This system
computes, for a set of data-sources and a preference criterion
$\leq$, the corresponding $\leq$-repaired databases\footnote{It
is important to note already in this stage that for computing the
$\leq$-repaired databases it won't be necessary to produce all
the repaired databases.}. Our framework is composed of an
abductive logic program \fullcite{DK00} and an abductive solver
${\cal A}$\mbox{system} \fullcite{KvND01,vNK01} that is based on
the abductive refutation procedure SLDNFA \fullcite{DD92,DD98}. In
the first three parts of this section we describe these
components: in Section~\ref{subsec:ID_logic} we give  a general
description of abductive reasoning, in Section~\ref{subsec:meta}
we show how it can be applied to encode database repairs, and in
Section \ref{subsec:the_system} we describe the `computational
platform'. Then, in Section~\ref{subsec:example} we demonstrate
the computation process by a comprehensive example, and in
Section~\ref{section:soundness_completeness} we specify soundness
and completeness results of our approach (with respect to the
basic definitions of Section~\ref{section:problem_definition} and
the model-based semantics of
Section~\ref{section:model_theoretic_analysis}). Finally, in
Section~\ref{subsec:specialized_information} we consider some
ways of representing special types of data in the system.


\subsection{Abductive Logic Programming}
\label{subsec:ID_logic}

We start with a general description of abductive reasoning in the
context of logic programming. As usual in logic programming, the
language contains constants, functions, and predicate symbols. A
{\em term\/} is either a variable, a constant, or a compound term
$f(t_1,\dots,t_n)$, where $f$ is an $n$-ary function symbol and
$t_i$ are terms. An {\em atom\/} is an expression of the form
$p(t_1,\dots,t_m)$, where $p$ is an $m$-ary predicate symbol and
$t_i$ $(i \!=\! 1,\!\ldots\!,m)$ are terms. A {\em literal\/} is
an atom or a negated atom. A {\em denial\/} is an expression of
the form $\forall \XX(\leftarrow F)$, where $F$ is a conjunction
of literals and $\XX$ is a subset of the variables in $F$. The
free variables in $F$ (those that are not in $\XX$) can be
considered as place holders for objects of unspecified identity
(Skolem constants). Intuitively, the body $F$ of a denial $\forall
\XX(\leftarrow F)$ represents an invalid situation.

\begin{definition}
{\rm \cite{KKT92,DK00} An {\em abductive logic theory\/} is a
triple ${\cal T} = ({\cal P}\:,\:{\cal A}\:,\:{\cal IC})$, where:
\begin{itemize}
   \item ${\cal P}$ is a {\em logic program\/}, consisting of clauses of the
         form $h \leftarrow l_{1} \wedge \ldots \wedge l_{n}$, where $h$
         is an atomic formula and $l_i$ $(i = 1,\ldots,n)$ are literals.
         These clauses are interpreted as definitions for the predicates in
         their heads,
   \item ${\cal A}$ is a set of {\em abducible predicates\/}, i.e.,
         predicates that do not appear in the head of any clause in
         ${\cal P}$,
   \item ${\cal IC}$ is a set of first-order formulae, called
         {\em integrity constraints\/}.
\end{itemize}
} \end{definition}


All the main model semantics of logic programming can be extended
to abductive logic programming. This includes two-valued
completion \cite{CTT91} and three-valued completion semantics
\cite{DD93}, extended well-founded semantics \cite{PAA91}, and
generalized stable semantics \cite{KM90b}. These semantics can be
defined in terms of arbitrary interpretations \cite{DD93}, but
generally they are based on Herbrand interpretations. The effect
of this restriction on the semantics of the abductive theory is
that a {\em domain closure\/} condition is imposed: the domain of
interpretation is known to be the Herbrand universe.  A {\em
model\/} of an abductive theory under any of these semantics is a
Herbrand interpretation ${\cal H}$, for which there exists a
collection of ground abducible facts $\Delta$, such that ${\cal
H}$ is a model of the logic program ${\cal P} \cup \Delta$ (with
respect to the corresponding semantics of logic programming) and
${\cal H}$ classically satisfies any element in ${\cal IC}$. \\

Similarly, for any of the main semantics ${\cal S}$ of logic
programming, one can define the notion of an abductive solution
for a query and an abductive theory.

\begin{definition}
\label{def:abductive_solutions} {\rm \cite{KKT92,DK00} An
(abductive) {\em solution\/} for a theory $({\cal P}\:,\:{\cal
A}\:,\:{\cal IC})$ and a query ${\cal Q}$ is a set $\Delta$ of
ground abducible atoms, each one having a predicate symbol in
${\cal A}$, together with an answer substitution $\theta$, such
that the following three conditions are satisfied:
\begin{itemize}
   \item [a)] ${\cal P} \cup \Delta$ is consistent in the semantics ${\cal S}$,
   \item [b)] ${\cal P} \cup \Delta \models_{\cal S} {\cal IC}$,
   \item [c)] ${\cal P} \cup \Delta \models_{\cal S} \forall{\cal Q}\theta$.
\end{itemize}
} \end{definition}

In the next section we will use an abductive theory with a
non-recursive program to model the database repairs. The next
proposition shows that for such abductive theories all Herbrand
semantics coincide, and models correspond to abductive solutions
for the query {\tt true}.

\begin{proposition}
Let ${\cal T} = ({\cal P}\:,\:{\cal A}\:,\:{\cal IC})$ be an
abductive theory, such that ${\cal P}$ is a non-recursive
program. Then ${\cal H}$ is a Herbrand model of the three-valued
completion semantics, iff ${\cal H}$ is a Herbrand model of the
two-valued completion semantics, iff ${\cal H}$ is a generalized
stable model of ${\cal T}$, iff ${\cal H}$ is a generalized
well-founded model of ${\cal T}$.

If ${\cal H}$ is a model of ${\cal T}$, then the set $\Delta$ of
abducible atoms in ${\cal H}$ is an abductive solution for the
query ${\tt true}$. Conversely, for every abductive solution for
${\tt true}$, there exists a unique model ${\cal H}$ of ${\cal
T}$, such that $\Delta$ is the set of true abducible atoms in
${\cal H}$.
\end{proposition}

\noindent{\em Proof:} The proof is based on the well-known fact
that for non-recursive logic programs, all the main semantics of
logic programming coincide. In particular, for a non-recursive
logic program ${\cal P}$ there is a Herbrand interpretation
${\cal H}$, which is the unique model under each  semantics
\cite<see, for example,>{DD93}.

Let ${\cal H}$ be a model of ${\cal T} = ({\cal P}\:,\:{\cal
A}\:,\:{\cal IC})$ under any of the four semantics mentioned
above. Then there exists a collection of ground abducible facts
$\Delta$, such that ${\cal H}$ is a model of the logic program
${\cal P} \cup \Delta$ under the corresponding semantics of logic
programming.  Since ${\cal P}$ is non-recursive, so is ${\cal P}
\cup \Delta$. By the above observation, ${\cal H}$ is the unique
model of ${\cal P} \cup \Delta$ under any of the above mentioned
semantics. Hence, ${\cal H}$ is a model of ${\cal T}$ under any
of the other semantics. This proves the first part of the
proposition.

When ${\cal H}$ is a Herbrand model of ${\cal T}$, there is a set
$\Delta$ of abducible atoms such that ${\cal H}$ is a model of
${\cal P}\cup\Delta$. Clearly, $\Delta$ must be the set of true
abducible atoms in ${\cal H}$. Then ${\cal P}\cup\Delta$ is
obviously consistent, and it entails the integrity constraints of
${\cal T}$, which entails ${\tt true}$. Hence, $\Delta$ is an
abductive solution for ${\tt true}$.  Conversely, for any set
$\Delta$ of abducible atoms, $P\cup\Delta$ has a unique model
${\cal H}$ and the set of true abducible atoms in ${\cal H}$ is
$\Delta$. When $\Delta$ is an abductive solution for ${\tt
true}$, ${\cal H}$ satisfies the integrity constraints, and hence
${\cal H}$ is a model of ${\cal T}$. Consequently, ${\cal H}$ is
the unique model of ${\cal T}$, and its set of true abducible
atoms is $\Delta$. \hfill$\Box$ \\

In addition to the standard properties of abductive solutions for
a theory ${\cal T}$ and a query ${\cal Q}$, specified in
Definition~\ref{def:abductive_solutions}, one frequently imposes
optimization conditions on the solutions $\Delta$, analogous to
those found in the context of database repairs. Two frequently
used criteria are that the generated abductive solution $\Delta$
should be minimal with respect to set inclusion or with respect
to set cardinality (cf. Definition \ref{preference_criteria}). The
fact that the same preference criteria are used for choosing
appropriate abductive solutions and for selecting preferred
database repairs does not necessarily mean that there is a
natural mapping between the corresponding solutions. In the next
sections we will show, however, that {\em meta-programming\/}
allows us to map a database repair problem into an abductive
problem (w.r.t. the same type of preference criterion).


\subsection{An Abductive Meta-Program for Encoding Database Repairs}
\label{subsec:meta}

The task of repairing the union of $n$ given databases $\DB_i$
with respect to the integration of the local integrity
constraints ${\cal IC}$, can be represented by an abductive
theory ${\cal T} = ({\cal P}\:,\:{\cal A}\:,\:{\cal IC}')$, where
${\cal P}$ is a meta-program encoding how a new database is
obtained by updating the existing databases, ${\cal A}$ is the
set $\{{\tt insert}, {\tt retract}\}$ of abducible predicates
used to describe updates, and ${\cal IC}'$ encodes the integrity
constraints. In ${\cal P}$, facts $p$ that appear in at least one
of the databases are encoded by atomic rules ${\tt db}(p)$, and
facts $p$ that appear in the updated database are represented by
atoms ${\tt fact}(p)$. The latter predicate is defined as
follows: \vspace{2mm}

\noindent
\hspace*{5mm} {\tt fact(X) $\leftarrow$ db(X) $\wedge$ $\neg$retract(X) } \\
\hspace*{5mm} {\tt fact(X) $\leftarrow$ insert(X) } \vspace{2mm}

To assure that the predicates ${\tt insert}$ and ${\tt retract}$
encode a proper update of the database, the following integrity
constraints are also specified:
\begin{itemize}
\item An inserted element should not belong to a given database: \\
{\tt $\leftarrow$ insert(X) $\wedge$ db(X) }
\item A retracted element should belong to some database: \\
{\tt $\leftarrow$ retract(X) $\wedge$ $\neg$db(X) }
\end{itemize}

The set of integrity constraints ${\cal IC}'$ is obtained by a
straightforward transformation from ${\cal IC}$: every occurrence
of a database fact $p$ in some integrity constraint is replaced by
${\tt fact}(p)$\footnote{Since our abductive system (see
Section~\ref{subsec:the_system}) will accept integrity
constraints in a denial form, in case that the elements of ${\cal
IC}'$ are not in this form, the Lloyd-Topor transformation
\cite{LT84} may also be applied here; we consider this case in
Section~\ref{IC_2_denial_form}.}.

\begin{example}
\label{encoding_teaches}
 {\rm {\bf (Example~\ref{example:teachers}, revisited)}
 Figure~\ref{fig:examples} contains the meta-program encoding
 Example~\ref{example:teachers} (the codes for
 Examples~\ref{example:suppliers} and \ref{example:set_inclusion}
 are similar).

\begin{figure}[ht]
\begin{picture}(125,92) (-13,0)
 \put(5,85)   { \% System definitions: }
 \put(5,80)   { {\tt defined(fact(\_))} }
 \put(5,75)   { {\tt defined(db(\_))} }
 \put(5,70)   { {\tt abducible(insert(\_))} }
 \put(5,65)   { {\tt abducible(retract(\_))} }

 \put(5,55)   { \% The composer: }
 \put(5,50)   { {\tt fact(X) $\leftarrow$ db(X) $\wedge$ $\neg$retract(X)} }
 \put(5,45)   { {\tt fact(X) $\leftarrow$ insert(X)} }
 \put(5,40)   { $\leftarrow$ {\tt insert(X) $\wedge$ db(X)} }
 \put(5,35)   { $\leftarrow$ {\tt retract(X) $\wedge$ $\neg$db(X)} }

 \put(5,25)   { \% The databases: }
 \put(5,20)   { {\tt db(teaches(c1,n1))} }
 \put(110,20) { \% D$_1$ }
 \put(5,15)   { {\tt db(teaches(c2,n2))} }
 \put(5,10)   { {\tt db(teaches(c2,n3))} }
 \put(110,10) { \% D$_2$ }
 \put(5,5)    { {\tt Y = Z $\leftarrow$ fact(teaches(X,Y)) $\wedge$
                                      fact(teaches(X,Z)) } }
 \put(110,5)  { \% IC }
 \put(0,0){\framebox(125,92)}
 \end{picture}
 \caption{A meta-program for Example~\ref{example:teachers}}
 \label{fig:examples}
\end{figure}
} \end{example}

As noted in Section \ref{subsec:ID_logic}, under any of the main
semantics of abductive logic programing there is a one to one
correspondence between repairs of the composed database $\DB$ and
the Herbrand models of its encoding, the abductive meta theory
${\cal T}$. Consequently, abduction can be used to compute
repairs. In the following sections we introduce an abductive
method for this purpose.


\subsection{The Abductive Computational Model (The ${\cal A}$\mbox{system})}
\label{subsec:the_system}

Below we describe the abductive system that will be used to
compute database repairs. The ${\cal A}$\mbox{system}
\fullcite{KvND01,vNK01} is a tool combining abductive logic
theories and constraint logic programming (CLP). It is a synthesis
of the refutation procedures SLDNFA \fullcite{DD98} and ACLP
\shortcite{KMM00}, together with an improved control strategy.
The essence of the ${\cal A}$\mbox{system} is a reduction of a
high level specification to a lower level constraint store, which
is managed by a constraint solver.  See {\tt
http://www.cs.kuleuven.ac.be/$\sim$dtai/kt/} for the latest
version of the system\footnote{This version runs on top of Sicstus
Prolog 3.10.1 or later versions.}. Below we review the theoretical
background as well as some practical considerations behind this
system. For more information, see \fullcite{DD98} and
\fullcite{KvND01}.


\subsubsection{Abductive Inference}
\label{abductive_inferences}

The input to the \asystem\ is an abductive theory ${\cal T} =
({\cal P},\:{\cal A},\:{\cal IC})$, where ${\cal IC}$ consists of
universally quantified denials. The process of answering a query
$\cal Q$, given by a conjunction of literals, can be described as
a derivation for ${\cal Q}$ through rewriting {\em states.\/} A
state is a pair $(\G\:,\:\st{})$, where $\G$, the set of {\em
goal formulae,\/} is a set of conjunctions of literals and
denials.  During the rewriting process the elements in $\G$ (the
goals) are reduced to basic formulae that are stored in the
structure $\st{}$. This structure is called a {\em store\/}, and
it consists of the following elements\footnote{The actual
implementation of the \asystem\ also contains a store for finite
domain constraint expressions. This store is not needed for the
application here, and hence it is omitted.}:
\begin{itemize}
   \setlength{\itemsep}{0cm}
   \item a set $\Delta$ that contains abducibles $a(\ttt)$.
   \item a set $\Delta^*$ that contains denials of the form
         $\forall \XX(\leftarrow a(\ttt)\land Q)$, where $a(\ttt)$ is an
         abducible. Such a denial may contain free variables.
   \item a set $\cal E$ of equalities and inequalities over terms.
\end{itemize}
The consistency of $\cal E$ is maintained by a constraint solver
that uses the Martelli and Montanari unification algorithm
\cite{MM82} for the equalities and constructive negation for the
inequalities. \\

A state $\state = (\G\:,\:\st{})$ is called {\em consistent\/} if
$\G$ does not contain {\tt false} and $\st{}$ is consistent (since
$\Delta$ and $\Delta^*$ are kept consistent with each other and
with ${\cal E}$, the latter condition is equivalent to the
consistency of $\cal E$). A consistent state with an empty set of
goals $(\G = \emptyset)$ is called a {\em solution state\/}. \\

A derivation starts with an {\em initial state\/}
$(\goal{0}\:,\:\st{0})$, where every element in $\st{0}$ is empty,
and the initial goal, $\G_0$, contains the query $\cal Q$ and all
the integrity constraints ${\cal IC}$ of the theory $\cal T$.
Then a sequence of rewriting {\em steps\/} is performed. A step
starts in a certain state $\state_i = (\goal{i}\:,\:\st{i})$,
selects a goal in $\goal{i}$, and applies an inference rule (see
below) to obtain a new consistent state $\state_{i+1}$. When no
consistent state can be reached from $\state_i$ the derivation
backtracks. A derivation terminates when a solution state is
reached, otherwise it fails (see Section~\ref{subsec:example}
below for a demonstration of this process). \\

Next we present the inference rules in the ${\cal
A}$\mbox{system}, using the following conventions:
\begin{itemize}
   \setlength{\itemsep}{0cm}
   \item $\Gm{i} = \goal{i} - \{F\}$, where $F$ is the selected goal formula.
   \item \OR\ and \SELECT\ denote nondeterministic choices in an inference
         rule.
   \item Q is a conjunction of literals, possibly empty. Since an
         empty conjunction is equivalent to {\tt true}, the denial
         $\leftarrow Q$ with empty $Q$ is equivalent to {\tt false}.
   \item If $\Delta$, $\Delta^*$, and $\cal E$ are not mentioned, they remain
         unchanged.
\end{itemize}

The inference rules are classified in four groups, named after
the leftmost literal in the selected formula (shown in bold).
Each group contains rules for (positive) conjunctions of literals
and rules for denials.
\begin{enumerate}
   \item {\em Defined predicates:\/} \\
      The inference rules unfold the bodies of a defined predicate.
      For positive conjunctions this corresponds to standard resolution
      with a selected clause, whereas in the denial all clauses are used
      because every clause leads to a new denial.
      \begin{itemize}
         \item [D.1] $\bf p(\ttt)\land Q$: \\
               Let $p(\sss_i) \leftarrow B_i$  $\in {\cal P}$
               ($i = 1,\ldots,n$) be $n$ clauses with $p$ in the head.
               Then: \\
               $\goal{i+1} = \Gm{i} \cup \{\ttt=\sss_1\land B_1 \land Q\}$
               \OR \ \dots \OR \
               $\goal{i+1} = \Gm{i} \cup \{\ttt=\sss_n\land B_n \land Q\}$
         \item [D.2] $\bf \forall \XX (\leftarrow p(\ttt)\land Q)$: \\
               $\goal{i+1} = \Gm{i} \cup \{\forall \XX,\YY (\leftarrow
               \ttt=\sss\land B\land Q)\:|\:\mbox {there is }
               p(\sss) \leftarrow B \in {\cal P} \mbox{ with variables }
               \YY  \}$
      \end{itemize}
   \item {\em Negations:\/} \\
      Resolving negation corresponds to `switching' the mode of reasoning
      from a positive literal to a denial and vice versa. This is
      similar to the idea of negation-as-failure in logic programming.
      \begin{itemize}
         \item [N.1] $\bf \neg p(\ttt)\land Q$: \\
               $\goal{i+1} = \Gm{i} \cup \{Q,\leftarrow p(\ttt)\}$
         \item [N.2] $\bf \forall \XX (\leftarrow \neg p(\ttt)\land Q)$ and
               $\ttt$ does not contain variables in $\XX$: \\
               $\goal{i+1} = \Gm{i} \cup \{p(\ttt)\}$ \OR\
               $\goal{i+1} = \Gm{i} \cup \{\leftarrow p(\ttt), \forall \XX
               (\leftarrow Q) \}$
      \end{itemize}
   \item {\em Abducibles:\/} \\
      The first rule is responsible for the creation of new hypotheses.
      Both rules ensure that the elements in $\Delta$ are consistent
      with those in $\Delta^*$.
      \begin{itemize}
         \item [A.1] $\bf a(\ttt) \land Q$: \\
               \SELECT\ an arbitrary $a(\sss) \in \Delta$ and define
               $\goal{i+1} = \Gm{i} \cup \{Q\} \cup \{\sss=\ttt\}$ \\ \OR\
               $\goal{i+1} = \Gm{i} \cup \{Q\} \cup
               \{\forall \XX (\leftarrow \sss=\ttt\land R) \:|\: \forall \XX
               (\leftarrow a(\sss) \land R) \in \Delta^*_i\}  \cup
               \\ \hspace*{41mm}
               \{\leftarrow(\ttt=\sss)\:|\: a(\sss) \in \Delta_i \} $ and
               $\Delta_{i+1} = \Delta_{i} \cup \{a(\ttt)\}$
         \item [A.2] $\bf \forall \XX (\leftarrow a(\ttt)\land Q)$: \\
               $\goal{i+1} = \Gm{i} \cup \{\forall \XX (\leftarrow \sss=\ttt
               \land Q)\:|\: a(\sss) \in \Delta_i \}$
               and
               $\Delta^*_{i+1} = \Delta^*_i \cup \{\forall \XX (\leftarrow
               a(\ttt)\land Q)\}$
      \end{itemize}
   \item {\em Equalities:\/} \\
      These inference rules isolate the (in)equalities, so that the
      constraint solver can evaluate them. The first  rule applies  to
      equalities in goal formulae:
      \begin{itemize}
         \item [E.1] $\bf s=t \land Q$: \\
               $\goal{i+1} = \Gm{i} \cup \{Q\}$  and
               ${\cal E}_{i+1} = {\cal E}_i \cup \{s=t\}$
      \end{itemize}
      The following three rules handle equalities in denials. Which
      rule applies depends on whether $s$ or $t$ contain free or
      universally quantified variables. In these rules $Q[X/t]$ denotes the
      formula that is obtained from $Q$ by substituting the term $t$ for $X$.
      \begin{itemize}
         \item [E.2] $\bf \forall \XX (\leftarrow s=t \land Q)$: \\
               If $s$ and $t$ are not unifiable then $\goal{i+1} = \Gm{i}$; \\
               Otherwise, let $E_s$ be the equation set in solved form
               representing a most general unifier of $s$ and $t$ \cite{MM82}.
               $\goal{i+1} = \Gm{i} \cup \{ \forall \XX (\leftarrow E_s \land Q)\}$.
         \item [E.3] $\bf \forall X, \YY (\leftarrow X=t \land Q)$
               where $t$ is a term not containing $X$: \\
               $\goal{i+1} = \Gm{i} \cup \{ \forall \YY (\leftarrow Q[X/t]) \}$
        \item [E.4] $\bf \forall \XX,\YY (\leftarrow X=t\land Q)$
               where $X$ is a free variable and $\XX$ is the set of
               universally quantified variables in a term $t$: \\
               ${\cal E}_{i+1} = {\cal E }_{i} \cup \{\forall \XX (X\neq t)\}$
               \OR \ $\goal{i+1} = \Gm{i} \cup \{X=t\} \cup
               \{\forall \YY (\leftarrow Q[X/t]) \}$\footnote
               {In its first branch the inference E.4 explores the condition
               $\forall\XX (X\neq t)$. In the second branch, the negation of this
               condition is explored. Here $X$ is identical to $t$, for some
               values assigned to $\XX$. This is why in the second branch, the
               universally quantified variables $\XX$ are turned into free
               variables which may appear free in $\forall \YY
               (\leftarrow Q[X/t])$. }.
      \end{itemize}
\end{enumerate}

As usual, one has to check for {\em floundering negation\/}. This
occurs when the inference rule N.2 is applied on a denial with
universally quantified variables in the negative literal
$\neg p(\ttt)$. Floundering aborts the derivation. \\

An answer substitution $\theta$, derived from a solution state
$\state$, is any substitution $\theta$ of the free variables in
$\state$ which satisfies ${\cal E}$ (i.e. $\theta({\cal E})$ is
true) and grounds $\Delta$. Note that, in case of an abductive
theory without abducibles and integrity constraints, computed
answers as defined by \citeA{Ll87} are most general unifiers of
${\cal E}$ and correct answers are answer substitutions as
defined above.

\begin{proposition}
  {\rm \fullcite{KvND01}} Let ${\cal T} = ({\cal P},{\cal A},{\cal IC})$
  be an abductive theory, ${\cal Q}$ a query, \state\ a solution state
  of a derivation for ${\cal Q}$, and $\theta$ an answer substitution
  of \state.  Then the pair consisting of the ground abducible atoms
  $\theta(\Delta(\state))$ and of the answer substitution $\theta$ is
  an abductive solution for ${\cal T}$ and ${\cal Q}$.
\end{proposition}


\subsubsection{Constraint Transformation to Denial Form}
\label{IC_2_denial_form}

Since the inference rules of the \asystem\ are applied only on
integrity constraints in denial form, the integrity constraints
${\cal IC}$ in the abductive theory ${\cal T}$ must be translated
to this form. This is done by applying a variant of the
Lloyd-Topor transformation \cite{LT84} on the integrity
constraints \cite<see>{DD98}. This is the same procedure as the
well-known procedure used in deductive databases to convert a
first order quantified query ${\cal Q}$ into a logically
equivalent pair of an atomic query and a non-recursive datalog
procedure. The transformation is defined as a rewriting process
of sets of formulae: the initial set is $\{ \leftarrow \neg F | F
\in {\cal IC}\}$, and the transformation is done by applying De
Morgan and various distribution rules. New predicates and rules
may be introduced during the transformation in order to deal with
universal quantifications in denials. Below we illustrate the
transformation in the case of the integrity constraints of the
running example.

\begin{example}
\label{example:teachers_extended}
 {\rm Consider the following extension of the integrity constraints of
  Example~\ref{example:teachers}: \vspace{2mm} \\
  \hspace*{15mm} ${\cal IC} =
     \{ \: \forall X \forall Y \forall Z \: (teaches(X,Y) \wedge teaches(X,Z) \,
           \rightarrow \, Y = Z ) \:,\: \vspace{1mm} \\
  \hspace*{29mm} \forall X \: (teacher(X) \, \rightarrow \, \exists Y
  teaches(Y,X)) \: \}$. \vspace{2mm} \\
  Note that in addition to the original integrity constraint of
  Example~\ref{example:teachers}, here we also demand that every
  teacher has to give at least one course.
\begin{itemize}
   \item Lloyd-Topor transformation on the first integrity constraint:
         \begin{description}
           \item[(1)] $\leftarrow \neg \forall X\: \forall Y\: \forall Z\:
                       (\neg teaches(X,Y) \lor \neg teaches(X,Z) \lor Y = Z )$
           \item[(2)] $\leftarrow \exists X\: \exists Y\: \exists Z\:
                       (teaches(X,Y) \land teaches(X,Z) \land Y \neq Z)$
           \item[(3)] $\forall X\: \forall Y\: \forall Z\:
                       (\leftarrow teaches(X,Y) \wedge teaches(X,Z)
                        \wedge Y \neq Z)$
         \end{description}
   \item Lloyd-Topor transformation on the second integrity constraint:
         \begin{description}
           \item[(1)] $\leftarrow \neg \forall X \:
                       (\neg teacher(X) \lor \exists Y  teaches(Y,X))$
           \item[(2)] $\forall X \: (\leftarrow teacher(X) \land
                       \neg \exists Y teaches(Y,X))$
           \item[(3)] $\forall X \: (\leftarrow teacher(X) \land \neg
                       gives\_courses(X))$ where $gives\_courses$ is defined by: \\
                      $gives\_courses(X) \leftarrow \exists Y \: teaches(Y,X)$
           \item[(4)] $\forall X \: (\leftarrow teacher(X) \land \neg
                       gives\_courses(X))$, and  \\
                      $gives\_courses(X) \leftarrow teaches(Y,X)$
         \end{description}
\end{itemize}
} \end{example}


\subsubsection{Control Strategy}

The selection strategy applied during the derivation process is
crucial. A Prolog-like selection strategy (left first, depth
first) often leads to trashing, because it is blind to other
choices, and it does not result in a global overview of the
current state of the computation. In the development of the
\asystem\ the main focus was on the improvement of the control
strategy. The idea is to apply first those rules that result in a
deterministic change of the state, so that information is
propagated. If none of such rules is applicable, then one of the
left over choices is selected. By this strategy, commitment to a
choice is suspended until the moment where no other information
can be derived in a deterministic way. This resembles a
CLP-solver, in which the constraints propagate their information
as soon as a choice is made.  This propagation can reduce the
number of choices to be made and thus often dramatically
increases the performance.


\subsubsection{Implementation}
\label{subsec:implementation}

In this section we describe the structure of our implementation.
Figure~\ref{fig:asystem} shows a layered view. The upper-most
level consists of the specific abductive logic theory of the
integration task, i.e., the database information and the integrity
constraints. This layer together with the composer form the
abductive meta-theory (see Section~\ref{subsec:meta}) that is
processed by the ${\cal A}$\mbox{system}. \\

\begin{figure}[ht]
\begin{picture}(146,72)(-15,0)
% knowledge bases
 \put(30,62){\framebox(10,10){ \shortstack[l]{$\DB_{1}$}}}
 \put(45,62){\framebox(10,10){ \shortstack[l]{$\DB_{2}$}}}
 \put(63,65){$\cdots\cdots$}
 \put(85,62){\framebox(10,10){ \shortstack[l]{$\DB_{n}$}}}
% connection
 \put(35,62){\line(0,-1){5}}
 \put(50,62){\line(0,-1){5}}
 \put(90,62){\line(0,-1){5}}
% composer
 \put(30,47){\framebox(65,10){ \shortstack[l]{Composer}}}
% connection
 \put(60,47){\line(0,-1){5}}
% asystem
 \put(30,32){\framebox(65,10){ \shortstack[l]{Optimizer}}}
 \put(60,32){\line(0,-1){5}}
 \put(30,17){\framebox(65,10){
             \shortstack[l]{ \asystem\ (based on SLDNFA)}}}
 \put(60,17){\line(0,-1){5}}
 \put(30,02){\framebox(65,10){ \shortstack[l]{Sicstus Prolog}}}
 \put(25,00){\dashbox{2}(76,44)}
% on the left
 \put(11,65){\vector(0,1){7}}
 \put(2,61){ Abductive }
 \put(4,57){ Theory }
 \put(11,55){\vector(0,-1){8}}
 \put(11,33){\vector(0,1){12}}
 \put(2,29){ Abductive}
 \put(4,25){ System }
 \put(11,23){\vector(0,-1){23}}
% on the right
 \put(115,68){\vector(0,1){4}}
 \put(111,65){Input}
 \put(115,63){\vector(0,-1){5}}
 \put(115,43){\vector(0,1){14}}
 \put(107,39){Composing}
 \put(110,35){System}
 \put(115,33){\vector(0,-1){33}}
\end{picture}
\caption{A schematic view of the system components.}
\label{fig:asystem}
\end{figure}

As noted above, the {\em composer\/} consists of a meta-theory for
integrating the databases in a coherent way. It is interpreted
here as an abductive theory, in which the abducible predicates
provide the information on how to restore the consistency of the
amalgamated data. \\

The abductive system (enclosed by dotted lines in
Figure~\ref{fig:asystem}) consists of three main components: a
finite domain constraint solver (part of Sicstus Prolog), an
abductive meta-interpreter (described in the previous sections),
and an optimizer. \\

The {\em optimizer\/} is a component that, given a preference
criterion on the space of the solutions, computes only the
most-preferred (abductive) solutions. Given such a preference
criterion, this component prunes `on the fly' those branches of
the search tree that lead to solutions that are worse than others
that have already been computed. This is actually a branch and
bound `filter' on the solutions space, that speeds-up execution
and makes sure that only the desired solutions will be
obtained\footnote{See also the third item of
Note~\ref{note:main_example} (at the end of
Section~\ref{subsec:example}).}. If the preference criterion is a
pre-order, then the optimizer is {\em complete\/}, that is, it
can compute all the optimal solutions (more about this in
Section~\ref{section:soundness_completeness}). Moreover, this is
a general-purpose component, and it may be useful not only for
data integration, but also for, e.g., solving planning problems.


\subsubsection{Complexity}

It is well-known that in general, the task of repairing a database
is not tractable, as there may be an exponential number of
different ways of repairing it. Even in cases where integrity
constraints are assumed to be single-headed dependencies
\cite{GZ00}, checking whether there exists a $\leq$-repaired
database in which a certain query ${\cal Q}$ is satisfied, is in
$\Sigma_{2}^{P}$. Checking if a fact is satisfied by {\em all\/}
the $\leq$-repaired databases is in $\Pi_{2}^{P}$
\cite<see>{GZ00}. This is not surprising in light of the
correspondence between computations of $\leq$-minimal repairs and
computations of entailment relations defined by maximally
consistent models (see Propositions
\ref{prop:repair_3}--\ref{prop:repair_6}), also known to be on
the second level of the polynomial hierarchy. \\

A pure upper bound for the ${\cal A}$\mbox{system} is still
unknown, since -- to the best of our knowledge -- no complexity
results on SLDNFA refutation procedure are available.


\subsection{Example: A Derivation of Repairs by the ${\cal A}$\mbox{system}}
\label{subsec:example}

Consider again Example~\ref{example:teachers_extended}. The
corresponding meta-theory (assuming that the Lloyd-Topor
transformation has been applied on it) is given in
Figure~\ref{fig:main_example}. In this case, and in what follows,
we shall assume that all variables in the denials are universally
quantified, and so, in order to reduce the amount of notations,
universal quantifiers are omitted from the denial rules. \\

\begin{figure}[ht]
\begin{center}
\framebox[12.8cm]{
\begin{minipage}{12cm}
\begin{enumlist}
\setlength{\itemsep}{-0.1cm} {\tt
 \item
 \item db(teacher(n$_1$))
 \item db(teacher(n$_2$))
 \item db(teacher(n$_3$))
 \item db(teaches(c$_1$,n$_1$))
 \item db(teaches(c$_2$,n$_2$))
 \item db(teaches(c$_2$,n$_3$))
 \item
 \item $\leftarrow$ fact(teaches(X,Y)) $\wedge$ fact(teaches(X,Z)) $\wedge \
       $(Y $\neq$ Z) \hfill ({\bf ic1})
 \item $\leftarrow$ fact(teacher(X)) $\wedge$ $\neg$gives\_courses(X)
       \hfill ({\bf ic2})
 \item gives\_courses(X) $\leftarrow$ fact(teaches(Y,X)) \
 \item
 \item fact(X) $\leftarrow$ db(X) $\wedge$ $\neg$retract(X)
 \item fact(X) $\leftarrow$ insert(X)
 \item $\leftarrow$ insert(X) $\wedge$ db(X) \hfill ({\bf composer-ic1})
 \item $\leftarrow$ retract(X) $\wedge$ $\neg$db(X) \hfill ({\bf composer-ic2}) }
\item
\end{enumlist}
\end{minipage}
} \end{center}
 \caption{A meta-theory for Example \ref{example:teachers_extended}.}
 \label{fig:main_example}
\end{figure}

We have executed the code of Figure~\ref{fig:main_example}, as
well as other examples from the literature in our system. As
Theorem~\ref{completeness_2} in Section
\ref{section:soundness_completeness} guarantees, the output in
each case is the set of the most preferred solutions of the
corresponding problem. In what follows we demonstrate how some of
the most preferred solutions for the meta-theory above are
computed. \\
% by the ${\cal A}$\mbox{system}.

We follow one branch in the refutation tree, starting from the
initial state $({\cal G}_{0},\st{0})$, where the initial set of
goals is ${\cal G}_{0} = \{`{\tt true}'$, {\bf ic1}, {\bf ic2},
{\bf composer-ic1}, {\bf composer-ic2}$\}$, and the initial store
is $\st{0} = (\emptyset,\emptyset,\emptyset)$. Suppose that the
first selected formula is \vspace{2mm} \\
 $ F_1 \ = \ {\bf ic1} \ =
           \ \leftarrow {\tt fact(teaches(X,Y))} \wedge
                        {\tt fact(teaches(X,Z))} \wedge
                        {\tt (Y \neq Z)}.$ \vspace{2mm} \\
Then, by D.2, \vspace{2mm} \\
 $ {\cal G}_1 \ = \ {\cal G}_0 \ \setminus F_1 \ \cup
           \vspace{1mm} \\ \hspace*{5mm} \{ \:
           \leftarrow {\tt db(teaches(X,Y))} \wedge
                      \neg {\tt retract(teaches(X,Y))} \wedge
                      {\tt fact(teaches(X,Z))} \wedge {\tt (Y \neq Z)},
                      \vspace{1mm} \\ \hspace*{6mm}
           \leftarrow {\tt insert(teaches(X,Y))} \wedge
                      {\tt fact(teaches(X,Z))} \wedge {\tt (Y \neq Z)} \:\},$
                      \vspace{2mm} \\
and $\st{1} = \st{0}$. Now, pick \vspace{2mm} \\
 $ F_2 \ =  \ \leftarrow {\tt db(teaches(X,Y))} \wedge
                         \neg {\tt retract(teaches(X,Y))} \wedge
                         {\tt fact(teaches(X,Z))} \wedge {\tt (Y \neq Z)}$.
                         \vspace{2mm} \\
Select {\tt db(teaches(X,Y))}, unfold all the corresponding atoms in the database,
and then, again by D.2, followed by E.2 and E.3, \vspace{2mm} \\
 $ {\cal G}_2 \ = \ {\cal G}_1 \ \setminus F_2 \ \cup
           \vspace{1mm} \\ \hspace*{5mm} \{ \:
           \leftarrow \neg {\tt retract(teaches(c_1,n_1))} \wedge
                      {\tt fact(teaches(c_1,Z))} \wedge {\tt (n_1 \neq Z)},
                      \vspace{1mm} \\ \hspace*{6mm}
           \leftarrow \neg {\tt retract(teaches(c_2,n_2))} \wedge
                      {\tt fact(teaches(c_2,Z))} \wedge {\tt (n_2 \neq Z)},
                      \vspace{1mm} \\ \hspace*{6mm}
           \leftarrow \neg {\tt retract(teaches(c_2,n_3))} \wedge
                      {\tt fact(teaches(c_2,Z))} \wedge {\tt (n_3 \neq Z)} \:\},$
                      \vspace{2mm} \\
and still $\st{2} = \st{1}$. Pick then the second denial among
the new goals that were added to ${\cal G}_2$. Denote this denial
$F_3$. Since $F_3$ starts with a negated literal, N.2 applies, and
the derivation process splits here to two branches. The second
branch contains \vspace{2mm} \\
 $ {\cal G}_3 \ = \ {\cal G}_2 \ \setminus F_3 \ \cup \ \{ \:
           \leftarrow {\tt retract(teaches(c_2,n_2))}, \
           \leftarrow {\tt fact(teaches(c_2,Z))} \wedge {\tt (n_2 \neq Z)} \:\},$
                      \vspace{2mm} \\
\noindent and still $\st{3} = \st{2}$. Choose now the first new
goal, i.e.,
\vspace{2mm} \\
 $ F_4 \ = \ \leftarrow {\tt retract(teaches(c_2,n_2))}$. \vspace{2mm} \\
Now, since $\Delta_3 = \emptyset$, the only option is to add
$F_4$ to $\Delta_3^*$. Thus, by A.2, \vspace{2mm} \\
 $ {\cal G}_4 \ = \ {\cal G}_3 \ \setminus F_4$ and $\st{4} =
   (\emptyset,\{F_4\},\emptyset)$. \vspace{2mm} \\
Assume, now, that we take the second new goal of ${\cal G}_3$: \vspace{2mm} \\
 $ F_5 \ = \ \leftarrow {\tt fact(teaches(c_2,Z))} \wedge {\tt (n_2 \neq Z)}$.
 \vspace{2mm} \\
Following a similar process of unfolding data as described above,
using ${\tt db(teaches(c_2,n_3))}$, we end-up with \vspace{2mm} \\
 $\leftarrow {\tt retract(teaches(c_2,n_3))} \wedge {\tt (n_2 \neq n_3)}$.
 \vspace{2mm} \\
Selecting the negative literal ${\tt (n_2 \neq n_3)}$, N.2 applies
again. The first branch quickly results in failure after adding
${\tt (n_2 = n_3)}$ to ${\cal E}$. The second branch adds ${\tt
\leftarrow (n_2 = n_3)}$ and ${\tt retract(teaches(c_2,n_3))}$ to
the set of goals. The former one is added to the constraint store,
as ${\tt (n_2 \neq n_3)}$, and simplifies to true. Assume the
latter is selected next. Let this be the $i$-th step. We have
that by now $\Delta_{i-1}$ (the set of abducible predicates
produced until the current step) is empty, thus the only option
is to abduce ${\tt retract(teaches(c_2,n_3))}$. Thus, by A.1,
$\st{i}$ consists of:
\vspace{2mm} \\
 $\Delta_i = \{{\tt retract(teaches(c_2,n_3))}\}$, \ \
 $\Delta_i^* = \{F_4\} = \{\leftarrow {\tt retract(teaches(c_2,n_2))} \}$,
 \vspace{1mm} \\
 ${\cal E}_i = {\cal E}_{i-1}$, \ and \vspace{1mm} \\
 $ {\cal G}_i \ = \ {\cal G}_{i-1} \ \setminus
           \{{\tt retract(teaches(c_2,n_3))}\} \ \cup \
           \{ \leftarrow {\tt teaches(c_2,n_2)} =
                         {\tt teaches(c_2,n_3)} \}$. \vspace{2mm} \\
As the last goal is certainly satisfied, {\bf ic1} is resolved in this branch. \\

Now we turn to {\bf ic2}. So: \vspace{2mm} \\
 $F_{i+1} \ = \ {\bf ic2} \ = \
 \leftarrow {\tt fact(teacher(X))} \wedge \neg {\tt gives\_courses(X)}.$
 \vspace{2mm} \\
The evaluation of $F_{i+1}$ for either $x = n_1$ or $x = n_2$ is
successful, so the only interesting case is when $x = n_3$. In
this case the evaluation leads to the goal {\tt
gives\_courses(X)}. Unfolding this goal yields that ${\tt
fact(teaches(Y,n_3))}$ appears in the goal set. In order to
satisfy this goal, it should be resolved either with one of the
composer's rules (using D.1). The first rule (i.e., {\tt fact(X)
$\leftarrow$ db(X) $\wedge \neg$ retract(X)}) leads to a failure
(since ${\tt retract(teaches(c_2,n_3))}$ is already in $\Delta$),
and so the second rule of the composer, {\tt fact(X) $\leftarrow$
insert(X)}, must be applied. This leads to the abduction of ${\tt
insert(teaches(Y,n_3))}$. By {\bf ic1}, ${\tt Y \neq c_1}$ and
${\tt Y \neq c_2}$ is derived\footnote{One can verify that these
constraints are indeed detected during the derivations process.
We omit the details here in order to keep this example
tractable.}. Also, {\bf composer-ic1} and {\bf composer-ic2} are
satisfied by the current state, so eventually the solution state
that is reached from the derivation path described here, contains
the following sets: \vspace{2mm} \\
  \hspace*{22mm} $\Delta = \{ {\tt retract(teaches(c_2,n_3))}, \:
                              {\tt insert(teaches(Y,n_3))} \}$, \vspace{1mm} \\
  \hspace*{22mm} ${\cal E} = \{ {\tt Y \neq c_1} , {\tt Y \neq c_2}  \}$,
                 \vspace{2mm} \\
which means retraction of ${\tt teaches(c_2,n_3)}$ and insertion
of ${\tt teaches(Y,n_3)}$ for some ${\tt Y \neq c_1}$ and ${\tt Y
\neq c_2}$. The other solutions are obtained in a similar way.

\begin{note}
\label{note:main_example}
 {\rm Below are some remarks on the above derivation process.
\begin{enumerate}
   \item The solution above contains a non-ground abducible
         predicate. This indeed is the expected result, since this solution
         resolves the contradiction with the integrity constraint {\bf ic1}
         by removing the assumption that teacher $n_3$ teaches course $c_2$.
         As a result, teacher $n_3$ does not teach any course. Thus, in
         order to assure the other integrity constraint ({\bf ic2}), the
         solution indicates that $n_3$ must teach {\em some\/}
         course (other than $c_1$ and $c_2$).
   \item One possible (and realistic) explanation for the cause of the
         inconsistency in the database of
         Example~\ref{example:teachers_extended} and
         Figure~\ref{fig:main_example}, is a typographic error. It might
         happen, for instance, that {\tt c$_2$} was mistakenly typed
         instead of, say, {\tt c$_3$}, in {\tt teaches(c$_2$,n$_3$)}.
         In this case, the database repair computed above pinpoints
         this possibility (in our case, then, {\tt Y} should be equal to
         {\tt c$_3$})\footnote{The variable {\tt Y} is free and
         $\{{\tt Y}/{\tt c}_3\}$ is an answer substitution as it grounds
         $\Delta$ and satisfies ${\cal E}$.}. This explanation cannot be
         explicitly captured, unless particular repairs with non-ground
         solutions are constructed, as indeed is the case here.
         While some other approaches that have been recently introduced
         \cite<e.g.,>{BB03,CLR03} properly capture cases such as those of
         Example~\ref{example:teachers_extended}, to the best
         of our knowledge, no other {\em application\/} of database
         integration has this ability.
   \item Once the system finds a solution that corresponds to a goal
         state $\state_g = ({\cal G}_g,\st{g})$ with ${\cal G}_{g} =
         \emptyset$ and $\st{g} = (\Delta_g,\Delta_g^*,{\cal E}_{g})$,
         the $\leq_i$-optimizer may be used such that whenever a state
         $\state = ({\cal G}_s,(\Delta_s,\Delta_s^*,{\cal E}_{s}))$
         is reached, and $|\Delta_g| < |\Delta_s|$, the corresponding
         branch of the tree is pruned\footnote{As the size of $\Delta_s$
         can only increase along the derivation, the state $\state$ cannot
         lead to a solution that is better than the one induced by
         $\state_g$, and so the corresponding branch of the tree can indeed
         be pruned.}.
\end{enumerate}
} \end{note}


\subsection{Soundness and Completeness}
\label{section:soundness_completeness}

In this section we give some soundness and completeness results for the
${\cal A}$\mbox{system}, and relate these results to the model-based
preferential semantics, considered in
Section~\ref{section:model_theoretic_analysis}. \\

In what follows we denote by ${\cal T}$ an abductive meta-theory
(constructed as described in Section~\ref{subsec:meta}) for
composing $n$ given databases $\DB_{1},\ldots,\DB_{n}$. Let also
$\ProcALP$ be some sound abductive proof procedure for ${\cal
T}$\footnote{That is, $\ProcALP$ is a process for computing only
the abductive solutions of ${\cal T}$, in the sense of
Definition~\ref{def:abductive_solutions}.}. The following
proposition shows that $\ProcALP$ provides a coherent method for
integrating the databases that are represented by ${\cal T}$.

\begin{proposition}
\label{soundness} Every abductive solution that is obtained by
$\ProcALP$ for the query `${\tt true}$' on a theory ${\cal T}$,
is a repair of $\UDB$.
\end{proposition}

\noindent{\em Proof:} By the construction of ${\cal T}$ it is
easy to see that all the conditions that are listed in
Definition~\ref{def:repair} are satisfied. Indeed, the first two
conditions are assured by the integrity constraints of the
composer. The last condition is also met since by the soundness
of $\ProcALP$ it produces abductive solutions $\Delta_{i}$ for a
query `${\tt true}$' on ${\cal T}$. Thus, by the second property
in Definition~\ref{def:abductive_solutions}, for every such
solution $\Delta_{i} = (\xIn_{i},\xOut_{i})$ we have that ${\cal
P} \cup \Delta_{i} \models {\cal IC}$. Since ${\cal P}$ contains
a data section with all the facts, it follows that ${\cal D} \cup
\Delta_{i} \models {\cal IC}$, i.e. every integrity constraints
follows from ${\cal D} \cup \xIn_{i}
\setminus \xOut_{i}$. \hfill$\Box$ \\

As SLDNFA is a sound abductive proof procedure \cite{DD98}, it
can be taken as the procedure $\ProcALP$, and so
Proposition~\ref{soundness} provides a soundness theorem for the
current implementation of the ${\cal A}$\mbox{system}. When an
optimizer is incorporated in the ${\cal A}$system, we have the
following soundness result for the extended system:

\begin{theorem}
\label{soundness_2}
 {\rm (Soundness)} Every output that is obtained by the query
 `${\tt true}$' on ${\cal T}$, where the \asystem\ is executed
  with a $\leq_{c}$-optimizer {\rm[}respectively, with an
  $\leq_{i}$-optimizer{\rm]}, is a $\leq_{c}$-preferred repair
  {\rm[}respectively, an $\leq_{i}$-preferred repair{\rm]} of $\UDB$.
\end{theorem}

\noindent{\em Proof:} Follows from Proposition~\ref{soundness}
(since the \asystem\ is based on SLDNFA which is a sound abductive
proof procedure), and the fact that the $\leq_{c}$-optimizer
prunes paths that lead to solutions that are not
$\leq_{c}$-preferable. Similar arguments hold for systems with an
$\leq_{i}$-optimizer. \hfill$\Box$

\begin{proposition}
\label{completeness}
 Suppose that the query `${\tt true}$' has a finite SLDNFA-tree w.r.t.
 ${\cal T}$. Then every $\leq_{c}$-preferred repair and every
 $\leq_{i}$-preferred repair of $\UDB$ is obtained by running
 ${\cal T}$ in the \asystem.
\end{proposition}

\noindent{\em Outline of proof:} The proof that all the abductive
solutions with minimal cardinality are obtained by the system is
based on Theorem~10.1 of \citeR{DD98}, where it is shown that
SLDNFA$^{o}$, which is an extension of SLDNFA, aimed for
computing solutions with minimal cardinality, is complete; see
\citeR[Section 10.1,]{DD98} for further details. Similarly, the
proof that all the abductive solutions which are minimal w.r.t.
set inclusion are obtained by the system is based on Theorem~10.2
of \citeR{DD98}, that shows that SLDNFA$_{+}$, which is another
extension of SLDNFA, aimed for computing minimal solutions w.r.t.
set inclusion, is also complete; see \citeR[Section 10.2,]{DD98}
for further details.

Now, the \asystem\ is based on the combination of SLDNFA$^{o}$ and
SLDNFA$_{+}$. Moreover, as this system does not change the
refutation tree (but only controls the way rules are selected),
Theorems 10.1 and 10.2 in \citeA{DD98} are applicable in our case
as well. Thus, all the $\leq_{c}$- and the $\leq_{i}$-minimal
solutions are produced. This in particular means that every
$\leq_{c}$-preferred repair as well as every $\leq_{i}$-preferred
repair of $\UDB$ is produced by our system. \hfill$\Box$ \\

It should be noted that the last proposition does not guarantee
that non-preferred repairs will not be produced (as this is not
true in general). However, as the following theorem shows, the use
of an optimizer excludes this possibility.

\begin{theorem}
\label{completeness_2} {\rm (Completeness)} In the notations of
Proposition~\ref{completeness} and under its assumptions, the
output of the execution of ${\cal T}$ in the \asystem\ together
with a $\leq_{c}$-optimizer {\rm[}respectively, together with an
$\leq_{i}$-optimizer{\rm]} is exactly $!(\UDB,\leq_{c})$
{\rm[}respectively, $!(\UDB,\leq_{i})${\rm]}.
\end{theorem}

\noindent{\em Proof:} We shall show the claim for the case of
$\leq_{c}$; the proof w.r.t. $\leq_{i}$ is similar.

Let $(\xIn,\xOut) \!\in \ !(\UDB,\leq_{c})$. By
Proposition~\ref{completeness}, $\Delta = (\xIn,\xOut)$ is one of
the solutions produced by the \asystem\ for ${\cal T}$. Now,
during the execution of the system together with the
$\leq_{c}$-optimizer, the path that corresponds to $\Delta$
cannot be pruned from the refutation tree, since by our assumption
$(\xIn,\xOut)$ has a minimal cardinality among the possible
solutions, so the pruning condition is not satisfied. Thus
$\Delta$ will be produced by the $\leq_{c}$-optimized system. For
the converse, suppose that $(\xIn,\xOut)$ is some repair of $\UDB$
that is produced by the $\leq_{c}$-optimized system. Suppose for
a contradiction that $(\xIn,\xOut) \!\not\in \ !(\UDB,\leq_{c})$.
By the proof of Proposition~\ref{completeness}, there is some
$\Delta' = (\xIn',\xOut') \!\in \ !(\UDB,\leq_{c})$ that is
constructed by the \asystem\ for ${\cal T}$, and $(\xIn',\xOut')
\!<_{c}\! (\xIn,\xOut)$. But $|\Delta'| < |\Delta|$, and so the
$\leq_{c}$-optimizer would prune the path of the $\Delta$
solution once its cardinality becomes bigger than $|\Delta'|$.
This contradicts our assumption that $(\xIn,\xOut)$ is produced
by the $\leq_{c}$-optimized system. \hfill$\Box$

\begin{note}
{\rm The SLDNFA-resolution on which the \asystem\ is based is an
extension of SLDNF-resolution \cite{Ll87} and coincides with it
for logic programs with empty sets of abducible predicates.
SLDNF-resolution is complete only if its computation always
terminates. SLDNFA inherits this property. This is the reason why
the condition of a finite SLDNFA-tree is imposed in Proposition
\ref{completeness} and Theorem \ref{completeness_2}. Like SLDNF,
the termination of SLDNFA can be guaranteed by imposing syntactic
conditions on the program. We refer to \cite{Ve99}, where some
conditions are proposed to guarantee the existence of a finite
SLDNFA-tree.

In the context of our paper, floundering would arise in the
presence of unsafe integrity constraints (e.g.,  $\forall x\:
p(x)$). One way to eliminate this problem is to use a unary
domain predicate $dom$, ranging over the objects of the database,
and to add a range for each quantified variable in the integrity
constraints, so that we obtain formulae of the form $\forall x
(dom(x) \rightarrow \psi(x))$ and $\exists x (dom(x)\land
\psi(x))$.
} \end{note}

The following results immediately follow from the propositions
above and those of Section~\ref{section:model_theoretic_analysis}
(unless explicitly said, the \asystem\ is without optimizer).

\begin{corollary}
\label{sound_complete_1}
 Suppose that the query `${\tt true}$' has a finite SLDNFA
 refutation tree w.r.t. input theory ${\cal T}$. Then:
 \begin{enumerate}
    \item for every output $(\xIn,\;\xOut)$ of the \asystem\
          there is a classical model $M$ of ${\cal IC}$ s.t.
          $\xIn = M^{t} \setminus {\cal D}$ and $\xOut = {\cal D}
          \setminus M^{t}$.
    \item for every output $(\xIn,\;\xOut)$ of the \asystem\
          there is a 3-valued model $N$ of ${\cal D} \cup {\cal IC}$ s.t.
          $\xIn^{N} \!=\! \xIn$ and $\xOut^{N} \!=\! \xOut$.
 \end{enumerate}
\end{corollary}

\begin{corollary}
\label{sound_complete_2}
 In the notations of Corollary~\ref{sound_complete_1} and under its
 assumption, we have that:
 \begin{enumerate}
    \item for every output $(\xIn,\;\xOut)$ that is obtained by
          running the \asystem\ together with an $\leq_{i}$-optimizer
          {\rm[}respectively, together with a $\leq_{c}$-optimizer{\rm]},
          there is an $\leq_{i}$-maximally consistent element
          {\rm[}respectively, a $\leq_{c}$-maximally consistent
          element{\rm]} $N$ in ${\cal M}^{\UDB}$ s.t. $\xIn^{N} = \xIn$
          and $\xOut^{N} = \xOut$.
    \item for every $\leq_{i}$-maximally consistent element
          {\rm[}respectively, $\leq_{c}$-maximally consistent element{\rm]}
          $N$ in ${\cal M}^{\UDB}$ there is a solution $(\xIn,\;\xOut)$ that
          is obtained by running the \asystem\ together with an
          $\leq_{i}$-optimizer {\rm[}respectively, together with a
          $\leq_{c}$-optimizer{\rm]} s.t. $\xIn = \xIn^{N}$ and
          $\xOut = \xOut^{N}$.
 \end{enumerate}
\end{corollary}

The last corollaries show that the operational semantics, induced
by the ${\cal A}$\mbox{system}, can also be represented by a
preferential semantics, in terms of preferred models of the
theory. The set ${\cal R}(\UDB,\leq)$ that represents the intended
meaning of how to `$\leq$-recover' the database $\UDB$, can
therefore be obtained computationally, by the set
\[\{(\xIn,\xOut)~|~(\xIn,\xOut) \mbox{ is an output of the
                   ${\cal A}$system with an $\leq$-optimizer} \},\]
or, equivalently, it can be described in terms of preferred models of the
theory, by the following set:
\[\{(\xIn^{N},\xOut^{N})~|~N \mbox{ is $\leq$-maximally consistent in }
                   {\cal M}^{\UDB} \}. \]


\subsection{Handling Specialized Information}
\label{subsec:specialized_information}

The purpose of this section is to demonstrate the potential usage
of our system in more complex scenarios, where various kinds of
specialized data are incorporated in the system. In particular,
we briefly consider time information  and source identification.
We also give some guidelines on how to extend the system with
capabilities of handling these kinds of information.


\subsubsection{Timestamped Information}
\label{subset:timestamp_info}

Many database applications contain temporal information. This
kind of data may be divided in two types: time information that
is part of the data itself, and time information that is related
to database operations (e.g., records on database update time).
Consider, for instance, {\tt \small
birth\_day(John,15/05/2001)}$_{{\tt 16/05/2001}}$. Here, John's
date of birth is an instance of the former type of time
information, and the subscripted data that describes the time in
which this fact was added to the database, is an instance of the
latter type of time information. \\

In our approach, timestamp information can be integrated by
adding a temporal theory describing the state of the database at
any particular time point. One way of doing so is by using {\em
situation calculus\/}. In this approach a database is described
by some initial information and a history of events performed
during the database lifetime \cite<see>{Re95}. Here we use a
different approach, which is based on {\em event calculus\/}
\cite{KS86}. The idea is to make a distinction between two kinds
of events, {\tt add\_db} and {\tt del\_db}, that describe the
database modifications, and the composer-driven events {\tt
insert} and {\tt retract} that are used for constructing database
repairs. In this view, the extended composer has the following
form: \vspace{2mm}

\smallskip
\noindent
 \hspace*{5mm} {\tt holds\_at(P,T) $\leftarrow$
                    initially(P) $\wedge$ $\neg$clipped(0,P,T) }  \\
 \hspace*{5mm} {\tt holds\_at(P,T) $\leftarrow$
                    add(P,E) $\wedge$ E<T $\wedge$ $\neg$clipped(E,P,T) }
 \vspace{2mm} \\
 \hspace*{5mm} {\tt clipped(E,P,T) $\leftarrow$
                    del(P,C) $\wedge$ E$\leq$C, C<T }
 \vspace{2mm} \\
 \hspace*{5mm} {\tt add(P,T) $\leftarrow$ add\_db(P,T) } \\
 \hspace*{5mm} {\tt add(P,T) $\leftarrow$ insert(P,T)  } \\
 \hspace*{5mm} {\tt del(P,T) $\leftarrow$ del\_db(P,T) } \\
 \hspace*{5mm} {\tt del(P,T) $\leftarrow$ retract(P,T) }
 \vspace{2mm} \\
 \hspace*{5mm} {\tt $\leftarrow$ insert(P,T) $\wedge$ retract(P,T) } \\
 \hspace*{5mm} {\tt $\leftarrow$ insert(P,T) $\wedge$ add\_db(P,T) } \\
 \hspace*{5mm} {\tt $\leftarrow$ retract(P,T) $\wedge$ del\_db(P,T) }
 \vspace{2mm}

Note that in the above extended representation, the integrity
constraints must be carefully specified. Consider, e.g. the
statement that a person can be born only on one date:
% \vspace{2mm}

\smallskip
\noindent
 \hspace*{5mm} {\tt $\leftarrow$  holds\_at(birth\_day(P,D1),T) $\wedge$
                                  holds\_at(birth\_day(P,D2),T) $\wedge$
                                  D1$\neq$D2} \vspace{2mm}

The problem here is that to ensure consistency, this constraint
must be checked at every point in time. This may be avoided by a
simple rewriting that ensures that the constraint will be
verified only when an event for that person occurs: \vspace{2mm}

\smallskip
\noindent
 \hspace*{5mm} {\tt ic(P,T) $\leftarrow$
                    holds\_at(birth\_day(P,D1),T) $\wedge$
                    holds\_at(birth\_day(P,D2),T) $\wedge$ D1$\neq$D2} \\
 \hspace*{5mm} {\tt $\leftarrow$
                    add\_db(birth\_day(P,\_),T) $\wedge$ NT = T+1 $\wedge$
                    ic(P,NT)} \\
 \hspace*{5mm} {\tt $\leftarrow$
                    insert(birth\_day(P,\_),T) $\wedge$ NT = T+1 $\wedge$
                    ic(P,NT)} \\
 \hspace*{5mm} {\tt $\leftarrow$ ic(P,0)}

\begin{note}
{\rm In the last example we have used {\em temporal integrity
constraints\/} in order to resolve contradicting update events.
Clearly, contradicting events do not necessarily yield a
classically inconsistent database, and so the role of such
integrity constraints is to express possible events in terms of
time and causation, and -- if necessary -- describe their
consequence as a violation of consistency.

Instead of using temporal integrity constraints and event
calculus, one could repair a database with time-stamps by using
some time-based criterion for making preferences among its
repairs. For instance, denote by ${\tt
db}(x_{1},\ldots,x_{n})_{{\tt t}}$ that the data-fact ${\tt
db}(x_{1},\ldots,x_{n})$ has a timestamp ${\tt t}$, and suppose
that $(\xIn,\xOut)$ and $(\xIn',\xOut')$ are two repairs of a
database $\xDB$. A time-based criterion for preferring
$(\xIn,\xOut)$ over $(\xIn',\xOut')$ could state, e.g., that for
every data-fact ${\tt db}(x_{1},\ldots,x_{n})$ and timestamps
${\tt t}_{1},{\tt t}_{2}$ s.t. ${\tt
db}(x_{1},\ldots,x_{n})_{{\tt t}_{1}}$ follows from ${\cal D}
\cup \xIn \setminus \xOut$ and ${\tt
db}(x_{1},\ldots,x_{n})_{{\tt t}_{2}}$ follows from ${\cal D}
\cup \xIn' \setminus \xOut'$, necessarily ${\tt t}_{1} \geq {\tt
t}_{2}$. A more detailed treatment of this issue is outside the
scope of this paper. } \end{note}

The interested reader may refer, e.g., to \cite{Sr95,MB99} for a
detailed discussion on the use of logic programming based
approaches to the specification of temporal databases. Such
specifications can be easily combined with those for repairs,
given above.


\subsubsection{Keeping Track of Source Identities}

There are cases in which it is important to preserve the identity of the
database from which a specific piece of information was originated. This is
useful, for instance, when one wants to make preferences among different
sources, or when some specific source should be filtered out (e.g, when
the corresponding database is not available or becomes unreliable).
This kind of information may be decoded by adding another argument to every
fact, which denotes the identity of its origin. This requires minor
modifications in the basic composer, since the composer controls the way
in which the data is integrated. As such, it is the only component that can
keep track on the source of the information. \\

Suppose, then, that for every database fact we add another
argument that identifies its source. I.e., {\tt db(X,S)} denotes
that {\tt X} is a fact originated from a database {\tt S}. The
composer then has the following form: \vspace{2mm}

 \smallskip
 \noindent
 \hspace*{5mm} {\tt fact(X,S) $\leftarrow$  db(X,S) $\wedge$ $\neg$retract(X) } \\
 \hspace*{5mm} {\tt fact(X,composer) $\leftarrow$  insert(X) } \\
 \hspace*{5mm} {\tt $\leftarrow$  insert(X) $\wedge$ db(X,S) } \\
 \hspace*{5mm} {\tt $\leftarrow$  retract(X) $\wedge$ $\neg$db(X,S) } \vspace{2mm}

Note that the composer considers itself as an extra source that
inserts brand new data facts. Now it is possible, e.g., to trace
information that comes from a specific source, make preferences
among different sources (by specifying appropriate integrity
constraints), and filter data that comes from certain sources.
The last property is demonstrated by the next rule: \vspace{2mm}

\smallskip
\noindent
 \hspace*{5mm} {\tt validFact(X) $\leftarrow$
                    fact(X,S) $\wedge$ trusted\_source(S)} \vspace{2mm}

\smallskip
\noindent
where {\tt trusted\_source} enumerates all reliable
sources of the data. \\

Note that the last example of `source identification' can be
further extended in order to make preferences among different
sources (and not only ignoring some unreliable sources). By
introducing a new predicate, {\tt trust(Source,Amount)}, that
attaches a certain level of reliability to each source, it is
possible, in case of conflicts, to prefer sources with higher
reliability as follows: \vspace{2mm}

\smallskip
\noindent
\hspace*{5mm} {\tt $\leftarrow$
                   fact(X,S) $\wedge$ db(X,S$_{0}$) $\wedge$
                   S$\:\neq\:$S$_{0}$ $\wedge$ more\_trusted(S$_{0}$,S)} \\
\hspace*{5mm} {\tt more\_trusted(S$_{0}$,S) $\leftarrow$
                   trust(S$_{0}$,A$_{0}$) $\wedge$ trust(S,A) $\wedge$
                   A$_{0}\:>\:$A} \vspace{2mm}

This method is particularly useful when the integrity constraint
above acts as a functional dependency on specific facts. The
following example \cite<originally introduced in>{Su94}
demonstrates this.

\begin{example}
{\rm Consider the following simple scenario of `target
recognition', where three sensors of an autonomous vehicle, which
have different degrees of reliability, should identify objects in
the vehicle's neighborhood: \vspace{2mm}

\smallskip
\noindent
\hspace*{5mm} {\tt trust(radar,10)} \\
\hspace*{5mm} {\tt trust(gunchar,8)} \\
\hspace*{5mm} {\tt trust(speedometer,5)} \vspace{2mm} \\
\hspace*{5mm} {\tt db(observe(object1,t72),radar)} \\
\hspace*{5mm} {\tt db(observe(object1,t60),gunchar)} \\
\hspace*{5mm} {\tt db(observe(object1,t80),speedometer)} \vspace{2mm} \\
\hspace*{5mm} {\tt $\leftarrow$
                   fact(observe(O,V$_{1}$),S) $\wedge$
                   db(observe(O,V$_{2}$),S$_{0}$) $\wedge$
                   S$\:\neq\:$S$_{0}$ $\wedge$ more\_trusted(S$_{0}$,S)}
\vspace{1mm}

As the radar has the highest reliability, its observation will be
preserved. The observations of the other sensors will be retracted
from the database.
} \end{example}


% \subsubsection{View Predicates}
% \label{subset:view}
%
% The use of meta-programming is a technique that is easily
% extendable to more complex types of data. Consider an integration
% problem of a set of deductive databases where each database
% contains not only a database instance and a set of integrity
% constraints but also a set ${\cal V}$ of rules defining {\em
% view\/} or {\em intentional\/} predicates, which do not appear in
% the database. The set ${\cal V}$ consists of a set of datalog
% rules with view predicates in the head and view or database
% predicates in the body. View predicates may also occur in the
% integrity constraints. Below is a sketch of how the approach can
% be extended to this more general case. \\
%
% As before, we concentrate on the data integration phase and assume
% that a consistent set of integrity constraints ${\cal IC}$ and a
% set ${\cal V}$ defining the view predicates has been obtained
% from a preliminary phase. To extend our approach, we must extend
% the composer meta-program. The transformation of the integrity
% constraints ${\cal IC}$ is done as before, by substituting ${\tt
% fact}(p)$ for each database or view atom $p$. The composer
% program is more complex. First, three additional meta-predicates
% {\tt base}, {\tt view}, and {\tt clause} are introduced to
% represent the distinction between database and view predicates
% and to represent the rules of ${\cal V}$. For any (database or
% view) predicate $p$, ${\tt base}(p)$ means that $p$ is a database
% predicate and ${\tt view}(p)$ that $p$ is a view predicate. An
% atom ${\tt clause}(H,B)$ is used to represent a rule $H \leftarrow
% B \in {\cal V}$. Second, in the definition of the predicate {\tt
% fact}, distinction is made between database predicates and view
% predicates. For view predicates, the standard vanilla
% meta-program is used to define $fact$. Third, the integrity
% constraints must be modified to guarantee that only database atoms
% can be inserted or retracted, and not view predicate atoms. The
% composer now consist of the following rules and constraints:
% \vspace{2mm}
%
% \smallskip
% \noindent
% \hspace*{5mm} {\tt fact(X) $\leftarrow$ base(X) $\wedge$ db(X) $\wedge$ $\neg$retract(X)} \\
% \hspace*{5mm}  {\tt fact(X) $\leftarrow$ base(X) $\wedge$ insert(X)}  \\
% \hspace*{5mm}  {\tt fact(X) $\leftarrow$ view(X) $\wedge$  clause(X,B) $\wedge$ fact(B) }  \\
% \hspace*{5mm}  {\tt fact(F$\wedge$B) $\leftarrow$ fact(F)  $\wedge$ fact(B)  }  \\
% \hspace*{5mm}  {\tt fact($\neg$F) $\leftarrow$ $\neg$fact(F) }  \\ \\
% \hspace*{5mm}  $\leftarrow$ {\tt insert(X)  $\wedge$ db(X)} \\
% \hspace*{5mm}  $\leftarrow$ {\tt retract(X)  $\wedge$ $\neg$db(X)} \\
% \hspace*{5mm}  $\leftarrow$ {\tt insert(X) $\wedge$ view(X)} \\
% \hspace*{5mm}  $\leftarrow$ {\tt retract(X) $\wedge$ view(X)} \\
%
% As before, database repairs can be obtained by computing abductive
% solutions for the query {\tt true}.


% \subsubsection{Handling Quantitative Information}
%
% Next we consider a potential way of decoding in the integrated
% data some quantitative information, such as certainty factors or
% probabilities. \\
%
% Suppose that {\tt db(X,i)} denotes that fact {\tt X} holds with
% probability {\tt i}. One can define a strategy on how to reason
% with this kind of information, and decode it in the composer. For
% instance, the composer below uses a conservative policy that
% takes for each fact its lowest probability: \vspace{2mm}
%
% \smallskip
% \noindent
%  \hspace*{5mm} {\tt fact(X,i) $\leftarrow$ db(X,\_) $\wedge$
%                               not retract(X) $\wedge$
%                               i = min$\,\{$j | db(X,j)$\}$ } \\
%  \hspace*{5mm} {\tt fact(X,1) $\leftarrow$ insert(X,1) } \\
%  \hspace*{5mm} {\tt $\leftarrow$ insert(X,1) $\wedge$ db(X,\_) } \\
%  \hspace*{5mm} {\tt $\leftarrow$ insert(X,1) $\wedge$ retract(X) } \vspace{2mm}
%
% \smallskip
% For implementing this kind of program the underlying
% system should be able to compute aggregations (possibly together
% with recursion). Adding this capability to our system is one of
% the subjects for a future work.
%


\section{Discussion and an Overview of Related Works}
\label{section:related_works}

The interest in systems for coherent integration of databases has
been continuously growing in the last few years \cite<see,
e.g,>[and many
others]{Ol91,BKM91,BKMS92,Re93,Su94,Br97,GL97,Me97,LM98,LS00,Ul00,GZ00,GGZ01,FPLPS01,Le01,Le02,ABC99,ABC03,BB03,CLR03}.
Already in the early works on this subject it became clear that
the design of systems for data integration is a complex task,
which demands solutions to many questions from different
disciplines, such as belief revision, merging and updating,
reasoning with inconsistent information, constraint enforcement,
query processing and -- of course -- many aspects of knowledge
representation. In this section we shall address some of these issues. \\

One important aspect of data integration systems is how concepts
in the independent (stand-alone) data-sources and those of the
unified database are mapped to each other. A proper specification
of the relations between the source schemas and the schema of the
amalgamated data exempts the potential user from being aware
where and how data is arranged in the sources. One approach for
this mapping, sometimes called {\em global-centric\/} or {\em
global-as-view\/} \cite{Ul00}, requires that the unified schema
should be expressed in terms of the local schemas. In this
approach, every term in the unified schema is associated with a
view (alternatively, a query) over the sources. This approach is
taken by most of the systems for data integration, as well as
ours. The main advantage of this approach is that it induces a
simple query processing strategy that is based on unfolding of
the query, and uses the same terminology as that of the
databases. This indeed is the case in the abductive derivation
process, defined in Section~\ref{abductive_inferences}. The other
approach, sometimes called {\em source-centric\/} or {\em
local-as-view\/} (used, e.g., in \citeR{BCCG02}), considers every
source as a view over the integrated database, and so the meaning
of every source is obtained by concepts of the global database.
In particular, the global schema is independent of the
distributed ones. This implies, in particular, that an addition
of a new source to the system requires only to provide local
definitions and not necessarily involves changes in the global
schema. The main advantage of the latter approach is, therefore,
that it provides a better setting for maintenance. For a detailed
discussion on this topic, see
\shortcite{Ul00,Le01,CCdGL02,vNCDAB04}. More references and a
survey on different approaches to data integration appear in the
papers of \fullciteA{BLN86,RB01}, and \citeA{Le02}. \\

Another major issue that has to be addressed is the ability of
data integration systems to properly cope with dynamically
evolving worlds. In particular, the domain of discourse should not
be fixed in advance, and information may be revised on a regular
basis. The last issue is usually handled by methods of {\em
belief revision\/} \cite{AGM95,GH95} and {\em nonmonotonic
reasoning\/}. In the context of belief revision it is common to
make a distinction between revisions of integrity constraints and
changes in the sets of the data-facts, since the two types of
information have different nature and thus may require different
approaches for handling dynamic changes. When the set of
integrity constraints is given in a clause form, methods of {\em
dynamic logic programing\/} \cite{ALPQ00,APPP02} may be useful
for handling revisions. As noted in \cite{APPP02}, assuming that
each local database is consistent (as in our case), dynamic logic
programing (together with a proper language for implementing it,
like LUPS \cite{APPP02}) provides a way of avoiding contradictory
information, and so this may be viewed as a method of updating a
database by a sequence of integrity constraints that arrive at
different time points. \\

When the types of changes are predictable, or can be characterized
in some sense, temporal integrity constraints (in the context of
{\em temporal databases\/}) can be used in order to specify how
to treat new information. This method is also useful when the
revision criteria are known in advance (e.g., `in case of
collisions, prefer the more recent data', cf. Section
\ref{subset:timestamp_info}). See, e.g., \cite{Sr95,MB99} for a
detailed discussion on temporal integrity constraints and
temporal databases in a logic programming based formalisms. \\

The second type of revisions (i.e., modifications of data-facts)
is obtained here through the (preferred) repairs of the unified
database, which induce corresponding modifications of data-facts.
A repair is usually induced by a method of restoring (or assuring)
consistency of the amalgamated database by a minimal amount of
change. As in our case, the minimization criterion is often
determined by the aspiration to remain `as close as possible' to
the set of the collective information. This is a typical kind of
a {\em repair goal\/}, and the standard ways of formally
expressing it are by enumeration methods, such as the
following\footnote{See also \cite[Section 5]{GL97} for a
discussion on repair strategies.}:
\begin{itemize}
   \item Minimizing the Hamming distance between the (propositional) models
         of the unified database and its repairs \cite{LS00}, or minimizing
         the distance between the corresponding three-valued interpretations
         \cite{dACM02} according to a suitable generalization of Hamming
         distance.
   \item Minimizing the symmetric distance between the sets of consequences
         of the corresponding databases \fullcite{ABC99,ABK00,BCCG02} or,
         equivalently, minimizations in terms of set inclusion \cite{GZ00}.
   \item When the underlying data is prioritized, the corresponding
         quantitative information is also considered in the computations
         of distances \cite<see, for instance, the work of>{LS00}.
\end{itemize}

Various ways of computing (preferred/minimal) repairs are
described in the literature, among which are proof-theoretical
(deductive) methods \cite{BS02,dACM02}, abductive methods
\cite{KM90,IS95,SI99,SI00}, and algorithmic approaches that are
based on computations of maximal consistent subsets
\cite{BKM91,BKMS92}, or use techniques from model-based diagnosis
\cite{GL97}. A common approach is to view a database as a logic
program, and to adopt standard techniques of giving semantics to
logic programs in order to compute database repairs. For
instance, stable-model semantics on disjunctive logic programs is
used for computing repairs in \cite{GZ00,GGZ01,FPLPS01,ABC03},
and resolution-based procedures for integrating several annotated
databases are introduced by \citeA{Su90,Su94}. As it follows from
Section~\ref{section:A_system}, the application introduced here
is also based on an extended resolution strategy, applied on logic
programs that may contain negation-as-failure operators and
abducible predicates. \\

As repairing a database means in particular elimination of
contradictions, reasoning with inconsistent information has been
a major challenge for data integration systems. First, it is
important to note in this respect that not every formalism for
handling inconsistency is acceptable in the context of databases,
even if the underlying criterion for handling inconsistency is
the same as one of the repair goals mentioned above. The following
example demonstrates such a case:

\begin{example}
{\rm \fullcite{ABC99} Consider the following (inconsistent)
database: $\DB = (\{p,\:q\}, \{ \neg(p \wedge q) \})$. In the
approach of \citeA{Li96}, for instance, $p \vee q$ may be inferred
as the repaired database, following a strategy of minimal change.
However, in this approach none of $p$, $q$, and $\neg(p \wedge
q)$ holds in the repaired database. In particular (since in
\cite{Li96} there is no distinction between data-facts and
integrity constraints), the integrity constraint $\{ \neg(p
\wedge q) \}$ itself cannot be inferred, which violates the
intended meaning of an integrity constraint in databases. }
\end{example}

Many techniques for consistency enforcement and repairs of
constraint violations have been suggested, among which are
methods for resolving contradictions by quantitative
considerations, such as `majority vote' \cite{LM98,KPP02} or
qualitative ones (e.g., defining priorities on different sources
of information or preferring certain data over another, as in
\citeR{BCDLP93}, and \citeR{Ar99}). Another common method of
handling inconsistent (and incomplete) information is by turning
to multi-valued semantics. Three-valued formalisms such as the one
considered in Section~\ref{section:model_theoretic_analysis} are
used as a semantical basis of paraconsistent methods to construct
database repairs \fullcite{dACM02} and are useful in general for
pinpointing inconsistencies \cite{Pr91}. Other approaches use
lattice-based semantics to decode within the language itself some
meta-information, such as confidence factors, amount of belief
for or against a specific assertion, etc. These approaches
combine corresponding formalisms of knowledge representation, such
as annotated logic programs \cite{Su90,Su94,ABK00} or
bilattice-based logics \cite{Fi91,AA96,Me97}, together with
non-classical refutation procedures \cite{Fi89,Su90,KL92} that
allow to detect inconsistent parts of a database and maintain
them.


\section{Summary and Future Work}
\label{section:conclusion}

In this paper we have developed a formal declarative foundation
for rendering coherent data, provided by different databases, and
presented an application that implements this approach. Like
similar applications \fullcite<e.g.,>{Su94,BAF98,GZ00,LS00}, our
system mediates among the sources of information and also between
the reasoner and the underlying data. \\

Composition of several data-sources is encoded by meta-theories
in the form of abductive logic programs, and it is possible to
extend these theories by providing meta-information on the
data-facts, such as time-stamps and source identities. Moreover,
since the reasoning process of the system is based on a pure
generalization of classical refutation procedures, no syntactical
embedding of first-order formulae into other languages, nor any
extension of two-valued semantics, is necessary. \\

Due the inherent modularity of the system, each component is
independent and can be modified to meet different needs.
Thus, for instance, the underlying solver may be replaced with
any other solver that is capable of dealing with the meta-theory,
and any improvement of the optimizer will affect the whole system
and its efficiency, regardless the nature of its input. Also, the
way of keeping data coherent is encapsulated in the component
that integrates the data (i.e., the composer). This implies, in
particular, that no input from the reasoner nor any other external
policy for making preferences among conflicting sources is
compulsory in order to resolve contradictions. \\

As we have shown, the operational semantics for inconsistent
databases, induced by the ${\cal A}$\mbox{system}, is strongly
related to (multi-valued) preferential semantics. As preferential
semantics provides the background for many non-monotonic and
paraconsistent formalisms
\cite<e.g.,>{Sh88,Pr89,Pr91,KL92,AA96,Ar99,Ar03}, this implies
that the ${\cal A}$\mbox{system} may be useful for reasoning with
general uncertain theories (not necessarily in the
form of databases). \\

It is important to note that our composing system inherits the
functionality of the underlying solver. The outcome of this is
flexibility, modularity, simple interaction with different sources
of information, and the ability to reason with {\em any\/} set of
first-order formulae of integrity constraints\footnote {Provided,
of-course, that the constraints do not lead to floundering.}. To
the best of our knowledge no other application of data
integration has this ability. \\

There are several directions for further exploration. First, as
we have already noted, two more phases, which have not been
considered here, might be needed for a complete process of data
integration:
\begin{itemize}
   \item [a)] translation of difference concepts to a unified
              ontology, and
   \item [b)] integration of integrity constraints.
\end{itemize}
So far, formalisms for dealing with the first item \cite<e.g.,>
{Le01,Le02,vNCDAB04} mainly focus on the mutual relations between
the global schema and the source (local) schemas, in particular
how concepts of each ontology map to each other. On the other
hand, formalisms for handling the second item concentrate on
nonmonotonic reasoning for dynamically evolving (and mutually
inconsistent) worlds. A synthesis of the main ideas behind these
approaches, and incorporating them in our system, is a major
challenge for future work. \\

Another important issue that deserves attention is the repair of
inconsistency in the context of deductive databases with
integrity constraints and definitions of predicates, often called
{\em view predicates.\/} We refer to \cite{De00} for a sketch on
how this may be done. This kind of data may be further combined
with (possibly inconsistent) temporal information, (partial)
transactions, and (contradictory) update information. \\

Finally, since different databases may have different information
about the same predicates, it is reasonable to use some weakened
version of the closed word assumption as part of the integration
process (for instance, an assumption that something is false
unless it is in the database, or unless some other database has
some information about it).


\section*{Acknowledgements}

We would like to thank the anonymous reviewers for many helpful
comments and suggestions. This research was supported by the
Research Fund K.U.Leuven and by FWO--Vlaanderen.


\vskip 0.2in
\bibliography{arieli04a}
\bibliographystyle{theapa}
\end{document}
