MS90-9 : CONTEXT

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

TPS documentation homepage


MS90-9 : MATEOP

MS90-9 is a mating-search command.
Begin mating search MS90-9 on the current expansion proof.
Primitive substitutions and duplications are performed systematically,
with multiple jforms being worked on simultaneously. On each
particular jform, the search procedure MS90-3 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 MS90-9 is:

<Mate>MS90-9

TPS documentation homepage


MS90-9 : MODULE

MS90-9 is a module.

It is loaded.
Defines functions for integrating option trees with the search
procedure ms90-3.

NEEDED-MODULES MS89 MS90-3

FILES MS90-9

TPS documentation homepage


MS90-9 : REVIEW-SUBJECT

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

TPS documentation homepage


MS90-9 : TPS-FILE

MS90-9 is a file.
Contains mateops for using option tree search procedure with
path-focused duplication.
/home/theorem/tps/lisp/ms90-9.lisp is part of module MS90-9.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage