Algorithme de résolution de buts

On peut donner une première ébauche de l'algorithme de résolution de buts:

procedure Resoudre (in : but, environnement, niveau) is
begin
    if vide(but) then
        afficher(environnement)
    else
        Sommet   = sommet de la pile but
        Predicat = identificateur de son predicat
        Paquet   = paquet correspondant a Predicat

        for each clause Ci dont le nom est Predicat do
            if Sommet s'unifie a Ci dans environnement then
                Resultat  = environnement resultant de l'unification de
                            Sommet et Ci dans environnemesnt
                but = empiler(queue de Ci, but ecrete de Sommet)
                Resoudre(but, resultat, niveau+1)
            end if
        end do
    end if
end

La recherche du bon paquet consiste simplement à parcourir le programme jusqu'à trouver le bon paquet. Si jamais ce paquet n'existe pas, alors la résolution se termine et le but n'est pas résolvable. Ensuite, on parcourt chaque règle de ce paquet et on tente de l'unifier avec le but à résoudre. Si l'unification est possible, il faut alors supprimer le but de la pile de buts et le remplacer par la partie droite de la règle en question. On peut ainsi rajouter plusieurs buts en une seule fois. Il faut donc faire attention pour le niveau des variables au prochain appel récursif : tant qu'on essaye de résoudre un but de la même règle, il ne faut pas incrémenter le niveau des variables, même si on appelle Resoudre récursivement. Par contre, dès que l'on change de règle, le niveau est incrémenté.
Il est à noter que, ici aussi, on a le même problème que pour l'unification, à savoir qu'il faut construire une instance d'arbre à partir d'un arbre. Le problème est donc de savoir quel niveau lui donner. Or, comme on passe à un niveau supérieur dans la récursivité, le niveau est tout simplement le niveau du but^2.2 incrémenté de 1. Il ne faut pas oublier après chaque appel récursif de désallouer les buts et les environnements supplémentaires que l'on a rajoutés au fur et à mesure.