[isabelle-dev] More SPASS with Isabelle

[Jasmin Blanchette]

Hi all,

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 [1], 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

       Linux: http://www21.in.tum.de/~blanchet/spass-linux/SPASS
       Mac: http://www21.in.tum.de/~blanchet/spass-darwin/SPASS

   and put it somewhere (e.g., in "/foo/bar").

2. Add the following line to your "~/.isabelle/etc/settings" file:

       SPASS_NEW_HOME=/foo/bar

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] =
               [m,n,b,v,c,x,z,l,k,j,h,g,f,d,s,a,p,i,u,y,t,r,e,w,q]"
    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.

[1] http://www4.in.tum.de/~blanchet/more-spass.pdf

Jasmin