author | blanchet |
Wed, 03 Nov 2010 22:51:32 +0100 | |
changeset 40343 | 4521d56aef63 |
parent 40341 | 03156257040f |
child 40689 | 3a10ce7cd436 |
permissions | -rw-r--r-- |
36926 | 1 |
\documentclass[a4paper,12pt]{article} |
2 |
\usepackage[T1]{fontenc} |
|
3 |
\usepackage{amsmath} |
|
4 |
\usepackage{amssymb} |
|
5 |
\usepackage[english,french]{babel} |
|
6 |
\usepackage{color} |
|
7 |
\usepackage{footmisc} |
|
8 |
\usepackage{graphicx} |
|
9 |
%\usepackage{mathpazo} |
|
10 |
\usepackage{multicol} |
|
11 |
\usepackage{stmaryrd} |
|
12 |
%\usepackage[scaled=.85]{beramono} |
|
13 |
\usepackage{../iman,../pdfsetup} |
|
14 |
||
15 |
%\oddsidemargin=4.6mm |
|
16 |
%\evensidemargin=4.6mm |
|
17 |
%\textwidth=150mm |
|
18 |
%\topmargin=4.6mm |
|
19 |
%\headheight=0mm |
|
20 |
%\headsep=0mm |
|
21 |
%\textheight=234mm |
|
22 |
||
23 |
\def\Colon{\mathord{:\mkern-1.5mu:}} |
|
24 |
%\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}} |
|
25 |
%\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}} |
|
26 |
\def\lparr{\mathopen{(\mkern-4mu\mid}} |
|
27 |
\def\rparr{\mathclose{\mid\mkern-4mu)}} |
|
28 |
||
29 |
\def\unk{{?}} |
|
30 |
\def\undef{(\lambda x.\; \unk)} |
|
31 |
%\def\unr{\textit{others}} |
|
32 |
\def\unr{\ldots} |
|
33 |
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}} |
|
34 |
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}} |
|
35 |
||
36 |
\urlstyle{tt} |
|
37 |
||
38 |
\begin{document} |
|
39 |
||
40 |
\selectlanguage{english} |
|
41 |
||
42 |
\title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex] |
|
43 |
Hammering Away \\[\smallskipamount] |
|
44 |
\Large A User's Guide to Sledgehammer for Isabelle/HOL} |
|
45 |
\author{\hbox{} \\ |
|
46 |
Jasmin Christian Blanchette \\ |
|
47 |
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\ |
|
48 |
\hbox{}} |
|
49 |
||
50 |
\maketitle |
|
51 |
||
52 |
\tableofcontents |
|
53 |
||
54 |
\setlength{\parskip}{.7em plus .2em minus .1em} |
|
55 |
\setlength{\parindent}{0pt} |
|
56 |
\setlength{\abovedisplayskip}{\parskip} |
|
57 |
\setlength{\abovedisplayshortskip}{.9\parskip} |
|
58 |
\setlength{\belowdisplayskip}{\parskip} |
|
59 |
\setlength{\belowdisplayshortskip}{.9\parskip} |
|
60 |
||
61 |
% General-purpose enum environment with correct spacing |
|
62 |
\newenvironment{enum}% |
|
63 |
{\begin{list}{}{% |
|
64 |
\setlength{\topsep}{.1\parskip}% |
|
65 |
\setlength{\partopsep}{.1\parskip}% |
|
66 |
\setlength{\itemsep}{\parskip}% |
|
67 |
\advance\itemsep by-\parsep}} |
|
68 |
{\end{list}} |
|
69 |
||
70 |
\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin |
|
71 |
\advance\rightskip by\leftmargin} |
|
72 |
\def\post{\vskip0pt plus1ex\endgroup} |
|
73 |
||
74 |
\def\prew{\pre\advance\rightskip by-\leftmargin} |
|
75 |
\def\postw{\post} |
|
76 |
||
77 |
\section{Introduction} |
|
78 |
\label{introduction} |
|
79 |
||
80 |
Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs) |
|
40073 | 81 |
and satisfiability-modulo-theory (SMT) solvers on the current goal. The |
82 |
supported ATPs are E \cite{schulz-2002}, SPASS \cite{weidenbach-et-al-2009}, |
|
83 |
Vampire \cite{riazanov-voronkov-2002}, SInE-E \cite{sine}, and SNARK |
|
84 |
\cite{snark}. The ATPs are run either locally or remotely via the |
|
85 |
System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs, the |
|
86 |
\textit{smt} proof method (which typically relies on the Z3 SMT solver |
|
87 |
\cite{z3}) is tried as well. |
|
36926 | 88 |
|
40073 | 89 |
The problem passed to the automatic provers consists of your current goal |
90 |
together with a heuristic selection of hundreds of facts (theorems) from the |
|
91 |
current theory context, filtered by relevance. Because jobs are run in the |
|
92 |
background, you can continue to work on your proof by other means. Provers can |
|
93 |
be run in parallel. Any reply (which may arrive half a minute later) will appear |
|
94 |
in the Proof General response buffer. |
|
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
95 |
|
40073 | 96 |
The result of a successful proof search is some source text that usually (but |
97 |
not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed |
|
98 |
proof relies on the general-purpose Metis prover \cite{metis}, which is fully |
|
99 |
integrated into Isabelle/HOL, with explicit inferences going through the kernel. |
|
100 |
Thus its results are correct by construction. |
|
36926 | 101 |
|
39320 | 102 |
In this manual, we will explicitly invoke the \textbf{sledgehammer} command. |
103 |
Sledgehammer also provides an automatic mode that can be enabled via the |
|
104 |
``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof General. In |
|
105 |
this mode, Sledgehammer is run on every newly entered theorem. The time limit |
|
106 |
for Auto Sledgehammer and other automatic tools can be set using the ``Auto |
|
107 |
Tools Time Limit'' option. |
|
108 |
||
36926 | 109 |
\newbox\boxA |
110 |
\setbox\boxA=\hbox{\texttt{nospam}} |
|
111 |
||
112 |
Examples of Sledgehammer use can be found in Isabelle's |
|
113 |
\texttt{src/HOL/Metis\_Examples} directory. |
|
114 |
Comments and bug reports concerning Sledgehammer or this manual should be |
|
115 |
directed to |
|
116 |
\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak |
|
117 |
in.\allowbreak tum.\allowbreak de}. |
|
118 |
||
119 |
\vskip2.5\smallskipamount |
|
120 |
||
121 |
%\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for |
|
122 |
%suggesting several textual improvements. |
|
123 |
||
124 |
\section{Installation} |
|
125 |
\label{installation} |
|
126 |
||
127 |
Sledgehammer is part of Isabelle, so you don't need to install it. However, it |
|
40073 | 128 |
relies on third-party automatic theorem provers (ATPs) and SAT solvers. |
129 |
Currently, E, SPASS, and Vampire can be run locally; in addition, E, Vampire, |
|
130 |
SInE-E, and SNARK are available remotely via SystemOnTPTP \cite{sutcliffe-2000}. |
|
131 |
If you want better performance, you should install E and SPASS locally. |
|
36926 | 132 |
|
38043 | 133 |
There are three main ways to install ATPs on your machine: |
36926 | 134 |
|
135 |
\begin{enum} |
|
136 |
\item[$\bullet$] If you installed an official Isabelle package with everything |
|
137 |
inside, it should already include properly setup executables for E and SPASS, |
|
38043 | 138 |
ready to use.% |
139 |
\footnote{Vampire's license prevents us from doing the same for this otherwise |
|
140 |
wonderful tool.} |
|
36926 | 141 |
|
38043 | 142 |
\item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS |
36926 | 143 |
binary packages from Isabelle's download page. Extract the archives, then add a |
40203 | 144 |
line to your \texttt{\char`\~/.isabelle/etc/components} file with the absolute |
145 |
path to E or SPASS. For example, if the \texttt{components} does not exist yet |
|
146 |
and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create the |
|
147 |
\texttt{components} file with the single line |
|
36926 | 148 |
|
149 |
\prew |
|
150 |
\texttt{/usr/local/spass-3.7} |
|
151 |
\postw |
|
152 |
||
38043 | 153 |
in it. |
154 |
||
155 |
\item[$\bullet$] If you prefer to build E or SPASS yourself, or obtained a |
|
156 |
Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}), |
|
157 |
set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or |
|
158 |
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof}, |
|
38063 | 159 |
\texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested |
160 |
with E 1.0 and 1.2, SPASS 3.5 and 3.7, and Vampire 1.0% |
|
161 |
\footnote{Following the rewrite of Vampire, the counter for version numbers was |
|
162 |
reset to 0; hence the new Vampire 1.0 is more recent than Vampire 11.5.}% |
|
163 |
. Since the ATPs' output formats are neither documented nor stable, other |
|
164 |
versions of the ATPs might or might not work well with Sledgehammer. |
|
36926 | 165 |
\end{enum} |
166 |
||
167 |
To check whether E and SPASS are installed, follow the example in |
|
168 |
\S\ref{first-steps}. |
|
169 |
||
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
170 |
Remote ATP invocation via the SystemOnTPTP web service requires Perl with the |
39152
f09b378cb252
make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents:
38997
diff
changeset
|
171 |
World Wide Web Library (\texttt{libwww-perl}) installed. If you must use a proxy |
f09b378cb252
make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents:
38997
diff
changeset
|
172 |
server to access the Internet, set the \texttt{http\_proxy} environment variable |
39153 | 173 |
to the proxy, either in the environment in which Isabelle is launched or in your |
174 |
\texttt{\char`\~/.isabelle/etc/settings} file. Here are a few examples: |
|
39152
f09b378cb252
make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents:
38997
diff
changeset
|
175 |
|
f09b378cb252
make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents:
38997
diff
changeset
|
176 |
\prew |
39153 | 177 |
\texttt{http\_proxy=http://proxy.example.org} \\ |
178 |
\texttt{http\_proxy=http://proxy.example.org:8080} \\ |
|
179 |
\texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org} |
|
39152
f09b378cb252
make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents:
38997
diff
changeset
|
180 |
\postw |
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
181 |
|
36926 | 182 |
\section{First Steps} |
183 |
\label{first-steps} |
|
184 |
||
185 |
To illustrate Sledgehammer in context, let us start a theory file and |
|
186 |
attempt to prove a simple lemma: |
|
187 |
||
188 |
\prew |
|
189 |
\textbf{theory}~\textit{Scratch} \\ |
|
190 |
\textbf{imports}~\textit{Main} \\ |
|
191 |
\textbf{begin} \\[2\smallskipamount] |
|
192 |
% |
|
193 |
\textbf{lemma} ``$[a] = [b] \,\longleftrightarrow\, a = b$'' \\ |
|
194 |
\textbf{sledgehammer} |
|
195 |
\postw |
|
196 |
||
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
197 |
Instead of issuing the \textbf{sledgehammer} command, you can also find |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
198 |
Sledgehammer in the ``Commands'' submenu of the ``Isabelle'' menu in Proof |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
199 |
General or press the Emacs key sequence C-c C-a C-s. |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
200 |
Either way, Sledgehammer produces the following output after a few seconds: |
36926 | 201 |
|
202 |
\prew |
|
203 |
\slshape |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
204 |
Sledgehammer: ``\textit{e}'' for subgoal 1: \\ |
36926 | 205 |
$([a] = [b]) = (a = b)$ \\ |
206 |
Try this command: \textbf{by} (\textit{metis hd.simps}). \\ |
|
38043 | 207 |
To minimize the number of lemmas, try this: \\ |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
208 |
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount] |
36926 | 209 |
% |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
210 |
Sledgehammer: ``\textit{spass}'' for subgoal 1: \\ |
36926 | 211 |
$([a] = [b]) = (a = b)$ \\ |
212 |
Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\ |
|
38043 | 213 |
To minimize the number of lemmas, try this: \\ |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
214 |
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount] |
36926 | 215 |
% |
40073 | 216 |
Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\ |
36926 | 217 |
$([a] = [b]) = (a = b)$ \\ |
40073 | 218 |
Try this command: \textbf{by} (\textit{metis eq\_commute last\_snoc}) \\ |
38043 | 219 |
To minimize the number of lemmas, try this: \\ |
40073 | 220 |
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}]~(\textit{eq\_commute last\_snoc}). \\[3\smallskipamount] |
221 |
% |
|
222 |
Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\ |
|
223 |
$([a] = [b]) = (a = b)$ \\ |
|
224 |
Try this command: \textbf{by} (\textit{metis hd.simps}) \\ |
|
225 |
To minimize the number of lemmas, try this: \\ |
|
40203 | 226 |
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}). |
36926 | 227 |
\postw |
228 |
||
40073 | 229 |
Sledgehammer ran E, SPASS, Vampire, SInE-E, and the \textit{smt} proof method in |
230 |
parallel. Depending on which provers are installed and how many processor cores |
|
231 |
are available, some of the provers might be missing or present with a |
|
232 |
\textit{remote\_} prefix. |
|
36926 | 233 |
|
40073 | 234 |
For each successful prover, Sledgehammer gives a one-liner proof that uses the |
235 |
\textit{metis} or \textit{smt} method. You can click the proof to insert it into |
|
236 |
the theory text. You can click the ``\textbf{sledgehammer} \textit{minimize}'' |
|
237 |
command if you want to look for a shorter (and probably faster) proof. But here |
|
238 |
the proof found by E looks perfect, so click it to finish the proof. |
|
36926 | 239 |
|
240 |
You can ask Sledgehammer for an Isar text proof by passing the |
|
241 |
\textit{isar\_proof} option: |
|
242 |
||
243 |
\prew |
|
244 |
\textbf{sledgehammer} [\textit{isar\_proof}] |
|
245 |
\postw |
|
246 |
||
247 |
When Isar proof construction is successful, it can yield proofs that are more |
|
248 |
readable and also faster than the \textit{metis} one-liners. This feature is |
|
40073 | 249 |
experimental and is only available for ATPs. |
36926 | 250 |
|
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
251 |
\section{Hints} |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
252 |
\label{hints} |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
253 |
|
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
254 |
For best results, first simplify your problem by calling \textit{auto} or at |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
255 |
least \textit{safe} followed by \textit{simp\_all}. None of the ATPs contain |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
256 |
arithmetic decision procedures. They are not especially good at heavy rewriting, |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
257 |
but because they regard equations as undirected, they often prove theorems that |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
258 |
require the reverse orientation of a \textit{simp} rule. Higher-order problems |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
259 |
can be tackled, but the success rate is better for first-order problems. Hence, |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
260 |
you may get better results if you first simplify the problem to remove |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
261 |
higher-order features. |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
262 |
|
39320 | 263 |
Note that problems can be easy for \textit{auto} and difficult for ATPs, but the |
264 |
reverse is also true, so don't be discouraged if your first attempts fail. |
|
265 |
Because the system refers to all theorems known to Isabelle, it is particularly |
|
266 |
suitable when your goal has a short proof from lemmas that you don't know about. |
|
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
267 |
|
36926 | 268 |
\section{Command Syntax} |
269 |
\label{command-syntax} |
|
270 |
||
271 |
Sledgehammer can be invoked at any point when there is an open goal by entering |
|
272 |
the \textbf{sledgehammer} command in the theory file. Its general syntax is as |
|
273 |
follows: |
|
274 |
||
275 |
\prew |
|
276 |
\textbf{sledgehammer} \textit{subcommand\/$^?$ options\/$^?$ facts\_override\/$^?$ num\/$^?$} |
|
277 |
\postw |
|
278 |
||
279 |
For convenience, Sledgehammer is also available in the ``Commands'' submenu of |
|
280 |
the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c |
|
281 |
C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with |
|
282 |
no arguments in the theory text. |
|
283 |
||
284 |
In the general syntax, the \textit{subcommand} may be any of the following: |
|
285 |
||
286 |
\begin{enum} |
|
40203 | 287 |
\item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on |
288 |
subgoal number \textit{num} (1 by default), with the given options and facts. |
|
36926 | 289 |
|
290 |
\item[$\bullet$] \textbf{\textit{minimize}:} Attempts to minimize the provided facts |
|
291 |
(specified in the \textit{facts\_override} argument) to obtain a simpler proof |
|
292 |
involving fewer facts. The options and goal number are as for \textit{run}. |
|
293 |
||
40203 | 294 |
\item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued |
295 |
by Sledgehammer. This allows you to examine results that might have been lost |
|
296 |
due to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a |
|
36926 | 297 |
limit on the number of messages to display (5 by default). |
298 |
||
40203 | 299 |
\item[$\bullet$] \textbf{\textit{available\_provers}:} Prints the list of |
300 |
installed provers. See \S\ref{installation} and \S\ref{mode-of-operation} for |
|
301 |
more information on how to install automatic provers. |
|
36926 | 302 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
303 |
\item[$\bullet$] \textbf{\textit{running\_provers}:} Prints information about |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
304 |
currently running automatic provers, including elapsed runtime and remaining |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
305 |
time until timeout. |
36926 | 306 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
307 |
\item[$\bullet$] \textbf{\textit{kill\_provers}:} Terminates all running |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
308 |
automatic provers. |
36926 | 309 |
|
310 |
\item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote |
|
311 |
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}. |
|
312 |
\end{enum} |
|
313 |
||
314 |
Sledgehammer's behavior can be influenced by various \textit{options}, which can |
|
315 |
be specified in brackets after the \textbf{sledgehammer} command. The |
|
316 |
\textit{options} are a list of key--value pairs of the form ``[$k_1 = v_1, |
|
317 |
\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true}'' is optional. For |
|
318 |
example: |
|
319 |
||
320 |
\prew |
|
321 |
\textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120$\,s$] |
|
322 |
\postw |
|
323 |
||
324 |
Default values can be set using \textbf{sledgehammer\_\allowbreak params}: |
|
325 |
||
326 |
\prew |
|
327 |
\textbf{sledgehammer\_params} \textit{options} |
|
328 |
\postw |
|
329 |
||
330 |
The supported options are described in \S\ref{option-reference}. |
|
331 |
||
332 |
The \textit{facts\_override} argument lets you alter the set of facts that go |
|
333 |
through the relevance filter. It may be of the form ``(\textit{facts})'', where |
|
334 |
\textit{facts} is a space-separated list of Isabelle facts (theorems, local |
|
335 |
assumptions, etc.), in which case the relevance filter is bypassed and the given |
|
39320 | 336 |
facts are used. It may also be of the form ``(\textit{add}:\ \textit{facts}$_1$)'', |
337 |
``(\textit{del}:\ \textit{facts}$_2$)'', or ``(\textit{add}:\ \textit{facts}$_1$\ |
|
338 |
\textit{del}:\ \textit{facts}$_2$)'', where the relevance filter is instructed to |
|
36926 | 339 |
proceed as usual except that it should consider \textit{facts}$_1$ |
340 |
highly-relevant and \textit{facts}$_2$ fully irrelevant. |
|
341 |
||
39320 | 342 |
You can instruct Sledgehammer to run automatically on newly entered theorems by |
343 |
enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
344 |
General. For automatic runs, only the first prover set using \textit{provers} |
39320 | 345 |
(\S\ref{mode-of-operation}) is considered, \textit{verbose} |
346 |
(\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled, |
|
40073 | 347 |
fewer facts are passed to the prover, and \textit{timeout} |
348 |
(\S\ref{mode-of-operation}) is superseded by the ``Auto Tools Time Limit'' in |
|
349 |
Proof General's ``Isabelle'' menu. Sledgehammer's output is also more concise. |
|
39320 | 350 |
|
36926 | 351 |
\section{Option Reference} |
352 |
\label{option-reference} |
|
353 |
||
354 |
\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}} |
|
355 |
\def\qty#1{$\left<\textit{#1}\right>$} |
|
356 |
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$} |
|
357 |
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} |
|
358 |
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} |
|
359 |
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} |
|
360 |
\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} |
|
361 |
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]} |
|
362 |
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]} |
|
363 |
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]} |
|
364 |
\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} |
|
365 |
\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} |
|
366 |
||
367 |
Sledgehammer's options are categorized as follows:\ mode of operation |
|
38984 | 368 |
(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), |
369 |
relevance filter (\S\ref{relevance-filter}), output format |
|
370 |
(\S\ref{output-format}), and authentication (\S\ref{authentication}). |
|
36926 | 371 |
|
372 |
The descriptions below refer to the following syntactic quantities: |
|
373 |
||
374 |
\begin{enum} |
|
375 |
\item[$\bullet$] \qtybf{string}: A string. |
|
376 |
\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}. |
|
40203 | 377 |
\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or |
378 |
\textit{smart}. |
|
36926 | 379 |
\item[$\bullet$] \qtybf{int\/}: An integer. |
40343
4521d56aef63
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset
|
380 |
\item[$\bullet$] \qtybf{float\_pair\/}: A pair of floating-point numbers |
4521d56aef63
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset
|
381 |
(e.g., 0.6 0.95). |
38591 | 382 |
\item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}. |
40343
4521d56aef63
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset
|
383 |
\item[$\bullet$] \qtybf{float\_or\_none\/}: An integer (e.g., 60) or |
4521d56aef63
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset
|
384 |
floating-point number (e.g., 0.5) expressing a number of seconds, or the keyword |
4521d56aef63
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset
|
385 |
\textit{none} ($\infty$ seconds). |
36926 | 386 |
\end{enum} |
387 |
||
388 |
Default values are indicated in square brackets. Boolean options have a negated |
|
38984 | 389 |
counterpart (e.g., \textit{blocking} vs.\ \textit{non\_blocking}). When setting |
36926 | 390 |
Boolean options, ``= \textit{true}'' may be omitted. |
391 |
||
392 |
\subsection{Mode of Operation} |
|
393 |
\label{mode-of-operation} |
|
394 |
||
395 |
\begin{enum} |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
396 |
\opnodefault{provers}{string} |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
397 |
Specifies the automatic provers to use as a space-separated list (e.g., |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
398 |
``\textit{e}~\textit{spass}''). The following provers are supported: |
36926 | 399 |
|
400 |
\begin{enum} |
|
401 |
\item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz |
|
402 |
\cite{schulz-2002}. To use E, set the environment variable |
|
403 |
\texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable, |
|
404 |
or install the prebuilt E package from Isabelle's download page. See |
|
405 |
\S\ref{installation} for details. |
|
406 |
||
407 |
\item[$\bullet$] \textbf{\textit{spass}:} SPASS is an ATP developed by Christoph |
|
408 |
Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the |
|
409 |
environment variable \texttt{SPASS\_HOME} to the directory that contains the |
|
410 |
\texttt{SPASS} executable, or install the prebuilt SPASS package from Isabelle's |
|
37414
d0cea0796295
expect SPASS 3.7, and give a friendly warning if an older version is used
blanchet
parents:
36926
diff
changeset
|
411 |
download page. Sledgehammer requires version 3.5 or above. See |
d0cea0796295
expect SPASS 3.7, and give a friendly warning if an older version is used
blanchet
parents:
36926
diff
changeset
|
412 |
\S\ref{installation} for details. |
36926 | 413 |
|
414 |
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by |
|
415 |
Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use |
|
416 |
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory |
|
417 |
that contains the \texttt{vampire} executable. |
|
418 |
||
40073 | 419 |
\item[$\bullet$] \textbf{\textit{smt}:} The \textit{smt} proof method invokes an |
420 |
external SMT prover (usually Z3 \cite{z3}). |
|
421 |
||
38601 | 422 |
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs |
36926 | 423 |
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. |
424 |
||
425 |
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of |
|
38601 | 426 |
Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used. |
36926 | 427 |
|
38601 | 428 |
\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover |
429 |
developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of |
|
430 |
SInE runs on Geoff Sutcliffe's Miami servers. |
|
431 |
||
432 |
\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a prover |
|
433 |
developed by Stickel et al.\ \cite{snark}. The remote version of |
|
434 |
SNARK runs on Geoff Sutcliffe's Miami servers. |
|
40073 | 435 |
|
436 |
\item[$\bullet$] \textbf{\textit{remote\_smt}:} The remote version of the |
|
437 |
\textit{smt} proof method runs the SMT solver on servers at the TU M\"unchen (or |
|
438 |
wherever \texttt{REMOTE\_SMT\_URL} is set to point). |
|
439 |
||
36926 | 440 |
\end{enum} |
441 |
||
40073 | 442 |
By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and \textit{smt} in |
443 |
parallel---either locally or remotely, depending on the number of processor |
|
444 |
cores available. For historical reasons, the default value of this option can be |
|
445 |
overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu |
|
446 |
in Proof General. |
|
36926 | 447 |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
448 |
It is a good idea to run several provers in parallel, although it could slow |
40073 | 449 |
down your machine. Running E, SPASS, Vampire, and SInE-E together for 5 seconds |
450 |
yields a better success rate than running the most effective of these (Vampire) |
|
451 |
for 120 seconds \cite{boehme-nipkow-2010}. |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
452 |
|
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
453 |
\opnodefault{prover}{string} |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
454 |
Alias for \textit{provers}. |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
455 |
|
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
456 |
\opnodefault{atps}{string} |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
457 |
Legacy alias for \textit{provers}. |
36926 | 458 |
|
459 |
\opnodefault{atp}{string} |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
460 |
Legacy alias for \textit{provers}. |
36926 | 461 |
|
40343
4521d56aef63
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset
|
462 |
\opdefault{timeout}{float\_or\_none}{\upshape 30} |
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40203
diff
changeset
|
463 |
Specifies the maximum number of seconds that the automatic provers should spend |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
464 |
searching for a proof. For historical reasons, the default value of this option |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
465 |
can be overridden using the option ``Sledgehammer: Time Limit'' from the |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
466 |
``Isabelle'' menu in Proof General. |
38984 | 467 |
|
38983 | 468 |
\opfalse{blocking}{non\_blocking} |
469 |
Specifies whether the \textbf{sledgehammer} command should operate |
|
470 |
synchronously. The asynchronous (non-blocking) mode lets the user start proving |
|
471 |
the putative theorem manually while Sledgehammer looks for a proof, but it can |
|
472 |
also be more confusing. |
|
473 |
||
36926 | 474 |
\opfalse{overlord}{no\_overlord} |
475 |
Specifies whether Sledgehammer should put its temporary files in |
|
476 |
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for |
|
477 |
debugging Sledgehammer but also unsafe if several instances of the tool are run |
|
478 |
simultaneously. The files are identified by the prefix \texttt{prob\_}; you may |
|
479 |
safely remove them after Sledgehammer has run. |
|
480 |
||
481 |
\nopagebreak |
|
482 |
{\small See also \textit{debug} (\S\ref{output-format}).} |
|
483 |
\end{enum} |
|
484 |
||
485 |
\subsection{Problem Encoding} |
|
486 |
\label{problem-encoding} |
|
487 |
||
488 |
\begin{enum} |
|
489 |
\opfalse{explicit\_apply}{implicit\_apply} |
|
490 |
Specifies whether function application should be encoded as an explicit |
|
40073 | 491 |
``apply'' operator in ATP problems. If the option is set to \textit{false}, each |
492 |
function will be directly applied to as many arguments as possible. Enabling |
|
493 |
this option can sometimes help discover higher-order proofs that otherwise would |
|
494 |
not be found. |
|
36926 | 495 |
|
496 |
\opfalse{full\_types}{partial\_types} |
|
40073 | 497 |
Specifies whether full-type information is encoded in ATP problems. Enabling |
498 |
this option can prevent the discovery of type-incorrect proofs, but it also |
|
499 |
tends to slow down the ATPs significantly. For historical reasons, the default |
|
500 |
value of this option can be overridden using the option ``Sledgehammer: Full |
|
501 |
Types'' from the ``Isabelle'' menu in Proof General. |
|
38591 | 502 |
\end{enum} |
36926 | 503 |
|
38591 | 504 |
\subsection{Relevance Filter} |
505 |
\label{relevance-filter} |
|
506 |
||
507 |
\begin{enum} |
|
40343
4521d56aef63
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset
|
508 |
\opdefault{relevance\_thresholds}{float\_pair}{\upshape 0.45~0.85} |
38746 | 509 |
Specifies the thresholds above which facts are considered relevant by the |
510 |
relevance filter. The first threshold is used for the first iteration of the |
|
511 |
relevance filter and the second threshold is used for the last iteration (if it |
|
512 |
is reached). The effective threshold is quadratically interpolated for the other |
|
40343
4521d56aef63
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset
|
513 |
iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems |
4521d56aef63
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset
|
514 |
are relevant and 1 only theorems that refer to previously seen constants. |
36926 | 515 |
|
40343
4521d56aef63
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset
|
516 |
\opsmart{max\_relevant}{int\_or\_smart} |
38746 | 517 |
Specifies the maximum number of facts that may be returned by the relevance |
518 |
filter. If the option is set to \textit{smart}, it is set to a value that was |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
519 |
empirically found to be appropriate for the prover. A typical value would be |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
520 |
300. |
36926 | 521 |
\end{enum} |
522 |
||
523 |
\subsection{Output Format} |
|
524 |
\label{output-format} |
|
525 |
||
526 |
\begin{enum} |
|
527 |
||
528 |
\opfalse{verbose}{quiet} |
|
529 |
Specifies whether the \textbf{sledgehammer} command should explain what it does. |
|
530 |
||
531 |
\opfalse{debug}{no\_debug} |
|
40203 | 532 |
Specifies whether Sledgehammer should display additional debugging information |
533 |
beyond what \textit{verbose} already displays. Enabling \textit{debug} also |
|
534 |
enables \textit{verbose} behind the scenes. |
|
36926 | 535 |
|
536 |
\nopagebreak |
|
537 |
{\small See also \textit{overlord} (\S\ref{mode-of-operation}).} |
|
538 |
||
539 |
\opfalse{isar\_proof}{no\_isar\_proof} |
|
540 |
Specifies whether Isar proofs should be output in addition to one-liner |
|
541 |
\textit{metis} proofs. Isar proof construction is still experimental and often |
|
542 |
fails; however, they are usually faster and sometimes more robust than |
|
543 |
\textit{metis} proofs. |
|
544 |
||
40343
4521d56aef63
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset
|
545 |
\opdefault{isar\_shrink\_factor}{int}{\upshape 1} |
36926 | 546 |
Specifies the granularity of the Isar proof. A value of $n$ indicates that each |
547 |
Isar proof step should correspond to a group of up to $n$ consecutive proof |
|
548 |
steps in the ATP proof. |
|
549 |
||
550 |
\end{enum} |
|
551 |
||
38984 | 552 |
\subsection{Authentication} |
553 |
\label{authentication} |
|
554 |
||
555 |
\begin{enum} |
|
556 |
\opnodefault{expect}{string} |
|
557 |
Specifies the expected outcome, which must be one of the following: |
|
36926 | 558 |
|
559 |
\begin{enum} |
|
40203 | 560 |
\item[$\bullet$] \textbf{\textit{some}:} Sledgehammer found a (potentially |
561 |
unsound) proof. |
|
38984 | 562 |
\item[$\bullet$] \textbf{\textit{none}:} Sledgehammer found no proof. |
40203 | 563 |
\item[$\bullet$] \textbf{\textit{unknown}:} Sledgehammer encountered some |
564 |
problem. |
|
38984 | 565 |
\end{enum} |
566 |
||
567 |
Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning |
|
568 |
(otherwise) if the actual outcome differs from the expected outcome. This option |
|
569 |
is useful for regression testing. |
|
570 |
||
571 |
\nopagebreak |
|
572 |
{\small See also \textit{blocking} (\S\ref{mode-of-operation}).} |
|
36926 | 573 |
\end{enum} |
574 |
||
575 |
\let\em=\sl |
|
576 |
\bibliography{../manual}{} |
|
577 |
\bibliographystyle{abbrv} |
|
578 |
||
579 |
\end{document} |