Règle de résolution

En logique mathématique, la règle de résolution ou principe de résolution de Robinson est une règle d'inférence logique qui généralise le modus ponens. Cette règle est principalement utilisée dans les systèmes de preuve automatiques, elle est à la base du langage de programmation logique Prolog.

En logique propositionnelle

La règle du modus ponens s'écrit ${\displaystyle {\frac {p\qquad p\rightarrow q}{q}}}$ et se lit : de p et de "p implique q", je déduis q. On peut réécrire l'implication "p implique q" comme "p est faux ou q est vraie". Ainsi, la règle du modus ponens s'écrit ${\displaystyle {\frac {p\qquad (\lnot p\lor q)}{q}}}$.

La règle de résolution, elle, généralise la règle du modus ponens car elle s'applique sur des clauses quelconques. Une clause est une formule qui est une disjonction (un "ou") de littéraux (une proposition atomique ou une proposition atomique précédée d'une négation). Par exemple ${\displaystyle (\lnot p\lor q)}$ est une clause avec deux littéraux ("non p" et "q"). Ainsi, en logique propositionnelle, la règle de résolution s'écrit :

${\displaystyle {\frac {(p\lor L_{1}\lor \dots L_{n})\qquad (\lnot p\lor M_{1}\lor \dots \lor M_{k})}{(L_{1}\lor \dots L_{n}\lor M_{1}\lor \dots \lor M_{k})}}}$

Autrement dit, étant donné deux clauses ${\displaystyle (p\lor L_{1}\lor \ldots \lor L_{n})}$ et ${\displaystyle (\lnot p\lor M_{1}\lor \ldots \lor M_{k})}$, on en déduit ${\displaystyle (L_{1}\lor \dots L_{n}\lor M_{1}\lor \dots \lor M_{k})}$. La formule déduite, c'est-à-dire ${\displaystyle (L_{1}\lor \dots L_{n}\lor M_{1}\lor \dots \lor M_{k})}$ est appelé résolvant de ${\displaystyle (p\lor L_{1}\lor \ldots \lor L_{n})}$ et ${\displaystyle (\lnot p\lor M_{1}\lor \ldots \lor M_{k})}$. Bien sûr, l'application de la règle est donnée à permutation près des littéraux.

Exemples

Par exemple :

${\displaystyle {\frac {(a\lor \lnot b\lor \lnot c)\qquad (b\lor e\lor \lnot f)}{(a\lor \lnot c\lor e\lor \lnot f)}}}$

${\displaystyle {\frac {p\qquad \lnot p}{\bot }}}$ où ${\displaystyle {\bot }}$ dénote la contradiction (clause vide).

En logique des prédicats

En logique des prédicats les formules atomiques sont de la forme ${\displaystyle P(t_{1},\ldots ,t_{n})}$ où ${\displaystyle P}$ est un symbole de prédicat et les ${\displaystyle t_{i}}$ sont des termes composés de constantes, de variables et de symboles de fonctions. La règle de résolution en logique des prédicats est similaire à la règle de résolution en logique propositionnelle mais les formules atomiques partagées par deux clauses ne doivent pas être identiques mais unifiables. Deux formules atomiques sont unifiables s'il existe une substitution des variables par des termes qui rend les deux formules identiques (voir unification). Par exemple :

${\displaystyle {\frac {P(a)\qquad (\lnot P(x)\lor Q(x))}{Q(a)}}}$

est une application de la règle de résolution en logique des prédicats. Elle se lit : de "P(a)" et de "(pour tout x) non P(x) ou Q(x)", je déduis "Q(a)". Ici, la formule atomique ${\displaystyle P(a)}$ et la formule atomique ${\displaystyle P(x)}$ sont unifiables avec la substitution ${\displaystyle x\mapsto a}$. Plus généralement, la règle de résolution en logique des prédicats est :

${\displaystyle {\frac {(A\lor L_{1}\lor \dots L_{n})\qquad (\lnot B\lor M_{1}\lor \dots \lor M_{k})}{(L_{1}[\sigma ]\lor \dots L_{n}[\sigma ]\lor M_{1}[\sigma ]\lor \dots \lor M_{k}[\sigma ])}}}$

où ${\displaystyle \sigma }$ est un unificateur principal des formules atomiques ${\displaystyle A}$ et ${\displaystyle B}$.

On peut effectuer la résolution sur deux littéraux s'ils portent sur des formules atomiques identiques ou sur des formules unifiables.

Par exemple, les formules atomiques

${\displaystyle P(x,a,y)}$ et ${\displaystyle P(c,a,z)}$, où a et c sont des constantes,

sont unifiables par la substitution ${\displaystyle x\to c,y\to z}$. Par contre

${\displaystyle P(x,a,y)}$ et ${\displaystyle P(c,b,z)}$, où a, b et c sont des constantes,

ne sont pas unifiables car les constantes ne peuvent être remplacées.

Exemple

${\displaystyle C_{1}=\lnot P(x)\lor \lnot Q(y)\lor R(x,y)}$

${\displaystyle C_{2}=Q(a)}$

${\displaystyle C_{3}=P(b)}$

La substitution ${\displaystyle y\to a}$ permet d'appliquer la résolution sur Q, entre ${\displaystyle C_{1}}$ et ${\displaystyle C_{2}}$, ce qui produit

${\displaystyle C_{R}=\lnot P(x)\lor R(x,a)}$

La substitution ${\displaystyle x\to b}$ permet d'appliquer la résolution sur P, entre ${\displaystyle C_{3}}$ et ${\displaystyle C_{R}}$ pour produire

${\displaystyle C_{S}=R(b,a)}$

Résolution et preuves par réfutation

En général on utilise le principe de résolution pour effectuer des preuves par réfutation. Pour prouver que la formule ${\displaystyle f}$ est une conséquence logique des formules ${\displaystyle f_{1},\ldots ,f_{n}}$ on démontre que l'ensemble ${\displaystyle \{f_{1},\ldots ,f_{n},\lnot f\}}$ est inconsistant.

Pratiquement, il faut commencer par mettre toutes les formules sous forme clausale, pour cela on doit les mettre sous forme prénexe (tous les quantificateurs au début) puis les skolémiser.

Pour montrer qu'un ensemble de clauses est inconsistant, il faut réussir à engendrer la clause vide en appliquant la règle de résolution autant de fois que nécessaire.

Exemple

On veut montrer que les trois formules

1. ${\displaystyle \forall x\ ((S(x)\lor T(x))\to P(x))}$,
2. ${\displaystyle \forall x\ (S(x)\lor R(x))}$,
3. ${\displaystyle \lnot R(a)}$

ont pour conséquence la formule ${\displaystyle P(a)}$.

La première formule est équivalente à ${\displaystyle \forall x\ (\lnot S(x)\land \lnot T(x))\lor P(x)}$ qui est équivalente à ${\displaystyle \forall x\ (\lnot S(x)\lor P(x))\land (\lnot T(x)\lor P(x))}$ et produit donc les deux clauses

${\displaystyle C_{1}=\lnot S(x)\lor P(x)}$

${\displaystyle C_{2}=\lnot T(x)\lor P(x)}$

La seconde formule donne immédiatement la clause

${\displaystyle C_{3}=S(x)\lor R(x)}$

et la troisième

${\displaystyle C_{4}=\lnot R(a)}$.

La négation de la conséquence cherchée donne

${\displaystyle C_{5}=\lnot P(a)}$

Par résolution sur ${\displaystyle R}$ de ${\displaystyle C_{3}}$ et ${\displaystyle C_{4}}$ avec ${\displaystyle x\to a}$ on produit

${\displaystyle C_{6}=S(a)}$

Par résolution sur ${\displaystyle S}$ de ${\displaystyle C_{1}}$ et ${\displaystyle C_{6}}$ on produit

${\displaystyle C_{7}=P(a)}$

Enfin ${\displaystyle C_{5}}$ et ${\displaystyle C_{7}}$ donnent la clause vide.

Stratégie d'application de la règle

Le principe de résolution étant complet, si l'ensemble de clauses considéré est inconsistant, on arrive toujours à générer la clause vide. Par contre, le problème de la consistance (satisfaisabilité) n'étant pas décidable en logique des prédicats, il n'existe pas de méthode pour nous dire quelles résolutions effectuer et dans quel ordre pour arriver à la clause vide.

On peut facilement trouver des exemples où l'on « s'enfonce » dans la génération d'une infinité des clauses sans jamais atteindre la clause vide, alors qu'on l'aurait obtenue en faisant les bons choix.

Différentes stratégies ont été développées pour guider le processus. Le système Prolog se base, par exemple, sur l'ordre d'écriture des clauses et l'ordre des littéraux dans les clauses. D'autres systèmes, comme CyC, utilisent une stratégie de coupure (en fonction des ressources consommées) pour éviter de générer des branches infinies.

Preuves de longueurs minimales

Haken a démontré que toute réfutation du principe des tiroirs avec n chaussettes (en anglais, il s'agit du pigeonhole principle) est de longueur au moins 2^{n/10[réf. nécessaire]}.

Liens externes

Exercices pour manipuler la règle de résolution, outil développé à l'ENS Rennes

Références

• (en) Robinson J. A., A Machine-Oriented Logic Based on the Resolution Principle, J. Assoc. Comput. Mach. 12, 23-41, 1965.
• (en) Kowalski, R., Logic for Problem Solving, North Holland, Elsevier, 1979.
• (fr) Benzaken, C., Systèmes formels : introduction à la logique et à la théorie des langages, Masson, Paris, 1991.
• (en) Bundy, A., The Computer Modelling of Mathematical Reasoning, Academic Press, London, 1983.
• (en) Huth, M., Ryan, M. Logic in Computer Science, Cambridge University Press, 2004.

• Portail de la logique