SLD-résolution

La version imprimable n’est plus prise en charge et peut comporter des erreurs de génération. Veuillez mettre à jour les signets de votre navigateur et utiliser à la place la fonction d’impression par défaut de celui-ci.

Définition

En programmation logique, la SLD-résolution (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

Sources

Source:Wikipedia