Version sans JavaScript, en lecture seule : les ateliers, les quiz et l’exécution du code n’y sont pas. Version complète · Catalogue · Se connecter
Support de cours · chapitre 9
Forme prénexe et skolémisation
Sortir tous les quantificateurs en tête, remplacer les « il existe » par des fonctions, et arriver à des clauses, prêtes pour la résolution.
Où l'on va
La résolution du chapitre 5 travaille sur des clauses. Pour l'étendre au premier ordre (chapitre 10), il faut ramener toute formule à un ensemble de clauses. Trois étapes :
- la forme prénexe : tous les quantificateurs en tête ;
- la skolémisation : plus de $\exists$ ;
- la forme clausale : la partie sans quantificateur en FNC, les $\forall$ sous-entendus.
La première garde le sens de la formule. La deuxième ne le garde pas, mais garde ce qui compte pour réfuter : la satisfiabilité.
La forme prénexe
Définition
Une formule est en forme prénexe si elle s'écrit $Q_1 x_1\, Q_2 x_2 \ldots Q_n x_n\, M$, où chaque $Q_i$ est $\forall$ ou $\exists$, et où $M$, la matrice, ne contient aucun quantificateur.
Exemple : $\forall x\, \exists y\, (P(x) \to R(x, y))$ est prénexe ; $\forall x\, P(x) \to \exists y\, Q(y)$ ne l'est pas.
Les règles pour sortir un quantificateur
En plus des équivalences du chapitre 8, on utilise celles-ci, à condition que $x$ ne soit pas libre dans $B$ :
| Formule | Équivalente à |
|---|---|
| $\forall x\, A \land B$ | $\forall x\, (A \land B)$ |
| $\exists x\, A \land B$ | $\exists x\, (A \land B)$ |
| $\forall x\, A \lor B$ | $\forall x\, (A \lor B)$ |
| $\exists x\, A \lor B$ | $\exists x\, (A \lor B)$ |
| $B \to \forall x\, A$ | $\forall x\, (B \to A)$ |
| $B \to \exists x\, A$ | $\exists x\, (B \to A)$ |
| $\forall x\, A \to B$ | $\exists x\, (A \to B)$ |
| $\exists x\, A \to B$ | $\forall x\, (A \to B)$ |
Les deux dernières lignes surprennent : un quantificateur qui sort de la gauche d'une implication change de nature. C'est que $A \to B \equiv \lnot A \lor B$, et que la négation échange $\forall$ et $\exists$.
La méthode
- Éliminer $\leftrightarrow$ (et, si l'on veut, $\to$).
- Renommer les variables liées pour qu'elles soient toutes différentes entre elles, et différentes des variables libres. C'est ce qui garantit la condition « $x$ n'est pas libre dans $B$ ».
- Sortir les quantificateurs un à un avec les règles, de l'intérieur vers l'extérieur.
La forme prénexe n'est pas unique : quand deux quantificateurs sortent de deux côtés d'un $\land$, on peut les sortir dans un ordre ou dans l'autre. Tous les résultats sont équivalents.
La skolémisation
L'idée
Dans $\forall x\, \exists y\, R(x, y)$, le $y$ dépend de $x$ : pour chaque $x$, il y a un $y$. On peut donner un nom à ce choix : une fonction $f$ qui, à chaque $x$, associe un tel $y$. La formule devient $\forall x\, R(x, f(x))$. Le nouveau symbole $f$ s'appelle une fonction de Skolem (Thoralf Skolem, 1920).
La méthode
Sur une formule prénexe, on traite les $\exists$ de gauche à droite. Pour chaque $\exists y$ :
- on le supprime ;
- on remplace $y$, dans la matrice, par $f(x_1, \ldots, x_k)$, où $f$ est un symbole neuf, et où $x_1, \ldots, x_k$ sont les variables des $\forall$ placés avant ce $\exists$ ;
- s'il n'y a aucun $\forall$ avant, $f$ n'a pas d'argument : c'est une constante neuve.
Ce que la skolémisation garde
La formule skolémisée n'est pas équivalente à la formule de départ : $P(a)$ affirme quelque chose de l'objet $a$, $\exists x\, P(x)$ non. Mais elles sont équisatisfiables : l'une a un modèle si et seulement si l'autre en a un. C'est tout ce qu'il faut pour la résolution, qui cherche justement à montrer qu'un ensemble n'a pas de modèle.
La forme clausale
Après la skolémisation, il ne reste que des $\forall$ en tête. On met la matrice en FNC (chapitre 3), puis :
- on sous-entend les $\forall$ : toute variable d'une clause est quantifiée universellement ;
- on sépare les clauses ;
- on renomme les variables pour que deux clauses différentes n'en partagent pas. C'est permis, car $\forall x\, (A \land B) \equiv \forall x\, A \land \forall y\, B[x := y]$.