partie3-5.tex

\chapter{Preuves en logique propositionnelle}
\label{preuveprop}
		Une preuve est un raisonnement déductif qui démontre si une proposition
est vraie ou fausse.
On distingue des preuves informelles et des preuves formelles.
Une preuve informelle est un raisonnement en langage naturel, parfois augmenté avec des
notations mathématiques.
Une preuve formelle est un objet mathématique qui formalise le raisonnement déductif.
Un des buts de la logique mathématique est de prouver le plus possibles des résultats
mathématiques avec des preuves formelles.

Au 20ème siècle les mathématiciens sont arrivés à prouver la plupart des mathématiques
classiques (telles qu'utilisées par des ingénieurs) avec des preuves formelles.
Un des résultats les plus célèbres est la preuve formelle du théorème des quatre couleurs,
fait par Georges Gonthier et Benjamin Werner avec l'assistant de preuve Coq (un logiciel
qui automatise la plupart des manipulations formelles nécessaires).
Ce théorème dit que toute carte découpée en régions connexes peut être colorée avec seulement
quatre couleurs, de sorte que deux régions adjacentes ont toujours des couleurs distinctes.

Dans ce chapitre nous allons définir des preuves formelles pour la logique propositionnelle.
Nous présenterons trois approches:
		\begin{itemize}
			\item Table de vérité
			\item Preuve transformationnelle
			\item Preuve déductive (la plus générale)		
		\end{itemize}

		\section{Preuve avec table de vérité}
La preuve formelle la plus simple est une table de vérité.
			\newcolumntype{x}{>{\itshape\bfseries}c}
		Prouvons que $\lnot (P \land Q) \Leftrightarrow (\lnot P \lor \lnot Q)$ est vrai :
			\begin{center}
			\begin{tabular}{cc|ccxcx}
			$P$ & $Q$ & $\lnot P$ & $\lnot Q$ & $(\lnot P \lor \lnot Q)$ & $P \land Q$ & $ (\lnot P \lor \lnot Q)$\\
			\hline
			F&F&T&T&T&F&T\\
			T&F&F&T&T&F&T\\
			F&T&T&F&T&F&T\\
			T&T&F&F&F&T&F\\
			\end{tabular}
			\end{center}

On peut constater que le vecteur de vérité de $\lnot (P \land Q)$ est équivalent à celui de $(\lnot P \lor  \lnot Q)$. La preuve a donc vérifié la véracité de la proposition.
Notez qu'une table de vérité est un objet mathématique en métalangage
parce qu'elle n'est pas une proposition.

L'inconvénient de cette méthode de preuve est qu'elle devient rapidement très lourde quand le nombre de propositions premières augmente. Il faut en effet $2^n$ lignes dans la table pour $n$ propositions. 

\section{Preuve transformationnelle} \label{transfo_propositionelle}

Une preuve transformationnelle est une séquence de transformations
$p_1 \Lleftarrow \Rrightarrow p_2 \Lleftarrow \Rrightarrow \cdots \Lleftarrow \Rrightarrow p_n$,
dans laquelle on a toujours $p_i \Lleftarrow \Rrightarrow p_{i+1}$
(équivalence logique entre éléments adjacents dans la séquence).
Une preuve transformationnelle est aussi un objet mathématique en métalangage.
Pour faciliter la création d'une preuve transformationnelle,
on utilise des "Lois", c'est-à-dire des équivalences connues.
			\begin{center}
			\begin{tabular}{|ll|}
			\hline
			$p \Lleftarrow \Rrightarrow p \lor p$ & Idempotence\\
			$p \lor q \Lleftarrow \Rrightarrow q \lor p$ & Commutativité\\
			$(p \lor q) \lor r \Lleftarrow \Rrightarrow p \lor (q \lor r)$ & Associativité\\
			$ \lnot \lnot p \Lleftarrow \Rrightarrow p$ & Double Négation\\
			$p \Rightarrow q \Lleftarrow \Rrightarrow \lnot p \lor q$ & Implication\\
			$\lnot (p \land q) \Lleftarrow \Rrightarrow \lnot p \lor \lnot q$ & $1^{ere}$ loi de De Morgan\\
			$p \Leftrightarrow q \Lleftarrow \Rrightarrow (p \Rightarrow q) \land (q \Rightarrow p)$ & Équivalence\\
			\hline
			\end{tabular}
			\end{center}
