Arbres de résolution

[Alba.1337]

Bonjour à tous,

je me permets de poster car j'aurais besoin d'explications purement théoriques sur les arbres de résolution en Prolog.
Je comprends bien l'exemple donné ici : http://www.lifl.fr/~routier/enseigne...resolution.pdf
... Mais c'est un cas assez simple. Il suffit de chercher à unifier avec des déclarations faites dans le fichier de la forme s(a). s(b). etc...

Mais par exemple, j'ai du établir un prédicat permettant de dire si l'élément en premier paramètre, fait partie de la liste passée en 2e paramètre.
J'ai donc fait ceci :
member(X,[X|_]).
member(X,[Y|L]) :- member(X,L).

Qui me donnait par exemple :
member(a,[a,b]).
True;
False.

J'ai tâtonné, et suis parvenu à corriger le problème comme ceci :
member(X,[Y|L]) :- member(X,L).
member(X,[X|_]).

Seulement, j'ai d'autre prédicats plus complexe qui me donne le même problème... J'aurais besoin qu'on me montre comment construire l'arbre de résolution pour member, que je puisse reproduire la technique pour mes autres prédicats, et non plus modifier mon code en priant pour que ça marche...

Toute aide est la bienvenue (soyez cools c'est mon anniversaire! ).
Merci en tout cas.

[Alba.1337]

Personne a une petite idée?...