MS88 : CONTEXT

MS88 is a context.
Concerning mating search procedure MS88.

TPS documentation homepage


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

TPS documentation homepage


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

TPS documentation homepage


MS88 : REVIEW-SUBJECT

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

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage