Question

Define a predicate unifiable(List1,Term,List2) where List2 is the list of all members of List1 that unify with Term. The elements of List2 should not be instantiated by the unification. For example,

unifiable([X,b,t(Y)],t(a),List).
List= [X,t(Y)].

Note that X and Y are still not instantiated. So the tricky part is: how do we check that they unify with t(a) without instantiating them? Write the predicate so that it terminates immediately after finding the correct answer. (That is, after prolog produces its first solution, it terminates executing the query immediately.)

Hint: consider using possibilities associated with using tests of the form: \+ term1 = term2.

Answer 1

Solution

 if \+ H = Term succeeds we know that the H and Term cannot be unified so we fail and go to the default to second myUnifiable and add H to List2.
 if it fails we use a cut (i.e. it can be unified) we make a cut so that we don't end up trying the second myUnifiable which would add it regardless to  List2 even though it can't be unified Alternative we could've used a double \+ \+ so we add H in the case where the check succeeds to avoid confusion about the default case being the one that adds H to List2.

myUnifiable([H | List1],Term,List2) :-
  \+ H = Term, !,
  myUnifiable(List1, Term, List2).

myUnifiable([H | List1], Term, [H | List2]) :-
  myUnifiable(List1, Term, List2).

myUnifiable([],Term,[]).