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:


The result replaces the current wff.

TPS documentation homepage


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