SK1 : EDOP

SK1 is an editor command.
Skolemize a wff using method S1. See page 127 of Andrews' book.
If equivalences are present, you must eliminate them first by REW-EQUIV.
 
The command format for SK1 is:

<Ed>SK1 <<GWFF>> UNIVFLAG
<<GWFF0>> "BOOLEAN"


The result replaces the current wff.

TPS documentation homepage


SK1 : INFO

SK1 is a flag setting or other piece of information.
A setting for the flag SKOLEM-DEFAULT.
SK1 is 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 x such that FORALL x occurs in the wff
and EXISTS y . M is in its scope.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage