|
1 <HR><!------------------------------------------------------------------------> |
|
2 <H2>Isabelle/HOL 2013</H2> |
|
3 Jasmin C. Blanchette<sup>1</sup>, Lawrence C. Paulson<sup>2</sup>, |
|
4 Tobias Nipkow<sup>1</sup>, Makarius Wenzel<sup>3</sup> <BR> |
|
5 <sup>1</sup>Technische Universität München, Germany <BR> |
|
6 <sup>2</sup>University of Cambridge, United Kingdom <BR> |
|
7 <sup>3</sup>Université Paris Sud, France <BR> |
|
8 |
|
9 <H3>Architecture</H3> |
|
10 |
|
11 Isabelle/HOL 2013 [<A HREF="#References">NPW13</A>] is the higher-order |
|
12 logic incarnation of the generic proof assistant |
|
13 <A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/">Isabelle2013</A>. |
|
14 Isabelle/HOL provides several automatic proof tactics, notably an equational |
|
15 reasoner [<A HREF="#References">Nip89</A>], a classical reasoner [<A |
|
16 HREF="#References">Pau94</A>], and a tableau prover [<A |
|
17 HREF="#References">Pau99</A>]. It also integrates external first- and |
|
18 higher-order provers via its subsystem Sledgehammer [<A |
|
19 HREF="#References">PB10</A>, <A HREF="#References">BBP11</A>]. |
|
20 |
|
21 <P> |
|
22 Isabelle includes a parser for the TPTP syntaxes CNF, FOF, TFF0, and THF0, due |
|
23 to Nik Sultana. It also includes TPTP versions of its popular tools, invokable |
|
24 on the command line as <tt>isabelle tptp_<em>tool</em> <em>max_secs</em> |
|
25 <em>file.p</em></tt>. For example: |
|
26 |
|
27 <blockquote><pre> |
|
28 isabelle tptp_isabelle_hot 100 SEU/SEU824^3.p |
|
29 </pre></blockquote> |
|
30 |
|
31 <P> |
|
32 Two versions of Isabelle participate this year. The <em>demo</em> (or HOT) version |
|
33 includes its competitors LEO-II [<A HREF="#References">BPTF08</A>] and Satallax |
|
34 [<A HREF="#References">Bro12</A>] as Sledgehammer backends, whereas the |
|
35 <em>competition</em> version leaves them out. |
|
36 |
|
37 <H3>Strategies</H3> |
|
38 |
|
39 The <em>Isabelle</em> tactic submitted to the competition simply tries the |
|
40 following tactics sequentially: |
|
41 |
|
42 <DL> |
|
43 <DT> <tt>sledgehammer</tt> |
|
44 <DD> Invokes the following sequence of provers as oracles via Sledgehammer: |
|
45 <UL> |
|
46 <LI> <tt>satallax</tt>—Satallax 2.4 [<A HREF="#References">Bro12</A>] (<em>demo only</em>); |
|
47 <LI> <tt>leo2</tt>—LEO-II 1.3.2 [<A HREF="#References">BPTF08</A>] (<em>demo only</em>); |
|
48 <LI> <tt>spass</tt>—SPASS 3.8ds [<A HREF="#References">BPWW12</A>]; |
|
49 <LI> <tt>vampire</tt>—Vampire 1.8 (revision 1435) [<A HREF="#References">RV02</A>]; |
|
50 <LI> <tt>e</tt>—E 1.4 [<A HREF="#References">Sch04</A>]; |
|
51 <LI> <tt>z3_tptp</tt>—Z3 3.2 with TPTP syntax [<A HREF="#References">dMB08</A>]. |
|
52 </UL> |
|
53 <DT> <tt>nitpick</tt> |
|
54 <DD> For problems involving only the type <tt>$o</tt> of Booleans, checks |
|
55 whether a finite model exists using Nitpick [<A HREF="#References">BN10</A>]. |
|
56 <DT> <tt>simp</tt> |
|
57 <DD> Performs equational reasoning using rewrite rules [<A HREF="#References">Nip89</A>]. |
|
58 <DT> <tt>blast</tt> |
|
59 <DD> Searches for a proof using a fast untyped tableau prover and then |
|
60 attempts to reconstruct the proof using Isabelle tactics |
|
61 [<A HREF="#References">Pau99</A>]. |
|
62 <DT> <tt>auto+spass</tt> |
|
63 <DD> Combines simplification and classical reasoning |
|
64 [<A HREF="#References">Pau94</A>] under one roof; then invoke Sledgehammer |
|
65 with SPASS on any subgoals that emerge. |
|
66 <DT> <tt>z3</tt> |
|
67 <DD> Invokes the SMT solver Z3 3.2 [<A HREF="#References">dMB08</A>]. |
|
68 <DT> <tt>cvc3</tt> |
|
69 <DD> Invokes the SMT solver CVC3 2.2 [<A HREF="#References">BT07</A>]. |
|
70 <DT> <tt>fast</tt> |
|
71 <DD> Searches for a proof using sequent-style reasoning, performing a |
|
72 depth-first search [<A HREF="#References">Pau94</A>]. Unlike |
|
73 <tt>blast</tt>, it construct proofs directly in Isabelle. That makes it |
|
74 slower but enables it to work in the presence of the more unusual features |
|
75 of HOL, such as type classes and function unknowns. |
|
76 <DT> <tt>best</tt> |
|
77 <DD> Similar to <tt>fast</tt>, except that it performs a best-first search. |
|
78 <DT> <tt>force</tt> |
|
79 <DD> Similar to <tt>auto</tt>, but more exhaustive. |
|
80 <DT> <tt>meson</tt> |
|
81 <DD> Implements Loveland's MESON procedure [<A HREF="#References">Lov78</A>]. |
|
82 Constructs proofs directly in Isabelle. |
|
83 <DT> <tt>fastforce</tt> |
|
84 <DD> Combines <tt>fast</tt> and <tt>force</tt>. |
|
85 </DL> |
|
86 |
|
87 <H3>Implementation</H3> |
|
88 |
|
89 Isabelle is a generic theorem prover written in Standard ML. Its meta-logic, |
|
90 Isabelle/Pure, provides an intuitionistic fragment of higher-order logic. The |
|
91 HOL object logic extends pure with a more elaborate version of higher-order |
|
92 logic, complete with the familiar connectives and quantifiers. Other object |
|
93 logics are available, notably FOL (first-order logic) and ZF |
|
94 (Zermelo–Fraenkel set theory). |
|
95 <P> |
|
96 The implementation of Isabelle relies on a small LCF-style kernel, meaning that |
|
97 inferences are implemented as operations on an abstract <tt>theorem</tt> |
|
98 datatype. Assuming the kernel is correct, all values of type <tt>theorem</tt> |
|
99 are correct by construction. |
|
100 <P> |
|
101 Most of the code for Isabelle was written by the Isabelle teams at the |
|
102 University of Cambridge and the Technische Universität München. |
|
103 Isabelle/HOL is available for all major platforms under a BSD-style license |
|
104 from |
|
105 <PRE> |
|
106 <A HREF="http:////www.cl.cam.ac.uk/research/hvg/Isabelle/">http://www.cl.cam.ac.uk/research/hvg/Isabelle</A></PRE> |
|
107 |
|
108 <H3>Expected Competition Performance</H3> |
|
109 |
|
110 <P> |
|
111 Isabelle won last year by a thin margin. This year: first or second place. |
|
112 |
|
113 <H3>References</H3> |
|
114 <DL> |
|
115 |
|
116 <DT> BBP11 |
|
117 <DD> Blanchette J. C., Böhme S., Paulson L. C. (2011), |
|
118 <STRONG>Extending Sledgehammer with SMT Solvers</STRONG>, |
|
119 CADE-23, LNAI 6803, pp. 116–130, Springer. |
|
120 <DT> BN10 |
|
121 <DD> Blanchette J. C., Nipkow T. (2010), |
|
122 <STRONG>Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder</STRONG>, |
|
123 ITP 2010, <EM>LNCS</EM> 6172, pp. 131–146, Springer. |
|
124 <DT> BPTF08 |
|
125 <DD> Benzmüller C., Paulson L. C., Theiss F., Fietzke A. (2008), |
|
126 <STRONG>LEO-II—A Cooperative Automatic Theorem Prover for Higher-Order Logic</STRONG>, |
|
127 IJCAR 2008, <EM>LNAI</EM> 5195, pp. 162–170, Springer. |
|
128 <DT> BPWW12 |
|
129 <DD> Blanchette J. C., Popescu A., Wand D., Weidenbach C. (2012), |
|
130 <STRONG>More SPASS with Isabelle</STRONG>, |
|
131 ITP 2012, Springer. |
|
132 <DT> Bro12 |
|
133 <DD> Brown C. (2012), |
|
134 <STRONG>Satallax: An Automated Higher-Order Prover (System Description)</STRONG>, |
|
135 IJCAR 2012, Springer. |
|
136 <DT> BT07 |
|
137 <DD> Barrett C., Tinelli C. (2007), |
|
138 <STRONG>CVC3 (System Description)</STRONG>, |
|
139 CAV 2007, <EM>LNCS</EM> 4590, pp. 298–302, Springer. |
|
140 <DT> dMB08 |
|
141 <DD> de Moura L. M., Bjørner N. (2008), |
|
142 <STRONG>Z3: An Efficient SMT Solver</STRONG>, |
|
143 TACAS 2008, <EM>LNCS</EM> 4963, pp. 337–340, Springer. |
|
144 <DT> Lov78 |
|
145 <DD> Loveland D. W. (1978), |
|
146 <STRONG>Automated Theorem Proving: A Logical Basis</STRONG>, |
|
147 North-Holland Publishing Co. |
|
148 <DT> Nip89 |
|
149 <DD> Nipkow T. (1989), |
|
150 <STRONG>Equational Reasoning in Isabelle</STRONG>, |
|
151 <EM>Sci. Comput. Program.</EM> 12(2), |
|
152 pp. 123–149, |
|
153 Elsevier. |
|
154 <DT> NPW13 |
|
155 <DD> Nipkow T., Paulson L. C., Wenzel M. (2013), |
|
156 <STRONG>Isabelle/HOL: A Proof Assistant for Higher-Order Logic</STRONG>, |
|
157 <A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf">http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf</a>. |
|
158 <DT> Pau94 |
|
159 <DD> Paulson L. C. (1994), |
|
160 <STRONG>Isabelle: A Generic Theorem Prover</STRONG>, |
|
161 <EM>LNCS</EM> 828, |
|
162 Springer. |
|
163 <DT> Pau99 |
|
164 <DD> Paulson L. C. (1999), |
|
165 <STRONG>A Generic Tableau Prover and Its Integration with Isabelle</STRONG>, |
|
166 <EM>J. Univ. Comp. Sci.</EM> 5, |
|
167 pp. 73–87. |
|
168 <DT> PB10 |
|
169 <DD> Paulson L. C., Blanchette J. C. (2010), |
|
170 <STRONG>Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers</STRONG>, |
|
171 IWIL-2010. |
|
172 <DT> RV02 |
|
173 <DD> Riazanov A., Voronkov A. (2002), |
|
174 <STRONG>The Design and Implementation of Vampire</STRONG>, |
|
175 <EM>AI Comm.</EM> 15(2-3), 91–110. |
|
176 <DT> Sch04 |
|
177 <DD> Schulz S. (2004), |
|
178 <STRONG>System Description: E 0.81</STRONG>, |
|
179 IJCAR 2004, <EM>LNAI</EM> 3097, pp. 223–228, Springer. |
|
180 </DL> |
|
181 <P> |
|
182 |
|
183 <HR><!------------------------------------------------------------------------> |