« Résolution » : différence entre les versions
(Page créée avec « == en construction == Catégorie:Vocabulary Catégorie:Intelligence artificielle Catégorie:UTexas == Définition == xxxxxxx == Français == xx... ») Balise : Éditeur de wikicode 2017 |
Aucun résumé des modifications |
||
| Ligne 7 : | Ligne 7 : | ||
== 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. | |||
== Compléments == | |||
L'implication logique est transformée en notation normale conjonctive ce qui facilite le raisonnement automatique par un algorithme. | |||
== Français == | == Français == | ||
'''résolution''' | |||
== Anglais == | == Anglais == | ||
'''resolution ''' | '''resolution ''' | ||
a sound and complete method for obtaining proofs by contradiction. The axioms and the negation of the desired conclusion are converted to a set of clauses in conjunctive normal form. Pairs of clauses from the set are resolved, and the resolvents are added to the set. If the empty clause is produced, the theorem is proved. | <!-- a sound and complete method for obtaining proofs by contradiction. The axioms and the negation of the desired conclusion are converted to a set of clauses in conjunctive normal form. Pairs of clauses from the set are resolved, and the resolvents are added to the set. If the empty clause is produced, the theorem is proved. --> | ||
<small> | <small> | ||
[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] | |||
Version du 6 décembre 2022 à 14:39
en construction
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.
Français
résolution
Anglais
resolution
Contributeurs: Patrick Drouin, wiki
