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