MS93-1 : CONTEXT

MS93-1 is a context.
Concerning mating search procedure MS93-1.

TPS documentation homepage


MS93-1 : MATEOP

MS93-1 is a mating-search command.
Begin mating search MS93-1 on the current expansion proof.
The search is basically identical to MS89, but is performed using the
internal variable representations of MS90-9.
Primitive substitutions and duplications are performed systematically,
with multiple jforms being worked on simultaneously. On each
particular jform, the search procedure MS92-9 is used. The flags
MAX-SEARCH-LIMIT, SEARCH-TIME-LIMIT, and RANK-EPROOF-FN are used to
control the search. See also the command SHOW-OPTION-TREE.
 
The command format for MS93-1 is:

<Mate>MS93-1

TPS documentation homepage


MS93-1 : REVIEW-SUBJECT

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

TPS documentation homepage


MS93-1 : TPS-FILE

MS93-1 is a file.
Definitions, functions, etc., needed by ms93-1 and not already
provided by ms92-9. This is basically an extension to MS92-9, which
is why it's in the package MS90-3.
/home/theorem/tps/lisp/ms93-1.lisp is part of module MS90-3.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage