ajout relbin13

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

% \setcounter{Exo}{0}
% \setcounter{Def}{0}
% \setcounter{Th}{0}
% \setcounter{Rem}{0}
% \setcounter{Notation}{0}
% \setcounter{Ex}{0}


\chapter{Algorithme de résolution}

\section{Résolution sans variables}

\subsection{Cadre}

Il n'y a ici pas de variables autres que les variables
propositionnelles, et on se place en logique des propositions. 

\subsection{Le système formel RSV}


Le système formel RSV (Résolution sans variable) est le système formel
choisi pour traiter les problèmes posés en calcul propositionnel. 

\subsection{Principes généraux}

Quelques principes généraux de la résolution sans variable (RSV) :

\medskip

\begin{itemize}
\item Les seules formules correctes admises sont les clauses,
  c'est-à-dire des disjonctions de littéraux, positifs ou négatifs
  (précédé de $\non$). 

\item Les seuls connecteurs admis sont $\non$ et $\ou$.

\item Une clause est satisfaite quand l'un de ses littéraux est
  vrai.

\item La clause vide (ne contenant aucun littéral) ne vérifie pas
  cette condition, elle est dite insatisfaite. 
\end{itemize}

\begin{Notation}
 La clause vide est représentée par $\square$.
\end{Notation}


\subsection{Le système formel RSV}

\noindent Ces principes généraux se formalisent ainsi :

\medskip

\begin{itemize}
 \item alphabet : les variables propositionnelles, $\non$ et $\ou$.

 \item axiomes : pas d'axiomes.

 \item règles d'inférence : $\{F \ou G, \non F \ou G \} \vdash (RSV) G
   \ou H$ 
\end{itemize}

\bigskip

\begin{Rem}
Cette dernière règle est une généralisation du \og modus ponens \fg :  

$$\{F,F \imp G \} \vdash H , ~ \{F \ou B, \non F \ou H \}
\vdash B \ou H$$ 
\end{Rem}

Par rapport à la logique propositionnelle, la suppression des axiomes
et la généralisation de la règle d'inférence ont pour
conséquence la perte de la complétude (\emph{i.e.} équivalence
tautologie/théorème). 

\begin{Rem}
En logique propositionnelle, on avait $\{F\} \vdash F \ou G$. Cette
déduction ne peut plus être obtenue dans RSV. 
\end{Rem}



\subsection{Quelques indications sur les algorithmes de résolution}

\subsubsection{Généralités}

Il y a trois classes d'algorithmes de résolution :

\begin{description}
 \item[Les algorithmes de chaînage avant] : on part des données
   (l'ensemble des clauses de départ), on en déduit de nouvelles
   clauses, et ainsi de suite, en espérant arriver à la conclusion. 
 \item[Les algorithmes de chaînage arrière] on part de la conclusion,
   on construit les clauses qui par déduction permettraient de les
   obtenir, et ainsi de suite, en espérant obtenir les clauses de
   départ. 
\item[Les algorithmes mixtes]
 \end{description}

\begin{Th}[Théorème de falsification]
\index{Théorème de falsification} 
$\mathcal{F} \vdash A$ si et seulement si $\mathcal{F} \cup \{ \non A
\} \vdash \square$, où $\mathcal{F}$ est un ensemble de clauses, et
$A$ une clause. 
\end{Th}



\subsubsection{Un exemple de chaînage avant : algorithme de saturation}

On produit systématiquement toutes les clauses possibles à partir des
clauses de départ, et on recommence jusqu'à ce qu'il n'y ait plus
production de nouvelles clauses. 

Cet algorithme n'est cependant pas efficace. On peut l'améliorer en
\og saturation avec simplification \fg, les simplifications étant : 

\begin{itemize}
\item la suppression de tautologie,
\item la suppression des clauses subsumées ($C$ est subsumée par $C'$
  si tous les littéraux de $C'$ sont dans $C$ : $A \ou B \ou C$ est
  subsumée par $A \ou B$). 
\end{itemize}



\begin{Ex}
Ensemble de clauses de départ :

$$
\begin{array}{ll}
 a \imp b & C_1 = \non a \ou b \\
 b \imp c & C_2 = \non b \ou c \\
 c \imp a & C_3 = \non c \ou a \\
 a \ou b \ou c   & C_4 = a \ou b \ou c \\
\end{array}
$$



\paragraph{Génération 1}



\noindent $\{ C_1, C_2 \} \vdash C_5 = \non a \ou c$ \\
$\{ C_1, C_3 \} \vdash C_6 =  b \ou \non c$ \\
$\{ C_1, C_4 \} \vdash C_7 = b \ou c$ \\
$\{ C_2, C_3 \} \vdash C_8 = a \ou \non b$ \\
$\{ C_2, C_4 \} \vdash C_9 = a \ou c$ \\
$\{ C_3, C_4 \} \vdash C_{10} =  a \ou b$ \\

$C_4$ est subsumé par $C_7$.

\bigskip

\paragraph{Génération 2}

Les clauses des deux générations précédentes entre elles :

\noindent $\{ C_1, C_8 \} \vdash C_{11} = b \ou \non b$ \\
$\{ C_1, C_9 \} \vdash C_{12} =  b \ou c$ \\
$\{ C_1, C_{10} \} \vdash C_{13} = b$ \\
$\{ C_2, C_6 \} \vdash C_{14} = c \ou \non c$ \\
$\{ C_2, C_{10} \} \vdash C_{15} = b$ \\
etc.


$C_1, C_6, C_7, C_{10}$ sont subsumées par $C_{13}$.

$C_{12}$ est $C_7$, $C_{15}$ est $C_{13}$.

$C_{11}$ et $C_{14}$ sont des tautologies.
\end{Ex}



\begin{Rem}
Il est préférable de retirer les clauses subsumées au fur et à mesure.
\end{Rem}


\subsubsection{Exemple d'algorithme de chaînage arrière}

\paragraph{Présentation}

Le problème est de savoir si $\mathcal{F} \vdash C$, où $\mathcal{F}$ est un ensemble de clauses, et $C$ est une clause.



On sait que c'est équivalent à

\begin{center}$\mathcal{F} \vdash \{ \non C\}$ insatisfiable à condition que $\mathcal{F}$ soit satisfiable.
\end{center}



On étudie donc la clause pour essayer de formuler des diagnostiques.

On essaye, par exemple, si $C$ serait conséquence de $\mathcal{F}$, puis en cas de réponse positive, si $\non C$ ne serait pas aussi une conclusion possible.

Si c'est le cas, cela signifie que $\mathcal{F}$ est contradictoire : le problème est mal posé.

Le but de \og savoir si $C$ (un littéral) se déduit de $\mathcal{F}$ \fg{} se traduit par : \og Effacer $\non C$ dans l'ensemble des clauses de $\mathcal{F}$, la liste de ses ancêtres étant vide. \fg







\paragraph{Les règles de l'algorithme SL résolution}
\begin{enumerate}
\item Un littéral qui figure dans sa propre liste d'ancètres ne s'efface pas ($\imp$ arrêt de l'algo)

\item Un littéral dont la négation figure dans la liste des ancêtres s'efface.

\item Si on est dans aucun des cas précédent, on doit chercher une résolvante, c'est-à-dire une clause de $\mathcal{F}$ qui contienne la négation du littéral que l'on cherche à effacer qui permet donc une déduction (par RSV).

Le but \og effacer le littéral dans l'ensemble des clauses $\mathcal{F}$ et avec la liste d'ancêtre $N$ \fg{} est alors remplacé par \og effacer tous les littéraux de la résolvante dans $\mathcal{F}$, en rajoutant le littéral sur lequel se porte la déduction à la liste des ancêtres \fg.
\end{enumerate}


\begin{Ex}
$$
 \begin{array}{ll}
  a \ou b & \leftarrow C_1 \\
 \non b \ou c & \leftarrow C_2 \\
 a \ou \non c & \leftarrow C_3 \\
a \ou b \ou c & \leftarrow C_4 \\
 \end{array}
$$
On va demander à SL résolution un diagnostique sur $a$ ($a$ est déductible de cet ensemble de clauses).

Le but est \og effacer $\non a$ dans l'ensemble des clauses, liste d'ancêtres [] (vide) \fg.

Avec la clause $C_4$, on obtient la résolvante $\{ \non a, a \ou b \ou c \} \vdash b \ou c.$

Le but est remplacé par \og effacer les littéraux de $b \ou c$ dans l'ensemble des clauses, liste des ancêtres [ $\non a$ ].
\begin{itemize}
 \item Effacer $b$ \og $\hdots$ \fg, liste ancêtre [ $\non a$ ].\\
Avec $C_2 \{ b, \non b \ou c \} \vdash c$.\\
\og Effacer $c$, liste ancêtre [ $\non a, b$ ]. \fg \\
Avec $C_3 \{ c, \non c \ou a \} \vdash a$.\\
\og Effacer $a$, liste ancêtre [ $ \non a, b, c$ ]. \fg \\
$\imp$ Succès car $\non a$ dans liste des ancêtres.
\item Effacer $c$ \og $\hdots$ \fg, liste ancêtre [ $\non a$ ].\\
Avec $C_3 \{ c, \non c \ou a \} \vdash a$.\\
\og Effacer $a$, liste ancêtre [$\non a $]. \fg \\
$\imp$ Succès car $\non a$ dans la liste des ancêtres.
\end{itemize}
Succès pour effacer $a$.

Il reste à vérifier si on peut effacer $\non a$.
\end{Ex}


\subsection{Exemples complets de résolution}



Ces divers exemples sont indépendants...

\subsubsection{Méthode de résolution}

...La méthode de résolution est cependant la même. Elle est exposée ici, et elle est valable pour chacun d'entre eux sauf le dernier, qui ne se satisfait pas d'une déduction linéaire.

\begin{enumerate}
 \item Formaliser en logique des propositions (pas en calcul des prédicats) les propositions, puis

 \item les mettre sous forme de clauses (sans variables). Ces clauses seront numérotées, dans l'ordre de leur obtention.

\item Appliquer la règle d'inférence de \og RSV \fg{} pour obtenir la conclusion que l'on peut tirer de l'ensemble de propositions.

Les nouvelles clauses déduites recevront un numéro.

Une déduction sera présentée sous la forme $(C_i, C_j) \vdash C_k = ...$

La conclusion demandée est une clause qui ne contient comme littéraux que ceux qui ne figurent qu'une seule fois dans l'ensemble de clauses de départ.

Utiliser une déduction linéaire dont la racine est une clause qui contient l'un de ces littéraux.

\item Traduire la conclusion obtenue sous forme de phrase française.

\end{enumerate}


\subsubsection{Les exemples complets}

\begin{Ex}
Les animaux de la maison...
 \begin{enumerate}
  \item Les seuls animaux de cette maison sont des chats.
  \item Tout animal qui aime contempler la lune est apte à devenir un animal familier.
 \item Quand je déteste un animal, je l'évite soigneusement.
 \item Aucun animal n'est carnivore, à moins qu'il n'aille rôder dehors la nuit.
 \item Aucun chat ne manque jamais de tuer les souris.
 \item Aucun animal ne s'attache jamais à moi, sauf ceux qui sont dans cette maison.
 \item Les panthères ne sont pas aptes à devenir des animaux familiers.
 \item Aucun animal non carnivore ne tue de souris.
 \item Je déteste les animaux qui ne s'attachent pas à moi.
 \item Les animaux qui vont rôder dehors la nuit aiment toujours contempler la lune.
 \end{enumerate}
\end{Ex}

\noindent Réponse : L'univers est \{ Les animaux\}.

$$\begin{array}{l l l}
Maison \imp Chats & C_1 : & \non Maison \ou Chats \\
Lune \imp Familier & C_2 : & \non Lune \ou Familier \\
Deteste \imp Evite & C_3 : & \non Deteste \ou Evite \\
Rode \ou \non Carnivore & C_4 : & Rode \ou \non Carnivore \\
Chats \imp Tuer & C_5 : & \non Chats \ou Tuer \\
Attache \imp Maison & C_6 : & \non Attache \ou Maison \\
Panthere \imp \non Familier & C_7 : & \non Panthere \ou \non Familier\\
\non Carnivore \imp \non Tuer & C_8 : & Carnivore \ou \non Tuer \\
\non Attache \imp Deteste & C_9 : & Attache \ou Deteste \\
Rode \imp Lune & C_{10} : & \non Rode \ou Lune\\
  \end{array}
$$


$$\begin{array}{l  l  l}
\{ C_2 , C_7 \} & \vdash \non Panthere \ou \non Lune & : C_{11} \\
\{ C_{11}, C_{2} \} & \vdash \non Panthere \ou \non Rode & : C_{12} \\
\{ C_{12} , C_{10} \} & \vdash \non Panthere \ou \non Carnivore & : C_{13} \\
\{ C_{13} , C_4 \} & \vdash \non Panthere \ou \non Tuer & : C_{14} \\
\{ C_{14} , C_8 \} & \vdash \non Panthere \ou \non Chats & : C_{15} \\
\{ C_{15} , C_5 \} & \vdash \non Panthere \ou \non Maison & : C_{16} \\
\{ C_{16} , C_1 \} & \vdash \non Panthere \ou \non Attache & : C_{17} \\
\{ C_{17} , C_6 \} & \vdash \non Panthere \ou \non Deteste & : C_{18} \\
\{ C_{18} , C_9 \} & \vdash \non Panthere \ou Deteste & : C_{19} \\
\{ C_{19} , C_3 \} & \vdash \non Panthere \ou Evite &  \\
  \end{array}
$$

\noindent Soit $Panthere \imp Evite$ : J'évite les panthères.

\begin{Ex}
Les exercices de logique...
 \begin{enumerate}
  \item Quand un étudiant résout un exercice de logique sans soupirer, vous pouvez être sûr qu'il le comprend.
 \item Ces exercices ne se présentent pas sous la forme habituelle.
 \item Aucun exercice facile ne donne mal à la tête.
 \item Les étudiants ne comprennent pas les exercices qui ne se présentent pas sous la forme habituelle.
 \item Les étudiants ne soupirent jamais devant un exercice de logique, à moins qu'il ne leur donne mal à la tête.
 \end{enumerate}

\end{Ex}


\noindent Réponse : L'univers est \{ Exercices \}.

$$\begin{array}{l l l}
\non Soupirent \imp Comprend & C_1 : & Soupirent \ou Comprend \\

Ces ~ exercices \imp \non Habituelle & C_2 : & \non Ces ~ exercices \ou \non Habituelle \\

Facile \imp \non Mal & C_3 : & \non Facile \ou \non Mal \\

\non Habituelle \imp \non Comprend & C_4 : & Habituelle \ou \non Comprend \\

\non Soupirent \ou Mal & C_5 : & \non Soupirent \ou Mal \\
  \end{array}
$$


$$\begin{array}{l  l  l}
\{ C_2 , C_4 \} & \vdash \non Ces ~ exercices \ou \non Comprend & : C_{6} \\
\{ C_{6}, C_{1} \} & \vdash \non Ces ~ exercices \ou Soupirent & : C_{7} \\
\{ C_{7} , C_{5} \} & \vdash \non Ces ~ exercices \ou Mal & : C_{8} \\
\{ C_{8} , C_3 \} & \vdash \non Ces ~ exercices \ou \non Faciles &  \\
  \end{array}
$$

\noindent Soit $Ces ~ exercices \imp \non facile$ : Ces exercices ne sont pas faciles.



\begin{Ex}
 Mes idées sur les chaussons aux pommes...
\begin{enumerate}
 \item Toute idée de moi qui ne peut s'exprimer sous forme de syllogisme est vraiment ridicule.
 \item Aucune de mes idées sur les chaussons aux pommes ne mérite d'être notée par écrit.
 \item Aucune idée de moi que je ne parviens pas à vérifier ne peut être exprimée sous forme de syllogisme.
 \item Je n'ai jamais d'idée vraiment ridicule sans la soumettre sous le champ à mon avocat.
\item Mes rêves (idées) ont tous trait aux chaussons aux pommes.
\item Je ne soumets aucune de mes idées à mon avocat si elle ne mérite pas d'être notée par écrit.
\end{enumerate}
\end{Ex}


\noindent Réponse : L'univers est \{ Idée \}.

$$\begin{array}{l l l}
Ridicule \imp Sullogisme & C_1 : & \non Ridicule \ou Syllogisme \\

Pomme \imp \non Ecrit & C_2 : & \non Pomme \ou \non Ecrit \\

\non Verifier \imp \non Syllogisme & C_3 : & \non Verifier \ou \non Syllogisme \\

\non Ridicule \imp Avocat & C_4 : & Ridicule \ou Avocat \\

Reves \imp Pomme & C_5 : & \non Reves \ou Pomme \\

Avocat \imp Ecrit & C_5 : & \non Avocat \ou Ecrit \\
  \end{array}
$$


$$\begin{array}{l  l  l}
\{ C_3 , C_1 \} & \vdash \non Verifier \ou \non Ridicule & : C_{7} \\
\{ C_{7}, C_{4} \} & \vdash \non Verifier \ou Avocat & : C_{8} \\
\{ C_{8} , C_{6} \} & \vdash \non Verifier \ou Ecrit & : C_{9} \\
\{ C_{9} , C_2 \} & \vdash \non Verifier \ou \non Pomme & C_{10} \\
\{ C_{10} , C_5 \} & \vdash \non Verifier \ou \non Reves &  \\
  \end{array}
$$

\noindent Soit $Reves \imp \non Verifier$ : Mes rêves ne sont pas vérifiés.


\begin{Ex}
 Les matières enseignées à l'IUT
\begin{enumerate}
 \item Aucune matière n'est primordiale, sauf l'ACSI.
 \item Toute matière enseignée par des professeurs dynamiques est susceptible de plaire aux étudiants.
 \item Je ne travaille pas les matières que je n'aime pas.
 \item Les seules matières intéressantes sont les matières informatiques.
 \item Aucune matière informatique n'évite l'abstraction.
 \item Aucune matière ne me réussit, excepté les matières intéressantes.
 \item Les mathématiques ne sont pas susceptibles de plaire aux étudiants.
 \item Aucune matière non primordiale ne tombe dans l'abstraction.
 \item Je n'aime pas les matières qui ne me réussissent pas.
 \item L'ACSI est enseignée par des professeurs dynamiques.
\end{enumerate}
\end{Ex}


\noindent Réponse : L'univers est \{ Matieres \}.

$$\begin{array}{l l l}
Primordiale \imp ACSI & C_1 : & \non Primordiale \ou ACSI\\
Dynamique \imp Plait & C_2 : & \non Dynamique \ou Plait\\
\non Aime \imp \non Travaille & C_3 : & Aime \ou \non Travaille\\
Interessante \imp Informatique & C_4 : & \non Interessante \ou Informatique \\
Informatique \imp Abstraction & C_5 : & \non Informatique \ou Abstraction \\
Reussit \imp Interessant & C_6 : & \non Reussit \ou Interessant \\
Maths \imp \non Plait & C_7 : & \non Maths \ou \non Plait \\
\non Primordial \imp \non Abstraction & C_8 : & Primordiale \ou \non Abstraction \\
\non Reussit \imp \non Aime & C_9 : & Reussit \ou \non Aime\\
ACSI \imp Dynamique & C_{10} : & \non ACSI \ou Dynamique \\
  \end{array}
$$


$$\begin{array}{l  l  l}
\{ C_7 , C_2 \} & \vdash \non Maths \ou \non Dynamique & : C_{11} \\
\{ C_{11}, C_{10} \} & \vdash \non Maths \ou \non ACSI & : C_{12} \\
\{ C_{12} , C_{1} \} & \vdash \non Maths \ou \non Primordiale & : C_{13} \\
\{ C_{13} , C_8 \} & \vdash \non Maths \ou \non Abstraction & : C_{14} \\
\{ C_{14} , C_5 \} & \vdash \non Maths \ou \non Informatique & : C_{15} \\
\{ C_{15} , C_4 \} & \vdash \non Maths \ou \non Interessant & : C_{16} \\
\{ C_{16} , C_6 \} & \vdash \non Maths \ou Reussit & : C_{17} \\
\{ C_{17} , C_9 \} & \vdash \non Maths \ou \non Aime & : C_{18} \\
\{ C_{18} , C_3 \} & \vdash \non Maths \ou \non Travaille &  \\
  \end{array}
$$

\noindent Soit $Maths \imp \non Travaille$ : Je ne travaille pas les maths.

\subsection{Exercices}

\begin{Exo}
 Les logiciens ne dorment pas beaucoup.
\begin{enumerate}
 \item Un logicien qui dîne de deux côtelettes de porc risque de se ruiner.
 \item Un joueur dont l'appétit n'est pas féroce risque de se ruiner.
 \item Un homme qui est déprimé parce qu'il est ruiné et qu'il risque de se ruiner à nouveau se lèbe toujours à cinq heures du matin.
\item Un homme qui ne joue pas et qui ne dîne pas de deux côtelettes de porc est assuré d'avoir un appétit féroce.
 \item Un homme dynamique qui se couche avant quatre heures du matin aurait intérêt à devenir conducteur de taxi.
 \item Un homme doué d'un appétit féroce, qui ne s'est pas ruiné et qui ne se lève pas à cinq heures du matin, dîne toujours de deux côtelettes de porc.
\item Un logicien qui risque de se ruiner aurait intérêt à devenir conducteur de taxi.
\item Un joueur convaincu, qui est déprimé bien qu'il ne soit pas ruiné, ne court aucun risque de se ruiner.
 \item Un homme qui ne joue pas et dont l'appétit n'est pas féroce est toujours dynamique.
 \item Un logicien dynamique, qui est véritablement convaincu, ne risque pas de se ruiner.
 \item Un homme doté d'un appétit féroce n'a nul besoin de devenir conducteur de taxi, s'il est véritablement convaincu.
\item Un joueur qui est déprimé et qui ne risque pas de se ruiner reste debout jusqu'à quatre heures du matin.
\item Un homme qui est ruiné et qui ne dîne pas de deux côtelettes de porc aurait intérêt à devenir conducteur de taxi ou à se lever à cinq heures du matin.
 \item Un joueur qui se couche avant quatre heures du matin n'a nul besoin de devenir conducteur de taxi, à moins qu'il ne soit doué d'un appétit féroce.
\item Un homme doué d'un appétit féroce, déprimé et qui ne risque nullement de se ruiner, est un joueur.
\end{enumerate}

\end{Exo}



\begin{Exo}
 Les gastronomes...
\begin{enumerate}
 \item Tous les agents de police du secteur aiment dîner avec notre cuisinière.
\item Aucun homme aux cheveux longs ne peut être autre chose que poète.
\item Je n'ai jamais fait de séjour en prison.
\item Les cousins de notre cuisinière aiment tous le gigot froid.
\item Seuls les agents de police du secteur sont poètes.
\item Les hommes aux cheveux courts ont tous fait un séjour en prison.
\end{enumerate}
\end{Exo}



\begin{Exo}
 Les programmeurs...
\begin{enumerate}
 \item Les étudiants se sentent abandonnés lorque les professeurs ne s'intéressent pas à eux
\item Les seuls étudiants en informatique se trouvent dans cet IUT.
\item Aucun étudiant ne peut écrire correctement un programme s'il n'a pas reçu une formation convenable.
\item Aucun étudiant de cet IUT n'est complètement nul.
\item Quand un étudiant se sent abandonné, il risque de sombrer dans la dépression.
\item Les professeurs ne s'intéressent pas aux étudiants que n'apprennent pas l'informatique.
\end{enumerate}
\end{Exo}




\section{Résolution avec variable}
On est ici en calcul des prédicats. On ne s'occupe que de clauses :

\begin{itemize}
\item symbole de prédicat, de variables, de constantes,
\item $\non$ et $\ou$ seulement,
\item pas de quantificateurs.
\end{itemize}

\subsection{Unification}

\subsubsection{Composants de substitutions et substitutions}

\begin{Def}[Composant de substitution]
Si $x$ est un symbole de variable et $t$ un terme du calcul des prédicats, $(x|t)$ est un \emph{composant de substitution} \index{composant de substitution} et indique la substitution de $x$ par $t$, dans une certaine formule.
\end{Def}

\begin{Ex}
$A = p(x,y,z) \ou r(x,u)$, où $x,y,z,u$ sont des symboles de variables, et $p,r$ des symboles de prédicats.

Substitution de $x$ par $a$ (symbole de constante) dans $A$ :
$$(x|a)A = p(a,y,z) \ou r(a,u)$$

On peut composer les composants de substitution (par exemple considérer $(y|b) (x|t) A$.
\end{Ex}
\begin{Rem}
L'ordre a de l'importance, la composition des composants de substitution n'est pas commutative.
\end{Rem}

\begin{Rem}
On ne peut substituer que des variables.
\end{Rem}

\begin{Notation}
La substitution identique est notée $[]$.
\end{Notation}


\begin{Ex}
Si $x,y$ sont des symboles de variable, alors

$$\left\{ \begin{array}{lr}
           p(x) & (x|y) p(x) = p(y) \\
           \non p(y) & \non p(y) \\
          \end{array} \right\} \vdash \square
$$

\noindent mais si $a,b$ sont des symboles de constante, alors :

$$\left\{ \begin{array}{l}
           p(a) \\
           \non p(b) \\
          \end{array} \right.
$$
... on ne peut rien conclure.

Par ailleurs, comme il n'y a plus de quantificateurs, toutes les variables sont libres et toutes les substitutions licites (c'est-à-dire une variable par un terme quelconque : constante, variable, groupe opératoire) sont possibles.
\end{Ex}


\subsubsection{Unificateurs}
\'Etant donnés deux clauses $A$ et $B$, on appelle unificateur de ces deux clauses toute substitution $s$ telle que $sA = sB$.

\bigskip
\begin{itemize}
 \item Pour deux formules quelconques, il n'existe pas forcément d'unificateur. Ainsi, pour $A = p(x)$ et $B = q(y)$ : comme les deux symboles sont différents, elles ne sont pas unifiables.

 \item L'unificateur, s'il existe, n'est pas unique. Ainsi, si $s$ est un unificateur de $A$ et $B$ ($sA = sB$) et si $s'$ est une substitution quelconque, alors $s's$ est aussi unificateur.

\item Si $s$ est un unificateur de $A$ et $B$, et que, pour tout unificateur $s'$ de $A$ et $B$, $s'$ peut se mettre sous la forme $s' = s''s$, où $s''$ est une substitution, alors $s$ est appelé \emph{le plus grand unificateur} \index{unificateur!le plus grand} de $A$ et de $B$ (ce dernier n'existe pas forcément).
\end{itemize}


\subsection{Résolution}

Dans le système \og RAV \fg (résolution avec variable) :

\begin{itemize}
\item Les formules sont des clauses du calcul des prédicats.

\item Il n'y a pas d'axiomes.

\item Deux règles d'inférences :
\begin{description}
 \item[résolution] $\{a \ou f, \non b \ou g \} \vdash \theta (\sigma f \ou g) \}$, avec $\sigma$ une substitution de renommage, destinée à faire qu'il n'y ait aucune variable commune entre $a \ou f$ et $\non b \ou g$, et $\theta$ un unificateur de $(\sigma a)$ et de $b$.

\item[diminution] $\{ a \ou b \ou f \} \vdash \sigma (b \ou f)$, où $\sigma$ : unificateur de $a$ et $b$.
 \end{description}

\end{itemize}


\begin{Ex}
 $\{ p(x) \ou p(y) \ou q(z) \} \vdash p(y) \ou q(z)$

$(x|y)$ est un unificateur de $p(x)$ et $p(y)$
\end{Ex}


\subsubsection{Quelques exemples d'applications (en RAV)}

\begin{Ex}
 $\{ p(x,c) \ou r(x), \non p(c,c) \ou q(x) \}$, avec :
\begin{itemize}
\item $p,q,r$ : symboles de prédicats.

\item $x$ : symbole de variable.

\item $c$ : symbole de constante.
\end{itemize}



La substitution de $x$ par $c$ :

 $\{ p(c,c) \ou r(c), \non p(c,c) \ou q(c) \} \vdash r(c) \ou q(c)$

\noindent est incorrect, car le renommage n'a pas été fait.

On commence donc par un renommage dans l'une des deux clauses (qui ne doivent plus avoir de variable commune) : par exemple dans $C_2$, $(x|y)$.

$$\{ p(x,c) \ou r(x), \non p(c,c) \ou q(y) \}$$

puis on substitue $(x|c)$ dans les deux clauses pour unifier $p(x,c)$ et $p(c,c)$.

$$\{ p(c,c)\ou r(x), \non p(c,c) \ou q(y) \} \vdash r(c) \ou q(y)$$
\end{Ex}



\begin{Ex}
$\{ p(x,f(a)), \non p (a,y) \ou r(f(y)) \}$, avec
\begin{itemize}
\item $p,r$ : symbole de prédicat

\item $f$ : symbole opératoire

\item $x,y$ : symbole de variable

\item $a$ : symbole de constante
\end{itemize}

Pas de renommage, car pas de variable communes.

$$(y|f(a))(x|a) \{p(a,f(a)); \non p(a,f(a)) \ou r(f(f(a))) \} \vdash r(f(f(a)))$$
\end{Ex}



\begin{Ex}
 $p(x,g(y)) \ou p(f(c),x) \ou r(x,y,z)$


$p,r$ : symbole de prédicat

$f,g$ : symbole opératoire

$x,y,z$ : symbole de variable

$c$ : symbole de constante

$$(z|g(y)) (x|f(c)) \{ p(x,g(y)) \ou p(f(c),x) \ou r(x,y,z)\} = p(f(c),g(y)) \ou idem \ou r(f(c),y,g(y)) \vdash p(f(c),g(y)) \ou r(f(c),y,g(y))$$
\end{Ex}


\begin{Ex}[Un exemple complet]
$C_1 = \non cr(y) \ou cv(f(y),y)$

$C_2 = \non cr(y) \ou \non cv(x,y) \ou ma(x)$
 
$C_3 = \non ar(x) \ou  ma(x)$

$C_4 = \non ma(x) \ou  \non ar(x) \ou \non cr(y) \ou \non cv(x,y)$

$C_5 = cr(a)$

$C_6 = \non ma(x) \ou ar(x)$ : mise sous forme de clause de la négation de la conclusion.

La conclusion est valide ssi on peut déduire la clause vide de cet ensemble de clauses.

$\{ C_5, (y|a) C_1 \} \vdash C_7 = cv(f(a),a)$

$\{ C_5, (y|a) C_2 \} \vdash C_8 = \non cv(x,a) \ou ma(x)$

$\{ C_5, (y|a) C_4 \} \vdash C_9 = \non ma(x) \ou \non ar(x) \ou \non cv(x,a)$

$\{C_7, (x|f(a)) C_8 \} \vdash C_{10} = ma(f(a))$

$\{C_7, (x|f(a)) C_9 \} \vdash C_{11} = \non ma(f(a)) \ou \non ar(f(a))$

$\{ C_{10}, C_{11} \} \vdash C_{12} = \non ar (f(a))$

$\{C_{10} , (x|f(a)) C_{6} \} \vdash C_{13} = ar (f(a))$

$\{C_{12} , C_{13} \} \vdash \square $ : la conclusion était valide.
\end{Ex}


\begin{Exo}
On considère les formules suivantes de \og PR \fg{}.
\begin{itemize}
\item $A_1 : \forall x \left(p(x) \imp q(f(x)) \right)$
\item $A_2 : \forall x \left(q(x) \imp p(f(x)) \right)$
\item $B : \forall x \left( \non p(x) \imp \ou \non p (f(f(f(f(x))))) \right)$
\end{itemize}
($p$ et $q$ sont des symboles de prédicats, $f$ est un symbole opératoire et $x$ est un symbole de variable.)

Il s'agit de prouver que la formule $B$ est la conclusion des formules $A_1$ et $A_2$. On mettra ces formules, ainsi que la négation de $B$, sous forme de clauses. On utilisera ensuite les règles d'inférence de \og RAV \fg{} pour déduire, si possible, la clause vide de cet ensemble de clauses.
\end{Exo}



\begin{Exo}
On considère l'ensemble de deux clauses $\{ p(x) \ou p(y), \non p(x) \ou \non p(y) \}$ ($p$ est un symbole de prédicat, $x$ et $y$ sont des symboles de variables).

Peut-on en déduire quelque chose et, si oui, quoi ?
\end{Exo}
\subsection{Stratégie de résolution}

\begin{description}
 \item[correction] Une stratégie de résolution est correcte quand elle ne trouve dans l'arbre des déductions la clause vide que lorsqu'elle est effective.
 \item[complétude] Une stratégie de résolution est complète quand elle conduit effectivement à la découverte de la clause vide (si elle figure dans l'arbre de déduction).
 \end{description}


\begin{Rem}
 Aucune stratégie à ce jour ne peut détecter l'absence de la clause vide dans l'arbre des déductions lorsqu'il est infini. Ce résultat est dû à l'indécidabilité du calcul des prédicats.
\end{Rem}


Deux problèmes :
\begin{enumerate}
 \item gestion de l'ensemble des clauses,
 \item parcours de l'arbre de déduction.
\end{enumerate}


\paragraph{Gestions de l'ensemble des clauses}

Saturation (avec simplification).

Préférences des clauses simples : permet d'avancer plus rapidement.

Stratégies de résolution :
\begin{itemize}
 \item gestion de l'ensemble des clauses
 \item gestion de l'arbre des déductions
\end{itemize}

Parcours de l'arbre :

\begin{itemize}
 \item En profondeur d'abord : rapide, facile à programmer, se perd dans des branches infinies (arrête au bout d'un certain temps
 \item En largeur d'abord : lent, difficile à programmer, nécessite une mémoire importante.
\end{itemize}


\paragraph{Choix d'un sous-arbre}

\begin{description}
 \item[déduction linéaire] On appelle déduction linéaire de racine $C$ toute suite de clause : $C_0, \hdots C_n$ telle que $C_0 = C$ et $\forall i, C_{i+1}$ est obtenue par déduction entre $C_1$ et une autre clause. C'est une stratégie correcte, mais incomplète. Si $F$ est un ensemble de clauses satisfiables, et si $F \cup \{C\}$ (une autre clause) est un ensemble de clauses insatisfiables, alors il existe une déduction linéaire de racine $C$ menant à la clause vide.
\item[déduction limitée aux entrées] (\og entrées \fg{} : clauses de départ) On appelle déduction limitée aux entrées de racine $C$ toute suite de clauses ($C_0, C_1, \hdots C_n$) telle que $C_0 = C$ et que pour $i>0, C_{i+1}$ est obtenue par déduction entre des clauses dont l'une est une entrée. Il n'y a pas de résultat analogue à celui énoncé pour les déductions linéaires, sauf dans un cas très particulier.
\end{description}


\subsection{Exemples complets de résolution}

\subsubsection{La méthode de résolution}



Pour ces divers exercices, on demande le travail suivant :

\begin{enumerate}
 \item Mettre les diverses propositions sous forme de \og PR \fg{} (on rappelle que cette traduction doit être littérale, c'est-à-dire qu'elle ne doit pas être l'occasion de commencer à \og tirer des conclusions \fg{}).

\item Mettre les formules obtenues, ainsi que la négation de la conclusion proposée, sous forme de clauses (numérotées)

\item Utiliser la stratégie de \og préférence des clauses simples \fg{} pour décider si la conclusion est valide ou non. 

On présentera la résolution de manière très claire : des numéros seront affectés aux clauses, les déductions seront explicites, par exemple :

$$((x|a) C_i, C_k) \vdash C_n, \textrm{ avec } C_n = \hdots$$

On supprimera au fur et à mesure les clauses subsumées, en indiquant, par exemple,

\begin{center}
 La clause $C_i$ est subsumée par la clause $C_k$.
\end{center}

\end{enumerate}

\subsubsection{Les exemples complets}

Ils vont venir...

\subsection{Exercices}



\begin{Exo}
On considère les propositions suivantes :
\begin{itemize}
\item Il arrive que des programmes tournent.
\item Tout programme qui tourne est écrit par un programmeur.
\item Seuls les programmeurs compétents écrivent des programmes qui tournent.
\item Les programmeurs compétents qui ne sont pas engagés n'ont pas l'occasion d'écrire des programmes qui tournent.
\item On n'engage que des programmeurs compétents.
\end{itemize}
On désire vérifier que la conclusion suivante est correcte :
\begin{itemize}
\item Certains programmeurs compétents sont engagés.
\end{itemize}
\end{Exo}

\begin{Exo}
 Les exercices de logique...

\begin{itemize}
 \item Aucun exercice de logique n'est intéressant.
 \item Certains exercices de logique ne sont pas intéressants.
\end{itemize}
\noindent On désire vérifier que la conclusion suivante est valide :
\begin{itemize}
 \item Quelques exercices de logique ne sont pas mathématiques.
\end{itemize}
\end{Exo}



\begin{Exo}
 La logique est difficile...
\begin{itemize}
 \item Tous ceux qui comprennent la logique peuvent se passer de dormir.
\item Certains étudiants ne peuvent pas se passer de dormir.
\end{itemize}
\noindent On désire vérifier que la conclusion suivante est valide :
\begin{itemize}
 \item Certains étudiants ne comprennent pas la logique.
\end{itemize}
\end{Exo}


\begin{Exo}
 Encore les exercices...
\begin{itemize}
 \item Certains exercices sont franchement de mauvais goût.
\item Les étudiants aiment tout ce qui est de bon goût.
\end{itemize}
\noindent On désire vérifier que la conclusion suivante est valide :
\begin{itemize}
 \item Il y a certains exercices que les étudiants n'aiment pas.
\end{itemize}

\end{Exo}




\begin{Exo}
 Les professeurs...
\begin{itemize}
\item Certaines personnes instruites manquent de générosité.
\item Tous les professeurs sont généreux.
\end{itemize}
\noindent On souhaite vérifier que la conclusion suivante est valide :
\begin{itemize}
 \item Les professeurs ne sont pas des personnes instruites.
\end{itemize}

\end{Exo}




\begin{Exo}
Les étudiants de première année d'informatique sont répartis en six groupes, du groupe A au groupe F.

Chacun de ces groupes est subdivisé en deux sous-groupes ($A_1$, $A_2$, $B_1$, $B_2$, etc. )

Pour l'élaboration de l'emploi du temps du second semestre, les contraintes suivantes doivent être respectées :
\begin{itemize}
\item Si $A_1$ et $A_2$ suivent la même matière, s'il en est de même pour $B_1$ et $B_2$, et si $E_1$ suit la même que $F_2$, $C_1$ doit suivre la même que $D_2$.
\item Si $A_1$ et $A_2$ suivent la même matière, s'il en est de même pour $F_1$ et $F_2$, et si $B_1$ suit la même que $C_2$, $D_1$ ne peut pas suivre la même que $E_2$.
\item Si $C_1, C_2, D_1$ et $D_2$ suivent la même matière, et si $A_1$ ne suit pas la même matière que $B_2$, $E_1$ ne peut pas suivre la même que $F_2$.
 \item Si $A_1$ et $A_2$ suivent la même matière, s'il en est de même pour $D_1$ et $D_2$, et si $B_1$ ne suit pas la même que $C_2$, $E_1$ doit suivre la même que $F_2$. 
 \item Si $E_1$ et $E_2$ suivent la même matière, s'il en est de même pour $F_1$ et $F_2$, et si $C_1$ suit la même que $D_2$, $A_1$ doit suivre la même que $B_2$.
\item Si $B_1, B_2,  C_1$ et $C_2$ suivent la même matière, et si $E_1$ ne suit pas la même matière que $F_2$, $D_1$ doit suivre la même que $E_2$.
\end{itemize}
\noindent On souhaite vérifier que la conclusion suivante est valide :
\begin{itemize}
 \item A tout instant de la journée, il y aura un groupe au moins dont les deux sous-groupes ne suivront pas la même matière.
\end{itemize}
On pourra utiliser le prédicat $mm(x,y)$ qui signifie que le sous-groupe $x_1$ suit la même matière que le sous groupe $y_2$, et les symboles de CONSTANTES $a,b,c,d,e$ et $f$ qui représentent les groupes. 
\end{Exo}



\begin{Exo}
 Les intellectuels achètent des livres...
\begin{itemize}
\item Il y a des livres.
\item Certains intellectuels jouent en bourse.
 \item Seuls les intellectuels lisent des livres.
 \item Seuls les intellectuels se ruinent en jouant en bourse.
 \item Tout livre a un lecteur.
 \item Les intellectuels ruinés ne lisent pas de livres.
\end{itemize}
\noindent On souhaite vérifier que la conclusion suivante est valide :
\begin{itemize}
 \item Certains intellectuels ne sont pas ruinés.
\end{itemize}

\end{Exo}


\begin{Exo}
 Les châtelains sont riches...
\begin{itemize}
\item On ne prête qu'aux riches.
\item Il y a des châteaux.
 \item Les gens riches qui ont contracté un prêt ne possèdent pas de châteaux.
\item Seuls les gens riches sont propriétaires de châteaux.
\item Tous les châteaux ont des propriétaires.
\end{itemize}
\noindent On souhaite vérifier que la conclusion suivante est valide :
\begin{itemize}
 \item Tous les gens riches ne recourent pas à l'emprunt.
\end{itemize}

\end{Exo}






\section{Clauses de Horn}

\subsection{Définition}
Une clause de Horn est une clause ne comportant qu'un seul littéral positif.


\begin{Rem}
 ...donc de la forme $p \ou \non q_1 \ou \hdots \ou \non q_n = p \ou \non (q_1 \et \hdots \et q_n )$ : de la forme $\non Q ou P$, c'est-à-dire $P \imp Q$.
\end{Rem}

\subsection{Déduction ordonnée}

Une déduction est dite ordonnée quand elle porte sur le littéral de tête (entre deux clauses).

\subsection{Le résultat évoqué dans le paragraphe précédent}

Si $F$ est un ensemble de clauses de Horn ordonnées satisfiables, si $C$ est une clause ne comportant que des littéraux négatifs, et que $T \cup \{C\}$ est insatisfiable, alors il existe une déduction limitée aux entiers et ordonnée de racine $C$ qui conduit à la clause vide.

\gsaut
\centerline{\x{Fin du Chapitre}}