SWI-Prolog, comme beaucoup d'autres compilateurs Prolog, est basé sur une unification rapide dépourvue du test d'occurrence. Le temps d'exécution est alors bien meilleur et il est possible d'utiliser des termes cycliques. Mais parfois on a besoin d'éviter les termes cycles. Une solution simple consiste à redéfinir l'unification. Le prédicat '*='/2 effectue une unification propre avec le contrôle d'occurrence de ces deux arguments. On définit de même une semi-unification ('=>'/2) et une semi-unification avec test d'occurrence ('*=>'/2). La semi-unification X=>Y signifie que l'on va essayer d'instancier X de manière à ce qu'il s'unifie avec Y, sans modifier Y.
Exemple :
?-X=f(X). ...boucle infinie... ?-X*=f(X). No ?-f(X,y)=>f(X,Y). No ?-f(X,Y)=>f(Z,y). X=Z Y=Z Yes