On ajoute deux règles supplémentaires : la transitivité et la substitution.
			\subsection*{Transitivité de l'équivalence}
			\indent Si $p \Lleftarrow \Rrightarrow q$ et $q \Lleftarrow \Rrightarrow r$, alors $p \Lleftarrow \Rrightarrow r$.
			\subsection*{Substitution}
			Il est autorisé de remplacer une formule par une formule équivalente à l’intérieur d’une autre formule. Autrement dit : \\
			\indent Soit p,q,r des formules propositionnelles.\\
			\indent Si $p \Leftrightarrow q$ et $r(p)$, alors $r(p) \Lleftarrow \Rrightarrow r(q)$.\\
			On peut remplacer $p$ par $q$ car elles sont équivalentes. 
			
			
			\subsection*{Exemple}
			On veut prouver : $p \land (q \land r) \Lleftarrow \Rrightarrow (p \land q) \land r$
			\begin{center}
			\begin{tabular}{ll}
			
			$p \land (q \land r)$ & $\Lleftarrow \Rrightarrow p \land \lnot \lnot (q \land r)$\\
			& $\Lleftarrow \Rrightarrow p \land \lnot (\lnot q \lor \lnot r)$\\
			& $\Lleftarrow \Rrightarrow \lnot \lnot (p \land \lnot (\lnot q \lor \lnot r))$\\
			& $\Lleftarrow \Rrightarrow \lnot (\lnot p \lor \lnot \lnot (\lnot q \lor \lnot r))$\\
			& $\Lleftarrow \Rrightarrow \lnot (\lnot p \lor (\lnot q \lor \lnot r))$\\
			& $\Lleftarrow \Rrightarrow \lnot ((\lnot p \lor \lnot q) \lor \lnot r)$\\
			&$\vdots$\\
			& effectuer les mêmes lois dans le sens contraire \\
			&$\vdots$\\
			& $\Lleftarrow \Rrightarrow (p \land q) \land r$\\
			\end{tabular}
			\end{center}
Le problème de cette méthode de preuve est qu'elle requiert de l'intuition, de la créativité. Elle n'est donc pas forcément plus efficace que les tables de vérité, surtout si "l'astuce" est difficile à trouver.
		
\section{Preuve déductive}

Une preuve déductive est un objet mathématique qui formalise une séquence
de pas de raisonnement simples.
Chaque pas doit être justifié avec le nom de la règle ou la loi qui est utilisée.
Les pas utilisent trois techniques de raisonnement différentes:
les équivalences logiques, les règles d'inférence et les schémas de preuve.
Avec ces techniques,
une preuve déductive est beaucoup plus expressive qu'une preuve transformationnelle.

\subsection{Equivalences logiques}
			\begin{center}
			\begin{tabular}{ll}
			$p \lor q \Lleftarrow \Rrightarrow q \lor p$ & Commutativité de $\lor$\\
			$p \land q \Lleftarrow \Rrightarrow q \land p$ & Commutativité de $\land$\\
			$p \Leftrightarrow q \Lleftarrow \Rrightarrow q \Leftrightarrow p$ & Commutativité de $\Leftrightarrow$\\

			$(p \lor q) \lor r \Lleftarrow \Rrightarrow p \lor (q \lor r)$ & Associativité de $\lor$\\
			$(p \land q) \land r \Lleftarrow \Rrightarrow p \land (q \land r)$ & Associativité de $\land$\\

			$(p \land q) \lor r \Lleftarrow \Rrightarrow (p \lor r) \land (q \lor r)$ & Distributivité de $\lor$\\
			$(p \lor q) \land r \Lleftarrow \Rrightarrow (p \land r) \lor (q \land r)$ & Distributivité de $\land$\\
			\\

			$p \Lleftarrow \Rrightarrow p \lor p$ & Idempotence de $\lor$\\
			$p \Lleftarrow \Rrightarrow p \land p$ & Idempotence de $\land$\\

			$ \lnot \lnot p \Lleftarrow \Rrightarrow p$ & Double Négation\\
			$p \lor \lnot p \Lleftarrow \Rrightarrow true$ & Tiers exclu\\
			$p \land \lnot p \Lleftarrow \Rrightarrow false$ & Contradiction\\
			$p \Rightarrow q \Lleftarrow \Rrightarrow \lnot p \lor q$ & Implication\\
			$p \Rightarrow q \Lleftarrow \Rrightarrow \lnot q \Rightarrow \lnot p$ & Contraposée\\
			$p \Leftrightarrow q \Lleftarrow \Rrightarrow (p \Rightarrow q) \land (q \Rightarrow p)$ & Équivalence\\

			$\lnot (p \land q) \Lleftarrow \Rrightarrow \lnot p \lor \lnot q$ & $1^{ere}$ loi de De Morgan\\
			$\lnot (p \lor q) \Lleftarrow \Rrightarrow \lnot p \land \lnot q$ & $2^{eme}$ loi de De Morgan\\
			\\

			$p \land true \Lleftarrow \Rrightarrow p$ & Simplification\\
			$p \lor true \Lleftarrow \Rrightarrow true$ & Simplification\\
			$p \land false \Lleftarrow \Rrightarrow false$ & Simplification\\
			$p \lor false \Lleftarrow \Rrightarrow p$ & Simplification\\
			$p \lor (p \land q) \Lleftarrow \Rrightarrow p$ & Simplification\\
			$p \land (p \lor q) \Lleftarrow \Rrightarrow p$ & Simplification\\
			\end{tabular}
			\end{center}

\subsection{Règles d'inférence}

À la différence de la preuve transformationnelle, les règles d'inférences ont une direction : elles commencent par les prémisses et se terminent par la conclusion.
Pour chaque règle, si les prémisses sont vraies, alors la conclusion est vraie.
Nous utilisons un raisonnement informel pour justifier chaque règle.

\begin{center}
	\begin{tabular}{ccc}
		Conjonction & Simplification & Addition\\
		\begin{tabular}{c}
			p\\
			q\\
			\hline
			$p\land q$
		\end{tabular}
		&
		\begin{tabular}{c}
			$p \land q$ \\
			\hline
			$p$\\
		\end{tabular}
		&
		\begin{tabular}{c}
			$p $ \\
			\hline
			$p \lor q$\\
		\end{tabular}
		\\

		Contradiction & Double Négation & Transitivité de l'équivalence\\
		\begin{tabular}{c}
			$p$ \\
			$\lnot p$\\
			\hline
			$q$\\
		\end{tabular}
		&
		\begin{tabular}{c}
			$\lnot \lnot p $ \\
			\hline
			$p$\\
		\end{tabular}
		&
		\begin{tabular}{c}
			$p \Leftrightarrow q$ \\
			$q \Leftrightarrow r$ \\
			\hline
			$p \Leftrightarrow r$\\
		\end{tabular}
		\\

		Modus Ponens & Modus Tollens & Loi d'équivalence\\
		\begin{tabular}{c}
			$p \Rightarrow q$ \\
			$p$ \\
			\hline
			$q$\\
		\end{tabular}
		&
		\begin{tabular}{c}
			$p \Rightarrow q$ \\
			$\lnot q$ \\
			\hline
			$\lnot p$\\
		\end{tabular}
		&
		\begin{tabular}{c}
			$p \Leftrightarrow q$ \\
			\hline
			$q \Leftrightarrow p$\\
			$q \Rightarrow p$\\
			$p \Rightarrow q$\\
		\end{tabular}
		\\
		Syllogisme disjoint\\
		\begin{tabular}{c}
			$p\lor q$\\
			$\lnot p$\\
			\hline
			$q$\\
		\end{tabular}
		\\
	\end{tabular}
\end{center}
\subsection{Schémas de preuve}

En plus des équivalences logiques et des règles d'inférence,
nous ajoutons deux schémas de preuve qui formalisent des
techniques de raisonnement plus abstraites:
le théorème de déduction et la démonstration par l'absurde.
Ces schémas donnent à l'approche de preuve déductive une grande expressivité,
beaucoup plus qu'une preuve transformationnelle.

\subsubsection*{Théorème de déduction (preuve conditionnelle)}

Pour prouver la proposition $s\Rightarrow t$, on suppose $s$ vrai.
La proposition $s$ s'ajoute donc aux prémisses utilisées dans la preuve.  
Ensuite, on fait une preuve de $t$:
on peut construire une preuve (objet mathématique) de $t$ en commençant de $s$.
On note ce théorème $s \vdash t$.
On écrit ce schéma un peu comme une règle d'inférence:
			\begin{center}
			\begin{tabular}{c}
      		$p,...,r,s \vdash t$ \\
      		\hline
      		$p,...,r \vdash s\Rightarrow t$\\
   			\end{tabular}\\
			\end{center}
On déduit $t$ et donc on sait que l'hypothèse $s\Rightarrow t$ est vraie et on l'évacue.
			
			\textbf{Remarque :} Il ne faut pas confondre les deux notations $p\models t$ et $p\vdash t$.
			\begin{itemize}
			\item $p\models t$ est une notion de vérité (tout modèle de $p$ est un modèle de $t$), et donc de sémantique;
			\item $ p\vdash t$ est une notion syntaxique (en commençant de $p$ on peut construire une preuve de $t$),
car une preuve est une séquence de manipulations syntaxiques.
			\end{itemize}
			
\subsubsection*{Démonstration par l'absurde (preuve par contradiction)}
		On suppose que les prémisses $p, ..., q$ n'ont pas de problème,
c'est-à-dire qu'on ne peut pas prouver une contradiction à partir de ces propositions.
Ensuite, on ajoute $r$ aux prémisses.
S'il est possible de prouver $s$ et aussi de prouver $\lnot s$, cela signifie qu'il y a une erreur dans les prémisses.
On suppose que c'est l'ajout $r$ qui est fautif.
On justifie qu'il n'y a aucune contradiction dans $p, ... ,q$ car on part du principe qu'il existe un modèle de $p,...q$.
On écrit ce schéma ainsi:
		\begin{center}
			\begin{tabular}{c}
      		$p,...,q,r \vdash s$ \\
      		$p,...,q,r \vdash \lnot s$\\
      		\hline
      		$p,...,q \vdash \lnot r$\\
   			\end{tabular}\\
			\end{center}
			
\section{Exemple de preuve déductive}

Nous donnons un premier exemple de preuve déductive.
Voici les propositions premières :
\begin{enumerate}
\item[A =] "tu manges bien"
\item[B =] "ton système digestif est en bonne santé"
\item[C =] "tu pratiques une activité physique régulière"
\item[D =] "tu es en bonne forme physique"
\item[E =] "tu vis longtemps"
\end{enumerate}
On peut maintenant établir une théorie, c'est-à-dire, un ensemble de propositions,
dont on espère qu'elle aura un modèle.

\paragraph{Théorie} 
\begin{enumerate}
\item $A \implies B$
\item $C \implies D$
\item $B \lor D \implies E$
\item $\lnot E$
\end{enumerate}

\paragraph{À prouver} $\lnot A \land \lnot C$

\paragraph{Preuve}
Voici la preuve déductive.  Nous la mettons dans un cadre pour souligner qu'elle est un objet mathématique.
Chaque ligne est où une prémisse, où un pas de raisonnement (une équivalence ou une règle d'inférence).
Pour chaque ligne il faut donner le nom de la règle qui est appliquée, cela s'appelle la {\em justification}
et c'est une partie importante de la preuve.
Les deux schémas se présentent avec des indentations; la partie indentée d'une preuve contient une prémisse
en plus ($s$ pour la preuve conditionnelle, $r$ pour la preuve indirecte).

\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}\\

Les quatre premières lignes introduisent les prémisses (les propositions de la théorie).
La ligne 5 commence une première preuve indirecte: on fait l'hypothèse A
et ensuite on déduit E (sur la ligne 8).  C'est une contradiction avec la prémisse $\lnot$E
et donc on vient de prouver $\lnot$A (sur la ligne 9).
La ligne 10 commence une deuxième preuve indirecte: on fait l'hypothèse C
et ensuite on déduit E (sur la ligne 14).  De nouveau, c'est une contradiction (avec la prémisse $\lnot$E)
et donc on vient de prouver $\lnot$C (sur la ligne 15).
Les justifications pour les lignes 9 et 15 sont {\em preuve indirecte}.

Avec cette preuve déductive,
nous avons pu prouver que tu ne manges pas bien et que tu ne pratiques pas d'activité physique régulière. 

\section{Exemples de l'utilisation des schémas}

Pour illustrer l'utilisation des deux schémas, la preuve conditionnelle et la preuve par contradiction,
nous allons prouver la même conclusion en trois manières, avec chaque schéma et sans schéma.
\begin{itemize}
\item Prémisse: $(p \land q) \lor r$
\item Conclusion: $\lnot p \Rightarrow r$
\end{itemize}

\subsection{Exemple sans schéma}

\begin{tabular}{|l|l|}
\hline
1. $(p \land q) \lor r$ & \textit{Prémisse} \\
2. $r \lor (p \land q)$ & \textit{Commutativité en 1} \\
3. $(r \lor p) \land (r \lor q)$ & \textit{Associativité en 2}\\
4. $(r \lor p)$ & \textit{Simplification en 3}\\
5. $(p \lor r)$ & \textit{Commutativité en 4}\\
6. $\lnot \lnot p \lor r $ & \textit{Loi de la négation en 5}\\
7. $\lnot p \Rightarrow r $ & \textit{Implication en 6}\\
\hline
\end{tabular}

\subsection{Exemple de preuve conditionnelle}

\begin{tabular}{|l|l|}
\hline
1. $(p \land q) \lor r $ & \textit{Prémisse} \\
2. $\lnot \lnot(p \land q) \lor r $ & \textit{Double négation en 1} \\
3. $\lnot ( \lnot p \lor \lnot q) \lor r $ & \textit{Loi De Morgan en 2} \\
4. $\lnot p \lor \lnot q \Rightarrow r $ & \textit{Implication en 3}\\
\indent 5.  $\lnot p $ & \textit{Hypothèse}\\
\indent 6.  $\lnot p \lor \lnot q $& \textit{ Addition sur 5}\\
\indent 7.  $r$ & \textit{ Modus Ponens sur 4 et 6}\\
8.  $\lnot p \Rightarrow r $& \textit{Evacuation de l'hypothèse}\\
\hline
\end{tabular}

\subsection{Exemple de preuve par contradiction}

\begin{tabular}{|l|l|}
\hline
1. $(p \land q) \lor r $ & \textit{Prémisse}\\
2. $ (p  \lor r) \land (q \lor r)$ & \textit{Distributivité sur 1}\\
3. $(p \lor r)$ & \textit{Simplification en 2}\\

 \indent 4. $\lnot ( \lnot p \Rightarrow r)$ & \textit{Hypothèse}\\
 \indent 5. $\lnot ( \lnot \lnot p \lor r)$ &\textit{Implication en 4}\\
 \indent 6. $\lnot (p \lor r)$ & \textit{ Négation en 5}\\


7. $\lnot \lnot (\lnot p \Rightarrow r) $ & \textit{ Preuve par contradiction}\\
8. $\lnot p \Rightarrow r $ & \textit{Négation en 7}\\
\hline
\end{tabular}


\section{Principe de dualité}

Le principe de dualité affirme que l'on peut transformer
une propriété vraie en une autre propriété vraie en
remplaçant systématiquement tout symbole par un autre
selon un schéma de correspondances.

\subsubsection{Dans les formules sans $\Rightarrow$ :}

Les correspondances sont:
\begin{align*}
\land \leftrightarrow \lor \\ 
\true \leftrightarrow \false 
\end{align*}
Par exemple, si on prend la tautologie suivante:
\begin{align*}
\models \lnot ( p \land q)  \Leftrightarrow \lnot p \lor \lnot q
\end{align*}
en remplaçant chaque symbole par le symbole correspondant on obtient une autre tautologie:
\begin{align*}
\models \lnot ( p \lor q)  \Leftrightarrow \lnot p \land \lnot q 
\end{align*}

\subsubsection{Dans une formule quelconque:}

Les correspondances sont:
\begin{align*}
\land \leftrightarrow \lor \\ 
\true \leftrightarrow \false \\ 
p \leftrightarrow \lnot p 
\end{align*}
Par exemple, si on prend la définition suivante:
 \begin{align*}
	 \{p_1,...,p_n\} \models q \hspace{0.5cm}
         ssi \hspace{0.5cm} \models (p_1 \land ... \land p_n \land \lnot q) \Leftrightarrow \false
 \end{align*}
en remplaçant chaque symbole par le symbole correspondant on obtient une propriété vraie:
 \begin{align*}
	 \{p_1,...,p_n\} \models q \hspace{0.5cm}
         ssi \hspace{0.5cm} \models ( \lnot p_1 \lor ... \lor \lnot p_n \lor q) \Leftrightarrow \true
 \end{align*}


% Ancienne partie 5:

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

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.