MIN-SCOPE : EDOPMIN-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