Règle de résolution

Règle de résolution

La règle de résolution ou principe de résolution de Robinson est une règle d'inférence logique que l'on peut voir comme une généralisation du 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.

Sommaire

Définition

La règle de résolution s'applique sur deux clauses, c'est-à-dire des formules composées de disjonctions de littéraux, un littéral étant un atome (positif) ou un atome précédé d'une négation (négatif).

Etant donné deux clauses

C_1 = L_1 \lor \ldots \lor L_i \lor \ldots \lor L_m

C_2 = M_1 \lor \ldots \lor M_j \lor \ldots \lor M_n

où les littéraux Li et Mj sont l'un positif et l'autre négatif et qu'ils portent sur le même atome.

Le résolvant de C1 et C2 sur Li et Mj est la clause

C_R = \bigg( L_1 \lor \ldots \lor L_{i-1} \lor L_{i+1}\lor \ldots \lor L_m \ \bigg) \land \ \bigg( M_1 \lor \ldots \lor M_{j-1}\lor M_{j+1} \lor \ldots \lor M_n \bigg)

Exemples

Soit

C_1 = a \lor \lnot b \lor \lnot c

C_2 = b \lor e \lor \lnot f

La résolution sur b produit

C_R = a \lor \lnot c \lor e \lor \lnot f


La règle du modus ponens est un cas particulier de résolution avec

\begin{array}{ll} C_1 = \lnot p \lor q & \mathrm{la\ formule\ } p \to q \mathrm{\ sous\ forme\ de\ clause} \\ C_2 = p \\ C_R = q & \mathrm{r\acute{e}solvant\ sur\ } p \end{array}

Utilisation en logique des prédicats

En logique des prédicats les formules atomiques sont de la forme P(t_1, \ldots, t_n) où P est un symbole de prédicat et les ti sont des termes composés de constantes, de variables et de symboles de fonctions. On peut effectuer la résolution sur deux littéraux s'ils portent sur des formules atomiques identique ou sur des formules unifiables. Deux formules atomiques sont unifiables s'il existe une substitution des variables par des termes qui rend les deux formules identiques.

Par exemple, les formules atomiques

P(x,a,y) et P(c,a,z), où a et c sont des constantes,

sont unifiables par la substitution x \to c, y \to z. Par contre

P(x,a,y) et P(c,b,z)

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

Exemple

C_1 = \lnot P(x) \lor \lnot Q(y) \lor R(x, y)

C2 = Q(a)

C3 = P(b)

La substitution y \to a permet d'appliquer la résolution sur Q, entre C1 et C2, ce qui produit

C_R = \lnot P(x) \lor R(x, a)

La substitution x \to b permet d'appliquer la résolution sur P, entre C3 et CR pour produire

CS = 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 f est une conséquence logique des formules f_1, \ldots, f_n on démontre que l'ensemble \{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 prenex (tous les quantificateurs au début) puis les skolemiser.

Pour montrer qu'un ensemble de clause est inconsistant il faut réussir à générer 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. \forall x \ ((S(x) \lor T(x)) \to P(x)),
  2. \forall x \ (S(x) \lor R(x)),
  3. \lnot R(a)

ont pour conséquence la formule P(a).

La première formule est équivalente à (\forall x \ (S(x) \to P(x)) \land (\forall x \ (T(x) \to P(x)) et produit donc les deux clauses

C_1 = \lnot S(x) \lor P(x)

C_2 = \lnot T(x) \lor P(x)

La seconde formule donne immédiatement la clause

C_3 = S(x) \lor R(x)

et la troisième

C_4 = \lnot R(a).

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

C_5 = \lnot P(a)

Par résolution sur R de C3 et C4 avec x \to a on produit

C6 = S(a)

Par résolution sur S de C1 et C6 on produit

C7 = P(a)

Enfin C5 et C7 donnent la clause vide.

Stratégie d'application de la règle

Le principe de résolution étant complet, si l'ensemble de clause 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édicat, 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.

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.

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Règle de résolution de Wikipédia en français (auteurs)

Игры ⚽ Нужен реферат?

Regardez d'autres dictionnaires:

  • Résolution — Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom. Sur les autres projets Wikimedia : « Résolution », sur le Wiktionnaire (dictionnaire universel) Le mot résolution peut avoir plusieurs… …   Wikipédia en Français

  • Resolution de conflit — Résolution de conflit Pour les articles homonymes, voir Résolution. La résolution de conflit est un concept associé aux relations humaines, principalement lié au management et aux méthodes et outils d aide à la prise de décision[1]. Elle consiste …   Wikipédia en Français

  • Regle de jeu — Règle de jeu Pour les articles homonymes, voir Règle. Un jeu (et au delà toute activité humaine) est déterminé par trois éléments : la situation de départ le but à atteindre les règles : possibilités et contraintes qui doivent être… …   Wikipédia en Français

  • Règle du jeu — Règle de jeu Pour les articles homonymes, voir Règle. Un jeu (et au delà toute activité humaine) est déterminé par trois éléments : la situation de départ le but à atteindre les règles : possibilités et contraintes qui doivent être… …   Wikipédia en Français

  • règle — [ rɛgl ] n. f. • XIIIe, adapt. du lat.; ruile 1119; reille 1105; lat. regula I ♦ (1317) Planchette allongée ou tige à arêtes rectilignes qui sert à guider le crayon, la plume, quand on trace un trait, à mesurer une longueur, etc. ⇒ réglet,… …   Encyclopédie Universelle

  • réglé — règle [ rɛgl ] n. f. • XIIIe, adapt. du lat.; ruile 1119; reille 1105; lat. regula I ♦ (1317) Planchette allongée ou tige à arêtes rectilignes qui sert à guider le crayon, la plume, quand on trace un trait, à mesurer une longueur, etc. ⇒ réglet,… …   Encyclopédie Universelle

  • Resolution numerique — Résolution numérique Une image numérique est constituée de pixels. Un pixel n’a pas de taille bien définie. Pour représenter la taille d un pixel, il faut connaître la résolution utilisée pour représenter ce pixel. La résolution définit le nombre …   Wikipédia en Français

  • Résolution numérique — Une image numérique est constituée de pixels. Un pixel n’a pas de taille bien définie. Pour représenter la taille d un pixel, il faut connaître la résolution utilisée pour représenter ce pixel. La résolution définit le nombre de pixels par unité… …   Wikipédia en Français

  • Résolution spatiale — Résolution numérique Une image numérique est constituée de pixels. Un pixel n’a pas de taille bien définie. Pour représenter la taille d un pixel, il faut connaître la résolution utilisée pour représenter ce pixel. La résolution définit le nombre …   Wikipédia en Français

  • Regle de Cramer — Règle de Cramer Pour les articles homonymes, voir Cramer. La règle de Cramer (ou méthode de Cramer) est un théorème en algèbre linéaire qui donne la solution d un système d équations linéaires en termes de déterminants. En calcul, elle est… …   Wikipédia en Français

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”