Skolemize a wff using method S3. At the moment it takes only

those free variables which are universally quantified somewhere before,

all other variables are considered to be constants.

See page 127 of Andrews' book.

If equivalences are present, you must eliminate them first by REW-EQUIV.

The command format for SK3 is:

<Ed>SK3 <<GWFF>> UNIVFLAG

<<GWFF0>> "BOOLEAN"

The result replaces the current wff.

A setting for the flag SKOLEM-DEFAULT.

SK3 is a variant of the original method due to Skolem, where wffs

of the form EXISTS y . M are replaced by M(g(...)), and the Skolem

constants g take as arguments all the free variables

of EXISTS y . M.

© 1988-99, Carnegie Mellon University.