SLD-résolution
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.
Clauses définies
Une clause définie est une clause de Horn contenant exactement un littéral positif. La notion englobe donc les clauses de Horn strictes et les clauses de Horn positives. Dans le cadre de la SLD-résolution, le littéral positif d'une clause définie est appelée la tête, la conclusion ou le but. La disjonction des littéraux négatifs, s'ils existent, est appelée le corps, les antécédents, ou les sous-buts. Par exemple, la clause de Horn
¬ a ∨ ¬ b ∨ c
est logiquement équivalente à :
(a ∧ b) → c
ou encore à la règle Prolog suivante :
c :- a, b.
Dans chacun des cas, c est la conclusion, a et b sont les antécédents.
Le mécanisme de résolution
Étant donné un programme (un ensemble de clauses de Horn) et une requête (une conjonction de littéraux positifs dont on souhaite prouver qu'elle est vraie d'après le programme), la SLD-résolution fonctionne globalement comme d'autres formes de résolution, en tentant d'unifier des clauses de Horn pour en créer de nouvelles, jusqu'à ce qu'une contradiction soit atteinte, ou qu'aucune nouvelle unification ne puisse être faite.
Plus précisément, la SLD-résolution commence par construire la négation de la requête (on obtient donc une clause de Horn négative, que nous appelerons la liste de buts), puis unifie le premier élément de cette négation avec une clause du programme. La clause en question est recherchée de manière déterministe, en recherchant la première clause du programme dont la tête est la contrepartie positive de la première négation de la liste de buts.
Si une contradiction est trouvée, alors la négation de la requête est inconsistante avec le programme, la requête termine donc avec succès. Si aucune unification ne peut être trouvée pour le premier terme négatif de la liste de buts, alors la requête échoue. Si une unification sans contradiction existe, alors la nouvelle liste de buts devient la conjonction de l'ancienne avec la clause sélectionnée, et la SLD-résolution est relancée (de manière récursive) sur la nouvelle liste de buts. Si une sous-requête échoue, alors l'unification de niveau supérieur dont elle provient échoue, et l'algorithme cherche une autre unification (dans la suite du programme) pour le premier terme de la liste de buts. Cette étape s'appelle le retour sur trace.
Prenons le programme suivant comme exemple :
- q ∨ ¬p
- p
ainsi que la requête :
- {q}
La liste de buts est constituée de l'unique négation {¬q}, et une clause unifiable est recherchée dans le programme. La première clause correspond, elle est sélectionnée. La conjonction de la liste de buts avec la clause donne :
- (q ∨ ¬p ) ∧ ¬q
Soit :
- ¬p
En relançant l'algorithme sur cette nouvelle liste de buts, on trouve une unification avec la seconde clause du programme, menant à une contradiction :
- p ∧ ¬p
La liste de buts {¬q} est donc incompatible avec le programme, par conséquent la requête {q} termine avec succès.
Note : En Prolog, la première clause s'écrirait q :- p . L'algorithme se décrirait alors ainsi : « Pour prouver q, trouver une clause qui ait q comme tête. La première clause correspond, et requiert p pour être montrée. La seconde clause montre p, donc q est prouvé. »
Si la clause suivante devait être ajoutée en tête du programme :
- q ∨ ¬r
alors l'algorithme de SLD-résolution la sélectionnerait en premier, obtenant ¬r par unification, et échouerait ensuite à unifier ¬r. Cela induirait un retour sur trace ; l'algorithme chercherait de nouveau à unifier ¬q avec une clause dans la suite du programme. La clause q ∨ ¬p serait sélectionnée, et l'on retomberait sur le cas précédent.
Notes et références
- (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « SLD Resolution » (voir la liste des auteurs).
