SKOLEMS1 : WFFOP

SKOLEMS1 is a wff operation.
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 calling scheme for SKOLEMS1 is:

(SKOLEMS1 GWFF UNIVFLAG)
"GWFF0" "BOOLEAN"


The result is of type GWFF0.

The arguments have the following meaning:
GWFF : Wff to be Skolemized
UNIVFLAG : If NIL, existential quantifiers will be replaced

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage