La méthode de résolution de Robinson

Ce document présente la méthode de résolution de Robinson, une technique fondamentale en logique mathématique destinée aux étudiants en informatique et mathématiques. Cette méthode permet de démontrer la validité ou l'insatisfiabilité de formules logiques, notamment dans le cadre des preuves automatiques et de la programmation logique.

La méthode de résolution

La résolution est une méthode purement syntaxique, automatisable, développée par Robinson en 1965. Elle produit des preuves par réfutation, similaire à la démonstration par contradiction : pour prouver la validité d’une formule, on démontre l’insatisfiabilité de sa négation. Cette méthode est simple, efficace et complète, ce qui en fait un choix privilégié pour les preuves automatiques. Elle est à la base du langage de programmation logique Prolog.

La méthode applique une ou deux règles d'inférence sur des formules sous forme clausale.

Résolution close (sans variables)

Soient deux clauses closes (sans variables) C’ et C’’, et un atome p. La clause résolvante de C’ et C’’ sur p est obtenue en supprimant p dans C’ et ¬p dans C’’, puis en prenant l’union des restes.

Exemple :
C’ = {¬p, r}
C’’ = {p, q}
Résolvante = {r, q}

La clause facteur d’une clause C’ est une sous-clause contenant un seul littéral l de C’. Par exemple :

Clause facteur de {q, p} est {q}
Clause facteur de {¬p, q} est {¬p}

Le système d’inférence R0 pour la résolution close est défini par :

• Un alphabet ΣR0 contenant les symboles logiques et les constantes
• Un ensemble FR0 des clauses closes construites sur ΣR0
• Aucun axiome (AR0 = ∅)
• Deux règles d’inférence : résolution (Res) et factorisation (Fact)

La règle de résolution (Res) s’écrit :

De C’ ∪ {p} et C’’ ∪ {¬p} on déduit la clause résolvante C’ ∪ C’’

La règle de factorisation (Fact) permet de simplifier une clause en supprimant les littéraux redondants.

La clause vide (notée □) représente la contradiction, obtenue lorsqu’on déduit p et ¬p.

Propriétés

• Si {C1, C2} ⊢ C alors {C1, C2} ⊨ C (correction)
• La méthode est réfutationnellement complète : si un ensemble ℰ est insatisfiable, on peut déduire □ par R0 (complétude)

Application

Pour montrer qu’un ensemble ℰ de formules closes est insatisfiable :

1. Mettre chaque formule sous forme clausale, obtenant Ω
2. Tant que □ ∉ Ω, choisir deux clauses Ci et Cj dans Ω pour appliquer Res ou une clause Ci pour appliquer Fact
3. Ajouter la clause déduite à Ω

Exemple

Soit ℰ = {p ∨ q, ¬p ∨ q, p ∨ ¬q, ¬p ∨ ¬q}

On applique la résolution et la factorisation pour obtenir la clause vide, prouvant l’insatisfiabilité.

Unification

L’unification est essentielle pour appliquer la résolution aux clauses contenant des variables. Elle consiste à rendre identiques deux expressions en instanciant leurs variables par une substitution.

Définitions

• Substitution s = {x1 ← t1, ..., xn ← tn} où chaque xi est une variable et chaque ti un terme différent de xi.
• Instance Es d’une expression E est l’expression obtenue en appliquant la substitution s à E.
• Composition de deux substitutions s et q, notée s.q, est la substitution résultant de l’application successive de q puis s.
• Unificateur d’un ensemble d’expressions {E1, ..., En} est une substitution s telle que E1s = ... = Ens (égalité syntaxique).
• Unifiable signifie qu’il existe un unificateur pour l’ensemble d’expressions.
• Plus général unificateur (p.g.u) est un unificateur minimal, tel que tout autre unificateur q peut s’écrire q = s.l pour une substitution l.

Exemples

E = {f(x,g(y)), f(x,g(h(b))), f(a,z)}
s = {x ← a, y ← h(b), z ← g(h(b))}
E1s = E2s = E3s = f(a, g(h(b)))

Un unificateur n’est pas unique. Par exemple, pour A = f(x,b) et B = f(g(y),z) :

• s1 = {x ← g(y), z ← b}
• s2 = {x ← g(a), y ← a, z ← b}
• s3 = {x ← g(f(a)), y ← f(a), z ← b}

Algorithme d’unification

Pour unifier deux expressions A et B :

1. Initialiser la substitution s à vide
2. Tant que A s ≠ B s, déterminer les sous-expressions t1 et t2 les plus à gauche telles que rangA(t1) = rangB(t2) et racine(t1) ≠ racine(t2)
3. Si t1 et t2 ne sont pas des variables, ou si une variable apparaît dans son propre terme (occurcheck), alors échec
4. Sinon, si t1 est une variable x, ajouter {x ← t2} à s ; si t2 est une variable x, ajouter {x ← t1} à s
5. Retourner s

Exemple d’unification

A : P(x, f(x), a)
B : P(y, z, u)

Étapes :
s = {}
s := s ∪ {x ← y}
s := s ∪ {z ← f(y)}
s := s ∪ {u ← a}

Résultat : s = {x ← y, z ← f(y), u ← a}

Résolution avec variables

Le système d’inférence R1 étend R0 aux clauses du premier ordre avec variables. Il inclut :

• Un alphabet ΣR1
• Un ensemble FR1 de clauses du premier ordre
• Aucun axiome (AR1 = ∅)
• Deux règles d’inférence : résolution (Res) et factorisation (Fact) avec unification

La règle de résolution devient :

De C’ ∪ {l’} et C’’ ∪ {¬l’’} on déduit (C’ ∪ C’’) s
où s est le p.g.u de l’ et l’’

Il faut veiller à ce que deux clauses différentes n’aient pas de variables communes, ce qui nécessite un renommage préalable des variables.

Exemple de renommage et résolution

Clauses initiales :
P(x), Q(x)

Renommage :
P(x), Q(y)

Résolution avec s = {x ← a} :
De P(a) et ¬Q(a) on déduit ...

Propriétés

• Si {C1, C2} ⊢ C alors {C1, C2} ⊨ C (correction)
• La méthode de résolution avec variables est réfutationnellement complète (Théorème de Robinson)

Application

Pour montrer qu’un ensemble ℰ de formules du premier ordre est insatisfiable :

1. Mettre chaque formule sous forme clausale, obtenant Ω
2. Renommer les variables des clauses de Ω
3. Tant que □ ∉ Ω, choisir deux clauses Ci et Cj dans Ω pour appliquer Res ou une clause Ci pour appliquer Fact
4. Ajouter la clause déduite à Ω

Exemple

Soit ℰ = {¬P(x) ∨ O(x), ¬M(x) ∨ ¬O(x), M(a), P(a)}. On montre que ℰ est insatisfiable par résolution.

Stratégies de résolution

La méthode de résolution est non déterministe car le choix des clauses pour appliquer Res et Fact n’est pas fixé. Une stratégie vise à guider ces choix tout en conservant la complétude.

Définitions

• Clause initiale (input) : clause appartenant à l’ensemble ℰ donné
• Stratégie complète : si ℰ est insatisfiable, la stratégie permet de trouver □
• Stratégie linéaire : à chaque application de Res ou Fact, une des clauses parentes est la dernière clause résolvante obtenue
• Stratégie linéaire input : stratégie linéaire où une des clauses parentes est toujours une clause initiale

La stratégie linéaire est complète, mais la stratégie linéaire input ne l’est pas forcément.

Exemples de stratégies

• Stratégie non linéaire : choix libre des clauses (peut être inefficace)
• Stratégie linéaire : on construit une chaîne de résolutions à partir des clauses initiales
• Stratégie linéaire input : on utilise toujours une clause initiale dans la résolution, mais peut ne pas trouver □

Stratégies basées sur les littéraux

Un littéral positif (l+) est un atome, un littéral négatif (l-) est une négation d’atome.

• Stratégie négative : à chaque application de Res, une des clauses parentes est négative (ne contient que des littéraux négatifs)
• Stratégie positive : à chaque application de Res, une des clauses parentes est positive

Les stratégies négatives et positives sont complètes.

Stratégie ordonnée

Les littéraux de chaque clause sont ordonnés (par exemple, les littéraux positifs en tête), et la résolution n’est permise que sur certains littéraux (ex. le premier littéral).

Une stratégie à la fois linéaire et ordonnée est complète.

Stratégie SLD (Selected Linear Definite)

• Stratégie linéaire input
• Négative
• Ordonnée : littéraux positifs en tête, résolution uniquement sur le premier littéral

Chaque clause résolvante est négative et de la forme {¬A1, ..., ¬An} avec A un atome.

La SLD est généralement non complète sauf si les clauses initiales sont des clauses de Horn (au plus un littéral positif par clause), ce qui est le principe de Prolog.

La règle de factorisation n’est plus nécessaire avec la SLD.

Exemple SLD

Clauses :
¬p ∨ q
¬q ∨ r
¬r ∨ s
¬s

Résolution SLD conduit à la clause vide □

Glossaire des termes clés

• Clause : ensemble de littéraux (atomes ou négations d’atomes) reliés par des disjonctions.
• Clause close : clause sans variables.
• Clause résolvante : clause obtenue par application de la règle de résolution entre deux clauses.
• Clause facteur : sous-clause contenant un seul littéral d’une clause.
• Substitution : ensemble de couples variable-terme permettant de remplacer des variables.
• Instance : expression obtenue en appliquant une substitution à une expression.
• Unificateur : substitution rendant plusieurs expressions identiques.
• Plus général unificateur (p.g.u) : unificateur minimal dont toutes les autres instances sont dérivées.
• Renommage : changement des variables dans une clause pour éviter les conflits.
• Clause de Horn : clause contenant au plus un littéral positif.
• Clause initiale (input) : clause appartenant à l’ensemble de départ.
• Clause vide (□) : clause sans littéraux, représentant une contradiction.
• Stratégie de résolution : méthode pour choisir les clauses sur lesquelles appliquer les règles de résolution.
• Stratégie linéaire : stratégie où une clause résolvante est toujours utilisée dans la résolution suivante.
• Stratégie SLD : stratégie linéaire input, négative et ordonnée, utilisée notamment en Prolog.

Points clés à retenir

• La méthode de résolution est une technique syntaxique pour démontrer l’insatisfiabilité d’un ensemble de clauses.
• La résolution close s’applique aux clauses sans variables, la résolution avec variables nécessite l’unification.
• L’unification calcule une substitution rendant deux expressions identiques, avec un algorithme garantissant un plus général unificateur ou un échec.
• Le renommage des variables est nécessaire pour éviter les conflits lors de la résolution avec variables.
• La méthode de résolution est réfutationnellement complète : elle trouve la contradiction si elle existe.
• Différentes stratégies de résolution existent, certaines complètes (linéaire, négative, ordonnée), d’autres non.
• La stratégie SLD est utilisée en programmation logique (Prolog) mais n’est complète que pour les clauses de Horn.
• La règle de factorisation simplifie les clauses en supprimant les littéraux redondants.