`X` `^`

`P` is recognized as meaning “there exists an
`X` such that `P` is true”, and is treated as equivalent to
simply calling `P`. The use of the explicit existential
quantifier outside `setof/3`

and `bagof/3`

is superfluous.

Variables occurring in `Generator` will not be treated as free if they are
explicitly bound within `Generator` by an existential quantifier.
An existential quantification is written:

Y^Q

meaning “there exists a `Y` such that `Q` is true”, where `Y`
is some Prolog variable.
For example:

| ?-setof(X, Y^likes(X,Y), S).

would produce the single result

X = _400, Y = _415, S = [bill,dick,harry,jan,tom];no

in contrast to the earlier example.

Furthermore, it is possible to existentially quantify a term, where all the variables in that term are taken to be existentially quantified in the goal. e.g.

A=term(X,Y), setof(Z, A^foo(X,Y,Z), L).

will treat `X` and `Y` as if they are existentially quantified.

Send feedback on this subject.