Isabelle solvers: "auto" or "fastforce"? (comparison of solver strength)

Question

In Isabelle, I often find that I can prove a goal successfully using different solvers.

Generally I would prefer to use the weakest solver that can just about prove the goal. Based on my experience with Isabelle so far, my current understanding is that in order of increasing strength and decreasing speed, the common logic solvers rank as follows (i.e. when rule and simp both work, rule should be used, etc.):

rule < simp < auto < fastforce < force

Is this correct? Where does blast fit in here?

I checked Programming and Proving in Isabelle/HOL (PDF) and Concrete Semantics with Isabelle/HOL but couldn't find the answer.

Geodesic

Answer 1

There generally is no linear ordering on the strength of proving methods and your word "weakest" assume there is one. We can nevertheless say that "auto" generally have at least the power of "simp" or "rule" but as it is more powerful it can also do some useless work that can make it fail. fastforce, bestsimp and slowsimp have the same power with different proof search strategies.

I can't really say more details on this, but maybe someone else could.

Hannigan

I posted a new question about the difference between arith and presburger since that seems relatively unrelated. – Geodesic

Can you point me to a description of the proof strategies employed by fastforce, bestsimp, slowsimp etc.? – Geodesic

The most detailed description I could find was in section 9.4.4 of the Isabelle/Isar Reference Manual (isabelle.in.tum.de/dist/Isabelle2014/doc/isar-ref.pdf). I have never used bestsimp, slow, fast etc. myself; they are very rare. assumption, fact, rule, erule, intro, elim, clarify, simp, simp_all, blast, fastforce, force, auto and sometimes more specialised ones like induction, arith, algebra, etc. are the methods I use normally. Most of the time, you can get by with auto and simp/simp_all. – Valley