SIMPLIFY-DOWN* : WFFOP

SIMPLIFY-DOWN* is a wff operation.
Apply all active rewrite rules
A --> B or A <--> B to the current gwff in the forward direction.
(i.e. subformulas A are rewritten to B, modulo any functions
attached to the rules, so that the resulting formula will be a
rewrite instance of the original formula.)
 
The calling scheme for SIMPLIFY-DOWN* is:

(SIMPLIFY-DOWN* GWFF)
"GWFF"


The result is of type GWFF.

The arguments have the following meaning:
GWFF : gwff before rewriting

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage