[continued from previous message]   
      
   expression. A goal is evaluated to a truth value but if that truth   
   value is true the values of variables (if there are any) are also   
   evalueted to values that are not truth values. In the example   
      ?- G = not(provable(F, G)).   
   the answer   
      G = not(provable(F, G)).   
   mans that the Prolog implementation evaluated the query to true and   
   the variable G to the expression not(provable(F, G)). The quoted   
   text says that another Prolog implementation may interprethe the   
   same query differently.   
      
   The quoted text does not stay unify_with_occurs_check/2 would reject   
   anything as "semntically unsound". First of all, it nas no consequences   
   unless it is used. Secondly, if the result of unification would be   
   that at a cycle be created then it simpy evaluates to false just   
   like unify_with_occurs_check(1, 2) evaluates to false.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)