MST-FEWEST-OB-SEARCH : WFFOP

MST-FEWEST-OB-SEARCH is a wff operation.
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 calling scheme for MST-FEWEST-OB-SEARCH is:

(MST-FEWEST-OB-SEARCH MTREE)
"SYMBOL-OR-INTEGER"


The result is of type OBLIGATION.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage