MIN-QUANT-SCOPE : WFFOP

MIN-QUANT-SCOPE is a wff operation.
Minimize the scope of quantifiers in a gwff. Deletes vacuous
quantifiers. During proof transformation, the gap between a formula
and its min-quant-scope version is filled by RULEQ.
 
The calling scheme for MIN-QUANT-SCOPE is:

(MIN-QUANT-SCOPE GWFF)
"GWFF"


The result is of type GVAR.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage