Prologではどのように変数を用意して解の構造を作っているのか

環境/言語:[環境(Windows7 64bit)、使用言語(Prolog)]
分類:[.NET]

現在途方にくれています、よろしくお願い致します。


リストを逆順にする述語を
　reverse(X,Y) :- reverse(X,[],Y).
　reverse([],Y,Y) :- !.
　reverse([H|T],Aux,Y):- reverse(T,[H|Aux],Y).
と定義したとき、

reverse([a,b], X)で実行した場合はわかるのですが、
reverse(X, [a,b])で実行した場合にどのように解を求めているのかがわかりません。

Prologでは、解の具体的な値がその時点で不明でも必要な変数を用意して解の構造を作り上げるというので、
X = [H1|T1]というように変数を用意して考えていってみたのですが、そうするとどこまでも変数が続いてしまい、終わりません。

しかし、実際に実行してみると答えが出てくるので成立はするはず…と困っています。

reverse(X, [a,b])
= reverse(X, Y)
→reverse(X, [], [a,b])

X = [H1|T1], [] = Anx1として、
= reverse([H1|T1], Aux1, [a,b])
→reverse(T1, [H1|Aux1], [a,b])

T1=[H2|T2], [H1|Aux1]=Aux2として
= reverse([H2|T2], Aux2, [a,b])
→reverse(T2, [H2|Aux2], [a,b])
　　・
　　・
　　・

上記のようになってしまうと思うのですが、どうなっているのでしょうか？

もうずっと悩み続けていて途方にくれています。
どうかご教授お願い致します！

■No32509に返信(一ノ瀬さんの記事)

予想：
(a) 　reverse(X,Y) :- reverse(X,[],Y).
(b) 　reverse([],Y,Y) :- !.
(c) 　reverse([H|T],Aux,Y):- reverse(T,[H|Aux],Y).
として
(b)がゴールなので
reverse([], [a,b], [a,b]) :- !.
を適用

(c)に当てはめ
reverse([a], [b], [a,b]):- reverse([], [a,b], [a,b])

(c)に当てはめ
reverse([b,a], [], [a,b]) :- reverse([a], [b], [a,b])

(a)に当てはめ
reverse([b,a], [a,b]) :- reverse([b,a], [], [a,b])

よって
X=[b,a]
となる。