🚀 go-pugleaf

In article <1600016@otter.hple.hp.com> cwp@otter.hple.hp.com writes:
>
>Could any of you give me information on the representation of universal
>quantification in the various dialects of PROLOG available please? We
>have a problem which contains universal quantifications within the body
>of a clause, and wish to represent these in as pure and logical a fashion 
>as possible.
>
>Thanks for any help forthcoming.
>
>Chris

In article <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.
	
I don't think this is quite what the original request was about. You are
correct in saying that all variables in a Prolog clause are understood to
be universally quantified *at the front of the clause*. For example, given
the Prolog clause

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

we may interpret this as a formula of first-order logic as 

		all x all y p(x) if q(x,y)

which is equivalent to

		all x p(x) if exists y q(x,y)

This is well-known and appears in Lloyd's book. As I understood the
original posting, the question referred to clauses like

		all x p(x) if all y q(x,y)

which is different from the above clauses. I'm no expert, but two Prolog
systems which address this sort of issue are Nu-Prolog (guru: Lee Naish,
lee@mulga.oz) and Lambda Prolog (guru: Dale Miller, dale@linc.cis.upenn.edu).

	Chris <cwp@otter.hple.hp.com>: I tried to email you, but it
bounced, and when this article came along I decided to post. I hope this is
of some help.

			Cheers,
				James Harland
				jah@lfcs.ed.ac.uk