🚀 go-pugleaf

In article <TORKEL.92Dec17201903@bast.sics.se> torkel@sics.se (Torkel Franzen) writes:
>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.
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. If I use resolution to
show that P |- exists x. Q (by deriving the empty clause from
P /\ forall x. not Q) I have shown P |= exists x. Q, that is, for *any*
model M such that M |= P there is an assignment a for x such that
P, a |= Q. In particular (going back to my example) if I conclude
by resolution that P |- exists x. r(x,x) then in every model of P
there is an element that stands in the r relation with itself. With
P = forall u. r(u, f(u)), from which exists x. r(x,x) follows by resolution
without the occurs check, the model in which r is the successor relation
on |N and f the successor function refutes exists x. r(x, x). Thus
resolution without the occurs check is unsound as a method for deriving
valid consequences in (uninterpreted) first-order logic. It could
still be sound as a method for deriving true conseuqnces over some class of
models, eg. rational trees. But that is a *very* different thing. When
using logic for knowledge representation, we often do not know what
models to consider, but rather we are interested in characterizing
logically the class on models of interest. Thus we need to work with
valid consequence, not just true consequence in particular models.
On the other hand, if we are interested in using logic to define
relations over particular structures, eg. rational trees, resolution
modulo a particular equational theory can be the right way to go.
Still, it is important not to confuse those two alternatives.

Fernando Pereira
2D-447, AT&T Bell Laboratories
600 Mountain Ave, PO Box 636
Murray Hill, NJ 07974-0636
pereira@research.att.com