\documentclass[jair,twoside,11pt,theapa]{article} 
\input epsf %% at top of file
 

% Paquetages
\usepackage{jair}
\usepackage{theapa}
\usepackage{graphicx}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{alg}
\usepackage{stmaryrd}
\usepackage{pstricks}
\usepackage{pst-tree}
\usepackage{epsfig}

\usepackage[bottom]{footmisc}
% footnotes to appear on the first page

\jairheading{25}{2006}{269-314}{5/05}{2/06}
\ShortHeadings{Distributed Reasoning in a Peer-to-Peer Setting: Application to the Semantic Web}
                       {Adjiman, Chatalic, Goasdou\'e, Rousset, \&  Simon}
\firstpageno{269}

% R�glages du package alg.
\setlength{\algleftmarginwidth}{0cm}
\setlength{\algrightmarginwidth}{0cm}
\setlength{\alglinenowidth}{0.5cm}
\setlength{\algtabwidth}{0.3cm}

% Environnements
\newtheorem{defi}{Definition} 
\newenvironment{definition}[1]
        {\begin{defi}[#1]}
        {\end{defi}}

\newtheorem{Theorem}{Theorem} 
\newenvironment{theorem}
        {\begin{Theorem}}
        {\end{Theorem}}

\newtheorem{Proposition}{Proposition} 
\newenvironment{proposition}
        {\begin{Proposition}}
        {\end{Proposition}}

\newtheorem{Corollary}{Corollary} 
\newenvironment{corollary}
        {\begin{Corollary}}
        {\end{Corollary}}

\newtheorem{Lemma}{Lemma} 
\newenvironment{lemma}
        {\begin{Lemma}}
        {\end{Lemma}}

\newenvironment{proof}
        {\noindent Proof: }
        {\hfill $\Box$\\}

\newtheorem{exemple}{Example} 
\newenvironment{example}
        {\begin{exemple}\begin{normalfont}}
        {\end{normalfont}\end{exemple}}

% Commandes
% Commentez les deux lignes suivantes pour avoir une version TRAVAIL
        %\newcommand{\noproof}[1]{}
        %\newcommand{\reviewers}[1]{#1}
% Commentez les deux lignes suivantes pour avoir une version ECAI
        \newcommand{\noproof}[1]{#1}
        \newcommand{\reviewers}[1]{}

\newcommand{\eat}[1]{}
\newcommand{\tab}{\hspace*{0.4cm}}
\newcommand{\somewhere}{{\sc Somewhere}}
\newcommand{\deca}{{\sc DeCA}} 
\newcommand{\someone}{{\sc Someone}}
\newcommand{\pdms}[4]{\langle #1,#2,#3,#4\rangle}

\begin{document}
\title{Distributed Reasoning in a Peer-to-Peer Setting: \\
Application to the Semantic Web}

\author{\name Philippe Adjiman  \email adjiman@lri.fr \\
       \name Philippe Chatalic \email chatalic@lri.fr \\
       \name Fran\c{c}ois Goasdou\'e \email fg@lri.fr \\
       \name Marie-Christine Rousset \email mcr@lri.fr \\
       \name Laurent Simon \email simon@lri.fr \\
       \addr LRI-PCRI, B\^atiment 490 \\
        CNRS \& Universit\'e Paris-Sud XI -- INRIA Futurs \\
       91405 Orsay Cedex, France}

\maketitle
\bibliographystyle{theapa}

\begin{abstract}
In a peer-to-peer inference system, each peer can reason locally but can also solicit some of its acquaintances, 
which are peers sharing part of its vocabulary. In this paper, we consider peer-to-peer inference systems 
in which the local theory of each peer is a set of propositional clauses defined upon a local vocabulary. 
An important characteristic of peer-to-peer inference systems is that the global theory 
(the union of all peer theories) is not known (as opposed to partition-based reasoning systems). 
The main contribution of this paper is to provide the first
consequence finding algorithm in a peer-to-peer setting: \deca. It is
anytime and computes consequences gradually from the
solicited peer to peers that are more and more distant. We exhibit a
sufficient condition
on the acquaintance graph of the peer-to-peer inference system for
guaranteeing the completeness of this algorithm.
Another important contribution is to apply this general distributed reasoning setting to the setting 
of the Semantic Web through the \somewhere \ semantic 
peer-to-peer data management system. 
The last contribution of this paper is to provide an experimental analysis of
the scalability of the peer-to-peer infrastructure that we propose, on large 
networks of 1000 peers.
\end{abstract}

%Introduction
\section{Introduction}
Recently peer-to-peer systems have received considerable attention because their underlying
infrastructure is appropriate to scalable and flexible distributed applications over Internet.
In a peer-to-peer system, there is no centralized control or hierarchical organization: each peer
is equivalent in functionality and cooperates with other peers in order to solve a collective task.
Peer-to-peer systems have evolved from simple keyword-based peer-to-peer file sharing systems like 
\textsc{Napster} (http://www.napster.com) and \textsc{Gnutella} (http://gnutella.wego.com)
 to semantic peer-to-peer data management systems
like \linebreak \textsc{Edutella} \cite{edutella} or \textsc{Piazza}~\cite{piazza}, which handle semantic data description and
support complex queries for data retrieval. In those systems, the complexity of answering 
queries is directly related to the expressivity of the formalism used to state
the semantic mappings between peers schemas ~\cite{halevy-pdms}. 

In this paper, we are interested in peer-to-peer inference systems in which each peer can answer queries
by reasoning from its local (propositional) theory but can also ask queries to some other peers with 
which it is semantically related by sharing part of its vocabulary. This framework encompasses several 
applications like peer-to-peer information integration systems or intelligent agents,
in which each peer has its own knowledge (about its data or its expertise domain) and some partial 
knowledge about some other peers. In this setting, when solicited to perform a reasoning task, a peer, 
if it cannot solve completely that task locally, must be able to distribute appropriate reasoning 
subtasks among its acquainted peers. This leads to a step by step splitting of the initial task 
among the peers that are relevant to solve parts of it. The outputs of the different splitted tasks must 
then be recomposed to construct the outputs of the initial task.

We consider peer-to-peer inference systems in which the local theory of each peer is composed of a set of 
propositional clauses defined upon a set of propositional variables (called its local vocabulary). Each peer may share part of its vocabulary with some other peers. 
We investigate the reasoning task of finding consequences of a certain form (e.g., clauses involving only certain 
variables) for a given input formula 
expressed using the local vocabulary of a peer.
Note that other reasoning tasks like finding implicants of a certain form for a given input formula can be 
equivalently reduced to the consequence finding task.




It is important to emphasize that the problem of distributed reasoning that we consider in this paper is 
quite different from the problem of reasoning over partitions obtained by decomposition of a 
theory \cite{Dechter94,Amir2000}. In that problem, a centralized large theory is given and its 
structure is exploited to compute its best partitioning in order to optimize the use of a partition-based reasoning
algorithm. In our problem, the whole theory (i.e., the union of all the local theories) is not known and 
the partition is imposed by the peer-to-peer architecture. 
As we will illustrate it on an example (Section \ref{prel}), the algorithms based on transmitting
clauses between partitions  in the spirit of the work of \citeA{Amir2000,Dechter94} or \citeA{delVal1999a} 
are not appropriate for our consequence finding problem. Our algorithm splits clauses if they share variables of several
peers. Each piece of a splitted clause is then transmitted to the corresponding theory to find its consequences.
The consequences that are found for each piece of splitted clause must then be recomposed to get the consequences
of the clause that had been splitted.

The main contribution of this paper is to provide the first
consequence finding algorithm in a peer-to-peer setting:  \deca. It is
 anytime and computes consequences gradually from the
solicited peer to peers that are more and more distant. We exhibit a
sufficient condition
on the acquaintance graph of the peer-to-peer inference system for
guaranteeing the completeness of this algorithm.

Another important contribution is to apply this general distributed reasoning setting to the setting of the Semantic Web through the \somewhere \ semantic 
peer-to-peer data management system. \somewhere \ is based on a simple 
data model
made of taxonomies of atomic classes and mappings between classes of 
different taxonomies, 
which we think are the appropriate common semantic support needed 
for most of the future semantic web applications. The \somewhere \ data model
can be encoded into propositional logic so that query answering in \somewhere \
can be equivalently reduced to distributed reasoning over logical 
propositional theories.

The last contribution of this paper is to provide an experimental analysis of
the scalability of our approach, when deployed on large networks.
So far, the scalability of a system like \textsc{Piazza} goes up  to about 80 peers.
\textsc{Piazza} uses a more expressive language than the one used in our approach,
but its results rely on a wide range of optimizations (mappings composition, 
paths pruning \citeR{halevy-sigmod04}) made possible by the centralized 
storage of all the schemas and mappings in a global server. In contrast, we 
have stuck to a fully decentralized approach and performed our experiments 
on networks of 1000 peers. 

An important point characterizing peer-to-peer systems is their dynamicity: 
peers can join or leave the system at any moment. Therefore, it is not 
feasible to bring all the information to a single server in order to reason
with it locally using standard reasoning algorithms. 
Not only would it be costly to gather the data available through the system 
but it would be a useless task because of the changing peers 
connected to the network. The dynamicity of peer-to-peer inference systems
imposes to revisit any reasoning problem in order to address it in a completely
decentralized manner. 

The paper is organized as follows. Section~\ref{prel} defines formally the 
peer-to-peer inference problem that we address in this paper. In Section~\ref{algo}, 
we describe our distributed consequence finding algorithm and we state its properties. 
We describe \somewhere \ in Section~\ref{somewhere}. 
Section~\ref{exp} reports the experimental study of the scalability of our peer-to-peer 
infrastructure. Related work is summarized in Section~\ref{related}. 
We conclude with a short discussion in Section~\ref{conclusion}.

%Peer-to-peer inference: problem definition
\section{Consequence Finding in Peer-to-peer Inference Systems}
\label{prel}

A peer-to-peer inference system (P2PIS) is a network of peer theories.
Each peer $P$ is a finite set of propositional formulas of a language  $\mathcal{L}_P$.
We consider the case where $\mathcal{L}_P$ is
the language of clauses without duplicated literals that can be built from a finite set
of propositional variables $\mathcal{V}_P$, called the \emph{vocabulary} of 
$P$.
%
Peers can be semantically related by sharing  variables with other peers. 
A {\em shared variable} between two peers is in the intersection 
of the vocabularies of the two peers. We do not impose however that 
all the variables in common in the vocabularies of two peers are shared 
by the two peers: two peers may not be aware of all the variables that they 
have in common but only of some of them.

In a P2PIS, no peer has the knowledge of the global P2PIS theory. 
Each peer only 
knows its own local theory and the variables that it shares with some other 
peers 
of the P2PIS (its \emph{acquaintances}).  It does not necessarily knows
{\em all} the variables that it has in common with other peers (including with 
its acquaintances).
When a new peer joins a P2PIS it simply 
declares its acquaintances in the P2PIS, i.e., 
the peers it knows to be sharing 
variables with, and it declares the corresponding shared variables.  

\subsection{Syntax and Semantics}

A P2PIS can be formalized using the notion of {\em acquaintance graph} and
in the following we consider P2PIS and acquaintance graphs as equivalent. 
\pagebreak
\begin{definition}{Acquaintance graph}
Let $\mathcal{P}=\{P_i\}_{i=1..n}$ be a collection of clausal theories on their
respective vocabularies  $\mathcal{V}_{P_i}$, let $\mathcal{V} = \cup_{i=1..n} \mathcal{V}_{P_i}$.
An acquaintance graph  over $\mathcal{V}$ is a graph $\Gamma = (\mathcal{P},\mbox{\sc acq})$
where $\mathcal{P}$ is the set of vertices and $\mbox{\sc acq} \subseteq \mathcal{V} \times \mathcal{P} \times \mathcal{P}$ is a set of labelled edges
such that for every 
$(v,P_i,P_j)\in \mbox{\sc acq}$, $i \neq j$ and $v \in \mathcal{V}_{P_i}\cap \mathcal{V}_{P_j}$.
\end{definition}

A labelled edge $(v,P_i,P_j)$ expresses that peers $P_i$ and $P_j$ 
know each other to be sharing the variable $v$.
For a peer $P$ and a literal $l$,  $\mbox{\sc acq}(l,P)$ denotes the set of peers
sharing  with $P$ the variable of $l$. 



In contrast with other approaches \cite{ghidini-serafini,calvanese-et-al-2004}, 
we do not adopt an epistemic or  modal semantics for interpreting a P2PIS 
but we interpret it with the standard semantics of propositional logic.

\begin{definition}{Semantics of a P2PIS}
Let  $\Gamma = (\mathcal{P},\mbox{\sc acq})$ be a P2PIS 
with $\mathcal{P}=\{P_i\}_{i=1..n}$,
\begin{itemize}
\item  An \emph{interpretation} $I$ of $\mathcal{P}$ is an assignement of 
         the variables in $\bigcup_{i=1..n}P_i$ to $true$ or $false$. 
        In particular, a variable which is common to two theories $P_i$ and 
        $P_j$ of a given P2PIS is interpreted by the same value in the two theories.

\item  $I$ is a \emph{model of a clause} $c$ iff one of the literals of $c$ is evaluated 
           to $true$ in $I$.

\item $I$ is a \emph{model of a set of clauses} (i.e., a local theory, a union of a 
          local theories, or a whole P2PIS) iff it is a model of all the clauses 
         of the set.

\item A P2PIS is \emph{satisfiable} iff it has a model.

\item The \emph{consequence relation} for a P2PIS is the standard consequence relation
         $\models$: given a P2PIS $\mathcal{P}$, and a clause $c$, 
          $\mathcal{P}$ $\models$ $c$ iff every model of $\mathcal{P}$ is a model of $c$.
\end{itemize}
\end{definition}

\subsection{The Consequence Finding Problem}

For each theory $P$, we consider a subset  of \emph{target variables}
$\mathcal{TV}_P \subseteq \mathcal{V}_P$, supposed to represent
the variables of interest for the application, (e.g.,
observable facts in a model-based diagnosis
application, or classes storing data in an information integration 
application).
The goal is, given a  clause provided as an input to a given peer,
to find all the possible consequences belonging to some \emph{target language}
of the input clause and the union of the peer theories.

The point is that the input clause only uses the vocabulary of the queried 
peer, but that its expected consequences may involve target variables of different peers.
The target languages handled by our algorithm are defined in terms of target variables 
and require that a shared variable has the same target status in all the peers sharing it. It is worth noting that this requirement is a local property: 
the peers sharing variables with a given peer are its acquaintances and, 
by definition, they are its direct neighbours in the acquaintance graph.

\begin{definition}{Target Language}
Let $\Gamma = (\mathcal{P},\mbox{\sc acq})$ be a P2PIS, and for every peer $P$,
let $\mathcal{TV}_{P}$ be the set of its target variables such that 
if $(v, P_i,P_j)\in\mbox{\sc acq}$ then $v \in \mathcal{TV}_{P_i} $ 
iff  $v \in \mathcal{TV}_{P_j}$.
For a set $SP$ of peers of  $\mathcal{P}$, we define its 
\emph{target language} $\mathcal{T}arget(SP)$ as the language of clauses 
(including the empty clause) involving only variables of 
$\bigcup_{P\in SP} \mathcal{TV}_P$.
\end{definition}

The reasoning problem that we are interested in is to compute logical 
consequences of an input clause given a P2PIS. 
It corresponds to the notion
of proper prime implicates of a clause w.r.t. a clausal (distributed) theory, 
which if
formally defined in Definition~\ref{implicate}.



\begin{definition}{Proper prime implicate of a clause w.r.t. a clausal theory}
\label{implicate}
Let $P$ be a clausal theory and $q$ be a clause. A clause $m$ is said to be:
\begin{itemize}
\item  an {\em implicate} of $q$ w.r.t. $P$ iff $P \cup \{q\} \models m$.

\item  a {\em prime implicate} of $q$ w.r.t. $P$ iff $m$ is an implicate
           of $q$ w.r.t. $P$, and for any other clause $m'$ implicate of $q$ 
          w.r.t. $P$, if $m' \models m$ then $m' \equiv m$.

\item   a {\em proper prime implicate} of $q$ w.r.t. $P$ iff  it is a prime implicate of $q$ w.r.t. $P$
             but  $P \not \models m$.
\end{itemize}
\end{definition}

The problem of finding prime implicates from a new clause and a theory, 
a.k.a. $\Phi$-prime implicates, corresponds exactly to the problem of computing 
proper prime implicates of a clause w.r.t. a clausal theory. It has been extensively 
studied in the centralized case (see the work of \citeR{Marquis2000}, for a survey). 
Note that deciding whether a clause is a $\Phi$-prime implicate of a clausal 
theory is $BH_2$-complete \cite{Marquis2000}, i.e., both in $NP$ and $coNP$.
The problem we address may be viewed as a further refinement, restricting
to the computation of proper prime implicates of a given target language. It 
corresponds to $\langle L,\Phi \rangle$-prime implicates in the work of \citeA{Marquis2000}
and has the same complexity.

\begin{definition}{The consequence finding problem in a P2PIS}
\label{conseq-finding-pb}
Let $\Gamma = (\mathcal{P},\mbox{\sc acq})$ be a $P2PIS$,  
where $\mathcal{P}=\{P_i\}_{i=1..n}$ is a collection of clausal theories with
respective target variables.
The \emph{consequence finding problem} in $\Gamma$ is, given a peer $P$, 
its acquaintances in $\Gamma$, and a clause $q \in \mathcal{L}_P$, 
to find the set of proper prime implicates of $q$ w.r.t. $\bigcup_{i=1..n}P_i$ 
which belong to $\mathcal{T}arget(\mathcal{P})$.
\end{definition}



From an algorithmic point of view, the
consequence finding problem in a P2PIS is new and significantly different from
the consequence finding problem in a single global theory. 
According to the semantics, in order to be complete, a peer-to-peer
consequence finding
algorithm must obtain 
the same results as any standard consequence finding algorithm applied
to the union of the local 
theories, but without having it as a global input: it just has a partial and
local input made of the theory of a single peer and of its acquaintances.
The reasoning must be  distributed appropriately among
the different theories without a global view of the whole P2PIS. In a full 
peer-to-peer setting, such a consequence finding algorithm cannot be centralized
(because it would mean that there is a super-peer controlling the reasoning).
Therefore, we must design an algorithm running independently on each
peer and possibly distributing part of reasoning that it controls to acquainted
peers: no peer has control on the whole reasoning.

Among the possible consequences we distinguish {\em local consequences}, 
involving only target variables of the solicited peer, 
{\em remote consequences}, which involve target variables of
a single peer distant from the solicited peer,  and 
{\em combined consequences} 
which involve target variables of several peers.

\subsection{Example}
The following example illustrates the main characteristics of our
message-based distributed algorithm running on each peer, which will be 
presented in detail in Section \ref{algo}.

Let us consider 4 interacting peers. $P_1$ describes a tour operator.
Its theory expresses that its current $Far$ destinations
are either $Chile$ or $Kenya$.
These far destinations are international destinations ($Int$) and expensive ($Exp$).
%
The peer $P_2$   is only concerned with police regulations and expresses
that a passport is required ($Pass$) for international destinations.
%
 $P_3$ focuses on sanitary conditions for travelers.
 It expresses that,  in Kenya,  yellow fever vaccination ($YellowFev$) is strongly recommended
 and that a strong protection against paludism should be taken ($Palu$) when accomodation
 occurs in $Lodges$.
 %
 $P_4$ describes travel accommodation conditions : Lodge for Kenya
 and $Hotel$ for Chile. It also expresses that when  anti-paludism
 protection is required,  accommodations are equipped with appropriate anti-mosquito protections ($AntiM$).
 %
The respective theories of each peer are described on Figure \ref{fig:exemple} as the nodes of
the acquaintance graph. Shared variables are mentioned as edge labels. 
Target variables are defined by :
 %
 $\mathcal{TV}_{P_1} = \{Exp\}$,
 %
 $\mathcal{TV}_{P_2} = \{Pass\}$,
   %
 $\mathcal{TV}_{P_3} = \{Lodge, YellowFev, Palu\}$ and
 %
  $\mathcal{TV}_{P_4} = \{Lodge, Hotel, Palu, AntiM\}$.

\begin{figure}[H]
\begin{center}
{\scriptsize
\pstree[thislevelsep=2.5cm,treesep=1cm]
     {% Root  Node
     \Tr[vref=0]{\psframebox{
$
\begin{array}{l l}
  P_1:~\\
  \neg \textsf{Far} \vee  \textsf{Exp}         & \neg \textsf{Far} \vee  \textsf{Int}\\
  \neg \textsf{Far}  \vee  \textsf{Chile}  \vee  \textsf{Kenya}
\end{array}
$
     }
     }
     }     % Root  Node
     {% Leaf Nodes
     % First Node
     \Tr{\psframebox{
$ 
\begin{array}{l}
    P_2: \\
   \neg \textsf{Int} \vee \textsf{Pass}\\
\end{array}
$
     }}% First Node
     \tlput{ \textsf{Int}}
     % Second Node

      \Tr[name=P3]{\psframebox{
$
\begin{array}{l}
 P_3:\\
 \neg \textsf{Kenya} \vee \textsf{YellowFev}\\
\neg \textsf{Lodge} \vee \neg \textsf{Kenya} \vee \textsf{Palu}\\
\end{array}
  $ 
      }}% Second Node
    \tlput{\textsf{Kenya}}
     % Third Node
     \Tr[name=P4]{\psframebox{
$ 
\begin{array}{l}
   P_4:~\\
  \neg \textsf{Kenya} \vee \textsf{Lodge}\\
  \neg \textsf{Chile } \vee \textsf{Hotel}\\
  \neg \textsf{Palu} \vee \textsf{AntiM}
\end{array}
$
         }}% Third Node
      \trput{\textsf{Kenya,Chile}}
     % Additional arcs between nodes
     \ncdiag[angleA=-90,angleB=-90,armA=0.4cm,armB=0.3cm]{P3}{P4}
     \ncput*{\textsf{Lodge,Palu}}
  }% Leaf Nodes
}%scriptsize
\end{center}
\caption{Acquaintance graph for the tour operator example }
\label{fig:exemple}
\end{figure}
We now illustrate the behavior of the algorithm when the input clause 
$\textsf{Far}$ is provided to peer $P_1$ by the user. 
Describing precisely the behavior of
a distributed algorithm on a network of peers is not easy. 
In the following we present the propagation of the reasoning 
as a tree structure, the nodes of which correspond to peers and the branches of which
materialize the different reasoning paths induced by the initial input clause. 
Edges are labelled on the left side by literals which are propagated along paths  and/or 
on the right side by consequences that are transmitted back. A downward arrow on an edge
indicates the step during which a literal is propagated from one peer to
its neighbor. For instance, the initial step can be represented here by the following tree : 

\begin{center} 
{\scriptsize
  \pstree[thislevelsep=1.3cm,arrows=->]
     {% Root  Node
        \TC*[radius=2pt]
     } % Root  Node
     { 
        \Tr[name=P1]{
                \psframebox{
                      $
                      \begin{array}{l l l}
                        P_1:~\\
                       \end{array}
                      $
                }  %psframebox
        } %Tr
        \tlput{\begin{tabular}{r}
                      $Far$ \\
                      ~
                      \end{tabular}
       }
   } % pstree
} % scriptsize      
\end {center} 


%%%%%%%%%%%%%%%%%%%%%%%%
Local consequences of a literal propagated on a peer are then explicited within
the peer node. Target literals are outlined using a grey background,  as well as transmitted back
consequences. Vertical arrows preceding consequences 
distinguish the last returned consequences from earlier ones.
Although the successive trees presented here have increasing depth, as if all reasoning paths were explored 
synchronously and in parallel, the reader should keep in mind that 
all messages are exchanged in an asynchronous way and that the order in which consequents
are produced cannot be predicted.

In our example, consequences of \textsf{Far} derived by local reasoning 
on  $P_1$ are \textsf{Exp}, \textsf{Int} and $\textsf{Chile} \vee \textsf{Kenya}$.
Since \textsf{Exp} is in $\mathcal{T}arget(P_1)$ it is a local  consequence of \textsf{Far}.
%
\textsf{Int} is not a target literal but is shared with $P_2$, it is therefore transmitted to $P_2$. 
%
The clause $\textsf{Chile} \vee \textsf{Kenya}$ is also made of shared variables.
Such clauses are processed by our algorithm using a split/recombination approach. Each 
shared literal is processed
independently, and transmitted to its appropriate neighbors.
Each literal  is associated with some queue data structure, where transmitted back  consequences
are stored. 
As soon as at least one consequent has been obtained for each literal,   
the respective queued consequents of each literal   are recombined,  to produce consequences
of the initial clause. This recombination process continues, as new consequences
for a literal are produced.  Note that since each literal is processed asynchronously, 
the order in which the recombined consequences  are produced is unpredictable.
Here, the component \textsf{Chile} is transmitted to $P_4$ and \textsf{Kenya}
is transmitted to $P_3$ and $P_4$. Let us note that the peer $P_4$ appears two times 
in the tree, because two different literals are propagated on this peer, which induces two different 
reasoning paths. 

\vspace{-0.5cm}
\begin{center} 
{\scriptsize
  \pstree[thislevelsep=1.5cm]
     {% Root  Node
        \TC*[radius=2pt]
     } % Root  Node
     { 
      \pstree[thislevelsep=2cm,treesep=1.2cm ]
       {% Root  Node2
         \Tr[name=P1]{
          \psframebox{
           $
            \begin{array}{l l l }
              P_1:~\\
              \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Exp}}  & 
                          \rnode{P1Int}{\textsf{Int}} &
                           \rnode{P1Chile}{\textsf{Chile}} \vee \rnode{P1Kenya}{\textsf{Kenya}}
             \end{array}
           $
          }%psframebox
        }%Tr
              \tlput{\begin{tabular}{r}
                      $Far$ \\
                       ~
                      \end{tabular}
                  }

      }% Root  Node2
      {% Leaf Nodes 2
        % First Node
          \Tr[name=P2,edge=none]{\psframebox{
           $ 
             \begin{array}{l}
             P_2:
            \end{array}
           $
           }}% First Node
          %\tlput{ \textsf{Int}}

      % Second  Node
          \Tr[name=P41,edge=none]{\psframebox{
              $ 
              \begin{array}{l}
                P_4:~\\
             \end{array}
              $
          }} % Second Node

        %\tlput{\textsf{Chile}}


        % Third  Node
           \Tr[name=P3,edge=none]{\psframebox{
              $
               \begin{array}{l}
               P_3:\\
               \end{array}
             $ 
           }} % Third Node
          %\tlput{\textsf{Kenya}}

       % Fourth Node
          \Tr[name=P42,edge=none]{\psframebox{
              $ 
              \begin{array}{l}
                P_4:~\\
             \end{array}
              $
          }} % Fourth Node
        %\tlput{\textsf{Kenya}}

     }  % Leaf Nodes 
    } %pstree  
    \ncline[nodesepA=2pt]{->}{P1Int}{P2}\tlput{$Int$}
    \ncline[nodesepA=2pt]{->}{P1Chile}{P41}\tlput{$Chile$}
    \ncline[nodesepA=2pt]{->}{P1Kenya}{P3}\tlput{$Kenya$}
    \ncline[nodesepA=2pt]{->}{P1Kenya}{P42}\tlput{$Kenya$}
} % scriptsize      
\end {center} 
% \vspace{0.5cm}
%%%%%%%%%%%%%%%%%%%%%%%%
\vspace{0.1cm}
While \textsf{Exp} is transmitted back to the user as a first (\textit{local}) consequence
of \textsf{Far}.
\begin{itemize}
 \item The propagation of \textsf{Int} on $P_2$  produces the clause \textsf{Pass},
          which is in $\mathcal{T}arget(P_2)$ but is not shared and therefore, 
          cannot be further propagated.
          
\item The clause \textsf{Chile}, when transmitted to $P_4$, produces \textsf{Hotel} which 
          is in $\mathcal{T}arget(P_4)$ but is not shared and cannot be further propagated.
          
\item When transmitted to $P_3$, the clause \textsf{Kenya} produces  \textsf{YellowFev} as
          well as the clause $\neg \textsf{Lodge} \vee \textsf{Palu}$. The three variables are 
          in  $\mathcal{T}arget(P_3)$.  \textsf{Lodge} and \textsf{Palu} are also shared 
          variables and therefore, after splitting of the second clause,  their corresponding literals
          are transmitted (independently) to  $P_4$.
          
\item  When transmitted to $P_4$, $\textsf{Kenya}$ produces  $\textsf{Lodge}$,
          which is in  $\mathcal{T}arget(P_4)$ and is also shared and therefore further 
          transmitted to  $P_3$.
\end{itemize}

\vspace{-0.1cm}
\begin{center} 
{\scriptsize
  \pstree[thislevelsep=1.5cm] %
     {% Root  Node
        \TC*[radius=2pt]
     } % Root  Node
     { % Branches
      \pstree[thislevelsep=2.3cm,treesep=1.2cm]
       {% Root  Node2
         \Tr[name=P1]{
          \psframebox{
           $
            \begin{array}{l l l}
                P_1:~\\
              \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Exp}}  & 
                          \rnode{P1Int}{\textsf{Int}} &
                           \rnode{P1Chile}{\textsf{Chile}} \vee \rnode{P1Kenya}{\textsf{Kenya}}
             \end{array}
           $
          }%psframebox
        }%Tr
       \tlput{\begin{tabular}{r}
                      $Far$ \\
                       ~
                      \end{tabular}
                  }
       \trput{\begin{tabular}{l}
                       $\uparrow$ \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Exp}} \\
                      ~
                      \end{tabular}
                  }
       }% Root  Node2
      {   % Branches 2
        % First Node      
          \Tr[name=P2,edge=none]{\psframebox{
           $ 
             \begin{array}{l}
             P_2:\\
              \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Pass}}
            \end{array}
           $
           }}% First Son

        % Second Node      
          \Tr[name=P41,edge=none]{\psframebox{
           $ 
             \begin{array}{l}
             P_4:\\
              \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Hotel}}
            \end{array}
           $
           }}% Second Son

        % Third Son
          \pstree[thislevelsep=2cm,treesep=1cm,arrows=->]
            {% Root of the third Son
              \Tr[name=P3,edge=none]{\psframebox{
                    $
                    \begin{array}{l l}
                           P_3:\\
                           \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{
                               \textsf{YellowFev}
                           }
                           \  
                           \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{
                                \rnode{P3Lodge}{\neg\textsf{Lodge}}
                            }
                               \vee
                          \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{
                               \rnode{P3Palu}{\textsf{Palu}}
                           }\\
                  \end{array}
                  $ 
                 }} % Root of the second Son of the third one
               }
               {
                      \Tr[name=P45,edge=none]{\psframebox{
                           $ 
                             \begin{array}{l}
                                P_4:~\\
                             \end{array}
                            $
                        }} % 
                       \Tr[name=P46,edge=none]{\psframebox{
                           $ 
                             \begin{array}{l}
                                P_4:~\\
                             \end{array}
                            $
                        }} % 
              }

          % Fourth Son
          \pstree[thislevelsep=2cm,treesep=0.6cm,arrows=->]
            {\Tr[name=P42,edge=none]{\psframebox{
              $
               \begin{array}{l}
               P_4:\\
                   \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{
                       \rnode{P42Lodge}{\textsf{Lodge}}
                    }             
               \end{array}
             $ 
               }} % Fourth Node root          
               } 
              {
                   \Tr[name=P31]{\psframebox{
                           $ 
                             \begin{array}{l}
                                P_3:~\\
                             \end{array}
                            $
                        }} % 
              }

        }% Branches  2     
    } % Branches  
    \ncline[nodesepA=2pt]{-}{P1Int}{P2}\tlput{$Int$}
    \ncline[nodesepA=2pt]{-}{P1Chile}{P41}\tlput{$Chile$}
    \ncline[nodesepA=2pt]{-}{P1Kenya}{P3}\tlput{$Kenya$}
    \ncline[nodesepA=2pt]{-}{P1Kenya}{P42}\tlput{$Kenya$}
   \ncline[nodesepA=2pt]{->}{P3Lodge}{P45}\tlput{$\neg Lodge$}
   \ncline[nodesepA=2pt]{->}{P3Palu}{P46}\tlput{$Palu$}
   \ncline[nodesepA=2pt]{->}{P42Lodge}{P31}\tlput{$Lodge$}
 } % scriptsize
\end {center} 

%%%%%%%%%%%%
\begin{itemize}
          \addtolength{\itemsep}{-1.0\baselineskip}

\item The clause \textsf{Pass}, produced on $P_2$, is transmitted 
           back to $P_{1}$ as a consequence
          of \textsf{Int} and then to the user as a \textit{remote consequence} 
          of \textsf{Far}.

\item The clause \textsf{Hotel}, produced on $P_4$, is transmitted 
          back to  $P_{1}$ where it is queued as a consequent of \textsf{Chile}, 
          since it has to be combined with consequences of $\textsf{Kenya}$.
                   
\item The two local consequences of \textsf{Kenya} obtained on $P_3$ contain only 
          target variables.  They are transmitted back to  $P_{1}$ and queued there. 
          They may now be combined with  \textsf{Hotel} to produce two new 
          \textit{combined  consequences} of \textsf{Far} :
          $\textsf{Hotel} \vee  \textsf{YellowFev}$ and 
          $\textsf{Hotel} \vee  \neg \textsf{Lodge} \vee \textsf{Palu}$, which are transmitted back to the user.

\item Similarly on $P_{4}$,  \textsf{Lodge} is a local target consequent of \textsf{Kenya}, that is 
transmitted back to $P_{1}$ as a consequent of \textsf{Kenya}, where it is combined with \textsf{Hotel}
to produce a new consequence of \textsf{Far} that, in turn, is transmitted back to the user.

\end{itemize}

Simultaneously, the reasoning further propagates in the network of peers. The propagation of $\neg \textsf{Lodge}$ 
and $\textsf{Palu}$ on $P_{4}$ respectively produces  $\neg \textsf{Kenya}$, which is not a target literal but 
is shared and thus further propagated on $P_{1}$, as well as  $\textsf{AntiM}$, which is a target literal, but not
shared. We do not detail here the propagation of \textsf{Lodge} in the right most branch of the reasoning tree.

\begin{center} 
\scalebox{0.9}{
{\scriptsize
  \pstree[thislevelsep=3.2cm] %
     {% Root  Node
        \TC*[radius=2pt]
     } % Root  Node
     { % Branches
      \pstree[thislevelsep=2.3cm,treesep=1.5cm]
       {% Root  Node2
         \Tr[name=P1]{
          \psframebox{
           $
            \begin{array}{l l l}
                P_1:~\\
              \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Exp}}  & 
                          ~~~~~~\rnode{P1Int}{\textsf{Int}} &
                          ~~~~~~ \rnode{P1Chile}{\textsf{Chile}} \vee \rnode{P1Kenya}{\textsf{Kenya}}
             \end{array}
           $
          }%psframebox
        }%Tr
          \tlput{\begin{tabular}{r}
                      $Far$ \\
                      ~
                      \end{tabular}
          }
         \trput[labelsep=1pt]{\rput(1.7,0.2){
                  $
                  \begin{array}{l}
                        \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Exp}} \\
                        \uparrow \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Pass}} \\
                        \uparrow \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Hotel} \vee \textsf{YellowFev}} \\
                        \uparrow \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Hotel} \vee \neg \textsf{Lodge} \vee \textsf{Palu}}\\
                       \uparrow \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Hotel} \vee\textsf{Lodge}}\\
                        ~
                   \end{array}
                  $
                 } }
      }% Root  Node2
      {   % Branches 2
        % First Node      
          \Tr[name=P2,edge=none]{\psframebox{
           $ 
             \begin{array}{l}
             P_2:\\
              \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Pass}}
            \end{array}
           $
           }}% First Son

        % Second Node      
          \Tr[name=P41,edge=none]{\psframebox{
           $ 
             \begin{array}{l}
             P_4:\\
              \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Hotel}}~~~
            \end{array}
           $
           }}% Second Son

        % Third Son
          \pstree[thislevelsep=1.8cm,treesep=1cm]
            {% Root of the third Son
              \Tr[name=P3,edge=none]{\psframebox{
                    $
                    \begin{array}{l l}
                           P_3:\\
                           \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{
                               \textsf{YellowFev}
                           }
                           &  
                           \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{
                                \rnode{P3Lodge}{\neg\textsf{Lodge}}
                            }
                               \vee
                          \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{
                               \rnode{P3Palu}{\textsf{Palu}}
                           }\\
                  \end{array}
                  $ 
                 }} 
               }% Root of the second Son of the third one
               {
                   \pstree[thislevelsep=1.6cm]
                    {
                       \Tr[name=P45,edge=none]{
                           \psframebox{
                                $ 
                                \begin{array}{l}
                                    P_4:~ \\
                                   \neg \rnode{P45Kenya}{\textsf{Kenya}}
                                \end{array}
                                $
                            }%psframebox
                        } % Tr
                     } 
                     {
                         \Tr[name=P11,edge=none]{
                               \psframebox{
                                      $
                                       \begin{array}{l}
                                           P_1: ~\\
                                       \end{array}
                                      $
                              }
                           }
                       }                         

                       \Tr[edge=none,name=P46]{
                          \psframebox{
                           $ 
                             \begin{array}{l}
                                P_4:~\\
                                     \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{AntiM}}
                             \end{array}
                            $
                        }} % 
              }

          % Fourth Son
          \pstree[thislevelsep=1.8cm,arrows=-]
              {\Tr[name=P42,edge=none]{
                     \psframebox{
                            $
                               \begin{array}{l}
                                     P_4:\\
                                    \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{
                                           \rnode{P42Lodge}{\textsf{Lodge}}
                                      }             
                               \end{array}
                             $ 
                }} % Fourth Node root          
               } 
              {
                   \Tr[edge=none,name=P31]{
                       \psframebox{
                           $ 
                             \begin{array}{l}
                                P_3:~\\
                                ...
                             \end{array}
                            $
                        }
                   } % Tr
              }
        }% Branches  2     
    } % Branches  
    \ncline[nodesepB=2pt]{-}{P2}{P1Int}
    \nbput{\rput(0.2,-0.1){
                      $\uparrow$ \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Pass}}
                 }}

    \ncline[nodesepB=2pt]{-}{P41}{P1Chile}
    \nbput{\rput(0.2,-0.1){
                   $\uparrow$ \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Hotel}}
               }}

    \ncline[nodesepB=2pt]{-}{P3}{P1Kenya}
    \nbput{\rput(1,-0.1){
                                $
                                 \begin{array}{l}
                                     \uparrow \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\mathsf{YellowFev}} \\
                                     \uparrow \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\mathsf{\neg Lodge} \vee \mathsf{Palu}} \\
                                  \end{array}
                                $
              }}
      \ncline[nodesepB=2pt]{-}{P42}{P1Kenya}
    \nbput{\rput(1.2,-0.2){
                  $\uparrow$ \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Lodge}}
               }}

    \ncline[nodesepB=2pt]{-}{P45}{P3Lodge}
    \naput{\rput(-0.5,-0.2){
                   $\neg Lodge$
               }
     }

   \ncline[nodesepB=2pt]{-}{P46}{P3Palu}
    \naput{\rput(-0.2,-0.1){
                   $Palu$
               }
    }

   \ncline[nodesepB=2pt]{-}{P31}{P42Lodge}
   \naput{$Lodge$}

   \ncline[nodesepB=2pt]{<-}{P11}{P45Kenya}
   \naput{$\neg Kenya$}



 } % scriptsize
 }
\end {center} 
%%%%%%%%%%%%
Note on the deepest node that $P_1$ is here asked to produce the implicates
of $\neg \textsf{Kenya}$, while  the complementary
literal $\textsf{Kenya}$ is still under process. 
We will see in Section \ref{algo} that
such situations are handled in our algorithm by mean of histories keeping  track of the 
reasoning branches ending up to each transmitted literal.  
When a same history contains two complementary 
literals, the corresponding reasoning branch is closed and the empty 
clause $\Box$ is returned as a consequence of the literals in the history. 

In our example, the consequence produced by $P_1$ for $\neg \textsf{Kenya}$ is thus
$\Box$, which is sent back to $P_4$ and then to $P_3$. After combination on $P_3$ with $\textsf{Palu}$
we thus obtain  $\textsf{Palu}$ as a new consequent of $\textsf{Kenya}$, which subsumes the previously obtained
 $\neg\textsf{Lodge}�\vee \textsf{Palu}$. When transmitted back to $P_1$ and combined with
 $\textsf{Hotel}$ we obtain $\textsf{Hotel}�\vee \textsf{Palu}$ which subsumes the
previously obtained consequent  $\textsf{Hotel}�\vee \neg\textsf{Lodge} \vee \textsf{Palu}$.
Since $\textsf{AntiM}$ is not a shared variable
it is the only consequent of $\textsf{Palu}$ on  $P_4$. When 
transmitted back to $P_3$ for combination with $\Box$, we thus obtain $\textsf{AntiM}$ which,
in turn, is returned to $P_1$ for combination with $\textsf{Hotel}$, thus giving 
$\textsf{Hotel} \vee \textsf{AntiM}$ as a new consequent of \textsf{Far}.


\begin{center} 
\scalebox{0.9}{
{\scriptsize
  \pstree[thislevelsep=3.6cm] %
     {% Root  Node
        \TC*[radius=2pt]
     } % Root  Node
     { % Branches
      \pstree[thislevelsep=2.8cm,treesep=1.5cm]
       {% Root  Node2
         \Tr[name=P1]{
          \psframebox{
           $
            \begin{array}{l l l}
                P_1:~\\
              \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Exp}}  & 
                          ~~~~~~\rnode{P1Int}{\textsf{Int}} &
                          ~~~~~~ \rnode{P1Chile}{\textsf{Chile}} \vee \rnode{P1Kenya}{\textsf{Kenya}}
             \end{array}
           $
          }%psframebox
        }%Tr
          \tlput{\begin{tabular}{r}
                      $Far$ \\
                      ~
                      \end{tabular}
          }
         \trput[labelsep=1pt]{\rput(1.7,0.4){
                  $
                  \begin{array}{l}
                        \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Exp} ~~ \textsf{Pass}} \\
                        \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Hotel} \vee \textsf{YellowFev}} \\
                        \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Hotel} \vee\textsf{Lodge}}\\
                         \uparrow \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Hotel} \vee \textsf{Palu}}\\
                         \uparrow \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Hotel} \vee \textsf{AntiM}}\\
                         \uparrow \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Hotel} \vee \textsf{...}}\\
                         ~
                   \end{array}
                  $
                 } }
      }% Root  Node2
      {   % Branches 2
        % First Node      
          \Tr[name=P2,edge=none]{\psframebox{
           $ 
             \begin{array}{l}
             P_2:\\
              \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Pass}}
            \end{array}
           $
           }}% First Son

        % Second Node      
          \Tr[name=P41,edge=none]{\psframebox{
           $ 
             \begin{array}{l}
             P_4:\\
              \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Hotel}}~~~
            \end{array}
           $
           }}% Second Son

        % Third Son
          \pstree[thislevelsep=1.8cm,treesep=1cm]
            {% Root of the third Son
              \Tr[name=P3,edge=none]{\psframebox{
                    $
                    \begin{array}{l l}
                           P_3:\\
                           \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{
                               \textsf{YellowFev}
                           }
                           &  
                           \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{
                                \rnode{P3Lodge}{\neg\textsf{Lodge}}
                            }
                               \vee
                          \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{
                               \rnode{P3Palu}{\textsf{Palu}}
                           }\\
                  \end{array}
                  $ 
                 }} 
               }% Root of the second Son of the third one
               {
                   \pstree[thislevelsep=1.8cm]
                    {
                       \Tr[name=P45,edge=none]{
                           \psframebox{
                                $ 
                                \begin{array}{l}
                                    P_4:~ \\
                                   \neg \rnode{P45Kenya}{\textsf{Kenya}}
                                \end{array}
                                $
                            }%psframebox
                        } % Tr
                     } 
                     {
                         \Tr[name=P11,edge=none]{
                               \psframebox{
                                      $
                                       \begin{array}{l}
                                           P_1: ~\\
                                       \end{array}
                                      $
                              }
                           }
                       }                         

                       \Tr[edge=none,name=P46]{
                          \psframebox{
                           $ 
                             \begin{array}{l}
                                P_4:~\\
                                     \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{AntiM}}
                             \end{array}
                            $
                        }} % 
              }

          % Fourth Son
          \pstree[thislevelsep=1.8cm,arrows=-]
              {\Tr[name=P42,edge=none]{
                     \psframebox{
                            $
                               \begin{array}{l}
                                     P_4:\\
                                    \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{
                                           \rnode{P42Lodge}{\textsf{Lodge}}
                                      }             
                               \end{array}
                             $ 
                }} % Fourth Node root          
               } 
              {
                   \Tr[edge=none,name=P31]{
                       \psframebox{
                           $ 
                             \begin{array}{l}
                                P_3:~\\
                                ...
                             \end{array}
                            $
                        }
                   } % Tr
              }
        }% Branches  2     
    } % Branches  
    \ncline[nodesepB=2pt]{-}{P2}{P1Int}
    \nbput{\rput(0.2,-0.1){
                      \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Pass}}
                 }}

    \ncline[nodesepB=2pt]{-}{P41}{P1Chile}
    \nbput{\rput(0.2,-0.2){
                   \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Hotel}}
               }}

    \ncline[nodesepB=2pt]{-}{P3}{P1Kenya}
    \nbput{\rput(0.7,-0.1){
                                $
                                 \begin{array}{l}
                                     \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\mathsf{YellowFev}} \\
                                     \uparrow \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\mathsf{Palu}} \\
                                    \uparrow \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\mathsf{AntiM}} \\
                                  \end{array}
                                $
              }}
      \ncline[nodesepB=2pt]{-}{P42}{P1Kenya}
     \nbput{\rput(1.2,-0.2){
                               $
                                 \begin{array}{l}
                                     \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{Lodge}} \\
                                     \uparrow \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\ldots} \\
                                 \end{array}
                                $
               }}

    \ncline[nodesepB=2pt]{-}{P45}{P3Lodge}
   \nbput{\rput(0.2,0){
                           $\uparrow$ \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{$\Box$}
                }
  }

   \ncline[nodesepB=2pt]{-}{P46}{P3Palu}
    \nbput{\rput(0.6,-0.1){
                           $\uparrow$ \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{\textsf{AntiM}}
               }
    }

   \ncline[nodesepB=2pt]{-}{P31}{P42Lodge}
  \nbput{\rput(0.3,-0.1){
                           $\uparrow$ \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{$...$}
               }
   }

   \ncline[nodesepB=2pt]{-}{P11}{P45Kenya}
   \nbput{\rput(0.2,-0.1){
                           $\uparrow$ \psframebox[fillcolor=lightgray,linecolor=lightgray,fillstyle=solid]{$\Box$}
                 }
 }



 } % scriptsize
 } % scalebox
\end {center} 




We have not detailed the production of consequences of $\textsf{Lodge}$ on $P_3$ in the right most branch.
The reader could check in a similar way that 
it also produces $\textsf{AntiM}$ (which has already been produced through $P_{3}/P_{4}$ in the third branch).
Eventually, the whole set of consequences of $\textsf{Far}$ is 
$\{\textsf{Exp},
     \textsf{Pass},
     \textsf{Hotel} \vee \textsf{Lodge},
     \textsf{Hotel} \vee \textsf{Palu},
     \textsf{Hotel} \vee \textsf{AntiM},
     \textsf{Hotel} \vee \textsf{YellowFev}\}$. 
Among those consequences, it is important to note that some of them (e.g.,
$\textsf{Hotel} \vee \textsf{YellowFev}$) 
involve target variables from different peers. Such implicates could not be 
obtained by partition-based algorithms like those in \cite{Amir2000}.
This is made possible thanks to the split/recombination strategy of our algorithm.

%Distributed consequence finding algorithm
\section{Distributed Consequence Finding Algorithm}
\label{algo}
The message passing distributed algorithm that we have implemented is 
described 
in Section \ref{message}. We show that it terminates and that it computes
the same results as the recursive algorithm described in Section 
\ref{recursive}. We exhibit a property of the acquaintance graph that 
guarantees the completeness of this recursive algorithm, and therefore of
the message passing distributed algorithm (since both algorithms compute the
same results).



\noindent
For both algorithms, we will use the following notations :

\begin{itemize}
   \item for a literal $q$, $Resolvent(q,P)$ denotes the set of clauses 
             obtained by resolution from the set $P \cup \{q\}$ but not from
             $P$ alone. We call such clauses \em{proper resolvents} of $q$ w.r.t. $P$,

     \item for a literal $q$, $\bar q$ denotes its complementary literal,

      \item for a clause $c$ of a peer $P$, $S(c)$ (resp. $L(c)$) denotes the 
                disjunction of literals  of $c$ whose variables are shared (resp. not shared)
                with some acquaintance of $P$. 
                The condition $S(c) = \Box$ thus expresses that 
                $c$ does not contain any variable shared with an acquaintance of $P$,

      \item a history $hist$ is a sequence of triples $(l,P,c)$ 
               (where $l$ is a literal, $P$ a peer, and $c$ a clause).
              An  history  $[(l_n,P_n,c_n),\ldots,$ $(l_1,P_1,c_1),(l_0,P_0,c_0)]$
              represents a branch of reasoning initiated by the propagation 
              of  the literal $l_0$ within the peer $P_0$, which either contains the clause 
              $\neg l_0 \vee c_0$ (in that case $c_0$ may have been splitted into
             its different literals among which $l_1$ is propagated in $P_1$), or not
            (in that case $l_0 = c_0$ and $l_0$ is propagated into $P_1$, and thus 
            $l_0= l_1$): for every $i \in [0..n-1]$, $c_i$ is a consequence of $l_i$ and
             $P_i$, and $l_{i+1}$ is a literal of $c_i$, which is propagated in $P_{i+1}$,

      \item $\ovee$ is the distribution operator on sets of clauses: 
        $S_1 \ovee \cdots \ovee S_n$ = $\{c_1 \vee \cdots \vee c_n$ $| c_1 \in S_1,
      \ldots, c_n \in S_n\}$.
       If $L = \{l_1, \ldots, l_p\}$, we will use the notation 
        $\ovee_{l \in L} S_l$ to denote $S_{l_1} \ovee \cdots \ovee S_{l_p}$.

\end{itemize}

\subsection{Recursive Consequence Finding Algorithm}
\label{recursive}
Let $\Gamma = (\mathcal{P},\mbox{\sc acq})$  be a P2PIS, $P$ one of its peers,
and $q$ a literal whose variable belongs to the vocabulary of $P$.
$RCF(q, P)$ computes implicates of the literal 
$q$ w.r.t.  ${\cal P}$, 
starting with the computation of local consequences of $q$, i.e., implicates
of $q$ w.r.t.   $P$, and then recursively following the acquaintances
of the visited peers.
To ensure termination, it is necessary to keep track of the literals already 
processed by peers. This is done by
the recursive algorithm $RCFH(q,SP ,  hist)$, where $hist$
is the history of the reasoning branch ending up to the propagation of
the literal $q$ in $SP$, which is the set of acquaintances of the last peer 
added to the history.

\begin{algorithm}[!h]
\caption{Recursive consequence finding algorithm}
%\vspace{-0.5cm}
\algname{$RCF$}{$q, P$}
\begin{algtab}
\algreturn $RCFH(q, \{P\} , \emptyset)$ \\
\end{algtab}
\vspace{0.5cm}
\algname{$RCFH$}{$q, SP,hist$}
\begin{algtab}
{\bf if} there exists $P\in SP$ s.t. $q \in P$ or if for every $P \in SP$, $\, (q,P, \_) \in hist$
{\bf return} $\emptyset$ \label{alg1:returnVide}\\
{\bf else} {\bf if} ($\bar q,\_,\_) \in hist$ {\bf return} $\{\Box\}$
\label{alg1:returnBox1}\\
{\bf else} 
for every $ P \in SP$ \, $\mbox{\sc local}(P) \leftarrow \{q\} \cup Resolvent(q,P)$ \\
{\bf if} there exists $P \in SP$ s.t. $\Box \in \mbox{\sc local}(P)$ {\bf return} $\{\Box\}$ 
\label{alg1:returnBox2}\\
{\bf else} for every $ P \in SP$ \,$\mbox{\sc local}(P) 
\leftarrow \{c \in \mbox{\sc local}(P)| L(c) \in \mathcal{T}arget(P) \}$\\
{\bf if} for every $ P \in SP$ and for every $c \in \mbox{\sc local}(P)$,  $S(c) = \Box$, {\bf return}
 $\bigcup_{P \in SP}${\sc local}$(P)$  \label{alg1:returnLocal}\\
{\bf else} \\
\tab $\mbox{\sc result} \leftarrow 
\bigcup_{P \in SP}\{c \in \mbox{\sc local}(P) | S(c) \in \mathcal{T}arget(P)\}$ \\
\tab \algforeach 
{\label{alg1:foreach} $P \in SP$ and $c \in \mbox{\sc local}(P)$  s.t. $S(c) \neq \Box$} 
\tab {\bf if} $\neg q \vee c \in P$, 
$P \leftarrow P  \backslash \{\neg q \vee c \}$ \\
\tab \algforeach {\label{alg1:foreach2} literal $l \in S(c)$ } 
\label{alg1:answer} 
\tab $\mbox{\sc answer}(l) \leftarrow$ 
$RCFH(l,\mbox{\sc acq}(l,P), [(q,P,c)|hist])$ \\
\algend
\tab $\mbox{\sc disjcomb} \leftarrow (\ovee_{l \in S(c)} \mbox{\sc answer}(l)) \ovee \{L(c)\} $  \label{alg1:distrib}\\
\tab $\mbox{\sc result}   \leftarrow \mbox{\sc result} \cup \mbox{\sc disjcomb}$\\
\algend
\tab \algreturn $\mbox{\sc result}$\\

\end{algtab}
\end{algorithm}

%\pagebreak
We now establish properties of this algorithm. Theorem~\ref{soundness} states
that the algorithm is guaranteed to terminate and that it is sound. 
Theorem~\ref{completeness} exhibits a condition on the acquaintance 
graph for the algorithm to be complete. 
For the properties of soundness 
and completeness, we consider that the topology and the content of the P2PIS 
do not change while the algorithm is running. 
Therefore, those properties have the following meaning  for a P2PIS:
%
the algorithm is sound (respectively, complete) iff for every P2PIS, 
the results returned by 
$RCF$($q,P$), where $P$ is any peer of the P2PIS and $q$ 
any literal whose variable belongs to the vocabulary of $P$, are implicates
(respectively, include all the proper prime implicates) of $q$ w.r.t.   
the union of all the peers in the P2PIS, {\em if there is no change
in the P2PIS while the algorithm is running}.

The sufficient condition exhibited in Theorem~\ref{completeness}
for the completeness of the algorithm is a global property of 
the acquaintance graph: any two peers having a variable in common must be
either acquainted (i.e., must share that variable) or must be related by 
a path of acquaintances sharing that variable. 
First, it is important to emphasize that even if that
property  is global, it has not to be checked before running the algorithm. 
If it is not verified, the algorithm remains sound but not complete.
Second, it is worth noticing that the modeling/encoding of  applications
into our general peer-to-peer propositional reasoning setting may result
in acquaintance graphs satisfying that global property by construction.
In particular, as it will be shown in 
Section~\ref{somewhere} (Proposition \ref{property}),
it is the case for the propositional encoding of the Semantic Web applications
that we deal with in \somewhere.


\begin{theorem}
\label{soundness}
Let $P$ be a peer of a P2PIS and $q$ a literal belonging to the vocabulary of
$P$. $RCF$($q,P$) is sound and terminates. 
\end{theorem}
\begin{proof}
\noindent
{\bf Soundness: } We need to prove that every result returned by $RCF$($q,P)$ 
    belongs to the target language and is an implicate of 
$q$ w.r.t.   $\mathcal{P}$, where $\mathcal{P}$ is the union 
of all the peers in the P2PIS. 
For doing so, we prove by induction on the 
number $rc$ of recursive
calls of $RCFH$($q, SP,hist)$ that every result returned by
$RCFH$($q, SP, hist)$ (where the history $hist$, if  not empty,
is of the form $[(l_n,P_n,c_n),\ldots,(l_0,P_0,c_0)]$)  
is an implicate of $q$ w.r.t. 
$\mathcal{P} \cup \{l_n, \ldots, l_0\}$ which belongs to
the target language.

\begin{itemize}
\item $rc$ = $0$: either one of the conditions of
          Line (\ref{alg1:returnVide}), Line (\ref{alg1:returnBox1}),
          Line (\ref{alg1:returnBox2}) or Line (\ref{alg1:returnLocal}) is satisfied.

\tab - If the condition in Line (\ref{alg1:returnVide}) is satisfied, 
the algorithm returns an empty result.\\
         \tab - If either there exists a peer $P$ such that $(\bar q , \_, \_) 
          \in hist$ or $\Box \in \mbox{\sc local}(P)$:  in both cases,
           $\Box$ is returned by the algorithm (in respectively Line
          (\ref{alg1:returnBox1}) and Line (\ref{alg1:returnBox2})) and it is indeed
          an implicate of $q$ w.r.t.  ${\cal P} \cup \{l_n, \ldots, l_0\}$ belonging to
           the target language.



          \tab - Let $r$ be
a result returned by the algorithm at Line (\ref{alg1:returnLocal}):
          there exists $P \in SP$ such that $r \in \mbox{\sc local}(P)$, 
and it is obvioulsy
         an implicate of $q$ w.r.t.  ${\cal P} \cup \{l_n, \ldots, l_0\}$
          (as $q$ or a resolvent of $q$ and of a clause of $P$), and it
         belongs to the target language.

% Cas recursif
\item Suppose the induction hypothesis true for $rc \leq p$, and let $SP$ 
be a set of peers of a P2PIS and $q$ a literal (belonging to the vocabulary
of all the peers of $SP$) such that 
         $RCFH$($q,SP,hist)$ requires  $p+1$
          recursive calls to terminate. Let $r$ be a result returned by $RCFH$($q,SP,hist)$.

          - If $r \in \mbox{\sc local}(P)$ for a $P \in SP$ and is such that 
            $S(r) = \Box$ or $S(r) \in \mathcal{T}arget(P)$, it is obviously an implicate 
           of $q$ w.r.t. 
          ${\cal P} \cup \{l_n, \ldots, l_0\}$ belonging to the target language.

         - If  $r \not \in \mbox{\sc local}(P)$ for any $P \in SP$, 
           it is obtained at
          Line (\ref{alg1:distrib}): there exist $P \in SP$ and
 a clause $c$ of $P$ of the form $S(c) \vee L(c)$ 
         such that $S(c) = ll_1 \vee \cdots \vee ll_k$ and $r = r_1$ $\vee \cdots \vee$ 
          $r_k \vee L(c)$, where every $r_i$ is a result returned by
          $RCFH(ll_i,\mbox{\sc acq}(ll_i,P), [(q,P,c)|hist])$ (Line 
          (\ref{alg1:answer})).
        According to the induction hypothesis (the number of recursive calls
        of  $RCFH(ll_i,\mbox{\sc acq}(ll_i,P),  [(q,P,c)|hist])$ for every
        $ll_i$ is less than or equal to $p$), every $r_i$ belongs to the target language
and is an implicate of $ll_i$ w.r.t. 
        ${\cal P} \backslash \{\neg q \vee c \} \cup \{q,  l_n, \ldots, l_0\}$,
or, equivalently, an implicate of $q$ w.r.t.  ${\cal P} \backslash \{\neg q \vee c \} \cup \{ll_i,  l_n, \ldots, l_0\}$.

Therefore, $r_1 \vee \cdots \vee r_k$  belongs to the target language and 
is an implicate of $q$ w.r.t. 
${\cal P} \backslash \{\neg q \vee c \} \cup \{S(c),l_n, \ldots, l_0\}$.
Since $L(c)$ belongs to the target language and $c = S(c) \vee L(c)$, 
        $r$ (i.e, $r_1 \vee \cdots \vee r_k$
        $\vee L(c)$) belongs to the target language, and is an implicate
        of $q$ w.r.t.  ${\cal P} \backslash \{\neg q \vee c \} 
\cup \{c,  l_n, \ldots, l_0\}$, and a fortiori of $q$ w.r.t.  
${\cal P} 
\cup \{c,  l_n, \ldots, l_0\}$
        Since $c \in \mbox{\sc local}(P)$, $c$ is an implicate of $q$ w.r.t. 
${\cal P}$, and therefore $r$ is an implicate of $q$ w.r.t.  ${\cal P} \cup 
\{l_n, \ldots, l_0\}$.
\end{itemize}

\noindent {\bf Termination: }
at each recursive call, a {\em new} triple $(sl, P,c)$ is added to the  
history.
If the algorithm did not terminate, the history would be infinite, which
is not possible since the number of peers, literals and clauses
within a P2PIS is finite.

\end{proof}


The following theorem exhibits a sufficient condition for the algorithm to be
complete. 
\begin{theorem}
\label{completeness} 
Let $\Gamma=(\mathcal{P},\mbox{\sc acq})$ be a P2PIS.
If for every $P$, $P'$ and $v \in  \mathcal{V}_P\cap\mathcal{V}_{P'}$ there exists a path 
between $P$ and $P'$ in $\Gamma$, all edges of which are labelled with $v$, 
then for every literal $q \in  \mathcal{L}_P$, $RCF$($q,P)$ 
computes all the proper prime implicates of $q$ w.r.t.  $\mathcal{P}$  
which belong to $\mathcal{T}arget(\mathcal{P})$.
\end{theorem}

\begin{proof}
In fact, we prove that  $RCF$($q,P)$ computes at least all the {\em prime} proper resolvents
of $q$ w.r.t. $P$, i.e., the elements of $Resolvent(q,P)$ that are not strictly subsumed by other
elements of  $Resolvent(q,P)$. 

We first show that proper prime implicates of $q$ w.r.t. $P$ are prime proper resolvents of $q$ w.r.t. $P$.
Let $m$ be a proper prime implicate of $q$ w.r.t. $P$. By definition  $P \cup \{q\} \models m$
and  $P \not \models m$. By completeness of resolution w.r.t. prime implicates, $m$ can be 
obtained by resolution from the set $P \cup \{q\}$ but not from $P$ alone, i.e., it is 
a proper resolvent of $q$ w.r.t. $P$. Let us suppose that $m$ is strictly subsumed by another
element $m'$ of $Resolvent(q,P)$. This means that $P \cup \{q\} \models m' \models m$ 
and $m \not \equiv m'$, which contradicts that $m$ is a prime implicate of
$q$  w.r.t. $P$.

Now we prove by induction on the maximum number $rc$ of recursive calls involving
a same literal  when triggering  $RCFH$($q, SP, hist)$ that $RCFH$($q, SP, hist)$
computes all the proper prime implicates  belonging to the target language of $q$ w.r.t.  ${\cal P}(hist)$, where
${\cal P}(hist)$ is obtained from ${\cal P}$  by replacing each 
$\neg l_i \vee c_i$ by $l_i$ if $l_i \neq c_i$. Thus:

${\cal P}(hist)$ = ${\cal P}$ if $hist$ is empty, 

\noindent 
otherwise:

${\cal P}(hist)$ = ${\cal P} \backslash \{\neg l_i \vee c_i | (l_i,P_i,c_i) \in hist$ s.t. $l_i \neq c_i\}$ $ \cup \{l_i| (l_i,P_i,c_i) \in hist$ 
s.t. $l_i \neq c_i\}$ \\


If the history $hist$ is not empty, it is of the form 
$[(l_n,P_n,c_n),\ldots,(l_0,P_0,c_0)]$. 
According to the algorithm, when $RCFH(q, SP, hist)$ is triggered, 
there have been at least $n+1$ previous calls of
the algorithm $RCFH$: $RCFH(l_0, SP_0, \emptyset$) and  
$RCFH(l_i, SP_i, hist_i)$ for $i \in [1..n]$, where 
$hist_i$ =$[(l_{i-1},P_i, c_{i-1})\ldots,(l_0,P_0,c_0)])$, 
and $P_i \in SP_i$ for every $i \in [0..n]$.
Since the P2PIS can be cyclic, it may be the case that when we
call $RCFH(q, SP, hist)$, $(q,P,q)\in
hist$. If that is the case, there have been previous calls of $RCFH$ 
involving $q$, i.e., of the form
$RCFH(q,SP_i,hist_i)$.

\begin{itemize}
% Cas de base
\item $rc$ = $0$: either one of the conditions of 
Line (\ref{alg1:returnVide}), Line (\ref{alg1:returnBox1}), 
Line (\ref{alg1:returnBox2}) or Line (\ref{alg1:returnLocal}) is satisfied.

\tab - If the first condition is satisfied, since $rc = 0$, it cannot 
be the case that for every $P \in SP$, $(q,P,\_) \in hist$, and therefore
there exists $P \in SP$ such that $q \in P$: in this case, there is no 
{\em proper} prime implicate of $q$ w.r.t.  ${\cal P}(hist)$, because $q \in {\cal P}(hist)$
and all the prime implicates  of $q$ w.r.t.  a theory containing $q$ are consequences of that theory.
 
\tab - If either $(\bar q , \_, \_) \in hist$ or 
$\Box \in \mbox{\sc local}(P)$ for a given peer $P$ of $SP$:  in both cases,
$\Box$ is the only prime implicate of 
$q$ w.r.t.  ${\cal P}(hist)$ and therefore, if it is a 
{\em proper} prime implicate, it is the only one too.
It is returned by the algorithm 
(respectively Line (\ref{alg1:returnBox1}) and Line (\ref{alg1:returnBox2})).


\tab - If for every $P \in SP$, every resolvent of $q$ w.r.t.  $P$ has no shared variable
with any acquaintance of $P$: if ${\cal P}$ satisfies the property stated in the theorem, this means that
every prime implicate of $q$ w.r.t.  $P$ has no variable in common with any
other theory of ${\cal P}$. 
According to Lemma \ref{disjoint}, the set of proper resolvents of $q$ w.r.t. 
${\cal P}(hist)$ is included in $\bigcup_{P \in SP}\textsc{local}(P)$, 
and thus in particular every proper prime implicate of $q$ w.r.t. 
${\cal P}(hist)$, which is in the target language, is
returned by the algorithm (Line(\ref{alg1:returnLocal})).


% Induction
\item Suppose the induction hypothesis true for $rc \leq p$, and 
let $SP$ be a set of peers of a P2PIS satisfying the property stated in 
the theorem, such that $RCFH$($q,SP, hist)$ requires  atmost $p+1$
recursive calls involving $q$. Since there is at least one recursive call,
the condition of 
Line (\ref{alg1:returnVide}) is not satisfied. 
Let $m$ be in the
target language and a proper prime implicate of $q$ w.r.t.  
${\cal P}(hist)$, where 
${\cal P}(hist)$ = ${\cal P} \backslash \{\neg l_i \vee c_i | (l_i,P_i,c_i) 
\in hist$ s.t. $l_i \neq c_i\}$ $ \cup \{l_i| (l_i,P_i,c_i) \in hist$ 
s.t. $l_i \neq c_i\}$. 
Let us show that $m$ belongs to 
the result
returned by $RCFH$($q,SP, hist)$. 

- If $m$ is a proper resolvent of $q$ w.r.t.  a given $P$ of $SP$, then 
$m \in \mbox{\sc local}(P)$ and is returned by the
algorithm since it is in the target language. 

-If $m$ is not a proper resolvent of $q$ w.r.t.  a given $P$ of $SP$, then, according to Lemma \ref{disjoint}, 
either (i) $q$ has its variable in common with clauses in 
${\cal P}(hist)\backslash \bigcup_{P \in SP}P$, or (ii)
there exists a clause $\neg q \vee c$ in $\bigcup_{P \in SP}P$ 
such that $c$  has variables in common with 
${\cal P}(hist) \backslash \bigcup_{P \in SP}P$ and 
$m$ is a proper resolvent of $c$
w.r.t.  ${\cal P}(hist) \backslash \{\neg q \vee c \} \cup \{q\}$.
In addition, it is a {\em prime} proper resolvent of $c$ w.r.t. 
${\cal P}(hist) \backslash \{\neg q \vee c \} \cup \{q\}$.
Let us suppose that this is not the case. Then there exists some 
clause $m' \in Resolvent(c, {\cal P}(hist) \backslash \{\neg q \vee c \} \cup \{q\})$,
such that $m' \models m$ and $m' \not \equiv m$. 
By soundness,  ${\cal P}(hist) \backslash \{\neg q \vee c \} \cup \{q\} \cup
\{c\} \models m'$. Since ${\cal P}(hist) \backslash \{\neg q \vee c \} \cup \{q\}
\cup\{c\}
 \equiv  
{\cal P}(hist) \cup \{q\} $,  ${\cal P}(hist) \cup \{q\} \models m'$ with 
$m' \models m$ and $m' \not \equiv m$, which contradicts that $m$ is a 
prime implicate of $q$ w.r.t. ${\cal P}(hist)$.


\tab (i) In the first case, according to the property stated in the theorem, 
the variable of $q$ is shared with other peers of the P2PIS than those in 
$SP$, and therefore $q$ is involved in an iteration of
the loop of Line (\ref{alg1:foreach}).
According to the induction hypothesis (the number of recursive calls to 
obtain $\mbox{\sc answer}(q)$ in Line (\ref{alg1:answer})  is 
less than or equal to $p$) $\mbox{\sc answer}(q)$ 
includes the set of proper prime resolvents of $q$ w.r.t.  
${\cal P}(hist')$, which are in the target language, where 
$hist' = [(q,P,q)|hist]$, and thus ${\cal P}(hist')$ = ${\cal P}(hist)$.
Therefore, $\mbox{\sc answer}(q)$
includes the set of proper prime resolvents of $q$ w.r.t.  
${\cal P}(hist)$, 
in particular $m$. \\
\tab (ii) In the second case, according to the property stated in the theorem, 
$c$ shares variables with other peers of the P2PIS than those in 
$SP$. In addition, since $m$ is in the target language, the local variables
of $c$ are target variables. Therefore
$c$ is involved in an iteration of the loop of Line (\ref{alg1:foreach}).
According to the induction hypothesis (the number of recursive calls to 
obtain $\mbox{\sc answer}(l)$ in Line (\ref{alg1:answer})  is 
less than or equal to $p$),  for every $l \in S(c)$, 
$\mbox{\sc answer}(l)$ 
includes the set of all proper prime resolvents of $l$ w.r.t.  ${\cal P}(hist')$
and thus in particular, the set of all proper prime implicates 
 of $l$ w.r.t.  ${\cal P}(hist')$ which are in the target language.
Since $hist' = [(q,P,c)|hist]$ with $q \neq c$ (because there is no duplicate
literals in the clauses that we consider), 
${\cal P}(hist')$ = ${\cal P}(hist) \backslash \{\neg q \vee c \} \cup \{q\}$.
We can   apply Lemma \ref{split} to infer that 
$DisjComp$, which is computed in Line (\ref{alg1:distrib}),
includes the set of proper prime implicates of
$c$ w.r.t.  ${\cal P}(hist) \backslash \{\neg q \vee c \} \cup \{q\}$, 
which are in the target language,  and in particular $m$.
\end{itemize}
\vspace{-0.9cm}
\end{proof}

\begin{lemma}
\label{disjoint}
Let $P$ be a set of clauses and $q$ a literal.
Let $P' \subseteq P$ such that it contains
clauses having a variable in common with $q$.
If $m$ is a proper resolvent of $q$ w.r.t.  $P$, then :
\begin{itemize}
  \item either $m$ is a proper resolvent of $q$ w.r.t.  $P'$, 

  \item  or the variable of $q$ is common with clauses of $P \backslash P'$, 

  \item  or there exists a clause $\neg q \vee c$ of $P'$ such that $c$ has  
            variables in common with  clauses of $P \backslash P'$ and  
            $m$ is a proper resolvent of $c$  w.r.t. 
             $P \backslash \{\neg q \vee c \} \cup \{q\}$.
\end{itemize}
\end{lemma}
\begin{proof}
Let $m$ be a proper resolvent of $q$ w.r.t.  $P$.
If $m$ is different from $q$, there exists a clause $\neg q \vee c$ in $P$ such that 
$m$ is a proper resolvent of $c$ w.r.t.  $P \cup \{q\}$. Since 
$P \backslash \{\neg q \vee c \} \cup \{q\} \equiv P \cup \{q\}$,
$m$ is a proper resolvent of $c$ w.r.t.  
$P \backslash \{\neg q \vee c \} \cup \{q\}$.

\begin{itemize}
  \item If such a clause does not exist in $P'$, it exists  in $P\backslash P'$ 
           and therefore  the variable of $q$ is common  with clauses of
           $P \backslash P'$.

  \item If there exists a clause $\neg q \vee c$ in $P'$ such that $m$ is a proper 
            resolvent of $c$ w.r.t.  $P \backslash \{\neg q \vee c \} \cup \{q\}$, and 
            $m$ is not a proper resolvent of $q$ w.r.t.  $P'$, then for every proof 
           of $m$ there must exist a  clause $c'$ in  $P\backslash P'$ with which 
           either $q$ or $\neg q \vee c$ must be resolved.
          Therefore, either $q$ or $c$ has variables in common with clauses 
          of $P \backslash P'$.
\end{itemize}
\vspace{-0.9cm}
\end{proof}

\begin{lemma}
\label{split}
Let $P$ be a set of clauses, and let  $c = l_1 \vee \cdots \vee l_n$ be a clause.
For every proper prime implicate $m$ of $c$  w.r.t.  $P$, 
there exists  $m_1, \ldots, m_n$ such that $m \equiv m_1 \vee \cdots \vee m_n$, and
for every $i \in [1..n]$,  $m_i$ is a proper prime implicate of $l_i$ w.r.t.  $P$.
\end{lemma}

\begin{proof}
Let $m$ be a proper prime implicate of $c$ w.r.t.  $P$.
For every literal $l_i$, let $Mod(l_i)$ be the set of models of $P$ which make $l_i$ true.
If $Mod(l_i) = \emptyset$, that means that $\Box$ is the only proper prime implicate of $l_i$ w.r.t.  $P$.
For every $i$ such that $Mod(l_i) \neq \emptyset$, every model in $Mod(l_i)$ is a model of $P \cup \{c\}$,
and then a model of $m$ ; therefore, $m$ is a proper implicate of $l_i$ w.r.t. $P$, 
and, by definition of proper {\em prime} implicates, there exists a 
proper prime implicate $m_i$ of $l_i$ w.r.t.  $P$ 
such that $m_i \models m$.
Consequently, there exists $m_1, \ldots, m_n$ such that $m_1 \vee \cdots \vee m_n \models m$, and for
every $i \in [1..n]$,  $m_i$ is a proper
prime implicate of $l_i$ w.r.t.  $P$ ($m_i$ may be $\Box$).
Since $P \cup \{l_1 \vee \cdots \vee l_n \}  \models m_1 \vee \cdots \vee m_n $ , and $m$ 
is a proper implicate of $l_1 \vee \cdots \vee l_n$ w.r.t.  $P$, we necessarily get that
$m \equiv m_1 \vee \cdots \vee m_n$.
\end{proof}

\subsection{Message-based Consequence Finding Algorithm}
\label{message}
In this section, we exhibit the result of the transformation of the previous
recursive algorithm into \deca: a message-based \textsc{De}centralized Consequence 
finding Algorithm running locally on each peer. \deca\ is 
composed of three procedures, each one
being triggered by the reception of a message.
The procedure $\mbox{\sc ReceiveForthMessage}$
 is triggered by the reception of a 
$forth$ message $m(Sender, Receiver, forth, hist, l)$ sent by the peer $Sender$ to 
the peer $Receiver$ which executes the procedure: on the demand of $Sender$,
with which it shares the variable of $l$,
it processes the literal $l$.
The procedure $\mbox{\sc ReceiveBackMessage}$
is triggered by the reception of a $back$
message $m(Sender, Receiver, back, hist ,r)$
sent by the peer $Sender$ to 
the peer $Receiver$ which executes the procedure: it processes the consequence
$r$ 
(which is a clause the variables of which are target variables) sent back by
$Sender$  for the literal $l$ (last added in the history) ; it may have to combine it with
other consequences of literals being in the same clause as $l$.
The procedure $\mbox{\sc ReceiveFinalMessage}$
is triggered by the reception of a $final$
message $m(Sender, Receiver, final, hist ,true)$: the peer 
$Sender$ notifies 
the peer $Receiver$ that computation of the consequences of the literal 
$l$ (last added in the history) is completed. 
Those procedures handle two data structures stored at each peer:
$\mbox{\sc cons}(l,hist)$ caches the consequences of $l$ computed by the
reasoning branch corresponding to $hist$ ; 
$\mbox{\sc final}(q,hist)$ is set to true when the propagation of $q$ within the
reasoning branch of the history $hist$ is completed.


The reasoning is initiated by the user (denoted by a particular peer $User$) 
sending to a given peer $P$ a message $m(User, P, forth, \emptyset, q)$. 
This triggers on the peer $P$ the local execution of the procedure 
$\mbox{\sc ReceiveForthMessage}(m(User,P,forth,\emptyset,q))$.
In the description of the procedures, since they are locally executed
 by the peer which receives the message, we will denote by $Self$ the receiver
peer.

\begin{algorithm}[!h]
\caption{\deca\  message passing procedure for propagating literals forth}
%\vspace{0.5cm}
{\small
\algname{ReceiveForthMessage}{$m(Sender,Self,forth,hist,q)$}
\begin{algtab}       
\label{alg2:box1} \algif{$(\bar q, \_, \_) \in hist$} 
{\bf send} $m(Self, Sender, back, [(q,Self,\Box) |hist], \Box)$ 
\label{alg2:ReturnBox1}\\
{\bf send} $m(Self,Sender, final, [(q,Self,true) |hist], true)$ 
\label{alg2:ReturnFinal1}\\
\algelsif {\label{alg2:empty} $q \in Self$ or $(q, Self, \_) \in hist$}
{\bf send} $m(Self,Sender, final, [(q,Self,true) |hist], true)$ 
\label{alg2:ReturnFinalEmpty}\\
\algelse 
$\mbox{\sc local}(Self) \leftarrow \{q\} \cup Resolvent(q,Self)$ \\
\label{alg2:box2} \algif {$\Box \in \mbox{\sc local}(Self)$}
{\bf send} $m(Self, Sender, back, [(q,Self,\Box) |hist], \Box)$ 
\label{alg2:ReturnBox2}\\
{\bf send} $m(Self,Sender,final,[(q,Self,true)|hist],true)$\label{alg2:ReturnFinal2}\\
\algelse $\mbox{\sc local}(Self)\leftarrow
\{c\in\mbox{\sc local}(Self)|$ $L(c)$ $\in$ $\mathcal{T}arget(Self)\}$\\
\label{alg2:local} \algif {for every $c \in \mbox{\sc local}(Self), 
S(c) = \Box$}
\algforeach{$c \in \mbox{\sc local}(Self)$}
{\bf send} $m(Self, Sender, back,[(q,Self,c)|hist], c)$ 
\label{alg2:ReturnLocal}\\
\algend
{\bf send} $m(Self,Sender,final,[(q,Self,true)|hist],true)$\label{alg2:ReturnLocalFinal} \\
\algelse 
\algforeach{ \label{alg2:looplocal} $c \in \mbox{\sc local}(Self)$} 
\algif {\label{alg2:local2} $S(c) = \Box$}
{\bf send} $m(Self,Sender,back,[(q,Self,c)|hist],c)$\label{alg2:ReturnLocal2}\\
\algelse
\algforeach {\label{alg2:loopshared} literal $l \in S(c)$}
\algif {$l \in \mathcal{T}arget(Self)$} 
$\mbox{\sc cons}(l,[(q,Self,c)|hist]) \leftarrow \{l\}$ \\
\algelse 
$\mbox{\sc cons}(l,[(q,Self,c)|hist]) \leftarrow \emptyset$ \\
\algend
$\mbox{\sc final}(l,[(q,Self,c)|hist]) \leftarrow false$ \\
\algforeach{$RP \in \mbox{\sc acq}(l,Self)$}
{\bf send} $m(Self, RP, forth, 
[(q,Self,c)|hist], l)$ 
\label{alg2:ReturnShared}\\
\algend
\algend

\algend

\algend

\algend
\end{algtab}
}
\end{algorithm}

\begin{algorithm}[!h]
\caption{\deca\  message passing procedure for processing the return of consequences}
{\small
\algname{ReceiveBackMessage}{$m(Sender,Self, back, hist,r)$}
\begin{algtab}
$hist$ is of the form 
$[(l', Sender,c'), (q, Self, c)|hist']$ \\
{\sc cons}$(l', hist) \leftarrow$ {\sc cons}
$(l',hist) \cup \{ r \}$ \\
{\sc result}$\leftarrow \ovee_{l \in S(c) \backslash \{l'\}} 
\mbox{\sc cons}(l,hist) \ovee \{L(c) \vee r \}$ 
\label{alg3:Returnshared}\\
{\bf if} $hist' = \emptyset$,  $U \leftarrow User$ 
{\bf else} $U \leftarrow$ the first peer $P'$ of $hist'$ \\
\algforeach {$cs \in \mbox{\sc result}$}
{\bf send} $m(Self, U, back, [(q, Self, c)|hist'], cs)$ 
\label{alg3:Sendshared}\\ 
\algend
\end{algtab}
}
\end{algorithm}

\begin{algorithm}[H]
\caption{\deca\  message passing procedure for notifying termination}
{\small
\algname{ReceiveFinalMessage}{$m(Sender,Self, final, hist, true)$}
\begin{algtab}
$hist$ is of the form 
$[(l', Sender,true), (q, Self, c)|hist']$ \\
{\sc final}$(l', hist) \leftarrow true$ \\
\algif{\label{alg4:cond} for every $l \in S(c)$, 
$\mbox{\sc final}(l, hist) = true$}
{\bf if} $hist' = \emptyset$ $\, U \leftarrow User$ 
{\bf else} $U \leftarrow$ the first peer $P'$ of $hist'$ \\
{\bf send} $m(Self, U, final, [(q, Self, true)|hist'], true)$ 
\label{alg4:ReturnFinal}\\ 
\algforeach{$l \in S(c)$}
$\mbox{\sc cons}(l, [(l, Sender, \_), (q,Self,c)|hist']) 
\leftarrow \emptyset$ \\
\algend
\algend
\end{algtab}
}
\end{algorithm}

The following theorem states two important results: 
first, the message-based distributed algorithm computes the same
 results as the algorithm of Section~\ref{recursive}, and thus, is complete 
 under the same conditions as in Theorem~\ref{completeness} ; 
second the user is notified of the termination when it occurs, which is  
crucial for an anytime algorithm. 

\begin{theorem}
Let $r$ be a result returned by $RCF(q, P)$.
If $P$ receives from the user the message $m(User, P, forth, \emptyset, q)$,
then a message $m(P, User, back, [(q,P,\_)], r)$ will be produced.
If $r$ is the last result returned by $RCF(q, P)$, then
the user will be notified of the termination by a message 
$m(P, User, final, [(q,P,true)], true)$.
\end{theorem}
\begin{proof}
We prove by induction on the number of recursive calls of 
$RCFH(q,SP,$ $hist)$ that:

(1) for
any result $r$ returned by 
$RCFH(q,SP, hist)$, there exists $P \in SP$ such that
$P$ is bound to send
a message $m(P,S, back, [(q,P,\_) | hist], r)$ after receiving the
message $m(S,P, forth, hist, q)$,

(2) if $r$ is the last result returned by 
$RCFH(q,SP, hist)$, all the peers $P \in SP$ are bound 
to send
the message $m(P,S, final, [(q,P,true) | hist], true)$, where $S$ is the first peer
in the history.

$\bullet$ $rc$ = $0$:
either one of the conditions of 
Lines (\ref{alg1:returnVide}), (\ref{alg1:returnBox1}), 
(\ref{alg1:returnBox2}) or (\ref{alg1:returnLocal})  of the algorithm 
$RCFH(q,SP, hist)$ is satisfied.
We have shown
in the proof of Theorem \ref{completeness} that if the conditions of 
Lines (\ref{alg1:returnBox1}) and (\ref{alg1:returnBox2}) are satisfied, 
$\Box$ is the only result
returned by the algorithm. 
The condition of Line (\ref{alg1:returnBox1}) of the algorithm 
$RCFH(q,SP, hist)$ corresponds to the condition 
of Line (\ref{alg2:box1}) of the algorithm 
R{\sc eceive}F{\sc orth}M{\sc essage}($m(S,P,$ $forth$, $hist, q)$) for any $P$
of $SP$, which 
triggers the sending of a message $m(P,S, back, [(q,P,\Box)| hist], \Box)$ 
(Line (\ref{alg2:ReturnBox1})) 
and of a 
message $m(P,S, final, [(q,P,true)| hist], true)$ 
(Line(\ref{alg2:ReturnFinal1})).
If the condition of Line (\ref{alg1:returnBox2}) of the algorithm 
$RCFH(q,SP, hist)$ is satisfied, there exists $P \in SP$ such that
$\Box \in P$. 
That condition corresponds to the condition of Line (\ref{alg2:box2}) 
of the algorithm for 
R{\sc eceive}F{\sc orth}M{\sc essage}($m(S,P, forth, hist, q)$), which 
triggers the sending of a message $m(P,S, back, [(q,P,\Box)| hist], \Box)$ 
(Line (\ref{alg2:ReturnBox2}) 
and of a 
message $m(P,S, final, [(q,P,true)| hist], true)$ (Line 
(\ref{alg2:ReturnFinal2})).
The condition (\ref{alg1:returnVide}) of the algorithm 
$RCFH(q,SP, hist)$, in which no result is returned
(see proof of Theorem \ref{completeness}), corresponds to the condition of 
Line (\ref{alg2:empty}) of the algorithm 
R{\sc eceive}F{\sc orth}M{\sc essage}($m(S,P, forth, hist, q)$), for every 
$P \in SP$, which only
triggers the sending of a final message (Line (\ref{alg2:ReturnFinalEmpty})).
Finally, if the condition of  Line (\ref{alg1:returnLocal}) 
of the algorithm $RCFH(q,SP, hist)$ is satisfied,   
there exists $P \in SP$ such that $r \in \mbox{\sc local}(P)$.
The condition of  Line (\ref{alg1:returnLocal}) 
of the algorithm $RCFH(q,SP, hist)$ corresponds to the 
condition of Line (\ref{alg2:local}) in 
R{\sc eceive}F{\sc orth}M{\sc essage}($m(S,P, forth, hist, q)$), which triggers
the sending of all the messages $m(P, S, back, [(q, P, c)|hist], c)$, where
$c$ is a clause of $\mbox{\sc local}(P)$ (Line (\ref{alg2:ReturnLocal})), 
and in particular the message
$m(P, S, back, [(q, P, r)|hist], r)$. 
It triggers too the sending of a final message 
(Line (\ref{alg2:ReturnLocalFinal})) for $P$.
If $r$ is the last result returned by $RCFH(q,SP, hist)$, 
such final messages has been sent by every $P \in SP$.



$\bullet$ Suppose the induction hypothesis true for $rc \leq p$, and 
let $\Gamma = ({\cal P}, \mbox{\sc acq})$ a P2PIS  such that 
$RCFH$($q,SP, hist)$ requires  $p+1$ recursive calls to terminate. 

- If there exists $P \in SP$ such that $r \in \mbox{\sc local}(P)$, 
 $r$ is not the last result returned by the algorithm,
 and $r$ is one of the clauses $c$ involved in the iteration of the 
loop of Line (\ref{alg2:looplocal}) of the algorithm 
R{\sc eceive}F{\sc orth}M{\sc essage}($m(S,P, forth, hist, q)$), and verifying
the condition of Line (\ref{alg2:local2}), which
triggers the sending of the message $m(P, S, back, [(q,P,r)|$ \linebreak $hist], r)$ 
(Line (\ref{alg2:ReturnLocal2})). 

-If there exists $P \in SP$ and a clause $c: l_1 \vee \cdots \vee l_k \vee L(c)$ of  $\mbox{\sc local}(P)$
 such that $c$ is involved in the iteration of the 
loop of Line (\ref{alg1:foreach}) of the algorithm $RCFH(q,P, hist)$, 
and $r$ is an element $r_1 \vee \cdots \vee r_k \vee L(c)$ 
of $(\ovee_{l \in S(c)} \mbox{\sc answer}(l)) \ovee \{L(c)\}$ computed at
 Line (\ref{alg1:answer}), where each $\mbox{\sc answer}(l)$ is
obtained as the result of  
$RCFH(l,\mbox{\sc acq}(l,P), [(q,P,c)|hist])$ 
(Line (\ref{alg1:distrib})), which requires  $p$ or less than $p$ recursive calls. 
By induction, for each literal $l_i \in S(c)$, there exists
$RP_i \in \mbox{\sc acq}(l_i,P)$ 
such that $RP_i$ sends  a message $m(RP_i,P, back, [(l_i, RP_i, \_),$ \linebreak 
$(q,P,c)|hist], r_i)$ if it has received
the message $m(P, RP_i, forth, [(q,P,c)|hist], l_i)$.
The loop of Line (\ref{alg1:foreach2})  of the algorithm 
$RCFH(q,SP,$ $hist)$ corresponds to the loop of Line 
(\ref{alg2:loopshared})
of the algorithm 
R{\sc eceive}F{\sc orth}M{\sc essage}($m(S,P,forth$,$hist$,$q)$), which
triggers the sending of the messages $m(P,$ $ RP_i$ , $forth,$ 
$[(q,P,c)|hist]$, $l_i)$ for each literal $l_i \in S(c)$ (Line 
(\ref{alg2:ReturnShared})).
Therefore, according to the induction hypothesis, for every $l_i \in S(c)$,
$RP_i$ sends
a message $m(RP_i, P, back, [(l_i, RP_i, \_), (q,P,c)|hist], r_i)$.
When the last of those messages (let us say 
$m(RP_j$, $P, back$, $[(l_j, RP_j, \_)$, $(q,P,c)|hist]$, $r_j)$) is processed, 
 $r$ is produced by Line (\ref{alg3:Returnshared}) of 
R{\sc eceive}B{\sc ack}M{\sc essage}($m(RP_j, P$, $back,$ $[(l_j, RP_j, \_)$, $(q,P,c)|hist]$, $r_j)$), and there exists a peer $U$ such that $P$ is bound
to send to it the message $m(P,U, back, [(q,P,c)|hist], r)$ 
(Line (\ref{alg3:Sendshared})).

- If $r$ is the last result returned by the algorithm 
$RCFH$($q,SP$, $hist)$, for every $P$ $\in$ $SP$, for every $c \in \mbox{\sc local}(P)$,
for every $l \in S(c)$,  
$RCFH(l,\mbox{\sc acq}(l,P)$,  $[(q,P,c)|hist])$  has 
finished, and, by induction, every peer $RP$ of $\mbox{\sc acq}(l,P)$ has sent 
a message $m(RP,P,$ $final$, $[(l,RP,true)$, $(q,P,c)|hist]$, $true)$. 
Therefore, 
the condition of Line (\ref{alg4:cond}) of the algorithm 
R{\sc eceive}F{\sc inal}M{\sc essage}($m(RP, P, final,[(l, RP, \_),$ $(q,P,c)|hist],true)$) 
is satisfied, which triggers the sending of a message $m(P,U, final, [(q,P,true)|hist], true)$ (Line (\ref{alg4:ReturnFinal})).

\end{proof}
\reviewers{
The full proof can be obtained upon request to the PC chair. \\
}

For sake of simplicity, both recursive and distributed algorithms have 
been presented as applying to literals. It does not mean that the 
formulas that we consider are limited to literals. Clauses can be
handled by splitting them into literals and then using the $\ovee$ 
operator to recompose the results obtained for each literal.

It is also important to notice that $\Box$ can be returned by our algorithm as a proper prime implicate because of 
the lines (1) to (3) and (8) to (10) in $\mbox{\sc ReceiveForthMessage}$. In that case,  as a corollary of 
the above theorems, the P2PIS is detected unsatisfiable with the
input clause. Therefore, our algorithm  can be exploited for checking the satisfiability of the P2PIS at 
each join of a new peer theory.

%Somewhere: application to the Semantic Web
\section{Application to the Semantic Web: the {\sc somewhere} Peer-to-peer Data Management System}
\label{somewhere}

The Semantic Web \cite{berners-lee} envisions a world wide distributed architecture where data 
and computational resources will easily inter-operate based on 
semantic marking up of web resources using {\em ontologies}. 
Ontologies are a formalization of the semantics of application domains
(e.g., tourism, biology, medicine) through the definition of classes and
relations modeling the domain objects and properties
that are considered as meaningful for the application.
Most of the concepts, tools and techniques deployed so far by the Semantic Web community correspond
to the "big is beautiful" idea that 
high expressivity is needed for describing domain ontologies. As a result, when they are applied, 
the current Semantic Web technologies 
are mostly used for building thematic portals but do not scale up to the Web.
In contrast,  \somewhere \ promotes a "small is beautiful" vision of 
the Semantic Web \cite{rousset-iwsc} based on 
simple personalized ontologies (e.g., taxonomies of atomic classes) but which are 
distributed at a large scale.
In this vision of the Semantic Web introduced by \citeA{PLU-WWW-03}, 
no user imposes to others his own ontology but logical mappings between
ontologies make possible the creation of a web of people in which personalized
semantic marking up of data cohabits nicely with a collaborative exchange of
data. In this view, the Web is a huge peer-to-peer data management system   
based on simple distributed ontologies and mappings. 

Peer-to-peer data management systems have been proposed 
recently~\cite{halevy-pdms,Ooi-Shu-Tan,hyperion,bernstein-pdms,calvanese-et-al-2004} to generalize 
the centralized approach of information integration systems based
on single mediators.
In a peer-to-peer data management system, there is no central mediator: each peer has its own ontology 
and data or services,
and can mediate with some other peers to ask and answer queries. 
The existing systems vary according to (a) the expressive power of their 
underlying data model and (b) the way the different peers are semantically
connected. Both characteristics have impact on the allowed queries and their 
distributed processing.

In \textsc{Edutella}~\cite{edutella}, each peer stores locally data (educational 
resources) that are described in RDF relative to some reference ontologies
(e.g., \textsc{Dmoz} - http://dmoz.org). For instance, a peer can declare that it has 
data related to the concept of the dmoz taxonomy corresponding to  
the path {\em Computers/Programming/Languages/Java}, and that for such data it can export the {\em author} 
and the {\em date} properties. The overlay network underlying \textsc{Edutella} is a 
hypercube of super-peers to which peers are directly connected. Each super-peer
is a mediator over the data of the peers connected to it. When it is queried,
its first task is to check if the query matches with its schema: 
if that is the  case, it transmits the query to the peers connected to it,
which are likely to store the data answering the query ; otherwise, 
it routes the query to some of its
neighbour super-peers according to a strategy exploiting the hypercube 
topology for guaranteeing a worst-case logarithmic time for reaching the
relevant super-peer.

In contrast with Edutella, \textsc{Piazza}~\cite{halevy-pdms,piazza} does not 
consider that 
the data distributed over the different peers must be described relatively
to some existing reference schemas. In \textsc{Piazza}, each peer
has its own data and schema and can mediate with some other peers by declaring
{\em mappings} between its schema and the schemas of those peers.
The topology of the network is not fixed (as the hypercube in 
\textsc{Edutella}) but accounts for the existence of mappings between peers: two 
peers are logically connected if there exists a mapping between their two 
schemas.
The underlying data model of the first version of  \textsc{Piazza}~\cite{halevy-pdms} 
is relational and the mappings between relational peer schemas are inclusion 
or equivalence statements between conjunctive queries. Such a mapping 
formalism encompasses the {\em local-as-views} and the {\em global-as-views} \cite{alon-gav-lav}
formalisms used in information integration systems based on single
mediators.
The price to pay is that
query answering is undecidable except if some restrictions are imposed
on the mappings or on the topology of the network \cite{halevy-pdms}. 
The currently implemented version of \textsc{Piazza}~\cite{piazza} relies on a 
tree-based
data model: the data is in XML and the mappings are equivalence and inclusion
statements between XML queries. Query answering is implemented based on 
practical (but not complete) algorithms for XML query containment and rewriting.
The scalability of \textsc{Piazza} so far does not go up to more than about 80 peers in the published
experiments and relies on a wide range
of optimizations (mappings composition, \citeR{halevy-vldb03}, paths pruning, \citeR{halevy-sigmod04}), 
made possible by the centralized storage of all the schemas and mappings 
in a global server.

In \somewhere, we have made the choice of being fully distributed:  
there are neither super-peers (as in \textsc{Edutella}) nor a central server 
having the global view of the overlay network (as in \textsc{Piazza}). 
In addition, we aim at scaling up to thousands of peers. 
To make it possible, we have chosen a simple class-based data model in which
the data is a set of resource identifiers (e.g., URIs), the schemas
are (simple) definitions of classes possibly constrained by 
inclusion, disjunction or equivalence statements, and mappings are
inclusion, disjunction or equivalence statements between classes of different 
peer schemas.
That data model is in accordance with the W3C recommendations since it is
captured by the propositional fragment of the OWL ontology language 
(http://www.w3.org/TR/owl-semantics). 
Note that OWL makes possible, through a declarative import mechanism, 
to retrieve ontologies that are physically distributed. 
Using this transitive mechanism in peer data management systems amounts 
in the worst case to centralized on a single peer the whole 
set of peer ontologies, and to reason locally. 
Our feeling is that on very large networks such a mechanism cannot scale up satisfactorily.
Moreover, because of the dynamicity of peer-to-peer settings, such imports would have to
be re-actualized each time that a peer joins or quit the network. 


Section~\ref{prelsomewhere} defines the 
\somewhere \ data model, for which an illustrative example is given in Section \ref{example}.  
In Section~\ref{rewriting}, we show how query rewriting in \somewhere, and 
thus query answering, can be reduced by a propositional encoding to 
distributed reasoning in propositional logic.


\subsection{\somewhere\ Data model}
\label{prelsomewhere}
In \somewhere,
a new peer joins the network through some peers that it 
knows (its acquaintances) 
by declaring mappings between its own ontology
and the ontologies of its acquaintances. Queries are posed to a given
peer using its local ontology. The answers that are expected are not only
instances of local classes but possibly instances of classes of peers distant from the
queried peer if it can be infered from the
peer ontologies and the mappings that they satisfy the query. 
Local ontologies, storage descriptions and mappings are defined using a 
fragment of OWL DL which is the description logic fragment of the
Ontology Web Language recommended by W3C. We call OWL PL the fragment
of OWL DL that we consider in \somewhere, where PL stands for 
propositional logic. 
OWL PL is the fragment of OWL DL reduced to the disjunction, 
conjunction and negation constructors for building 
class descriptions. 

\subsubsection{Peer ontologies}
Each peer ontology is made of a set of class definitions and possibly a set of
equivalence, inclusion or disjointness
axioms between class descriptions. A class description is either the universal class 
($\top$), the empty class ($\bot$), an 
atomic class or the union ($\sqcup$), 
intersection ($\sqcap$) or complement ($\neg$) of class descriptions.

The name of atomic classes is unique to each peer: we use the notation
$P$:$A$ for identifying an atomic  class  $A$ of the ontology of a peer $P$.
The {\em vocabulary} of a peer $P$ is the set of names of its atomic classes. \\

\noindent
\begin{small}
\begin{tabular}{@{}l}
{\bf Class descriptions} \\
\begin{tabular}{l|c|c}
 & {\em Logical notation} & {\em OWL notation} \\
\hline
universal class & $\top$ & $Thing$ \\
empty class & $\bot$ & $Nothing$ \\
atomic class & $P$:$A$ & $classID$ \\
conjunction & $D1 \sqcap D2$ & $intersectionOf (D1 \ D2)$ \\
disjunction & $D1 \sqcup D2$ & $unionOf (D1 \ D2)$ \\
negation & $\neg D$ & $complementOf (D)$ \\
\end{tabular} 
\end{tabular} 


\noindent
\begin{tabular}{@{}l}
{\bf Axioms of class definitions} \\

\begin{tabular}{l|c|c}
 & {\em Logical notation} & {\em OWL notation} \\
\hline
Complete & $P$:$A$ $ \equiv D$ & $Class(P$:$A$ $complete$ $D)$ \\
Partial  & $P$:$A$ $\sqsubseteq D$ & $Class(P$:$A$ $partial$ $D)$ \\
\end{tabular} 
\end{tabular}


\noindent
\begin{tabular}{@{}l}
{\bf Axioms on class descriptions} \\

\begin{tabular}{l|c|c}
 & {\em Logical notation} & {\em OWL notation} \\
\hline
equivalence & $D1 \equiv D2$ & $EquivalentClasses(D1 \ D2)$ \\
inclusion  & $D1 \sqsubseteq D2$ & $SubClassOf (D1 \ D2)$ \\
disjointness  & $D1 \sqcap D2 \equiv \bot$ & $DisjointClasses(D1 \ D2)$ \\
\end{tabular} 
\end{tabular}
\end{small}

Taxonomies of atomic classes (possibly enriched by disjointness statements
between atomic classes) are particular cases of the allowed ontologies in
\somewhere \ . Their specification is made of a set of inclusion
(and disjointness) axioms involving atomic classes only: there is no
class definition using (conjunction, disjunction or negation) constructors.

\subsubsection{Peer storage descriptions}
The specification of the data that is stored locally in a peer $P$ is done 
through the declaration of atomic {\em extensional classes} defined in terms of atomic classes of the peer ontology, and assertional statements relating
data identifiers (e.g., URIs) to those extensional classes. 
We restrict the axioms defining the extensional classes to be inclusion 
statements between an atomic extensional class and a description combining
atomic classes of the ontology. We impose that restriction in order to fit with 
a {\em Local-as-Views} approach and an open-world assumption within the information
 integration setting \cite{alon-gav-lav}.
We will use the notation $P$:$ViewA$ to denote an extensional class $ViewA$
of the peer $P$.

\vspace{0,5cm}
\noindent
\begin{small}
\begin{tabular}{@{}l}
\noindent
{\bf Storage description} \\
declaration  of extensional classes: \\
\begin{tabular}{c|c}
 {\em Logical notation} & {\em OWL notation} \\
\hline
 $P$:$ViewA$ $\sqsubseteq C$ & 
$SubClassOf(P$:$ViewA$ \ $C$) \\
\end{tabular} \\
assertional statements: \\
\begin{tabular}{c|c}
{\em Logical notation} & {\em OWL notation} \\
\hline
$P$:$ViewA(a)$ & $individual(a \ type(P$:$ViewA$)) \\
\end{tabular}
\end{tabular}
\end{small}

\subsubsection{Mappings}
Mappings are disjointness, equivalence or inclusion statements involving 
atomic classes of different peers. They express the semantic correspondence 
that 
may exist between the ontologies of different peers.

\subsubsection{Schema of a \somewhere\ network}
In a \somewhere \ network, the schema is not centralized  but distributed 
through the union of the different peer ontologies and the mappings.
The important point is that 
each peer has a partial knowledge of the schema: it just knows its own
local ontology and the mappings with its acquaintances. 

Let $\cal{P}$ be a \somewhere\ peer-to-peer network made of a collection
of peers $\{P_i\}_{i=1..n}$. For each peer $P_i$, let $O_i$, $V_i$ and
$M_i$ be  the sets of axioms defining respectively the local ontology of $P_i$,
the declaration of its extensional classes  and the set of  mappings
stated at $P_i$ between classes
of $O_i$ and classes of the ontologies of the acquaintances of $P_i$.
The schema of $\cal{P}$, denoted  $S(\cal{P})$,  is the union 
$\bigcup_{i=1..n}O_i \cup V_i \cup M_i$ of the
ontologies, the declaration of extensional classes and of the sets of mappings of all the peers.



\subsubsection{Semantics}

The semantics isis the standard semantics of first order logic 
defined in terms of {\em interpretations}. An interpretation $I$ is a 
pair  $(\Delta^I,.^I)$ where $\Delta$ is a non-empty set, 
called the domain of interpretation, and $.^I$ is an interpretation function 
which assigns a subset of $\Delta^I$ to every class identifier
and an element of $\Delta^I$ to every data identifier.



An interpretation $I$ is a {\em model} of the distributed schema 
of a \somewhere\ peer-to-peer network $\cal{P}$ = $\{P_i\}_{i=1..n}$
iff for each axiom
in $\bigcup_{i=1..n}O_i \cup V_i \cup M_i$ is satisfied by $I$. 
%
Interpretations of axioms rely on interpretations of class descriptions 
which are inductively defined as follows:

$\bullet$ $\top^I = \Delta^I$, $\bot^I = \emptyset$

$\bullet$ $(C_1 \sqcup C_2)^I = C_1^I \cup C_2^I$

$\bullet$ $(C_1 \sqcap C_2)^I = C_1^I \cap C_2^I$

$\bullet$ $(\neg C)^I = \Delta^I \backslash C^I$

Axioms are satisfied if the following holds:

$\bullet$ $C \sqsubseteq D$ is satisfied in $I$ iff  $C^I \subseteq D^I$

$\bullet$ $C \equiv D$ is satisfied in $I$ iff  $C^I = D^I$

$\bullet$ $C \sqcap D \equiv \bot$ is satisfied in $I$ iff  $C^I \cap D^I = \emptyset$


A \somewhere\ peer-to-peer network is {\em satisfiable} iff its 
(distributed) schema has a model.

Given a \somewhere\ peer-to-peer network $\cal{P}$ = $\{P_i\}_{i=1..n}$, 
a class description $C$  {\em subsumes} a class description $D$ 
iff for any model $I$ of $S(\cal{P})$  $D^I \subseteq C^I$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Example - OWL PL
%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Illustrative Example}
\label{example}

We illustrate the \somewhere\ data model on a small example of four peers modeling 
four persons Ann, Bob, Chris and Dora, each of them bookmarking URLs
about restaurants they know or like, according to their own taxonomy
for categorizing restaurants. 

\vspace{0.3cm}
{\bf Ann}, who is working as a restaurant critic, organizes its restaurant
URLs according to the following classes:


$\bullet$ the class $Ann$:$G$ of restaurants considered as offering a "good" cooking,
among which she distinguishes the subclass $Ann$:$R$ of those which are
 rated: $Ann$:$R \sqsubseteq Ann$:$G$

$\bullet$ the class $Ann$:$R$ is the union of three disjoint classes 
$Ann$:$S1$, $Ann$:$S2$, $Ann$:$S3$ 
corresponding respectively to the restaurants rated with $1, 2$ or $3$ 
stars: 

$Ann$:$R \equiv$ $Ann$:$S1 \sqcup Ann$:$S2 \sqcup Ann$:$S3$

$Ann$:$S1 \sqcap Ann$:$S2 \equiv \bot$ \,  $Ann$:$S1 \sqcap Ann$:$S3 \equiv \bot$ 

$Ann$:$S2 \sqcap Ann$:$S3 \equiv \bot$  

$\bullet$ the classes $Ann$:$I$ and $Ann$:$O$, respectively corresponding to Indian 
and Oriental restaurants

$\bullet$ the classes $Ann$:$C$, $Ann$:$T$ and $Ann$:$V$ which are subclasses of $Ann$:$O$ denoting 
Chinese, Ta\"{\i} and Vietnamese restaurants respectively: $Ann$:$C \sqsubseteq$ $Ann$:$O$, $Ann$:$T \sqsubseteq$ $Ann$:$O$, $Ann$:$V \sqsubseteq$ $Ann$:$O$ 

\noindent 
Suppose that the data stored by Ann that she accepts to make available
deals with restaurants of various specialties, and only with those rated with $2$ stars among the rated
restaurants. The extensional classes declared by Ann 
are then: \\
$Ann$:$ViewS2 \sqsubseteq Ann$:$S2$, $Ann$:$ViewC \sqsubseteq Ann$:$C$, $Ann$:$ViewV \sqsubseteq Ann$:$V$, \\
$Ann$:$ViewT \sqsubseteq Ann$:$T$, $Ann$:$ViewI \sqsubseteq Ann$:$I$ \\

%%%%%%
\vspace{0.3cm}
{\bf Bob}, who is fond of Asian cooking and likes high quality, organizes his 
restaurant
URLs according to the following classes:

$\bullet$ the class $Bob$:$A$ of Asian restaurants

$\bullet$ \hspace{-0.1cm} the class $Bob$:$Q$ of high quality restaurants that he knows

\noindent Suppose that he wants to make available every data that he has stored. The
extensional classes that he declares are $Bob$:$ViewA$ and $Bob$:$ViewQ$ 
(as subclasses of $Bob$:$A$ and $Bob$:$Q$):
$Bob$:$ViewA \sqsubseteq$ $Bob$:$A$, $Bob$:$ViewQ \sqsubseteq$ $Bob$:$Q$ 

%%%%%%
\vspace{0.3cm}
{\bf Chris} is more fond of fish restaurants but recently discovered some places serving 
a very nice cantonese cuisine.  He organizes its data with respect to the following classes:

$\bullet$ the class $Chris$:$F$ of fish restaurants,

$\bullet$ the class $Chris$:$CA$ of Cantonese restaurants

\noindent Suppose that he declares the extensional classes $Chris$:$ViewF$ and 
$Chris$:$ViewCA$ as subclasses of $Chris$:$F$ and $Chris$:$CA$ respectively:\\
$Chris$:$ViewF \sqsubseteq$ $Chris$:$F$, $Chris$:$ViewCA \sqsubseteq$ $Chris$:$CA$ 


%%%%%%
\vspace{0.3cm}
{\bf Dora} organizes her restaurants URLs around 
the class $Dora$:$DP$ of her preferred restaurants, among which she
distinguishes the subclass $Dora$:$P$ of pizzerias and the subclass $Dora$:$SF$
of seafood restaurants.

\noindent
Suppose that the only URLs that she stores concerns pizzerias: the only 
extensional class that she has to declare is $Dora$:$ViewP$ as
a subclass of $Dora$:$P$: $Dora$:$ViewP$$\sqsubseteq$$Dora$:$P$ 

%%%%%%
\vspace{0.3cm}
{\bf Ann}, {\bf Bob}, {\bf Chris} and {\bf Dora} express what they know about each other using mappings stating properties
of class inclusion or equivalence.

{\bf Ann} is very confident in Bob's taste and agrees to include 
Bob' selection as good restaurants by stating  $Bob$:$Q$ $\sqsubseteq$ $Ann$:$G$.
%
Finally, she thinks that Bob's Asian restaurants encompass 
her Oriental restaurant concept: $Ann$:$O$ $\sqsubseteq$ $Bob$:$A$

{\bf Bob} knows that what he calls Asian cooking corresponds exactly
 to what Ann classifies as Oriental cooking. This may be expressed using
 the equivalence statement : $Bob$:$A$ $\equiv$ $Ann$:$O$ (note the difference
 of perception of Bob and Ann regarding the mappings between 
 $Bob$:$A$ and $Ann$:$O$)

{\bf Chris} considers that what he calls fish specialties is  
a particular case of Dora seafood specialties:
 $Chris$:$F$ $\sqsubseteq$ $Dora$:$SF$

{\bf Dora} counts on both Ann and Bob to obtain good Asian restaurants :
$Bob$:$A$ $\sqcap$ $Ann$:$G$  $\sqsubseteq$ $Dora$:$DP$ \\


Figure \ref{fig:acqgraph-with-ontologies} describes the resulting
overlay network.
In order to
alleviate the notations, we omit the local peer name prefix except for the 
mappings.
Edges are labeled with the class identifiers that are shared through the mappings 
between peers. 


\begin{figure}[!h]
\begin{center}

\scalebox{0.8}{
\begin{pspicture}(-2,-2.5)(8,9)
\rput(-1.5,7){\rnode{Dora}{\psframebox[framearc=0.4]{
                                                \begin{tabular}{ll}
                                                        \multicolumn{2}{l}{\textbf{Dora}} \\
                                                       \multicolumn{2}{l}{\textsl{ontology :}} \\
                                                            & $DP\sqsubseteq \top$,\\ 
                                                            & $P\sqsubseteq DP$, $SF\sqsubseteq  DP, $\\
                                                            & $ViewP \sqsubseteq P$\\
                                                         \multicolumn{2}{l}{\textsl{mappings :}} \\
                                                            & $Bob$:$A$ $\sqcap$ $Ann$:$G$ $\sqsubseteq$ $Dora$:$DP$\\
                                                \end{tabular}
                                          }}}
\rput(3.5,2.5){\rnode{Bob}{\psframebox[framearc=0.4]{
                                                \begin{tabular}{ll}
                                                        \multicolumn{2}{l}{\textbf{Bob}} \\
                                                       \multicolumn{2}{l}{\textsl{ontology :}} \\
                                                             & $A\sqsubseteq \top$, $Q\sqsubseteq \top$,\\ 
                                                             & $ViewA \sqsubseteq A$,\\ 
                                                             & $ViewQ \sqsubseteq Q$\\
                                                        \multicolumn{2}{l}{\textsl{mappings :}} \\
                                                            & $Bob$:$A \equiv Ann$:$O$\\
                                                 \end{tabular}
                                        }}}
\rput(-1.5,-0.5){\rnode{Chris}{\psframebox[framearc=0.4]{
                                                \begin{tabular}{ll}
                                                        \multicolumn{2}{l}{\textbf{Chris}} \\
                                                        \multicolumn{2}{l}{\textsl{ontology :}} \\
                                                             & $F\sqsubseteq \top$, $CA\sqsubseteq \top$,\\ 
                                                             & $ViewF \sqsubseteq F$,$ViewCA \sqsubseteq CA$\\
                                                       \multicolumn{2}{l}{\textsl{mappings :}} \\
                                                             & $Chris$:$F \sqsubseteq  Dora$:$SF$ \\
                                                \end{tabular}
                                           }}}
\rput(10,3){\rnode{Ann}{\psframebox[framearc=0.4]{
                                                \begin{tabular}{ll}
                                                       \multicolumn{2}{l}{\textbf{Ann}} \\
                                                       \multicolumn{2}{l}{\textsl{ontology :}} \\
                                                             & $G \sqsubseteq \top$,  $O \sqsubseteq \top$,  $I \sqsubseteq \top$,  \\
                                                             & $R\sqsubseteq G$,\\ 
                                                             & $(S1 \sqcup S2 \sqcup S3) \equiv R$, \\
                                                             & $ S1 \sqcap S2 \equiv \bot$, \\ 
                                                             & $S1 \sqcap S3 \equiv \bot$,\\ 
                                                             & $S2 \sqcap S3 \equiv \bot$,\\
                                                             & $(C \sqcup V \sqcup T) \sqsubseteq O$, \\
                                                             & $ViewC \sqsubseteq C$, \\ 
                                                             & $ViewV \sqsubseteq V$, \\ 
                                                             & $ViewT \sqsubseteq T$,\\
                                                             & $ViewI \sqsubseteq I$, \\ 
                                                             & $ViewS2 \sqsubseteq S2$\\
                                                      \multicolumn{2}{l}{\textsl{mappings :}} \\
                                                             & $Ann$:$O$ $\sqsubseteq$ $Bob$:$A$,\\ 
                                                             & $Bob$:$Q$ $\sqsubseteq$ $Ann$:$G$\\ 
                                              \end{tabular}
                                        }}}
\ncline{Dora}{Chris}\tlput{$Dora$:$SF$}
\ncline{Dora}{Bob}\tlput{$Bob$:$A$}
\ncline{Dora}{Ann}\taput{$Ann$:$G$}
\ncline{Bob}{Ann}\tbput{ \rput(-0.3,-0.8){
                                             \begin{tabular}{c}
                                               $Bob$:$Q,$\\
                                               $Bob$:$A,$\\
                                               $Ann$:$O$
                                             \end{tabular}
                                         }}

\end{pspicture}
}
\vspace{-.1cm}
\caption{The restaurants network}
\label{fig:acqgraph-with-ontologies}
\end{center}
\vspace{-.8cm}
\end{figure}


\subsection{Query Rewriting in  \somewhere\ through Propositional Encoding}
\label{rewriting}
In \somewhere, each user interrogates the peer-to-peer network through 
one peer of his choice, and uses the vocabulary of this peer  to express his query.
Therefore, queries are logical combinations of classes of a given peer ontology. 

The corresponding answer sets are expressed in intention in terms of the 
combinations of extensional classes that are {\em rewritings} of the query.
The point is that extensional classes of several distant peers can participate to the rewritings, 
and thus to the answer of a query posed to a given peer.

\begin{definition}{Rewritings}
Given a \somewhere\ peer-to-peer network $\cal{P}$ = $\{P_i\}_{i=1..n}$, a  logical combination $Q_e$ of 
extensional classes is a {\em rewriting} of a query $Q$ iff $Q$ subsumes $Q_e$ w.r.t. $\cal{P}$.  \\
$Q_e$ is a {\em proper rewriting} if there exists some model of $I$ of $S(\cal{P})$ 
such that $Q_e^{I} \neq \emptyset$.
$Q_e$ is a {\em conjunctive rewriting} if it is a rewriting which is  a conjunction of extensional classes.\\
$Q_e$ is a {\em maximal (conjunctive) rewriting} if there does not exist another 
(conjunctive) rewriting $Q'_e$ of $Q$ (strictly) subsuming $Q_e$  w.r.t. $\cal{P}$.
\end{definition}

In general, finding all answers in a peer data management system is a critical issue 
\cite{halevy-pdms}. In our setting however, we are in a case where all the answers 
can be obtained using {\em rewritings} of the query: it has been shown 
\cite{GoasdoueRousset-TOIT-2004} that when a query has a {\em finite number 
of maximal conjunctive rewritings}, then {\em all} its answers (a.k.a. certain answers) 
can be obtained as the union of the answer sets of its rewritings.
From the query answering point of view, it is the notion of {\em proper} rewriting which is relevant
because it guarantees a non empty set of answers. If a query  has no proper rewriting, it won't get any answer.

In the \somewhere\ setting, query rewriting  
can be equivalently reduced to distributed reasoning over logical 
propositional theories by a straighforward propositional encoding of 
the query and of the distributed schema of a \somewhere\ network.
It consists in transforming each query and schema statement into a propositional 
formula using class identifiers as propositional variables.

The propositional encoding of a class description $D$, and thus of a query, 
is the propositional formula $Prop(D)$
obtained inductively as follows:

$\bullet$ $Prop(\top) = true$, $Prop(\bot) = false$

$\bullet$ $Prop(A) = A$, if $A$ is an atomic class

$\bullet$ $Prop(D_1 \sqcap D_2)=Prop(D_1) \wedge Prop(D_2)$

$\bullet$ $Prop(D_1 \sqcup D_2)=Prop(D_1) \vee Prop(D_2)$

$\bullet$ $Prop(\neg D) = \neg(Prop(D))$ 

The propositional encoding of the schema $\mathcal{S}$ of a \somewhere \ 
peer-to-peer network $\mathcal{P}$ is the
distributed propositional theory $Prop(\mathcal{S})$ made of the formulas 
obtained inductively from the axioms in $\mathcal{S}$ as follows:

$\bullet$ $Prop(C \sqsubseteq D)$ = $Prop(C) \Rightarrow Prop(D)$

$\bullet$ $Prop(C \equiv D)$ = $Prop(C) \Leftrightarrow Prop(D)$

$\bullet$ $Prop(C \sqcap D \equiv  \bot) = \neg Prop(C) \vee \neg Prop(D)$


From now on, for simplicity, we use the propositional clausal form 
notation for  the queries and \somewhere \ peer-to-peer network schemas. 
As an illustration, let us consider the propositional encoding of the example presented in Section
\ref{example}. After application of the transformation rules, conversion of each 
produced formula in clausal form and suppression of tautologies, we obtain 
(Figure \ref{fig:proppdms}) �a new acquaintance graph where each peer schema 
is described as a propositional theory. 

%%%%%%
% Quelques macros pr�alables pour y voir plus clair dans le dessin
%%%%%%

%%%% La theorie de Ann
 \newcommand{\annth}{
 {\scriptsize
 \psframebox{$
  \begin{array}{ll}
 \mathbf{Ann:}\\
 \neg Ann$:$S1 \vee \neg Ann$:$S2    & \neg Ann$:$S1 \vee \neg Ann$:$S3   \\
 \neg Ann$:$S2 \vee  \neg Ann$:$S3   & \neg Ann$:$S1  \vee Ann$:$R           \\
 \neg Ann$:$S2  \vee Ann$:$R            & \neg Ann$:$S3  \vee Ann$:$R            \\
\multicolumn{2}{l}{\neg Ann$:$R  \vee Ann$:$S1 \vee Ann$:$S2 \vee Ann$:$S3} \\
\neg Ann$:$ViewS2  \vee S2 \\
\neg Ann$:$R  \vee Ann$:$G            &   \neg Bob$:$Q  \vee Ann$:$G \\
\neg Ann$:$O  \vee Bob$:$A            &   \neg Ann$:$C  \vee Ann$:$O \\
 \neg Ann$:$V  \vee Ann$:$O           &   \neg Ann$:$T  \vee Ann$:$O \\
 \neg Ann$:$ViewC  \vee Ann$:$C    &  \neg Ann$:$ViewV \vee Ann$:$V \\
 \neg Ann$:$ViewT \vee Ann$:$T     &  \neg Ann$:$ViewI  \vee Ann$:$I \\
\neg Chris$:$CA  \vee Ann$:$C 
\end{array}
 $}}}

%%%% La theorie de Bob
  \newcommand{\bobth}{
 {\scriptsize
  \psframebox{$
\begin{array}{l}
 \mathbf{Bob:}\\
 \neg Bob$:$ViewA  \vee Bob$:$A \\
 \neg Bob$:$ViewQ  \vee Bob$:$Q \\
 \neg Bob$:$A  \vee Ann$:$O\\
 \neg Ann$:$O \vee Bob$:$A \\
\end{array}
$}}}

%%%% La theorie de Chris
\newcommand{\christh}{
 {\scriptsize
 \psframebox{$
 \begin{array}{l}
 \mathbf{Chris:} \\
 \neg Chris$:$ViewF  \vee Chris$:$F\\
 \neg Chris$:$ViewCA \vee Chris$:$CA\\
 \neg Chris$:$F  \vee Dora$:$SF\\
 \end{array}
$}}}

%%%% La theorie de Dora
\newcommand{\dorath}{
 {\scriptsize
 \psframebox{$
 \begin{array}{l}
 \mathbf{Dora:} : \\
 \neg Dora$:$ViewP  \vee Dora$:$P\\
 \neg Dora$:$P  \vee Dora$:$DP\\
 \neg Dora$:$SF \vee Dora$:$DP\\
 \neg Bob$:$A  \vee  \neg Ann$:$G  \vee Dora$:$DP\\
 \end{array}
$}}}
%%%%%% Fin  macros  %%%%%%

%%%%%%% %%%% % Le dessin %%%% %%%% %%%% 
\begin{figure}[h]
\begin{center}
\scalebox{0.9}{
\begin{pspicture}(0,0)(9,8)
% Nodes
\rput(-1.8,7){\rnode{Dora}{\dorath}}
\rput(1,4){\rnode{Bob}{\bobth}}
\rput[b](-1.8,0){\rnode{Chris}{\christh}}
\rput(9.2,5.8){\rnode{Ann}{\annth}}
% Arcs
\ncline{Dora}{Chris} \tlput{$Dora$:$SF$}
\ncline{Dora}{Bob} \trput{$Bob$:$A$}
\ncline{Dora}{Ann} \taput{$Ann$:$G$~~~~~~~~~~~~~~~~~~~~~~~~~~}
\ncline{Bob}{Ann} \tbput{\begin{tabular}{ll}
                                                 $Bob$:$Q$, &\\
                                                 $Bob$:$A$, &\\
                                                 $Ann$:$O$ &
                                           \end{tabular}
                                            }
\ncarc[arcangleA=-20,arcangleB=-70]{Chris}{Ann}\taput{$Chris$:$CA$}
\end{pspicture}
} % scalebox

\caption{The propositional encoding for the restaurant network}
\label{fig:proppdms}
\end{center}
\end{figure}
%%%%%%%%% %%%% %%%% %%%% 

We now state two propositions showing that query rewriting in
\somewhere \ can be reduced to consequence finding in a P2PIS as presented
in the previous sections. 

Proposition \ref{implicates} states that the propositional encoding 
transfers satisfiability and establishes the connection  between proper 
(maximal) conjunctive rewritings and proper (prime) implicates. 

Proposition \ref{property} states that the P2PIS  resulting from the 
propositional encoding of a \somewhere \ schema fulfills by construction 
the property exhibited in Theorem \ref{completeness} as a sufficient condition 
for the completeness of the algorithms described in Section \ref{algo} that 
compute proper prime implicates of a clause w.r.t  distributed propositional theories.


\begin{proposition}
\label{implicates}
Let $\mathcal{P}$ be a \somewhere \ peer-to-peer network and let $Prop(S(\mathcal{P}))$ be the propositional 
encoding of its schema. Let $V_e$ be the set of all the extensional classes.

$\bullet$ $S(\mathcal{P})$ is satisfiable iff $Prop(S(\mathcal{P}))$ is satisfiable. 

$\bullet$ $q_e$ is a proper maximal conjunctive rewriting of a query $q$ iff 
$\neg Prop(q_e)$ is a {\em proper prime implicate of $\neg Prop(q)$ w.r.t. $Prop(S(\mathcal{P}))$} such that all 
its variables are extensional classes.
\end{proposition}


\begin{proof}
We first exhibit some properties that will be used in the proof of the proposition.
Let $\mathcal{P}$ be a \somewhere \ network, $S(\mathcal{P})$ its schema
and $Prop(S(\mathcal{P}))$ its propositional encoding.
For an interpretation $I$ of $S(\mathcal{P})$, and an element $o$ of its domain of interpretation $\Delta^I$, 
we define the interpretation 
$p_o(I)$ of $Prop(S(\mathcal{P}))$ as follows: for every propositional variable 
$v$  of $Prop(S(\mathcal{P}))$ ($v$ is the name of an atomic class of 
$S(\mathcal{P})$), $v^{p_o(I)} = true$ iff $o \in v^I$.
For an interpretation $J$ of $Prop(S(\mathcal{P}))$, we define the 
interpretation $i(J)$ of $S(\mathcal{P})$ as follows: the domain of $i(J)$
is  $\{true\}$, and for every atomic class $A$ of 
$S(\mathcal{P})$ ($A$ is the name of a propositional variable of 
$Prop(S(\mathcal{P}))$), if $A^J = true$ then $A^{i(J)} = \{true\}$ else
$A^{i(J)} = \emptyset$.
It is easy to show the following properties, for every 
interpretation $I$ of $S(\mathcal{P})$ (and every $o \in \Delta^I$), for every interpretation $J$ of
$Prop(S(\mathcal{P}))$:

\begin{enumerate}
\item for every class description $C$ of $S(\mathcal{P})$:

$a$) $o \in C^I  \Leftrightarrow Prop(C)^{p_o(I)} = true$

$b$) $true \in C^{i(J)} \Leftrightarrow Prop(C)^{J} = true$


\item $I$ is a model of $S(\mathcal{P})$ $\Leftrightarrow p_o(I)$ is a model
of $Prop(S(\mathcal{P}))$

\item $i(J)$ is a model of $S(\mathcal{P})$ $\Leftrightarrow J$ is a model
of $Prop(S(\mathcal{P}))$.

\end{enumerate}

\begin{itemize}
\item Suppose that $S(\mathcal{P})$ is satisfiable and let $I$ be a model of 
it and let $o$ be an element of $\Delta^I$: according to the above Property 2, $p_o(I)$ is
a model of $Prop(S(\mathcal{P}))$, and thus $Prop(S(\mathcal{P}))$ is 
satisfiable. In the converse way, let $J$ be a propositional model of 
$Prop(S(\mathcal{P}))$.  
According to the above Property 3, $i(J)$ is a model of
$S(\mathcal{P})$, and thus $S(\mathcal{P})$ is satisfiable.

%% Dans le sens <== 
\item 
Suppose that $Prop(\neg q_e)$ is a proper prime implicate of 
$Prop(\neg q)$ w.r.t. $Prop(S(\mathcal{P}))$, 
such that all its variables are extensional classes, 
and let us show that $q_e$ is a proper maximal conjunctive rewriting of $q$.

Let us first show that $q_e$ is a {\em rewriting} of $q$. 
Suppose that it is not the case:
there exists an interpretation $I$ of $S(\mathcal{P})$ such that 
$q_e^I \not\subseteq  q^I$ and thus an element of $o \in \Delta^I$ such
that $o \in q_e^I$ and $o \not\in q^I$. 
According to Property 2, $p_o(I)$ is a model of $Prop(S(\mathcal{P}))$, 
and according to Property 1.a, $(Prop(q_e))^{p_o(I)} = true$ and 
$(Prop(q))^{p_o(I)} \neq true$, i.e., 
$(Prop(\neg q_e))^{p_o(I)} = false$ and 
$(Prop(\neg q))^{p_o(I)} = true$. 
This is impossible since it would contradict the fact that 
$Prop(\neg q_e)$ is a proper prime implicate of 
$\{Prop(\neg q)\} \cup Prop(S(\mathcal{P}))$. 
Therefore, $q_e$ must be a rewriting of $q$.

Let us show now that $q_e$ is a {\em conjunctive} rewriting of $q$, i.e.,
$q_e$ is a conjunction of extensional classes. 
In $S(\mathcal{P})$, extensional classes only appear in inclusion axioms.
Therefore, the propositional encoding of $S(\mathcal{P})$ 
ensures that extensional classes only appear as variables in $Prop(S(\mathcal{P}))$ 
in negative literals. 
Resolution being sound and complete for prime implicate computation, 
$Prop(\neg q_e)$ is obtained as the result of a finite chain of resolutions, starting from
the clauses of $Prop(S(\mathcal{P}))$ and from $Prop(\neg q)$. Since in  $Prop(S(\mathcal{P}))$
extensional classes only appear in negative literals, they only appear in negative literals in the
computed implicates, and in particular in $Prop(\neg q_e)$. Therefore, $q_e$ is a conjunction of extensional  classes.

Let us show now that $q_e$ is a {\em proper} rewriting of $q$, i.e., 
that it is satisfiable in some model of $S(\mathcal{P})$. 
Since $Prop(\neg q_e)$ is a {\em proper} prime implicate of $Prop(\neg q)$ w.r.t. $Prop(S(\mathcal{P}))$, 
there exists a model $J$ of $Prop(S(\mathcal{P}))$ s.t. $Prop(\neg q_e)^J = false$
and thus  $Prop(q_e)^J = true$.  By Property 3, $i(J)$ is a model of $S(\mathcal{P})$
and according to the above Property 1.b, $true \in (q_e)^{i (J)}$. 
Therefore there exists a model of $S(P)$ in which $q_e$ is satisfiable, and thus 
$q_e$ is a proper rewriting of $q$.

Finally, let us show that $q_e$ is a {\em maximal} conjunctive rewriting of $q$. 
Suppose that this is not the case. Then, there exists a conjunctive rewriting $q'_{e}$ of $q$
such that $q_e \models q'_{e}$ and $q_e \not \equiv q'_e$. This means that
there exists an interpretation $I$ and an element $o \in \Delta^I$ such that 
$o \in {q'}_e^I$, thus $o \in q^I$, and $o \not\in q_e^I$. 
According to Property 1.a, $Prop(q'_e)^{p_o(I)}  = true$, 
$Prop(q)^{p_o(I)} = true$, and $Prop(q_e)^{p_o(I)} = false$, 
i.e., $Prop(\neg q'_e)^{p_o(I)} = false$, 
$Prop(\neg q)^{p_o(I)} = false$, and $Prop(\neg q_e)^{p_o(I)} = true$.
This is impossible since it contradicts that $Prop(\neg q_e)$ is 
a prime implicate of $Prop(\neg q)$ w.r.t. $Prop(S(\mathcal{P}))$. 
Therefore, $q_e$ is a maximal conjunctive rewriting of $q$.


%% == >
\item Let us now prove the converse direction. Suppose that $q_e$ is a proper maximal 
conjunctive rewriting of a query $q$ and let us show hat $Prop(\neg q_e)$ is a proper prime
implicate of  $Prop(\neg q)$ w.r.t. $Prop(S(\mathcal{P}))$.
By definition of a proper rewriting, for every  model $I$ of $S(\mathcal{P})$ 
$q_e^I \subseteq q^I$, or equivalently $(\neg q)^I \subseteq (\neg q_e)^I$ and
 there exists a model $I'$ of $S(\mathcal{P})$ such that $q_e^{I'} \neq \emptyset$.

Let us first  show that $Prop(\neg q_e)$ is an {\em implicate} of 
$Prop(\neg q)$ w.r.t $Prop(S(\mathcal{P}))$. 
Suppose that this is not the case, i.e., that 
$\{Prop(\neg q)\} \cup  Prop(S(\mathcal{P})) \not \models Prop(\neg q_e)$. 
Then, there exists a model $J$ of $\{Prop(\neg q)\} \cup Prop(S(\mathcal{P}))$ 
such that $Prop(\neg q_e)^J=false$. 
According to the above Property 3, $i(J)$ is a model of $S(\mathcal{P})$. 
According to the above Property 1.b,  $true \in (\neg q)^{i (J)}$ and $(\neg q_e)^{i (J)}=\emptyset$. 
This is impossible since it contradicts that $(\neg q)^{i(J)} \subseteq (\neg q_e)^{i(J)}$. 
Therefore, $Prop(\neg q_e)$ is an implicate of $Prop(\neg q)$ w.r.t. $Prop(S(\mathcal{P}))$.

Let us now show that $Prop(\neg q_e)$ is a {\em proper} implicate of 
$Prop(\neg q)$ w.r.t. $Prop(S(\mathcal{P}))$, i.e., that $Prop(\neg q_e)$ is not 
an implicate of $Prop(S(\mathcal{P}))$ alone. 
By definition of a proper rewriting, there exists a model $I'$ of $S(\mathcal{P})$ 
such that  $q_e^{I'} \neq \emptyset$. 
Let $o$ be an element of $q_e^{I'}$. 
According to Property 2, $p_o(I')$ is a model of $Prop(S(\mathcal{P}))$, 
and according to Property 1.a, $(Prop(q_e))^{p_o(I')} = true$, i.e.,  $(Prop(\neg q_e))^{p_o(I')} = false$. 
Therefore, $Prop(\neg q_e)$ is not an implicate of $Prop(S(\mathcal{P}))$. 

Finally, let us show that $Prop(\neg q_e)$ is a {\em prime} implicate 
of $Prop(\neg q)$ w.r.t. $Prop(S(\mathcal{P}))$. 

Let us show that if $c$ is a clause such that 
$Prop(S(P)) \cup \{Prop(\neg q)\} \models c \mbox{ and } c \models Prop(\neg q_e)$, 
then $c \equiv Prop(\neg q_e)$.
Since $c \models Prop(\neg q_e)$ and $Prop(\neg q_e)$ is a disjunction of 
negation of extensional classes, $c$ is a disjunction of a subset of the literals 
of $Prop(\neg q_e)$. Let $q_e'$ be the conjunction  of the extensional classes 
of $c$, then $c=Prop(\neg q_e')$. We have proved previously that 
if $Prop(\neg q_e')$ is an implicate of $Prop(\neg q)$ w.r.t. $Prop(S(P))$ 
then $q_e'$ is a rewriting of $q$, and similarly that 
 if $Prop(\neg q_e)$ is an implicate of $Prop(\neg q_e')$ w.r.t. $Prop(S(P))$ 
 then $q_e'$ subsumes $q_e$.
Therefore, $q_e'$ is a rewriting of $q_e$ which subsumes $q_e$. 
Since $q_e$ is a maximal  conjunctive rewriting of q, $q_e' \equiv q_e$,
thus  $\neg q_e' \equiv \neg q_e$ and  $Prop(\neg q_e') \equiv Prop(\neg q_e)$,
i.e. $c \equiv Prop(\neg q_e)$.
\end{itemize}

\end{proof}



\begin{proposition}
\label{property}
Let $\mathcal{P}$ be a \somewhere \ peer-to-peer network and let 
$Prop(S(\mathcal{P}))$ be the propositional encoding of its schema.
Let $\Gamma=(Prop(S(\mathcal{P})),\mbox{\sc acq})$ be the corresponding
 P2PIS, where the set of labelled edges $\mbox{\sc acq}$ is such that:
(P'':A, P, P') $\in \mbox{\sc acq}$ iff P'':A is involved in a mapping
between P and P' (i.e, P'' = P or P'' = P').
For every $P$, $P'$ and 
$v \in  \mathcal{V}_P \cap\mathcal{V}_{P'}$ there exists a path 
between $P$ and $P'$ in $\Gamma$ such that all edges of it are labelled 
with $v$.
 \end{proposition}
\begin{proof}
Let $P$ and $P'$ be two peers having a variable $v$ in common. 
Since the vocabularies of the local ontologies of different peers are disjoint,
$v$ is necessarily a variable $P''$:$A$ involved in a mapping declared between 
$P$ and some its acquaintances $P_1$ (and thus $P''$ = $P$ or $P''$= $P_1$), 
or between $P'$ and some of its acquaintances $P'_1$ 
(in this case $P''$ = $P'$ or $P''$= $P'_1$).

\noindent
- If $v$ is of the form $P''$:$A$ such that $P'' = P$ (respectively $P'' = P'$), 
then $P$:$A$ is an atomic class of $P$ (respectively $P'$:$A$ is an atomic class of $P'$) 
which is involved in a mapping between $P$ and $P'$, and therefore, there is an edge 
(and thus a path) between
$P$ and $P'$ labelled with $v$ ($P$:$A$ or $P'$:$A$ respectively) in $\Gamma$.

\noindent
- If $v$ is of the form $P''$:$A$ such that $P''$ is  distinct from
$P$ and $P'$, then $P''$:$A$ is an atomic class of $P''$, which is involved
in a mapping between $P''$ and $P$ and in a mapping between $P''$ and 
$P'$. Therefore, there exists 
an edge between $P''$ and $P$ labelled with $v$ and an edge between 
$P''$ and $P'$ labelled with $v$, and thus a path between $P$ and $P'$ 
such that all edges of it are labelled with $v$.



\end{proof}

From those two propositions, it follows that the message-based distributed 
consequence finding algorithm of Section \ref{message} can be used to compute 
the maximal conjunctive rewritings of a query.
This algorithm computes the set of proper prime implicates of a literal 
w.r.t. a distributed propositional clausal theory. Therefore, if it is applied to
the distributed theory resulting from the propositional encoding of the schema
of a \somewhere \ network, with the extensional classes symbols 
as {\em target variables}, and triggered with a literal 
$\neg q$, it computes in fact the negation of the maximal conjunctive
rewritings of the {\em atomic} query $q$. 
This result also holds for any arbitrary query since, in our setting, the maximal 
rewritings of such a query can be obtained by combining the maximal rewritings 
of its atomic components.

A corollary of these two propositions is that, in our setting, 
query answering is $BH_2$-complete w.r.t. query complexity and 
polynomial w.r.t. data complexity. 


%Experiments
\section{Experimental Analysis} \label{exp}

This section is devoted to an experimental study of the performances
of the distributed consequence finding algorithm described in Section
\ref{algo}, when deployed on real peer-to-peer inference systems.
Particularly, the aim of our experiments is to study scalability
issues of the \somewhere \ infrastructure for the Semantic Web. 
Our experiments have been performed on networks of 1000 peers. 
Our goal is thus to study the practical
complexity of the reasoning on networks of this size and to answer
questions such as: how deep and how wide does the reasoning spread on
the network of peers?  Does the network cope with the traffic load?
How fast are the results obtained?  To what extent do the results
integrate information from distinct peers? etc.

So far, large real corpus of distributed clausal theories are
still missing.  Since deploying new real applications at this scale
requires a significant amount of time, we have chosen to perform these
experiments on artificially generated instances of peer-to-peer networks. These
instances are characterized by the size and the form of the local
theories corresponding to each peer of the network, as well as by the
size and the topology of the acquaintance graph.

Since our aim is to use the \somewhere \ infrastructure for Semantic
Web applications, we focus our benchmarking to instances with suitable
characteristics. In particular we generate local theories supposed to
encode realistic ontologies and mappings, that could be written by
people to categorize their own data.  Acquaintances between peers are
generated in such way that the topology of the resulting graph looks
realistic with respect to the acquaintances between people on the
Web. Therefore we focus our generation on acquaintance graphs having
the so-called {\em small world} property, which is admitted
\cite{smallworld2} as being a general property of social networks
(including the Web).

In the following, we first detail in Section \ref{bench} the
generation process of our benchmark instances, the involved parameters
and how they have been allowed to vary in our experiments.  In
Section \ref{single}, a first series of experiments studies the
hardness of local reasoning within a single peer by evaluating the
number and the size of computed proper prime implicates.  This allows
us to realize the intrinsic complexity of this task and thus, of the
reasoning on large scale networks of such theories.  It also helps us
to justify the choice of some parameter values for further
experiments.  Finally, Section \ref{network} reports the
experimental results that have been obtained concerning the
scalability of \somewhere \ on large networks of peers.


\subsection{Benchmark Generation}
\label{bench}
Generating satisfactory instances of peer-to-peer networks for our framework
means both generating realistic propositional theories for each peer,
as well as an appropriate structure for the acquaintance graph. The
latter is induced by the variables shared between peer theories. In the
setting of the Semantic Web, they correspond to names of atomic
classes involved in mappings between peer ontologies.

\subsubsection{Generation of the local theories}

We make the following assumptions on the ontologies and the mappings
that are likely to be deployed at large scale in the future Semantic
Web: the ontologies will be taxonomies of atomic classes (possibly
with disjointness statements between pairs of atomic classes) ; most
mappings between such ontologies are likely to state simple
inclusion or equivalence between two atomic classes of two different
peers, but we do not want to exclude some more complex mappings
involving logical combination of classes. 

As a consequence, the propositional encoding of a taxonomy results in
a set of clauses of length 2. Most mappings result as well in clauses
of length 2.  The most complex mappings might result in longer
clauses, but since any set of clauses may equivalently be rewritten as
a set of clauses of length 3, we can restrict to the case where these
are encoded with clauses of length 3.  Clauses encoding the mappings
(called {\em mapping clauses}) are thus only clauses of length 2 and
3, (2-clauses and 3-clauses for short). We denote by $\%3cnf$ the
ratio of 3-clauses to the total number of mapping clauses.  This ratio
reflects in some way the degree of complexity of the mappings.  In our
experiments we study variations of this parameter because of its
significant impact on the hardness of reasoning.

The local theories  are generated in two steps. We first generate a set of 
$m$ random 2-clauses on a number $n$ of propositional variables and
randomly select a number $t$ ($t \leq n$) of target variables
(corresponding to the names of extensional classes). Mapping clauses
are then generated, according to a given value $\%3cnf$ and added to
the theories. Since mapping clauses induce the structure of the
acquaintance graph, the way they are generated is discussed below.
Peer theories are thus composed of only 2-clauses and
3-clauses.  In the literature on propositional reasoning, such
theories correspond to so-called {\em $2+p$ formulas},
% REF ?
  where $p$ denotes the proportion of 3-clauses in the whole set of
clauses (note that $p$ and $\%3cnf$ are different ratios).

\subsubsection{Generation of the acquaintance graph}

In order to focus on realistic acquaintance graphs, we have chosen to
generate random graphs with ``small worlds'' properties, as proposed
and studied by \citeA{smallworld1}, as well as \citeA{smallworld2}. 
Such graphs have two
properties that are encountered in social networks: first, a short
path length between any pair of nodes, observed in all social relationship
(for instance, the widely accepted ``six-degrees of separation''
between humans) and, second, a high {\em clustering ratio}, a
measurement of the number of common neighbors shared by two neighbors
(for instance, it is likely that two friends share a common subset of
friends).

To generate such graphs, we first generate the pairs of peers that are
connected.  Following the work of \citeA{smallworld1}, we start from a so called
{\em k-regular ring structure} of $np$ nodes, i.e., a graph the nodes
of which may be arranged as a ring, and such that each node is
connected to its $k$ closest neighbors. Edges of this graph are then
randomly rewired, with a given probability $pr$, by replacing one (or
both) of the connected peers with another peer. It has been shown that
between regular graphs ($pr=0$) and uniform random graphs ($pr=1$),
the graphs generated with $pr=0.1$ have ''small world''
properties. All acquaintance graphs used in our experiments have been
generated in that way, with $pr=0.1$.  Moreover, since our aim is to
evaluate the scalability of our approach, we have chosen to focus on
networks of significant size. For all our instances, we have fixed the
number of peers $np$ to $1000$ and the number $k$ of edges per peer to
$10$.

Once the topology of the network has been generated, local theories of
each peer are generated. Portion of the theories encoding taxonomies
are first generated as previously described. Then, for each edge of
the generated graph mapping clauses are added. For simplicity, we have
chosen to add a fixed number $q$ of mapping clauses for each
edge. Mapping clauses are randomly generated by picking one variable
in each of the two peers theories and by negating them with
probability $0.5$. With a $\%3cnf$ probability, a third literal
(randomly chosen between the two peers) is added to the clause to
produce mapping clauses of length 3. As a consequence, the average
number of variables shared between two connected peers is
$(2+\%3cnf)*q$.
 
\subsection{Hardness of Local Reasoning within a Single Peer}
\label{single}

In our setting, the first part of the reasoning performed at each peer
consists in computing the {\em proper} prime implicates of the
received litteral w.r.t. the local theory of the peer. In order to
grasp the hardness of this local reasoning we have first conducted an
experimental study to evaluate the number and the form of such
implicates, and also, since our local theories are $2+p$ clausal
theories, to evaluate the impact of the ratio $p$ on these
values. These experiments have been performed using a modified version
of \textit{Zres} \cite{SimonDelVal2001}.

Prime implicates have been already studied for 3-CNF random formulas
\cite{SchragCrawford1996}. This corresponds to the case where
$p=100\%$.  We first take this as a reference for comparison with {\em
proper} prime implicates.  We consider 3-CNF theories of $m=30$
clauses over $n$ variables ($n$ ranging from 12 to 28). The left part
of Figure \ref{fig:pi-30c} presents the characteristics of prime
implicates for different values of $n$. Each curve describes how the
prime implicates distribute according to their length. The curves
correspond to average values over 1500 experiments.  For instance, for
$n=28$ variables, there are on average more than 680 prime implicates
of length 7.  The right part of Figure \ref{fig:pi-30c} describes the
size of the whole set of prime implicates by means of the cumulative
distribution function of its total number $L$ of literals. Each point
$(x,\,y)$ on a curve must be read as ``over the $N=1500$ runs, $y.N$
of them led to a $L$ value smaller than $x$''. This representation is
convenient for exhibiting exponential distributions. The point to
stress here is that for such small formulas, the median value of the
size of the whole set of prime implicates already reaches more than
ten thousand literals. On some rare runs (less than 5\%), the set of
prime implicates has more than one hundred thousand literals.  We can
also observe that augmenting the number of variables increases the
difficulty since it results in longer and longer prime implicates
being produced in the final result.  Note that a simple random 3CNF
formula of only 30 clauses may already generate thousands of prime
implicates. Since computing implicates for random formulas is
known to require lots of subsumption checks \cite{SimonDelVal2001},
the final set of prime implicates may be very hard to obtain in
practice.

\begin{figure}[!t]
\centerline{
\begin{tabular}{c c}
\epsfig{figure=pi-30c.eps,width=0.48\textwidth} & 
\epsfig{figure=cdf-pi-30c.eps,width=0.48\textwidth} \\
\end{tabular}
}
\vspace{-0.3cm}
\caption{Prime Implicates in a uniform random 3-CNF theory}
\vspace{-0.2cm}
\label{fig:pi-30c}
\end{figure}
\begin{figure}[!t]
\centerline{
\begin{tabular}{c c}
\epsfig{figure=ppi-30c.eps,width=0.48\textwidth} & 
\epsfig{figure=cdf-ppi-30c.eps,width=0.48\textwidth} \\
\end{tabular}
}
\vspace{-0.3cm}
\caption{Proper Prime Implicates in a uniform random 3-CNF theory}
\vspace{-0.5cm}
\label{fig:ppi-30c}
\end{figure}


While such results are not new \cite{SchragCrawford1996}, it is
interesting to compare them with those obtained in similar conditions
when computing {\em proper} prime implicates, described on Figure
\ref{fig:ppi-30c}.  We can observe that curve shapes are very similar
to those previously obtained but that the values are one order of
magnitude smaller. Note that for $n=28$, the median value of the size
of the whole set of proper prime implicates is already about one
thousand of literals.  And similarly, for large values of $n$, a majority
of proper prime implicates are long.
Intuitively, one may explain this phenomenon by the fact that proper
prime implicates are prime implicates of the initial theory augmented
with an additional literal. But this literal presumably induces
clauses reductions in the theory and as a consequence more
subsumptions.  The problem thus becomes a simplified --~but not very
much~-- version of the prime implicates problem.
%
From these experiments, a first conclusion is that, even for very small
3-CNF theories, the number of proper prime implicates may be quite
large, and some of them may be quite big.


Let us now focus our further experiments on local $2+p$ CNF theories,
with smaller values of $p$, supposed to better correspond to the
encoding of applications in which part of the knowledge is structured
as a tree or as a dag (which is encoded with 2-clauses).  Figure
\ref{fig:pi-2pcnf} describes the prime implicates for a $2+p$ CNF theory
with $m=30$ clauses and $n=28$ variables, for values of $p$ ranging
from 0\% to 100\% (the curve corresponding to the case $p=100\%$ is
the same as in Figure \ref{fig:pi-30c}). Similarly, Figure
\ref{fig:ppi-2pcnf} describes the characteristics of the proper prime
implicates for the different values of $p$.  As previously, we can
observe that the curves have similar shapes.  From the
cumulative distribution function (CDF) curves, it appears that the
hardness (measured as the total size of the prime/proper prime
implicates) of the $2+p$ CNF formula grows exponentially with the value
of $p$. Even for small values of $p$ the problem may be hard. And as
$p$ increases, larger and larger clauses quickly appear in the result.

\begin{figure}[!t]
\centerline{
\begin{tabular}{c c}
\epsfig{figure=2pCNF-PI.eps,width=0.48\textwidth} & 
\epsfig{figure=cdf-2pCNF-PI.eps,width=0.48\textwidth} \\
\end{tabular}
}
\vspace{-0.3cm}
\caption{Prime Implicates in a uniform random $2+p$-CNF theory ($m=30,\,n=28$)}
\vspace{-0.5cm}
\label{fig:pi-2pcnf}
\end{figure}
\begin{figure}[t]
\centerline{
\begin{tabular}{c c}
\epsfig{figure=2pCNF-PPI.eps,width=0.48\textwidth} & 
\epsfig{figure=cdf-2pCNF-PPI.eps,width=0.48\textwidth} \\
\end{tabular}
}
\vspace{-0.3cm}
\caption{Proper Prime Implicates in a uniform random $2+p$-CNF theory ($m=30,\,n=28$)}
\vspace{-0.5cm}
\label{fig:ppi-2pcnf}
\end{figure}

Figure \ref{fig:pi-2pcnf100c} studies the characteristics of
proper prime implicates for a fixed and small value of $p=10\%$, and
increasing sizes $m$ of the theory and of the number of variables $n$.
We have chosen a small value of $p$ to focus on the characteristics of
larger theories (up to $m=100$ clauses). It is worth noticing that
even for $m=100$ and $p=10\%$, the problem seems simpler than for $m=30$
and $p=100\%$ (note that on the right part of Figure
\ref{fig:pi-2pcnf} the $y$-axis has been rescaled to $[0.5-1]$). Such
kinds of peer theories seem to have a reasonable behavior from an
integration perspective: half of the queries are very short and only a
small part of the queries are still very hard (the exponential
distribution is still observed).

\begin{figure}[!t]
\centerline{
\begin{tabular}{c c}
\epsfig{figure=cdf-2pCNF100c-PI.eps,width=0.48\textwidth} & 
\epsfig{figure=cdf-2pCNF100c-PPI.eps,width=0.48\textwidth} \\
\end{tabular}
}
\vspace{-0.3cm}
\caption{Size of Prime and Proper Prime Implicates in a uniform random $2+p$-CNF theory for a fixed $p$}
\vspace{-0.5cm}
\label{fig:pi-2pcnf100c}
\end{figure}




\subsection{Scalability of Distributed Reasoning}
\label{network}
The previous section has clearly shown that the local computation
performed at each peer may be really hard, even for small and simple
theories. When focusing at the level of whole \somewhere \
networks, the splitting/recombining strategy followed by our
distributed consequence finding algorithm clearly adds another source
of combinatorial explosion.  In order to evaluate the scalability of
\somewhere \ networks, we have performed two kinds of experiments. The
first one aims at studying the behavior of \somewhere\ networks during
query processing. It consists in counting the number of messages
circulating in a network and the number of peers that are solicited
while processing a query. In particular, we have measured the
distribution of the depth of query processing as well as the potential
width of a query.  The {\em depth of processing} ({\em depth} for
short) of a query is the maximum length of the reasoning branches
developed by the distributed algorithm for returning an answer to this
query. The {\em width} of the query measures the average number of
neighbors that are solicited by a peer during the reasoning.  The
second kind of experiments aims at evaluating the processing time and
the number of answers obtained for a query.

In all our experiments, the local theories of the 1000 peers of the
network have been generated as described in Section \ref{bench}, with
the fixed values $m=n=70$ and $t = 40$.  Those numbers are close to
what we would obtain by encoding taxonomies having the form of
balanced trees, with a depth between $3$ and $5$, in which each class
has between 2 and 3 sub-classes, and the extensional classes of which
correspond to the leaves of the tree.  Each peer theories contains in
addition $10*(1-\%3cnf)*q$ mapping clauses of length 2 and $10*q*\%3cnf$
mapping clauses of length 3.  Since we have seen in Section
\ref{single} that the proportion of 3-clauses in each local theory has
a strong impact on the hardness of the local computing performed for
each (sub)query at each peer, we have studied variations of the two
related parameters: $q$ and $\%3cnf$ of increasing complexity.
Note that the distributed theories considered in these experiments are quite large since
the size of the corresponding centralized theories ranges from 80~000 up
to 130~000 clauses over 70~000 variables.

\subsubsection{Behavior of Distributed Query Processing}
Let us now study the impact of the number $q$ of mapping clauses per
edge and of the ratio $\%3cnf$ of mapping clauses of length 3, on the
depth of queries. For this purpose we have measured, for each pair
$(q, \%3cnf)$, the depth of 1000 random queries\footnote{For
convenience, and since time is not here a direct issue (except from
the timeout impact), these experiments have been performed on a single
computer, running the 1000 peers. This made the building of reports
relying on peer traces much easier.}. Since we know (cf. Section
\ref{single}) that local computing may be sometimes very hard and
therefore may require a lot of time, it has been necessary to introduce an
additional {\em timeout} parameter. Each query is thus tagged with its
remaining time to live, which, on each peer, is decreased of the local
processing time, before propagating the induced subqueries. For these
experiments, the timeout value has been set to 30 seconds.



\begin{figure}[t]
\centerline{
\epsfig{figure=cdf-history-depth.eps,width=0.60\textwidth}
}
\caption{Cumulative distribution function of the depth of 1000 queries.
$q$ is the number of mapping clauses per edge, and
$\%3cnf$ is the ratio of 3-clauses in the mappings.  The $y$ scale has been
re-centered on $[0.4 - 1.0]$.}
\label{fig:queries-depth}
\end{figure}


Figure \ref{fig:queries-depth} shows the cumulative distribution
functions corresponding to each pair $(q, \%3cnf)$.  Each point on the 
figure reports a run, for a distinct query. 
The four leftmost curves correspond to cases where the query
depth remains relatively small. For instance, for $q=2$ and $\%3cnf=0$ 
none of the 1000 queries has a depth greater than 7. Altogether on the 
four leftmost curves none of the queries has a depth greater than 36. 
This suggests that our algorithm behaves well on such networks.

When the value of $\%3cnf$ increases, queries have longer depths. For
instance, with $q=3$ and $\%3cnf=20$, we can observe that 22\% of the
queries have a depth greater than 100 (the maximum being 134).  The
three rightmost curves have a similar shape, composed of three phases:
a sharp growth, corresponding to small depth queries, followed by a
plateau, and then a slower growth. The small depth query processing
and the 'plateau' are characteristics of an exponential distribution
of values: most of the processing is easy, but the little remaining is
very hard.  The slow growth observed is due to the timeout, a
side-effect of which is to bound the query depth. Without such a
timeout, previous experiments suggest that there would exist some
queries requiring very long reasoning branches.  This point is
outlined on the curve corresponding to the hardest cases ($q=3$ and
$\%3cnf=20$) where there is no query of depth between 20 and 60. This
suggests that when hard processing appears, it is {\em very hard}. One
may notice here that this last case corresponds to local theories
which are very close to one of cases studied in section \ref{single}.
As a matter of fact, with $q=3$ and $\%3cnf=20$ local theories are
very close to a $2+p$ theories of $m=100$ clauses with $p=6\%$.

In other experiments that we not detail here, we have checked that
such an exponential distribution of values cannot be observed when the
acquaintance graphs have a strong structure of a ring (this
corresponds to a rewiring probability $p=0$ in the network generator).
Because such an exponential distribution can be observed on random
graphs (corresponding to $p=1$), we suspect that such a behavior is
due to the short path length between two peers, a property shared by
both random and small world graphs. However, those two types of graphs
differ on their clustering coefficient, a property having a direct
impact on our algorithm behavior.

The depth of a query is the length of the history handled by the
algorithm, in which a given peer can appear several times since the
processing of subqueries (resulting of several splitting of clauses
entailed by the initial query) can solicit the same peer several times.
We have also measured the {\em integration degree} of queries, which is the
number of {\em distinct} peers involved in the query processing.  We
have observed the same kind of exponential distributions of values than
for the depth of queries, but with $20\%$ smaller values. This means that
about one fifth of the history peers are repeated ones. 
That phenomenon was not observed on random acquaintance graphs and
this seems closely related to the small world topology.  It is
important to point out that such a difference between small world and
random graphs could only be observed on large experimental data, with
a large number of peers.

\begin{figure}[t]
\centerline{
\epsfig{figure=cdf-width-linear.eps,width=0.60\textwidth}
}
\caption{Cumulative Distribution Function of queries width without
timeouts. Each curve summarise 20000 runs. The Y scale has been
re-centered on $[0.5 - 1.0]$, the X axis on $[0-25]$.}
\label{fig:queries-width}
\end{figure}

We have also studied how wide the reasoning propagates in the
network of peers during query processing.  For this purpose we have
evaluated the average number of neighbors peers that are solicited by
a peer when solving a query. We have estimated this value by
generating 20000 random queries on random peers, and counting for each
of them, the number of induced subqueries to neighbor peers.  Figure
\ref{fig:queries-width} shows, for different pairs $(q, \%3cnf)$, the
corresponding cumulative distribution functions. For instance, for
$q=2$ and $\%3cnf=0$, more than 75\% of the queries are solved locally
and 15\% of the remaining ones are solved by asking only one
neighbor. With $q=5$ and $\%3cnf=100$, about 25\% of the queries
solicit at least 10 neighbors. Of course, 25\% of the subqueries may
also solicit at least 10 peers and so on.

To summarize, our experiments have pointed out a direct impact of the
$\%3cnf$ value on the hardness of query processing, which is not surprising
considering the hardness of clauses of length 3 for prime implicates
computation.  Those experiments also suggest an exponential
distribution of query depths, due to the short path length between two
peers in the acquaintance graphs, and with an important repetition of
solicited peers, due to the large clustering coefficient of
small world acquaintance graphs.


\subsubsection{Time and Number of Answers}

We now report a time performance study of our algorithm when it is
deployed on a real cluster of 75 heterogeneous computers\footnote{All
computers were Linux Athlon units, with 1GB of RAM.  26 of them ran at
1.4GHz, 9 at 1.8GHz and 40 at 2 GHz.  Each computer was running around
14 randomly assigned peers}.  Based on the observations of the
previous sections, we have chosen to focus on 5 differents kinds of
acquaintance graphs, denoted {\em Very Easy}, {\em Easy}, {\em
Medium}, {\em Hard} and {\em Very Hard} (see Table \ref{tab:exp}). One
of the main goals of this section is to estimate where the limits of
processing of our algorithm are when it faces with hard (and even very
hard) \somewhere\ networks. Again, for all these experiments, we have
set the timeout value to 30s.

\begin{table}[!h]
\begin{center}\small
\begin{tabular}{c|| c | c | c | c | c }
 & Very Easy & Easy  & Medium & Hard & Very Hard\\
Network & $q=2$  & $q=3$  & $q=3$ & $q=5$ & $q=10$\\
&$\%3cnf=0$   & $\%3cnf=20$ & $\%3cnf=100$ & $\%3cnf=100$ & $\%3cnf=100$\\\hline \hline
$1^{st} ans.$ & 0.04s (100\%)& 1.26s (99.6\%) & 1.58s (95.6\%) & 1.39s (89.3\%) & 2.66s (49.7\%)\\
$10^{th} ans.$ & 0.06s (14.3\%)  & 1.37s (25.6\%) & 0.99s (33.3\%)& 1.13s (12.0\%) & 5.38s (29.9\%)\\ 
$100^{th} ans.$ &--   & 2.11s (12.7\%) & 0.84s (27.0\%) & 4.09s (10.7\%) & 11.0s (9.0\%)\\
$1000^{th} ans.$ & --    & 4.17s (6.80\%) & 4.59s (21.2\%)& 11.35s (7.15\%) & 16.6s (1.80\%)\\ \hline
all & 0.07s  & 5.56s & 14.6s & 21.23s & 27.74s\\ \hline\hline
\% timeout & 0\%  & 13.9\% & 37.5\% & 66.9\% & 86.9\%\\\hline\hline
\#answers & 5.17 & 364 & 1006 & 1004 & 65\\
\%unsat & 4.4\%  & 3.64\% & 3.76\% & 1.84\% & 1.81\% \\ 
\end{tabular}
\caption{Characteristics of the query processing ranging from very easy to very hard cases.} \label{tab:exp}
\end{center}
\end{table}


The values reported in Table \ref{tab:exp} are mean values over
more than three hundred different random queries. Each column
indicates the time needed to produce respectively the $1^{st}$,
$10^{th}$, $100^{th}$ and $1000^{th}$ answer of a query. The mean time
(in seconds) is followed by the percentage of initial queries that are
taken into account in the average. For instance, for a medium case
with $q=3$, 12.7\% of the queries have produced more than 100 answers,
and the $100^{th}$ answer was given on average after 2.11 seconds (the
average does not take into account queries that did not produce at
least 100 answers). The {\em all} row corresponds to the mean time
needed to produce all answers, including queries that lead to timeout,
 the percentage of which is reported in the {\em\%timeout}
row. The last two rows report the mean number of answers and the ratio
of proved unsatisfiable queries w.r.t. the \somewhere\ network (some
unsatisfiable queries w.r.t. the network may not have been counted since
inconsistency might have been found after the timeout).

Unsurprisingly, no timeout occurs for the {\em Very Easy} case.  It is
known that satisfiability checking and prime implicates computation
are tractable for sets of clauses of length 2. Moreover, the high
partitioning of the global theory induced by the low value of $q$
(number of mappings per peer) is often a witness of ``easy'' cases for
reasoning for centralized theories.  The point to outline for this
case is that there are 5 answers on average, and that they are
produced very quickly by our algorithm (in less than 0.1 seconds).

Let us now point out that, even on {\em Medium} and {\em Hard} instances, our algorithm
produces a lot of answers. For instance, we have obtained an average
of 1006 answers for $q=3$, and of 1004 answers for $q=5$. In addition, on those
hard instances, 90\% of runs produced at least one answer. It is
noticeable that in the {\em Very Hard case} ($q=10$), half of the
queries produce at least one answer, even if only 13\% of them
do complete without a timeout. 
%
Let us note yet that checking the satisfiability of the corresponding centralized
theories can also be very hard.
%
As a matter of fact the formula
corresponding to the centralized version of all the distributed
theories has $n$=70~000 variables and $m$=120~000 clauses, 50~000 of
which are of length 3. The ratio of 3-clauses in those $2+p$ theories is
thus $p=0.416$.  It has been shown \cite{ref2ppsat} that, for $2+p$
random formulas, if one does not restrict the locality of variables,
the SAT/UNSAT transition is continuous for $p<p_0$ ($p_0= 0.41$) and
discontinuous for $p>p_0$, like in 3-SAT instances.  Intuitively, for
$p>p_0$, the random $2+p$-SAT problem shares the characteristics of the
random 3-SAT problems, which is well known as the canonical
NP-Complete problem.  Let us recall that our generation model induces
a high clustering of variables inside each peer. Therefore we cannot claim that
the corresponding centralized theories have exactly the same cararacteristics
as  uniform $2+p$-SAT random formulas. However, if one only
focus on the values of the parameters $m$ and $n$, for the
characteristics of our {\em Very Hard} network, the transition phase
between SAT and UNSAT instance occurs at $m/n$=1.69. Here, we have
$m/n$=1.71, which is close enough from the transition phase to suspect
that this is where hard instances may be found.

To summarize, when deployed on a real cluster of heterogeneous
computers, our algorithm scales very well. Even on {\em Very Hard} instances
that share some characteristics of a very large $2+p$-SAT formula at
the crossover between the 2-SAT/3-SAT and the SAT/UNSAT transitions,
our algorithm is able to return many answers in a reasonable time.

%Related work & Conclusion
\section{Related work}
\label{related}

In Section \ref{logic}, we situate our work w.r.t. existing work related to distributed reasoning or 
distributed logics, while in Section \ref{pdms} we summarize the distinguishing points of
\somewhere \ among the existing peer data management systems.

\subsection{Related Work on Distributed Reasoning}
\label{logic}
The message passing distributed algorithm that we have described in
Section~\ref{algo} proceeds by splitting clauses and distributing
the work corresponding to each piece of clause to appropriate neighbor peers
in the network. The idea of splitting formulas into several parts may be found back
as the so called "splitting rule" in the natural deduction calculus, introduced in the 
middle of the 1930's by two independent works of \citeA{Gent35,Gentzen69} 
and \citeA{Jaskowski34}.  Our algorithm may be viewed as a 
distributed version of Ordered Linear Deduction \cite{Chang1973a} to produce 
new target clauses. This principle has been extended by  \citeA{Siegel1987a} in order to
produce all implicates of a given clause belonging to some target language,
and further extended to the first order case by \citeA{Inoue1992a}. 

We have already pointed out  the differences between our work 
and the approach of \citeA{Amir2000}. In a peer-to-peer setting, tree decomposition
of the acquaintance graph is not possible. In addition, 
as we have shown in the introductory example, the 
algorithm of \citeA{Amir2000} is not complete in the general case
for proper prime implicate computation.
However, \citeA{GR-IEEE-IS-03} have shown that completeness
can be guaranteed for a family of P2PIS with peer/super-peers topology.
It describes how to encode a P2PIS with peer/super-peers
into a  partitioned propositional theory in order to use the consequence 
finding algorithm of \citeA{Amir2000}. 
The model-based diagnosis framework for distributed embedded systems
\cite{Provan02} is based on the work of \citeA{Amir2000}.
We think it can benefit from our approach to apply to a real peer-to-peer setting 
in which no global knowledge has to be shared.

Other forms of distributed reasoning procedures may be found in multiagent frameworks,
where several agents try to cooperate to solve  complex problems. Problems
addressed in this way can generally be decomposed in several interacting subproblems,
each of which is addressed by one agent. This is the case for Distributed Constraint 
Satisfaction Problems (DCSP, \citeR{yokoo98distributed}). Given a set of variables, each of them being associated 
to a given domain, and a set of constraints on theses variables, the problem is to assign 
each variable one value in its respective domain, in such a way that all constraints are
satisfied.  In the distributed case, each variable is associated to some agent. Constraints may either
concern a set of variables relevant to a same agent or variables relevant to different agents. In the
first case, they may be considered as characterizing the local theory of the agent, while in the second
case they may be assimilated to mapping constraints between agents. Each mapping constraint is 
assigned to one agent. The problem addressed in DCSP is easier than the problem of consequence finding since
it is a satisfiability problem, which is NP-complete. While centralized CSP are
solved using a combination of backtrack search and consistency techniques, algorithms used to solve DCSP use
asynchronous versions of backtracking \cite{Yokoo1992a,yokoo98distributed} and consistency techniques
\cite{silaghisam-haroud_al_00}. Basically, agents proceed by exchanging invalid partial affectations, until 
converging to a globally consistent solution. Similar ideas may also be found in  
distributed ATMS \cite{datms}, where agents exchange nogood sets in order to
converge to a globally consistent set of justifications. 
Let us note that in contrast with the peer-to-peer vision, such methods aim at
sharing some global knowledge among all agents. 

Probabilistic reasoning on bayesian networks \cite{pearl88} has also given rise several adaptations
suited to distributed reasoning (e.g., the message passing algorithm of \citeR{pfeffer_tai_05a}). 
However the problem addressed in this context is different, since it consists in updating a 
set of a posteriori beliefs, according to observed  evidence and a set of 
conditional probabilities. These conditional probabilities are of the form $P(x|u_{1},...,u_{n})$ 
and describe the probability of the event $x$ when $u_{1}$ and \ldots and $u_{n}$ are observed.
They describe value interactions that can be viewed as mappings between a conjunction 
of literals and a single literal, which are oriented because of the nature or conditioning.

Another work using oriented mappings is the framework of {\em distributed first order logic}
\cite{ghidini-serafini}, in which a collection of first order theories can communicate 
through {\em bridge rules}. This approach adopts an epistemic semantics
where connections 
between peer theories are reflected by mappings between the respective domains of interpretation of 
the involved peers.  Based on that work, {\em distributed description logics} have been introduced by 
\citeA{borgida-serafini} and a distributed tableau method is described for reasoning in distributed
description logics has been proposed by \citeA{SerafiniTamilin04}. 
A reasoning algorithm has been implemented in \textsc{Drago} \cite{drago} 
where the bridge rules are restricted to inclusion statements between atomic concepts.

\subsection{Related Work on Peer Data Management Systems}
\label{pdms}
As we have pointed it out in Section \ref{somewhere}, the  \somewhere \
peer data management system distinguishes from \textsc{Edutella} ~\cite{edutella} by the fact that
there is no need of super-peers, and from \textsc{Piazza} \cite{halevy-pdms,piazza} because it does
not require a central server having the global view of the overlay network. \\

From the semantic point of view, \somewhere uses a propositional language and mappings
correspond to unrestricted formulas. Its semantics is the standard propositional semantics 
and query answering is always decidable. 
The peer data management systems investigated by \citeA{halevy-pdms} use a relational language
and their mappings correspond to inclusion statements between conjonctive queries. 
The semantics used in this work is the  standard FOL semantics, for which query answering 
is shown to be undecidable in the general case. Restricting to acyclic mappings renders query 
answering decidable in Piazza, but checking this property requires some global knowledge 
on the network topology and is performed by the central server.


The peer data  management system considered in the work of \citeA{calvanese-et-al-2004} 
is similar to that of \citeA{halevy-pdms} but proposes an alternative 
semantics based on  epistemic logic. With that semantics it is shown that query answering is always 
decidable (even with cyclic mappings). Answers obtained according to this semantics correspond
to a subset of those that would be obtained according to the standard  FOL semantics. 
However, to the best of our knowledge, these results are not implemented. \\
 
From the systems point of view, the recent work around the \textsc{coDB} peer data management system 
\cite{coDB} supports dynamic networks but the first step of the distributed algorithm is to let each 
node know the network topology. In contrast,  in \somewhere \, no node does have to know the 
topology of the network.

The \textsc{KadoP} system \cite{kadop} is an infastructure based on distributed hash tables 
for constructing and querying peer-to-peer warehouses of XML resources
semantically enriched by taxonomies  and mappings. The mappings that are considered 
are simple inclusion statements between atomic classes. Compared to \textsc{KadoP} 
(and also to \textsc{Drago}, \citeR{drago}), the mapping  language that is dealt with in \somewhere \ is
more expressive than simple inclusion statements between atomic classes. 
It is an important difference which 
makes \somewhere \ able to {\em combine} elements of answers 
coming from different sources for answering a query, 
which  \textsc{KadoP} or \textsc{Drago} cannot do.

\somewhere \ implements in a simpler setting the (not implemented) vision of peer to peer data 
management systems proposed by \citeA{bernstein-pdms} for the relational model.


\section{Conclusion}
\label{conclusion}
%% Conclusion
The contributions of this paper are both theoretical and practical.
We have provided the first distributed consequence finding algorithm 
in a peer-to-peer setting, and we have exhibited a sufficient condition
for its completeness.
We have developed a P2PIS architecture that implements this algorithm and for which 
the first experimental results look promising. This architecture is used in a joint 
project with France T\'el\'ecom, which aims at enriching
peer-to-peer web applications with reasoning services (e.g., \textsc{Someone}, \citeR{PLU-WWW-03}).


% Target language

So far, we have  restricted our algorithm to deal with a vocabulary-based 
target language. However,  it can  be adapted to 
more sophisticated target languages (e.g., implicates of
a given, maximal, length, language based on literals and not only
variables). This can be done by adding a simple tag over
all messages to encode the desired target language.

Another possible extension of our algorithm is to allow more compact
representation of implicates, as proposed by \citeA{SimonDelVal2001}. This
work relies on an efficient clause-distribution operator.
It can be adapted by extending messages in
our algorithm in order to send \textit{compressed} sets of clauses
instead of one clause as it is the case right now, without changing
the deep architecture of our algorithm.

In the Semantic Web direction, we plan to deal with  distributed RDF(S) resources 
shared at large scale. 
RDF(S) \cite{SWP} is a W3C standard for annotating web resources, which we think can be
encoded in our propositonal setting.

In the distributed reasoning direction, we plan  to consider more sophisticated reasoning 
in order to deal with a real multi-agent setting, in which possible inconsistencies between agents
must be handled.

\section*{Acknowledgnents}
This  paper is a revised and extended version of an ECAI short paper \cite{ACGRS-ECAI-04} and of 
an IJCAI paper \cite{ACGRS-IJCAI-05}.

%Bibliography
\bibliography{biblio}
\end{document}
