modifs main et arithmétiques

[cours-maths-dis.git] / logique / Resolution.tex

Que ce soit dans le cas dans le cas propositionnel 
(comme montré à la Sec.~\ref{sec:rob:prop}) ou dans le cas du calcul
des prédicats (cf Sec.~\ref{sec:rob:pred}) la 
méthode de \emph{résolution de Robinson}  est un algorithme simple 
de démonstration automatique.

Sa principale différence avec les systèmes
déductifs des chapitres précédents se situe dans le sens de la preuve:
tandis que ces deux derniers exploitent le modus ponens et 
effectuent ainsi une preuve en arrière la 
résolution va engendrer de nouveaux lemmes jusqu'à saturation 
et fonctionne donc en avant.  

On commencera par voir son application tout d'abord à la logique
propositionnelle pour s'intéresser ensuite à son intégration dans 
le calcul des prédicats. 

\section{Cas propositionnel}\label{sec:rob:prop}

\subsection{Clauses propositionnelles}

% \subsubsection{Clauses}

\begin{Def}[Forme clausale propositionnelle]
Une \emph{clause propositionnelle} est une disjonction de variables 
propositionnelles éventuellement niées. 
Une formule propositionnelle est en \emph{forme clausale} (CNF)
si elle est exprimée comme une conjonction de clauses.
On la représente classiquement comme un ensemble de clauses.
\end{Def} 

Une clause propositionnelle  est donc de la forme  
$A \ou B\ou \non C\ou\ldots$.
Pour parvenir à cette forme on utilise successivement les 
règles de réécriture:
\begin{enumerate}
\item réduire les connecteurs : on ne conserve que $\et$ ,
$\ou$ et $\non$:
\begin{eqnarray*}
A\imp B &\leadsto  & \non A\ou B \\
A\eqv B & \leadsto & (\non A\et\non B)\ou(A\et B)
\end{eqnarray*}
\item distribuer récursivement chaque  OU sur un ET:
  \begin{eqnarray*}
    (A \land B) \lor C & \leadsto &  (A \lor C) \land (B \lor C) 
  \end{eqnarray*}
\item réécrire les conjonctions de clauses comme un ensemble de clauses:
  \begin{eqnarray*}
     (B \lor D) \land (A \lor C \lor \neg D)  & \leadsto &  
    \begin{array}{rcl}
      \{ C_1 & =&  B \lor D,   \\
      C_2 & =& A \lor C \lor \neg D \}.
    \end{array}    
  \end{eqnarray*}
\end{enumerate}


Enfin, la clause vide (sans littéraux) est 
représentée par \clv. Elle est insatisfaisable dans
toute interprétation.

\begin{Exo}\label{cnf1}
Mettre chacune des formules propositionnelles suivantes sous la forme CNF.
\begin{enumerate}
\item $P \Rightarrow Q$
\item $(P\lor Q) \Rightarrow R$
\item $(P \land Q) \lor (R \land S)$
\item $(P \Rightarrow Q) \land (Q \Rightarrow R) \land (\neg R)$
\end{enumerate}
\end{Exo}

