3. Passer du calcul des prédicats aux clauses

3. Passer du calcul des prédicats aux clauses

3.1 Les neuf étapes et leur justification

1. Éliminer les implications et équivalences.

A → B ≡ ¬A ∨ B
A ↔ B ≡ (¬A ∨ B) ∧ (¬B ∨ A)

Une implication interdit précisément le cas A vrai et B faux. La forme ¬A∨B exprime la même condition. L’équivalence exige les deux directions; elle est donnée pour mémoire, car le cours utilise surtout l’implication.

2. Faire descendre les négations et simplifier.

¬¬A ≡ A
¬(A ∨ B) ≡ ¬A ∧ ¬B
¬(A ∧ B) ≡ ¬A ∨ ¬B
¬∃x A ≡ ∀x ¬A
¬∀x A ≡ ∃x ¬A

Il faut conserver la portée des parenthèses. Nier « tout le monde possède une propriété » revient à affirmer l’existence d’un contre-exemple; nier « quelqu’un possède une propriété » revient à dire que personne ne la possède.

3. Distinguer les variables liées.

(∀x p(x,x)) ∧ (∃x q(x))
    → (∀x p(x,x)) ∧ (∃y q(y))

Les deux quantificateurs initiaux lient des occurrences différentes. Renommer le second x évite de les confondre; toutes les occurrences qu’il lie doivent être changées ensemble.

4. Mettre les quantificateurs en préfixe.

∀x ((∃y p(x,y)) ∧ (∀z q(x,z)))
    → ∀x ∃y ∀z (p(x,y) ∧ q(x,z))

Le cours demande de respecter l’ordre et les dépendances. Le déplacement doit éviter la capture : une variable déplacée ne doit pas devenir liée dans une partie où elle était libre. L’étape précédente facilite ce contrôle. Intervertir arbitrairement ∀x∃y et ∃y∀x change en général le sens et les dépendances des témoins.

5. Supprimer les existentiels par skolémisation.

Le témoin est représenté par une nouvelle constante s’il ne dépend d’aucun universel extérieur, ou une nouvelle fonction de ces universels sinon. Les exemples sont détaillés en §3.2. Un même témoin doit être remplacé de manière cohérente dans toutes ses occurrences.

6. Omettre les quantificateurs universels.

Après skolémisation, les universels restants deviennent implicites. ∀x∀y p(x,y) s’écrit alors p(x,y) dans la clause. On ne remplace pas arbitrairement x et y par des constantes : la clause reste générale.

7. Distribuer OU sur ET.

A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C)

On obtient une conjonction de disjonctions. Le ET extérieur reliera les clauses; il ne restera pas à l’intérieur d’une clause.

8. Séparer les facteurs conjonctifs.

(A ∨ B) ∧ C → { A ∨ B, C }
(A ∨ B) ∧ (A ∨ C) → { A ∨ B, A ∨ C }

Une formule unique peut produire une ou plusieurs clauses. Il faut conserver chaque facteur : en supprimer un changerait les connaissances.

9. Renommer les variables entre clauses.

{ p(x,y) ∨ ¬q(y), r(x,x) }
    → { p(x,y) ∨ ¬q(y), r(z,z) }

La première clause et la seconde ont des universels indépendants. Le renommage prépare les applications de résolution. En revanche, on conserve les mêmes symboles de Skolem entre les clauses issues d’une même formule; seuls les arguments variables sont renommés.

Il faut examiner les neuf étapes dans l’ordre, mais une étape peut n’exiger aucune modification. Une formule sans existentiel n’a pas de témoin à introduire; une disjonction déjà simple n’a pas de distribution à faire.

3.2 Les trois cas de skolémisation du cours

Témoin indépendant.

∃x ∀y (p(x,y) ∧ q(x))
    → ∀y (p(k,y) ∧ q(k))

L’existentiel x précède l’universel y : le même témoin convient pour tous les y. k est une constante nouvelle; ce n’est pas un objet déjà utilisé arbitrairement dans la base.

