Développement d'un algorithme de résolution en prolog

Bonjour,



Je suis débutant en prolog et je ne connu pas vraiment comment faire l algorithme de résolution(Le principe de résolution est une méthode automatique pour montrer la validité d'une formule) suivant en prolog

début
écrire la négation de F
tq la liste vide est n'est pas rencontrée et qu'il existe de paires réductible faire
début
chercher des clauses resolvante;
ajouter ce resultat à la liste des clause ;
fin tq.
si on trouve la liste vide alors F est valide
sinon F invalide.
fin si
FIN.
aide moi SVP,
et merci d'avance