MS91-7 : MATEOP

MS91-7 is a mating-search command.
Begin mating search MS91-7 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 MS90-3 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-7 is:

<Mate>MS91-7

TPS documentation homepage


MS91-7 : REVIEW-SUBJECT

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

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage