\documentclass[twoside,11pt]{article}

\usepackage   []            {jair}
\usepackage   [latin1]      {inputenc}
\usepackage   [T1]          {fontenc}
\usepackage   []            {theapa}
\usepackage   []            {latexsym}
\usepackage   [dvips]       {graphicx}
\usepackage   []            {amsmath}
\usepackage   []            {amssymb}
\usepackage   []            {amsfonts}
\usepackage   []            {epsfig}
\usepackage   []            {float}
\usepackage   []            {pstexscale}
\usepackage   []            {psfrag} 


\jairheading{16}{2002}{425-465}{06/01}{06/02}
\ShortHeadings{The Complexity of Rules and Constraints}
{Baget \&  Mugnier}
\firstpageno{425}

\newtheorem{definition} {Definition}
\newtheorem{property}   {Property}
\newtheorem{theorem}   {Theorem}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}    {Lemma}



\newcommand{\qed} {\hfill $\Box$ \smallskip}

\newcommand{\nbN}{\ensuremath{\mathrm{I\!N}}}
\newcommand{\mb} [1] {\mbox{\textit {\textrm{#1}}}}


\begin{document}

\title{Extensions of Simple Conceptual Graphs:\\ the Complexity of Rules and Constraints}

\author{\name Jean-François Baget \email baget@lirmm.fr \\
        \name Marie-Laure Mugnier \email mugnier@lirmm.fr \\
        \addr LIRMM (CNRS \& UM II), 161 rue Ada \\
         34392 Montpellier, Cédex 5, France}

\maketitle


\begin{abstract}

\emph{Simple conceptual graphs} are considered as the kernel
of most knowledge representation formalisms built upon
Sowa's model. Reasoning in this model can be
expressed by a graph homomorphism called projection, whose semantics 
is usually given in terms of positive, conjunctive, existential FOL. 
We present here a family of extensions of this model, based on
\emph{rules} and \emph{constraints}, keeping graph homomorphism as the
basic operation. We focus on the formal 
definitions of the different models obtained, including their operational semantics 
and relationships with FOL, and we analyze the decidability and 
complexity of the associated problems (consistency and deduction).
 As soon as rules are involved in
reasonings, these problems are not decidable, but we exhibit a
condition under which they fall in the polynomial hierarchy.
 These results extend and complete the ones 
already published by the authors.
Moreover we systematically study the complexity of some particular
cases obtained by restricting the form of constraints and/or rules. 

\end{abstract}

\section{Introduction}
%%%%%%%%%%%%%%%%%%%%%

Conceptual graphs (CGs) have been proposed as a knowledge 
representation and reasoning model, mathematically founded both on logics 
and graph theory  \cite{sowa:84}. Though they have been mainly  studied as a graphical 
interface for logics or as a diagrammatic system  of logics (for 
instance, see  \citeR{wermelinger:95}, for general CGs equivalent to FOL), 
their graph-theoretic foundations
have been less investigated. Most works in this area are limited to \emph{simple 
conceptual graphs}, or \emph{simple graphs}
\cite{sowa:84,chein-mugnier:92}, which correspond to the positive,
conjunctive and existential fragment of FOL without functions. 
This model has three fundamental characteristics:
\begin{enumerate}
        \item objects are bipartite \emph{labelled graphs} 
        (nodes represent 
        \emph{entities} and \emph{relations} between these entities);
        \item reasonings are based on graph-theoretic operations, relying on  a 
        kind of graph homomorphism called \emph{projection};
        \item it is logically founded, reasonings being sound and complete 
        w.r.t. FOL semantics, usually by way of the translation called $\Phi$.
\end{enumerate}

Main extensions of the simple graphs model, keeping graph
homomorphism based operations 
and sound and complete semantics, are 
\emph{inference rules}
\cite{gosh-wuwongse:95,salvat-mugnier:96,salvat:98} and  \emph{nested graphs} 
\cite{chein-mugnier-simonet:98,preller-mugnier-chein:98}; for \emph{general CGs} equivalent to FOL,
an original deduction system \cite{kerdiles:97}
combines analytic tableaux with the simple graphs projection. Some kind
of \emph{constraints} have been proposed to validate a knowledge base composed
of simple graphs \cite{mineau-missaoui:97,dibie-haemmerle-loiseau:98}.

We present here a family of extensions of the simple graphs model. The common
ground for these extensions is that objects are \emph{colored simple graphs} representing
 \emph{facts}, \emph{rules} or 
\emph{constraints}, and operations are based upon projection. 
Given a knowledge base $\mathcal K$ and a simple graph $Q$ 
(which may represent a query, a goal, \dots, 
depending on the application), the \emph{deduction problem} asks
whether $Q$ can be deduced from  $\mathcal K$.
%the
%deduction problem asks, given  $\mathcal K$ a knowledge base and
%$Q$ a simple graph (which may represent a query, a goal, \dots, 
%depending on the application), whether $Q$ can be deduced from  $\mathcal K$. 
According to the kinds of objects 
considered in $\mathcal K$,
different reasoning models are obtained, composing the $\mathcal {SG}$ family.
Though similar notions of rules and constraints can be found in the
CG literature, their combination in reasonings had never been studied.
One interest of our approach thus resides in providing a unifying
framework combining rules and constraints in different ways.

In this paper,
we focus on the formal definitions of these models, including  their
operational semantics and relationships with FOL, and we study the
decidability and complexity of their associated decision problems, 
namely consistency and deduction. These results extend and complete the ones 
already published by the authors \cite{baget-mugnier:01}. Though
both consistency and deduction are undecidable in the most general
model of this family, we had already used a decidable subset of
rules to solve the {\sc Sisyphus-I} problem, a test-bed proposed
in the knowledge acquisition community \cite{baget-genest-mugnier:99}.
We present here for the first time a detailed analysis of complexity
when we restrict the knowledge base to this kind of rules (called
\emph{range restricted} rules). We also study particular cases of
constraints. 

In section 2 basic definitions and results about simple
graphs are recalled. Section 3 presents an overview of the $\mathcal
{SG}$ family. In particular, we explain why we consider graphical
features of the simple graphs model as essential for  knowledge modeling  and
point out that these properties are preserved in the $\mathcal
{SG}$ family. In next sections we
study the different members of the family. Rules are introduced in section 4,
constraints in section 5, and section 6 studies models combining rules
and constraints. As soon as rules are involved in reasonings, the
associated decision problems are not decidable, but we exhibit a
condition (finite expansion sets) under which computations always
stop. In the particular case of \emph{range restricted} rules,
the complexity of these problems fall into the polynomial hierarchy.
Section 7 is devoted to these
decidable cases. In section 8, relationships with other works are established.
In particular we point out algorithmic connections with constraint
satisfaction problems (CSP) and show that the problem of checking the consistency of a knowledge base composed of simple graphs and constraints ($\mathcal{SGC}$-consistency) is equivalent to that of deciding the consistency of a mixed CSP \cite<MIXED-SAT, >{fargier-lang-schiex:96}.  

\section{Basic Notions: the $\mathcal{SG}$ Model}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We recall in this section basic notions about simple conceptual graphs
\cite{sowa:84,chein-mugnier:92}. These graphs are considered as the kernel for most
knowledge representation formalisms built upon Sowa's work. They are also the
basic model for the $\mathcal{SG}$ family.

\subsection{Definitions and Notations}

Basic ontological knowledge is encoded in a structure  called a
\emph{support}. Factual knowledge is encoded into \emph{simple graphs}
(SGs), defined with respect to a given support. A SG is a bipartite labelled
graph (strictly speaking, it is a \emph{multigraph}, since there can be
several edges between two nodes). One class of nodes represents
entities, the other class represents relationships between these
entities. Nodes are labelled by elements of the support. 
Elementary reasonings are computed by a graph homomorphism 
called \emph{projection}.


\begin{definition}[Support]
A \emph{support} is a 4-tuple $\mathcal S = (T_C, T_R, \mathcal I, \tau)$.
$T_C$ and $T_R$ are two partially ordered finite sets, respectively of \emph{concept types}
and \emph{relation types}. $T_R$ is partitioned into subsets $T_R^1
\dots  T_R^k$ of relation types of arity $1 \dots k$ respectively ($k
\geq 1$). Two elements of distinct subsets are incomparable. Both
orders on $T_C$ and $T_R$ are denoted by $\leq$ ($x \leq y$ means that
$x$ is a subtype of $y$). 
$\mathcal I$ is the set of \emph{individual markers}. $T_C$, $T_R$ and
$\mathcal I$ are pairwise disjoint. $\tau$ is a
mapping from $\mathcal I$ to $T_C$.  
We denote by $\ast$ the \emph{generic marker}, 
where $\ast \notin \mathcal I$. A partial order on $\mathcal I \cup \{\ast\}$ considers
elements of $\mathcal I$ as pairwise incomparable, and $\ast$ as its greatest element.
\end{definition}

 All partial orders will be denoted by $\leq$,
and, if needed, indexed by the name of the set on which they are
defined. In this paper the intuitive meaning of $x \leq y$ is always
\emph{$x$ is a specialization of $y$}.  Fig. \ref{support} partially describes a support, 
which will be used in further examples. 

\begin{figure}[h]
\begin{center}
\psfrag{Universal}[c][c][1]{\scriptsize{$\top_c$}}
\psfrag{Project}[c][c][1]{\scriptsize{\tt Project}}
\psfrag{Person}[c][c][1]{\scriptsize{\tt Person}}
\psfrag{Office}[c][c][1]{\scriptsize{\tt Office}}
\psfrag{Researcher}[c][c][1]{\scriptsize{\tt Researcher}}
\psfrag{Manager}[c][c][1]{\scriptsize{\tt Manager}}
\psfrag{HeadOfProject}[c][c][1]{\scriptsize{\tt HeadOfProject}}
\psfrag{member}[c][c][1]{\scriptsize{\tt member}}
\psfrag{work-with}[c][c][1]{\scriptsize{\tt works-with}}
\psfrag{geographical-relation}[c][c][1]{\scriptsize{\tt geographical-relation}}
\psfrag{in}[c][c][1]{\scriptsize{\tt in}}
\psfrag{near}[c][c][1]{\scriptsize{\tt near}}
\psfrag{adjoin}[c][c][1]{\scriptsize{\tt adjoin}}
\psfrag{link}[c][c][1]{\scriptsize{$\top_r^2$}}
\psfrag{TC}[c][c][1]{$T_C$}
\psfrag{TR = TR2}[c][c][1]{$T_R = \{T_R^2\}$}
\includegraphics[width=11cm]{./figures/support}

\medskip

$\mathcal I = \{$ {\tt J., K., \#124,~...}$\}$ \\
$\tau =   \{$ {\tt (J., {\tt Researcher}), (K., {\tt Researcher}), (\#124, {\tt Office}),~... }$\}$
\caption{Support}
\label{support}
\end{center}
\end{figure}

\begin{definition} [Simple Graph]
A \emph{simple graph} $G$, defined over a support $\mathcal S$, is a
finite bipartite
multigraph $(V = (V_C, V_R), U, \lambda)$. 
 $V_C$ and $V_R$ are the node sets, respectively of \emph{concept nodes} 
and of \emph{relation nodes}.  $U$ is the multiset of \emph{edges}. 
Edges incident on a relation node are totally ordered;
they are numbered from 1 to the degree of the node. An edge numbered $i$
between a relation node $r$ and a concept node $c$ is denoted by $(r,i,c)$ and  identifies a unique element of $U$. $U$ will also be seen as a set of
such triples.
  
%%%XXXWe denote by $G_i(r)$ the $i^{th}$ neighbor of a relation node $r$
%%%in $G$ NECESSAIRE? XXX

Each node has a label given by
the mapping $\lambda$. A  relation node $r$ is labelled by \emph{type($r$)}, an element of $T_R$, called its 
\emph{type}, and the degree of $r$ must be equal to the arity of
\emph{type($r$)}.
Thus, if $r \in T^k_R$, $|\{(r,~i,~c)| (r,~i,~c) \in U \}| = k$ and
$\{ i |(r,~i,~c) \in U \} = \{1,~...~k\}$. 
A concept node $c$ is labelled by 
a pair \emph{(type($c$), marker($c$))}, where \emph{type($c$)} is an
element of $T_C$, called its \emph{type}, and \emph{ marker($c$)} is an element of $\mathcal I \cup \{\ast\}$, called 
its \emph{marker}. If  marker($c$) is an individual marker $m$, then  type($c$)= $\tau(m)$. 

\end{definition}

A concept node with a generic marker is called a \emph{generic node} (it refers to an unspecified entity of a certain type);
otherwise it is called an \emph{individual node} (it refers to a specific individual defined in the support). We will adopt the following
classical conventions about SGs. 
In the drawing of a SG, concept nodes are represented by rectangles and relation nodes
by ovals. In textual notation, rectangles are replaced by {\tt[]} and ovals
by {\tt ()}. Generic markers are omitted. Thus a generic concept label $(t, *)$ is
simply noted $t$. An individual concept label $(t,m)$ is noted $t:m$. When in our examples we use  binary relations, we may replace numbers on
edges by directed edges: a binary relation node is then incident to
exactly one incoming and one outgoing edge. Fig.~\ref{simplegraphs}
shows two (connected) simple graphs $G$ and $Q$ assumed to be
defined over the support of Fig. \ref{support}. 



\begin{figure}[h]
\psfrag{Project}[c][c][1]{\scriptsize{\tt Project}}
\psfrag{Person}[c][c][1]{\scriptsize{\tt Person}}
\psfrag{Office}[c][c][1]{\scriptsize{\tt Office}}
\psfrag{Office: #124}[c][c][1]{\scriptsize{\tt Office: \#124}}
\psfrag{Researcher}[c][c][1]{\scriptsize{\tt Researcher}}
\psfrag{Researcher: J.}[c][c][1]{\scriptsize{\tt Researcher: J.}}
\psfrag{Researcher: K}[c][c][1]{\scriptsize{\tt Researcher: K.}}
\psfrag{member}[c][c][1]{\scriptsize{\tt member}}
\psfrag{works-with}[c][c][1]{\scriptsize{\tt works-with}}
\psfrag{in}[c][c][1]{\scriptsize{\tt in}}
\psfrag{near}[c][c][1]{\scriptsize{\tt near}}
\psfrag{G}[c][c][1]{$G$}
\psfrag{G'}[c][c][1]{$G'$}
\psfrag{Q}[c][c][1]{$Q$}
\centerline{\includegraphics[width = 15 cm]{./figures/simplegraphs}}

%\small \centerline{
%Dashed lines identify a subgraph $G'$ of $G$}. 

\caption{Simple graphs.}

\label{simplegraphs}
\end{figure}

%%\vspace*{-0.6cm}

The elementary reasoning operation, projection, is a kind of graph homomorphism
that preserves the partial order defined on labels. Let us first precise this
order for concept node labels. We have defined the following partial order on the marker set 
$\mathcal I \cup \{*\}$: $*$ is the greatest element (for all $m \in \mathcal
I$, $m \leq *$) and elements of $\mathcal
I$ are pairwise non comparable. Then the \emph{partial order on concept node
labels} is the product of the partial orders on  $T_C$ and $I \cup
\{*\}$, i.e. $(t,m) \leq (t',m')$ iff $t \leq t'$ and  $m \leq m'$. 
In other words, a concept label $(t,m)$ is more specific than a
concept label $(t',m')$ if $t$ is a subtype of $t'$ and, if $m' = *$,
then $m$ can be any marker, otherwise $m$ must be equal to $m'$.

  
\begin{definition}[Projection]
Let $Q$ and $G$ be two SGs defined on a support $\mathcal S$. A \emph{projection} from $Q$ into $G$
is a mapping $\pi$ from $V_C(Q)$ to $V_C(G)$ and from $V_R(Q)$ to
$V_R(G)$ which preserves edges (it is a bipartite graph homomorphism)
as well as their numbering, and may specialize concept and relation
node labels:

%%\vspace*{-0.2cm}

\begin{enumerate}
        \item $\forall (r,i,c)\in U(Q), (\pi(r),i,\pi(c)) \in U(G)$;
        \item $\forall x \in V(Q), \ \lambda(\pi(x)) \leq \lambda (x)$
\end{enumerate}
\end{definition}

%%\vspace*{-0.1cm}


We note $Q \geq G$ ($Q$ subsumes $G$) if there exists a projection 
from $Q$ into $G$. Typically, $Q$ represents a query, $G$ a fact, and projections
from $Q$ to $G$ define answers to $Q$. 
In Fig. \ref{simplegraphs}, suppose \emph{Researcher}
$\leq$ \emph{Person}, then there is  one projection from $Q$ into
$G$. The image of $Q$ by this projection is the
subgraph $G'$ of $G$. 

\subsection{Relationships with FOL}


The semantics  $\Phi$ maps SGs to the existential conjunctive and
positive fragment of FOL. 
Given a support $\mathcal{S}$,
 a constant is assigned to each individual marker
and an $n$-adic (resp. a unary) predicate is assigned to each $n$-adic  
relation (resp. concept) type. 
For simplicity, we consider that each constant or predicate has the same name as the associated element
of the support. A set of formulas $\Phi(\mathcal S)$ is
assigned to any support $\mathcal S$, translating partial orders on
types. More specifically, for all distinct types $t_1$ and $t_2$ such that $t_2
\leq t_1$, one has the formula
 $\forall x_1 ... x_p  (t_2(x_1,~...,x_p) \rightarrow t_1(x_1,~...,x_p))$, 
where $p=1$ for concept types, and  $p$ is otherwise the arity of the
relation type. Given any SG $G$, a formula $\Phi(G)$ is built as follows. A
term is assigned to each concept node: a distinct variable for each
generic node, and the constant corresponding to its marker
otherwise. Then an atom 
 $t(c)$
 (resp.~$t(c_1,~...~,c_k)$) is associated to each
concept node  (resp.~relation node $r$ of arity $k$), where $t$ is the type of the node,
and $c$ (resp.~$c_i$) is the term assigned to this node (resp.~assigned to
the $i$th neighbour of $r$).  Let
$\alpha(G)$ be the conjunction of these atoms. $\Phi(G)$ is the
existential closure of $\alpha(G)$. E.g.  the formula assigned to the
subgraph $G'$ in Fig. \ref{simplegraphs} is \emph{$\exists x \exists
y (\mbox{Researcher}(x)  \wedge \mbox{Project}(y) \wedge
\mbox{Researcher}(K) \wedge \mbox{member}(x, y) \wedge \mbox{member}(K,
y) \wedge \mbox{works-with}(x,K))$}. 

%%\vspace*{-0.1cm}


 Projection is sound and complete  w.r.t. the semantics $\Phi$, up to a
normality condition for completeness; the \emph{normal form} of a SG
$G$ is the SG $\mb{nf}(G)$ obtained by merging concept nodes having the
same individual marker. This SG always exists (and is computable in
linear time with a naive algorithm). Figure \ref{normal} shows a
counter-example to projection completeness when SGs are not in
normal form: $G$ for instance does not project to $H$, even if both
SGs have the same logical semantics, but it projects to
$\mb{nf}(H)$. A SG in normal form is said to be \emph{normal}.

\begin{figure}[h]
\psfrag{G}[c][c][1]{$G$}
\psfrag{H}[c][c][1]{$H$}
\psfrag{nf(G) = nf(H)}[c][c][1]{$\mbox{nf}(G) = \mbox{nf}(H)$}
\centerline{\includegraphics[width = \linewidth]{./figures/normal}}

\medskip

\begin{center}
{\footnotesize
 $\Phi(G) = \Phi(H)=
  \exists x t(x) \wedge t(a) \wedge t(a) \wedge r(x,~a) \wedge
 s(x,~a) \wedge u(x,~a)$\\
$G$ and $H$ have same logical translation (thus same normal form) but they are
 incomparable by projection.
}
\end{center}

        \caption{The need for normal forms}
\label{normal}
\end{figure}


\begin{theorem}[\citeR{chein-mugnier:92,gosh-wuwongse:95}]
\label{acp}
Let $Q$ and $G$ be two $SG$s defined on a support $\mathcal S$. Then 
$Q \geq \mb{nf}(G)$ if and only if $\Phi(\mathcal S),
\Phi(G) \vDash \Phi(Q)$.
 \end{theorem}

We claimed in the introduction that SGs are equivalent to the
positive, conjunctive and existential fragment of FOL without
functions (let us denote it by FOL($\wedge$, $\exists$)). One embedding is immediate (from FOL to SGs), but requires the definition of a 
support that does not add anything to the semantics of the
involved graphs. A \emph{flat support} is a support whose
translation by $\Phi$ is empty, \emph{i.e.} where all distinct types
are non comparable. If $V$ is the vocabulary (constants and predicates) 
for a set of formulas, we consider the flat
support $\mathcal S_f(V) = (T_C, T_R, \mathcal I)$ where
$T_C$ is restricted to the element $\top_C$, the relation types
of $T_R^i$ are the predicates of arity $i$ in $V$,
and the individual markers of $\mathcal I$ are the constants
in $V$.



%To any set $\mathcal F$ of formulas, we can
%associate the flat support 
%$\mathcal S_f(\mathcal F) = (T_C, T_R, \mathcal I)$ where
%$T_C$ is restricted to the element $\top$, the relation types
%of $T_R^i$ are the predicates of arity $i$ in $\mathcal F$,
%and the individual markers of $\mathcal I$ are the constants
%in $\mathcal F$.



\begin{property}[Embedding FOL($\wedge$, $\exists$) into
  $\mathcal{SG}$]
There is a bijection $f2g$ mapping the set of FOL($\wedge$, $\exists$) formulas
over a vocabulary $V$ to the set of normal SGs defined on the flat
support $\mathcal S_f(V)$ such that, for any two formulas $g$ and
$h$, $g \vDash h$ iff there is a
projection from $f2g(h)$ into $f2g(g)$.
%Moreover, $f2g^{-1} = \Phi$.
%Let $g$ and $h$ be two formulas of FOL($\wedge$, $\exists$). 


%There
%exist (normal) SGs $G$ and $H$ defined on the flat support 
%$\mathcal S_f(\{g, h\})$ 
%such that $g = \Phi(G)$, $h = \Phi(H)$,
%and $g \vDash h$ iff there is a
%projection from $H$ into $G$.  
\end{property}

\noindent \emph{Proof:} 
Let $f$ be a FOL($\wedge$, $\exists$) formula over a vocabulary $V$.
The SG $f2g(f)$ defined on the support $\mathcal S_f(V)$ is built as
follows: to each term of $f$ we associate a concept node typed $\top_C$
(generic if the term is a variable, individual with a marker $c$ if
the term is the constant $c$), and to each atom $t(x_1, \dots, x_q)$
we associate a relation node $r$ typed $t$, such that, for $1 \leq i \leq q$,
the $i$th neighbor of $r$ is the concept node associated to $x_i$.

The mapping $f2g$ is clearly injective, \emph{i.e.} it maps different
formulas (not identical up to variable renaming) to different SGs
(not identical up to an isomorphism). Moreover, it is a bijection
if we restrict SGs to those in normal form.

Let us now consider the  FOL($\wedge$, $\exists$) formula $f =
\exists \vec{x_i} (\alpha(\vec{x_i}))$ (where $\alpha(\vec{x_i})$
is a conjunction of atoms whose variables belong to $\vec{x_i}$). 
The $\top_C$-enriched formula of $f$ is the formula $te(f) =
\exists \vec{x_i} (\alpha(\vec{x_i}) \wedge \beta(\vec{x_i}))$
where $\beta(\vec{x_i})$ is the conjunction of the atoms
$\top_C(x)$, for every term $x$ in $f$.
We now prove the property by pointing out that, 1) for $f$ and $g$
two FOL($\wedge$, $\exists$) formulas, $f \vDash g$ iff $te(f) \vDash te(g)$,
and 2) for any FOL($\wedge$, $\exists$) formula $f$, $te(f) = \Phi(f2g(f))$,
and conclude using Th.~\ref{acp}.
%Given $g$ and $h$, let us build a support $\mathcal S$, where
%$T_C$ is restricted to one element, say $\top$, $T_R$ is the set of
%predicates in $g$ and $h$, all non comparable, and $\mathcal I$ is the set of
%constants in $g$ and $h$. Let $g'$ and $h'$ be the formulas obtained
%from $g$ and $h$ by adding an atom $\top(e)$ for each term $e$ in $g$
%and $h$. Now let us restrict the domain of $\Phi$ to normal
%SGs. $\Phi$ is then a bijection. Then, let $G = \Phi^{-1}(g)$ and
%$H = \Phi^{-1}(h)$. We conclude with theorem \ref{acp}, noticing that
%$\Phi(\mathcal S)$ is empty. 
\qed


For the other direction, the apparent problem is that formulas assigned to the support by $\Phi$ are
universally quantified and are used in the deduction process. However,
we can do without them, by encoding the partial order on types directly in the SGs. 
%the knowledge
%encoded in the support.
%For instance, let us define a variant of $\Phi$, say
%$\Phi'$, which maps a SG to an existential formula integrating the needed
%knowledge about the support.  Let us call $\mathcal S_{flat}$  the
%trivial support obtained from $\mathcal S$ by removing the partial orders
%(i.e. $\leq$ is the identity relation). Given a SG $G$ over $\mathcal S$, let us consider the
%SG $G_{\mathcal S}$ over $\mathcal S_{flat}$ obtained from $G$ in the following way: for each
%relation node $r$ of type $t_r$ in $G$, for each relation type $t_{r'}$ in
%$\mathcal S$ greater than $t_r$, a relation node of type $t_{r'}$ with
%same neighbors as $r$ is added. It is immediately checked that,
%given two SGs $G$ and $H$ over $\mathcal S$, there is a projection
%from $H$ to $G$ iff there is a projection from $H_{\mathcal S}$ to
%$G_{\mathcal S}$, both relative to $\mathcal S_{flat}$. Now let us define
%$\Phi'(G, \mathcal S) = \Phi(G_{\mathcal S})$. Also notice that
%$\Phi(\mathcal S_{flat})=\emptyset$. Then, $\Phi(\mathcal S),
%\Phi(G) \vDash \Phi(H)$ holds iff $\Phi'(G, \mathcal S) \vDash
% \Phi'(H, \mathcal S)$  holds.  


\begin{property}[Embedding  $\mathcal{SG}$ into FOL($\wedge$, $\exists$)]
%Let $G$ and $H$ be two normal SGs over a support $\mathcal S$. There exist  
%formulas of FOL($\wedge$, $\exists$) $g$ and $h$ such that $g \vDash
%h$ iff there is a projection from $H$ to $G$.  
There is a injective application $g2f$ mapping the set 
of normal SGs defined on a support $\mathcal S$ to the set of 
FOL($\wedge$, $\exists$) formulas such that, for any two SGs
$G$ and $H$ defined on $\mathcal S$, there is a projection from
$H$ into $G$ iff $g2f(G) \vDash g2f(H)$.
%of FOL($\wedge$, $\exists$) formulas
%over a vocabulary $V$ to the set of normal SGs defined on the flat
%support $\mathcal S_f(V)$ such that, for any two formulas $g$ and
%$h$, $g \vDash h$ iff there is a
%projection from $f2g(h)$ into $f2g(g)$.
\end{property}

\noindent \emph{Proof:} Let $G$ be a graph defined on a support
$\mathcal S$. The expansion of $G$, $exp(G)$, is the SG defined
on the flat support $\mathcal S_f(V)$ (where $V$ is the vocabulary
for the formulas of $\Phi(\mathcal S)$), built as follows:
1) for every concept node $x = [t: m]$ of $G$, $exp(G)$ contains an associated concept node
$x' = [\top_C: m]$, s.t., for each concept type $t' \in \mathcal S$ greater or equal
to $t$, a unary relation node of type $t'$ linked to $x'$ and 2) for every relation node $x$ of $G$ (of type $r$ and arity $k$),
for every relation type $r' \in \mathcal S$ s.t. $r \leq r'$, we add
in   $exp(G)$ a relation node typed $r'$ with same neighbors as $x$.
%are the same
%as those of $x$. 
%In this construction, concept types are considered as
%unary relation types. 
We now define the application $g2f$ as $\Phi \circ exp$,
and conclude using Th.~\ref{acp}, noticing that $\Phi(\mathcal S_f(V)) = \emptyset$.




%Take $g=\Phi'(G, \mathcal S)$ and $h=\Phi'(H,
%\mathcal S)$ and use theorem \ref{acp}. 
\qed

Using similar transformations, a close relationship to the problem of
\emph{query containment} studied in the database field has been shown: checking
query containment for non recursive conjunctive queries is equivalent
to checking projection between SGs \cite{chein-mugnier-simonet:98,mugnier:00}. 

\subsection{The Deduction Problem: Computational Complexity}

For the sake of
brevity, we consider in what follows that SGs 
are given in normal
form, and put into normal form if needed after a modification. 
And, since a SG does not need to be a connected graph, we conflate
a set of SGs with the SG obtained by performing the
disjoint union of its elements. In the following definition, for
instance, the SG $\mathcal G$ represents a set of SGs.  

\begin{definition}[$\mathcal{SG}${\sc -deduction}] 
Let $\mathcal G$ and $Q$ be two SGs  defined on a support $\mathcal S$.
$Q$ can be deduced from $\mathcal G$ if $Q \geq \mathcal G$. 
\end{definition}

\citeA{chein-mugnier:92} have shown that projection checking 
is NP-complete with a reduction from  
{\sc clique}. 
Equivalence with CSP (satisfiability of a constraint network)
was also used later \cite{feder-vardi:93,Mugnier-Chein:96}, and
independently in a very similar model by \citeA{rudolf:98} (see part
\ref{related} of this paper).
We give below another proof of this result based on a reduction from
3-SAT. 
Though more complicated than the previous ones, this reduction is
the basis for other reductions presented later in this paper. 

The following theorem keeps into account the complexity of concept and
relation type checking, though in this paper this test can
obviously be performed in polynomial time  since 
concept and relation types are only labels partially ordered in
a hierarchy.

 
\begin{theorem}[\citeR{chein-mugnier:92}]\label{npc}
$\mathcal{SG}${\sc -deduction} is a NP-complete problem, iff
type checking in $\mathcal S$ belongs to NP.
\end{theorem}

\noindent \emph{Proof:} First see that if type checking is in NP,
then $\mathcal{SG}${\sc -deduction} is also in NP: a 
projection, enriched by certificates for all type checks used,
is a polynomial certificate. 
The reciprocal is obviously true. We now show that,
even if type checking
can be done in $\Theta(1)$, $\mathcal{SG}${\sc -deduction}
is NP-complete. 

Let us now build a reduction from 3-SAT.  The input of 3-SAT is
a formula $\mathcal F$ in 3-conjunctive normal form (3-CNF), i.e.  a conjunction of disjunctions (clauses), each with at most three
literals, and the question is whether there is a truth assignment of
the variables of $\mathcal F$ such that $\mathcal F$ is true. Notice
the classical 3-SAT problem considers clauses with exactly three
literals, but for further proofs we prefer to use the above variant.  


\begin{figure}[h]
\psfrag{G}[c][c][1]{$G$}
\psfrag{Q}[c][c][1]{$Q$}
\includegraphics[width=\linewidth]{./figures/3SAT}

\caption{Example of transformation from 3-SAT to {\sc projection}}
\label{3sat}
\end{figure}

Let $\mathcal F = C_1 \wedge \ldots \wedge C_k$ be an instance of
3-SAT. W.l.o.g. we suppose that each variable appears at most once in a
clause. Let us create four concept types for each variable $x$: {\tt x},
{\tt xf}, {\tt xt}  and {\tt xv}. We also create one relation type
{\tt C$_i$} for each clause $C_i$, and a relation type {\tt val}.  
Each concept type
{\tt xv} is greater than {\tt xt} and {\tt xf}, 
these are the only possible comparisons between distinct types.

We build the graph $G(\mathcal F)$ as follows: 
for every variable $x$
in $\mathcal F$, we have three concept nodes {\tt [x]}, {\tt [xt]} and
{\tt [xf]} in $G(\mathcal F)$ and two relation nodes typed {\tt val}
linking the first to the latter ones (intuitively, it means that the
variable $x$ can be valuated by {\tt true} or {\tt false}). Let us say
that the truth value {\tt true} (resp.  {\tt false}) is associated
with {\tt [xt]} (resp. {\tt [xf]}). 
Then for
every clause $C_i = (l_x \vee l_y \vee l_z)$ in $\mathcal F$ (where 
$l_x$, $l_y$ and $l_z$ are literals over variables $x$, $y$ and $z$), we add the 7
relation nodes typed {\tt C$_i$}, having as first argument  {\tt [xt]} or
{\tt [xf]}, as second argument {\tt [yt]} or {\tt [yf]}, and as third
argument {\tt [zt]} or {\tt [zf]}, that correspond to an evaluation of
the clause to true (more precisely, if we replace in the clause $C_i$
each positive (resp. negative) literal $l_j$, $1 \leq j \leq 3$, by
the truth value (resp. the negation of the truth value) associated
with the $jth$ neighbor of the relation node, $C_i$ is evaluated to
true). 

For clauses restricted to $(l_x \vee l_y)$ or $(l_x)$,
we proceed similarly, adding 3 binary relation nodes or one unary relation
node.
Note that having $k$-clauses, where
$k$ is a constant, is of primary importance to have a polynomial 
transformation,
since we obtain $2^k - 1$ relation nodes for each clause.

In the graph  $Q(\mathcal F)$, two
concept nodes {\tt [x]} and {\tt [xv]} are created for each variable
$x$  and a binary relation node {\tt (val)} links {\tt [x]} to {\tt [xv]}.
For each clause $C_i = (l_x  \vee l_y  \vee l_z)$, there is one relation {\tt (C$_i$)}
linked to {\tt [xv]}, {\tt [yv]} and {\tt [zv]} (and similarly for
clauses with one or two literals). $Q(\mathcal F)$ represents the question 
``is there a valuation of the variables such that all clauses
evaluate to {\tt true}?''

This transformation from the 3-SAT formula $(a \vee b \vee \neg c) \wedge
(\neg a \vee c \vee \neg d)$ is illustrated in Fig.~\ref{3sat}. In the
graph $G$, not all edges issued from the clauses  have been drawn, for
the sake of readability. It is immediate to check that, for a formula
$\mathcal F$, there is a valuation of its variables
such that each clause is evaluated to true if and only if $Q(\mathcal F)$
can be projected into $G(\mathcal F)$. \qed

\subsection{A Note on Redundancy}


Note that the subsumption relation induced by projection over SGs
is a quasi-order, but not an order: it is  a reflexive and transitive but not anti-symmetrical relation. Two SGs are said to be \emph{equivalent} if they project to
each other. A SG is said to be \emph{redundant} if it is 
equivalent to one of its strict subgraphs (i.e. a subgraph not equal
to $G$ itself), otherwise it is said to be
\emph{irredundant}. 

\begin{theorem}[\citeR{chein-mugnier:92}]
Redundancy checking is an
NP-complete problem. Each equivalence class
admits a unique (up to isomorphism) irredundant graph.
\end{theorem}

The \emph{irredundant form} of a SG $G$ is
an irredundant subgraph of $G$ equivalent to it (when $G$ is irredundant, this graph is $G$ itself, otherwise there may be several such subgraphs, but they are all isomorphic). 

\section{The $\mathcal{SG}$ Family: Extensions of Simple Conceptual Graphs}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

This section is devoted to an overview of the different models composing
the $\mathcal{SG}$ family. 
We will first outline the main motivations for our graph-based approach
of knowledge representation.

\subsection{Knowledge Representation and Reasonings with Graphs}

\paragraph{A modeling viewpoint}

From a modeling viewpoint, we see two
essential properties in the simple graph  model. The \emph{objects}, simple graphs, are easily
understandable by an end-user (a knowledge engineer or
even an expert). And \emph{reasonings} are easily understandable too, for two reasons:
projection is a graph matching operation, thus easily interpretable
and visualisable; and the same language is used at interface and
operational levels.


Although there is a gap between the theoretical foundations studied here and a
language usable in real applications, we would like to 
briefly mention two projects in which these properties have been exhibited. The first one is an experiment in
document retrieval done by \citeA{genest:00}.  In
this work, conceptual
graphs are used to define a language for indexing and querying documents.
%This language is based on a modified version of the simple graphs
%model, where in particular a value is associated to the
%projection operation,
%allowing to estimate the relevance of an indexation
%relative to a query. 
Concept types are taken from the thesaurus of RAMEAU
(about 400 000 types), a documentary language used in most french
public and universitary libraries. The experiment proved the
feasibility of the proposed system (w.r.t. computing time) and
an improved relevance w.r.t. to the existing system based upon
RAMEAU, mainly due to the use of semantic relations instead of
keywords only. One side effect was also to prove the interest of
simple graphs from a modeling viewpoint. Indeed, their graphical
properties  enabled to build an indexing/querying tool that was
considered as easy to use for the indexers. The users were master
humanities students, not aware from conceptual graphs neither from
RAMEAU; with the software and an indexing guide, they became
quickly able to build indexations, that were considered of high
quality by a senior librarian. 

The second project takes place in knowledge engineering \cite{bos-botella:97}. Its purpose
 is the construction of  tools for modeling and simulating human organizations, as emergency
procedures for instance. One main difficulty in knowledge engineering
 is to validate a modeling, i.e. to check that the expert reasoning is correctly modeled. 
This validation is usually done when the design is achieved, here  by simulating the
constructed modeling of the organization. At this final stage, modifications are very costly.
The key idea of the project is to overcome this difficulty by giving the expert the
 ability to use simulation inside the design cycle as a mean of
enriching and building his modeling. This implies that the chosen
 modeling language enables the expert to follow reasonings step by step, directly on his own
 modelization. It was decided to build such a language upon conceptual graphs. General conceptual graphs equivalent to FOL were not considered as
 good candidates because they are indeed  a diagrammatic system of
 logic that is not at the expert level. Instead, the language was
 grounded upon simple graphs and extensions (such as nestings of
 graphs) keeping  their
 readability. Operations mixed simple graph deduction
 (i.e. projection) with non
 declarative procedures. First experiments were conclusive.

\paragraph{A computational viewpoint} From a computational viewpoint,
we think that graph-based reasonings, benefitting from graph-theoretical results, 
can bring an interesting perspective
to logic programming. By example, the equivalence between SG projection
and deduction in FOL$(\wedge, \exists)$ can be seen as an alternative
version of the \emph{homomorphism theorem} \cite{Chandra-Merlin:77},
considered as fundamental for database queries optimization \cite{Abiteboul}.
Other results are obtained from constraint programming. The strong
equivalence between $\mathcal{SG}${\sc -deduction} and the {\sc Constraint Satisfaction Problem}
(see Sect.~\ref{related}, where the transformations used keep all solutions and preserve the
structure of the constraint network in the query) allows to translate the
results obtained in this latter community (by example, tractable cases based
upon the structure of the graph, \citeR{Gottlob-Leone-Scarcello:99}),
first to $\mathcal{SG}${\sc -deduction}, then to deduction in FOL$(\wedge, \exists)$.

The graph structure can also be used to develop efficient algorithms in more
general models of the $\mathcal{SG}$ family: in the model we call $\mathcal{SR}$ (see below),
\citeA{coulondre-salvat:98} use the graph-based notion of \emph{piece} to build
an efficient backward-chaining algorithm. To enhance the forward-chaining
algorithm used in the more general models of the $\mathcal{SG}$ family, \citeA{Baget:01}
expresses dependencies between rules and constraints in terms of a graph homomorphism.

\paragraph{}


Our aim is thus to build formal extensions of simple conceptual
graphs, keeping readability of objects as well as reasonings, and
preferably, logically founded.  The $\mathcal {SG}$ family is a first
step  in this direction. 


\subsection{An Overview of the $\mathcal{SG}$ Family}


Let us now informally present the $\mathcal{SG}$ family. 
The generic
problem to be solved, {\sc Deduction}, asks, given a knowledge base (KB)
$\mathcal K$ and a simple graph $Q$, whether $Q$ can be deduced from
$\mathcal K$.
According to the kinds of objects composing $\mathcal K$, one obtains the
different members of the family. In the
basic  model $\mathcal{SG}$, $\mathcal K$ is composed of a set
$\mathcal G$ of simple graphs
representing facts, and solving {\sc Deduction} amounts to check whether
there is a projection from $Q$ into $\mathcal G$.  
Rules and constraints are more complex objects based upon simple
graphs, and operations dealing with these objects are based upon
projection.   

 Throughout this section, we will use examples inspired from a
modelization of a  knowledge acquisition case study, called
{\sc Sysiphus-I}: it describes 
a resource allocation problem, where the aim is to assign offices to
persons of a research group while fulfilling some constraints
\cite{baget-genest-mugnier:99}.

\paragraph{Rules}

\begin{figure}[h]
\psfrag{R1}[c][c][1]{$R_1$}
\psfrag{R2}[c][c][1]{$R_2$}
\psfrag{R3}[c][c][1]{$R_3$}
\centerline{\includegraphics[width = 10cm]{./figures/rules}}

\caption{Rules}
\label{rules}
\end{figure}

A \emph{rule} expresses knowledge of form ``if $A$ is present then $B$ can be
added''. It is encoded into a simple graph provided with two colors,
the first color subgraph defining the hypothesis and the second color the conclusion. In drawings, we
represent the hypothesis by white nodes, and the conclusion by gray
ones. Figure \ref{rules} shows three rules. $R_1$ and $R_2$ represent knowledge about
the \emph{near} relation, supposed to be defined between offices only.
$R_1$ expresses that the
relation \emph{near} is symmetrical (``if an office $x$ is
\emph{near} an office $y$, then $y$ is \emph{near} $x$''), $R_2$ that `` if an
office $x$ \emph{adjoins} an office $y$ that \emph{adjoins} an office $z$ then $x$
is \emph{near} $z$''. The rule $R_3$ says that every researcher is member of
a project (``if there is a researcher $x$,
there is a project of which $x$ is a member'').  


\begin{figure}
\psfrag{G}[c][c][1]{$G$}
\psfrag{H}[c][c][1]{$H$}
\centerline{\includegraphics[width=\linewidth]{./figures/full}}

\caption{Rule applications}
\label{full}
\end{figure}


Rules are used to enrich facts: if the
hypothesis of a rule can be projected into a SG, then the rule
is applicable to this SG, and its conclusion can be added to the SG
according to  the projection. Notice that each projection of a same
rule to a SG defines a different way of applying this rule and is
likely to add new information to the SG. Consider for instance the SG $G$
of Fig. \ref{full}, which describes spatial information about offices, and
rules of Figure \ref{rules}. $R_1$ is applicable (since \emph{adjoin $\leq$
  near}), and so is $R_2$. Let us consider $R_2$. There are two ways of
applying this rule, depending
on whether its hypothesis is mapped onto the path {\tt
  [Office:$\#1$]->(adjoin)->[Office:$\#2$]->(adjoin)->[Office:$\#3$]} or onto the
path   {\tt [Office:$\#2$]->(adjoin)->[Office:
  $\#3$]->(adjoin)->[Office:$\#4$]}. In the
first case for instance, a relation node {\tt (near)} with predecessor  {\tt
  [Office:$\#1$]} and successor  {\tt [Office:$\#3$]} is added to the
  SG. Notice that in this example, applying  all rules in
  all possible ways as long as they add new information is a finite process (leading
  to the graph $H$ of Figure \ref{full}) but it is not true in general. 


When the KB is composed of a set of facts $\mathcal G$ and
a set of rules $\mathcal R$, the {\sc Deduction}
problem asks whether there is a sequence of rule applications
enriching the facts such that the goal $Q$ can be reached, i.e. leading
to a graph into which the SG $Q$ can be projected. E.g. consider the
fact $G$ of Figure \ref{full}, and let $Q$ be the SG
{\tt [Office:$\#4$]->(near)->[Office]} (``is $\#4$ near an office?''). $Q$
does not project into  $\mathcal G$, but applying the rules, one adds
the information {\tt [Office:$\#4$]->(near)->[Office:$\#3$]} (also {\tt
  [Office:$\#4$]->(near)->[Office:$\#2$]}), thus answering $Q$. 



\begin{figure}[h]
\psfrag{C1}[c][c][1]{$C_1$}
\psfrag{C2}[c][c][1]{$C_2$}
\centerline{\includegraphics[width = 11cm]{./figures/constraints}} 

\caption{Constraints}
\label{constraints}
\end{figure}


\paragraph{Constraints} A \emph{constraint} can be positive or negative,
expressing knowledge of form  ``if $A$ holds,
so must $B$'', or ``if $A$ holds, $B$ must not''.
It is also a bicolored simple graph: the first color defines the
condition part (or \emph{trigger}), and the second color the mandatory (or forbidden)
part. A SG $G$ satisfies a positive constraint $C$ if \emph{each}
projection from the condition part of $C$ into $G$ can be extended to
a projection of the whole $C$. And $G$ satisfies a negative constraint
if \emph{no} projection of the condition of $C$ into $G$ can be extended to a projection of
the whole $C$. 
Fig. \ref{constraints} shows two constraints.
The negative constraint $C_1$ expresses that ``two
persons working together should not share an office''. The SG $G$ of Fig \ref{simplegraphs} does not
satisfy this constraint because ``there is a researcher who works with 
researcher K'' (projection of the condition part of $C1$) ``and they share
office \#124'' (extension of the projection to a projection of the whole
$C1$). The positive constraint  $C_2$ expresses that
the office of a head of group must be near the offices of all
secretaries.


When the KB is composed of a set of facts $\mathcal{G}$ and a  set of constraints $\mathcal{C}$, the role
of constraints is to define the consistency of the base, i.e. of
$\mathcal{G}$. The base is said to be consistent if all constraints are
satisfied. Provided that the base is consistent, deduction is done as in
$\mathcal{SG}$. Even if they are both bicolored graphs, constraints
are not to be confused with rules. Consider for instance the bicolored
graph $R_3$ of Figure \ref{rules}: as a rule, it says that every
researcher is a member of a project. Take the fact  $\mathcal G$ = {\tt
  [Researcher:K.]} and the query $Q$={\tt
  [Researcher:K.]->(member)->[Project]} (``is K. member of a
project?''). If $Q$ is asked on $\mathcal K = (\mathcal G, \mathcal
R=\{R3\})$, the answer is ``yes''. Now, see  $R_3$ as a positive
constraint $C$. It says that every researcher must be a member of a
project. $\mathcal K = (\mathcal G, \mathcal C = \{C\})$ is inconsistent, thus nothing can be deduced from
it, including $Q$. The KB has to be repaired first.   

\paragraph{Combining rules and constraints}
Let us combine rules and constraints in reasoning.  We distinguish now
between two kinds of rules:  \emph{inference rules} 
%%of form ``if $A$ then add $B$'' 
and \emph{evolution rules}. 
%of form  ``if
%$A$ then try to add B''. 

%Rules seen above (Figure \ref{rules}) 
Inference rules represent
implicit knowledge that is made explicit by rule applications. 
This is the case for rules seen above (Figure \ref{rules}). Facts
and inference rules can be seen as describing a world, and applying a
rule modifies the explicit description of the world (the facts). Now,
if we consider a KB composed of a set of facts $\mathcal{G}$, a set of
inference rules $\mathcal{R}$, and a set of constraints $\mathcal{C}$, the notion of consistency 
has to take rules into
account. For instance,  add to the SGs $G$ and $H$ of Figure
\ref{full} the following information about office assignments: {\tt
  [HeadOfgroup:L.]->(in)->[Office:$\#1$]},  {\tt
  [Secretary:H.]->(in)->[Office:$\#2$]} and  {\tt
  [Secretary:P.]->(in)->[Office:$\#3$]}. Let $G'$ and $H'$ be the
(normal) SGs
obtained. 
Consider the world composed of the SG $G'$, inference rules $\{R_1, R_2\}$ of
  Figure \ref{rules}, and the positive constraint $C_2$ of Figure
  \ref{constraints}.   The
SG $G'$ alone does not satisfy the constraint $C2$ (because ``the head of group L. is in office $\#1$,
and the secretary P. is in office $\#3$'', but it does not hold that
``$\#1$ is near  $\#3$''). But after a certain
number of rule applications, it does. Thus the KB is said to be
consistent. In this case it is easy to define and check consistency because the
world description can be completely explicited by a finite SG (the
graph $H'$,  said to be {\em full} w.r.t. $\mathcal R$), thus it
suffices to check that this graph is consistent. In general case, consistency relies on whether each
``constraint violation'' can be repaired by rule applications, as
will be formally defined later. As with simpler worlds described by
facts only, deduction is not  possible on inconsistent knowledge bases. 

\begin{figure}[h]
\centerline{\includegraphics[width = 6cm]{./figures/evolution}} 

\caption{A rule}
\label{evolution}
\end{figure}

Evolution rules represent possible actions leading from one world to another
one. E.g. consider the colored graph of Figure \ref{evolution}. As an inference
rule, it would allow to deduce that all persons are in all offices. As an
evolution rule, it says that ``when there are a person and an office, a possible action
is to assign this office to that person''.
%obey to another reasoning schema. They do not
%represent knowledge about a world but possible actions, or
%transitions, leading from one world to another one. Note that these
%actions  are very particular since they only add positive information.
%E.g. consider the colored graph of Figure \ref{evolution}. Taken as an inference rule, it
%would say that all persons are in all offices.  Taken as
%an evolution rule, it says that ``when there are a person and an
%office, try to assign this office to that person''. 
Consider a KB composed of
a set of facts $\mathcal G$, a set of evolution rules  $\mathcal E$,
and a set of constraints  $\mathcal C$. Facts describe an initial
world; evolution  rules represent possible transitions from one world
to other worlds; constraints define
consistency of each world; a successor of a 
consistent world is obtained by an evolution rule application;
given a SG $Q$, the deduction problem asks  whether there
is a path of consistent worlds evolving from the initial one to a
world satisfying $Q$. 

%From a programming viewpoint, evolution rules
%allows one to develop a research tree and constraints cut this tree,
%thus leading to backtrack.


% Compared to this schema, the most general model of the $\mathcal{SG}$
%family adds to the KB a set of inference rules $\mathcal
%R$, representing implicit knowledge about worlds. 
% For instance, $R$ would allow to consider the SG of Fig. XX
% as the initial world instead of the SG full w.r.t. $\mathcal R$.  

The most general model of the $\mathcal{SG}$ family considers both kinds
of rules, \emph{i.e.} a set $\mathcal R$ of inference rules, and a set
$\mathcal E$ of evolution rules.
In the particular case of the {\sc Sysiphus-I}  modelization,
$\mathcal G$ and $\mathcal R$ describe the initial information about
office locations, persons and the group organization. $\mathcal R$ also
encodes general knowledge (such as properties of the \emph{dif}
relation put between two concept nodes representing distinct
entities). $\mathcal C$
represents obligations and interdictions defining what acceptable
assignments are (including cardinality constraints such as ``a person
cannot be \emph{in} several  offices'' or ``a large office cannot
contain more than two persons'', using the \emph{dif} relation).  
$\mathcal E$ consists of one evolution rule 
whose result is to place a person into an office
(it could also be composed of several rules considering
specific preconditions before trying an assignment).  
The goal represents a situation where each person of the group has an
office. A solution to the problem is a world obtained from the initial
one by a sequence of office assignments, where each person has an
office, while satisfying the allocation constraints.

\subsection{The $\mathcal{SG}$ Family}

Let us now specify definitions and
notations concerning the $\mathcal{SG}$ family. 


\begin{definition}[colored SGs]
A \emph{colored simple graph} is a pair $K = (G, \rho)$ where $G$ is a SG and $\rho$ is a mapping from 
$V(G)$ into $\{0, 1\}$. The number associated to a node is called the \emph{color} of the node. We denote
by $K_{(i)}$ the subgraph of $G$ induced by $i$-colored nodes. The
subgraph $K_{(0)}$ must form a SG (i.e. the neighbors of a relation
node of $K_{(0)}$ must also belong to $K_{(0)}$).
\end{definition}

The latter condition ($K_{(0)}$ must form a SG) is necessary as
soon as we consider rules as colored SGs: should a rule not satisfy this
condition, its application on a SG could generate a graph that is not
a SG.


A KB is denoted by 
$\mathcal K = (\mathcal G, \mathcal R, \mathcal E, \mathcal C)$,
where $\mathcal G$ is a set of simple graphs representing facts, 
$\mathcal R$, $\mathcal E$ and $\mathcal C$ are three sets of
colored simple graphs respectively representing \emph{inference rules},
\emph{evolution rules}, and \emph{constraints} 
(positive ones in $\mathcal C^+$,
negative ones in $\mathcal C^-$).
Given a KB $\mathcal K$  and a goal $Q$, the \emph{deduction problem} asks whether $Q$ can be deduced from $\mathcal K$ (we note $Q \geq \mathcal
K$). If we impose some of the sets $\mathcal R$, $\mathcal E$ or $\mathcal
C$ to be empty, one obtains specific reasoning models.  
 Note that in the absence of constraints  ($\mathcal C = \emptyset$),
 inference and evolution rules have the same behavior, thus $\mathcal
 R$ and $\mathcal E$ can be confused. The 
$\mathcal {SG}$ family is then composed of the six following models.  

\begin{itemize}
\item the $\mathcal {SG}$ model for $\mathcal K$ = $(\mathcal
  G,~\emptyset,~\emptyset,~\emptyset)$
\item the $\mathcal {SR}$ model for $\mathcal K$ = $(\mathcal
  G,~\mathcal R,~\mathcal E,~\emptyset)$
\item the $\mathcal {SGC}$ model for $\mathcal K$ = $(\mathcal
  G,~\emptyset,~\emptyset,~\mathcal C)$
\item the $\mathcal {SRC}$ model for $\mathcal K$ = $(\mathcal
  G,~\mathcal R,~\emptyset,~\mathcal C)$
\item the $\mathcal {SEC}$ model for $\mathcal K$ = $(\mathcal
  G,~\emptyset,~\mathcal E,~\mathcal C)$
\item the $\mathcal {SREC}$ model for $\mathcal K$ = $(\mathcal
  G,~\mathcal R,~\mathcal E,~\mathcal C)$
\end{itemize}


Since a fact has the same semantics as a rule with
an empty hypothesis, the set $\mathcal G$  is used 
in models names only 
when both rule sets $\mathcal R$ and $\mathcal E$ are
empty. 
The hierarchy of these models is represented in
Fig.~\ref{sgfamilyhierarchy}. It highlights
the decidability properties and the complexity of the
associated deduction problem. Notice we divide non decidable problems
into \emph{semi-decidable} and \emph{truly undecidable} problems. 
In the
first case, an answer can be computed in finite time for all positive
instances but not for all negative ones. In the second case, there is no 
finite procedure, neither for all positive instances, nor for all negative
ones. 

%such the computation halts both for all positive instances
%and for all negative ones.


\begin{figure}[h]
\psfrag{SREC}[c][c][1]{\scriptsize$\mathcal{SREC}$}
\psfrag{SRC}[c][c][1]{\scriptsize$\mathcal{SRC}$}
\psfrag{SEC}[c][c][1]{\scriptsize$\mathcal{SEC}$}
\psfrag{SGC}[c][c][1]{\scriptsize$\mathcal{SGC}$}
\psfrag{SR}[c][c][1]{\scriptsize$\mathcal{SR}$}
\psfrag{SG}[c][c][1]{\scriptsize$\mathcal{SG}$}
\psfrag{S2P-complete}[c][c][1]{$\Pi_2^P$-complete}
\psfrag{NP-complete}[c][c][1]{NP-complete}
\psfrag{Semi-decidable}[c][c][1]{Semi-decidable}
\psfrag{Truly undecidable}[c][c][1]{Truly undecidable}
%\centerline{\pstexscale{hierarchy.pstex}{width}{\linewidth}}
\centerline{\includegraphics[width = \linewidth]{./figures/hierarchy}}
\caption{The $\mathcal{SG}$ family: models and complexity of the
  associated deduction problem}
\label{sgfamilyhierarchy}

\end{figure}


\section{SGs and Rules: the $\mathbf{\mathcal{SR}}$ Model}
\label{srmodel}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

A \emph{simple graph rule} (SG rule) embeds knowledge of form ``if $A$
then $B$''. The following definition as a colored SG is equivalent to the more traditional definition
of a rule as an object composed of two SGs related with coreference
links used by \citeA{gosh-wuwongse:95}, or  \citeA{salvat-mugnier:96}.

\subsection{Definitions and Notations}


\begin{definition}[SG Rules]

A \emph{simple graph rule} $R$ is a colored SG. $R_{(0)}$ is called its \emph{hypothesis}, and $R_{(1)}$ its 
\emph{conclusion}.
\end{definition}

%%\vspace*{-0.1cm}
 
Deduction depends on the notion of a \emph{rule application}: it is a graph
transformation based upon projection.


%%\vspace*{-0.6cm}

\begin{definition}[Application of a SG Rule]
Let $G$ be a SG, and $R$ be a rule.
$R$ is \emph{applicable} to $G$ if there exists a projection, say
$\pi$, from
 $R_{(0)}$ (the hypothesis of
$R$) into $G$. In that case, the result of the \emph{application 
of $R$ on $G$ according to $\pi$} is the SG  $G'$ obtained 
by making the disjoint union of $G$ and of a copy
of $R_{(1)}$ (the conclusion of $R$), then, for every edge $(r, i, c)$, where $c \in
R_{(0)}$ and $r \in R_{(1)}$, adding an edge with the same number between  $\pi(c)$ and the
copy of $r$. $G'$ is said to be an \emph{immediate $R$-derivation}
from $G$. 
% on remplace def. ci-dessous par ``useless''
% A rule application is \emph{redundant} if $G'$ is equivalent to $G$.
\end{definition}

%%\vspace*{-0.1cm}

% The normality problem of Sect.~\ref{sgmodel} still holds: two SGs may be equivalent
% w.r.t. $\Phi$, though a rule is applicable to only one of them. As a consequence, before checking
% if a rule is applicable to a SG, it must be put into its normal form. We say that a SG $G'$
% is an immediate $R$-derivation from a SG $G$ if $G'$ is the result of the application of the rule
% $R$ on $nf(G)$, following some possible projection of the hypothesis of $R$ on $nf(G)$.
% The graph $G$ presented in Fig.~\ref{rule} is an immediate $K$-derivation 
% from the graph $G'$ in Fig.~\ref{simplegraphs}.

%Having formally defined the mechanisms allowing to immediately derive an object into another one,
%we can now define, as usual in formal languages, 

A derivation is  a (possibly empty) sequence of rule applications:  

%from the graph $G'$ in Fig.~\ref{simplegraphs}.

%In that case, we note 
%$G' = \mb{apply}(R, \pi, G)$ 
%and say that $G'$ is an immediate $R$-derivation from $G$.
%The graph $G_1$ (resp. $G_2$) presented in Fig.~\ref{rule} is an immediate $K_1$-derivation (resp.  $K_2$-derivation)
%from the graph $G'$ in Fig.~\ref{simplegraphs}.

%%\vspace*{-0.1cm}

\begin{definition}[Derivation]
Let $\mathcal R$ be a set of rules, and $G$ be a SG. We call \emph{$\mathcal R$-derivation} from $G$
to $G'$ a sequence of SGs
$G = G_0, \dots, G_k = G'$ such that, for $1 \leq i \leq k$,
$G_i$ is an immediate $R$-derivation from $G_{i-1}$, where $R$ is a rule
in $\mathcal R$.
%1 \leq i \leq k \Rightarrow \exists R \in \mathcal R /$ $G_i$ is an immediate
%$R$-derivation from $G_{i-1}$.
\end{definition}

To deduce a SG $Q$, we must be able to derive a SG into which $Q$
can be projected. This notion is captured by the following definition:

\begin{definition}[$\mathbf{\mathcal{SR}}${\sc -deduction}] Let $\mathcal K = (\mathcal G, \mathcal R)$ be a KB
and let $Q$ be a SG. $Q$ can be deduced from $\mathcal K$ (notation $Q
\geq (\mathcal G, \mathcal R)$) if  there exists an $\mathcal R$-derivation from $\mathcal G$ to 
 a SG $H$ such that $Q \geq H$.
\end{definition}

\subsection{Logical Semantics}

The semantics $\Phi$ is extended to translate rules: given a rule
$R$, let $R_0$ and $R_1$ be the two SGs respectively corresponding to its hypothesis and its conclusion, i.e. $R_0 = R_{(0)}$
and $R_1$ is the SG obtained from  $R_{(1)}$
by adding the neighbors of the relation nodes of $R_{(1)}$ which
are concept nodes of $R_{(0)}$. 
Then $\Phi(R) = \forall
x_1~...~x_p~(\alpha(R_0) \rightarrow \exists
y_1~...~y_q~\alpha(R_1)$) where $\alpha(R_0)$ and $\alpha(R_1)$ are
the conjunctions of atoms associated with $R_0$ and  $R_1$, $x_1~...~x_p$ are the variables of
$\alpha(R_0)$ and $y_1~...~y_q$ are the variables of $\alpha(R_1)$ that do
not appear in  $\alpha(R_0)$. 
For instance, consider the rule $R_3$ in Fig.~\ref{rules}. Then 
\emph{$\Phi(R_3) = \forall x (\mbox{Researcher}(x) \rightarrow \exists y (\mbox{Project}(y) 
\wedge \mbox{member}(x, y)))$}.
Should we interpret the colored graph $C_1$ in Fig.~\ref{constraints} as a rule,
its formula
would be \emph{$\Phi(C_1)= \forall x \forall y ((\mbox{Person}(x) \wedge
\mbox{Person}(y) \wedge \mbox{works-with}(x,y))
\rightarrow \exists z (\mbox{Office}(z) \wedge \mbox{in}(x,z) \wedge \mbox{in}(y,z)))$}. Notice, unlike in 
clauses, variables proper to the conclusion are existentially quantified. 
%Actually, formulas associated 
%with rules correspond to the tuple-generating dependencies of databases \cite<TGD, >{coulondre-salvat:98}.

The following soundness and completeness
result is obtained:

\begin{theorem}[\citeR{salvat-mugnier:96,salvat:98}]\label{srlog}
Let $\mathcal K = (\mathcal G, \mathcal R)$ be a KB
and $Q$ be a SG. Then
$Q \geq (\mathcal G, \mathcal R)$ iff $\Phi(\mathcal
S), \Phi( \mathcal G), \Phi(\mathcal R) \vDash \Phi(Q)$. 
\end{theorem}

Notice this result assumes that graphs are given in normal form, and, if needed, put
into their normal form after each rule application.

%can be achieved only by considering the normal
%form of all the graphs in the involved $\mathcal R$-derivation. We
%will assume all along this paper that all graphs are in normal form,
%and \emph{they are put into their
%normal form after each rule application}.

\subsection{A Semi-decidable Problem}

\citeA{coulondre-salvat:98} proved that  $\mathcal{SR}${\sc
  -deduction} is semi-decidable with a reduction from 
the {\sc the implication problem for TGDs}. The reduction given
by \citeA{Baget:01} (from the {\sc Halting Problem of a Turing Machine})
points out that $\mathcal{SR}$ {\sc -deduction} is a computation model.
We give here 
another reduction, from the {\sc word problem in a semi-thue system},
  that we will use  as the starting point  in the proof of
  Prop.~\ref{xy}. This reduction is also interesting in itself since it proves that, even when rules are of the form 
``if \emph{path} $o \ x_1 \dots x_k \ e$ then \emph{path} $o \ y_1 \dots y_q \ e$'', $\mathcal{SR}${\sc -deduction}
remains semi-decidable. 

\begin{theorem}[\citeR{coulondre-salvat:98}]
\label{srcomp}
$\mathcal{SR}${\sc -deduction} is semi-decidable.
\end{theorem}

\noindent\emph{Proof:} First check that $\mathcal{SR}${\sc -deduction}
is not truly undecidable (\emph{i.e.} there exists an algorithm that
can decide in finite time if the answer to the problem is ``yes''): 
when $Q$ can be deduced from $\mathcal K$, a
breadth-first search of the tree of all derivations from  $\mathcal K$
provides the answer in finite time. 

We then prove that no algorithm is ensured to halt when the 
answer to the problem is ``no''.
Let us now show that
$\mathcal{SR}${\sc -deduction} is not decidable by building a
reduction from  the 
{\sc word problem in a semi-thue system} \cite{thue:14}. This problem
was proven semi-decidable by \citeA[reduction to his correspondence
Problem]{post:47}.


The {\sc word problem} can be expressed as: let $m$ and $m'$ be two
words, and $\Gamma = \{\gamma_1, \ldots, \gamma_k\}$ be a set of
rules, each rule $\gamma_i$ being a pair of words $(\alpha_i, \beta_i)$:
is there a derivation from $m$ to $m'$?
There is an immediate derivation from $m$ to $m'$  (we note
$m \rightarrow m'$) if, for some
$\gamma_j$, $m = m_1 \alpha_j m_2$ and $m' = m_1 \beta_j m_2$.
A \emph{derivation} from $m$ to $m'$ (we note $m \leadsto m'$)
is a sequence 
$m = m_0 \rightarrow m_1 \rightarrow \ldots \rightarrow m_p = m'$.

\begin{figure}[h]
\psfrag{x1}[c][c][1]{\scriptsize{$x_1$}}
\psfrag{xk}[c][c][1]{\scriptsize{$x_k$}}
\psfrag{y1}[c][c][1]{\scriptsize{$y_1$}}
\psfrag{yp}[c][c][1]{\scriptsize{$y_p$}}
\psfrag{z1}[c][c][1]{\scriptsize{$z_1$}}
\psfrag{zq}[c][c][1]{\scriptsize{$z_q$}}
\psfrag{T}[c][c][1]{\scriptsize{$\top$}}
\psfrag{G(m)}[c][c][1]{$\mathcal G(m)$}
\psfrag{U(g)}[c][c][1]{$\mathcal U(\gamma)$}

\includegraphics[width = \linewidth]{./figures/thue1}
\caption{Transformation from the {\sc word problem} into 
 $\mathcal{SR}${\sc -deduction}}
\label{thue1}
\end{figure}

This problem can easily be expressed in the $\mathcal{SR}$
model. One concept type {\tt x$_i$} is assigned to each letter
$x_i$. There are three other concept types: {\tt B} (for ``begin''),
{\tt E}  (for ``end'') and
$\top$ (for ``anything'').  $\top$ is the greatest concept type and all other
types are pairwise non-comparable. There is one relation type {\tt s}
(for ``has successor''). A word $m = x_1\ldots x_k$ is associated the graph $\mathcal G(m)$,
and to any rule $\gamma = (y_1\ldots y_p, \ z_1\ldots z_q)$ is
associated the graph rule $\mathcal U(\gamma)$, as represented in
Fig.~\ref{thue1}.
By a straightforward proof (a recurrence on the smallest derivation length), 
we obtain that to every path from the node typed $B$ to the node
typed $E$ (``begin'' to ``end'') in a graph $\mathcal R$-derived from $\mathcal G(m)$, corresponds a word (and not a subword)
derivable from $m$, and reciprocally.
It follows that  $m \leadsto m' \ \Leftrightarrow \ \mathcal G(m') \geq
(\mathcal G(m), \mathcal U(\Gamma))$.
 \qed



%%\vspace*{-0.2cm}

\section{SGs and Constraints: the $\mathbf{\mathcal{SGC}}$ Model}
\label{sgcmodel}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%\vspace*{-0.1cm}

Let us now introduce \emph{constraints}, which are used to validate
knowledge. A knowledge base will be validated if it satisfies every
constraint, and no deduction will be allowed unless the KB has been 
validated: in presence of constraints, deduction is defined only on a
\emph{consistent} knowledge base. 

\subsection{Definitions and Some Immediate Properties}

%%\vspace*{-0.1cm}

\begin{definition}[Constraints]
A \emph{positive} (resp.~\emph{negative}) \emph{constraint} $C$ is a colored 
SG. $C_{(0)}$ is called the \emph{trigger} of the constraint,
$C_{(1)}$ is called its \emph{obligation} (resp.~\emph{interdiction}).
A SG $G$ \emph{$\pi$-violates} a positive (resp.~negative) constraint $C$ if 
$\pi$ is a projection of the trigger of $C$ into the
irredundant form of $G$ (resp. into $G$)  that cannot be extended
(resp.~that can be extended) to a projection of $C$ as a whole. $G$ \emph{violates} $C$ if it $\pi$-violates $C$ for some
projection $\pi$. Otherwise, $G$ \emph{satisfies} $C$. 
\end{definition}
 
\begin{figure}[h]
\psfrag{C (positive)}[c][c][1]{$C$ (positive)}
\psfrag{G}[c][c][1]{$G$}
\psfrag{H}[c][c][1]{$H$}
\centerline{\includegraphics[width = 7cm]{./figures/irr}}
\caption{Redundancy and constraint violation}
\label{irr}
\end{figure}

We have to point out the importance of the irredundancy condition 
on the graph to be validated by positive constraints: should we forget this condition,
there may be two equivalent SGs, such that one satisfies a positive
constraint and the other does not. Fig. \ref{irr} shows an example of
such graphs. $G$ satisfies $C$, but  the equivalent (redundant) graph
$H$, obtained by making the disjoint union of $G$ and the
trigger of $C$, does not. To avoid different 
consistency values for equivalent graphs, we have chosen to define
positive  constraint 
satisfaction w.r.t. the
 irredundant form of a SG. This problem does not occur with negative
constraints. Indeed, let $G_1$ and $G_2$ be two equivalent graphs and
suppose $G_1$ $\pi$-violates a negative constraint $C$;  since
there exists a projection from $G_1$ into $G_2$, say  $\pi_1$, 
$\pi_1 \circ \pi$ is
a projection from $C$ to $G_2$, thus $G_2$ also violates $C$.

Two constraints $C_1$
and $C_2$ are said to be \emph{equivalent} if any graph that violates
$C_1$ also violates $C_2$ and conversely. Any negative constraint is equivalent to the
negative constraint obtained by coloring all its nodes by 1. Furthermore, negative constraints are indeed
a particular case of positive ones: consider the positive constraint $C'$ obtained from a negative 
constraint $C$
by coloring all nodes of $C$ by 0, then adding a concept node colored by 1, with type {\tt NotThere},
where {\tt NotThere} is incomparable with all other types and does not appear in any graph of the KB,
except in constraints.
Then a simple graph $G$ violates the constraint $C$ if and
only if it violates $C'$. 
Positive constraints strictly include
negative constraints, in the sense that the associated consistency
problems are not in the same complexity class (the proof follows 
from Th.~\ref{complexitySGC}).

\begin{property}
Unless $\Pi^P_2$ = co-NP, positive constraints are a strict generalization of negative ones.
\end{property} 

Since negative constraints are indeed a particular case of positive ones, we will now,
unless indicated otherwise, denote by ``a set of constraints'' a set of  positive
constraints: some of them can be equivalent to negative ones.

% The colored graph $K$ in Fig.~\ref{rule}, considered as a (positive) constraint, 
% can be understood as: \emph{if a person $x$ works with a person $y$, then $x$ must share all his offices with $y$}. The SG $G'$ of Fig.~\ref{simplegraphs} 
% violates this constraint $K$, since office \#117 is not shared.
% %), but fulfills $K_2$ (exhibiting the shared office \#123 is a sufficient proof).

\begin{definition}[Consistency/Deduction in $\mathbf{\mathcal{SGC}}$]
  A KB $\mathcal K = (\mathcal G, \mathcal C)$ 
 is \emph{consistent} if 
$\mathcal G$ satisfies all constraints of $\mathcal C$. 
Otherwise, it is said \emph{inconsistent}.
A SG $Q$ can be  \emph{deduced} from $\mathcal K$ if
$\mathcal K$ is consistent and $Q$ can be deduced from $\mathcal G$.
\end{definition}

Note that a SG $Q$ that violates a constraint of $\mathcal K$ may still
be deduced from $\mathcal K$. It does not
matter since $Q$ is a \emph{partial} representation of knowledge deducible
from  $\mathcal K$. 

\subsection{Relationships with Logics}

Deduction in $\mathcal{SGC}$ is essentially non monotonic. Adding information to $\mathcal G$
can trigger a new constraint, and thus can create a new violation: since nothing can be deduced
from an inconsistent knowledge base, previous deductions are no longer valid.
That is why for $\mathcal{SGC}$ and more general models (next sections), 
it is  impossible to obtain results of form ``$Q$ can be deduced
from the knowledge base $\mathcal{K}$ iff $\Phi(\mathcal K) \vDash \Phi(Q)$'' 
as it was the case for $\mathcal{SG}$ and $\mathcal{SR}$.

However, the notion of consistency can be translated into FOL. 
For negative
constraints, the correspondence is immediate, and relies on projection
soundness and completeness w.r.t. the semantics $\Phi$ (theorem \ref{acp}). Intuitively,
a SG $G$ violates a negative constraint $C^-$ if and only if the information represented
by $C^-$ is deducible from the information represented by $G$.

\begin{theorem}
A SG $G$ violates a negative constraint $C=(C',~\rho)$ iff $\Phi(\mathcal S),
\Phi(G) \vDash \Phi(C')$, where $C'$ is the SG underlying $C$ (and
$\Phi(C')$ is the logical formula associated to this SG).  
\end{theorem}

Consistency relative to positive constraints can be explained with FOL,
translating ``projection'' into  a notion of
``logical substitution'' \cite{chein-mugnier:92} between the formulas associated to graphs.
We call an \emph{S-substitution} from $\Phi(G)$ into $\Phi(H)$ a
substitution $\sigma$ of terms of $\Phi(G)$ by terms of $\Phi(H)$ 
such that constants of $\Phi(G)$ are kept invariant and, for any atom
$t(e_1,~...,e_k)$ of $\Phi(G)$, there is $t' \leq t$ such that 
$t'(\sigma(e_1),~...,\sigma(e_k))$ is an atom of  $\Phi(H)$. The following
property holds: 

\begin{property}
Every projection $\pi$ from $G$ to $H$ defines an
S-substitution $\sigma$ from $\Phi(G)$ to $\Phi(H)$. Assuming
that $H$ is in normal form, the converse also holds.
\end{property}

\noindent\emph{Proof:} Let $\pi$ be a projection from
$G$ to $H$. For each variable $x$ of $\Phi(G)$, 
let $c$ be the unique generic concept node such that
$x = \Phi(c)$, then  $\sigma(x)=\Phi(\pi(c))$.
Reciprocally, provided that $H$ is in normal form,
the application from concept nodes of
$G$ to concept nodes of $H$, mapping each $c$ to the node $c'$ such that 
$\sigma(\Phi(c)) = \Phi(c')$ is a projection from $G$ to
$H$. Note that, unless $H$ is in normal form, $c'$ is not uniquely defined when
$\Phi(c')$ is a constant. \qed

\begin{corollary}
A graph $G$ $\pi$-violates a constraint
$C$ iff the S-substitution $\sigma$ from $\Phi(C_{(0)})$ into $\Phi(G)$
associated with $\pi$ cannot be extended to an S-substitution from $\Phi(C)$ into $\Phi(G)$.
\end{corollary}

Another bridge can be built using rules.     
Indeed, a graph $G$ satisfies a positive constraint $C$ if and only
if, considering $C$ as a rule, all applications of $C$ on $G$
produce a graph equivalent to $G$. Or, more specifically: 

\begin{property}\label{p1}
A SG $G$  $\pi$-violates a positive constraint
$C$ iff, considering $C$ as a rule,
the application of $C$ on $G$ according to $\pi$ 
 produces a graph not equivalent to $G$.
\end{property}

\noindent \emph{Proof:} Let $C$ be a constraint and $G$ be a SG such that $G$ satisfies $C$.
If $\pi_0$ is a projection from $C_{(0)}$ into $G$, let us
consider the graph $G'$ obtained by the application of $C$ (considered now as a rule) 
on $G$ according to $\pi_0$. Let us now build the following
projection $\pi'$ from $G'$ into $G$: for each
node $v$, $\pi'(v) = v$ if $v$ belongs to $G$; otherwise, $v$ is a
copy of a node $w$ of $C_{(1)}$, and if $\pi$ is one of the projections
from $C$ into $G$ that extends $\pi_0$,  we have $\pi'(v) =
\pi(w)$. Then $\pi'$ is a projection of $G'$ into $G$, and since 
$G$ trivially projects into $G'$, they are thus equivalent. 

This proves the $\Leftarrow$ part of
property \ref{p1}. For the  $\Rightarrow$ part, we use the following
property, proved by \citeA{cogis-guinaldo:95}. In their property
(prop. 6 of their paper)
the SGs considered are connected graphs, but the proof holds for non connected graphs.

\begin{property} [\citeR{cogis-guinaldo:95}] \label{folding}
Let $G$ be a SG and irr$(G)$ be one of its equivalent irredundant subgraphs 
(if $G$ is not redundant 
then irr$(G) = G$). 
Then there exists a \emph{folding} from $G$ to irr$(G)$, i.e. a projection $f$ from $G$ into irr$(G)$, 
such that the restriction of $f$ to nodes of irr$(G)$ is the identity 
(for every node $x$ of irr$(G)$, $f(x) = x$). 
\end{property} 

Suppose now $G$ $\pi$-violates $C$. Since constraint violation is defined with respect to the 
irredundant form of a graph, we can consider, without loss of generality, that $G$ is
irredundant. We denote by $G'$ 
the graph obtained by the application of $C$ (again, considered now as a rule) on $G$ 
according to $\pi$. We prove that ``$G'$ equivalent to $G$'' leads to a contradiction.
 
If $G'$ is equivalent to $G$, then there exists a projection from $G'$
into $G$. And since $G$ is an irredundant subgraph of $G'$,
there exists a \emph{folding} $f$ from $G'$ into $G$ (property \ref{folding}). 
Consider now $\pi'$ the projection from $C$ to $G$ defined as follows: 
for any node $x$ of $C_{(0)}$, $\pi'(x)$ = $f(\pi(x))$, otherwise let $x'$ be the copy of 
$x$ in $G'$, we have $\pi'(x)$ = $f(x')$. Since for all
$x$ in $C_{(0)}$, $f(\pi(x)) = \pi(x)$, $\pi'$ extends $\pi$. This
contradicts the hypothesis ``$G$ $\pi$-violates $C$''.  Thus $G'$ is
not equivalent to $G$. \qed


\begin{property}\label{p2}
If a SG $G$ satisfies a positive constraint $C$, then any graph in a
$\{C\}$-derivation of $G$ is equivalent to $G$.
\end{property} 

\noindent \emph{Proof:} Let $G = G_0~,...,~G_k$ be a
$\{C\}$-derivation of $G$. From property \ref{p1}, each $G_i$, $1\leq i
\leq k$, is equivalent to $G_{i-1}$, thus by transitivity, is
equivalent to $G$. \qed

Using soundness and completeness of the $\mathcal{SR}$ deduction, and
properties \ref{p1} and \ref{p2}, one obtains the following relation with FOL deduction. 

\begin{theorem}\label{sgclog}
A SG $G$ violates a positive constraint  $C$ iff there exists a  SG
 $G'$ such that 
 $\Phi(\mathcal S), \Phi(G), \Phi(C)  \vDash  \Phi(G')$ and not  
 $\Phi(\mathcal S), \Phi(G) \vDash  \Phi(G')$, where $\Phi(C)$ is the
 translation of $C$ considered as a rule. 
\end{theorem}

This theorem can be reformulated in terms of abductive inference 
(using in fact indirect abduction, 
see, for example, \citeR{Konolige:96}).
Indeed, given a background theory $\Sigma = \Phi(\mathcal S), \Phi(G)$ and an observation
$O = \neg \Phi(C)$, $G$ violates $C$ iff there is an abductive explanation for $O$ of the form $\neg F$,
where $F$ is a formula belonging to FOL$(\wedge, \exists)$.

% \noindent \emph{Proof:} First part of the equivalence is a consequence
% of Prop.~\ref{p1}, second part comes from the converse of Lem.~\ref{p2}. \qed



% Let us  point out that constraints leads to an essentially non-monotonic form
% of reasonings: suppose a SG $Q$ that can be deduced from a KB.
% By adding information in the KB, we may create a constraint violation
% ;  in that case the KB becomes inconsistent and, by definition,  \emph{nothing} (and in particular $Q$)
% can be deduced from that base. That is why in models $\mathcal{SRC}$,
% $\mathcal{SEC}$ and
% $\mathcal{SREC}$ (next sections), it is impossible to obtain results of form ``$Q$ can be deduced
% from the knowledge base $\mathcal{K}$ iff $\Phi(\mathcal K) \vDash \Phi(Q)$'' as it was the case for $\mathcal{SG}$ and $\mathcal{SR}$.

\subsection{Computational Complexity}

The problem ``does a given graph satisfy a given constraint?'' is
co-NP-complete if this constraint is negative (since we must check the absence of projection), but becomes $\Pi_2^P$-complete for a
positive one ($\Pi_2^P$ is $\mbox{co-NP}^{\text{NP}}$).
%: cf. \cite{Papadimitriou:94}). 


\begin{theorem}[Complexity in $\mathbf{\mathcal{SGC}}$]
\label{complexitySGC}
  $\mathcal{SGC}${\sc -consistency}
 is $\Pi_2^P$-complete  (but is co-NP-com\-plete if all constraints are
 negative).
\end{theorem}


\noindent{\em Proof:} Without change of complexity, one can
consider that $\mathcal C$ is composed of only one positive constraint, say $C$. 
First recall that deciding whether a SG $G$ satisfies $C$ is done on
the irredundant form of $G$. We shall consider two ways of integrating this
fact in the complexity of $\mathcal{SGC}${\sc -consistency}. One way 
is to  assume that the irredundant form of $G$ is computed before the
consistency check. This can be achieved with a number of calls to a
projection oracle linear in the size of $G$
\cite{mugnier:95}. But, since we have then to solve a function problem (compute the irredundant form of $G$) instead of a decision problem (is $G$ irredundant?), we prefer to integrate irredundancy into
the consistency check: then, for a projection $\pi_0$ from the trigger of $C$ into $G$, the projection from $C$ to $G$ we look for does not necessarily extends $\pi_0$, but extends the composition of a projection from $G$ into one of its subgraphs (possibly equal to $G$ itself) and $\pi_0$. 

First, $\mathcal{SGC}${\sc -consistency} belongs to $\Pi_2^P$ since it 
 corresponds to the language 
$L = \{ x \ | \ \forall y_1 \ \exists y_2  \ R(x,~y_1,~y_2)\}$, where $x$ encodes an
instance $(G,C)$ of the problem and $(x,~y_1,~y_2) \in R$  iff $y_1$ encodes a projection  $\pi_0$ 
from $C_{(0)}$ into
$G$ and $y_2$ encodes a  projection $\pi_G$ from $G$ into one of its subgraphs and a projection $\pi$ from $C$ into $G$ s.t.  $\pi[C_{(0)}] =
\pi_G \circ \pi_0$. Note that if $G$ is in irredundant form, then $\pi_G$ is an automorphism. 

Now, let us consider the  problem $B_2^c$: given a boolean formula $E$, and a partition
$\{X_1,~X_2\}$ of its variables, is it true that for any truth
assignment for the variables in $X_1$ there
exists a  truth assignment for the variables in $X_2$ s.t. $E$ is
true? This problem is $\Pi_2^P$-complete, since its complementary $B_2$ is shown to 
be $\Sigma_2^P$-complete by \citeA{stockmeyer:77}. In order to build a polynomial
reduction to $\mathcal{SGC}${\sc -consistency}, we use a restriction
of this problem to $k$-CNFs, i.e. conjunctions of disjunctions with at most
$k$ literals per clause.  Let us call 3-$SAT_2^c$ the special case 
where $E$ is a 3-CNF, in other words  an instance of 3-SAT. Then 3-$SAT_2^c$ is also $\Pi_2^P$-complete. 
Indeed, in the same paper (Th.~4.1), \citeauthor{stockmeyer:77} shows that $B_2$ with $E$ restricted to 
a 3-disjunctive normal form (3-DNF) remains $\Sigma_2^P$-complete. Since the negation of a 3-DNF is a 3-CNF,
it follows that the complementary problem $B_2^c$ with $E$ restricted to a 3-CNF is $\Pi_2^P$-complete.

\begin{figure}[h]
\psfrag{G}[c][c][1]{$G$}
\psfrag{C}[c][c][1]{$C$}
\includegraphics[width=\linewidth]{./figures/PI2P}

\caption{Example of transformation from 3-$SAT_2^c$ to
  $\mathcal{SGC}${\sc-consistency}}
\label{pi2p}
\end{figure}

%We first show that the special case where $E$ is a 3-CNF (a conjunction of clauses, each clause 
%having at most three literals), or in other words is an instance of
%3-SAT, remains $\Pi_2^P$-complete (let us call this problem
%3-$SAT_2^c$): see lemma \ref{lem3SAT} below. 

%XXX 
%Plus besoin du lemme : Let us call 3-$SAT_2^c$ the special case where $E$ is a 3-CNF (a conjunction 
%of clauses, each clause having at most three literals), or in other words $E$ is an instance of 3-SAT. 
%3-$SAT_2^c$ is also $\Pi_2^P$-complete. 
%(Indeed, theorem 4.1. in cite{stockmeyer:77} shows in particular that $B_2$ with $E$ restricted to a 
%3-disjunctive normal form (3-DNF) remains $\Sigma_2^P$-complete; since the negation of a 3-DNF is a 3-CNF, 
%it follows that the complementary problem $B_2^c$ with $E$ restricted to a 3-CNF is $\Pi_2^P$-complete).
%XXX

Let us now reduce 3-$SAT_2^c$ to
$\mathcal{SGC}${\sc -consistency}. The transformation used is very similar
to the one from 3-SAT to $\mathcal{SG}${\sc -deduction} (proof of
theorem \ref{npc}), illustrated in Fig. \ref{3sat}. 
Let $E$ be an instance of 3-SAT.
Let  $G(E)$ and $Q(E)$ be the SGs obtained by the transformation 
described in the proof of Th.~\ref{npc}. The constraint
$C(E) = (Q(E),\rho(X_2))$ is obtained by adding a coloration to
$Q(E)$: all relation nodes obtained from 
clauses (nodes typed {\tt C$_{i}$}) and all nodes obtained from
variables in $X_2$ (concept nodes typed {\tt x} or {\tt xv} and
relation nodes typed {\tt val}) are colored by
1 (i.e. belong to the obligation). Once again, having clauses of
bounded size leads to a polynomial transformation. The simple graph $G$ and the
positive constraint $C$ presented in Fig.~\ref{pi2p} are obtained from
the 3-SAT formula $(a \vee b \vee \neg c) \wedge
(\neg a \vee c \vee \neg d)$ and the partition
 $X_1 = \{a, b\}, X_2 = \{c, d\}$.

%We first build a constraint
%$C$ from $E$. There is one concept node [t:*] for each
%variable of $E$ and one relation node with type $r_i$ for each clause
%$c_i$ of $E$. 
% The arity of a relation type $r_i$ is the number of literals of the
%clause $c_i$. And the $jth$ neighbor of a relation node is
%the concept node corresponding to the variable of the $jth$ literal of
%the associated clause. 
%$C_{(0)}$ is composed of all concept nodes coming from variables in
%$X_1$. 
%Now, $G$ is composed of two concept nodes with individual markers, $c_0$=[t:0]
%and $c_1$=[t:1], corresponding to the truth values {\bf false} and
%{\bf true} respectively, and, for each clause $c_i$ of $E$, 
%for each truth assignment of the  variables of $c_i$ giving the value
%true to $c_i$, there is one relation node of type $r_i$ ; 
% $jth$ neighbor of such a relation node is
%$c_0$ if the variable of the $jth$ literal of $c_i$ takes the value
%false, and $c_1$ otherwise. For
%instance, for a clause $c_1$ = $(\neg g \vee h)$, one has three relation
%nodes of type $c_1$, whose neighbors correspond to all truth
%assignments of $(g,~h)$ giving $c_1$ true, i.e. (0,0), (0,1) and (1,1).
%Note
%that, since clauses have at most three literals, the number of
%relation nodes of $G$ is linearly related to the number of clauses of
%$E$. Thus the transformation is polynomial in the size of $E$. 

Each truth assignment of the variables of $E$ s.t. $E$ is true
naturally gives a projection from $C$ into $G$, and reciprocally
(as indicated in the proof of Th.~\ref{npc}). Furthermore, any truth
assignment for the variables of $X_1$ naturally gives a projection from $C_{(0)}$ into $G$,
and reciprocally. Thus, the question ``is it true that for any truth
assignment for the variables in $X_1$ there
exists a  truth assignment for the variables in $X_2$ s.t. $E$ is
true?'' is equivalent to the question ``is it true that for
any projection $\pi_0$ from $C_{(0)}$ into $G$ there exists a projection
from $C$ into $G$ extending $\pi_0$?''. 
\qed

Note that this reduction is less straightforward than the one we proposed
in \cite{baget-mugnier:01}, but it will be used as a basis for the proof
of Th.~\ref{red3}.

%MNote that the reduction we proposed in \cite{baget-mugnier:01} is much
%simpler, but can be of no use to prove Th.~\ref{red3}.

%\begin{lemma}[Complexity of 3-$SAT_2^c$]  \label{lem3SAT}
%The problem  3-$SAT_2^c$ (``given a set of clauses $\mathcal C$, where each
%clause contains at most three literals,  and a partition
%$\{X_1,~X_2\}$ of its variables, is it true that for any truth
%assignment for the variables in $X_1$ there
%exists a  truth assignment for the variables in $X_2$ s.t. $\mathcal C$ is
%true?'') is $\Pi_2^P$-complete. 
%\end{lemma}

%\noindent{\em Proof:}  3-$SAT_2^c$ is a particular case of the problem
%$B_2^c$ (where the input is any boolean formula) known to be
%$\Pi_2^P$-complete. Let us show that it remains $\Pi_2^P$-complete by
%reducing $B_2^c$ to it. Let $E$ be any boolean formula, and
%$\{X_1,~X_2\}$ be a partition of its variables. To transform $E$ into an
%instance of 3-SAT, we use a polynomial 
%transformation $R$ from any boolean formula to an equivalent set of clauses,
%inspired from that  described
%in (\cite{Papadimitriou:94}, example 8.3). First, let us see $E$ as a boolean
%circuit (a directed graph) whose gates are the variables and
%the boolean connective $\wedge$, $\vee$, $\neg$, $\leftarrow$,
%$\leftrightarrow$. We call these gates ``input gates'' and
%``connective gates'' respectively. The size of the circuit is polynomially related
%to that of $E$. The set of variables of $R(E)$
%contains all variables of $E$, and in addition, for each connective gate
%$g$, there is a new variable (also denoted $g$). The clauses of $R(E)$
%are generated from gates. 
% If $g$ is a variable gate corresponding to
% $x$, we add the clauses $(\neg g \vee x)$ and $(g \vee x)$, i.e. the
% conjunctive normal form of $(g \Leftrightarrow x)$. If $g$ is a
% \bf{true} (resp.\bf{false}) gate, we add $(g)$  (resp. $(\neg g)$). 
%If $g$ is a NOT gate with predecessor gate $h$, we add  the clauses
%$(\neg g \vee \neg h)$ and  $(g \vee  h)$ equivalent to $(g
%\Leftrightarrow \neg h)$.  If $g$ is a OR gate with predecessors $h$
%and $h'$ we add the clauses $(\neg h \vee g)$, $(\neg h' \vee g)$ and
%$(h \vee h' \vee \neg g)$  
%equivalent to  $(g \Leftrightarrow (h \vee h'))$. For all binary
%connectives, we proceed  similarly, adding
%clauses equivalent to the formula $(g \Leftrightarrow (h~op~h'))$,
%where $op \in \{\wedge, \vee, \neg, \leftarrow,
%\leftrightarrow\}$. 
% Finally, if $g$ is also the output
%gate, we add the clause $(g)$. Note that the number of generated
%clauses is linearly related to the number of boolean connectives of
%$E$, thus $R$ is a polynomial transformation. And all clauses of  $R(E)$ have
%at most three literals.  

%The transformation $R$ fulfills the following properties. 
%{\bf (P1)} For any truth assignment $t$ for the variables of $E$, 
%there is a natural
%extension to a truth assignment $t'$ for the variables of $R(E)$
%(corresponding to connective gates) giving the
%same truth value to $E$ and $R(E)$. $t'$ is recursively
%defined from $t$ as follows: if $x$ is a variable associated to an input gate
%($x$ belongs to $E$), $t(x) = t'(x)$.  
% If $g$ is a NOT gate
%with one predecessor $h$, $t'(g) = \neg t'(h)$; if $g$ is a gate
%corresponding to a binary connective $op$, with predecessors $h_1$ and
%$h_2$, $t'(g) = t'(h_1)~op~t'(h_2)$. 
% {\bf (P2)} Reciprocally, for any truth assignment $t'$ for the variables of 
%$R(E)$, let $t$ be the restriction of $t'$ to
%the variables of $E$, then $t(E) = t'(R(E))$. These properties can be
%proved by induction on the depth of the boolean circuit associated
%with $E$.\footnote{Faudrait le faire. Sans oublier que si E = E1 op
%  E2, R(E1) par exemple  n'est pas egal a la restriction de R(E) a la partie
%  correspondant a E1. Il y a une clause (g1) en plus, ou g1 est la
%  porte de sortie du cricuit associé a E1. mais ca n'est pas genant.}  

%To obtain an instance of  3-$SAT_2^c$ it
%remains to define a partition $\{X'_1,~X'_2\}$ of the variables of
%$R(E)$. Let $X'_1$ be equal to $X_1$ (thus $X'_2$ is the union of $X_2$
%and the new variables corresponding to connective gates). Now, suppose that for any  truth
%assignment  $t_1$ for the variables in $X_1$, there exists a  truth
%assignment  $t_2$ for the variables in $X_2$, such that $E$ is
%true. Such $t_1$ is also any  truth
%assignment  $t'_1$ for the variables in $X'_1$, since $X_1 = X'_1$. Let
%$t'_2$ be the truth assignment for the variables of $X'_2$  
%induced by
%the natural extension of $t_1$ and $t_2$ to $R(E)$ as defined in
%property (P1). 
%Following (P1), $t'_1$ and $t'_2$ give the value true to $R(E)$.  
%Reciprocally, suppose that for any  truth
%assignment  $t'_1$ for the variables in $X'_1$, there exists a  truth
%assignment  $t'_2$ for the variables in $X'_2$, such that $R(E)$ is
%true. $t'_1$ is also any assignment $t_1$ for the variables in $X_1$;
%let $t_2$
%be the restriction of  $t'_2$ to variables of $X_2$. Following (P2),
%$t_1$ and $t_2$ give the value true to $R(E)$.

%\qed


\begin{corollary}
Deduction in  $\mathcal{SGC}$ is
$\Pi_2^P$-complete. 
\end{corollary}


%\vspace*{-0.1cm}

\section{Rules and Constraints: $\mathcal{SEC/SRC/SREC}$}
\label{srcSEcmodel}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%\vspace*{-0.1cm}
In presence of constraints, the two kinds of rules, inference rules $\mathcal R$ and evolution rules $\mathcal E$, define two
alternative models. 

\subsection{Definitions and Notations}

In $\mathcal {SEC}$, $\mathcal G$ is seen as the initial
world, root of a potentially infinite tree of possible worlds, and
$\mathcal E$ describes the possible evolutions from one world to
others. The deduction problem asks whether there is \emph{a path of
consistent worlds from $\mathcal G$ to a world satisfying $Q$}. 

\begin{definition} [$\mathbf{\mathcal{SEC}}${\sc -deduction}] 
Let $\mathcal K = (\mathcal G, \mathcal E, \mathcal C)$ be a KB, and
let $Q$ be a SG. $Q$ can be deduced from $\mathcal K$ if there is
an $\mathcal E$-derivation $\mathcal G = G_0, \dots, G_k$ such that,
for $0 \leq i \leq k$, $(G_i, \mathcal C)$ is consistent and $Q$ can be
deduced from $G_k$. 
\end{definition}

In
$\mathcal{SRC}$, $\mathcal G$ provided with $\mathcal R$ is a finite
description of a potentially infinite world, that has to be
consistent. 
Applying a rule to
$\mathcal G$ can create inconsistency, but a further application of a
rule may restore consistency. Let us formalize this notion of
\emph{consistency restoration}. Suppose there is a $\pi$-violation of
a positive constraint $C$ in $\mathcal G$; this  violation $(C, \pi)$ is said to be \emph{$\mathcal R$-restorable} if there exist an $\mathcal R$-derivation
from $\mathcal G$ into a SG $H$ and a projection $\pi'$ from $H$ into irr$(H)$ 
such that the projection $\pi' \circ \pi$ of the trigger of $C$ into irr$(H)$ can be extended to
a projection of $C$ as a whole. The violation of a negative constraint
can never be restored. Note that the $\mathcal R$-restoration can create new violations,
that must themselves be proven $\mathcal R$-restorable. 

%In the $\mathcal {SRC}$ model, violations
%are \emph{local}, and all possible violations must be locally
%repaired for the% KB to be consistent. 

\begin{definition}[$\mathbf{\mathcal{SRC}}${\sc -consistency} 
and $\mathbf{\mathcal{SRC}}${\sc -deduction}]
  A KB $\mathcal K = (\mathcal G, \mathcal R, \mathcal C)$
 is \emph{consistent} if, for any SG $H$ that can be $\mathcal R$-derived from $\mathcal G$,
for every constraint $C \in \mathcal C$, for every $\pi$-violation of $C$ in $H$, $(C, \pi)$ is 
$\mathcal R$-restorable. A SG $Q$ can be deduced from $\mathcal K$ if $\mathcal K$ is consistent and 
$Q$ can be deduced from $(\mathcal G, \mathcal R)$.
\end{definition}


\begin{figure}[h]
\psfrag{A simple graph G}[c][c][1]{A simple graph $G$}
\psfrag{A colored SG K}[c][c][1]{A colored SG $K$}
\centerline{\includegraphics[scale = 0.8]{./figures/numbers}}

%%\vspace*{-0.1cm}

\caption{Consistency in $\mathcal{SEC/SRC}$}
%\caption{$G$ asserts existence of 0, $K$ can express some properties of $\nbN$}
\label{numbers}
\end{figure}


Consider for instance a KB containing the SG $G$ in Fig.~\ref{numbers}, expressing the existence of the
number 0, a constraint  and a rule, both represented by the
colored SG $K$. The
constraint asserts that \emph{for every integer $n$, there must be an
  integer $n'$, successor of $n$}. If the rule is an evolution rule, 
$G$ is seen as an inconsistent initial world (there is no successor of
0 in $G$) and nothing will be deduced from this KB. If the rule is an
inference rule, its application immediately repairs the
constraint violation, while creating a new integer, that has no
successor, thus a new violation. Finally, every constraint violation
could eventually be repaired by a rule application, and the KB should be proven 
consistent. 

Let us point out that the $\mathcal{SR}$ model is obtained from
$\mathcal{SRC}$ or $\mathcal{SEC}$ when $\mathcal{C}$ is empty, and 
$\mathcal{SGC}$ is obtained from $\mathcal{SRC}$
(resp.~$\mathcal{SEC}$) when $\mathcal{R}$ (resp.~$\mathcal{E}$) is
empty. 


The $\mathcal{SREC}$ model combines both derivation schemes of the 
$\mathcal{SRC}$ and $\mathcal{SEC}$ models.
Now, $\mathcal G$ describes an 
initial world,  inference rules of $\mathcal R$ complete the description of any world,
constraints of $\mathcal C$ evaluate the consistency of a world, evolution rules of $\mathcal E$
try to make a consistent world evolve into a new, consistent one. The deduction
problem asks whether $\mathcal G$ can evolve into a consistent world
satisfying the goal. 


%%\vspace*{-0.1cm}

\begin{definition}[$\mathbf{\mathcal{SREC}}${\sc -deduction}]
A SG $G'$ is an \emph{immediate $\mathcal{RE}$-evolution} from a SG $G$ if there exists an 
$\mathcal R$-derivation from
$G$ into $G''$  and an \emph{immediate} $\mathcal E$-derivation from
$G''$ into $G'$. An \emph{$\mathcal{RE}$-evolution} from a SG $G$ to a
SG $G'$ is a sequence of SGs $G = G_0, \dots, G_k = G'$ such that, for
$0 \leq i \leq k$, $(G_i, \mathcal R, \mathcal C)$ is
consistent and, for $1 \leq i \leq k$, $G_i$ is an immediate $\mathcal{RE}$-evolution from $G_{i-1}$.
Given a KB $\mathcal K = (\mathcal G, \mathcal R,$ $\mathcal E,
\mathcal C)$, a SG 
$Q$ can be \emph{deduced} from $\mathcal K$ if there is  an
$\mathcal{RE}$-evolution $\mathcal G = G_0, \dots, G_k$ such that 
 $Q$ can be deduced from $(G_k,  \mathcal R)$.

\end{definition}

When $\mathcal E = \emptyset$ (resp. $\mathcal R = \emptyset$), one
obtains the  $\mathcal{SRC}$ model (resp. $\mathcal{SEC}$ ).

\subsection{Consistency in $\mathcal{SRC}$ and Logics}

To translate $\mathcal{SRC}${\sc -deduction} in logics, a starting
point could be to extend the logical translation of $\mathcal{SGC}${\sc -consistency}
given in Th.~\ref{sgclog} to a translation of $\mathcal{SRC}${\sc -consistency}.
However, the following theorem points out the limitations of this approach.

\begin{theorem}\label{marchepas}
Let $\mathcal K = (\mathcal G, \mathcal R,  \mathcal C)$ be a KB. If there exists a SG 
 $G'$ such that 
 $\Phi(\mathcal S), \Phi(\mathcal G), \Phi(\mathcal R), \\ \Phi(\mathcal C)  \vDash  \Phi(G')$ and not  
 $\Phi(\mathcal S), \Phi(\mathcal G), \Phi(\mathcal R) \vDash  \Phi(G')$, where $\Phi(\mathcal C)$ is the
 translation of the constraints of $\mathcal C$ considered as rules, then $\mathcal K$ is
inconsistent. However, the converse is false in the general case.
\end{theorem}

\noindent{\em Proof:} We first prove the positive part of this theorem. If there exists such a graph $G'$,
then (Th.~\ref{srlog}) there is a $(\mathcal R \cup \mathcal C)$-derivation 
(considering the colored graphs of $\mathcal C$
as rules) $\mathcal G = G_0, \dots, G_k$ such that $G'$ projects to $G_k$. See that $G_k$ cannot be
deduced from $(\mathcal G, \mathcal R)$, otherwise $G'$ would also be deducible from  $(\mathcal G, \mathcal R)$.
Let us consider the first $G_i$ from this derivation that is not deducible
from $(\mathcal G, \mathcal R)$. Then $G_i$ is obtained from
$G_{i-1}$ (a graph $\mathcal R$-deducible from $\mathcal G$) by applying a rule $C_q \in \mathcal C$
following a projection $\pi$.
Since $G_{i-1}$ is deducible
from $(\mathcal G, \mathcal R)$, then there exists a graph $H$ $\mathcal R$-derivable from $\mathcal G$
such that $G_{i-1}$ projects into $H$. Let us call $\pi'$ such a projection, and consider the
projection $\pi'' = \pi' \circ \pi$ of the hypothesis/trigger of the rule/constraint $C_q$ into $H$. We now
have to prove that 1) $H$ $\pi''$-violates $C_q$, and 2) this violation is not $\mathcal R$-restorable.
Suppose 1) or 2) is false. Then there would exist a graph $H'$ $\mathcal R$-derived from $H$ such that
$\pi''$ can be extended to a projection $\Pi$ of $C_q$ as a whole in the irredundant form of $H'$.
This is absurd, since $\Pi$ is a projection of $G_i$ in a graph $\mathcal R$-derivable from $\mathcal G$.

The counterexample presented in Fig.~\ref{marchepasfig} is sufficient to prove the negative part of the theorem.

\begin{figure}[h]
\psfrag{A graph G}[c][c][1]{A graph $G$}
\psfrag{A positive constraint C}[c][c][1]{A positive constraint $C$}
\psfrag{A rule R}[c][c][1]{A rule $R$}
\centerline{\includegraphics[scale = 0.9]{./figures/celog}}

%%\vspace*{-0.1cm}

\caption{A counterexample to Th.~\ref{marchepas}}
%\caption{$G$ asserts existence of 0, $K$ can express some properties of $\nbN$}
\label{marchepasfig}
\end{figure}

It is immediate to check that every graph that can be $\{R, C\}$-derived from $G$
can also be $\{R\}$-derived from $G$. However, the projection of the trigger
of $C$ into the unique node of $G$ defines a violation of $C$ that will never be restored. 
\qed

\medskip

We will study in the next section (Th.~\ref{marchemieux}) 
a particular case of rules where the converse of Th.~\ref{marchepas}
is true.

\subsection{Undecidability of the Associated Deduction Problems}

\begin{theorem}[Complexity in $\mathbf{\mathcal{SEC/SRC}}$]
\label{CompSEC}
$\mathcal{SEC}${\sc -deduction} is semi-decidable. Both
$\mathcal{SRC}${\sc -consistency} and $\mathcal{SRC}${\sc -deduction}
are truly undecidable.
\end{theorem}

\noindent \emph{Proof:} $\mathcal{SEC}$ includes $\mathcal {SR}$ thus
$\mathcal{SEC}$-deduction is not decidable. 
 When $Q$ is deducible from $\mathcal K$, a breadth-first
search of the tree of all derivations from $\mathcal K$, each graph being
checked for consistency, ensures that $G_k$ is found in finite time. 
 For $\mathcal{SRC}$, we
show that checking consistency is truly undecidable. Let
$\mathcal K$ be a KB where $\mathcal C$ contains a positive constraint
$C^+$ and a negative constraint $C^-$, both with an empty
trigger. For proving consistency, one has to prove that $C^-
\not\geq (\mathcal G,\mathcal R)$, and the algorithm does not
 necessarily stop in this case
(from semi-decidability of deduction in $\mathcal{SR}$). The same holds for
the complementary problem (proving inconsistency) taking $C^+$ instead
of $C^-$, hence the undecidability. \qed  

\medskip

As a generalization of $\mathcal{SRC}$, deduction 
in $\mathcal{SREC}$ is truly undecidable. Next section studies a
decidable fragment of $\mathcal{SREC}$, which in
particular was sufficient for the {\sc Sysiphus-I} modelization.   

\section{Decidability and Complexity of some Particular Cases}
%%%%%%%%%%%%%%%%%%%%%%%%

A rule application may add redundant information to a graph. In
general, detecting redundancy is difficult (recall determining whether a
graph is redundant is 
an  NP-complete problem), but there are some trivial cases, which we will get rid of, since they may create artificially infinite derivations.
First, once a rule has been applied to a graph according to a given projection, it can be applied again to 
the resulting graph, according to the same projection, and this indefinitely. These further applications 
obviously produce redundant information. They are said to be \emph{useless}. 
Another case of trivial redundancy in a graph is that of \emph{twin} relation nodes, i.e. with exactly 
the same neighbors in the same order. Consider for instance a rule of kind ``if $r(x,~y)$ then $r(x,~y)$''. This rule 
can be applied indefinitely, even if useless applications are avoided,
but all applications create twin relation nodes.
In what follows, we consider that the construction of the graph resulting
from a rule application prevents the generation of twin relation
nodes, and that a
derivation does not comprise any useless rule application. 

%XXXX
%Revoir notions de closed : n'a pas de sens independamment d'une derivation
%XXXX

Given a set of rules $\mathcal R$ and an $\mathcal R$-derivation leading to a SG $ H$, 
$H$ is said to be \emph{closed} if no rules of $\mathcal R$ can be applied to $H$
in an original way,  i.e. all applications
of any rule of $\mathcal R$ on $H$ are useless. More formally, $H$ is closed w.r.t. 
$\mathcal R$ and  w.r.t. an $\mathcal R$-derivation 
$H_0 ~ \pi_1 ~... ~\pi_k  H_k= H$, where $H_i$ ($1 \leq i \leq k$) is the  graph obtained 
by the application of a rule of $\mathcal R$ on $ H_{i-1}$ 
according to the projection 
$\pi_i$, if for every rule $R$ of $\mathcal R$ , for every projection
$\pi$ from $R_{(0)}$ into $H$, 
there exists a projection $\pi_i$ from  $R_{(0)}$ to $H_{i-1}$ ($1 \leq i \leq k$), such that $\pi =\pi_i$.

Given a set of rules $\mathcal R$ and a graph $G$, if a closed graph is $\mathcal R$-derivable from $G$, then it is unique. Moreover, if this graph is derivable with $n$ rule applications, then $n$ is the maximal length of an $\mathcal R$-derivation, and all derivations of length $n$ lead to it.  
When it exists, we call it the \emph{closure} of $G$ w.r.t. $\mathcal
R$, which we note $G^\ast_\mathcal R$. 

%xxxxxxxxxxxxxxxAncienne versionxxxxxxxxxxxxx

%We
%note, when it exists,  $G^\ast_\mathcal R$
%(the closure of $G$ w.r.t. $\mathcal R$) the 
%graph derived from $G$ that is closed w.r.t. every rule in $\mathcal
%R$. Equivalently, $G^\ast_\mathcal R$ can be defined as the graph obtained by the shortest derivation that leads to a closed graph. 
%When it exists $G^\ast_\mathcal R$ is unique. 

%xxxxxxxxxxxRemarquexxxxxxxxxxxxxxxxx

Let us also define another notion, related to the fact that we are interested in irredundant graphs. 
In this perspective, let us say that an irredundant graph $H$ is \emph{full} w.r.t. a set of rules  
$\mathcal R$ if every graph that can be obtained by applying one of those rules
on $H$ is equivalent to $H$. 
Assuming that $G$ is an irredundant graph and that graphs obtained by a rule application are put into 
irredundant form, if a full graph can be derived from $G$ then it is unique. 

Informally, the notion of a closed graph translates the fact that nothing can be added that has not been 
already added, whereas the notion of a full graph says that nothing can be added that really adds 
new information to the graph. When the closure of a graph $G$ exists, then the irredundant form of this 
closure is exactly the full graph derivable from $G$. But note that when the
full graph exists, the closure does not necessarily exists (see proof of
Prop.~\ref{xy}). 

\subsection{Finite Expansion Sets}

The notion of a
full graph  being more general than the notion of a closure, we can
generalize the definition of finite expansion sets used in a previous
paper \cite{baget-mugnier:01}, and adopt the following one:



%xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

\begin{definition}[Finite expansion sets]
A set of rules $\mathcal R$ is called a \emph{finite expansion set} if, for every
SG $G$, there exists an $\mathcal R$-derivation $G \ldots G'$
such that irr$(G')$ is full w.r.t. $\mathcal R$. We denote by $G^{\mathcal R}$
this full graph.
\end{definition}

If $\mathcal R$ is a finite expansion set (f.e.s), 
deduction in $\mathcal{SR}$ 
becomes decidable (but it is not a \emph{necessary} condition for decidability).
Indeed, in order to determine whether a SG $Q$ is deducible from a KB
$(\mathcal{G}, \mathcal{R})$, it suffices to compute $\mathcal
G^\mathcal R$, then to check the existence of a projection from
$Q$ to $\mathcal G^\mathcal R$. Similarly, consistency checks in
$\mathcal{SRC}$ are done on  $\mathcal G^\mathcal R$.



\begin{property}[Finite expansion sets]
\label{fes}
Let $\mathcal K = (\mathcal G, \mathcal R, \mathcal C)$ be a KB where
$\mathcal R$ is a finite expansion set. Then
$\mathcal K$ is consistent iff $(\{\mathcal G^\mathcal R\}, \mathcal C)$ 
is consistent,
and a SG $Q$ can be deduced from $(\mathcal G, \mathcal R)$ iff $Q$ can be
deduced from $(\{\mathcal G^\mathcal R\})$. 
\end{property}

This property allows us to prove that the converse of Th.~\ref{marchepas} is true when $\mathcal R$ is
restricted to a finite expansion set.

\begin{theorem}\label{marchemieux}
Let $\mathcal K = (\mathcal G, \mathcal R, \mathcal C)$ be a KB, 
where $\mathcal R$ is a finite expansion set. Then $\mathcal K$ is inconsistent iff
there exists a SG 
 $G'$ such that 
 $\Phi(\mathcal S), \Phi(\mathcal G), \Phi(\mathcal R), \Phi(\mathcal C)$ $\vDash  \Phi(G')$ and not  
 $\Phi(\mathcal S), \Phi(\mathcal G), \Phi(\mathcal R) \vDash  \Phi(G')$, where $\Phi(\mathcal C)$ is the
 translation of the constraints of $\mathcal C$ considered as rules.
\end{theorem}

\noindent{{\em Proof:} $(\Leftarrow)$ holds as a particular case of Th.~\ref{marchepas}. Let us now prove
the $(\Rightarrow)$ part. Since $\mathcal K$ is inconsistent, the previous property asserts that
$(\{\mathcal G^\mathcal R\}, \mathcal C)$  is inconsistent. Th.~\ref{sgclog} ensures
that there
exists a graph $H$ such that 1) $\Phi(\mathcal S), \Phi(\mathcal G^\mathcal R), \Phi(\mathcal C) \vDash \Phi(H)$,
and 2) $\Phi(\mathcal S), \Phi(\mathcal G^\mathcal R) \not\vDash \Phi(H)$.
Since $\Phi(\mathcal S), \Phi(\mathcal G), \Phi(\mathcal R) \vDash \Phi(\mathcal G^\mathcal R)$ (Th.~\ref{srlog}),
we obtain $\Phi(\mathcal S), \Phi(\mathcal G), \Phi(\mathcal R), \Phi(\mathcal C) \vDash \Phi(H)$.
Let us now suppose that $\Phi(\mathcal S), \Phi(\mathcal G), \Phi(\mathcal R) \vDash \Phi(H)$, and prove
that it is absurd. In that case, there would be a graph $G'$ $\mathcal R$-derivable from $\mathcal G$
such that $H$ projects into $G'$ (Th.~\ref{srlog} again). And since 
$H \geq G' \geq \mathcal G^{\mathcal R}$,
we should have $\Phi(\mathcal S), \Phi(\mathcal G^{\mathcal R}) \vDash \Phi(H)$ (Th.~\ref{acp}): this is absurd. \qed

\medskip

More generally, one obtains the following decidability results, depending on whether $\mathcal R$, $\mathcal E$, or $\mathcal R \cup \mathcal E$ is a finite expansion set.

\begin{property}[Complexity with finite expansion rule sets]
$~$
\begin{itemize}
\item When $\mathcal R$ is a f.e.s, deduction in $\mathcal{SR}$ is decidable, consistency and deduction in $\mathcal{SRC}$ are decidable, deduction
in $\mathcal{SREC}$ is semi-decidable.
\item  When $\mathcal E$ is a  f.e.s, deduction in $\mathcal{SEC}$ is
  decidable, but remains truly undecidable in $\mathcal{SREC}$.
\item When  $\mathcal R \cup \mathcal E$ is a f.e.s, deduction in $\mathcal{SREC}$ is decidable.
 \end{itemize}
 
\end{property}
%%\vspace*{-0.1cm}

\noindent{{\em Proof:} 
Suppose $\mathcal R$ is a f.e.s. Decidability of problems in
  $\mathcal{SR}$ and $\mathcal{SRC}$ follows from property
  \ref{fes}. In $\mathcal{SREC}$, when the answer is "yes", it can be obtained
  in finite time; we proceed as for $\mathcal{SEC}$ (see proof of
  theorem \ref{CompSEC}) but  consistency checks are done on the full graph
  instead of the graph itself. 

Now, suppose $\mathcal E$ is a f.e.s. $\mathcal G^{\mathcal E}$ exists, thus the derivation tree in $\mathcal{SEC}$ is
  finite, and consistency checks may only cut some parts of this tree.
Deduction in $\mathcal{SREC}$ remains undecidable because when
  $\mathcal E = \emptyset$, one obtains the $\mathcal{SRC}$ model, in which deduction is truly undecidable.    

Finally, if $\mathcal R \cup
\mathcal E$ is a f.e.s., $\mathcal G^{\mathcal R \cup
\mathcal E}$ exists, thus the derivation tree is finite, and consistency checks may only cut parts of this tree.
\qed 

Note that the condition ``$\mathcal R \cup \mathcal E$ is a 
finite expansion set'' is stronger than ``both $\mathcal R$ and 
$\mathcal E$ are finite expansion sets''. The following property justifies
this condition:

\begin{property}\label{xy}
If both $\mathcal R$ and $\mathcal E$ are finite expansion sets, then $\mathcal{SREC}${\sc -deduction}
is not necessarily decidable.
\end{property}

\noindent\emph{Proof:} We build a reduction from  {\sc word problem in
  a semi-thue system}  \cite{thue:14} to $\mathcal{SREC}${\sc -deduction}, where
the obtained rule sets $\mathcal R$ and $\mathcal E$ are both finite
expansion sets. This reduction relies on the one built for proving the
semi-decidability of $\mathcal{SR}$-{\sc deduction} (theorem \ref{srcomp}).  

Let us first present the two kind of finite expansion sets
used in this reduction. $\mathcal E$ is  a finite expansion set
since only relation nodes are present in the conclusion of rules:
$\mathcal E$ is indeed a particular case of range-restricted rules
(see Prop.~\ref{rr}). $\mathcal R$ is also a finite expansion set
since, for every rule in $\mathcal R$, the hypothesis is disconnected
from the conclusion (we call these rules \emph{disconnected}). Note this 
time that, though $\mathcal R$ is
trivially a f.e.s., the closure of a graph w.r.t. $\mathcal R$
does not necessarily exist.

Recall the  {\sc word problem} takes as input two words $m$ and $m'$ 
and a set of rules $\Gamma = \{\gamma_1, \ldots, \gamma_k\}$, 
each rule $\gamma_i$ being a pair of words $(\alpha_i,
\beta_i)$, and asks whether there is a derivation from $m$ to $m'$. 
There is an immediate derivation from $m$ to $m'$  (we note
$m \rightarrow m'$) if, for some
$\gamma_j$, $m = m_1 \alpha_j m_2$ and $m' = m_1 \beta_j m_2$.
A \emph{derivation} from $m$ to $m'$ (we note $m \leadsto m'$)
is a sequence 
$m = m_0 \rightarrow m_1 \rightarrow \ldots \rightarrow m_p = m'$.

\begin{figure}[h]
\psfrag{x1}[c][c][1]{\scriptsize{$x_1$}}
\psfrag{xk}[c][c][1]{\scriptsize{$x_k$}}
\psfrag{y1}[c][c][1]{\scriptsize{$y_1$}}
\psfrag{yp}[c][c][1]{\scriptsize{$y_p$}}
\psfrag{z1}[c][c][1]{\scriptsize{$z_1$}}
\psfrag{zq}[c][c][1]{\scriptsize{$z_q$}}
\psfrag{T}[c][c][1]{\scriptsize{$\top$}}
\psfrag{G(m)}[c][c][1]{$\mathcal G(m)$}
\psfrag{U(g)}[c][c][1]{$\mathcal U(\gamma)$}
\psfrag{R(g)}[c][c][1]{$\mathcal R(\gamma)$}
\psfrag{E(g)}[c][c][1]{$\mathcal E(\gamma)$}

\includegraphics[width = \linewidth]{./figures/thue}
\caption{Transformations from the {\sc word problem} into models of the $\mathcal{SG}$ family}
\label{thue}
\end{figure}

We have shown how this problem  can be expressed in the $\mathcal{SR}$
model: to a word $m = x_1\ldots x_k$ is associated the graph $\mathcal G(m)$,
and to any rule $\gamma = (y_1\ldots y_p, \ z_1\ldots z_q)$ is
associated the graph rule $\mathcal U(\gamma)$, as represented in
Fig.~\ref{thue} (where $\top$ is greater than all other concept types). 
Then $m \leadsto m'$ iff  $\mathcal G(m') \geq
(\mathcal G(m), \mathcal U(\Gamma))$ (see proof of Th.~\ref{srcomp}). 

Let us now split each obtained rule $\mathcal U(\gamma)$ into
one disconnected inference rule $\mathcal R(\gamma)$ 
and one range-restricted evolution rule $\mathcal E(\gamma)$. 
We distinguish in the hypothesis of  $\mathcal E(\gamma)$ two
subgraphs: the \emph{origin}, which corresponds to the hypothesis of
$\mathcal U(\gamma)$, and the \emph{destination}, which corresponds to
the conclusion of $\mathcal R(\gamma)$.  
It is easy
to check that one part of the above equivalence still holds:
$m \leadsto m' \ \Rightarrow \ \mathcal G(m') \geq
(\mathcal G(m), \mathcal R(\Gamma) \cup \mathcal E(\Gamma))$.
However, the converse is no longer valid: check by exemple
that, if $\Gamma = \{\gamma = (a, c)\}$, we have $\mathcal G(c) \geq
(\mathcal G(aba), \mathcal R(\Gamma) \cup \mathcal E(\Gamma))$
though $aba \not\leadsto c$ (apply  $\mathcal R(\gamma)$ once, then
two times  $\mathcal E(\gamma)$ using different nodes {\tt [a]} but
the same node {\tt [c]}). 

We thus need the notion of a \emph{good} application of 
a rule $\mathcal E(\gamma)$: it is such that the projection
of its destination part is a mapping to a subgraph
that was obtained by applying the rule $\mathcal R(\gamma)$,
and that was never used to project the destination part
of any rule of $\mathcal E(\Gamma)$, including $\mathcal E(\gamma)$
itself. Moreover, the origin and destination must be projected
into disjoint paths (i.e. a node of the origin cannot have the same
image has a node of the destination). If we restrict ourselves in some way to good applications of
rules of $\mathcal E(\Gamma)$, then we can verify that
$\mathcal G(m') \geq (\mathcal G(m), \mathcal U(\Gamma))$
iff $\mathcal G(m') \geq (\mathcal G(m), \mathcal R(\Gamma) \cup \mathcal E(\Gamma))$.

This restriction is obtained by using constraints, that will allow
every good application of a rule of $\mathcal E(\Gamma)$, and be
violated by the obtained graph otherwise. Let us note $\mathcal
R'(\Gamma)$ and  $\mathcal E'(\Gamma)$ the new sets of inference
rules and evolution rules.
The new  transformation is described in Fig.~\ref{thue2}. It allows to 
obtain the following result: $m \leadsto m' \ \Leftrightarrow \
\mathcal G'(m') \geq (\mathcal G'(m), \mathcal R'(\Gamma), \mathcal E'(\Gamma),
\{C_+, C_-\})$. The names of relation types $=$, $\in$ and $\rightarrow$  have been chosen to
give an intuitive idea of their role but they are just types as
others. A relation node $(\in)$ from a node {\tt [z$_j$]} to a node
{\tt [$\gamma_i$]} means that the letter $z_j$ has been obtained by
applying the rule $\gamma_i$. A relation  node $(\rightarrow)$  from
 {\tt [y$_k$]} to {\tt [$\gamma_i$]} means that the letter $y_k$ belongs to the subword
on which the rule $\gamma_i$ has been applied. $=$ is used to indicate
that two concept nodes have to be projected on the same node (in CG
terms, we would see it as a co-reference link). 
The evolution rule $\mathcal E'(\gamma_i)$, starting from a path
representing the subword $\alpha_i$ used to apply $\gamma_i$ and from the
representation of $\beta_i$ generated by  $\mathcal R'(\gamma_i)$,
produces the two relation nodes typed $s$ simulating the application
of  $\mathcal U(\gamma_i)$, thus $\gamma_i$, and the relation nodes
typed $\rightarrow$ which mark the representation of $\alpha_i$ as
used by an application of $\gamma_i$.  
The negative constraint $C_-$ prevents an application of  $\mathcal
E'(\gamma_i)$ in which two nodes of the 
origin and destination parts have the same image (a node necessarily
obtained by some application of the rule 
$\mathcal R'(\gamma_i)$); while the positive constraint
$C_+$ prevents such a subgraph to be used twice for applying $\mathcal
E'(\gamma_i)$ with different projections of its origin: it says that in this case, the two projections of
the origins must be the same. \qed

\begin{figure}[h]
\psfrag{x1}[c][c][1]{\scriptsize{$x_1$}}
\psfrag{xk}[c][c][1]{\scriptsize{$x_k$}}
\psfrag{y1}[c][c][1]{\scriptsize{$y_1$}}
\psfrag{yp}[c][c][1]{\scriptsize{$y_p$}}
\psfrag{z1}[c][c][1]{\scriptsize{$z_1$}}
\psfrag{zq}[c][c][1]{\scriptsize{$z_q$}}
\psfrag{T}[c][c][1]{\scriptsize{$\top$}}
\psfrag{ap}[c][c][1]{\scriptsize{$\in$}}
\psfrag{gi}[c][c][1]{\scriptsize{$\gamma_i$}}
\psfrag{>}[c][c][1]{\scriptsize{$\rightarrow$}}
\psfrag{G(m)}[c][c][1]{$\mathcal G'(m)$}
\psfrag{U(g)}[c][c][1]{$\mathcal U(\gamma)$}
\psfrag{R(g)}[c][c][1]{$\mathcal R'(\gamma_i)$}
\psfrag{E(g)}[c][c][1]{$\mathcal E'(\gamma_i)$}
\psfrag{C-}[c][c][1]{$C_-$}
\psfrag{C+}[c][c][1]{$C_+$}


\includegraphics[width = \linewidth]{./figures/thue2}
\caption{Reduction from the {\sc word problem} to $\mathcal{SREC}${\sc -deduction}, with $\mathcal E$ and $\mathcal R$ f.e.s.}
\label{thue2}
\end{figure}

%---FAUX
%Suppose that every set of rules $\mathcal R$ can be associated
%two distinct sets of rules  $\mathcal R_X$ and $\mathcal R_Y$, 
%such that these two
%sets are finite expansion sets and $\mathcal R$ is equivalent to 
%$\mathcal R_X \cup \mathcal R_Y$.
%Note that two sets of rules $\mathcal R$ and $\mathcal R'$ are 
%\emph{equivalent} if, 
%for every graphs $G$ and $G$,
%$Q \geq (G, \mathcal R) \ \Leftrightarrow \ Q \geq (G, \mathcal R')$. 
%Then  $\mathcal{SREC}${\sc -deduction},
%restricted to inference rules of $\mathcal R_X$, evolution rules of 
%$\mathcal R_Y$, and an empty set of
%constraints, is equivalent to $\mathcal{SR}${\sc -deduction}, 
%%where rules belong to 
%$\mathcal R_X \cup \mathcal R_Y$. According to our supposition, 
%this problem is equivalent to the
%whole $\mathcal{SR}${\sc -deduction} problem, and is thus semi-decidable. 
%To end this proof, we
%need to exhibit such a decomposition into finite expansion sets, 
%which is given by the following
%property: \qed

%\begin{property}\label{lem1}
%Any set of rules is equivalent to the union of two finite expansion sets.
%\end{property}

%\noindent\emph{Proof:} If $\mathcal R_X$ is a set of rules having only
%relation nodes in its conclusion, then, as a sub-case of range restricted
%rules, it is a finite expansion set (see Prop.~\ref{rr}). Then if
%$\mathcal R_Y$ is a set of rules such that the conclusion is disconnected
%from the hypothesis, it is also a finite expansion set: a derivation 
%of length at most $|\mathcal R_Y|$ is necessary to build the full graph
%w.r.t. $\mathcal R_Y$. Also note that the closure of a graph w.r.t. 
%$\mathcal R_Y$
%does not necessarily exist.

%Let us now prove that any set of rules $\mathcal R = \{R_1, \dots, R_k\}$ 
%is equivalent to a set
%of rules that belong to $\mathcal R_X \cup \mathcal R_Y$. For every rule 
%$R_i \in \mathcal R$, 
%having $n_i$ concept nodes in its conclusion, let us build the two rules 
%$R_i^X$ and $R_i^Y$ obtained 
%in the following way:
%\begin{itemize}
%\item $R_i^Y$ is obtained from $R_i$ by adding a $n_i$-ary relation node 
%typed {\tt R}$_i$ in its
%conclusion (where {\tt R}$_i$ is a new type, incompatible with any other 
%type present in the support),
%linked to all concept nodes of the conclusion. Then we delete all nodes 
%from the conclusion
%(they are relation nodes) that have a neighbor in the hypothesis.
%\item $R_i^X$ is obtained from $R_i^Y$ by assigning the color 0 to all 
%its nodes, then by replacing
%the relation nodes that were deleted. These nodes are this time colored by 1.
%\end{itemize}

%It is immediate to check that $\mathcal R_X = \{R_i^X\}_{1 \leq i \leq k}$
%and $\mathcal R_Y = \{R_i^Y\}_{1 \leq i \leq k}$ are two finite expansion sets
%as described above, and that $\mathcal R$ is equivalent to $\mathcal R_Y 
%\cup \mathcal R_X$. \qed

\subsection{Range Restricted Rules}

Let us now focus on the rules that were used to solve the {\sc Sisyphus-I}
problem. 
A bicolored graph (rule or constraint) is said to be \emph{range
  restricted} (r.r.)
if its second part (conclusion or obligation) does not comprise any generic 
concept node. We use this expression by analogy with the
so-called rules in Datalog, where all variables of
the head must appear in the body \cite{Abiteboul}. Such rules are also
called \emph{safe} in the literature. Consider for instance the rules of 
Fig.~\ref{rules}: $R_1$ and $R_2$ are range restricted, while $R_3$ is not. 


Also notice that a range restricted rule $R$ can be decomposed into an
equivalent set of rules  $\mathcal D(R)$ with exactly one node in conclusion
(either an individual concept node or a relation node). There is one
rule for each node of the conclusion of $R$:  for each
individual node $c$, one rule with
same hypothesis as $R$ and a conclusion restricted to $c$; for each
relation node $r$, one rule whose
hypothesis is the disjoint union of the hypothesis of $R$ and
of all individual concept nodes of the conclusion of $R$, and conclusion
is $r$, with same neighbors as in $R$. The logical interpretation of
such rules are (function free) range restricted Horn rules. If a SG
$Q$ is deducible from a set of r.r. rules $\mathcal R$, then it is
deducible from the set of their decompositions $\mathcal D(\mathcal R)$, and reciprocally. However, as soon as constraints are involved, this equivalence does not hold any more. 

\begin{property}\label{rr}
        A set of range restricted rules is a finite expansion set.
\end{property}

\noindent{{\em Proof:} 
 Since all graphs are put into
normal form, an individual marker appears at most once in a graph.
The number of individual nodes created by the set of rules is bounded
by $M = |\mathcal R| \times \mb{max}_{R \in \mathcal R}|R_{(1)}|$.
So the number of relation nodes created (no twin relation nodes are created) is bounded by
$N = \sum_{n = 1}^k P_n(|V_C(G)| + M)^n$, where $P_n$ is the number of relation types with a given arity $n$ appearing in a rule conclusion, and $k$ is the
greatest arity of such a relation type.
 So the closure of a graph can be obtained with a derivation of 
length $L \leq N+M$. We thus obtain $\mathcal G^\mathcal R$ in finite time.
\qed

Note that, contrary to general finite expansion sets, existence of the closure
and existence of the full graph are equivalent notions in the case of
range restricted rules. It follows from the proof of property \ref{rr} that the length of a
derivation from $\mathcal G$ to $\mathcal G^{\mathcal R}$ is in $\mathcal O(n^{k+1})$, where $n$ is the size of
$(\mathcal G, \mathcal R)$ and $k$ is the greatest arity of a relation type appearing in a rule  conclusion. 
This rough upper bound could be refined but it is sufficient to obtain the following property, which will be used throughout the proofs of  complexity results involving range restricted rules. 


\begin{property} \label{poly}
Under the assumption that the maximum arity of relation types is a
constant, given a range restricted set of rules $\mathcal R$, the
length of an $\mathcal R$-derivation from $\mathcal G$  is polynomially
related to the size of $(\mathcal G, \mathcal R)$. 
\end{property}

% XXXX Completement faux !! XXXX
% Another useful property is that a SG immediately derived from a irredundant SG by a range restricted rule can be put in irredundant form in time linear in the size if the rule. More generally:

% \begin{property} \label{irr}
% Given a irredundant SG $G$ and a range restricted set of rules $\mathcal R$, any graph $G_k$ $\mathcal R$-derived from $G$ can be put into irredundant form in time linear in its size (and, under the assumption of property \ref{poly}, the size of $G_k$ is polynomially related to the size of $(\mathcal G, \mathcal R)$.  
% \end{property}

% XXXXXXXX

In what follows, we assume that the arity of relation types is
bounded by a constant. 

\begin{theorem}[Complexity with range restricted rules]\label{red3}
When $\mathcal E$ and $\mathcal R$ are range restricted rules:
\begin{itemize}
\item  Deduction in $\mathcal{SR}$ is NP-complete.
\item Consistency and deduction in $\mathcal{SRC}$ are
  $\Pi_2^P$-complete.
\item Deduction in $\mathcal{SEC}$ and $\mathcal{SREC}$ is $\Sigma_3^P$-complete.

\end{itemize}
\end{theorem}

\noindent{{\em Proof:} The following results heavily rely on Prop.~\ref{poly}:
all derivations involved being of polynomial length, they admit a polynomial
certificate (the sequence of projections used to build the derivation).
%for any derivation from a graph $G$ into a graph $G'$, using r.r. rules,
%there is a graph $G''$ equivalent to $G'$ such that the derivation from
%$G$ into $G''$ admits a polynomial certificate: the polynomial number
%of projections used. 

%In this proof what we  call a derivation from $G$ to $G'$ is of form $G = G_0 ~ \pi_1 ~... ~\pi_k  G_k= G'$, where $ G_i$, $1 \leq i \leq k$, is the  graph obtained by the application of a rule to $ G_{i-1}$ following the projection $\pi_i$. It follows that, when $k$ is polynomial in the size of the input, one can polynomially check whether a given string encodes a derivation.

{\em NP-completeness of $\mathcal{SR}$-{\sc deduction}}. The problem belongs
to NP. Indeed, a polynomial certificate is
given by a derivation from $\mathcal G$ to a graph $G'$, followed by a projection from the goal to
$G'$.  
When $\mathcal R =
\emptyset$, one obtains $\mathcal{SG}$-{\sc deduction} (projection checking), thus the NP-completeness. 


\emph{$\Pi_2^P$-completeness of  $\mathcal{SRC}$-{\sc consistency} and 
 $\mathcal{SRC}$-{\sc deduction}}. Recall the consistency check involves the irredundant
  form of $\mathcal G$. In order to lighten the problem formulation, we assume here
  that all SGs are irredundant, but irredundancy can be integrated
  without increasing the consistency check complexity: see the proof of theorem
  \ref{complexitySGC}. 
 $\mathcal{SRC}${\sc -consistency} belongs to $\Pi_2^P$ since it corresponds
  to the language 
$L = \{ x\ | \  \forall y_1 \ \exists y_2 \ R(x,~y_1,~y_2)\}$, where $x$ encodes an
instance $(\mathcal G;\mathcal R;\mathcal C)$ of the problem and 
$(x,~y_1,~y_2) \in R$  iff
  $y_1=(d_1;\pi_0)$, where $d_1$ is a derivation from $\mathcal G$ to
  $G'$,
  $\pi_0$  is a projection from the trigger of a constraint $C_{i{(0)}}$ into
$G'$, $y_2=(d_2;\pi_1)$,  $d_2$ is a derivation from
  $G'$ to $G''$
  and $\pi_1$ is a projection  from $C_i$ into $G''$ s.t.  
$\pi_1$[$C_{i{(0)}}$] =
$\pi_0$. $R$ is polynomially decidable and polynomially balanced (since
  the lengths of $d_1$ and $d_2$ are polynomial
  in the size of the input).   
When   $\mathcal R =
\emptyset$, one obtains the problem $\mathcal{SGC}${\sc -consistency}, thus
  the $\Pi_2^P$-completeness. 
 Since $\mathcal{SRC}${\sc -deduction} consists in solving two
  independent problems, $\mathcal{SRC}${\sc -consistency}
  ($\Pi_2^P$-complete) and
  $\mathcal{SR}$-{\sc deduction} (NP-complete), and since NP is included in $\Pi_2^P$, $\mathcal{SRC}$-{\sc deduction} is also $\Pi_2^P$-complete. 


\emph{{$\Sigma_3^P$-completeness of  $\mathcal{SEC}${\sc -deduction}}}.  
As for $\mathcal{SRC}$ (see above), we assume that all SGs are irredundant. 
The question is ``are there a
derivation from $\mathcal G$ to a SG $G'$ and a projection from $Q$
into $G'$, such that for all $G_i$ of this derivation, for all constraint $C_j$, for all projection $\pi$
from $C_{j(0)}$ into $G_i$, there exists a projection $\pi'$
from $C_j$ into $G_i$ s.t. $\pi'[C_{j{(0)}}]=\pi$?''.  
  $R$ is polynomially decidable and
  polynomially balanced (since the size of the derivation from 
$\mathcal G$ to $G'$ is polynomially related to the size of the
input). Thus, $\mathcal{SEC}$-{\sc deduction} is in $\Sigma_3^P$.
In order to prove the completeness, we build a reduction from a special case of the problem $B_3$, where the formula is a 3-CNF (i.e. an instance of 3-SAT): given a formula $E$, which is a conjunction of clauses with at most 3 literals, and a partition $\{X_1, X_2, X_3\}$ of its variables, does there exist a truth assignment for the variables in $X_1$, such that for all truth assignment for the variables of $X_2$, there exists a truth assignment for the variables of $X_3$ such that $E$ is true? This problem is $\Sigma_3^P$-complete 
\cite[theorem 4.1]{stockmeyer:77}. Let us call it 3-SAT$_3$.

\begin{figure}[h]
\psfrag{G}[c][c][1]{$G$}
\psfrag{E}[c][c][1]{$E$}
\psfrag{Q}[c][c][1]{$Q$}
\psfrag{C+}[c][c][1]{$C_+$}
\includegraphics[width=\linewidth]{./figures/PI3P}
\caption{Example of transformation from 3-$SAT_3$ to $\mathcal{SEC}${\sc-deduction}}
\label{pi3p}
\end{figure}

The transformation we use is illustrated in Fig.~\ref{pi3p}. The 3-SAT 
formula used is again $(a \vee b \vee \neg c) \wedge
(\neg a \vee c \vee \neg d)$, and the partition is 
$X_1 = \{a, b\}, X_2 = \{c\},  X_3 = \{d\}$. The graph $G$ obtained is the
same as in the proof of Th.~\ref{complexitySGC}, Fig.~\ref{pi2p},
except that concept nodes {\tt [x]} corresponding to variables in $X_1$ are
not linked to the nodes {\tt [xt]} and {\tt [xf]} representing their
possible values.  

First check that in this initial world, no constraint is violated,
but the goal $Q$ cannot be satisfied. By applying once the evolution
rule $E$, we try some valuation of the variables in $X_1$ and obtain a 
world $G_1$, that contains an answer to $Q$. But this world has to
satisfy the positive constraint $C_+$, expressing that ``for every
valuation of the variables in $X_1 \cup X_2$, there must exist a valuation
of the variables in $X_3$ such that the formula evaluates to \emph{true}''.
If $G_1$ satisfies this constraint, it means that we have found (by applying
$E$) a valuation of the variables in $X_1$ such that for all valuations
of variables in  $X_1 \cup X_2$ (which can be simplified in ``for all 
valuations of variables in  $X_2$'', since there is only one such valuation
for $X_1$), there is a valuation of the variables in $X_3$ such that the
formula evaluates to \emph{true}. Then there is an answer \emph{yes} to
the 3-$SAT_3$ problem.
Conversely, suppose an answer \emph{no} to the $\mathcal{SEC}$ problem.
It means that for every world $G_1$ that can be obtained by applying
the rule $E$, the constraint $C_+$ is violated (otherwise $Q$ could
be projected into $G_1$ and the answer would be \emph{yes}). Thus
there is no assignment of the variables in $X_1$ satisfying
the constraint, \emph{i.e.} the answer to the 3-$SAT_3$ problem is
{\emph{no}.

\emph{$\Sigma_3^P$-completeness of  $\mathcal{SREC}$-{\sc deduction}}.
$\mathcal{SREC}${\sc -deduction} stays in the same class of complexity as 
$\mathcal{SEC}${\sc -deduction}. Indeed, the question is ``are there an
$\mathcal{RE}$-derivation from $\mathcal G$ to $G'$ and a projection from $Q$
to a SG $G'$, such that for all $G_i$ of this derivation either equal to 
$\mathcal G$ or obtained by an immediate
$\mathcal E$-derivation, for all $G'_i$ of this derivation derived from $G_i$ by an
$\mathcal R$-derivation, for all constraint $C_j$, for all projection $\pi$
from $C_{j(0)}$ to $G'_i$, there exists an $\mathcal R$-derivation from
$G'_i$ to a SG $G''_i$ and a projection $\pi'$
from $C_j$ to $G''_i$ s.t. $\pi'[C_{j(0)}]=\pi$?'' and the lengths of all
derivations are polynomial in the size of the input. 
When $\mathcal R = \emptyset$, one obtains $\mathcal{SEC}$\sc
-deduction}, thus the $\Sigma_3^P$ completeness.
\qed


Let us point out that, whereas in general case, deduction
is more difficult in $\mathcal{SRC}$ (truly undecidable) than in
$\mathcal{SEC}$ (semi-decidable), the converse holds for the
particular case of range-restricted rules. 

\subsection{Particular Constraints}


One may consider the case where not only rules but also constraints
are restricted. Let us first consider the meaningful
category of negative constraints. 



%\noindent{{\em Proof:} As noticed in section \ref{sgcmodel}, 
%a negative constraint is equivalent to a positive constraint 
%whose obligation is composed of
%one concept node of type {\tt NotThere}, where {\tt NotThere} is 
%incomparable with
%all other types and does not appear in any SG except $\mathcal
%C$. W.l.o.g. this node can be labeled by an individual marker (which,
%as {\tt NotThere}, appears only in $\mathcal C$), thus leading
%to a range-restricted constraint. \qed

%When constraints are range-restricted, consistency checking
%becomes easier. The reason is that, given a projection
%$\pi_0$ from a constraint trigger $C_{(0)}$ into a graph $G$, it can
%now be determined in polynomial time whether $\pi_0$ can be extended to a
%projection of $C$ into $G$ (since there is no choice for the images of
%individual concept nodes of $C_{(1)}$, and $C_{(1)}$ does not have any
%generic concept node).

\begin{theorem}[Complexity with negative constraints]
\label{cneg}
Without any assumption on the rules in $\mathcal E$ or $\mathcal R$,
but using only negative constraints:
\begin{itemize}
\item $\mathcal{SGC}${\sc -consistency} becomes co-NP-complete.
\item $\mathcal{SGC}${\sc -deduction} becomes DP-complete.
\item $\mathcal{SRC}${\sc -inconsistency} ($\mathcal{SRC}${\sc -consistency}
	co-problem) becomes semi-decidable.
\item $\mathcal{SEC}${\sc -deduction} remains semi-decidable.
\item $\mathcal{SRC}${\sc -deduction} and $\mathcal{SREC}${\sc -deduction} remain 
truly undecidable.
\end{itemize}
\end{theorem}

\noindent\emph{Proof:}

\emph{Co-NP-completeness of  $\mathcal{SGC}${\sc -consistency:}} from
NP-completeness of projection checking (th.~\ref{complexitySGC}).

\emph{DP-completeness of  $\mathcal{SGC}${\sc -deduction}:} this problem can be expressed
as ``is it true that $Q$ can be projected into $\mathcal G$ and that no
constraint of $\mathcal C$ can be projected into
$\mathcal G$?'' thus belongs to DP.  Now let us consider that $\mathcal C$
contains only one constraint. A reduction from 3-SAT to {\sc Projection} (see
f.i. the proof of th. \ref{npc}) provides a straightforward reduction from
{\sc SAT/UNSAT} to  $\mathcal{SGC}${\sc -deduction} (see f.i. 
\citeR{papadimitriou:94}), thus the
DP-completeness. 

\emph{Semi-decidability of $\mathcal{SRC}${\sc -inconsistency}:} To prove the 
inconsistency of a KB,
we must find some violation of a constraint that will never be restored.
But no violation of a negative constraint can ever be restored (further
rule applications can only add information, thus more possible projections, and cannot remove the culprit
one). So we only have to prove that one
constraint of $\mathcal C$ can be deduced from $(\mathcal G, \mathcal R)$: it is
a semi-decidable problem. \emph{Undecidability of} $\mathcal{SRC}${\sc-deduction}
follows: we must prove that $Q$ can be deduced from 
$(\mathcal G, \mathcal R)$, but that no constraint of $\mathcal C$ can.

The arguments proving semi-decidability of deduction in $\mathcal{SEC}$
and undecidability of deduction in $\mathcal{SREC}$ are the same as
the ones used in the proof of Th.~\ref{CompSEC}. \qed

\smallskip

The restriction to
negative constraints decreases complexity of problems in the
$\mathcal{SGC}$ model, but it  does not help much as soon as rules are
involved, since these problems remain undecidable. Combining range
restricted rules and negative constraints, we obtain more
interesting complexity results:

\begin{theorem}[Complexity with r.r. rules and negative constraints]
If only range-restricted rules and negative constraints are present
in the knowledge base:
\begin{itemize}
\item $\mathcal{SRC}${\sc -consistency} becomes co-NP-complete.
\item $\mathcal{SRC}${\sc -deduction} becomes DP-complete.
\item $\mathcal{SEC}${\sc -deduction} and $\mathcal{SREC}${\sc -deduction} become
$\Sigma_2^P$-complete.
\end{itemize}
\end{theorem}

\noindent\emph{Proof:} Inconsistency in $\mathcal{SRC}$ admits a polynomial certificate,
a derivation (of polynomial length) from $\mathcal G$ leading to a
graph into which a  constraint of $\mathcal C$ can
be projected, and this projection. Inconsistency is thus in NP, and completeness follows from the
particular case when $\mathcal R$ is empty. For deduction, we must prove that no constraint
can be deduced from $(\mathcal G, \mathcal R)$, but that $Q$ can. So the
problem is in DP. For completeness, remark that the problem is still complete
when $\mathcal R$ is empty (Th. \ref{cneg}).

To prove that $\mathcal{SEC}${\sc -deduction} with r.r. rules and negative constraints 
is $\Sigma_2^P$-complete, we will first
show that it belongs to $\Sigma_2^P$, then exhibit a
reduction from a $\Pi_2^P$-complete problem to its co-problem $\mathcal{SEC}${\sc -non-deduction}
(since co-$\Sigma_i^P$ =  $\Pi_i^P$).

$\mathcal{SEC}${\sc -deduction} corresponds to the language $L = \{x \ | \ \exists y_1
\forall y_2 \ R(x, y_1, y_2)\}$, where $x$ encodes an instance $(Q; (\mathcal G, \mathcal E, \mathcal C))$
of the problem, and $(x, y_1, y_2) \in R$ if $y_1$ encodes an
$\mathcal E$-derivation from $\mathcal G$ to $G'$ and a projection
from $Q$ to $G'$, and $y_2$ encodes a mapping from some constraint of
$\mathcal C$ to $G'$ that is not a 
projection (note that if $G'$ does not violate any constraint, then no graph in the
derivation from $\mathcal G$ to $G'$ does).

We exhibit now a reduction from the general $\mathcal{SGC}${\sc -consistency} problem
to $\mathcal{SEC}${\sc -non-deduction} with r.r. rules and negative constraints.
Let $(\mathcal G, \mathcal C =\{C\})$ be an instance of $\mathcal{SGC}${\sc -consistency} (w.l.o.g., we restrict
the problem to consider only one positive constraint). The transformation we consider builds
an instance of $\mathcal{SEC}${\sc -non-deduction} $(Q(C); (\mathcal G, \mathcal E(C), \mathcal C^-(C)))$
as follows. We call the \emph{frontier} of the positive constraint $C$
the set of nodes
in the trigger (\emph{i.e.} colored by 0) having at least one neighbor in the
obligation. The definition of colored graphs implies that frontier nodes are
concept nodes (their neighbors are thus relation nodes). Let us denote these 
frontier nodes by $1, \dots, k$. The evolution rule $\mathcal E(C)$ has for hypothesis
the trigger of $C$, and for conclusion a relation node typed {\tt found}, where
 {\tt found} is a new $k$-ary relation type incomparable with all
 other types. The $i^{th}$ neighbor of this
node is the concept node $i$. Check that $\mathcal E(C)$ is a range
restricted rule. The negative constraint $\mathcal C^-(C)$ is the subgraph of $C$
composed of its obligation ($C_{(1)})$ added with nodes of the
frontier and
the relation node typed {\tt found}, linked to the frontier nodes in the same way
as above. Finally, the SG $Q(C)$ is made of one relation node
typed {\tt found} and its neighbors frontier nodes. This transformation is illustrated
in Fig.~\ref{sigma3d}.

\begin{figure}
\psfrag{A generic positive constraint C}[c][c][1]{$C$}
\psfrag{The obtained evolution rule}[c][c][1]{$\mathcal E(C)$}
\psfrag{The obtained negative constraint}[c][c][1]{$\mathcal C^-(C)$}
\psfrag{The obtained query}[c][c][1]{$Q(C)$}
\psfrag{done}[c][c][1]{\scriptsize{found}}
\includegraphics[width=\linewidth]{./figures/sigma3}
\caption{Transformation from $\mathcal{SGC}${\sc -consistency} to a restricted $\mathcal{SEC}${\sc -non-deduction}}
\label{sigma3d}
\end{figure}

W.l.o.g. we can assume that $\mathcal G$ is irredundant: in that case, 
$\mathcal{SGC}${\sc -consistency} is still $\Pi_2^P$-complete (see that the transformation used
in the proof of Th.~\ref{complexitySGC} produces an irredundant graph $G$).
Now suppose that $(\mathcal G, C)$ is consistent: it means that either
the trigger of $C$ does not project
into $\mathcal G$, and in that case, the rule $\mathcal E(C)$ will never produce the needed {\tt (found)} node,
or every (existing) projection of the condition of $C$ into $\mathcal G =
irr(\mathcal G)$ can be extended to a projection of $C$
as a whole. So every application of $\mathcal E(C)$ produces a
violation of $\mathcal C^-(C)$. In both cases
$Q(C)$ cannot be deduced from the knowledge base. Conversely,
suppose that $\mathcal G$ $\pi$-violates 
$C$, then the application of  $\mathcal E(C)$ following $\pi$ produces a graph that does not violate
$\mathcal C^-(C)$, and we can deduce $Q(C)$. \qed

The above theorem shows a decrease in complexity when general
positive constraints are restricted to negative ones. $\mathcal{SGC}${\sc -consistency} 
falls from $\Pi_2^P$ to co-NP and, when also considering range restricted rules, $\mathcal{SRC}${\sc -consistency} 
falls from $\Pi_2^P$ to DP, and $\mathcal{SEC}${\sc -deduction} falls from $\Sigma_3^P$ to $\Sigma_2^P$.
It would be  interesting to exhibit particular cases of constraints,
more general than negative ones,
that
 make this complexity
fall into intermediary classes (by example DP and $\Delta_2^P$ for $\mathcal{SGC}${\sc -consistency}).
Some syntactic restrictions we defined for rules are good candidates: though a finite
expansion set of constraints has no sense, let us consider  \emph{range
restricted constraints}. Let us  also define \emph{disconnected
constraints} as constraints where the trigger and the obligation are
not connected; such constraints include the ``topological
constraints'' used in \cite{mineau-missaoui:97}. 


The following property highlights the relationships of these
particular cases with negative
constraints:

%XXX 

%Comment integrer la mise sous forme irredondante ?? 
%``calculer la forme irredondante de G'' est un ``function problem''
%appartenant a $FP^{NP}$ (on fait un nombre polynomial d'appels a un
%oracle de NP). Je parierais qu'il est  $FP^{NP[log n]}$-complet.

%XXX  
 
%\begin{theorem}
%[Complexity in  $\mathcal{SREC}$ with r.r. rules and constraints]
%When $\mathcal E$, $\mathcal R$ and $\mathcal C$ are range restricted:
%\begin{itemize}
%\item Assuming that $\mathcal G$ is irredundant, consistency in $\mathcal{SGC}$ is co-NP-complete and deduction
%  is DP-complete.
%\item Consistency and deduction in $\mathcal{SRC}$ are
 % DP-complete.
%\item Deduction in $\mathcal{SEC}$ is$\Sigma_2^P$-complete.
%\item Consistency and deduction in  $\mathcal{SREC}$ are
%$\Sigma_2^P$--complete.
%\end{itemize}
%\end{theorem}

%\begin{lemma}
%The problem ``given  $G$ a SG, $K$ a r.r. bicolored graph, and $\pi_0$
%a projection from  $C_{(O)}$ to $G$, can $\pi_0$ be extended to a
%projection from $C$ to $G$?'' is in P. 
%\end{lemma}

%\noindent{{\em Proof of the theorem:} Attention, le probleme de la verification de l'irredondance d'un graphe obtenu par une rrr appliquee a un graphe irredondant est un probleme (co)-NP-complet !!!!
%Si on ne trouve pas de solution satisfaisante pour traiter la mise sous forme irredondante, on peut se restreindre aux contraintes negatives, pour lesquelles% il n'y a pas de probleme de redondance. 
%\qed








\begin{property} Negative constraints are a particular case
  of both range-restricted constraints and disconnected constraints.
\end{property}



\noindent{{\em Proof:} As noticed in section \ref{sgcmodel}, 
a negative constraint is equivalent to a positive constraint 
whose obligation is composed of
one concept node of type {\tt NotThere}, where {\tt NotThere} is 
incomparable with
all other types and does not appear in any SG except in $\mathcal
C$ (it is thus a disconnected constraint). W.l.o.g. this node can be labeled by an individual marker (which,
as {\tt NotThere}, appears only in $\mathcal C$), thus leading
to a constraint which is both disconnected and  range-restricted. \qed

\begin{theorem}[Complexity with disconnected constraints]
When $\mathcal C$ contains only disconnected constraints:
\begin{itemize}
\item $\mathcal{SGC}${\sc -consistency} becomes co-DP-complete.
\item $\mathcal{SRC}${\sc -consistency} and  $\mathcal{SRC}${\sc -deduction} remain undecidable, but
$\mathcal{SRC}${\sc -consistency} becomes co-DP-complete when rules are
range-restricted.
\item $\mathcal{SEC}${\sc -deduction} remains semi-decidable, but becomes $\Sigma_2^P$-complete
when rules are range-restricted.
\item $\mathcal{SREC}${\sc -deduction} remains undecidable, but becomes $\Sigma_2^P$-complete
when rules are range-restricted.
\end{itemize}
\end{theorem}

\noindent\emph{Proof:} $\mathcal{SGC}${\sc -inconsistency} belongs to
DP, since we must prove that for one constraint
there is a projection of its trigger and no projection of its obligation.
Completeness is proved with a reduction from SAT/UNSAT (as in proof of Th. \ref{cneg}). 
$\mathcal{SGC}${\sc -consistency} is thus co-DP-complete.
%For $\mathcal{SGC}${\sc -deduction}, we have
%to solve \emph{independently} the $\mathcal{SGC}${\sc -consistency} (co-DP-complete) and the 
%$\mathcal{SG}${\sc -deduction} (NP-complete) problems, hence the result. 

Arguments for undecidability of $\mathcal{SRC}${\sc -consistency},
$\mathcal{SRC}${\sc -deduction} and $\mathcal{SREC}${\sc -de\-duction}, as well as semi-decidability
of $\mathcal{SEC}${\sc -deduction}, are the same as in the proof of Th.~\ref{CompSEC}: the constraints
we used were already disconnected.

When rules are range-restricted, $\mathcal{SRC}${\sc -inconsistency} belongs to DP:
we must prove that the trigger of the constraint can be deduced from $(\mathcal G, \mathcal R)$,
but not its obligation, and these problems belong respectively to NP and co-NP.
Completeness comes from the particular case where
$\mathcal R$ is empty.
$\mathcal{SRC}${\sc -consistency} is thus co-DP-complete. 
 %$\mathcal{SRC}${\sc -deduction} adds independently
%an NP-complete problem, thus it is also co-DP-complete.

$\mathcal{SEC}${\sc -deduction} belongs to $\Sigma_2^P$ when rules
involved are range-restricted. Though this property does not appear with
an immediate formulation of the
problem, it becomes obvious when the problem is stated as follows: 
``does there exist a sequence of
graphs $\mathcal G = G_0, ~\dots, ~G_p,~G_{p+1}$, where $\mathcal G = G_0, ~\dots,
~G_p$ is an $\mathcal E$-derivation and $G_{p+1}$ is the disjoint
union of $G_p$ and $C_{(1)}$,
a projection from $Q$ to $G_p$ and a projection
from $C_{(1)}$ to a SG $G_k$, $0\leq k \leq p+1$ such that for every graph $G_i,
0 \leq i < k$,\emph{($\ast$)} for every mapping $\pi$ of $C_{(0)}$ into
$G_i$, $\pi$ is not a projection ?''. Notice that no $G_i$ before
$G_k$ in such a sequence triggers the constraint ($C_{(0)}$ does not project into $G_i$)
and that all $G_i$, $i \geq k$, satisfy it (since $C_{(1)}$ projects to
$G_i$), thus all $G_i$ of the sequence are consistent. $G_{p+1}$ ensures that $C_{(1)}$ projects into at least one
graph of the sequence, which allows the above formulation of the
problem.
Completeness
follows from the particular case of negative constraints.

Proof for $\mathcal{SREC}${\sc -deduction} in the case of range restricted rules
is similar: in the expression of the problem above,
the derivation is now an $(\mathcal E \cup \mathcal R)$-derivation, the $G_i$ considered are
only the ones obtained after the application of a rule from $\mathcal
E$, and \emph{($\ast$)} ``for every mapping $\pi$ of $C_{(0)}$ into
$G_i$'' is replaced by ``for every graph that can be $\mathcal R$-derived from $G_i$''. \qed

Unfortunately, range-restricted constraints are trickier to study: intuitively, consistency
checking should become easier than with general constraints, but the role of irredundancy is still unclear. Though it is easy
to check that $\mathcal{SGC}${\sc -deduction} with range restricted constraints is at least
DP-hard (transformation from SAT/UNSAT) and we have proven (though it is not included
in this paper) that it
is in $\Delta_2^P$ (i.e. $P^{NP}$),
we did not manage to achieve an exact complexity result for this problem.

We did not either manage to assign a complexity class for the $\mathcal{SGC}^d${\sc -deduction}
and $\mathcal{SR}^{rr}\mathcal C^d${\sc -deduction} problems, though both problems trivially
belong to $\Delta_2$P.

Complexity results obtained in this paper are summarized in
table.~\ref{summary}. We also present in Fig.~\ref{complexity} 
a ``complexity map''  emphasizing the relationships between problems.   
In this figure, if $E$ denotes a set of bicolored graphs
(rules or constraints),
$E^{fes}$, $E^{rr}$, $E^{d}$ respectively denote its restriction to a
finite expansion set, range restricted elements, or disconnected
elements. $\mathcal C^-$ denotes a set of negative
constraints. All problems represented  are complete for their class. Edges are directed from bottom to
top. An edge from a problem P1 to a problem P2 means that P1 is
a particular case of P2. Moreover, in order that the map remains
readable, problems which are intermediate
between two problems P1 and P2 of the same
complexity class, do not appear in the figure. The complexity of such
problems can be obtained by ``classifying'' them in the hierarchy. For
instance, $\mathcal{SEC}${\sc -deduction} is more general than
$\mathcal{SR}${\sc -deduction} (which is obtained if $\mathcal C =
\emptyset$) and more specific than   $\mathcal{SR}^{fes}\mathcal{EC}${\sc
  -deduction} (which adds the set $R^{fes}$), and, since these
problems are both semi-decidable, so is  $\mathcal{SEC}${\sc
  -deduction}.     


%::::::::::::

\begin{table}
\begin{center}
\begin{scriptsize}
\begin{tabular}{|l|c|c|c|c|c|c|c|c|}
\hline
 & General& $\mathcal R$ fes & $\mathcal E$ fes & $\mathcal R \cup
\mathcal E$& $\mathcal R \& \mathcal E$  & $\mathcal C^-$ & $\mathcal R
\& \mathcal E$ & $\mathcal R \& \mathcal E$ \\
 & case & & &fes &r.r. & & r.r., $\mathcal C^-$ & r.r., $\mathcal C^d$
\\
\hline
$\mathcal{SG}${\sc -ded.} & NP-C& / &/ &/ &/ &/ &/ &/ \\
\hline
$\mathcal{SGC}${\sc -cons.} & $\Pi_2^P$-C &/ &/ &/ &/ &co-NP-C &co-NP-C
& co-DP-C\\
\hline
$\mathcal{SGC}${\sc -ded.} &$\Pi_2^P$-C &/ &/ &/ &/ &DP-C &DP-C & ? \\
\hline
$\mathcal{SR}${\sc -ded.} &semi-dec. &dec. &/ &dec. &NP-C &/ & NP-C&NP-C
\\
\hline
$\mathcal{SRC}${\sc -cons.} &undec. &dec. & / &dec. &$\Pi_2^P$-C
&co-semi-dec. &co-NP-C & co-DP-C\\
\hline
$\mathcal{SRC}${\sc -ded.} & undec. & dec. & / & dec. & $\Pi_2^P$-C
&undec. & DP-C & ?\\
\hline
$\mathcal{SEC}${\sc -ded.} & semi-dec. &/ &dec. &dec. &$\Sigma_3^P$-C
&semi-dec. & $\Sigma_2^P$-C &$\Sigma_2^P$-C \\
\hline
$\mathcal{SREC}${\sc -ded.} & undec. & semi-dec.& undec.&
dec.&$\Sigma_3^P$-C &undec. &$\Sigma_2^P$-C & $\Sigma_2^P$-C \\
\hline
\end{tabular}
\end{scriptsize}
\end{center}
\caption{Summary of Complexity Results}
\label{summary}
\end{table}

\begin{figure}
\psfrag{Polynomial hierarchy}[c][c][1]{\scriptsize{\sc Polynomial hierarchy}}
\psfrag{TrulyUndecidable}[c][c][1]{\fbox{\scriptsize{\sc Truly Undecidable}}}
\psfrag{SemiDecidable}[c][c][1]{\fbox{\scriptsize{\sc Semi-Decidable}}}
\psfrag{coSEMIDecidable}[c][c][1]{\fbox{\scriptsize{\sc co-Semi-Decidable}}}
\psfrag{Decidable}[c][c][1]{\fbox{\scriptsize{\sc Decidable}}}
\psfrag{S3P}[c][c][1]{\fbox{\scriptsize{$\Sigma_3$P}}}
\psfrag{P3P}[c][c][1]{\fbox{\scriptsize{$\Pi_3$P}}}
\psfrag{D3P}[c][c][1]{\fbox{\scriptsize{$\Delta_3$P}}}
\psfrag{S2P}[c][c][1]{\fbox{\scriptsize{$\Sigma_2$P}}}
\psfrag{P2P}[c][c][1]{\fbox{\scriptsize{$\Pi_2$P}}}
\psfrag{D2P}[c][c][1]{\fbox{\scriptsize{$\Delta_2$P}}}
\psfrag{DP}[c][c][1]{\fbox{\scriptsize{\sc DP}}}
\psfrag{CoDP}[c][c][1]{\fbox{\scriptsize{\sc co-DP}}}
\psfrag{coNP}[c][c][1]{\fbox{\scriptsize{\sc co-NP}}}
\psfrag{NP}[c][c][1]{\fbox{\scriptsize{\sc NP}}}
\psfrag{P}[c][c][1]{\fbox{\scriptsize{\sc P}}}

\psfrag{SREC-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SREC}$\sc{-deduction}}}
\psfrag{SRC-CONSISTENCY}[c][c][1]{\scriptsize{$\mathcal{SRC}$\sc{-consistency}}}
\psfrag{SRC--DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SRC}^-$\sc{-deduction}}}
\psfrag{SRC--CONSISTENCY}[c][c][1]{\scriptsize{$\mathcal{SRC}^-$\sc{-consistency}}}
\psfrag{SRCrr-CONSISTENCY}[c][c][1]{\scriptsize{$\mathcal{SRC}^{rr}$\sc{-consistency}}}
\psfrag{SRfeEC-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SR}^{fes}\mathcal{EC}$\sc{-deduction}}}
\psfrag{S(RE)feC-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{S(RE)}^{fes}\mathcal{C}$\sc{-deduction}}}
\psfrag{SRdErrCrr-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SR}^d\mathcal{E}^{rr}\mathcal{C}^{rr}$\sc{-deduction}}}
\psfrag{SRfe-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SR}^{fes}$\sc{-deduction}}}
\psfrag{SR-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SR}$\sc{-deduction}}}
\psfrag{SRrrErrC-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SR}^{rr}\mathcal{E}^{rr}\mathcal{C}$\sc{-deduction}}}
\psfrag{SRrrC-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SR}^{rr}\mathcal{C}$\sc{-deduction}}}
\psfrag{SGC-CONSISTENCY}[c][c][1]{\scriptsize{$\mathcal{SGC}$\sc{-consistency}}}
\psfrag{SGC-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SGC}$\sc{-deduction}}}
\psfrag{SGCd-CONSISTENCY}[c][c][1]{\scriptsize{$\mathcal{SGC}^d$\sc{-consistency}}}
\psfrag{SGCd-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SGC}^d$\sc{-deduction}}}

\psfrag{SErrC-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SE}^{rr}\mathcal{C}^d$\sc{-deduction}}}
\psfrag{SECrr-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SE}^{rr}\mathcal{C}$\sc{-deduction}}}
\psfrag{SRrr-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SR}^{rr}$\sc{-deduction}}}
\psfrag{SG-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SG}$\sc{-deduction}}}
\psfrag{SGa-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SG}^T$\sc{-deduction}}}
\psfrag{SRrrErrCd-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SR}^{rr}\mathcal{E}^{rr}\mathcal{C}^d$\sc{-deduction}}}
\psfrag{SErrC--DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SE}^{rr}\mathcal{C}^-$\sc{-deduction}}}
\psfrag{SGC--CONSISTENCY}[c][c][1]{\scriptsize{$\mathcal{SG}\mathcal{C}^-$\sc{-consistency}}}
\psfrag{SRrrC--CONSISTENCY}[c][c][1]{\scriptsize{$\mathcal{SR}^{rr}\mathcal{C}^-$\sc{-consistency}}}
\psfrag{SRfeC--CONSISTENCY}[c][c][1]{\scriptsize{$\mathcal{SR}^{fes}\mathcal{C}^-$\sc{-consistency}}}
\psfrag{SRrrCd-DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SR}^{rr}\mathcal{C}^d$\sc{-deduction}}}
\psfrag{SRrrCd-CONSISTENCY}[c][c][1]{\scriptsize{$\mathcal{SR}^{rr}\mathcal{C}^d$\sc{-consistency}}}
\psfrag{SRrrC--DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SR}^{rr}\mathcal{C}^-$\sc{-deduction}}}
\psfrag{SGC--DEDUCTION}[c][c][1]{\scriptsize{$\mathcal{SG}\mathcal{C}^-$\sc{-deduction}}}
\includegraphics[width=\linewidth]{./figures/complexity2}
\caption{Complexity Results: a Geography}
\label{complexity}
\end{figure}

\section{Related Works}\label{related}
%%%%%%%%%%%%%%%%%%%%



One interesting relationship from an algorithmic viewpoint is with the
CSP framework. Recall the input of a constraint satisfaction problem
({\sc CSP}) is a constraint network, composed of a set of variables, sets of possible values for the
variables (called their domains) and a set of constraints between the variables. The question
is whether there is a solution to the CSP, i.e. an
assignment of values to the variables that satisfies the constraints. 

The constraints involved in a classical {\sc CSP} are simpler than
ours. Actually, {\sc CSP}  corresponds to
the $\mathcal {SG}${\sc -deduction} (projection) problem. 

Several authors noticed the strong equivalence between
{\sc CSP} and {\sc labelled graph homomorphism}
(Given two labeled graphs
$G$ and $H$, is there a homomorphism from $G$ to $H$?). As far as we
know, the first paper on this subject was \cite{feder-vardi:93}. 
In \cite{mugnier:00} correspondences are detailed from {\sc Projection}
(Given two SGs $G$ and $H$ is there a projection from $G$ to $H$ ?)
to
{\sc CSP}, and reciprocally (developing the ones presented in \cite{Mugnier-Chein:96}). Let us outline the
ideas of the transformation from  {\sc CSP} to {\sc Projection}, called $C2P$.
 Consider a constraint network $P$.
$P$ is transformed into two SGs $G$ and $H$ as follows. $G$ translates the {\em structure} of $P$:
each concept node is generic and corresponds to a variable and each
relation node corresponds to a constraint (its $i$th neighbor is the concept node corresponding to the $i$th variable of
the constraint). $H$ represents the  {\em constraint
definitions}: there is one individual concept node for each value of
a variable domain, and one relation node for each tuple of compatible values.
Roughly said, there is a solution to $P$ if there is a mapping from
variables (concept nodes of $G$) to values (concept nodes of $H$) that satisfies the
constraints (maps relation nodes of $G$ onto relation nodes of $H$),
\emph{i.e.} a projection from $G$ to $H$.  The same result has been achieved
independently in the Attributed Graph Grammar formalism by \citeA{rudolf:98}.

One could also see {\sc CSP}  as a particular case of
$\mathcal{SGC}${\sc -consistency}: indeed, there is 
a projection from a SG $G$ into a SG $H$ if and only if
$H$ satisfies the positive constraint with an empty trigger
and $G$ as its obligation.
%%one positive constraint
%with an empty trigger ($G$ in the above transformation) and one SG
%($H$ in the above transformation). 

Now, in order to deal with incomplete knowledge \citeA{fargier-lang-schiex:96} 
\footnote{We thank Christian Bessi\`ere for this reference.}
extend the CSP framework to mixed-CSP. In a mixed-CSP
the set of variables is decomposed into controllable and
uncontrollable variables, say $X$ and $\Delta$. The {\sc MIXED-SAT} problem
asks whether a binary mixed-CSP is consistent, which can be reformulated as follows:  is it
true that every solution to the subnetwork induced by $\Delta$
can be extended to a solution of the whole network?  MIXED-SAT is shown to be $\Pi_2^P$-complete. This result provides us another
proof of $\Pi_2^P$-completeness for $\mathcal{SGC}$-consistency.
 Indeed, any mixed-CSP can be translated  
into an instance of $\mathcal{SGC}${\sc -consistency}. Using the $C2P$
reduction described above, the mixed-CSP is mapped
to SGs $G$ and $H$. $G$ is then provided with two colors, giving a
positive constraint $C$, whose trigger is the
subgraph corresponding to the subnetwork induced by $\Delta$. The
mixed-CSP is consistent if and only if $H$ satisfies $C$. 
Fig. \ref{mixedsat} illustrates this transformation. The constraint
network is composed of the two variable sets $X = \{x_1,~x_2\}$ and
$\Delta = \{l_1,~l_2\}$ and three constraints $C_1$, $C_2$ and
$C_3$. $x_1$ and $x_2$ have same domain  $\{1,~2,~3\}$ and $l_1$ and $l_2$
have same domain $\{a,~b\}$. The constraint definitions are
given in the figure. All concept types are supposed to
be incomparable. 


\begin{figure}[h]
\psfrag{L1  L2}[c][c][1]{\small{$l_1~~l_2$}}
\psfrag{L1 X1 X2}[c][c][1]{\small{$l_1~~x_1~~x_2$}}
\psfrag{L2  X2}[c][c][1]{\small{$l_2~~x_2$}}
\psfrag{tl}[c][c][1]{\small{$t_l$}}
\psfrag{tl : a}[c][c][1]{\scriptsize{$t_l : a$}} 
\psfrag{tl : b}[c][c][1]{\scriptsize{$t_l : b$}}
\psfrag{tx}[c][c][1]{\small{$t_x$}}
\psfrag{tx : 1}[c][c][1]{\scriptsize{$t_x : 1$}}
\psfrag{tx : 2}[c][c][1]{\scriptsize{$t_x : 2$}}
\psfrag{tx : 3}[c][c][1]{\scriptsize{$t_x : 3$}}
\psfrag{C0}[c][c][1]{\small{$C_0$}}
\psfrag{C1}[c][c][1]{\small{$C_1$}}
\psfrag{C2}[c][c][1]{\small{$C_2$}}
\centerline{\includegraphics[scale=0.8]{./figures/MixedSat}}

\caption{Transformation from MIXED-SAT to  $\mathcal{SGC}${\sc -consistency}}

\label{mixedsat}
\end{figure}


Let us relate our definitions to other definitions
of constraints found in the CG literature. 
Our constraints (let us call them SG-constraints) are a particular case of the minimal descriptive constraints defined in  \cite{dibie-haemmerle-loiseau:98}: a minimal descriptive constraint can be seen as a set of SG-constraints with the same trigger; its intuitive semantics is ``if $A$ holds so must $B_1$ or $B_2$ or ... $B_k$''. A SG satisfies a minimal descriptive constraint if it satisfies at least one element of the set. Note that the ``disjunction'' does not increase the complexity of the consistency check relative to SG-constraints. The proof of theorem \ref{complexitySGC} (complexity of $\mathcal {SGC}$ {\sc -consistency}) can be used to show that
consistency of minimal descriptive constraints is also  $\Pi_2^P$-complete. 
\citeA{dibie-haemmerle-loiseau:98} have pointed out that minimal 
descriptive constraints generalize most constraints found in the CG literature. Actually, these latter constraints are also particular cases of SG-constraints
(for instance, as already noticed, the topological constraints 
used by
\citeR{mineau-missaoui:97} are disconnected SG-constraints). Let us add
that, in these CG works, constraints are used to check consistency of
SGs solely and not of richer knowledge bases composed of rules (as in
$\mathcal {SRC}$) and they are not integrated into more complex reasonings (as in $\mathcal{SEC}$ or in $\mathcal{SREC}$). 


There should be other connections with works about verification of knowledge bases composed of logical rules (for instance Horn rules), namely with 
the works of \citeA{levy-rousset:96}, in which constraints are TGDs, thus have the same form than ours, but we did not find direct relationships between their framework and ours. 

As both models are rooted in semantic networks, comparing conceptual graphs and
descriptions logics is a problem that has often been issued.
\citeA{Baader-Molitor-Tobies:99} have identified a fragment of the $\mathcal{SG}$
model (where simple graphs are restricted to those having a tree-like structure, but
conjunctive types are allowed) with a language called $\mathcal{ELIRO}^1$: this equivalence
has led to a new tractability result in description logics. However, trying to identify larger fragments seems
to be a dead-end: as pointed out by \citeA{mugnier:00}, projection cannot handle
negation on primitive types. On the other hand, even the most expressive description
logics cannot express the whole FOL$(\wedge, \exists)$ fragment \cite{borgida:96}. Encoding 
some existing
description logics into models of the $\mathcal{SG}$ family is an interesting perspective,
that could allow one to identify new decidable classes for our models, add type
expressiveness to conceptual graphs, and may be cycles in the description of DLs
concepts.

%to identify new decidable classes for our models, add type expressiveness to conceptual
%graphs, and may be cycles in the description of DLs concepts.





%Another connection is with the notion of a tgd, tuple generating
%dependency, in databases. TGD and rules have the same logical semantics
% (see \cite{coulondre-salvat:98} for more details, the proximity of
%both notions was pointed out by M.C. Rousset). In
%\cite{coulondre-salvat:98}, it is shown that the problems
%TGD- in $\mathcal{SEC}$ and $\mathcal SR$-consistency are indeed equivalent. 



\section{Conclusion}
%%%%%%%%%%%%%%%%%%%%

We have proposed a family of models that can be seen as the basis of a
generic modeling framework. Main features of this framework are the
following: a clear distinction between different kinds of knowledge,
that fit well with intuitive categories, a uniform graph-based
language that keeps essential properties of the SG model, namely
readability of objects as well as reasonings. We guess this latter
point is  particularly important for the usability of any knowledge
based system. In our framework, all kinds of knowledge are graphs
easily interpreted, and reasonings can be graphically represented in a
natural manner using the graphs themselves, thus explained to the user
on its own modelization. 

Technical contributions, w.r.t. previous works on conceptual graphs,
can be summarized as follows: 
\begin{itemize}
        \item the representation of different kinds of knowledge as
          colored SGs: facts, inference rules, evolution rules
          and constraints. 
         \item the integration of constraints into a reasoning model;
           more or less similar notions of a constraint had already
           been introduced
        but were only used to check consistency of a simple graph (as in
        the $\mathcal{SGC}$ model). The complexity of consistency 
        checking was not known. 
        \item a systematic study of the obtained family of models with
          a complexity classification of associated
          consistency/deduction problems, including the study of
          particular cases of rules and constraints, which provide interesting complexity results. 
\end{itemize}

We also established links between consistency checking and FOL
deduction, translating the consistency/deduction problems in terms of FOL deduction. It should be noticed that the operational semantics of models combining rules and constraints, namely  $\mathcal {SREC}$,
$\mathcal {SRC}$ and $\mathcal {SEC}$, is easy to understand but we were not able to give a global logical semantics. Indeed, there
is an underlying non monotonic mechanism whose logical interpretation should require non standard logics. The definition of a logical semantics for these
models is thus  an open problem. 
 

\section*{Acknowledgments.} We are indebted to  Michel Chein and Genevi\`eve
Simonet for their careful reading of an earlier version of this work and helpful comments.
We also wish to thank Marie-Christine Rousset and Pierre Marquis, as well as anonymous
referees, for their interesting
suggestions and some corrections.


\bibliographystyle{theapa}
\bibliography{biblio}

\end{document}

