Only affects path-focused search procedures. When this flag

is T, the scope of quantifiers is minimized in primsubs appearing in

the expansion proof after searching is done and before the

propositional proof checker starts. This allows the corresponding

instantiation terms in the ND proof to be in non-prenex form, often

giving more readable proofs.

MIN-QUANT-ETREE takes values of type BOOLEAN.

It belongs to subjects MS93-1 MS92-9 MS91-7 MS90-9 MS90-3 MATING-SEARCH ETREES .

Its default value is T

Its current value is T.

Contains functions for minimizing quantifier scopes in

primsubs appearing in expansion trees. This allows the corresponding

instantiation terms in the ND proof to be in non-prenex form. When

flag MIN-QUANT-ETREE is T, these functions are applied after searching

is done and before propositional proof checker starts.

/home/theorem/tps/lisp/min-quant-etree.lisp is part of module MS90-3.

© 1988-99, Carnegie Mellon University.