\documentclass[a4paper]{article}
\usepackage{entete}
\author{Référence~: Fondements mathématiques de l'informatique. \\ Jacques~\textsc{Stern}}
\title{Complétude de la méthode de résolution.}
\date{2011-2012}

\begin{document}
\maketitle

Rappelons la méthode de résolution pour un ensemble $\mathfrak F$ de formules closes~:
\begin{enumerate}
    \item on met chaque formule sous forme prénexe ;
    \item on skolemise ces formules ;
    \item on distribue les quantificateurs.
\end{enumerate}
On a maintenant un ensemble de clauses, qu'on note $\{C_1,\ldots,C_r\}$. On renomme les variables de chaque clauses pour que
$$\forall i\not = j,~ Var(C_i) \cap Var(C_j) = \emptyset.$$
On cherche à appliquer la règle de résolution~:

\begin{defi}[règle de résolution]
    Soient $C,C_1,C_2$ trois clauses. On dit que $C$ est une {\em résolvante} de $C_1$ et $C_2$ s'il existe $S_1 \subset C_1$ et $S_2\subset C_2$ deux ensembles de littéraux tels que~:
    \begin{itemize}
        \item $S_1$ et $\lnot S_2$ sont unifiables par $\sigma$ unificateur principal ;
        \item $C = ((C_1 \backslash S_1) \cup (C_2 \backslash S_2))\sigma$.
    \end{itemize}
\end{defi}

Un {\em arbre de résolution} est un arbre dont les feuilles sont étiquetées par des clauses de $\Sigma$, et chaque nœud a deux fils dont il est une résolvante.

Si la racine de l'arbre est la clause vide $\qedsymbol$, alors on dit que l'arbre est un arbre de {\em réfutation}.

On se donne un langage $L$ qui a au moins un symbole de constante. On rappelle la définition d'un modèle de Herbrand (Jacques Herbrand, 1908 - 1931)~:
\begin{defi}
    On appelle {\em modèle de Herbrand} $\mathfrak H$ une réalisation de $L$ de domaine $H$ qui a les propriétés suivantes~:
    \begin{itemize}
        \item $H$ est l'ensemble de tous les termes clos de $L$ ;
        \item chaque constante est interprétée par elle-même ;
        \item l'interprétation d'une fonction $f$ d'arité $n$ est la fonction $t_1,\ldots,t_n \mapsto f(t_1,\ldots,t_n)$, où les $t_i$ sont des termes ;
        \item à chaque formule atomique close $R(t_1,\ldots,t_n)$ on associe une {\em variable de Herbrand}, $p[R(t_1,\ldots,t_n)]$.
    \end{itemize}
    On associe alors à la distribution de vérité $\sigma$ le modèle de Herbrand $\mathfrak H(\sigma)$ en interprétant $R$ par
        $$R^{\mathfrak H(\sigma)} = \{(t_1,\ldots,t_n)~|~\sigma(p[R(t_1,\ldots,t_n)]) = 1\}.$$

\end{defi}

\begin{defi}
    À toute formule du calcul propositionnel $F$ sur les variables de Herbrand, on associe une formule close sans quantificateur $\Phi(F)$ définie par induction, en partant de 
    $$\Phi(p[R(t_1,\ldots,t_n)]) = R(t_1,\ldots,t_n).$$
\end{defi}

On a alors clairement $Val(F,\sigma) = Val(\Phi(F),\mathfrak A(\sigma))$.

On définit maintenant une particularisation~:

\begin{defi}
    Soit $F$ une formule close. On appelle {\em particularisation} de $F$ toute formule qui s'écrit $F(\EnsQ{x_1}{t_1},\ldots,\EnsQ{x_n}{t_n})$ où les $t_i$ sont des termes clos.
\end{defi}

On a alors le~:
\begin{thm}[de Herbrand]
    Soit $\Sigma$ un ensemble de formules closes universelles. Alors l'une ou l'autre des propositions est vraie~:
    \begin{itemize}
        \item il existe un modèle de Herbrand qui satisfait $\Sigma$ ;
        \item il existe un ensemble fini de particularisations de formules de $\Sigma$ qui est contradictoire.
    \end{itemize}
\end{thm}

\begin{proof}
    On remplace chaque formule de $\Sigma$ par l'ensemble de ses particularisations. On obtient ainsi un ensemble $\Sigma'$ de formules closes. Par $\Phi$, cet ensemble provient d'un ensemble de formules du calcul propositionnel~:
    $$\Sigma' = \{\Phi(F)~|~F \in \Sigma_0 \}.$$

    S'il existe $\sigma$ qui satisfait $\Sigma_0$, alors le modèle de Herbrand $\mathfrak A(\sigma)$ satisfait toutes les formules de $\Sigma'$ et donc de $\Sigma$.

    Si $\Sigma_0$ est contradictoire, alors par compacité du calcul propositionnel, on a un sous-ensemble fini de $\Sigma_0$ qui est contradictoire, et par $\Phi$, on a un sous-ensemble fini de $\Sigma'$ qui est contradictoire.
\end{proof}

\begin{thm}[de complétude de la méthode de résolution]
    Soit $\Sigma$ un ensemble de clauses contradictoire. Alors il existe un arbre de résolution qui réfute $\Sigma$.
\end{thm}

\begin{proof}
    Notons $\Sigma'$ l'ensemble des particularisations des clauses de $\Sigma$.

    Par le théorème de Herbrand, $\Sigma'$ est contradictoire. Via l'application $\Phi$, on a un ensemble de formules propositionnelles contradictoire.

    On a donc un arbre de réfutation au sens propositionnel qui réfute $\Sigma'$. On va remplacer chaque nœud $c$ de l'arbre par une clause $C$ dont elle est une particularisation. Pour les feuilles, la construction est évidente. Pour les nœuds internes, on utilise le
    \begin{lem}[de relèvement]
        Soient $C_1$ et $C_2$ des clauses au sens du calcul des prédicats, et soient $c_1$ et $c_2$ des clauses propsitionnelles qui en sont respectivement des particularisations. Alors pour toute résolvante $c$ de $c_1$ et $c_2$, il existe une résolvante $C$ de $C_1$ et $C_2$ donc $c$ est une particularisation.
    \end{lem}
    \begin{prooflem}
        Quitte à renommer les variables, on peut supposer que les variables $x_1,\ldots,x_n$ de $C_1$ et $y_1,\ldots,y_p$ de $C_2$ sont distinctes. 

        $c_1$ et $c_2$ étant des particularisations, il existe des termes $t_1,\ldots,t_n,t_1',\ldots,t_p'$ tels que $c_1$ et $c_2$ proviennent de $C_1$ et $C_2$ par la substitution
        $$\tau = ( \EnsQ{x_1}{t_1},\ldots,\EnsQ{y_p}{t_p'} ).$$

        Soit $u$ le littéral qui intervient dans la coupure de $c_1$ et $c_2$. On définit $S_1$ (resp. $S_2$) l'ensemble $L$ des littéraux de $C_1$ (resp. $C_2$) tels que $L\tau$ conduise à $u$ (resp. $\overline u$).

        Alors $S_1 \cup \lnot S_2$ est unifiable par $\tau$. On choisit un unificateur principal $\sigma$~: on a $\tau = \sigma \theta$.

        $c$ est obtenue par l'action de $\tau$ sur l'ensemble de littéraux
        $$(C_1 \backslash S_1) \cup (C_2 \backslash S_2),$$
        c'est-à-dire par l'action de $\theta$ sur la résolvante de $C_1$ et $C_2$
        $$C = ((C_1 \backslash S_1) \cup (C_2 \backslash S_2))\sigma.$$
        Comme $\theta$ élimine toutes les variables de $C$, $c$ est la particularisation de $C$ obtenue en remplaçant chaque variable $x$ par $x\theta$.
    \end{prooflem}
\end{proof}

\end{document}