Témoin dépendant de deux universels.

∀x ∀y ∃z p(x,y,z)
    → ∀x ∀y p(x,y,f(x,y))

Le témoin z peut dépendre du couple (x,y). Une constante unique imposerait à tort le même témoin pour tous ces couples.

Témoin dépendant seulement de l’universel extérieur.

∀z ∃x ∀y q(x,y,z)
    → ∀z ∀y q(g(z),y,z)

Le témoin x dépend de z, mais pas du y quantifié après lui. Le préfixe sert donc à déterminer les arguments de g.

La skolémisation conserve la satisfaisabilité dans une signature étendue. Ce n’est pas une équivalence ordinaire avec la formule initiale dans le même vocabulaire. Cette distinction suffit pour la réfutation : on veut conserver la possibilité, ou l’impossibilité, de satisfaire les connaissances et la négation du but.

3.3 Trois conversions complètes

3.3.1 Implication simple

∀x∀y (p(x,y) → q(x,y))
≡ ∀x∀y (¬p(x,y) ∨ q(x,y))
→ { ¬p(x,y) ∨ q(x,y) }

L’implication est supprimée et les universels deviennent implicites. Les variables sont déjà distinctes, les quantificateurs en préfixe, et il n’y a ni existentiel, ni négation composée, ni conjonction à séparer.

3.3.2 Antécédent conjonctif et implication quantifiée

La lecture correspondant aux étapes du diaporama est :

∀x ((r(x) ∧ p(x,M)) → (r(x,C) ∨ ∀y ((∃z r(y,z)) → s(x,y))))

Ici x, y et z sont des variables; M et C sont des constantes de cette formule. Le C de cette notation ne désigne pas la base de clauses des preuves ultérieures.

Supprimer les deux implications :

∀x (¬(r(x)∧p(x,M)) ∨ r(x,C) ∨ ∀y (¬∃z r(y,z) ∨ s(x,y)))

Distribuer les négations : ¬(r∧p) donne ¬r∨¬p, tandis que ¬∃z r(y,z) donne ∀z ¬r(y,z). Le préfixe devient ∀x∀y∀z; aucun existentiel ne subsiste. Omettre les universels donne directement :

{ ¬r(x) ∨ ¬p(x,M) ∨ r(x,C) ∨ ¬r(y,z) ∨ s(x,y) }

Il n’y a qu’une clause. Les signatures r/1 et r/2 sont distinctes. Pour une transcription en Prolog, les constantes M/C doivent être nommées comme des constantes, plutôt qu’être recopiées comme des variables majuscules.

3.4 Exercices de traduction et solutions

Les quatre phrases sur Pierre permettent de distinguer les connecteurs sans ajouter de variables :

Le corrigé distingue va et ira dans le dernier cas, suivant le présent/futur de l’énoncé. La troisième ligne contient deux clauses, chacune devant être vraie; elle n’est pas une disjonction.

Les exercices de prédicats ajoutent deux structures qui se ressemblent, mais ne sont pas équivalentes :

∀x∀y (p(x,y) → (q(x,y) → r(x,y)))
    → { ¬p(x,y) ∨ ¬q(x,y) ∨ r(x,y) }

L’implication imbriquée donne une seule disjonction de trois littéraux.

∀x∀y ((p(x,y) ∨ q(x,y)) → r(x,y))
    → (¬p(x,y) ∧ ¬q(x,y)) ∨ r(x,y)
    → (¬p(x,y) ∨ r(x,y)) ∧ (¬q(x,y) ∨ r(x,y))
    → { ¬p(x,y) ∨ r(x,y), ¬q(w,v) ∨ r(w,v) }

Dans le second cas, la négation de l’antécédent produit un ET, puis la distribution produit deux clauses. Le corrigé renomme effectivement les variables de la seconde. La place des parenthèses détermine donc la conversion.