\subsection{Résolvantes d'une paire de clauses}
Deux clauses $C_1$ et $C_2$ forment une \emph{paire résoluble} s'il
existe un et un seul littéral $t$ tel que 
$t$ appartient à $C_1$ et $\neg t$ appartient à $C_2$.
Dans ce cas, on appelle \emph{résolvante} de $C_1$ et $C_2$ la clause 
notée $\textit{res}(C_1,C_2)$ obtenue en prenant la réunion des
littéraux de $C_1$ et $C_2$ moins cette paire  opposée.


\begin{Exoc}
Soit quatre clausess $C_1$, $C_2$, $C_3$,$C_4$ 
définies à l'aide de variables propositionnelles $P$, $Q$, $R$ et $S$:
\begin{eqnarray*}
C_1 &= & P \lor \neg Q \lor \neg R \\
C_2 &= & \neg P \lor S \\
C_3 & =& \neg Q \\
C_4 & =& P \lor \neg S 
\end{eqnarray*}
Quelles paires de clauses sont résolubles et dans ce cas, quelle est la
résolvante?

Réponse:
La seule paire résoluble est $(C_1,C_2)$ et sa résolvante est 
$\textit{res}(C_1,C_2) = \neg Q \lor \neg R \lor S$.
\end{Exoc}

\begin{Exo}
Pour chacun des ensembles de clauses de l'exercice~\ref{cnf1}, dire quelles 
paires sont résoluble et donner la résolvante le cas échéant. 
\end{Exo}


\subsection{Résolution d'un ensemble de clauses}\label{sub:res:ens}
A partir d'un ensemble de clauses, on appelle
\emph{résolution}  l'ensemble obtenu en appliquant la seule règle 
%de résolution 
qui, à partir de toute paire résoluble $(C_1,C_2)$ engendre la
résolvante $\textit{res}(C_1,C_2)$.
On peut alors appliquer cette méthode à la démonstration d'une formule
d'après le théorème suivant:

\begin{Th}[Déduction syntaxique par résolution]
Soit $\Gamma$ un ensemble de clauses et $C$ une clause, alors
\begin{itemize}
\item $\Gamma$ est contradictoire  si et seulement si la clause vide $\clv$
  appartient à la résolution de $\Gamma$.
\item $\Gamma \theor C$ si et seulement si $\Gamma  \cup CNF(C)$ 
  est contradictoire.
\end{itemize}
\end{Th}

\begin{Exoc}
Montrer que 
$$
\begin{array}{lrll}
\{& C_1 = & a \lor b \lor c, &  \\
  & C_2 = & \neg a \lor b \lor c,& \\
  & C_3 = & \neg b \lor c & \} \theor c.
\end{array}  
$$

\noindent Réponse:
on nomme $C_4$ la clause $\neg c$;
on cherche à démontrer que la résolution de  
$\{C_1,C_2,C_3,C_4 \}$
contient la clause vide.

\begin{itemize}
\item $C_1$ et $C_2$ sont résolubles, soit 
$C_5 = \textit{Res}(C_1,C_2) = b \lor c $.
\item $C_3$ et $C_5$ sont résolubles, soit 
$C_6 = \textit{Res}(C_3,C_5) = c $.
\item $C_4$ et $C_6$ sont résolubles, soit 
$C_7 = \textit{Res}(C_3,C_5) = \clv $.
\end{itemize}
On a donc bien le résultat souhaité.
\end{Exoc}


\begin{Exo} $ $
\begin{enumerate}
\item 
Montrer que l'ensemble des clauses engendrées par la  formule suivante est
contradictoire
  $$(A \Imp B) \land 
  (\neg A \Imp B \lor C) \land 
  (\neg C \Imp \neg B) \land 
  ((B \land C) \Imp \neg A) \land 
  (C \Imp A)$$
\item Démontrer la déduction suivante:
$$
\{A \lor B \lor \neg D, \neg A \lor C \lor \neg D, \neg B, D \} \theor
C
$$
\end{enumerate}
\end{Exo}

\begin{Exo}[Les Pures et les Pires~\cite{Smu98}]
L'ile de Puro Pira est peuplée 
de \emph{Purs} qui disent toujours la vérité et de 
de \emph{Pires} qui ne disent que des mensonges.
\begin{enumerate}
\item Débarqué sur l'île, l'antropologue Abercrombie rencontre trois indigènes 
  Arthur, Bernard et Charles. 
  Abercrombie demande d'abord à Arthur:
  \og Est-ce que Bernard et Charles sont tous les deux des Purs?\fg{}, et 
  Arthur lui répondit:\og Oui\fg{}.
  Alors Abercrombie lui demande encore:
  \og Est-ce que Bernard est un Pur?\fg{}; la réponse d'Arthur fur 
  \og Non\fg{}.
  A l'aide de la méthode de résolution de Robinson, déduire dans quel groupe 
  appartient chacun des trois indigènes.
\item Abercrombie rencontre ensuite deux autres individus Armand et Bertrand. 
Armand déclare d'une part \og  l'un de nous deux au moins est un pire \fg{} et 
d'autre part \og l'un de nous deux au plus est un pire\fg{}.
A l'aide de la méthode de résolution de Robinson, déduire dans quel groupe 
  appartient Armand et Bertrand.
\end{enumerate}
\end{Exo}

\section{Formes normales en logique des prédicats}\label{sec:form}


Pour pouvoir appliquer la méthode de résolution dans la logique des 
prédicats il est nécessaire 
d'exprimer ces formules sous la forme clausale qui est une version étendue  de la forme clausale propositionnelle.

Cette section présente la mise en forme prénexe, Sec.~\ref{sec:prenex},
la mise en forme de Skolem, Sec.~\ref{sec:skol} et 
la mise en forme clausale, Sec.~\ref{sec:cnf}.

\subsection{Forme prénexe } \label{sec:prenex}


\begin{Def}[Forme prénexe]
Une formule $G$ est en forme prénexe si tous ses
quantificateurs ($\forall$ et $\exists$) apparaissent en tête, à
gauche, dans cette formule. 
Elle est ainsi de la forme
$Q_1 x_1\,.\, Q_2 x_2\, .\, \ldots Q_n x_n\, .\,  B$, où $B$ est une
formule sans quantificateurs.
\end{Def}

% \subsubsection{Méthode}
La méthode à suivre est la suivante:
\begin{itemize}
\item Réduire les connecteurs: on ne conserve que $\et$ ,
$\ou$, $\non$:
\begin{eqnarray*}
A\imp B &\leadsto  & \non A\ou B \\
A\eqv B & \leadsto & (\non A\et\non B)\ou(A\et B)
\end{eqnarray*}
\item Renommer les variables liées, de manière à ce que toute variable
liée ne le soit qu'une seule fois, et qu'aucune variable liée ne
présente d'occurrence libre, d'après les égalités suivantes: 
\begin{eqnarray*}
\qqs x\, .\,  A(x) & \leadsto & \qqs  y \, .\, A(y)\\
\exi x \, .\, A(x) & \leadsto & \exi  y \, .\, A(y)
\end{eqnarray*}
\item Faire \og remonter\fg{} les quantificateurs en tête, par les
réécritures  suivantes:
\begin{eqnarray*}
\non\non A& \leadsto &  A \\
\non(\qqs x \, .\,    A(x))& \leadsto &  \exi x \, . \, \non A(x) \\
\non(\exi x \, .\,  A(x))& \leadsto &  \qqs  x \, . \,  \non A(x) 
\end{eqnarray*}
\noindent et, si $x$ n'est pas variable libre de $C$ 
\begin{eqnarray*}
C\ou\qqs x \, .\, A(x)& \leadsto & \qqs x \, .\, (C\ou A(x))\\
C\ou\exi x \, .\, A(x)& \leadsto & \exi x \, .\, (C\ou A(x))\\
C\et\qqs x \, .\, A(x)& \leadsto & \qqs x \, .\, (C\et A(x))\\
C\et\exi x \, .\, A(x)& \leadsto & \exi x \, .\, (C\et A(x))
\end{eqnarray*}
\end{itemize}



\begin{Exo}\label{ex:crime}
 On considère les propositions suivantes:\par
\begin{tabular}{ c l}
$P_1$ & Tout crime a un auteur \\
$P_2$ & Seuls les gens malhonnêtes commettent des crimes \\
$P_3$ & On n'arrête que les gens malhonnêtes \\
$P_4$ & Les gens malhonnêtes arrêtés ne commettent pas de crimes \\
$P_5$ & Des crimes se produisent \\
\end{tabular}\par
On voudrait en déduire:\par
\begin{tabular}{ c l}
$Q$ & Il y a des gens malhonnêtes en liberté \\
\end{tabular}\par\noindent
Sans anticiper sur les méthodes de résolution, on va ajouter aux
propositions $P_1$ à $P_5$ la proposition $P_6\approx\non Q$

% (si on montre que cet ensemble de propositions est \og insatisfaisable\fg{} , on aura
% montré que $Q$ est conséquence de $P_1$ à $P_5$).
% \par\noindent
Pour cela, on considère les prédicats
\begin{itemize}
\item $\textit{ar}(x)$: la personne $x$ est arrêtée;
\item $\textit{mal}(x)$: la personne $x$ est malhonnête;
\item $\textit{cou}(x,y)$: la personne $x$ commet l'action $y$;
\item $\textit{cr}(y)$: l'action $y$ est un crime.
\end{itemize}

Traduisez chacune des propositions ci dessus en logique des prédicats et 
ecrivez chaque formule sous la forme prenexe.

% On obtient\par
% \begin{tabular}{c l}
% $F_1$ & $\forall y\, .\, (\textit{cr}(y)\imp\exists x\, .\,  {\rm
%   co}(x,y))$ \\ 
% $F_2$ & $\forall x, y  \, .\, (\textit{cr}(y)\et \textit{cou}(x,y)) \imp {\rm
%   mal}(x)$ \\ 
% $F_3$ & $\forall x\, .\, \textit{ar}(x)\imp \textit{mal}(x)$ \\
% $F_4$ & $\forall x\, .\, (\textit{mal}(x) \et \textit{ar}(x)) \imp
% (\forall y\, .\,  \textit{cr}(y) \imp \neg \textit{cou}(x,y))$ \\ 
% $F_5$ & $\exists x \, .\, \textit{cr}(x)$ \\
% $F_6$ & $\non (\exists x \, .\, \textit{mal}(x) \et \non \textit{ar}(x))$ \\
% \end{tabular}\par
% \noindent qui deviennent, sous forme prénexe,\par
% \begin{tabular}{c l}
% $F_1$ & $\forall y\,.\,\exists x \, .\, (\non\textit{cr}(y)\ou\textit{cou}(x,y))$ \\
% $F_2$ & $\forall x, y \, .\, (\non\textit{cr}(y)\ou\non\textit{cou}(x,y)\ou{\rm
% mal}(x))$ \\
%  $F'_3$ & $\forall x \, .\, (\non\textit{ar}(x)\ou\textit{mal}(x))$ \\
% $F_4$ & $\forall x,y \, .\, (\non\textit{mal}(x)\ou\non
% \textit{ar}(x)\ou\non\textit{cr}(y)\ou\non\textit{cou}(x,y))$ \\
% $F_5$ & $\exists x\,.\, \textit{cr}(x)$ \\
% $F_6$ & $\forall x\,.\, (\non\textit{mal}(x)\ou\textit{ar}(x))$ \\
% \end{tabular}
\end{Exo}


\subsection{Forme de Skolem}\label{sec:skol}



 
\begin{Def}[Forme de Skolem]
  Une formule  est
  sous forme normale de Skolem 
  si sa forme prénexe contient uniquement des quantificateurs
  universels. 
\end{Def}

La démarche qui consiste a supprimer les quantifications
existentielles de la forme prénexe est appelée \emph{skolémisation} et
est définie comme suit:

\begin{itemize}
\item Soit $\exi x_j$ un quantificateur existentiel qui figure
après les $n$ quantificateurs universels 
$\qqs x_{j_1}\qqs  x_{j_2}\ldots\qqs x_{j_n}$. 
La quantification  $\exi x_j$ est supprimée et la variable 
 $x_j$ est remplacé par le terme $f(x_{j_1}, x_{j_2}\ldots,
 x_{j_n})$ où $f$ est un symbole fonctionnel  $n$-aire qui n'apparaît
 pas ailleurs.
\item Soit $\exi x_j$ un quantificateur existentiel qui n'est
précédé par aucun quantificateur universel: on peut le supprimer et
remplacer $x_j$ par un symbole de constante frais $c_j$ 
%(qui n'est autre qu'un symbole fonctionnel zéro-aire)
\end{itemize}

Cette transformation est autorisée par le théorème suivant, que l'on admettra.


\begin{Th}[Théorème de Skolem]
Soit ${\cal A}$ un ensemble fini de formules 
et ${\cal A}_S$  l'ensemble des formes de Skolem de ces formules. 
Alors, ${\cal A}$ peut être interprétée à \og \vrai\fg{} 
si et seulement si ${\cal A}_S$ peut aussi être interprétée à \og \vrai\fg{}.
\end{Th}




% On va vérifier ce théorème pour un ensemble réduit à une seule
% formule du type
% $$A = \qqs x\,.\, \exi y\, .\,  p(x,y)$$
% Sa forme de Skolem est
% $$A_S = \qqs x\,.\, p(x,f(x))$$
% \begin{itemize}
% \item Soit $E$ un modèle de $A$; 
% % Ce modèle admet une relation binaire $p$. 
% % $E$ étant un modèle de $A$, par définition, $A$ y
% % est satisfaite. 
% Comme la formule $\exi y\,.\, p(x,y)$ est vraie dans $E$,
% % Ceci
% % signifie que, 
% pour chaque valeur $\alpha$ de $x$, il existe au moins une
% valeur $\beta$ de $y$ telle que $p(\alpha,\beta)$ 
% a la valeur de vérité \og \vrai\fg{}.
% On peut définir une fonction $f$ de $E$
% dans lui-même en posant, qui associe à chaque valeur de $\alpha$ un
% des $\beta$ choisis précédemment ($f(\alpha) = \beta$). 
% % Le problème se complique s'il existe plusieurs, voire
% % une infinité de valeurs de $y$ possibles pour une valeur donnée de $x$.
% % Autrement dit, se pose le problème de l'axiome du choix. Mais c'est le
% % théorème de Löwenheim-Skolem qui intervient ici; ce théorème
% % affirme en effet que, si un ensemble de formules de \og \textit{PR}\fg{} admet un
% % modèle, alors il admet un modèle.% de base dénombrable. 
% % En se plaçant
% % dans ce modèle, le choix auquel il est fait allusion est possible, sans
% % recours à l'axiome du choix. Ayant ainsi défini une fonction $f$, E,
% % cette fois muni de $p$ et de $f$, constitue 
% On a donc un modèle pour la formule
% $\qqs x \, .\,  p(x,f(x))$, c'est à dire pour $A_S$. 
% \item Réciproquement, si
% $E$ est un modèle de $A_S$, alors, évidemment, $\exi y\,.\, p(x,y)$
% est valide dans $E$, puisqu'il suffit d'exhiber $y=f(x)$ pour le
% montrer, et 
% donc, $E$ est un modèle de $A$.
% \end{itemize}



\begin{Exo}[Suite exemple~\ref{ex:crime}]\label{ex:crime:2}
Donnez la forme de Skolem de chacune des formules de l'exercice~\ref{ex:crime}.  

% Des formes de Skolem des formules énoncées à l'exemple
% sont:

% \begin{tabular}{c l}
% $F''_1$ & $\qqs y\,. \, \non\textit{cr}(y) \ou \textit{cou}(f(y),y)$ \\
% $F''_2$ & $\qqs x, y \, .\, \non\textit{cr}(y)\ou\non\textit{cou}(x,y)\ou{\rm
% mal}(x)$ \\ 
% $F''_3$ & $\qqs x \, .\, \non\textit{ar}(x)\ou\textit{mal}(x)$ \\
% $F''_4$ & $\qqs x, y \, .\, \non
% \textit{mal}(x)\ou\non\textit{ar}(x)\ou\non\textit{cr}(y)\ou\non\textit{cou}(x,y)$ \\
% $F''_5$ & $\textit{cr}(a)$ \\
% $F''_6$ & $\forall x  \, . \, \non\textit{mal}(x)\ou\textit{ar}(x)$ \\
% \end{tabular}

% où 
% $f$ est un symbole fonctionnel frais et 
% $a$ est une constante fraîche. 
\end{Exo}


\subsection{Forme clausale}\label{sec:cnf} 

% \subsubsection{Suppression des quantificateurs universels} 
Dans la forme de Skolem 
d'une formule ne subsistent donc que des quantificateurs
universels. Ceux-ci 
sont purement et simplement supprimés. Cette suppression est autorisée 
par la méthode de déduction utilisée 
%(et n'est possible que si c'est cette méthode qui est effectivement utilisée).
 En effet, pour prouver
que la formule $T$ est conséquence de l'ensemble de formules ${\cal A}$, on
cherche à prouver que ${\cal A}\cup\{\non T\}$ n'admet pas de modèle.
Pour cela, il suffit d'exhiber une contradiction dans un \og cas 
particulier\fg{} , et il est bien clair que, si, dans l'ensemble
${\cal A}$ de 
formules, on supprime les quantificateurs universels, et qu'on prouve
que 
ces formules, avec $\non T$, n'admettent pas de modèle, alors les 
formules \og complètes\fg{} , avec quantificateurs, et $\non T$, n'en
auront pas 
non plus. 



On étend enfin la notion de clause propositionnelle en considérant ici 
des littéraux au lieu de variables propositionnelles.

\begin{Def}[Forme clausale]
Une \emph{clause} est une disjonction de littéraux (atome ou négation d'un
atome). 
Une formule est en \emph{forme clausale} (CNF)
si elle est exprimée comme une conjonction de clauses.
On la représente classiquement comme un ensemble de clauses.
\end{Def} 



\begin{Exo}[Suite de l'exo~\ref{ex:crime:2}]
Donner la forme clausale des formes de Skolem de l'exo~\ref{ex:crime:2}.
\end{Exo}
% La forme clausale est 

% $$
% \begin{array}{l}
%   \{\non\textit{cr}(y) \ou \textit{cou}(f(y),y), \\
%   \quad \non \textit{cr}(y)\ou\non\textit{cou}(x,y)\ou\textit{mal}(x), \\ 
%   \quad \non\textit{ar}(x)\ou\textit{mal}(x), \\
%   \quad \non \textit{mal}(x) \ou \non\textit{ar}(x) \ou \non\textit{cr}(y) \ou
%   \non \textit{cou}(x,y), \\ 
%   \quad \textit{cr}(a), \\
%   \quad  \non\textit{mal}(x)\ou\textit{ar}(x)\} \\
% \end{array}
% $$
% \end{Ex}

% \section{Système de Herbrand}

% %________________ 61.

% \subsection{Introduction}

% Pour reconnaître si, oui ou non, un ensemble de formules admet un
% modèle, il faut essayer diverses interprétations possibles: à un élément, à
% deux éléments, \ldots., à une infinité d'éléments. Chacun de ces 
% essais conduit lui-même à de nombreux cas; l'intérêt du théorème
% de Herbrand est qu'il affirme que tous ces essais peuvent se ramener à un
% seul, qui n'utilise que le \og vocabulaire\fg{} des formules qui sont en question,
% un \og modèle syntaxique\fg{} unique. Par ailleurs la méthode des \og tables de
% vérité\fg{} , ou, ce qui revient au même, la méthode des fonctions de
% vérité booléennes, conduit elle aussi à un nombre d'essais très
% rapidement beaucoup trop grand (dès que les formules sont un peu
% compliquées ou un peu nombreuses et comportent beaucoup de variables. Le
% nombre d'essais croît comme $2^n$, et devient très vite trop
% important).

% %________________ 62.

% \subsection{Univers, atomes, système de Herbrand}
% Pour un ensemble de formules (mis sous forme de clauses), l'univers de Herbrand associé 
% est l'ensemble des termes sans variables qui peuvent être construits à
% partir du vocabulaire de ces formules (symboles de constantes et symboles
% opératoires ou fonctionnels). Pour que cet univers ne soit pas vide, s'il
% n'y a pas de constante, on en introduit une. Les atomes de Herbrand sont les
% atomes qui interviennent dans ces formules, lorsqu'on a remplacé les
% variables par des éléments de l'univers de Herbrand.
% \psaut\noindent
% Reprenons l'exemple de nos criminels\par
% \begin{tabular}{c l}
% $F'''_1$ & $\non\textit{cr}(y)\ou\textit{cou}(f(y),y)$ \\
% $F'''_2$ & $\non\textit{cr}(y)\ou\non\textit{cou}(x,y)\ou\textit{mal}(x)$ \\
% $F'''_3$ & $\non\textit{ar}(x)\ou\textit{mal}(x)$ \\
% $F'''_4$ & $\non\textit{mal}(x)\ou\non\textit{ar}(x)\ou\non\textit{cr}(y)\ou\non{\rm
% co}(x,y)$ \\
% $F'''_5$ & $\textit{cr}(a)$ \\
% $F'''_6$ & $\non\textit{mal}(x)\ou\textit{ar}(x)$ \\
% \end{tabular}\par\noindent
% Les éléments du vocabulaire de ces clauses sont:
% \begin{itemize}
% \item un symbole de constante ($a$)
% \item un symbole opératoire de poids 1 ($f$)
% \end{itemize}
% L'univers de Herbrand est donc
% $$\{a,f(a),f(f(a)),f(f(f(a))),\ldots\}$$
% Un atome de Herbrand est\par
% \centerline{$\textit{ar}(a)$, ou $\textit{mal}(f(f(a)))$, ou, etc\ldots}\par\noindent
% Le système de Herbrand est obtenu en remplaçant successivement les
% variables de l'ensemble de formules considéré par les éléments de
% l'univers de Herbrand.

% %________________ 63.

% \subsection{Théorème de Herbrand}

% Un ensemble de clauses admet un modèle si et seulement s'il admet un
% modèle basé sur l'univers de Herbrand. De plus, pour que cet ensemble de
% clauses soit insatisfaisable, il suffit que l'une des formules du système de
% Herbrand ne soit pas satisfaisable.

% \noindent Application:
% \begin{itemize} 
% \item 1$^{\hbox{\rm ère}}$ génération: avec $x=a$ , $y=a$\par 
% \{$\non\textit{cr}(a)\ou\textit{cou}(f(a),a)$ , $\non\textit{cr}(a)\ou\non{\rm
% co}(a,a)\ou\textit{mal}(a)$ , $\non\textit{ar}(a)\ou\textit{mal}(a)$ , $\non{\rm
% mal}(a)\ou\non\textit{ar}(a)\ou\non\textit{cr}(a)\ou\non\textit{cou}(a,a)$ , ${\rm
% cr}(a)$ , $\non\textit{mal}(a)\ou\textit{ar}(a)$\}\vskip 5pt
% satisfaisables:\par
% \begin{tabular}{c c c c c}
% $\textit{cr}(a)$ & $\textit{cou}(f(a),a)$ & $\non\textit{cou}(a,a)$ & $\non\textit{ar}(a)$
% & $\non\textit{mal}(a)$ \\ ou \\
% $\textit{cr}(a)$ & $\textit{cou}(f(a),a)$ & $\non\textit{cou}(a,a)$ & $\textit{ar}(a)$ &
% $\textit{mal}(a)$ \\ \end{tabular}
% \item 2$^{\hbox{\rm ème}}$ génération: avec $x=f(a)$ , $y=a$\par
% \{$\non\textit{cr}(a)\ou\non\textit{cou}(f(a),a)\ou\textit{mal}(f(a))$ , $\non{\rm
% ar}(f(a))\ou \textit{mal}(f(a))$ , $\non\textit{mal}(f(a))\ou\non{\rm
% ar}(f(a))\ou\non\textit{cr}(a)\ou\non\textit{cou}(f(a),a)$ , $\non{\rm
% mal}(f(a))\ou\textit{ar}(f(a))$\}\vskip 5pt
% la première exige $\textit{mal}(f(a))$,
% donc la dernière exige $\textit{ar}(f(a))$, donc la troisième ne peut
% être satisfaite: c'est terminé.
% \end{itemize}
% L'ensemble de clauses n'admet pas de
% modèle ayant basé sur l'univers de Herbrand, donc il n'admet aucun
% modèle, donc la formule $F_6$ n'est pas conséquence des cinq
% premières, donc $\non F_6$ est un théorème, et donc \og il y a bien des
% personnes malhonnêtes en liberté\fg{} .

% %________________ 64.

% \subsection{Algorithme de Herbrand}

% Il s'agit du premier algorithme de \og démonstration automatique\fg{} . D'un
% point de vue théorique, il ne fait rien de plus que celui qui consisterait
% à produire toutes les conséquences possibles (à l'aide des règles
% d'inférence) des formules de l'ensemble de départ, pour essayer de
% trouver la formule finale comme conséquence de cet ensemble. Il est
% cependant plus facile à mettre en \oe uvre, et donne souvent le résultat
% plus rapidement que la méthode des tables de vérité. Cependant, il doit
% être clair qu'il s'agit d'un algorithme qui s'arrête au bout d'un temps
% fini (éventuellement long!) si l'ensemble de clauses est insatisfaisable,
% mais qui ne s'arrête pas dans le cas contraire (conséquence
% désagréable de l'indécidabilité du calcul des prédicats\ldots).



% % \bibliographystyle{alpha}
% % \bibliography{biblio}


\section{Résolution en logique des prédicats}\label{sec:rob:pred}
La méthode de résolution étendue au calcul des prédicats est plus
complexe que sa version en calcul propositionnel puisqu'elle doit
prendre en compte l'existence de variables.
Elle sert de base au langage Prolog qui est étudié en TP.

\subsection{Résolvante d'une paire de clauses}
Comme précédemment, on ne considère que des formules mises sous la
forme clausale. 

Deux clauses $C_1$ et $C_2$ forment une paire résoluble si et
seulement si elles contiennent au moins une paire de littéraux 
$P(t_1,\ldots, t_n)$ et $\neg P(t'_1,\ldots,t'_n)$ telle qu'il existe 
une substitution $\sigma$ avec 
$\sigma(t_1)= \sigma(t'_1)$, \ldots, $\sigma(t_n)= \sigma(t'_n)$.


pour tout $i$, $1 \le i \le n$, 
$t_i\ sigma  = t'_i \sigma$.
%[[JFC : est ce que qu'il ne doit y avoir qu'un seul literal]]

Dans un tel cas, à partir de la liste de paires de termes
$\{(t_1, t'_1), \ldots, (t_n, t'_n)\}$, toute substitution 
telle que $\sigma(t_i)= \sigma(t'_i)$ est appelé \emph{unificateur}. 
Il s'agit de trouver l'unificateur \emph{le plus général}: c'est celui tel que
toute autre substitution se déduit de cet unificateur par composition
à partir d'une autre substitution.

En pratique, on cherchera la substitution la moins particulière possible.
Dans ce cas, on appelle résolvante de $C_1$ et $C_2$ la clause notée 
$\textit{Res}(C_1,C_2)$ obtenue en prenant la réunion de $C_1$ et de
$C_2$, en effectuant $\sigma$ et en supprimant la paire opposée 
$P(\sigma(t_1),\ldots, \sigma(t_n))$ et 
$\neg P(\sigma(t'_1),\ldots,\sigma(t'_n))$.

\begin{Ex}
Soit deux clauses $C_1 = P(x) \lor Q(g(x))$ et 
$C_2 = \neg P(f(y))$.
La paire $(C_1, C_2)$ est résoluble  en prenant comme substitution
$(f(y)/x, y/y)$. 
Sa résolvante est $\textit{Res}(C_1,C_2)= Q(g(f(y)))$.

Dans la pratique, on ne mentionne que les substitution qui modifient
les variables. On omettra ainsi celles du type $(y/y)$.
\end{Ex}

\begin{Exo}
Peut-on unifier les deux formules atomiques suivantes?
$$ P(f(X,g(Z)),X,f(Y,g(b))) \textrm{ et } 
P(f(U,g(f(a,b))),X,U) $$ 
\end{Exo}


\subsection{Résolution d'un ensemble de
  clauses}\label{sub:res:ens:pred}
La démarche est exactement la même qu'à la section~\ref{sub:res:ens},
modulo le fait qu'on considère ici la règle de résolution avec
unificateur.

\begin{Ex}
Démontrons que l'ensemble de clauses 
$$\begin{array}{rll}
\{ & C_1 = P(a,X) \lor Q(Y,X), & \\
 & C_2 = \neg Q(Z,T) \lor R(a,Z), & \\
 & C_3 = \neg P(a,b), & \\
 & C_4 = \neg R(U,V) &\} \\
\end{array}
$$
est contradictoire.
Pour cela on résout les clauses et on calcule leur résolvante:
\begin{itemize}
\item $C_1$ et $C_3$ sont résolubles avec comme substitution $(b/X)$. 
Soit $C_5 = Q(W,b)$; 
\item $C_2$ et $C_4$ sont résolubles avec comme substitution
  $(a/U,Z/V)$. Soit $C_6 = \neg Q(Z',T')$;
\item $C_5$ et $C_6$ sont résolubles avec comme substitution
  $(W/Z',b/T')$. Soit $C_7 = \clv$, ce qui termine la démonstration.
\end{itemize}
\end{Ex}

\subsection{Mise en {\oe}uvre de la résolution}
La mise en {\oe}uvre de la résolution est moins immédiate que dans le
cas propositionnel: en raison de la présence de variables quantifiées:
\begin{itemize}
\item  la mise en forme clausale est plus complexe car elle
nécessite deux étapes supplémentaires (mise en forme prénexe et
skolémisation);
\item la résolution est aussi plus complexe car elle nécessite 
d'exhiber l'unificateur le plus général.
\end{itemize}

\begin{Exo}
Montrer que les figures suivantes sont valides ou contradictoires à
l'aide de la méthode de résolution de Robinson.
\begin{eqnarray*}
\varphi_1 & = & (\exists X \, . \, 
( \forall Y \,.\, 
S(X) \Ssi S(Y))) \land 
(\forall Z \, .\, S(Z)) \\
\varphi_2 & = & 
\forall X\,.\, \exists Y,Z \,. \,
(R(X,X) \Imp R(Z,Y)) \land 
(\neg R(X,X) \lor R(Y,Z)) \\
\varphi_3 & = & 
\forall X,Y\, .\, 
\exists Z\,.\, (R(X,X)\land R(X,Y)) \Imp R(X,Z) \\
\varphi_4 & = & 
\forall X,Y\, .\, 
\exists Z\,.\, R(X,Y)\land (R(Y,Z) \Imp \neg R(Z,Z)) \\
\end{eqnarray*}
\end{Exo}

\begin{Exo}
Démontrons la déduction suivante à l'aide de la méthode de
résolution de Robinson:
$$\begin{array}{rll}
\{ & \forall X \,.\, S(X,X) \Imp U(X,X) & \\
\{ & \forall X,Z \, .\, \neg (T(Z,F(X)) \land U(Z,F(X))) & \\
\{ & \forall Y,Z\, . \, R(Y,Z) \lor S(Y,Z) & \} \theor  
\exists X,Y\,.\, T(X,Y) \Imp R(X,Y)
\end{array}
$$
\end{Exo}

\begin{Exo}
Sachant que :
\begin{itemize}
\item l'inspecteur fouillait tous ceux qui pénétraient dans le
  bâtiment sauf ceux accompagnés par des membres du personnel de
  l'entreprise;
\item certains des hommes de la bande de F. pénétraient dans le
  bâtiment sans être accompagnés de personne étrangère  à la bande de
  F.;
\item l'inspecteur n'a fouillé aucun des hommes de la bande de F..
\end{itemize}
Établir que certains membres de la bande de F. étaient membres du
personnel de l'entreprise. 
\end{Exo}

\begin{Exo}
\item Sachant que :
\begin{itemize}
\item un oncle est soit le frêre d'une mère, sont le frère d'un père;
\item Fred est l'oncle de  Jack;
\item Bob est le père de  Jack;
\item Carol est la mère de Jack;
\item Bob n'a pas de frère;
\end{itemize}
Déduire par la méthode de résolution le nom du frère de Carol.
\end{Exo}

\begin{Exo}
\item Sachant que :
\begin{itemize}
\item Jack possède un chien;
\item Chaque possesseur de chien aime les animaux;
\item Un amoureux des animaux ne peux pas tuer un animal
\item Soit Jack ou Curiosity ont tué le chat (dont le nom est Tuna)
\end{itemize}
Montrer que c'est Curiosity qui a tué le chat
\end{Exo}





 \gsaut

\centerline{\x{Fin du Chapitre}}




% \item Article 1: Tout membre non \'Ecossais porte des chaussettes
%   oranges. 
% \item Article 2: Tout membre porte une jupe ou ne porte pas de
%   chaussettes oranges. 
% \item Article 3: Les membres mariés ne sortent pas le dimanche.
% \item Article 4: Un membre sort le dimanche si et seulement s'il
% est \'Ecossais. \item Article 5: Tout membre qui porte une jupe est
% \'Ecossais et 
% marié. \item Article 6: Tout membre \'Ecossais porte une jupe.

% \end{itemize}

% Déterminer le nombre de membres de ce club.
% \end{Exo}