PRIMSUB-METHOD : FLAG

PRIMSUB-METHOD is a flag or parameter.
Takes one of the values PR89, PR93, PR95, PR97, PR97A, PR97B.
This determines how primsubs will be generated, in
conjunction with MAX-PRIM-DEPTH, MIN-PRIM-DEPTH,
MAX-PRIM-LITS and MIN-PRIM-LITS.
With PRIMSUB-METHOD PR89 :
Primsubs of the form "exists x . literal" and
"forall x . literal" will be generated.
With PRIMSUB-METHOD PR93 :
For all integers from MIN-PRIM-DEPTH to MAX-PRIM-DEPTH:
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 :
For all integers from MIN-PRIM-DEPTH to MAX-PRIM-DEPTH:
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 :
For all integers from MIN-PRIM-DEPTH to MAX-PRIM-DEPTH:
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. (Note:
both the instantiated and uninstantiated versions of each
definition are used.)
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 :
Using the connectives AND and OR, and the quantifiers EXISTS and
FORALL (ranging over variables of types PRIM-BDTYPES), and also using
any abbreviations or equalities that occur in the gwff to be proven,
primsubs are built up using the bounds given by MIN- and MAX-PRIM-LITS
and MIN- and MAX-PRIM-DEPTH. See also PR97C-PRENEX and PR97C-MAX-ABBREVS.
PRIMSUB-METHOD takes values of type SYMBOL.
It belongs to subjects IMPORTANT MS93-1 MS92-9 MS91-7 MS91-6 MS90-9 MS90-3 MS89 MS88 PRIMSUBS .
Its default value is PR93
Its current value is PR93.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage