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:


TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage