SLD-résolution

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.

Français

SDL-résolution

Choisissez parmi ces termes proposés :

• SDL-résolution
• résolution SLD

Discussion Pour le moment, le terme privilégié est «SDL-résolution».

Anglais

SLD resolution

Source:Wikipedia