MS88 : MATEOP
MS88 is a mating-search command.
Call mating search procedure on the current eproof. This
procedure uses a naive level-saturation method, exhaustively searching
a single jform before applying any duplications. Quantifier duplications
are applied uniformly to outermost quantifiers. Will try primitive
substitution for outermost variable only. Works on only a single
jform at a time.
The command format for MS88 is:
<Mate>MS88
MS88 : MODULE
MS88 is a module.
It is loaded.
The MS88 mating search module.
NEEDED-MODULES EXPANSION-TREE EVENTS UNIFICATION SKOLEMIZING SAVE-TPS-WORK PRIMITIVE-SUBST OTLRULEP TACTICS
FILES MATING-AUX CONNECTIONS MATING MATING-PATHS UNIF-MAT MATING-DIR MATING-EVENTS MATING-PROP UNIF-FO MATING-SUB
MS88 : REVIEW-SUBJECT
MS88 is a subject.
Flags relevant to the MS88 mating-search procedure.