MIN-PRIM-DEPTH : FLAG

MIN-PRIM-DEPTH is a flag or parameter.
Minimum depth at which primsubs with quantifiers are generated.
The types of the quantified variables range over the values in PRIM-BDTYPES.
With PRIMSUB-METHOD PR89 :
This flag is ignored. Primsubs of the form "exists x . literal" and
"forall x . literal" will be generated.
With PRIMSUB-METHOD PR93 :
At depth 1, a single quantifier is introduced, as in PR89.
At depth N>1, we have (N-1) quantifiers ranging over a formula
containing (N-1) conjunctions {disjunctions} of (N-2)
disjunctions {conjunctions}.
With PRIMSUB-METHOD PR95 :
At depth 1, as in PR89.
At depth N>1, we have (N-1) quantifiers ranging over a formula
with between MIN-PRIM-LITS and MAX-PRIM-LITS literals, with
all combinations of connectives between them.
With PRIMSUB-METHOD PR97 :
At depth N>0, we have (N-1) quantifiers ranging over each
subformula taken from the etree which contains between
MIN-PRIM-LITS and MAX-PRIM-LITS literals. You can see these
subformulas by doing NAME-PRIM from the MATE top level.
With PRIMSUB-METHOD PR97A :
As in PR97, but all substitutions are in negation normal form.
With PRIMSUB-METHOD PR97B :
The substitutions from PR97A and PR95 are interleaved. The order
is determined firstly by the number of literals, then by the number of
quantifiers, and lastly with PR97 substs taking precedence over PR95.
With PRIMSUB-METHOD PR97C :
If set to N, the number of quantifiers in any primsub will be >= N-1.
MIN-PRIM-DEPTH takes values of type POSINTEGER.
It belongs to subjects IMPORTANT MS93-1 MS92-9 MS91-7 MS91-6 MS90-9 MS90-3 MS89 MS88 PRIMSUBS .
Its default value is 1
Its current value is 1.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage