🚀 go-pugleaf

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

   >No, it is not too strong. I think you are confusing deduction in
   >an interpreted system (eg. Horn clauses over the domain of finite trees,
   >or of rational trees) with deduction that yields consequences true
   >in any model, that is, valid consequences.

  There is no confusion involved. It is merely a matter of "valid
consequences of what". The answers yielded by a Prolog system using
unification without occurs check are consequences in first order logic
of the clauses of the program together with the first order identity
theory of rational trees.