# HG changeset patch # User blanchet # Date 1436808170 -7200 # Node ID 9a14d574ea65de4d2b02f4f220cee6440b6e8c38 # Parent 8e82a83757dff98274ff65db042d609583f2588a updated Isabelle description to CASC diff -r 8e82a83757df -r 9a14d574ea65 src/HOL/TPTP/CASC/SysDesc_Isabelle.html --- a/src/HOL/TPTP/CASC/SysDesc_Isabelle.html Mon Jul 13 16:54:27 2015 +0200 +++ b/src/HOL/TPTP/CASC/SysDesc_Isabelle.html Mon Jul 13 19:22:50 2015 +0200 @@ -43,12 +43,11 @@

sledgehammer

Invokes the following sequence of provers as oracles via Sledgehammer:

satallax—Satallax 2.4 [Bro12] (demo only); -
leo2—LEO-II 1.3.2 [BPTF08] (demo only); +
satallax—Satallax 2.7 [Bro12] (demo only); +
leo2—LEO-II 1.6.2 [BPTF08] (demo only);
spass—SPASS 3.8ds [BPWW12]; -
vampire—Vampire 1.8 (revision 1435) [RV02]; -
e—E 1.4 [Sch04]; -
z3_tptp—Z3 3.2 with TPTP syntax [dMB08]. +
vampire—Vampire 3.0 (revision 1803) [RV02]; +
e—E 1.8 [Sch04];

nitpick

For problems involving only the type $o of Booleans, checks @@ -64,9 +63,9 @@ [Pau94] under one roof; then invoke Sledgehammer with SPASS on any subgoals that emerge.

z3 -

Invokes the SMT solver Z3 3.2 [dMB08]. -

cvc3 -

Invokes the SMT solver CVC3 2.2 [BT07]. +

Invokes the SMT solver Z3 4.4.0-prerelease [dMB08]. +

cvc4 +

Invokes the SMT solver CVC4 1.5-prerelease [BT07].

fast

Searches for a proof using sequent-style reasoning, performing a depth-first search [Pau94]. Unlike