diff -r f353fe3c2b92 -r 6c38df1d294a src/HOL/TPTP/CASC/SysDesc_Isabelle.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/CASC/SysDesc_Isabelle.html Tue May 21 11:01:14 2013 +0200 @@ -0,0 +1,183 @@ +
+

Isabelle/HOL 2013

+Jasmin C. Blanchette1, Lawrence C. Paulson2, +Tobias Nipkow1, Makarius Wenzel3
+1Technische Universität München, Germany
+2University of Cambridge, United Kingdom
+3Université Paris Sud, France
+ +

Architecture

+ +Isabelle/HOL 2013 [NPW13] is the higher-order +logic incarnation of the generic proof assistant +Isabelle2013. +Isabelle/HOL provides several automatic proof tactics, notably an equational +reasoner [Nip89], a classical reasoner [Pau94], and a tableau prover [Pau99]. It also integrates external first- and +higher-order provers via its subsystem Sledgehammer [PB10, BBP11]. + +

+Isabelle includes a parser for the TPTP syntaxes CNF, FOF, TFF0, and THF0, due +to Nik Sultana. It also includes TPTP versions of its popular tools, invokable +on the command line as isabelle tptp_tool max_secs +file.p. For example: + +

+isabelle tptp_isabelle_hot 100 SEU/SEU824^3.p
+
+ +

+Two versions of Isabelle participate this year. The demo (or HOT) version +includes its competitors LEO-II [BPTF08] and Satallax +[Bro12] as Sledgehammer backends, whereas the +competition version leaves them out. + +

Strategies

+ +The Isabelle tactic submitted to the competition simply tries the +following tactics sequentially: + +
+
sledgehammer +
Invokes the following sequence of provers as oracles via Sledgehammer: + +
nitpick +
For problems involving only the type $o of Booleans, checks + whether a finite model exists using Nitpick [BN10]. +
simp +
Performs equational reasoning using rewrite rules [Nip89]. +
blast +
Searches for a proof using a fast untyped tableau prover and then + attempts to reconstruct the proof using Isabelle tactics + [Pau99]. +
auto+spass +
Combines simplification and classical reasoning + [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]. +
fast +
Searches for a proof using sequent-style reasoning, performing a + depth-first search [Pau94]. Unlike + blast, it construct proofs directly in Isabelle. That makes it + slower but enables it to work in the presence of the more unusual features + of HOL, such as type classes and function unknowns. +
best +
Similar to fast, except that it performs a best-first search. +
force +
Similar to auto, but more exhaustive. +
meson +
Implements Loveland's MESON procedure [Lov78]. +Constructs proofs directly in Isabelle. +
fastforce +
Combines fast and force. +
+ +

Implementation

+ +Isabelle is a generic theorem prover written in Standard ML. Its meta-logic, +Isabelle/Pure, provides an intuitionistic fragment of higher-order logic. The +HOL object logic extends pure with a more elaborate version of higher-order +logic, complete with the familiar connectives and quantifiers. Other object +logics are available, notably FOL (first-order logic) and ZF +(Zermelo–Fraenkel set theory). +

+The implementation of Isabelle relies on a small LCF-style kernel, meaning that +inferences are implemented as operations on an abstract theorem +datatype. Assuming the kernel is correct, all values of type theorem +are correct by construction. +

+Most of the code for Isabelle was written by the Isabelle teams at the +University of Cambridge and the Technische Universität München. +Isabelle/HOL is available for all major platforms under a BSD-style license +from +

+    http://www.cl.cam.ac.uk/research/hvg/Isabelle
+ +

Expected Competition Performance

+ +

+Isabelle won last year by a thin margin. This year: first or second place. + +

References

+
+ +
BBP11 +
Blanchette J. C., Böhme S., Paulson L. C. (2011), + Extending Sledgehammer with SMT Solvers, + CADE-23, LNAI 6803, pp. 116–130, Springer. +
BN10 +
Blanchette J. C., Nipkow T. (2010), + Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder, + ITP 2010, LNCS 6172, pp. 131–146, Springer. +
BPTF08 +
Benzmüller C., Paulson L. C., Theiss F., Fietzke A. (2008), + LEO-II—A Cooperative Automatic Theorem Prover for Higher-Order Logic, + IJCAR 2008, LNAI 5195, pp. 162–170, Springer. +
BPWW12 +
Blanchette J. C., Popescu A., Wand D., Weidenbach C. (2012), + More SPASS with Isabelle, + ITP 2012, Springer. +
Bro12 +
Brown C. (2012), + Satallax: An Automated Higher-Order Prover (System Description), + IJCAR 2012, Springer. +
BT07 +
Barrett C., Tinelli C. (2007), + CVC3 (System Description), + CAV 2007, LNCS 4590, pp. 298–302, Springer. +
dMB08 +
de Moura L. M., Bjørner N. (2008), + Z3: An Efficient SMT Solver, + TACAS 2008, LNCS 4963, pp. 337–340, Springer. +
Lov78 +
Loveland D. W. (1978), + Automated Theorem Proving: A Logical Basis, + North-Holland Publishing Co. +
Nip89 +
Nipkow T. (1989), + Equational Reasoning in Isabelle, + Sci. Comput. Program. 12(2), + pp. 123–149, + Elsevier. +
NPW13 +
Nipkow T., Paulson L. C., Wenzel M. (2013), + Isabelle/HOL: A Proof Assistant for Higher-Order Logic, + http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf. +
Pau94 +
Paulson L. C. (1994), + Isabelle: A Generic Theorem Prover, + LNCS 828, + Springer. +
Pau99 +
Paulson L. C. (1999), + A Generic Tableau Prover and Its Integration with Isabelle, + J. Univ. Comp. Sci. 5, + pp. 73–87. +
PB10 +
Paulson L. C., Blanchette J. C. (2010), + Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers, + IWIL-2010. +
RV02 +
Riazanov A., Voronkov A. (2002), + The Design and Implementation of Vampire, + AI Comm. 15(2-3), 91–110. +
Sch04 +
Schulz S. (2004), + System Description: E 0.81, + IJCAR 2004, LNAI 3097, pp. 223–228, Springer. +
+

+ +