SK3 : EDOP

SK3 is an editor command.
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.

TPS documentation homepage


SK3 : INFO

SK3 is a flag setting or other piece of information.
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.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage