🚀 go-pugleaf

In article <2562@randvax.UUCP> narain@randvax.UUCP (Sanjai Narain) writes:
>
>In a sense, an executable specification is quite easy to obtain.  Suppose
>one can specify a problem in a formal language.  Then, one can use any
>complete theorem prover for it to query that specification.  So, what is
>to distinguish doing this in full first-order logic from doing the same in
>definite clauses (with SLD-resolution)?  It is the possibility of
>specifying algorithmic knowledge in the latter.

I am somewhat surprised that no-one has yet (to my knowledge) produced a
logic program development/teaching environment which includes a decent
complete theorem prover (preferably connected to a declarative
debugging system).  It seems like such an obvious thing to do.

It allows you to to first get the logic right, then concentrate on
the algorithm, using SLDNF resolution.  I think this would be
particularly nice for teaching purposes.  We could first teach students
to write specifications in logic, then explain SLDNF resolution (so they
could write Prolog code which does not loop), then explain Prolog
implementation (so they could write tail recursive code, not leave
choice points around, etc).

The testing facility in the NU-Prolog Debugging Environment goes a
little way in this direction (it has a meta interpreter which uses a
fair search strategy, and is connected to a declarative debugger), but
the technology exists to do much better.

Logic programming has a huge potential for great programming
environments.  Its a great shame that so few people are working on the
area.

	lee