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:
+
+ - satallax—Satallax 2.4 [Bro12] (demo only);
+
- leo2—LEO-II 1.3.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].
+
+ - 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.
+
+
+
+