MST-LB-SEARCH : WFFOP

MST-LB-SEARCH is a wff operation.
Least Branching Search: In each leaf node, take the current
obligation and find a literal that can be mated, but with as few
mates as possible. Add all of these mates as sons to this node.
Repeat until a closed leaf is generated.
This search is probably not complete.
 
The calling scheme for MST-LB-SEARCH is:

(MST-LB-SEARCH MTREE)
"SYMBOL-OR-INTEGER"


The result is of type OBLIGATION.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage