4 ms·

I vote twice for this one!

• palashkulsh 10y ago
  Any laymen explanation ? Not able to grasp the concept.
  • deleted 10y ago
    [deleted]
  • pwdisswordfish 10y ago
    First you vote once, and then you vote again.
  • theemathas 10y ago
    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 since it is independent from the inputs. Of course, this constant is ridiculously huge.
    • AstralStorm 10y ago
      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.
  • palashkulsh 10y ago
    @theemathas thanks, @pwdisswordfish - nice one :D