🚀 go-pugleaf

In his reply to: cwp@otter.hple.hp.com (Chris Preist),
   <7000001@osiris.cso.uiuc.edu> goldfain@osiris.cso.uiuc.edu writes:
>
>Clocksin and Mellish chapter 10 discusses this and related notions.
>
>Basically, all variables in a Prolog  clause are understood  to be universally
>quantified.   It is  existential  quantification that  is somewhat  harder  to
>express.


You seem to have some confusion concerning universal and existential
quantification. What the previous message was referring to was universal
quantification in the body of a clause. What Clocksin & Mellish were talking
about was universal quantification at the beginning of a clause. When you
move a universal quantifier from the body of a clause to the outside of
that clause, it becomes an existential quantifier. The following example
provides a distinction between the two cases:

	p(X) :- forall(Y) q(X,Y)       can be rewritten as:

	forall(X) (p(X) <- forall(Y) q(X,Y))
	forall(X) (p(X) v ~ forall(Y) q(X,Y))
	forall(X) (p(X) v exists(Y) ~q(X,Y))
	forall(X) exists(Y) (p(X) v ~q(X,Y))
	forall(X) exists(Y) (p(X) <- q(X,Y))

or in PROLOG (assuming it is allowed):

	exists(Y) p(X) :- q(X,Y). 

In fact, the above is not an acceptable logic program clause.
As the following example (supplied by VS Subrahmanian) shows:

	b <- forall(X) q(X)
	q(a) <-
	q(s(X)) <- q(X)

The least fixed point of this program is attained after omega+1 iterations
of the Tp operator, instead of omega steps which is the case for pure logic
programs.