🚀 go-pugleaf

In article <24435@alice.att.com> pereira@alice.att.com (Fernando Pereira)
 writes:

   >If you think of Prolog programs as *logic* programs where the logic is
   >(a fragment of) first-order logic, what is wrong it that the answers
   >derived without the occurs-check are in general unsound.

  This is putting it too strongly, since such answers are perfectly
sound relative to the interpretation of a (pure) program as the union
of the clauses and the identities true in a suitable universe of
rational trees. The logic involved is still first order logic, it's
just that we have a somewhat stronger interpretation of programs.
Generally speaking, these distinctions are much simpler if we think in
terms of wedding different constraint theories to Horn clauses, as
originally suggested by Colmerauer.