Subject: [SWIPL] Skolemization

From: [email-masked]
Date: Mon, 5 Feb 2001 23:17:06 +0100

Hi,

After skolemization I get this formula:

p(x) & ~q(f(x),x) -> r(x)

is it equivalent to this Prolog clause:

r(X) :- p(X), \+ q(Y,X). ?

If yes, what happen to Skolem Function?
If they are not equivalent, the latter implies the former?
Are they equivalent under Closed World Assumption?

Thank for you help
Regards
--
Stefano De Giorgi