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.

© 1988-99, Carnegie Mellon University.