## 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.