CLAUSE-FORM : EDOP

CLAUSE-FORM is an editor command.
Converts the given wff to clause form, as if the resulting wff is to
be given to a resolution theorem prover. The gwff is skolemized,
rectified, etc.
 
The command format for CLAUSE-FORM is:

<Ed>CLAUSE-FORM <<GWFF>>
<<GWFF>>


The result replaces the current wff.

TPS documentation homepage


CLAUSE-FORM : WFFOP

CLAUSE-FORM is a wff operation.
Converts the given wff to clause form, as if the resulting wff is to
be given to a resolution theorem prover. The gwff is skolemized,
rectified, etc.
 
The calling scheme for CLAUSE-FORM is:

(CLAUSE-FORM <<GWFF>>)
<<GWFF>>


The result is of type GWFF.

The arguments have the following meaning:
GWFF : gwff

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage