Re: [isabelle] provers used by sledgehammer



Hi Christian,

Am 20.07.2012 um 09:28 schrieb Christian Sternagel:

> Let me reformulate ;). Why not use all installed provers by default? (If I wouldn't want to use it I would hardly install a prover.)

It's a bit tricky -- e.g. we ship CVC3, which is then installed but it doesn't mean you want to use it. CVC3 and Yices don't yield unsat cores or usable proofs, so we have to use brute-force minimalization to get usable Metis proofs, which can be quite expensive.

How many cores do you have on your machine? If you have only 4, then E, SPASS, Vampire, Z3 is probably the best combination anyway. If you have 8, then what you describe would probably make sense. I think I'll change the default to do something along those lines.

Cheers,

Jasmin






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.