Forme prénexe et skolémisation

1. Le $\forall x$ sort de la gauche de $\to$ et devient $\exists x$ : $\exists x\, \exists y\, (P(x) \to Q(y))$.
2. $\forall x\, \lnot(P(x) \land \forall y\, R(x, y)) \equiv \forall x\, (\lnot P(x) \lor \exists y\, \lnot R(x, y)) \equiv \forall x\, \exists y\, (\lnot P(x) \lor \lnot R(x, y))$.
3. Renommer : $\forall x\, P(x) \land \exists z\, Q(z)$, puis $\forall x\, \exists z\, (P(x) \land Q(z))$. (Ou $\exists z\, \forall x\, (P(x) \land Q(z))$ : les deux sont équivalentes, car les deux quantificateurs portent sur des parties indépendantes.)
4. Le $\exists x$ sort de la gauche et devient $\forall x$ ; puis $\forall y$ et $\exists z$ sortent de la droite : $\forall x\, \forall y\, \exists z\, (P(x) \to Q(y) \lor R(y, z))$.

1. $y$ dépend de $x$ : $f(x)$ ; $w$ dépend de $x$ et $z$ : $g(x, z)$. $\forall x\, \forall z\, R(x, f(x), z, g(x, z))$.
2. $x$ ne dépend de rien : une constante $a$. $\forall y\, R(a, y)$.
3. $z$ dépend de $x$ et $y$ : $\forall x\, \forall y\, (R(x, h(x, y)) \land R(h(x, y), y))$.
4. Deux constantes neuves : $\forall z\, (R(a, z) \to R(z, b))$.

1. Dans tout modèle de $P(a)$, l'objet $a^{\mathcal{M}}$ vérifie $P$ : il existe donc un $x$ qui vérifie $P$.
2. $D = \{1, 2\}$, $a$ interprété par 1, $P = \{2\}$ : $\exists x\, P(x)$ est vraie, $P(a)$ fausse.
3. La résolution cherche à montrer qu'un ensemble n'a pas de modèle. Or $\exists x\, P(x)$ a un modèle si et seulement si $P(a)$ en a un (avec $a$ neuf) : il suffit, dans un modèle de $\exists x\, P(x)$, d'interpréter $a$ par un objet qui vérifie $P$. Les deux sont équisatisfiables, et c'est tout ce que la résolution utilise.

• $\forall x\, (C(x) \to G(x))$ : clause $\lnot C(x) \lor G(x)$.
• $\forall x\, (C(x) \to \mathit{Car}(x))$ : clause $\lnot C(y) \lor \mathit{Car}(y)$ (variable renommée).
• $\exists x\, C(x)$ : skolémisation, $C(a)$ avec $a$ neuf.
• $\lnot A = \lnot \exists x\, (\mathit{Car}(x) \land G(x)) \equiv \forall x\, (\lnot \mathit{Car}(x) \lor \lnot G(x))$ : clause $\lnot \mathit{Car}(z) \lor \lnot G(z)$.

Si l'on avait skolémisé $A$ avant de la nier, on aurait obtenu $\lnot(\mathit{Car}(b) \land G(b))$, qui dit seulement que $b$ n'est pas un carnivore à griffes : bien plus faible que $\lnot A$.