teacher(tom).
teacher(X) :- wise(X), old(X).
teacher(X) :- likes(Y,X), !, minister(Y).

wise(X) :- hasBeard(X).

old(tom).
old(alice).

hasBeard(tom).
hasBeard(john).
hasBeard(bill).

minister(x).
likes(alice,bob).
likes(x,bob).




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%not(Goal) :- Goal,!,fail.
%not(_).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% an interesting application which can be solved using Prolog is Constraint Satisfaction

% Assume we have a variable X, a set of possible values for X (i.e. a domain D, expressed in Prolog as a list), and a constraint C over X. Let us write a predicate:
% csp1(X,D,E,C) such that, for X, D, and C given, D would be bound to a list of values for which C is satisfied.
% example: csp1(X,[9,2,3,4,5,6],E,X>1).

csp1(_,[],[],_).

csp1(X,[DH|DT],E,C) :- X is DH, C, !, csp1(X,DT,E1,C), E = [DH|E1].
csp1(X,[DH|DT],E,C) :- X is DH, not(C), !, csp1(X,DT,E,C).

%let us test this implementation using trace
%it is straightforward that our problem is that X is bound to the first value from DH, and remains bound to it. How can we solve the problem ?

%the negation, discussed previously, offers a hint:
csp2(_,[],[],_).
csp2(X,[DH|DT],E,C) :- not((X is DH, C)), csp2(X,DT,E,C).
csp2(X,[DH|DT],E,C) :- csp2(X,DT,E1,C), E = [DH|E1].

%everything appears to be ok, yet still there is another problem. When D = [1,2,3,4,5,6], the goal not((X is 1, C)) is satisfied. However, Prolog tries to resatisfy it, using the second clause (which does not explicitly mention that not((X is 1, C)) is not satisfied.

%a possible alternative to this issue is:
csp3(_,[],[],_).
csp3(X,[DH|DT],E,C) :- not((X is DH, C)), csp3(X,DT,E,C).
csp3(X,[DH|DT],E,C) :- not(not((X is DH, C))), csp3(X,DT,E1,C), E = [DH|E1].

%however this approach is cumbersome. A more elegant implementation is:

csp4(_,[],[],_).
csp4(X,[DH|DT],E,C) :- csp4(X,DT,E1,C), (not((X is DH, C)), E=E1, !; E = [DH|E1]).

%which can be read: try to satisfy (recursively) csp4(X,DT,E1,C). After doing so, if the condition C is not satisfied for DH, unify E with E1 and stop any attempt to resatisfy the goal. Otherwise (C is satisfied for X is DH), unify E with [DH|E1].