\documentclass[11pt]{article}

\usepackage{fullpage,french,epsf,fancyheadings}

\pagestyle{fancy}
\lhead{Résolution propositionnelle}
\rhead{Jean-Christophe Filliâtre}

\newcommand{\vrai}{\mbox{\sc Vrai}}
\newcommand{\faux}{\mbox{\sc Faux}}
\newcommand{\prop}{proposition}
\newcommand{\imp}{\rightarrow}
\newcommand{\lorb}{\stackrel{}{\bar{\lor}}}
\newcommand{\landb}{\stackrel{}{\bar{\land}}}
\newcommand{\Caml}{Caml Light}
\newcommand{\C}[1]{{\cal C}(#1)}

\newtheorem{defi}{Définition}
\reversemarginpar
\newcommand{\question}{\marginpar{\hfill$\Box$}}


\begin{document}

\begin{center}
  {\Large\bf Devoir surveillé} \\[1em]
  {\huge\bf Résolution propositionnelle} \\[1em]
  {\normalsize 3 décembre 1996 -- 2 heures}
\end{center}


\paragraph{Logique propositionnelle.}

On se donne un ensemble de symboles de propositions atomiques. On définit
alors l'ensemble des propositions de la manière suivante :
\begin{itemize}
  \item \vrai\ et \faux\ sont des propositions ;
  \item si $P$ est un symbole de proposition atomique alors $P$ est une
    proposition ;
  \item si $P$ est une proposition alors $\neg P$ est une \prop\ ;
  \item si $P$ et $Q$ sont des \prop s, alors $P \imp Q$, $P \land Q$
    et $P \lor Q$ sont des \prop s.
\end{itemize}

\noindent On représentera les propositions par le type \Caml\ suivant :
\begin{verbatim}
     type proposition_atomique == string;;

     type proposition =
         Atome of proposition_atomique
       | Vrai
       | Faux
       | Neg of proposition
       | Imp of proposition * proposition
       | Et  of proposition * proposition
       | Ou  of proposition * proposition ;;
\end{verbatim}

\paragraph{Exemples.} 
La proposition $A \imp (A \imp B) \imp B$ est représentée par le terme
suivant :
\begin{verbatim}
     let A = Atome "A" and B = Atome "B" in Imp (A, Imp (Imp (A,B), B));;
\end{verbatim}

\noindent On sait que la logique propositionnelle est décidable ; on peut
par exemple examiner les tables de vérité des propositions (Post,
1921). On se propose ici d'implanter un autre algorithme de décision :
la résolution propositionnelle.


\section{Forme normale conjonctive}

\begin{defi}[Clauses et formes clausales]
  Une {\em clause} est une proposition de la forme $A_1 \lor A_2 \lor \ldots
  \lor A_n$ où $A_i$ est une \prop\ atomique, la négation
  d'une \prop\ atomique, \faux\ ou $\neg\faux$.
  Une {\em forme clausale} est une proposition de la forme
  $C_1 \land C_2 \land \ldots \land C_n$ où $C_i$ est une clause.
\end{defi}

\noindent Pour des raisons pratiques, on représentera les clauses et les
formes clausales par des listes :
\begin{verbatim}
     type clause == proposition list;;
     type forme_clausale == clause list;;
\end{verbatim}

\noindent Ecrire \question une fonction
{\tt union : 'a list ->~'a list ->~'a list}
effectuant la concaténation de deux listes en supprimant les répétitions.

\medskip
Soient $C^1 = C_1^1 \lor \ldots \lor C_1^n$ et
$C^2 = C_2^1 \lor \ldots \lor C_2^m$ deux clauses. On note $C_1 \lorb C_2$
l'``union'' de ces deux clauses, c'est-à-dire la disjonction
$C_1^1 \lor \ldots \lor C_1^n \lor C_2^1 \lor \ldots \lor C_2^m$
dans laquelle on a supprimé toute répétition.
De même, si $F_1$ et $F_2$ sont deux formes clausales, on note $F_1 \landb F_2$
leur ``union'', c'est-à-dire la conjonction de leurs clauses parmi lesquelles
on a supprimé toute répétition.

Les deux opérations $\lorb$ et $\landb$ sont donc tout simplement réalisées
par la fonction \verb!union!.

\medskip
Soit $A = A_1 \land \ldots \land A_n$ et 
$B = B_1 \land \ldots \land B_m$ deux formes clausales (les $A_i$ et $B_i$
étant des clauses).  On note $A \otimes B$ la forme clausale définie par
$$A \otimes B = \bar{\bigwedge\limits_{i,j}} A_i \lorb B_j$$

\noindent Ecrire \question une fonction
{\tt prod : forme\_clausale ->~forme\_clausale ->~forme\_clausale}
implantant l'opération $\otimes$.

\medskip
\noindent Quelle \question est la complexité de {\em votre} implantation
de la fonction \verb!prod! en fonction de la taille des formes clausales
passées en arguments et en terme de nombre d'opérations \verb!::! ?


\begin{defi}[Mise en forme clausale]
  Soit $P$ une proposition. On définit sa {\em forme clausale} $\C{P}$,
  ou forme normale conjonctive, de la manière suivante :
  \begin{itemize}
  \item Si $P$ est une \prop\ atomique, la négation d'une \prop\ atomique,
    \faux\ ou $\neg\faux$, alors $\C{P} = P$ ;
  \item $\C{A \land B} = \C{A}      \landb  \C{B}$ ;
  \item $\C{A \lor  B} = \C{A}      \otimes \C{B}$ ;
  \item $\C{A \imp  B} = \C{\neg A} \otimes \C{B}$ ;
  \item $\C{\vrai} = \neg\faux$ et $\C{\neg\vrai} = \faux$ ;
  \item $\C{\neg(A \land B)} = \C{\neg A}  \otimes  \C{\neg B}$ ;
  \item $\C{\neg(A \lor  B)} = \C{\neg A}  \landb  \C{\neg B}$ ;
  \item $\C{\neg(A \imp  B)} = \C{A} \landb \C{\neg B}$ ;
  \item $\C{\neg\neg A} = \C{A}$.
  \end{itemize}
\end{defi}

\noindent Justifier \question la ``terminaison'' de cette définition.

\medskip
\noindent Ecrire \question une fonction {\tt fnc : proposition 
->~forme\_clausale} qui calcule la forme clausale $\C{P}$ d'une proposition
$P$ passée en argument.

\medskip
\noindent {\bf Applications :} \question Calculer la forme clausale
des propositions suivantes : $(A \land B) \imp A$, $A \imp (A \land B)$
et $A \imp (A \imp B) \imp B$.

\paragraph{Proposition.} {\em Soit $P$ une proposition. $P$ est vraie
si et seulement si $\C{P}$ est vraie.}


\section{Méthode de résolution}

\begin{defi}[Règle de résolution]
  De deux clauses
  $$\begin{array}{l}
  P = B_1 \lor \ldots \lor B_k \lor A \lor B_{k+1} \lor \ldots \lor B_n \\
  Q = C_1 \lor \ldots \lor C_l \lor \neg A \lor C_{l+1} \lor \ldots \lor C_p
  \end{array}$$
  on peut déduire la clause 
  $$ R = (B_1 \lor \ldots \lor B_k \lor B_{k+1} \lor \ldots \lor B_n)
  \lorb  (C_1 \lor \ldots \lor C_l \lor C_{l+1} \lor \ldots \lor C_p)$$
  Lorsque cette clause est vide on pose $R = \faux$.
\end{defi}


Soient deux clauses $A$ et $B$. La règle de résolution peut s'appliquer,
ou ne pas s'appliquer, aux clauses $A$ et $B$.
Le cas échéant, elle peut parfois s'appliquer de plusieurs
fa\c cons différentes. On représentera donc le résultat d'une résolution
de $A$ et $B$ par la liste des clauses que l'on peut obtenir à partir de 
$A$ et $B$ par résolution.

\medskip
\noindent {\bf Exemple :}
Si $A = P \lor \neg Q$ et $B = Q \lor R \lor \neg P$ alors le résultat
est la liste de deux clauses :
$$[ P \lor R \lor \neg P \,;\, \neg Q \lor Q \lor R ]$$

\medskip
\noindent Ecrire \question une fonction
{\tt enleve : 'a list ->~'a ->~'a list} qui enlève un élément d'une liste.

\medskip
\noindent Ecrire \question une fonction
{\tt resolutions : clause ->~clause ->~clause list}
qui calcule toutes les résolutions possibles de deux clauses.

\medskip
\noindent Ecrire \question une fonction {\tt succes : clause list ->~bool}
qui teste si la clause $\faux$ apparait dans une liste de clauses
(test de succès).

\paragraph{Proposition (Robinson, 1965).}
{\em Soit $P$ une propoistion et $C_1 \land \ldots \land C_n$ la forme clausale
de $\neg P$. Alors $P$ est vraie si et seulement si $\faux$ est dérivable
par résolution propositionnelle à partir des clauses $C_1, \ldots, C_n$.}


\bigskip
\noindent En déduire \question une fonction
{\tt decision : proposition ->~bool}
qui, appliquée à $P$, renvoie \verb!true! si $P$ est vraie
et \verb!faux! sinon.

\medskip
\noindent{\bf Indication :} Etant donnée une liste de clauses
$l = c_1,\ldots,c_n$, on pourra dans un premier temps calculer toutes
les paires $\{x,y\}$ d'éléments distincts de $l$. Ensuite, pour chaque
paire $\{x,y\}$ on pourra calculer avec \verb!resolutions! la liste de
toutes les résolutions de $x$ et $y$. Si cette liste contient la
clause réduite à \faux, alors on retourne \verb!true!.  Sinon, pour
chaque résolution $r$, on rappelle récursivement la procédure de
décisions sur $(l \backslash \{x,y\}) \cup \{r\}$.

\bigskip
\noindent Quelle \question est la complexité de {\em votre} implantation
de la résolution propositionnelle en fonction du nombre $n$ de clauses et
de la taille maximale $t$ des clauses ?
Comparer cette complexité avec la méthode des tables de vérité.


\paragraph{\bf Application : le Club Ecossais.}
Il existe en Ecosse un club très fermé qui obéit aux règles suivantes :
\begin{itemize}
  \item Tout membre non-écossais porte des chaussettes rouges ;
  \item Tout membre porte un kilt ou ne porte pas de chaussettes rouges ;
  \item Les membres mariés ne sortent pas le dimanche ;
  \item Un membre sort le dimanche si et seulement s'il est écossais ;
  \item Tout membre qui porte un kilt est écossais et marié ;
  \item Tout membre écossais porte un kilt.
\end{itemize}

On souhaite prouver que ce club est si fermé qu'il ne peut accepter personne !

\medskip
\noindent Donner \question une proposition $P$ telle que $P$ est vraie
si et seulement si aucun membre ne peut être accepté dans ce club.

\medskip
\noindent Appliquer \question la fonction \verb!decision! ci-dessus à cette
proposition pour montrer qu'aucun membre ne peut être accepté dans ce club.


\end{document}
