Path: utzoo!utgpu!water!watmath!clyde!att!osu-cis!tut.cis.ohio-state.edu!mailrus!ames!amdcad!sun!pitstop!sundc!seismo!uunet!mcvax!ukc!etive!lfcs!jah
From: jah@lfcs.ed.ac.uk (James Harland)
Newsgroups: comp.lang.prolog
Subject: Re: Universal Quantification in PROLOG
Message-ID: <745@etive.ed.ac.uk>
Date: 30 Aug 88 11:31:41 GMT
References: <1600016@otter.hple.hp.com> <7000001@osiris.cso.uiuc.edu>
Sender: news@etive.ed.ac.uk
Reply-To: jah@lfcs.ed.ac.uk (James Harland)
Organization: Lab. for the Foundations of CS, University of Edinburgh
Lines: 52


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