MS92-9 : CONTEXT

MS92-9 is a context.
Concerning mating search procedure MS92-9.

TPS documentation homepage


MS92-9 : MATEOP

MS92-9 is a mating-search command.
Call mating search procedure MS92-9 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 procedure is almost identical to MS88, except that the flag
NUM-OF-DUPS is used to govern how many times the outermost quantifier
may be duplicated. The internal representation of variables is as in
MS90-3.
 
The command format for MS92-9 is:

<Mate>MS92-9

TPS documentation homepage


MS92-9 : REVIEW-SUBJECT

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

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage