Re: [isabelle] Difficulties with "setsum" (Alfio Martini)



On Wed, 22 Apr 2015, Alfio Martini wrote:

I use the Windows installation of  Isabelle 2014 and my sledgehammer
installation does not find any proof for this lemma. Actually, it never
finds any proof whatsoever. I have just realized that it does not solve
even that lemma in section 3 (First Steps) of the Sledgehammer tutorial. I
have always used Sledgehammer as it is packaged. I just set z3
non-commercial
use to "yes". The prover "remote-vampire" is never available (literally),
while e, spass and z3 always time out.

I will have to take a look into this. This is really making may Isabelle
experience miserable  at the moment.

There is Isabelle2015-RC1 already, to try if the situation has improved. If not, we also need a bit of information about your hardware and operating system version.

I am not aware of any such problems in Isabelle2014 or Isabelle2015-RC1, so unless there are tangible problem reports, the problems don't exist.


	Makarius





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