🚀 go-pugleaf

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

   >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.

   This is not so, since the class of rational tree models cannot be
characterized by any set of first order axioms, any more than the finite
tree models.

   >In any case, one needs to be *very* clear about what one
   >is assuming to the left of the |-. 

  In a more perspicuous description of Prolog-style Horn clause programming,
I think it's a good idea to separate the constraint system from the
resolution mechanism. Thus Prolog (in the simplified version here considered),
whatever the constraint system used, delivers answers to a question A(x)
of the form C(x,y), where C(x,y) is a conjunction of constraints, and
it always holds that

    (1)                     C(x,y) -> A(x)

is a logical consequence of the program, read as a set of Horn clauses. Of
course (1) does not imply that there is an x such that A(x); for this to
follow, the constraint theory must be used.