MIN-SCOPE : EDOP

MIN-SCOPE is an editor command.
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 command format for MIN-SCOPE is:

<Ed>MIN-SCOPE <<GWFF>>
<<GWFF>>


The result replaces the current wff.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage