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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
