MS90-3 : CONTEXT

MS90-3 is a context.
Concerning mating search procedure MS90-3.

TPS documentation homepage


MS90-3 : MATEOP

MS90-3 is a mating-search command.
Start mating search procedure MS90-3 on current eproof.
This search procedure incorporates Issar's path-focused duplication,
but works on just one jform at a time. Only duplications are done,
not primitive substitutions. This is not an interactive procedure.
 
The command format for MS90-3 is:

<Mate>MS90-3

TPS documentation homepage


MS90-3 : MODULE

MS90-3 is a module.

It is loaded.
The mating search module MS90-3. This search procedure
incorporates Issar's path-focused duplication, working on a single jform.
Note that the search will proceed in an automatic mode, and none of the
interactive facilities described either in this top-level or
elsewhere in TPS will work.

NEEDED-MODULES EXPANSION-TREE EVENTS SKOLEMIZING

MACRO-FILES MS90-3-NODE MS90-3-DATA

FILES MS90-3-UNIF-SIMPL MS90-3-PATH-ENUM MS90-3-PATH-BKUP MS90-3-UNIF-MATCH MS90-3-UNIF-TREE MS90-3-UNIF-FO MS90-3-TOP MS90-3-EXPAND-ETREE MS90-3-EXP-JFORM MIN-QUANT-ETREE MS90-3-PROP MS92-9-TOP MS93-1

TPS documentation homepage


MS90-3 : REVIEW-SUBJECT

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

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage