« SLD-résolution » : différence entre les versions
| Ligne 5 : | Ligne 5 : | ||
== Définition == | == Définition == | ||
En programmation logique, la SLD-résolution (SLD signifiant Sélectionné, Linéaire, Défini) est un algorithme servant à prouver une formule de logique du premier ordre à partir d'un ensemble de clauses de Horn. Elle est basée sur une résolution linéaire, avec une fonction de sélection sur les clauses définies. La SLD-résolution est mieux connue par son extension, SLDNF (NF signifiant negation as failure, la négation par l'échec), qui est l'algorithme de résolution employé par le langage Prolog. | |||
Source: | |||
https://fr.wikipedia.org/wiki/SLD-r%C3%A9solution | |||
== Français == | == Français == | ||
Version du 20 février 2019 à 03:21
Domaine
Définition
En programmation logique, la SLD-résolution (SLD signifiant Sélectionné, Linéaire, Défini) est un algorithme servant à prouver une formule de logique du premier ordre à partir d'un ensemble de clauses de Horn. Elle est basée sur une résolution linéaire, avec une fonction de sélection sur les clauses définies. La SLD-résolution est mieux connue par son extension, SLDNF (NF signifiant negation as failure, la négation par l'échec), qui est l'algorithme de résolution employé par le langage Prolog.
Source:
https://fr.wikipedia.org/wiki/SLD-r%C3%A9solution
Français
résolution SDL
Anglais
SLD resolution
SLD resolution (Selective Linear Definite clause resolution) is the basic inference rule used in logic programming. It is a refinement of resolution, which is both sound and refutation complete for Horn clauses.
Contributeurs: Claude Coulombe, Imane Meziani, wiki
