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:


The result replaces the current wff.

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage