SLD-résolution


Révision datée du 28 janvier 2024 à 12:10 par Pitpitt (discussion | contributions) (Remplacement de texte : « ↵<small> » par «  ==Sources== »)
(diff) ← Version précédente | Voir la version actuelle (diff) | Version suivante → (diff)

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