🚀 go-pugleaf

In article <2554@randvax.UUCP>, narain@randvax.UUCP (Sanjai Narain) writes:

[stuff deleted]

> An interesting question is this: why is it that algorithmic knowledge
> can be expressed using definite clauses, but not using full first-order
> logic (at least in any obvious way)?

	A subject close to my heart. In brief, I think the answer is that
the restriction to definite formulae is strong enough to ensure the
completeness of a special kind of proof ie those found by SLD-resolution.
The close association between the proof search process and computation (a
la the original Kowalski scheme) doesn't seem to hold for arbitrary proofs
in full first-order logic, for various technical and pseudo-technical
reasons, and hence full first-order logic is not as suitable for
programming purposes as definite clauses.

	In order to extend the class of formulae which can be used as
programs, it is important to preserve the strong proof properties of
definite clauses. Precise definitions of these properties may differ, but
one interesting one studied by Dale Miller et al. is the class of uniform
proofs. An in-depth discussion is probably a bit long for this forum, but
this class of proofs leads naturally to a class of formulae which
generalise definite clauses to a larger subset of first-order logic, known
as hereditary Harrop formulae. Uniform proofs are sound and complete for
this class of formulae, and hence such formulae may be used as logic
programs. It is an informal conjecture that this class of formulae form the
"ultimate" first-order logic programming language -- at least as far as
uniform proofs are concerned. I am currently writing a paper on some ways
to make some formal connection of this kind, ie roughly that there is no
class of formulae which properly includes hereditary Harrop formulae for
which the completeness of uniform proofs can be guaranteed.

		
	Hope this helps. 

					Cheers,
						James Harland.