4. Résolution, unification et réfutation

4. Résolution, unification et réfutation

4.1 La résolvante

Le modèle propositionnel est :

¬A ∨ B     ¬B ∨ C
----------------- résolution sur B
     ¬A ∨ C

On supprime un couple de littéraux complémentaires et réunit les littéraux restants. La nouvelle clause est la résolvante. Le raisonnement correspond à la transitivité de A→B et B→C.

Au premier ordre, les deux atomes peuvent ne pas être écrits à l’identique. Pour L∨Γ et ¬L′∨Δ, on cherche une substitution θ rendant L et L′ identiques. Après renommage des variables pour distinguer les deux clauses, la résolvante est :

(Γ ∨ Δ)θ

Γ et Δ sont les parties restantes; θ est appliquée à tous leurs termes concernés, pas seulement au couple retiré. La substitution sert à ces clauses dans cette application; elle ne réécrit pas toutes les autres clauses de la base.

4.2 Unifier correctement

Une constante ne s’unifie qu’avec elle-même. Une variable peut être liée à une autre variable ou à un terme compatible. Pour des termes composés, le symbole et l’arité doivent correspondre, puis leurs arguments doivent être compatibles. Écrire x↦b signifie remplacer x par b dans les occurrences concernées.

Le premier exemple du support donne :

C1 : ¬p(x) ∨ q(b,y)
C2 : ¬q(x,a) ∨ r(x,y)

Les variables étant locales, renommer C2 :

C2 : ¬q(u,a) ∨ r(u,v)

Pour résoudre q et ¬q, l’unificateur le plus général est {u↦b, y↦a}. Il ne lie ni x dans C1, ni v dans C2. La résolvante est :

¬p(x) ∨ r(b,v)

Le support annonce ¬p(b)∨r(b,a). Ce résultat est une instance valide si l’on ajoute x↦b et v↦a; il n’est pas le résultat le plus général du couple choisi. Ne pas obtenir ces liaisons supplémentaires en confondant les noms identiques de deux clauses indépendantes.

Le second exemple est :

C1 : p(x) ∨ p(f(y)) ∨ r(x,y)
C2 : q(w) ∨ ¬p(f(w))

Résoudre p(f(y)) et ¬p(f(w)), avec w↦y, donne :

p(x) ∨ r(x,y) ∨ q(y)

La substitution inverse y↦w convient également avec un résultat renommé de façon cohérente. On ne supprime pas aussi p(x) : une application retire le couple sélectionné, pas tous les littéraux de même prédicat.

4.3 La procédure de réfutation

Pour établir le but B à partir de la base C :

1. Convertir les connaissances en clauses si nécessaire.
2. Nier B, convertir ¬B en clauses et les ajouter à C.
3. Choisir deux clauses ayant un couple complémentaire unifiable.
4. Renommer, unifier et construire la résolvante.
5. Si elle est non vide, l’ajouter à la base et recommencer.
6. Si elle est vide, conclure explicitement que B est déductible de C.

L’image du « sac de clauses » donnée dans les conseils est utile : les clauses initiales et nouvelles sont toutes disponibles. Elles ne sont pas consommées par une résolution; on peut réutiliser une clause plusieurs fois. Plusieurs chemins peuvent conduire à une preuve correcte.

Le raisonnement est : C et ¬B conduisent à une contradiction, donc aucune interprétation ne peut satisfaire C tout en rendant B faux. Ainsi C ⊨ B. La correction signifie que toute interprétation satisfaisant les prémisses satisfait la conclusion démontrée.

La trace demandée utilise la résolution binaire pour dériver ses nouvelles clauses. Il faut identifier les deux lignes parentes et la substitution, plutôt que mêler librement les règles d’inférence étudiées auparavant. Les conversions préalables ne sont pas des résolvantes; il faut distinguer ces deux phases.

Un arrêt parce qu’« aucun progrès n’est perceptible » est un arrêt pratique proposé par le support. Il ne démontre pas à lui seul ¬B ni l’impossibilité d’une preuve. Une recherche peut manquer un chemin ou ne pas terminer. Si C est déjà contradictoire, une réfutation ne fournit pas une validation factuelle indépendante du but : les hypothèses doivent aussi être pertinentes.

La complétude pour la réfutation signifie que tout ensemble insatisfaisable possède une réfutation dans un système complet. Une recherche équitable doit éviter de délaisser indéfiniment les possibilités nécessaires à cette preuve. Cette propriété permet de trouver une réfutation lorsqu’elle existe, avec une procédure complète et équitable; elle ne garantit pas un arrêt lorsque l’ensemble est satisfaisable. La correction des étapes, la possibilité de trouver toute réfutation et la terminaison sur toute entrée restent donc distinctes.