Dmitry Vyal wrote:

Currently I'm playing with theorem-proving using resolution. So I need some technique to break a computation, if takes too long.

When it comes to resolution proofs, perhaps a better approach is to use a better monad that natively offers termination guarantees. For example, http://pobox.com/~oleg/ftp/Computation/monads.html#fair-bt-stream First of all, the monad can let succeed the computations that surely diverge in List and similar monads. As the code at the end of that file shows, the monad avoids depth-first traps, and can even handle left-recursion at the monadic level. Furthermore, the monad has the inherent `timing' metric: Incomplete eliminations. Each elimination is bounded in time. One can specify the upper bound on the number of eliminations and thus force the termination if no solution was found thus far. It is possible to modify the run function of the monad to return the continuation once the counter has expired. So, one can run the monad for a bit more, if desired. In contrast to iterative deepening, running the continuation does _not_ repeat any of the previous work. We have used the FBackTrack monad to implement a Datalog-like system (with top-down. resolution-based search however), and we could successfully solve the problem of finding the transitive closure in a _cyclic_ graph (the poster problem for post-Prolog systems like XSB). No tabling was needed. A scheme version of the monad was used in a leanTAP theorem prover (for the full first-order predicate logic): http://cvs.sourceforge.net/viewcvs.py/kanren/kanren/mini/leanTAP.scm http://cvs.sourceforge.net/viewcvs.py/kanren/kanren/mini/book-si.scm The original leanTAP prover was meant to be used with iterative deepening. Our implementation removes the limiting counter from the leanTAP (which throttles instantiations of a universally quantified formula); the monad has enough strength to find the solution anyway (Pelletier problems 43 and 38).