🚀 go-pugleaf

In article <TORKEL.92Dec18231028@lludd.sics.se> torkel@sics.se (Torkel Franzen) writes:
>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.
I agree. Adding the first-order theory of rational trees to the left of the
|- is precisely restricting the class of models under consideration
from arbitrary first-order models to rational tree models. For some
applications this is fine, but as I pointed out earlier for many others
it is not. In any case, one needs to be *very* clear about what one
is assuming to the left of the |-. 

Fernando Pereira
pereira@research.att.com