MIN-QUANT-ETREE : FLAG

MIN-QUANT-ETREE is a flag or parameter.
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.

TPS documentation homepage


MIN-QUANT-ETREE : TPS-FILE

MIN-QUANT-ETREE is a file.
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.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage