From 091f7faf2e5eb70d3bd76de835bb02a87da4974c Mon Sep 17 00:00:00 2001 From: Peter Van Roy Date: Tue, 7 Jul 2015 16:50:28 +0200 Subject: [PATCH] Finished chapter 6. --- partie5.tex | 1 + partie6-10.tex | 1127 +++++++++++++++++++++++++++++++++++++++++++++ partie6-7-8-9.tex | 4 +- partie8.tex | 8 +- partie9.tex | 5 +- 5 files changed, 1137 insertions(+), 8 deletions(-) create mode 100644 partie6-10.tex diff --git a/partie5.tex b/partie5.tex index 0cd9b5c..692e50b 100644 --- a/partie5.tex +++ b/partie5.tex @@ -48,6 +48,7 @@ \section{Algorithme de preuve} 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. diff --git a/partie6-10.tex b/partie6-10.tex new file mode 100644 index 0000000..4373112 --- /dev/null +++ b/partie6-10.tex @@ -0,0 +1,1127 @@ +%Packages à ajouter pour la compilation +%\usepackage{amsmath} +%\usepackage{lmodern} +%\usepackage{vmargin} +%\usepackage{tabularx} +%\usepackage[usenames,dvipsnames]{color} +%Partie 6 +\chapter{La logique des prédicats} + +\section{Introduction} + +Nous allons maintenant étudier une logique beaucoup plus expressive que la +logique propositionnelle, la logique des prédicats, qui est aussi appelée +la logique de premier ordre.\footnote{Il existe des logiques d'ordres supérieures, +mais elles ne feront pas l'objet de ce cours.} +Voici un premier tableau qui montre les différences entre la logique propositionnelle vue jusqu'à présent et la logique des prédicats que nous allons étudier. +\begin{center} +\begin{tabular}{|c|c|} +\hline +Logique Propositionnelle & Logique des prédicats \\ +\hline +Propositions premières & Prédicats P(x,y) \\ +P, Q, R & Quantifieurs: $\exists$x, $\forall$y \\ +$\hookrightarrow$ Pas de Relations & $\hookrightarrow$ Relation \\ +\hline +\end{tabular} +\end{center} + +On note P(x,y) dans la logique des prédicats avec x,y, les arguments du prédicat P qui sont des variables. +Dans la logique propositionnelle, chaque proposition est isolée/indépendante alors que dans les prédicats on peut lier plusieurs prédicats ensemble. + + +\begin{center} +\begin{tabular}{|c|c|c|} +\hline +Exemple & Logique propositionnelle & Logique des prédicats \\ +\hline +Socrate est un philosophe & P & Phil(Socrate) \\ +Platon est un philosophe & Q & Phil(Platon) \\ +\hline +\end{tabular} +\end{center} + +En logique propositionnelle il n'y a aucune relation entre P et Q, alors qu'en logique des prédicats on peut lier Socrate et Platon avec le prédicat Philosophe qui prend en argument le nom du philosophe (Socrate ou Platon dans ce cas). Phil(Socrate) est donc vrai. On peut donc dire grâce aux prédicats que Socrate et Platon sont "la même chose", des philosophes.\\ + +Un autre exemple de prédicat: + +\begin{center} +$\forall \alpha$ Phil($\alpha$) $\Rightarrow$ Savant($\alpha$)\\ +\vspace{3mm} +$\hookrightarrow$ ... \textit{cette formulation permet de résumer un très grand nombre de faits. L'ensemble des arguments $\alpha$ peut être infini} +\end{center} +Comme Socrate est un philosophe, on peut déduire que Socrate est un savant aussi! + +Dire la même chose en logique propositionnelle serait beaucoup plus compliqué: \\ + +"Socrate est un savant" Proposition "R"\\ +\indent "Platon est un savant" Proposition "S"\\ + +On va donc noter en logique propositionnelle +\begin{center} +(P$\Rightarrow$R) $\cup$ (Q$\Rightarrow$S) $\cup$ ...(\textit{potentiellement infini}) +\end{center} + +On doit tout énumérer car il n'y a aucune relation entre les différentes propositions. S'il y a un nombre infini, ça ne marche pas. Il y a donc de grandes limitations dans la logique propositionnelle. + +Néanmoins parfois la logique propositionnelle peut être utile. +Il existe des outils informatiques qui utilisent la logique propositionnelle. On peut prendre l'exemple de ``SAT solver'' à qui on donne des équations booléennes très compliquées et qui va trouver les valeurs des propositions primitives qui rendent vraie cette proposition. +La logique propositionnelle est utile, mais si l'on veut faire du raisonnement sur plus que "vrai" et "faux" avec des relations entre des propositions, la logique propositionnelle ne marche pas. Si on veut faire un logiciel qui montre une certaine intelligence, il faut utiliser la logique des prédicats.\\ + +Autre exemple: + +\begin{tabular}{|ccc|} +\hline +Exemple & Logique propositionnelle & Logique des prédicats \\ +\hline +Tout adulte peut voter & P & $\forall$x adulte(x) $\Rightarrow$ voter(x) \\ +John est un adulte & Q & adulte(\textcolor{OliveGreen}{John}) \\ +\line(1,0){50} & \line(1,0){10} & \line(1,0){45} \\ + +John peut voter & \textcolor{Red}{?R?}& voter(\textcolor{OliveGreen}{John}) \\ +\hline +\end{tabular}\\ + +Ce genre de raisonnement est très difficile à faire en logique propositionnelle alors qu'en logique des prédicats c'est beaucoup plus simple. +Le John en ligne 3 et en ligne 4 correspond à la même personne, ou de manière plus général à la même variable. +Ceci montre donc bien l'utilité de la logique des prédicats pour faire des relations de ce type. + +\section{Quantificateurs} + +Les expressions "pour tout $x$" ($\forall x$) et "il existe $x$ tel que" ($\exists x$) sont appelés des {\em quantificateurs}. +Les quantificateurs permettent de résumer un grand nombre de formules en une formule. +La notion de {\em portée} d'un quantificateur est un concept très important auquel il faut faire très attention, +car il peut changer complètement le sens d'une formulation. +Par exemple, les deux formules suivantes: + +$\forall x$ (enfants($x$) $\wedge$ intelligents($x$) $\Rightarrow$ $\exists y$ aime($x$,$y$)) \\ + +$\forall x$ (enfants($x$) $\wedge$ intelligents($x$)) $\Rightarrow$ $\exists y$ aime($x$,$y$) \\ + +Ces deux formules peuvent paraître équivalentes, mais en réalité elles ont un sens tout à fait différent. +En effet, dans le deuxième cas on remarque que le quantificateur $\forall x$ ne porte pas sur +la dernière variable $x$ qui est l'argument du prédicat aime($x$,$y$). +Il faut donc faire bien attention à quel quantificateur une variable s'identifie lorsqu'on manipule des formules. + +\begin{itemize} +\item[$\bullet$] $\forall x$ P($x$) $\wedge$ $\exists x$ Q($x$) : contient deux variables différentes\\ + +\item[$\bullet$] $\forall x$ $\exists x$ P($x$) $\wedge$ Q($x$) : est une forme incorrecte, conflit des noms de variables \\ +\end{itemize} + +Pour résoudre ces conflits, on fait appel à une nouvelle opération, le {\em renommage}. +Cette opération permet de changer le nom des variables tout en conservant le sens de la formule. Ainsi on obtient : \\ + +$\forall x$ $\exists z$ P($x$) $\wedge$ Q($z$) \textit{renommage (2)} \\ + +Le concept de variables, de leurs portées ainsi que d'opérateurs en logique des prédicats fait fortement penser au langage de programmation + +Une comparaison peut être faite entre un code de programme et une formule. +Prenons un code tout à fait banal comprenant des variables différentes avec des portées différentes qui ont le même identificateur ainsi qu'une formule correspondante. + +\begin{verbatim} +1. begin { +2. var x,y: int; +3. x := 4; +4. y := 2; +5. +6. begin { +7. var x: int; +8. x := 5; +9. x := x*y; +10. end } +11. x := x*y; +12. end } +\end{verbatim} + + +\textcolor{Green}{$\forall x$} \textcolor{Red}{$\forall y$} p(\textcolor{Green}{$x$}) $\wedge$ ((\textcolor{Blue}{$\exists x$} q(\textcolor{Blue}{$x$},\textcolor{Red}{$y$})) $\vee$ r(\textcolor{Green}{$x$},\textcolor{Red}{$y$})) \\ + +Cet exemple illustre la hiérarchie et la portée des variables et des quantificateurs. + +En analysant la formule morceau par morceau : \\ + +\begin{itemize} + +\item[$\bullet$] " \textcolor{Green}{$\forall x$} \textcolor{Red}{$\forall y$} p(\textcolor{Green}{$x$}) $\wedge$ " correspond aux lignes $\lbrace 2,3,4 \rbrace$ du code \\ + +\item[$\bullet$]" \textcolor{Blue}{$\exists x$} q(\textcolor{Blue}{$x$},\textcolor{Red}{$y$}) $\vee$ " correspond aux lignes $\lbrace 7,8,9 \rbrace$ \\ + +\item[$\bullet$]" r(\textcolor{Green}{$x$},\textcolor{Red}{$y$})) " correspond à la ligne $\lbrace 11 \rbrace$ \\ + +\end{itemize} + +Cet exemple montre bien la correspondance entre le concept de portée +dans le monde de la programmation et celui de la logique des prédicats. + +\section{Syntaxe} + +\subsection{Symboles} + +Voici les différents symboles utilisés dans une formule de la logique des prédicats. +Nous appelons {\em arité} d'un prédicat ou d'une fonction son nombre d'arguments +(fonction unaire, prédicat binaire, etc.). + +\begin{tabular}{|c|c|c|} + \hline + Symboles logiques & quantificateurs & $\forall$ $\exists$ \\ + & connecteurs logiques & $\wedge$ $\vee$ $\neg$ $\Rightarrow$ $\Leftrightarrow$ \\ + & parenthèses & ( ) \\ + & variables & $x, y, z$ \\ + & & true, false\\ + \hline + Symboles non logiques & symboles de prédicat & $P$ $Q$ $R$ (avec arité $\geq 0$) \\ + & symboles de fonction & $f$ $g$ $h$ (avec arité $\geq 0$) \\ + & symboles de constante & $a$ $b$ $c$ (si arité $= 0$) \\ + \hline +\end{tabular} + +\subsection{Règles de Grammaire} +\begin{tabular}{rl} +$::=$ & $$ \\ + & $\vert$ $\neg$ $$ \\ + & $\vert$ $$ $$ $$ \\ + & $\vert$ $\forall .$ \\ + & $\vert$ $\exists .$ \\ +$::=$ + & true, false \\ + & $\vert$ $(*)$ \\ +$::=$ & $$ \\ + & $\vert $ \\ + & $\vert (*)$ \\ +$::=$ + & $\wedge \vert \vee \vert \Rightarrow \vert \Leftrightarrow$ \\ + +\end{tabular} + +\section{Sémantique} + +Dans la logique des prédicats, nous gardons les notions de modèle et d'interprétation déjà définies dans la logique propositionnelle. Même si la logique des prédicats est beaucoup plus puissante, sa sémantique reste similaire à la logique propositionnelle. +Comme pour la logique propositionnelle, une interprétation peut avoir une valeur (true, false). + +\subsection{Exemple} +Illustrons par un exemple : + +\begin{center} +$p : P(b,f(b)) \Rightarrow \exists y P(a,y)$ \\ +\vspace{3mm} +\end{center} +On suppose que le $a$ et le $b$ sont des constantes et que le $f$ est une fonction. +Une interprétation possible de cette formule est la suivante: +\begin{itemize} +\item[$\bullet$]P : $\mathrm{val}_{I}(P) = $ $ \geq $ \hspace{3mm} (\textit{considéré comme un vrai prédicat}) +\item[$\bullet$] a : $\mathrm{val}_{I}(a) = $ $ \sqrt{2} $ +\item[$\bullet$] b : $\mathrm{val}_{I}(b) = $ $ \pi $ +\item[$\bullet$] $f$ : $\mathrm{val}_{I}(f) = $ $ f_{i} $ \hspace{3mm} $f_{i}= \Re \rightarrow \Re : d \rightarrow \dfrac{d}{2} $ +\end{itemize} +Avec ces éléments, on peut donc interpréter la formule $p$: +\begin{center} +\textit{Si $\pi \geq \dfrac{\pi}{2}$, alors $\exists$ $ d \in \Re$ tel que $\sqrt2 \geq d$ } +\end{center} +Avec cette interprétation, la phrase logique donne ce sens. +Une autre interprétation donnerait un sens totalement différent à la phrase logique. Voici une autre interprétation totalement différente : +\begin{itemize} +\item[$\bullet$] a : $\mathrm{val}_{I}(a) = $ "Barack Obama" +\item[$\bullet$] b : $\mathrm{val}_{I}(b) = $ "Vladimir Putin" +\item[$\bullet$] $f$ : $\mathrm{val}_{I}(f) = $ $ f_{i} $ \hspace{3mm} $f_{i}: d \rightarrow \mathrm{père}(d)$ +\item[$\bullet$] P : $\mathrm{val}_{I}(P) = $ $P_{I}$ \hspace{3mm} $d_{1}$ est enfant de $d_{2}$\\ +\end{itemize} + +Avec ce nouveau sens, on trouve l'interprétation suivante : +\begin{center} +\textit{Si Vladimir Putin est un enfant du père de Vladimir Putin alors il existe une personne telle que Barack Obama est un enfant de cette personne.} +\end{center} +La seconde interprétation est très différente de la première malgré le fait que ce soit la même formule à l'origine ! La connexion entre une formule et son sens permet de garder une certaine souplesse dans le sens où l'on peut choisir ça. C'est un peu comme dans la logique propositionnelle, mais avec encore plus de souplesse. + +On peut se demander si ces deux interprétations sont des modèles de la formule ? \\ +La première interprétation est un modèle de la formule, car le sens de la formule est vrai dans l'interprétation. En effet, $\pi \geq \dfrac{\pi}{2}$ et $\exists$ $ d \in \Re$ tel que $\sqrt2 \geq d$. On voit donc que le modèle est vrai. + +La deuxième interprétation est aussi un modèle de la formule, car l'interprétation trouvée est vraie aussi. Cela peut paraître bizarre, mais c'est correct. +%Partie 7 + +\subsection{Interprétation} + +\subsubsection{Interprétation des symboles} + +L'approche que nous utilisons pour définir une sémantique de la logique des prédicats est très proche +de l'approche que nous avons utilisée pour la logique propositionnelle. +Nous allons définir une interprétation $I$ de chaque formule, qui nous permettra de calculer si la formule est vraie ou fausse. +Cependant, l'interprétation en logique des prédicats est plus générale qu'en logique propositionnelle. +En plus des propositions, nous avons des variables, des fonctions et des prédicats avec des arguments, +et des quantificateurs ($\forall$ et $\exists$). + +Une {\em interprétation} $I$ en logique des prédicats est une paire $I = (D_I, \mathrm{val}_I)$, +avec un ensemble $D_I$ qui s'appelle le {\em domaine de discours} et une fonction $\mathrm{val}_I$ qui s'appelle +la {\em fonction de valuation} qui renvoie un élément de $D_I$ pour chaque symbole. +Nous avons donc pour chaque symbole $s$: +\begin{itemize} +\item Si $s$ est un symbole de prédicat, + $\mathrm{val}_{I}(s) = P_{I}$ une fonction $P_{I}:D_{I}^{n} \rightarrow (\mathrm{true},\mathrm{false})$. +\item Si $s$ est un symbole de fonction, + $\mathrm{val}_I(s) = f_I$ une fonction $f_{I}:D_{I}^{n} \rightarrow D_{I}$ avec $n$ le nombre d'arguments. +\item Si $s$ est une constante (une fonction avec zéro arguments), + $\mathrm{val}_I(s) = c$ un élément de $D_I$. +\item Si $s$ est une variable, + $\mathrm{val}_{I}(x) = x_{I}$, un élément $D_{I}$. +\end{itemize} +Cela implique chaque fonction correspond à une vraie fonction, chaque prédicat +correspond à un vrai prédicat, et chaque constante et chaque variable correspondent à une constante dans le domaine de discours. + +Attention à la différence entre les variables et les constantes. +Pour les deux, l'interprétation est un élément de $D_I$, +mais on peut utiliser les variables dans les quantificateurs et pas les constantes. +Cela veut dire que dans une formule, la valeur d'une variable dépend de l'endroit où se trouve la formule, +ce qui n'est pas vrai pour une constante. + +\subsubsection{Interprétation des termes et formules} + +Avec la fonction $\mathrm{val}_I$ qui est définie sur tous les symboles, nous pouvons définir une fonction +$\mathrm{VAL}_I$ sur les termes et les formules: +\begin{equation} +\mathrm{VAL}_I : \mathrm{TERM} \cup \mathrm{PRED} \rightarrow D_I \cup \{T, F\} +\end{equation} +Ici, $\mathrm{TERM}$ est l'ensemble des termes et $\mathrm{PRED}$ est l'ensemble des formules. +Nous avons donc: +\begin{itemize} +\item Si $t$ est un terme, $t \rightarrow \mathrm{VAL}_I(t)$. +\item Si $p$ est une formule, $p \rightarrow \mathrm{VAL}_I(p)$. +\end{itemize} +Nous pouvons définir $\mathrm{VAL}_I$ avec $\mathrm{val}_I$, en suivant la définition de la syntaxe des formules: +\begin{itemize} +\item $\mathrm{VAL}_I ( P(t_1, \ldots, t_m) = (\mathrm{val}_I(P)) (\mathrm{VAL}_I(t_1), \ldots, \mathrm{VAL}_I(t_m))$. +\item $\mathrm{VAL}_I ( \forall x.p ) = T$ si pour chaque $d \in D_I$, $\mathrm{VAL}_{\{x \leftarrow d\} \circ I}(p) = T$. Sinon, c'est $F$. +En clair, $d$ est l'interprétation de $x$ dans la formule $p$. Si pour tous les $d$, l'interprétation de $p$ est vraie, alors le +quantificateur universel est vrai aussi. +\item $\mathrm{VAL}_I ( \exists x.p ) = T$ s'il existe un élément $d \in D_I$ tel que $\mathrm{VAL}_{\{x \leftarrow d\} \circ I}(p) = T$. +Sinon, c'est $F$. +\item $\mathrm{VAL}_I(p \wedge q) = T$ si $\mathrm{VAL}_I(p)=T$ et $\mathrm{VAL}_I(q)=T$. Si au moins un des deux est $F$, c'est $F$. +\item $\mathrm{VAL}_I(p \vee q) = T$ si $\mathrm{VAL}_I(p)=T$ ou $\mathrm{VAL}_I(q)=T$. Si tous les deux sont $F$, c'est $F$. +\item $\mathrm{VAL}_I(c) = \mathrm{val}_I(c)$ si $c$ est un symbole de constante. +\item $\mathrm{VAL}_I(x) = \mathrm{val}_I(x)$ si $x$ est un symbole de variable. +\item $\mathrm{VAL}_I(f(t_1, \ldots, t_n)) = (\mathrm{val}_I(f))(\mathrm{VAL}_I(t_1), \ldots, \mathrm{VAL}_I(t_n))$ si $f$ est un symbole de fonction. +\item $\mathrm{VAL}_I(\mathrm{true}) = T$. +\item $\mathrm{VAL}_I(\mathrm{false}) = F$. +\item Dans cette énumération, j'ai omis de mentionner l'implication $\Rightarrow$ et l'équivalence $\Leftrightarrow$. +Je vous les laisse en exercice. +\end{itemize} +En décomposant une formule $p$ en ses symboles de base, nous pouvons donc calculer $\mathrm{VAL}_I(p)$, c'est-à-dire si la formule +est vraie ou fausse, à partir de la fonction $\mathrm{val}_I$. + +\subsubsection{Modèle} + +Un modèle d'un ensemble de formules est une interprétation qui rend toutes les formules vraies. +Formellement, si on a un ensemble de formules $B = \{ p_1, \ldots, p_n \}$, +une interprétation $I$ pour $B$ est un {\em modèle} si et seulement si: +\begin{equation} +\forall p_i \in B: \mathrm{VAL}_I(p_i) = T +\end{equation} + +% \section{Différence avec la logique des propositions} +% Les trois différences entre les deux logiques sont: +% \begin{enumerate} +% \item les variables, +% \item les quantificateurs, +% \item les symboles de fonction (moins important). +% \end{enumerate} +% Imaginons un modèle $B: +% \{ +% \begin{array}{rcr} +% P_{1},...P_{n} +% \end{array} +% \} +% $ +% Si nous utilisons une interprétation I pour B cela donne: +% $\forall P_{I} \in B : VAL_{I} (P_{I}) = True$ qui est très générale, car $P_{I}$ peut avoir des variables, des quantificateurs ... + +% partie 1 (15 à 30 min) Thomas) + +\section{Preuves en logique des prédicats} + +Comme pour la logique propositionnelle, il est important de pouvoir faire des preuves avec la logique des prédicats. +Il y a deux approches principales: la preuve manuelle et la preuve automatisée. +Pour les deux approches, la preuve est toujours un objet mathématique, une séquence de déductions avec ses formules et +ses justifications, qui sont une application des règles de preuve. + +\subsection{Preuves manuelles} + +Les preuves manuelles sont le sujet du chapitre \ref{preuvemanuelle}. + +\subsection{Preuves automatisées} + +Les preuves automatisées sont le sujet du chapitre \ref{algorithmepreuve}. +L'algorithme de preuve que nous allons définir est une généralisation de l'algorithme pour la logique propositionnelle. +Il y a toujours : +\begin{itemize} + \item Une règle de résolution pour les preuves automatisées, mais celle-ci est plus générale. Elle va utiliser un concept appelé +``unification''. Ce nouveau concept est nécessaire à cause des variables. +En effet, celles-ci peuvent être différentes, il faut donc trouver un nouveau moyen de les fusionner. + \item Une forme normale, qui est plus compliquée à cause des quantificateurs et des symboles de fonctions, mais qu'il est encore possible de l'obtenir. + \item Un algorithme avec ses propriétés. Mais il est moins fort/complet que l'algorithme développé pour la logique des propositions. Il ne sera plus décidable, mais seulement semi-décidable. C'est-à-dire que parfois il tournera en boucle. Cela est dû aux variables et aux quantificateurs. La logique des prédicats est beaucoup plus riche que la logique des propositions, mais en contrepartie l'algorithme arrive à prouver moins de choses. Cependant, l'algorithme sera toujours adéquat, mais pas forcément complet. Il ne sera pas toujours possible de trouver une preuve, même quand elle existe parce qu'elle sera trop compliquée. +\end{itemize} +Qu'est il possible de faire avec ce genre d'algorithme moins fort? + +\subsubsection{L'utilisation de l'algorithme de preuve} + +Il y a deux possibilités : +\begin{itemize} +\item {\em Un assistant de preuve} +C'est un outil qui aide les gens à faire des preuves formelles. Deux exemples d'assistants de preuves sont Coq et Isabelle. C'est un outil très sophistiqué, mais qui a permis de prouver des choses de manière totalement formelle, alors qu'avant des preuves prenaient des dizaines voire des centaines de pages de preuves mathématiques. Mais cet assistant ne fait pas tout parce que l'algorithme est moins bon. Cependant, il aide beaucoup. C'est à l'être humain de lui donner des coups de pouce sous forme de lemmes, hypothèses, chemins, stratégies ... Ensuite, l'algorithme s'occupe de la manipulation des symboles.\\ +Un exemple très célèbre est le théorème de la coloration d'une carte. La question est : est-il toujours possible de colorier chaque pays avec une couleur, de façon à ce que deux pays limitrophes n'aient pas la même couleur et en utilisant un certain nombre de couleurs différentes? Ce n'est pas évident à prouver et ça a demandé beaucoup de travail aux mathématiciens. Mais récemment, Georges Gonthier (un informaticien) a réussi à formuler ce problème avec l'assistant de preuves. Ce fut un tour de force. Désormais, il existe une preuve complètement formalisée, sans erreur pour ce théorème. +\item {\em Un langage de programmation} +L'algorithme peut être considéré comme le moteur d'un programme. C'est ce qu'on appelle maintenant la programmation logique. Elle consiste à utiliser la logique dans un programme. Le langage le plus célèbre qui a suivi cette approche est Prolog. Ce fut un énorme succès, car les gens ne croyaient pas que c'était possible de faire un programme en logique qui pouvait tourner. Cela a donné naissance à la programmation par contraintes (une contrainte est une relation logique). Cette discipline est très utile pour les optimisations, par exemple dans le cas du "voyageur de commerce". +\end{itemize} + +La logique des prédicats n'est donc pas quelque chose de seulement théorique, destiné uniquement aux mathématiciens. +Elle a été utilisée avec succès dans les programmes. + +%partie 3 de 30 à 45 min (Guillaume) + +\chapter{Preuves en logique des prédicats} +\label{preuvemanuelle} + +On va généraliser l'approche de la logique propositionnelle, car comme vu précédemment le langage des prédicats est beaucoup plus riche. Il ajoute entre autres : + +\begin{itemize} + \item Des variables + \item Des constantes + \item Des fonctions (détaillé plus tard) + \item Des prédicats + \item Des quantificateurs +\end{itemize} + +Les preuves en logique des prédicats ressemblent très fort aux preuves en logique propositionnelle. Il y a encore des prémisses, des formules avec leurs justificatifs et une conclusion. On peut aussi utiliser des preuves indirectes et des preuves conditionnelles. +Une preuve est toujours un objet formel: + +\begin{center} +\fbox{ +$ +\begin{array}{l l l} + 1. & \fbox{\ldots} & Prémisses \\ + 2. & \fbox{Formule, regle} & Justification \\ + \ldots & \ldots & \ldots \\ + n. & \fbox{Conclusion} & Justification \\ +\end{array} +$ +} +\end{center} + +Mais il est vrai que les preuves en logique des prédicats sont parfois délicates à cause des variables: +occurrences libres (par quantifiées), occurrences liées par $\forall$ et occurrences liées par $\exists$. +Dans ce chapitre nous allons surtout étudier comment manipuler les variables et les quantificateurs +correctement dans une preuve. + +\section{Exemple} + +Nous allons prouver que s'il est vrai que +$\forall x \cdot P(x) \wedge Q(x)$ (prémisse) +alors il est vrai que $\forall x \cdot P(x)\wedge(\forall x \cdot Q(x))$ (conclusion). +Nous utilisons l'approche suivante pour traiter les quantificateurs: +\begin{center} +$ +\begin{array}{l l} + 1. & $Enlever les quantificateurs pour avoir des variables libres$ \\ + 2. & $Raisonner sur l'intérieur$\\ + 3. & $Remettre les quantificateurs$\\ +\end{array} +$ +\end{center} +Les étapes difficiles à réaliser correctement sont les étapes $1$ et $3$. Voici la preuve en ``français'' : + +En retirant les quantificateurs des prémisses, cela donne : +``Comme $P(x) \wedge Q(x)$ est vrai pour tout $x$, alors $P(x)$ est vrai pour tout $x$''. +De là, on peut remettre les quantificateurs pour obtenir $\forall x \cdot P(x)$. De façon similaire, on obtient $\forall x \cdot Q(x)$. Et on conclut en remettant les quantificateurs: $\forall x \cdot P(x) \wedge \forall x \cdot Q(x)$, en utilisant la conjonction. + +En preuve formelle, cela donne : + +\begin{center} +\fbox{ +$ +\begin{array}{l l l} + 1. & \forall x \cdot P(x) \wedge Q(x) & $Prémisses$ \\ + 2. & P(x) \wedge Q(x) & $Élimination de $\forall \\ + 3. & P(x) & $Simplification$ \\ + 4. & \forall x \cdot P(x) & $Introduction de $ \forall \\ + 5. & Q(x) & $Simplification $ \forall \\ + 6. & \forall x \cdot Q(x) & $Introduction de $\forall \\ + 7. & \forall x \cdot P(x) \wedge \forall x \cdot Q(x) & $Conjonction$ \\ +\end{array} +$ +} +\end{center} + +On a donc utilisé 4 règles en plus par rapport aux preuves formelles en logique propositionnelle (les règles de la logique propositionnelle restent valables en logique des prédicats): +\begin{itemize} +\item Élimination de $\forall$ +\item Introduction de $\forall$ +\item Élimination de $\exists$ +\item Introduction de $\exists$ +\end{itemize} + +Certaines de ces règles sont simples d'utilisation, d'autres sont plus difficiles. +Il est également possible d'utiliser d'autres règles (certaines plus générales que d'autres\footnote{Voir "Inference logic" ou "Predicate logic"}). + +\begin{framed} +\textbf{Note} + +Il est possible d'utiliser les quantificateurs dans les formules mathématiques. Typiquement, on ne les note pas, car ils sont présents de manière implicite. Par exemple : +\begin{itemize} +\item $\forall x \cdot \sin(2x) = 2 \cdot \sin(x) \cdot \cos(x)$ +\item $\forall x \cdot x + x = 2x$ +\item $\exists x \cdot \sin(x) + \cos(x) = 0,5$ +\item $\exists x \cdot x + 5 = 9$ +\end{itemize} + +On peut remarquer que pour les deux premiers cas, $x$ est une véritable variable, on peut donc ajouter un quantificateur universel $\forall$. +Pour les deux cas suivants, on remarque que $x$ est une inconnue, car il y a une équation à résoudre et une solution à trouver, on peut donc ajouter un quantificateur existentiel $\exists$. + +Dans certains cas, les quantificateurs existentiels et universels sont utilisés au sein de la même formule mathématique. +\begin{itemize} +\item[] $\forall a \cdot \forall b \cdot \forall c \cdot \exists x \cdot ax^{2}+bx+c = 0$ +\end{itemize} +Dans l'exemple ci-dessus, nous avons 4 variables : $a,b,c,x$. Les 3 premières sont des véritables variables, on peut les affecter à n'importe quelle valeur, tandis que la dernière est une inconnue, c'est la solution à trouver. Il faut donc trouver $x$ pour toutes les valeurs possibles de $a,b,c$. +On appelle souvent $a,b,c$ des {\em paramètres}. +\end{framed} + +\section{Règles en logique des prédicats} + +Nous allons maintenant introduire les règles de déduction pour les quantificateurs. +D'abord, nous définissons une manipulation symbolique importante qui est utilisée +dans ces règles: la substitution. +Ensuite nous définissons les quatre règles pour les quantificateurs. + +Comment savons-nous que les règles sont correctes? +On ne peut pas le prouver dans la logique des prédicats: on ne peut pas prouver l'exactitude +des règles avec les règles elles-mêmes! +Il faut faire un raisonnement en dehors de la logique des prédicats. +Nous justifions chaque règle avec un raisonnement basé que un modèle de la formule. +Si la logique des prédicats est notre langage pour formaliser les raisonnements, +on peut donc dire que la justification des règles est faite en dehors de ce langage, donc en {\em meta-langage}. + +\subsection{La substitution} +Une manipulation fréquente en logique des prédicats est la \textbf{substitution}. Elle consiste à prendre une formule et remplacer une partie par une autre. + +Si on a une formule quelconque $p$, la notation $p[x/t]$ veut dire de remplacer toutes les occurrences libres de $x$ par $t$. +Une {\em occurrence libre} d'une variable est une occurrence qui n'est pas dans la portée d'un quantificateur. +Il faut faire attention aux variables dans $t$, pour éviter qu'une variable dans $t$ ne rentre dans la portée d'un quantificateur, +ce qui s'appelle la {\em capture de variable}. +Pour éviter la capture, il faut faire un {\em renommage} de variable, c'est-à-dire, changer les noms des variables dans $p$. +Voici un exemple de $p[x/y]$ où $p = P(x) \rightarrow \forall y \cdot (P(x) \wedge R(y))$ : +\begin{center} +\begin{tabular}{|l |l |>{\raggedright}m{6cm}|} +\hline +1. &$P(x) \rightarrow \forall y \cdot (P(x) \wedge R(y))$&$[x/y]$ veut dire qu'on va remplacer toutes les occurrences libres de $x$ par $y$.\tabularnewline +\hline +2. &$P(y) \rightarrow \forall y \cdot (P(y) \wedge R(y))$&En remplaçant $x$ par $y$, on a changé le sens de la formule, car avant, $x$ n'était pas dans la portée du quantificateur alors que maintenant il l'est. Ce changement de sens s'appelle une \textit{capture de variable}, car la variable $y$ est capturée par le quantificateur. Pour résoudre ce problème, on va effectuer un \textit{renommage}.\tabularnewline +\hline +3. &$P(y) \rightarrow \forall z \cdot (P(y) \wedge R(z))$&Résultat après renommage (pour éviter la capture de variable). +On a changé le $y$ en $z$ (renommage) et remplacé le $x$ par $y$ (substitution). \tabularnewline +\hline +\end{tabular} +\end{center} + +Voici un autre exemple avec $p = \exists y . P(x,y)$. +Nous donnons plusieurs possibilités de substitution correctes: +\begin{itemize} +\item $p[x/y] = \exists z. P(y,z)$ (attention: $y$ a été renommée) +\item $p[x/f(x)] = \exists y. P(f(x),y)$ +\item $p[x/c] = \exists y. P(c,y)$ ($c$ est une constante) +\item $p[x/z] = \exists y. P(z,t)$ +\end{itemize} + +% Ancienne partie 8 + +\subsection{Élimination de $\forall$} +\begin{flushleft} + +Parce que $\forall x . P(x)$ veut dire pour tout $x_{I}$ $\in$ $D_{I}$ : $P_{I}$($x_{I}$) est vrai, +on peut remplacer sans contrainte:$\linebreak \linebreak$ +$\forall$x$\bullet$P(x) $\rightarrow$ P(a) $\>$ a est une constante quelconque\\ +$\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\rightarrow$ P(y) $\>$ y est une variable $\>$ (parce que $P_{I}$($y_{I}$) est vrai)$\linebreak$ + +\underline{Règle :} +\begin{center} +{\LARGE $\frac{\forall x : p}{p[x/t]}$} +\end{center} +\textcolor{red}{\danger\ N'oubliez pas de faire le renommage si nécessaire} + +\underline{Exemple :}\\ +\begin{enumerate} +\item $\forall$x $\bullet$ $\forall$y $\bullet$ P(x,y) $\>$ Pr\'emisse +\item $\forall$y $\bullet$ P(x,y) $\>$ $\>$ $\>$ $\>$ $\>$ Élimination de $\forall$ +\item P(x,x) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ Élimination de $\forall$ +\item $\forall$x $\bullet$ P(x,x) $\>$ $\>$ $\>$ $\>$ $\>$ Introduction de $\forall$ +\end{enumerate} +Le renommage n'est pas nécessaire dans la ligne (3) parce qu'il n'y a pas de capture. + +\subsection{Élimination de $\exists$} + +Il faut faire attention avec cette règle, parce que $\exists x. P(x)$ veut dire qu'il existe +un élément $x_I \in D_I$ pour lequel $P_I(x_I)$ est vrai. +On ne connait pas cet élément, mais on peut introduire un symbole qui le représente:$\linebreak \linebreak$ +$\exists$x $\bullet$ P(x) $\rightarrow$ P(a) \\ +a = nouvelle constante qui n'apparaît nulle part ailleurs ($\mathrm{val}_{I}(a) = x_{I}$) $\linebreak$ \\ + +$\exists$x $\bullet$ P(x) $\rightarrow$ P(z) \\ +z = nouvelle variable dans la preuve ($\mathrm{val}_{I}(z) = x_{I}$) $\linebreak$\\ + +$\exists$x $\bullet$ P(x) $\nrightarrow$ P(y) (pas autorisé)\\ +y = variable qui existe d\'ej\`a dans la preuve, elle a déjà une valeur $\linebreak$ \\ + +\underline{Exemple 1 :}\\ +\begin{enumerate} +\item $\exists$x $\bullet$ chef(x) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>\>$Pr\'emisse +\item $\exists$x $\bullet$ voleur(x) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$Pr\'emisse +\item chef(y) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$Élimination de $\exists$ +\item voleur(y) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ Élimination de $\exists$ \textcolor{red}{(y pas nouvelle)} +\item chef(y) $\wedge$ voleur(y) $\>$ $\>$ $\>$ $\>$ $\>$ Conjonction +\item $\exists$y $\bullet$ chef(y) $\wedge$ voleur(y) $\>$ Introduction de $\exists$ \textcolor{red}{(FAUSSE)} +\end{enumerate} + +\underline{Exemple 2 :}\\ +\begin{enumerate} +\item $\exists$x $\bullet$ chef(x) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$Pr\'emisse +\item $\exists$x $\bullet$ voleur (x) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$Pr\'emisse +\item chef(y) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ Élimination de $\exists$ +\item voleur (z) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ Élimination de $\exists$ +\item chef(y) $\wedge$ voleur(z) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ Conjonction +\item $\exists$y $\exists$z chef(y) $\wedge$ voleur(z) $\>$ Introduction de $\exists$ (EXACTE) +\end{enumerate} + +\subsection{Introduction de $\exists$} + +Si $p[t]$ est vrai cela veut dire qu'il existe un élément $t_I = \mathrm{VAL}_I(t) \in D_I$ avec $(\mathrm{val}_I(p))(t_I)$. +On peut donc introduire $\exists x$ car un élément existe qui rend vrai $p[x]$. +Mais attention, on doit pouvoir trouver la formule originale à partir de $\exists x.p[x]$, +sinon l'introduction du quantificateur ``$\exists$'' a changé le sens de la formule (capture!). + +\underline{R\`egle :} +\begin{center} +{\LARGE $\frac{p[t]}{\exists x \bullet p[x]}$} +\end{center} +Autorisé si la substitution $p[x/t]$ retrouve la formule originale.$\linebreak$ + +\underline{Exemple :} +\begin{center} + P(y,y)\\ +$\exists$x $\bullet$ P(x,x)\\[2\baselineskip] +\sout{P(y,x)}\\ +\sout{$\exists$x $\bullet$ P(x,x)} +\begin{flushright} +\textcolor{red}{Ceci n'est pas correct !} +\end{flushright} +\end{center} +Le deuxième exemple ne marche pas parce que $P(x,x)[x/y]$ ne retrouve pas la formule originale. + +\subsection{Introduction de $\forall$} + +\underline{R\`egle :} +\begin{center} +{\LARGE $\frac{p}{\forall x \bullet p}$} +\end{center} +\begin{itemize} +\item Si $p$ n'a pas d'occurrence libre de $x$ alors c'est OK +\item Si $p$ contient une occurrence libre de $x$ : on doit s'assurer que la preuve jusqu'à cet endroit marchera pour toutes valeurs affectées à $x$\\ +$\> \> \> \hookrightarrow$ Aucune formule dans la preuve jusqu'à cet endroit ne doit mettre une contrainte sur $x$ ! +\end{itemize} +\underline{Deux conditions :} +\begin{itemize} +\item $x$ n'était pas libre dans une formule contenant un quantificateur $\exists$ qu'on a éliminé. +\item $x$ n'est pas libre dans une prémisse (dans ce cas, $x$ serait connu depuis le début donc il possède déjà une valeur). +\end{itemize} + +\underline{Exemple :}\\ +\begin{enumerate} +\item $\forall$x $\exists$y parent(y,x) $\>$ Prémisse +\item $\exists$y parent(y,x) $\>$ $\>$ $\>$ $\>$Élimination de $\forall$ +\item parent(y,x) $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ Élimination de $\exists$ \textcolor{blue}{$\rightarrow$ N'est valable que pour ce y et ce x, pas pour tous} +\item \sout{$\forall$x parent(y,x)} $\>$ $\>$ $\>$ $\>$Introduction de $\forall$ \textcolor{red}{$\rightarrow$ On ne peut pas faire ça, car il y a une contrainte sur x. Là on dit que ce y est parent de tous !} +\end{enumerate} + + + + +\end{flushleft} + +% Ancienne partie 9 + +\section{Exemple plus conséquent} + +Il est important de pouvoir faire des preuves manuellement, car cela permet de bien comprendre toutes les étapes de raisonnement +d'une preuve, même si par la suite on utilise un algorithme plutôt que de faire les preuves à la main. +Terminons donc par un exemple un peu plus conséquent d'une preuve manuelle en logique des prédicats avant d'introduire +l'algorithme permettant d'effectuer des preuves de manière automatisée. + +L'exemple suivant est inspiré de l'Empire Romain: +\subsubsection{Prémisses} +\begin{itemize} + \item Les maîtres et les esclaves sont tous des hommes adultes. + \item Toutes les personnes ne sont pas des hommes adultes. +\end{itemize} +\textit{Note: on voit dans les prémisses qu'il y a des quantificateurs: tous, toutes.} + +\subsubsection{A prouver} +\begin{itemize} + \item Il existe des personnes qui ne sont pas des maîtres. +\end{itemize} + +\subsubsection{Preuve} +\begin{enumerate} + \item $\forall{}x\ (maitre(x)\lor{}esclave(x)\implies{}adulte(x)\land{}homme(x))$ \hfill Prémisse + \item $\lnot{}\forall{}x\ (adulte(x)\land{}homme(x))$ \hfill Prémisse + \item $\exists{}x\ \lnot{}(adulte(x)\land{}homme(x))$ \hfill Théorème de négation\\ + \textit{S' il n'est pas vrai que toutes les personnes sont des hommes adultes alors il existe une personne qui n'est pas un homme adulte} + \item $\lnot{}(adulte(x)\land{}homme(x))$ \hfill Élimination de $\exists$ \\ +\textit{ On élimine le quantificateur existentiel: on peut le faire, car on introduit une variable x qu'on choisit comme étant une personne rendant vraie la proposition.} + \item $(maitre(x)\lor{}esclave(x)\implies{}adulte(x)\land{}homme(x))$ \hfill Élim. de $\forall$ \\ + \textit{On peut retirer le $\forall$ en réduisant le champ de x aux x rendant vraie la proposition.} + \item $\lnot{}(maitre(x)\lor{}esclave(x))$ \hfill Modus Tollens + \item $\lnot{}maitre(x)\land{}\lnot{}esclave(x)$ \hfill De Morgan + \item $\lnot{}maitre(x)$ \hfill Simplification + \item $\exists{}y\ \lnot{}maitre(y)$ \hfill Introduction de $\exists$ \\ + \textit{Comme dans l'interprétation, x est une personne qui rend valable cette proposition, on peut dire qu'il existe une personne rendant valable cette proposition et réintroduire le quantificateur $\exists$} +\end{enumerate} +C'était un exemple très simple ne faisant que quelques pas, mais la logique est assez expressive pour permettre des preuves plus complexes +(par exemple, formaliser les mathématiques). +Le nombre de pas serait alors beaucoup plus important. + +Les mathématiciens ont fait de grands efforts pour formaliser les mathématiques +avec la logique des prédicats. +Nous mentionnons le Principia Mathematica de Whitehead et Russell, et les ouvrages nombreux de Nicolas Bourbaki. + +\section{Note historique} + +\hfill {\begin{minipage}{0.90\textwidth} +\begin{small} +A la fin du 19ème siècle, début du 20ème: +\begin{itemize} +\item Création de la logique de 1er ordre (Gottlob Frege) +\item Deux personnes ont essayé de formaliser toutes les mathématiques. Principia Mathematica (Alfred Whitehead, Bertrand Russell) +\end{itemize} +Lors que l'arrivée des ordinateurs, fin du 20ème siècle (années 50-60 et fin du siècle) on a essayé de formaliser la logique via des algorithmes: +\begin{itemize} +\item Création de l'Algorithme de Preuves (1965): +\begin{itemize} +\item Alan Robinson invente la Règle de Résolution (qui va être expliquée au chapitre suivant) +\item Création de prouveurs (assistants de preuve) par exemple Coq et Isabelle en 1972 +\item Création de la logique de programmation qui aide à l'élaboration de la programmation par contraintes: Prolog (1972) +\end{itemize} +\item Création de la sémantique Web: OWL (Web Ontology Langage) +\end{itemize} +\end{small} +\end{minipage} + +\chapter{Algorithme de preuve pour la logique des prédicats} +\label{algorithmepreuve} + +Dans le chapitre précédent nous avons introduit des règles pour faire des preuves manuelles. +Avec l'arrivée des ordinateurs, les logiciens ont tout de suite essayé de faire des preuves mécanisées. +Nous avons vu dans le chapitre \ref{preuveprop} (Section \ref{algorithmeprop}) +un algorithme de preuve pour la logique propositionnelle qui utilise la réfutation. +La logique des prédicats est beaucoup plus expressive que la logique propositionnelle +et les raisonnement est plus délicat (voir chapitre précédent!). + +Est-ce que nous pouvons faire un algorithme de preuve pour la logique des prédicats? +Cela ne semble pas évident. +Beaucoup de logiciens ont travaillé sur cette question. +La réponse affirmative à la question est un des grands résultats des mathématiques du 20ème siècle. +Dans ce chapitre nous verrons un algorithme de preuve avec une grande puissance. +On peut le faire marcher malgré la complexité des variables et des quantificateurs ce qui est assez étonnant, +car c'est une logique très expressive. + +\section{Propriétés de l'algorithme} + +L'algorithme pour la logique des prédicats +ne garde pas toutes les propriétés de l'algorithme pour la logique propositionnelle, +car la logique des prédicats est beaucoup plus expressive. +En particulier, là où l'algorithme pour la logique propositionnelle est décidable, +l'algorithm pour la logique des prédicats n'est que semi-décidable. + +Supposons $B$ l'ensemble des axiomes (prémisses) et $T$ le théorème que l'on veut prouver. +On a les propriétés suivantes: +\begin{itemize} +\item L'algorithme est {\em adéquat} (``{\em consistent}''): Si $B\vdash T$ alors $B \models T$\\ +Si l'algorithme trouve une preuve de $T$ avec les axiomes $B$ alors $T$ sera vraie dans tous les modèles de $B$. +\item L'algorithme est {\em complet} (``{\em complete}''): Si $B \models T$ alors $B\vdash T$\\ +Si $T$ est vrai dans tous les modèles de $B$ alors l'algorithme trouvera une preuve de $T$ avec les axiomes $B$. +\item L'algorithme est {\em semi-décidable}: +\begin{itemize} +\item Si $B \models T$ alors l'algorithme trouve une preuve. +\item Si $B \not\models T$ il peut tourner en rond indéfiniment. +\end{itemize} +Si $T$ est vrai dans tous les modèles, l'algorithme trouvera une preuve, mais si $T$ n'est pas +vrai dans tous les modèles, l'algorithme peut tourner en rond et ne jamais se terminer. +Le problème est donc que quand l'algorithme prend trop de temps à trouver une preuve, +à un certain moment on doit l'arrêter et l'on n'est jamais certain du résultat. +On ne peut jamais être sûr que l'algorithme n'aurait pas trouvé une preuve si on l'avait laissé tourner plus longtemps. +Il est donc semi-décidable, car ses résultats ne sont totalement fiables que dans le cas ou une preuve est trouvée. +\end{itemize} + +\section{Concepts de base} + +L'algorithme de preuve est basé sur deux idées: +\begin{itemize} +\item Simplification des prémisses. +On transforme les prémisses dans une forme uniforme et simple qui s'appelle forme clausale. +\item Simplification des règles d'inférence. +On garde une seule règle d'inférence, la résolution, qui marche sur la forme clausale. +\end{itemize} +Avec ces deux simplifications, la définition de l'algorithme devient simple aussi. + +\subsection{Forme normale conjonctive (forme clausale)} + +Pour transformer les prémisses en forme clausale, il y a trois étapes: +\begin{enumerate} + \item Formule $\to$ forme prénexe: $$(\ldots{}\forall{}\ldots{}\exists{}\ldots{}\forall{} )\implies \forall{}\exists{}\forall{}(\ldots{})$$ + Tous les quantificateurs sont mis en tête de la formule. Les quantificateurs étant très compliqués à gérer, on transforme la formule pour les extraire de celle-ci. \\ + Les modèles sont préservés durant cette transformation, la formule avant la transformation a les mêmes modèles + que la formule après la transformation. + Cela est vrai parce que les deux formules sont équivalentes. + \item Forme prénexe $\to$ forme Skolem (élimination des $\exists{}$): $$ \forall{}\exists{}\forall{}(\ldots{}) \implies \forall{}\forall{}\forall{}(\ldots{}) $$ + Les quantificateurs existentiels sont très embêtants, car ils sont restrictifs. Ils disent qu'il existe des éléments, mais ne précisent pas lesquels, on va donc les éliminer. \\ + Cette transformation préserve l'{\em existence} des modèles (la satisfaisabilité), + mais pas les modèles eux-mêmes. Ils doivent être modifiés pour conserver la même signification. + \item Forme Skolem $\to$ forme normale conjonctive (forme clausale): + \[\forall \ldots \forall \land_i(\lor_j L_{ij})\] + Cette transformation consiste à transformer la formule en + une conjonction de disjonctions ($\land$ de $\lor$). Les règles pour cette transformation sont + les mêmes règles qu'en logique propositionnelle. \\ + Les modèles sont préservés lors de cette transformation. +\end{enumerate} + +\subsection{Résolution} + +La seule règle d'inférence gardée par l'algorithme s'appelle la résolution. +Cette règle existe déjà dans une forme plus simple dans la +logique des propositions: $$\frac{L\lor C_1, \neg L \lor C_2}{C_1\lor C_2}$$ +Cette règle est simple en logique des propositions, car il n'y a pas de variables: $L$ et $\neg L$ sont directement comparables +(il y a le même $L$ dans les deux). +En logique des prédicats ce n'est plus vrai: on peut avoir $L_1 \lor C_1$ et $\neg L_2 \lor C_2$ avec $L_1$ et $L_2$ qui ont +des variables différentes. +On ne peut donc pas faire la résolution immédiatement. + +Pour pouvoir faire la résolution, il va falloir en quelque sorte ``rendre $L_1$ et $L_2$ identiques''. +On va donc dire: ce ne sont peut-être pas toujours les mêmes, mais, pour certaines valeurs, ils sont identiques. +L'idée sera donc de les rendre identiques en substituant leurs variables par d'autres judicieusement choisies. +Cette opération s'appelle l'{\em unification}. +Prenons un exemple: + +\begin{minipage}{0.25\textwidth} + $L_1$ $=$ $P(x,a)$ \\ + $L_2$ $=$ $P(y,z)$ +\end{minipage} + +Pour que $L_1$ et $L_2$ deviennent identiques, on va restreindre leurs variables en faisant une substitution. +Nous avons les variables $x$, $y$, $z$ et une constante $a$. +Une substitution possible est de remplacer $x$ par $y$ et $z$ par $a$. +On écrit $\sigma = \{(x,y),(z,a)\}$ où $\sigma$ est la substitution. +Si on applique $\sigma$ à $L_1$ et $L_2$ on obtient: +$$L_1 \sigma = P(x,a) \sigma = P(y,a)$$ +$$L_2 \sigma = P(y,z) \sigma = P(y,a)$$ +Les deux formules sont maintenant identiques, et on peut donc faire la résolution. +Cette résolution marche pour toutes les valeurs qui sont limitées par la substitution. +Le résultat ne sera donc pas général. +En résumant, on peut écire la règle de résolution de façon plus générale en y mettant la substitution: +$$\frac{L_1 \lor C_1, \neg L_2 \lor C_2}{(C_1 \lor C_2)\sigma}$$ +Pour faire l'inférence +on choisit le $\sigma$ le plus général possible, ce que nous appellons +l'{\em unificateur le plus général} (``{\em most general unifier}''). +On peut démontrer qu'un unificateur le plus général existe toujours. +C'est cette règle d'inférence que nous allons utiliser dans l'algorithme de preuve. + +\section{Transformation en forme prénexe} + +Etapes de la transformation en formule logiquement équivalente: +\begin{enumerate} + \item Éliminer $\Leftrightarrow$ et $\Rightarrow$ + \item Renommer les variables. + \begin{itemize} + \item Chaque quantificateur ne porte que sur une variable, il faudra en créer de nouvelles si besoin en prenant soin de conserver l'équivalence de la formule . + \item Attention: ne jamais garder le même nom de variable pour une variable libre et une variable liée. + \item Supprimer les quantificateurs si possible. \\ + \end{itemize} + \item Migrer les négations ($\neg$) vers l'intérieur, vers les prédicats. On peut faire cela, car $\neg\exists$ peut être transformé en $\forall\neg$ et vice versa. + \item On peut mettre tous les quantificateurs de la logique des prédicats à l'avant de la formule. +\end{enumerate} +\subsection{Exemple d'une transformation en forme prénexe} +\begin{enumerate} +\item $\forall x [p(x) \land \neg (\exists y) \forall x ( \neg q(x,y)) = > \forall z \exists v \bullet p(a,x,y,v))]$\\ \textit{Expression de base} +\item $\forall x [p(x) \land \neg(\exists y) (\forall x) ($\colorbox{lightgray}{$\neg$} $\neg q(x,y) $\colorbox{lightgray}{$\lor$} $\forall z \exists v \bullet r(a,x,y,v)]$\\\textit{Suppression des $\implies{}$} +\item $\forall x [p(x) \land \neg(\exists y) (\forall $\colorbox{lightgray}{$u$}$)(\neg\neg q($\colorbox{lightgray}{$u$}$,y) \lor $\colorbox{lightgray}{$\cancel{\forall z}$}$\exists v \bullet r(a,$\colorbox{lightgray}{$u$}$,y,v)]$\\\textit{Renommage des variables et suppression des quantificateurs inutiles} +\item $\forall x [p(x) \land$ \colorbox{lightgray}{$\forall y \neg$} $ (\forall u)($ \colorbox{lightgray}{$\cancel{\neg \neg}$} $q(u,y) \lor \exists v \bullet r(a,u,y,v)] $\\$\neg\exists y\ devient\ \forall \ y\ \neg \ et\ simplification\ des\ \neg$ +\item $\forall x [p(x) \land \forall y $ \colorbox{lightgray}{$\exists u \neg$}$(q(u,y) \lor \exists v \bullet r(a,u,y,v)] $\\$\neg\forall u\ devient\ \exists \ u\ \neg$ +\item $\forall x [p(x) \land \forall y \exists u $\colorbox{lightgray}{$(\neg q(u,y) \land \neg (\exists v) \bullet r(a,u,y,v))]$}\\ \textit{Distribution des $\neg$}\textit{(De Morgan)} +\item $\forall x [p(x) \land \forall y \exists u (\neg q(u,y) \land $\colorbox{lightgray}{$(\forall v) \bullet \neg$}$ r(a,u,y,v))]$\\$\neg\exists y\ devient\ \forall \ y\ \neg$ +\item $\forall x$\colorbox{lightgray}{$ \forall y \exists u \forall v \bullet$}$ [p(x) \land (\neg q(u,y) \land \neg r(a,u,y,v))]$\\\textit{Extraction des quantificateurs.} +\end{enumerate} + +% Ancienne partie 10 + +\section{Transformation en forme Skolem} +\subsection{Intuition} + +Cette transformation consiste à éliminer toutes les occurrences de quantificateurs existentiels. +\smallskip + +$(\forall x)(\forall y)(\exists u)(\forall v) \big[ P(x) \wedge \neg Q(u,y) \wedge \neg R(a,u,y,v) \big]$ +\smallskip + + +Dans ce cas-ci, la valeur de $u$ dépend des valeurs de $x$ et $y$. Lorsqu'on a choisi $x$ et $y$, on est alors libre de choisir $u$. +On peut donc supposer qu'une fonction $g(x,y)$ fournit cet élément de façon à conserver la satisfaisabilité de la formule tout en supprimant $(\exists u)$. +\smallskip + +$(\forall x)(\forall y)(\forall v) \big[ P(x) \wedge \neg Q(\textbf{g(x,y)},y) \wedge \neg R(a,\textbf{g(x,y)},y,v) \big]$ +\smallskip + +Après la transformation, l'existence des modèles est préservée. + +\subsection{Règle} + +Pour chaque élimination d'un quantificateur existentiel $(\exists x)$, on remplace sa variable quantifiée par une fonction $f(x_1,...,x_n)$ dont les arguments sont les variables des quantificateurs universels dont $x$ est dans la portée. +Cette transformation ne conserve pas les modèles parce que la formule originale n'utilise pas le symbole $f$ +et la formule transformée utilise un symbole $f$. +Mais la satisfaisabilité est conservée: la première formule a un modèle si et seulement si la deuxième formule en a un. +\smallskip + +\underline{Justification par un exemple:} + +$p: \forall x \forall y \exists z \big[ \neg P(x,y) \vee Q(x,z) \big]$ +\smallskip + +$p_s: \forall x \forall y \big[ \neg P(x,y) \vee Q(x,\textbf{f(x,y)}) \big]$ +\smallskip + +Les modèles de $p$ ne sont les mêmes que les modèles de $p_s$. + +\underline{Pour $p$} +\begin{itemize} + \item Interprétation $I$ + \item $D_I =$ Professeur $\cup$ Université + \item $\mathrm{val}_I(P) = P_I = $ ``a enseigné à l'université'' + \item $\mathrm{val}_I(Q) = Q_I = $ ``est diplômé de l'université'' + \item $\mathrm{val}_I(f)$ n'existe pas (le symbole $f$ n'existe pas dans $p$). +\end{itemize} + +\vspace{\baselineskip} + +\underline{Pour $p_s$} +\begin{itemize} + \item Interprétation $I' = \{ f \leftarrow f_i \} \circ I$ (c'est une extension de $I$) + \item $D_I =$ Professeur $\cup$ Université + \item $\mathrm{val}_I(P) = P_I = $ ``a enseigné à l'université'' + \item $\mathrm{val}_I(Q) = Q_I = $ ``est diplômé de l'université'' + \item $\mathrm{val}_I(f) = f_I : \mathrm{Professeur} \times \mathrm{Université} \rightarrow \mathrm{Université}$ \\ + $f_I(a,b) = $ ``l'université ayant dû diplômer $a$ pour que $a$ puisse enseigner à $b$'' +\end{itemize} + +$p$ admet un modèle $(I)$ si et seulement si $p_s$ admet un modèle $(I')$. + +Que ça ne soit exactement le même modèle ne pose pas de problème pour notre algorithme. L'algorithme par réfutation continue à itérer jusqu'à trouver une contradiction ({\em false}). S'il n'y a pas de modèle pour $p_s$, il n'y a pas de modèle pour $p$ et ça suffit. + +\section{Transformation en forme normale conjonctive} + +On fait les +mêmes manipulations qu'en logique des propositions (voir Section \ref{fnc}). +On transforme la formule en une conjonction de disjonctions. + +\section{La règle de résolution} + +$$ \mbox{\Large $\frac{L_1 \vee C_1, \neg L_2 \vee C_2}{(C_1 \vee C_2)\sigma}$ } $$ + +Cette règle de résolution ne fonctionne que si $L_1$ et $L_2$ sont identiques. + +\underline{Exemple 1:} + +\begin{itemize} + \item $L_1 = P_1(a, y, z)$ + \item $L_2 = P_1(x, b, z)$ +\end{itemize} + +Dans un modèle de $\{L_1, L_2\}$ +il y a un prédicat qui correspond au symbole $P_1$ et il y a un ensemble de triplets qui rendent vrai $P_1$. + +L'unification de $L_1$ et $L_2$ donne $L$ qui représente l'intersection des deux ensembles. On écrit: +\begin{itemize} + \item $L_1 \sigma = L$ + \item $L_2 \sigma = L$ +\end{itemize} + +\vspace{5 mm} +$L_1$ et $L_2$ sont {\em unifiables} s'il existe une substitution $\sigma$ telle que $L_1 \sigma = L_2 \sigma$. +\begin{itemize} + \item $\sigma = \big\{(x,a),(y,b)\big\}$ + \item $L_1 \sigma = P(a,b,z)$ + \item $L_2 \sigma = P(a,b,z)$ +\end{itemize} + +\vspace{5 mm} +\underline{Exemple 2:} +\begin{itemize} + \item $L_1 = P_1(a,x)$ + \item $L_2 = P_2(b,x)$ +\end{itemize} +Il n'y pas de substitution qui existe, car on a deux constantes différentes, l'intersection des deux ensembles est vide. +$L_1$ et $L_2$ ne sont donc pas unifiables. +\smallskip + +\underline{Exemple 3:} + +\begin{itemize} + \item $L_1 = P(f(x), z)$ + \item $L_2 = P(y, a)$ +\end{itemize} + +Dans ce cas-ci, il y a beaucoup de substitutions possibles telles que: +\begin{itemize} + \item $\sigma_1 : \big\{ (y, f(a)), (x,a), (z,a) \big\}$ => $L_1 \sigma_1 = L_2 \sigma_1 = p(f(a), a)$ + \item $\sigma_2 : \big\{ (y, f(x)), (z,a) \big\}$ \hspace{11 mm}=> $L_1 \sigma_2 = L_2 \sigma_2 = p(f(x), a)$ +\end{itemize} +$L_1$ et $L_2$ sont donc unifiables. +On peut démontrer que $\sigma_2$ est l'unificateur le plus général (souvent abbrévié en {\em upg}, +en anglais {\em mgu}: most general unifier). +Il donne les ensembles les plus grands.\\ + +\begin{itemize} + \item Pour que la démonstration soit la plus générale possible, + on préfère toujours l'unificateur $\sigma$ \underline{le plus générale}. + \item On peut démontrer que l'unificateur le plus général est unique. + La démonstration de ce fait est hors de portée pour ce cours. + \item L'upg est calculable. +\end{itemize} + +\vspace{5 mm} +\textbf{\underline{Règle de résolution:}} +\begin{itemize} + \item $p_1, p_2$ clauses + \item $p_1 = L^{+} \vee C_1$ + \item $p_2 = \neg L^{-} \vee C_2$ + \item $ L^{+}$ et $L^{-}$ ont les mêmes symboles de prédicat. + \item $ \big\{L^{+}, L^{-}\big\}$ sont unifiables par l'upg $\sigma$. +\end{itemize} + +\underline{Alors} $$ \mbox{\Large $\frac{L^{+} \vee C_1, \neg L^{-} \vee C_2}{(C_1 \vee C_2)\sigma}$ } $$ + +\section{Algorithme} + +L'algorithme de preuve prend comme entrées un ensemble +de formules (``axiomes'') $\{ \mathrm{Ax}_1, ..., \mathrm{Ax}_n \}$ +et une formule à prouver $\mathrm{Th}$. +Chaque formule est en forme normale conjonctive. +L'algorithme utilise la preuve par contradiction (réfutation): +nous allons donc ajouter $\neg \mathrm{Th}$ à l'ensemble d'axiomes +et essayer de déduire une contradiction ($\mathrm{false}$). +Les déductions utilisent la règle de résolution, qui est bien adaptée +à la forme normale conjonctive. + +L'algorithme n'est pas garantie de terminer. +S'il termine avec une contradiction, cela démontre $\mathrm{Th}$. +S'il termine sans contradiction, cela démontre que l'on ne peut pas prouver $\mathrm{Th}$. +S'il ne termine pas, on est dans le cas de la semi-décidabilité. + +\subsection{Définition de l'algorithme} + +\begin{algorithm} +\KwIn{$S := \big\{ \mathrm{Ax}_1, ..., \mathrm{Ax}_n, \neg \mathrm{Th} \big\}$} +\While{$ \mathrm{false} \notin S$ et il existe une paire de clauses dans $S$ résolvables et non résolues.}{ + Choisir $p_i, p_j$ dans $S$ tel qu'il existe: + \begin{itemize} + \item $L^{+}$ dans $p_i$ + \item $L^{-}$ dans $p_j$ + \item $\big\{ L^{+}, L^{-} \big\}$ unifiable par upg $\sigma$ + \end{itemize} + + Calculer: + \begin{itemize} + \item $r:=(p_i - [L^{+}] \vee p_j - [\neg L^{-}]) \sigma$ + \item $S_i = S \cup \big\{ r \big\}$ + \end{itemize} +} +\eIf{$\mathrm{false} \in S$}{$S$ inconsistent, donc $\mathrm{Th}$ prouvé.}{$S$ consistent, donc $\mathrm{Th}$ non prouvé.} +\end{algorithm} + +\subsection{Exemple d'exécution} +Voici un exemple avant la mise en forme clausale: +\begin{itemize} + \item $(\forall x) \mathit{homme}(x) \wedge \mathit{fume}(x) \Rightarrow \mathit{mortel}(x)$ + \item $(\forall x) \mathit{animal}(x) \Rightarrow \mathit{mortel}(x)$ + \item $\mathit{homme}(\mathit{Ginzburg})$ + \item $\mathit{fume}(\mathit{Ginzburg})$ + \item \textbf{Candidat-théorème:} $\mathit{mortel}(\mathit{Ginzburg})$ +\end{itemize} + +\subsubsection{Initialisation de S} +Après la mise en forme clausale cela donne: +\begin{itemize} + \item P1: $(\forall x) \neg \mathit{homme}(x) \vee \neg \mathit{fume}(x) \vee \mathit{mortel}(x)$ + \item P2: $(\forall x) \neg \mathit{animal}(x) \vee \mathit{mortel}(x)$ + \item P3: $\mathit{homme}(\mathit{Ginzburg})$ + \item P4: $\mathit{fume}(\mathit{Ginzburg})$ + \item P5: $\neg \mathit{mortel}(\mathit{Ginzburg})$ +\end{itemize} + +\subsubsection{Itérations} + +\textbf{\underline{1}} +\begin{itemize} + \item P1 + P5 + \item $\sigma = \big\{ (x, \mathit{Ginzburg}) \big\}$ + \item $r = P6 = \neg \mathit{homme}(\mathit{Ginzburg}) \vee \neg \mathit{fume}(\mathit{Ginzburg})$ +\end{itemize} + +\textbf{\underline{2}} +\begin{itemize} + \item P3 + P6 + \item $\sigma = \big\{ \big\}$ + \item $r = P7 = \neg \mathit{fume}(\mathit{Ginzburg})$ +\end{itemize} + +\textbf{\underline{3}} +\begin{itemize} + \item P4 + P7 + \item $\sigma = \big\{ \big\}$ + \item $r = \mathrm{false}$ +\end{itemize} +Il y a une inconsistence donc le candidat théorème est prouvé. + +\subsubsection{Non-déterminisme} + +Cet algorithme a plusieures sources de non-déterminisme, c'est-à-dire +le choix des clauses et le choix des littéraux dans les clauses. +Ces choix sont faits à chaque itération. +Avec un mauvais choix, l'algorithm peut ne pas terminer ou +faire des déductions inutiles. +Par exemple, si on fait un autre choix lors de la première itération: + +\textbf{\underline{1}} +\begin{itemize} + \item P2 + P5 + \item $\sigma = \big\{ (x, Ginzburg) \big\}$ + \item $r = \neg animal(Ginzburg)$ +\end{itemize} + +C'est une déduction inutile qui n'aide pas pour la démonstration de $\mathrm{Th}$. + +\subsection{Stratégies} + +Pour que cet algorithme soit utilisable en pratique, il est très important +de concrétiser des stratégies pour les choix: +\begin{itemize} + \item Quelles paires $p_i$ et $p_j$ choisir? + \item Quelles $L^{+}$ et $L^{-}$ choisir? +\end{itemize} +Il y a deux possibilités pour ces stratégies qui sont utilisées en pratique, +qui donne lieu à deux sortes de programmes que l'on appelle {\em assistant de preuve} +ou {\em langage logique}. + +Un assistant de preuve, comme Coq ou Isabelle, est fait pour aider un humain à prouver des théorèmes compliqués. +Il utilise donc des stratégies complexes pour réduire un maximum le travail qui doit +être fait par l'être humain. +Les assistants de preuve sont des outils pratique pour prouver formellement des théorèmes mathématiques. + +Un langage logique, comme \textbf{Prolog}, inventé en 1972 par Alain Colmerauer et Robert Kowalski, +utilise {\em volontairement} des stratégies naïves qui permettent de rendre l'algorithme prévisible. +Les axiomes deviennent un {\em programme}. +Cette approche, appellée la programmation logique, donne alors un langage de programmation pratique. +Un exemple de stratégie naïve est la stratégie LUSH qui choisi de haut vers le bas les paires $p_i, p_j$, +et de gauche à droite dans chaque $p_i$. +La programmation logique sera expliquée plus en détail dans la Section \ref{prolog}. diff --git a/partie6-7-8-9.tex b/partie6-7-8-9.tex index 99fcbed..123b039 100644 --- a/partie6-7-8-9.tex +++ b/partie6-7-8-9.tex @@ -728,7 +728,7 @@ \chapter{Algorithme de preuve pour la logique des prédicats} On peut le faire marcher malgré la complexité des variables et des quantificateurs ce qui est assez étonnant, car c'est une logique très expressive. -\subsubsection{Propriétés de l'algorithme} +\section{Propriétés de l'algorithme} L'algorithme pour la logique des prédicats ne garde pas toutes les propriétés de l'algorithme pour la logique propositionnelle, @@ -828,7 +828,7 @@ \subsection{Résolution} On peut démontrer qu'un unificateur le plus général existe toujours. C'est cette règle d'inférence que nous allons utiliser dans l'algorithme de preuve. -\section{Transformation de la formule de base vers la forme prénexe} +\section{Transformation en forme prénexe} Etapes de la transformation en formule logiquement équivalente: \begin{enumerate} diff --git a/partie8.tex b/partie8.tex index 0146271..6ad567c 100644 --- a/partie8.tex +++ b/partie8.tex @@ -1,5 +1,5 @@ -\section{Élimination de $\forall$} +\subsection{Élimination de $\forall$} \begin{flushleft} $\forall$x$\bullet$P(x) $\rightarrow$ P(a) $\>$ a est une constante\\ @@ -21,7 +21,7 @@ \section{Élimination de $\forall$} \item $\forall$x $\bullet$ P(x,x) $\>$ $\>$ $\>$ $\>$ $\>$ Introduction de $\forall$ \end{enumerate} -\section{Élimination de $\exists$} +\subsection{Élimination de $\exists$} $\exists$x $\bullet$ P(x) $\rightarrow$ P(a) $\>$ a = nouvelle constante qui apparaît nulle part ailleurs ($val_{I}(a) = x_{I}$)\\ Il existe un $x_{I}$ $\in$ $D_{I}$ avec $P_{I}$($x_{I}$) est vrai\\ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\>$ $\nrightarrow$ P(y) $\>$ y = variable qui existe d\'ej\`a dans la preuve \\ @@ -46,7 +46,7 @@ \section{Élimination de $\exists$} \item $\exists$y $\exists$z chef(y) $\wedge$ voleur(z) $\>$ Introduction de $\exists$ \end{enumerate} -\section{Introduction de $\exists$} +\subsection{Introduction de $\exists$} \underline{R\`egle :}\\ \begin{center} {\LARGE $\frac{p[t]}{\exists x \bullet p[x]}$} @@ -67,7 +67,7 @@ \section{Introduction de $\exists$} \end{center} $\Rightarrow$ Il doit être possible de retrouver la formule originale en remplaçant.\\ -\section{Introduction de $\forall$} +\subsection{Introduction de $\forall$} \underline{R\`egle :}\\ \begin{center} {\LARGE $\frac{p}{\forall x \bullet p}$} diff --git a/partie9.tex b/partie9.tex index a8a6907..05fd15b 100644 --- a/partie9.tex +++ b/partie9.tex @@ -1,6 +1,7 @@ -Terminons par un exemple un peu plus conséquent d'une preuve manuelle en logique des prédicats avant d'introduire l'algorithme permettant d'effectuer des preuves de manière automatisée. -\subsection{Exemple de preuve manuelle} +\section{Exemple plus conséquent} + Il est important de pouvoir faire des preuves manuellement, car cela permet de bien comprendre toutes les étapes de raisonnement d'une preuve, même si par la suite on utilise un algorithme plutôt que de faire les preuves à la main. +Terminons donc par un exemple un peu plus conséquent d'une preuve manuelle en logique des prédicats avant d'introduire l'algorithme permettant d'effectuer des preuves de manière automatisée. L'exemple suivant est inspiré de l'Empire romain: \subsubsection{Prémisses}