PPT Slide
Non-Incremental Hsearch: pseudocode
Mp* (x): Initialize the shared variables L:={}, tfast:=?, pfast:=p*. Start algorithms A, B and C in parallel with 10%, 10\% and 80% computational resources, respectively.
A: Run through all proofs. if a proof proves for some (p,t) that p(?)
is equivalent to p(?) and has time-bound t(?) then add (p,t) to L.
B: Compute all t(x) in parallel for all (p,t)?L with relative computation time 2-l(p)-l(t). If for some t, t(x)<tfast, then tfast:=t(x) and pfast:=p.
C: For k:=1,2,4,8,16,32,... do run current pfast for k steps (w/o switching)
If pfast halts in less than k steps,
then print result and abort A, B and C.
else continue with next k.
Back to J. Schmidhuber's OOPS page