Earlier quoted context omitted.
Any laymen explanation ? Not able to grasp the concept.
It does two things concurrently: (1) search for an algorithm along with proofs for its correctness and time upper bound (2) run the fastest algorithm found so far, possibly aborting an slower algorithm when a faster one is found. Everything is scheduled so it's asymptotically optimal. However, there's an added cost to search for algorithms. This cost is exponential in the proof length, but constant for each problem s…
Funny thing is, you can offload most of this to compile time, which is what Isabelle is doing, but then you miss out on guaranteed optimal runtime. Also the proof database may not be complete anyway.