From sdg.ml@infinito.it Mon Feb  5 23:18:05 2001
Received: from sdegiorgi (mi1-581.dialup.tiscalinet.it [62.11.53.69])
	by swi.psy.uva.nl (8.11.2/8.11.2) with ESMTP id f15MI4Z11026
	for <prolog@swi.psy.uva.nl>; Mon, 5 Feb 2001 23:18:04 +0100 (MET)
Received: from [127.0.0.1] by sdegiorgi
  (ArGoSoft Mail Server, Version 1.5 (1.5.0.8)); Mon, 5 Feb 2001 23.18.40 +0100
From: sdg.ml@infinito.it
To: prolog@swi.psy.uva.nl
Date: Mon, 5 Feb 2001 23:17:06 +0100
Lines: 18
Message-ID: <MWMail.cbkhcffd@host.none>
Mime-Version: 1.0
Content-Transfer-Encoding: 7bit
X-Mailer: Kaufman Mail Warrior 3,61 Final
Subject: [SWIPL] Skolemization

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


