[isabelle-dev] More SPASS with Isabelle
jasmin.blanchette at gmail.com
Tue Feb 14 18:02:43 CET 2012
The automatic prover SPASS, integrated in Sledgehammer, now includes many enhancements, such as properly oriented term simplification, that should make a difference for Isabelle problems. Thanks to these, SPASS has become more effective than E, Vampire, or Z3 , and this is just the beginning.
If you are using the latest development version of Isabelle and would like to try it out, simply follow these instructions:
1. Get the "SPASS" binary from
and put it somewhere (e.g., in "/foo/bar").
2. Add the following line to your "~/.isabelle/etc/settings" file:
That's all. When you restart PIDE or Proof General and try Sledgehammer, "spass_new" will be one of the provers used by default. (The naming convention is temporary; once it has left the experimental stage, it will be called "spass" and subsume the old SPASS 3.7.) To test that it works fine, try
lemma "rev [q,w,e,r,t,y,u,i,p,a,s,d,f,g,h,j,k,l,z,x,c,v,b,n,m] =
sledgehammer [preplay_timeout = 0]
and see if "spass_new" finds a proof really quick.
I would be very interested in getting feedback from users, to see whether the new SPASS makes a real difference in practice.
More information about the isabelle-dev