Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!know!zaphod.mps.ohio-state.edu!rpi!uupsi!sunic!sics.se!sics.se!torkel
From: torkel@sics.se (Torkel Franzen)
Newsgroups: comp.lang.prolog
Subject: Re: Find the bug
Message-ID: <1990Jul19.155720.5632@sics.se>
Date: 19 Jul 90 15:57:20 GMT
References: <2635@randvax.UUCP>
Sender: news@sics.se
Organization: Swedish Institute of Computer Science, Kista
Lines: 9
In-Reply-To: narain@randvax.UUCP's message of 18 Jul 90 20:54:46 GMT

In article <2635@randvax.UUCP> narain@randvax.UUCP (Sanjai Narain) writes:

   >We now show that S->~exists(u).p(u) is valid.  We add exists(u).p(u) to S.
   >Skolemizing, we obtain:

   >S, ->p(c) where c is a new 0-ary constant.

  c isn't new in the required sense if it occurs in S, which you
presuppose in resolving with c=a->.