« Résolution » : différence entre les versions
Aucun résumé des modifications |
m (Remplacement de texte : « ↵<small> » par « ==Sources== ») |
||
| (3 versions intermédiaires par 2 utilisateurs non affichées) | |||
| Ligne 1 : | Ligne 1 : | ||
== Définition == | == 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. | 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 == | == Compléments == | ||
L'implication logique est transformée en notation normale conjonctive ce qui facilite le raisonnement automatique par un algorithme. | 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 == | == Français == | ||
| Ligne 18 : | Ligne 14 : | ||
==Sources== | |||
[https://www.cs.utexas.edu/users/novak/aivocab.html Source : Utexas Ai vocabulary] | [https://www.cs.utexas.edu/users/novak/aivocab.html Source : Utexas Ai vocabulary] | ||
[https://fr.wikipedia.org/wiki/R%C3%A8gle_de_r%C3%A9solution Source : Wikipedia] | [https://fr.wikipedia.org/wiki/R%C3%A8gle_de_r%C3%A9solution Source : Wikipedia] | ||
[Source : Robinson J. A., A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, 12, 23-41, 1965.] | |||
[[Catégorie:GRAND LEXIQUE FRANÇAIS]] | |||
Dernière version du 28 janvier 2024 à 12:24
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 : Robinson J. A., A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, 12, 23-41, 1965.]
Contributeurs: Patrick Drouin, wiki
