MS91-6 : MATEOP

MS91-6 is a mating-search command.
Begin mating search MS91-6 on the current expansion proof.
Primitive substitutions and duplications are performed systematically,
with multiple jforms being worked on simultaneously. On each
particular jform, the search procedure MS88 is used. The flags
MAX-SEARCH-LIMIT and SEARCH-TIME-LIMIT are used to control the amount
of time spent on each jform.

The order in which the possible jforms are considered depends on a
number of flags. Firstly, the primitive substitutions which are generated
are determined by the values of MAX-PRIM-DEPTH, MIN-PRIM-DEPTH,
PRIM-QUANTIFIER and NEG-PRIM-SUB. If DUP-ALLOWED is T, then additional
options are generated corresponding to duplicated quantifiers. These
options are then combined into sets; because there can be many such sets,
the flag NEW-OPTION-SET-LIMIT controls how many are generated at once.
Each set is given a weighting (see flags WEIGHT-x-COEFFICIENT and
WEIGHT-x-FN, for x = A,B,C), and the lowest-weighted set is chosen
for searching. If the weight of the lowest-weighted set is too large,
TPS may generate more sets; the interpretation of "too large" is given
by MS91-WEIGHT-LIMIT-RANGE. If the search fails, it will be discarded;
if it runs out of time then it will be re-weighted to be continued
later (see RECONSIDER-FN).
 
The command format for MS91-6 is:

<Mate>MS91-6

TPS documentation homepage


MS91-6 : REVIEW-SUBJECT

MS91-6 is a subject.
Flags relevant to the MS91-6 mating-search procedure.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage