Skolems and prolog

[Douglas R. Miles/LogicMoo]

Has anyone used attributed variables to implement existential or skolems (perhaps created for unit propagation ) ?

I am looking for papers and implementations to reference.

Thanks in advance!
Douglas Miles

[Jan Burse]

Check out (for example):

Projection in Constraint Logic Programming,
Andreas Fordan, DISKI 199
http://www.iospress.nl/book/projection-in-constraint-logic-programming/

He makes even a case where with projection a CLP(*)
problem runs much faster. But I guesss sometimes
projection can be also costly.

projection = existential quantifier

You can visually imagine the existential quantifier
effectively as a projection. For example if you have
a two dimensional relation R(x,y).

Then exists x R(x,y) is a one-dimensional relation
R'(y) :<==> exists x R(x,y). For example if R(x,y)
is a circle, then the projection is the diameter:

http://math.stackexchange.com/questions/200118/existential-quantification-as-projection

https://bakingandmath.files.wordpress.com/2016/02/thirdplace.png?w=490

(from
https://bakingandmath.com/2016/02/02/playtime-with-the-hyperbolic-plane/ )

Bye

P.S.: I don't like skolems approach for quantifiers for
many reasons. In my opinion, it doesn't work well together
with a fixed Herbrand Domain, as in Prolog.

It works well if you have equational reasoning, i.e.
logic with equality, but (=)/2 is fixed in Prolog belonging
to CLP(H), so basically it doesn't work very well.

It doesn't work very well in Prolog since the resulting
clauses after skolemization might talk about (=)/2 and
change its meaning.

Douglas R. Miles/LogicMoo schrieb: