SLD-résolution


Révision datée du 3 mars 2021 à 11:35 par Imeziani (discussion | contributions) (Imeziani a déplacé la page SLD resolution vers SLD-résolution)

en construction

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.

Français

SDL-résolution

Anglais

SLD resolution

Source:Wikipedia