Résolution

La version imprimable n’est plus prise en charge et peut comporter des erreurs de génération. Veuillez mettre à jour les signets de votre navigateur et utiliser à la place la fonction d’impression par défaut de celui-ci.

Définition

Technique de raisonnement automatique qui généralise le modus ponens (implication logique). Cette technique est utilisée dans les systèmes de preuve de théorèmes, elle est à la base du langage de programmation logique Prolog.

Compléments

L'implication logique est transformée en notation normale conjonctive ce qui facilite le raisonnement automatique par un algorithme proposé par J.A. Robinson en 1965.

Français

résolution

Anglais

resolution

Sources

Source : Utexas Ai vocabulary

Source : Wikipedia

[Source : Robinson J. A., A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, 12, 23-41, 1965.]