partie5.tex

\section{Algorithme de preuve}
\label{algorithmeprop}

% \subsection{Exemple de preuve propositionnelle}
% 
% \noindent Voici les propositions premières : \\
% A : tu manges bien \\
% B : ton système digestif est en bonne santé \\
% C : tu pratiques une activité physique régulière \\
% D : tu es en bonne forme physique \\
% E : tu vis longtemps \\
% 
% \noindent On peut maintenant faire une théorie et on espère qu'elle aura un modèle. \\
% A$\Rightarrow$B, C$\Rightarrow$D, B$\lor$D $\Rightarrow$ E, $\lnot$E
% \\
% \noindent On aimerait prouver que $\lnot$A $\land$ $\lnot$C est vrai.\\
% 
% \noindent Preuve : \\
% \\
% \begin{tabular}{|l|l|}
% \hline
% 1. A$\Rightarrow$B & prémisse \\
% 2. C$\Rightarrow$D & prémisse \\
% 3. B$\lor$D $\Rightarrow$E & prémisse \\
% 4. $\lnot$E & prémisse \\ 
% \indent 5. A & hypothèse \\
% \indent 6. B & modus ponens (1) \\
% \indent 7. B$\lor$D & addition (6) \\
% \indent 8. E & modus ponens (7) \\
% 9. $\lnot$A & preuve indirecte \\
% \indent 10. C & hypothèse \\
% \indent 11. D & modus ponens (2) \\
% \indent 12. D$\lor$B & addition (11) \\
% \indent 13. B$\lor$D & commutativité (12)\\
% \indent 14. E & modus ponens (9) \\
% 15. $\lnot$C & preuve indirecte \\
% 16. $\lnot$A $\land$ $\lnot$C & conjonction (9,15) \\
% \hline
% \end{tabular}\\
% 
% Grâce à la déduction on a donc pu prouver que tu ne manges pas bien et que tu ne pratiques pas d'activité physique régulière. 
% On aimerait maintenant pouvoir automatiser les preuves quand elles existent. Mais il faut savoir s'il peut tout résoudre ou pas. 
% On va donc construire un algorithme nous permettant de résoudre automatiquement les preuves en logique propositionnelle.

Nous allons maintenant introduire un algorithme qui permet de trouver
une preuve en logique propositionnelle.
Cet algorithme est une automatisation de la {\em démonstration par l'absurde}
qui est basé sur une seule règle d'inférence, la {\em résolution}.

\subsection{Transformation en forme normale conjonctive}
\label{fnc}

Toute formule peut être transformée en une formule équivalente, la forme normale conjonctive,
qui a toujours la même forme.
La forme normale conjonctive facilite la manipulation des formules nécessaire
par l'algorithme de preuve.

\subsubsection{Forme normale conjonctive}

Il y a deux formes normales qui sont souvent utilisées:
la forme normale conjonctive (FNC) et la forme normale disjonctive (FND).
Pour l'algorithme de preuve, nous allons utiliser la FNC, mais comme la FND est parfois importante,
nous les définissons toutes les deux.
Dans la FNC, la formule est écrite comme une conjonction de disjonctions.
Dans la FND, la formule est écrite comme une disjonction de conjonctions.
À l'intérieur de chaque forme normale on trouve des propositions premières ou des négations des propositions premières.
Voici un exemple de chaque forme normale:
\begin{itemize}
  \item FNC: $( P \lor \lnot Q ) \land ( Q \lor A ) \land ( \lnot S \lor R )$  
  \item FND: $( P \land \lnot Q ) \lor ( Q \land A ) \lor ( \lnot S \land R )$  
\end{itemize}
Pour faciliter la discussion autour des formes normales, nous introduisons une terminologie:
\begin{itemize}
\item Un {\em littéral}, écrit $L$, est où une proposition première où la négation d'une proposition première.
Pour une proposition première $P$ on peut faire deux littéraux,
$P$ et $\lnot P$.
\item Une {\em clause}, écrite $C$, est (pour la forme normale conjonctive) une disjonction de littéraux.
On écrit $\lor L_i$ ou $( L_1 \lor L_2 \lor L_3 \lor ... \lor L_i )$.
\end{itemize}

\subsubsection{L'algorithme de normalisation}

L'algorithme de normalisation se fait en quatre phases:
\begin{enumerate}
\item Eliminer les $\rightarrow$ et $\leftrightarrow$ en les remplaçant par des formules équivalentes.  Par exemple, $p \rightarrow q$ sera remplacée par $\lnot p \lor q$.
\item Déplacer les négations vers l'intérieur (jusqu'à dans les propositions premières) en utilisant les formules de De Morgan.
\item Déplacer les disjonctions ($\lor$) vers l'intérieur en utlisant les lois distributives.
\item Simplifier en éliminant les formes $(P \lor \lnot P)$ dans chaque disjonction.
\end{enumerate}

\subsubsection{Exemple de normalisation}

\begin{align*}
& (P \rightarrow (Q \rightarrow R)) \rightarrow ((P \land S) \rightarrow R) \\
& \lnot (\lnot P \lor (\lnot Q \lor R)) \lor (\lnot (P \land S) \lor R) \\
& ( \lnot \lnot P \land \lnot (\lnot Q \lor R)) \lor ((\lnot P \lor \lnot S) \lor R) \\
& (P \land (Q \land \lnot R)) \lor ( \lnot P \lor \lnot S \lor R) \\
& (P \lor \lnot P \lor \lnot S \lor R) \land ( Q \lor \lnot P \lor \lnot S \lor R) \land (\lnot R \lor \lnot P \lor \lnot S \lor R) \\
& (Q \lor \lnot P \lor \lnot S \lor R) 
\end{align*}

\subsection{La résolution}

On veut quelque chose de simple, sans toutes les règles que nous avons vues auparavant, mais le plus puissant possible. Nous n'utiliserons qu'une seule règle : la \textbf{résolution}. On peut faire des résolutions de preuves propositionnelles rien qu'en ayant cette règle. Cette règle utilise la forme normale conjonctive. 
On utilise les preuves indirectes (preuves par l'absurde), car c'est le plus simple.
\\
Commençons par un exemple de résolution.

\subsubsection{Exemple de résolution}

\noindent Prenons comme propositions premières :\\

\noindent P$_{1}$ : il neige \\
P$_{2}$ : la route est dangereuse \\
P$_{3}$ : on prend des risques \\
P$_{4}$ : on va vite \\
P$_{5}$ : on va lentement \\
P$_{6}$ : on prend le train \\


\noindent $\left.
\begin{array}{l}
$1. P$_{1}$ $\Rightarrow$ P$_{2}$ $ \\
$2. P$_{2}$ $\Rightarrow$ $\lnot$P$_{3}$ $ \\
$3. P$_{4}$ $\Rightarrow$ P$_{3}$ $\lor$   P$_{6}$ $ \\
$4. P$_{4}$ $\lor$ P$_{5}$ $ \\
$5. P$_{1}$ $ \\
\end{array}
\right\rbrace$ B : notre théorie \\
\\
On va utiliser B + modus ponens + résolution. \\
\\
\begin{tabular}{|l|l|}
\hline
1. P$_{1}$ $\Rightarrow$ P$_{2}$&  \\
2. P$_{2}$ $\Rightarrow$ $\lnot$P$_{3}$ & \\
3. P$_{4}$ $\Rightarrow$ P$_{3}$ $\lor$ P$_{6}$ & 1-5 : B : notre théorie que l'on utilise comme prémisse\\
4. P$_{4}$ $\lor$ P$_{5}$ & \\
5. P$_{1}$ & \\
3'. $\lnot$P$_{3}$ $\Rightarrow$ $\lnot$P$_{4}$ $\lor$ P$_{6}$ & réécriture de 3 \\
6. P$_{2}$ & modus ponens (1,5) \\
7. $\lnot$P$_{3}$ & modus ponens (6,2) \\
8. $\lnot$P$_{4}$ $\lor$ P$_{6}$ & modus ponens (7,3') \\
9. P$_{5}$ $\lor$ P$_{6}$ & résolution (4,8) \\
\hline
\end{tabular}\\
\\

La ligne 3 n'étant pas symétrique, nous pouvons la transformer pour obtenir une proposition symétrique et donc choisir le membre qui est à gauche de l'implication. Pour rappel, P$_{4}$ $\Rightarrow$ P$_{3}$ $\lor$ P$_{6}$ peut être réécrit  : $\lnot$P$_{4}$ $\lor$ P$_{3}$ $\lor$ P$_{6}$ (loi de l'implication), qui est logiquement équivalent à $\lnot$P$_{3}$ $\Rightarrow$ $\lnot$ P$_{4}$ $\lor$ P$_{6}$ (loi de l'implication). C'est de cette manière que nous avons obtenu la ligne 3'.\\

On peut fusionner les lignes 4 et 8 grâce à la résolution. La \textbf{résolution} est une règle qui prend deux disjonctions avec une proposition première et sa négation, et qui les fusionne en retirant cette proposition première. On peut prouver que cela fonctionne de plusieurs manières.\\ 
Par exemple : si P$_{4}$ est vrai, P$_{6}$ doit être vrai. Si P$_{4}$ est faux, P$_{5}$ doit être vrai. Donc on sait que P$_{5}$ ou P$_{6}$ doit être vrai car on sait que dans tous les cas de figure, c'est soit l'un soit l'autre qui doit être vrai. 


\subsubsection{Principe de résolution}
\noindent p$_{1}$ $\lor$ q \\
\noindent p$_{2}$ $\lor$ $\lnot$q \\
\rule{3cm}{0.4pt} \\
p$_{1}$ $\lor$ p$_{2}$
\\

Cette règle représente la base de l'algorithme de résolution.
On peut la vérifier en utilisant le métalangage.
Nous allons voir que cette règle sera utilisée aussi dans la logique des prédicats. 

\subsubsection{La résolution préserve les modèles}
\noindent Tout ce qui est modèle des deux premières disjonctions sera aussi modèle de la résultante. \\

\noindent $p$ : $\bigwedge\limits_{1 \leq i \leq n}$ C$_{i}$ \indent   \indent \indent \indent C$_{i}$ : disjonction : $\bigvee\limits_{1 \leq j \leq n}$ L$_{j}$ \indent  \{C$_{1}$, ..., C$_{n}$\}\\

\noindent C$_{1}$, C$_{2}$ = deux disjonctions \\

\noindent On doit prouver : \{C$_{1}$, ..., C$_{n}$\} $\models$ $r$ avec  $r$ = C$_{1}$ - \{P\} $\lor$ C$_{2}$ - \{$\lnot$P\}. $r$ est une nouvelle disjonction à partir de deux autres disjonctions. On doit prouver que $r$ est toujours vrai.\\

\noindent On considère que P est dans C$_{1}$ et que $\lnot$P est dans C$_{2}$.\\
\\
Pour prouver cela, on utilise la sémantique. On fait une preuve en métalangage, ce n'est pas formalisé. \\
Val$_{I}$(P) =
$\left\lbrace
\begin{array}{l}
T \\
F \\
\end{array}
\right.$ 

Dans les deux cas de figure, on doit démontrer que quand on a un modèle, une interprétation qui rend vrai $p$, le $r$ sera vrai aussi. Si P est vrai alors $\lnot$P est faux, donc C$_{2}$ sera vrai et donc $r$ sera vrai. Quand P est faux, le C$_{1}$ doit être vrai, donc $r$ est vrai. $r$ est donc vrai dans les deux cas. 

\subsection{Algorithme}

Prenons des axiomes $C_{i}$ qui sont normalisés:
\begin{align*}
C_{i} = \bigvee\limits_{i} L_{i} \\
L_{i} = P \mbox{ ou } \lnot P
\end{align*}
et un candidat théorème C à démontrer.
Nous voulons donc démontrer:
\begin{align*}
& \{C_{i}, ..., C_{n}\} \vdash C
\end{align*}
C'est-à-dire, qu'il existe une preuve avec les règles d'inférence $\{C_{i}, ..., C_{n}\}$ tel qu'on obtient $C$.
Nous savons que 
$\{C_{i}, ..., C_{n}\} \models C$ ssi $\{C_{i}, ..., C_{n}, \lnot C\} \models \false$.
Il suffit donc de démontrer que
$S = \{C_{i}, ..., C_{n}, \lnot C\}$ est inconsistant.
Pour arriver à cela, nous allons combiner des éléments de S avec la résolution,
jusqu'à que l'on arrive sur le résultat $\false$ ou qu'il n'y a plus de possibilités d'utiliser la résolution.
Dans le premier cas, nous avons prouvé $C$.
Dans le deuxième cas, il n'existe pas de preuve de $C$.

\subsubsection{Pseudocode}

\begin{algorithm}[H]
\While{$false \not\in S$ et $\exists$? clauses résolvables non résolues}{
	\begin{itemize}
		\item choisir $C_1,C_2 \in S$ tel que $\exists P \in C_1, \lnot P \in C_2$ 		
		\item calculer r:=$C_1 - \{P\} \lor C_2 - \{\lnot P\}$
		\item calculer S:= $S \cup \{r\}$
	\end{itemize}
}
\eIf{$false \in S$}{C est prouvé}{C n'est pas prouvé}
\end{algorithm}


La subtilité de cet algorithme est de choisir correctement les clauses C$_{1}$ et C$_{2}$ car l'efficacité de l'algorithme en dépend. 

\subsection{Exemples}

\subsubsection{Exemple 1}
\begin{tabbing}
\hspace{3cm}\=\hspace{2cm}\=\kill
C$_{1}$ : P $\lor$ Q \\
C$_{2}$ : P $\lor$ R \\
C$_{3}$ : $\lnot$Q $\lor$ $\lnot$R \\
C : P \> \> \{C$_{1}$,C$_{2}$,C$_{3}$,$\lnot$C\} \\
\end{tabbing}

\noindent \emph{Quelques pas de résolution :}

\noindent C$_{1}$ + $\lnot$C $\rightarrow$  Q (C$_{5}$) \newline
C$_{2}$ + $\lnot$C $\rightarrow$ R  (C$_{6}$) \newline
C$_{3}$ + C$_{5}$ $\rightarrow$ $\lnot$R (C$_{7}$) \newline 
C$_{6}$ + C$_{7}$ $\rightarrow$ \underline{false} ($\in$ S donc C est prouvé) \newline

\subsubsection{Exemple 2}
\noindent p$_{1}$ : Mal de tête $\land$ Fièvre $\Rightarrow$ Grippe \newline
p$_{2}$ : Gorge blanche $\land$ Fièvre $\Rightarrow$ Angine \newline
p$_{3}$ : Mal de tête \newline
p$_{4}$ : Fièvre\newline

\noindent \underline{Algorithme}
\begin{itemize}
\item{Normalisation en forme normale}
\item{Pseudocode avec résolution}
\end{itemize}
Question : Grippe ?

\subsection{Conclusion}
Nous pouvons tirer des conclusions sur la logique des propositions et sur notre algorithme.

Pour toute théorie $B = \left\{c_1, \dots, c_n \right\}$ et $p$,
\begin{itemize}
\item si $B \vdash p$ alors $B \models p$ (Adéquat - \textit{Soundness}) ;
\item si $B \models p$ alors $B \vdash p$ (Complet - \textit{Completeness}) ;
\item $\forall$ $B, p$, l'exécution de l'algorithme se termine après un nombre fini d'étapes. (Décidable - \textit{Decidable})
\end{itemize}

Cet algorithme est très puissant mais n'est pas toujours très efficace. Par contre, quoi qu'il arrive, on peut au moins être sûr qu'il s'arrêtera toujours à un moment.

La logique des propositions n'est malheureusement pas très expressive. Elle ne permet pas de relations entre les propositions. 
Nous allons essayer d'appliquer la même démarche mais avec une logique plus puissante : la logique des prédicats. 
Il n'est par contre pas possible d'arriver à un algorithme aussi puissant avec la logique des prédicats, la logique étant trop forte.