MT95-1 : MTREEOP

MT95-1 is a matingstree command.
Fewest Obligations Search: Choose the matingstree node (from the
entire tree, not just the tree below the current node) with the
fewest open obligations. Go to that node and do one step of MT94-12
(i.e. choose the literal with the fewest number of mates, and generate
all of the associated branches of the mtree).
Repeat until a closed leaf is generated.
This search is probably not complete.
 
The command format for MT95-1 is:

<Mtree>MT95-1 MTREE
"SYMBOL-OR-INTEGER"

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage