LEAST-SEARCH-DEPTH : MEXPR

LEAST-SEARCH-DEPTH is a top-level command.
Print the least needed unification tree depth for the last proven
higher-order theorem. Also suggest to lower flags MAX-SEARCH-DEPTH to the least
needed value if they are greater than it.
The command format for LEAST-SEARCH-DEPTH is:

 <n>LEAST-SEARCH-DEPTH 

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage