% Occurs Check in Prolog
% Author: Steve Wolfman
% Based on ideas by David Poole.
% Released into the public domain.

% On its own, there's nothing wrong with this.
nest(X, inner(X)).

% On its own, there's nothing wrong with this..
% except that it isn't very interesting. Since we cannot
% establish unnest/1 by anything but this rule, and
% this rule is recursive, there is no unnest(X) that
% is a logical consequence of this KB.
unnest(inner(Z)) :- unnest(Z).

% Now, try the queries:
% ?- nest(Y, Y).
% ?- nest(Y, Y), unnest(Y).

% For the first, does the result make sense?
% For the second, what is Prolog doing?