Exos unification

Les lettres a et b sont des symboles de constante, f,g,h,k,p et q sont des symboles de fonction et X,Y,Z,U,V,W et T sont des variables.
Appliquez l’algorithme d’unification aux problèmes suivants et vérifiez vos résultats avec SWI-Prolog (voir ci-dessous).
  1. p(a,X,f(g(Y))) = p(Z,f(Z),f(U))
  2. q(f(a),g(X)) = q(Y,Y)
  3. p(X,f(X),f(f(X))) = p(f(f(Y)),Y,f(Y))
  4. p(X,f(Y,Z)) = p(X,g(h(k(X))))
  5. p(X,f(U,X)) = p(f(Y,a),f(Z,f(b,Z)))
  6. p(X,f(X),g(f(X),X)) = p(Z,f(f(a)),g(f(g(a,Z)),V))
  7. p(f(g(X,Y)),g(V,W),Y) = p(f(Z),X,f(X))
  8. p(f(Y),f(Z),f(T),f(X)) = p(g(Z),g(X),g(Y),g(Z))

Avec SWI-Prolog

Par défaut

SWI-Prolog utilise l'unification rationnelle. 
$ swipl
...
?- s(X)=X.
X = s(X).

?- set_prolog_flag(occurs_check, true).
true.

?- s(X)=X.
false.

?- set_prolog_flag(occurs_check, error).
true.

?- s(X)=X.
ERROR: =/2: Cannot unify _G326 with s(_G326): would create an infinite tree
?- set_prolog_flag(occurs_check, false).
true.

?- s(X)=X.
X = s(X).

?-

CHR

Voici le fichier correspondant au cours.