author | blanchet |
Wed, 23 Jun 2010 15:06:40 +0200 | |
changeset 37517 | 19ba7ec5f1e3 |
parent 37498 | b426cbdb5a23 |
child 37582 | f329e1b99ce6 |
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) |
|
81 |
on the current goal. The supported ATPs are E \cite{schulz-2002}, SPASS |
|
82 |
\cite{weidenbach-et-al-2009}, and Vampire \cite{riazanov-voronkov-2002}, which |
|
83 |
can be run locally or remotely via the SystemOnTPTP web service |
|
84 |
\cite{sutcliffe-2000}. |
|
85 |
||
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
86 |
The problem passed to ATPs consists of your current goal together with a |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
87 |
heuristic selection of hundreds of facts (theorems) from the current theory |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
88 |
context, filtered by relevance. Because jobs are run in the background, you can |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
89 |
continue to work on your proof by other means. Provers can be run in parallel. |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
90 |
Any reply (which may arrive minutes later) will appear in the Proof General |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
91 |
response buffer. |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
92 |
|
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
93 |
The result of a successful ATP proof search is some source text that usually |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
94 |
(but not always) reconstructs the proof within Isabelle, without requiring the |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
95 |
ATPs again. The reconstructed proof relies on the general-purpose Metis prover |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
96 |
\cite{metis}, which is fully integrated into Isabelle/HOL, with explicit |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
97 |
inferences going through the kernel. Thus its results are correct by |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
98 |
construction. |
36926 | 99 |
|
100 |
\newbox\boxA |
|
101 |
\setbox\boxA=\hbox{\texttt{nospam}} |
|
102 |
||
103 |
Examples of Sledgehammer use can be found in Isabelle's |
|
104 |
\texttt{src/HOL/Metis\_Examples} directory. |
|
105 |
Comments and bug reports concerning Sledgehammer or this manual should be |
|
106 |
directed to |
|
107 |
\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak |
|
108 |
in.\allowbreak tum.\allowbreak de}. |
|
109 |
||
110 |
\vskip2.5\smallskipamount |
|
111 |
||
112 |
%\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for |
|
113 |
%suggesting several textual improvements. |
|
114 |
||
115 |
\section{Installation} |
|
116 |
\label{installation} |
|
117 |
||
118 |
Sledgehammer is part of Isabelle, so you don't need to install it. However, it |
|
119 |
relies on third-party automatic theorem provers (ATPs). Currently, E, SPASS, and |
|
120 |
Vampire are supported. All of these are available remotely via SystemOnTPTP |
|
121 |
\cite{sutcliffe-2000}, but if you want better performance you will need to |
|
122 |
install at least E and SPASS locally. |
|
123 |
||
124 |
There are three main ways to install E and SPASS: |
|
125 |
||
126 |
\begin{enum} |
|
127 |
\item[$\bullet$] If you installed an official Isabelle package with everything |
|
128 |
inside, it should already include properly setup executables for E and SPASS, |
|
129 |
ready to use. |
|
130 |
||
131 |
\item[$\bullet$] Otherwise, you can download the Isabelle-aware E and SPASS |
|
132 |
binary packages from Isabelle's download page. Extract the archives, then add a |
|
133 |
line to your \texttt{\char`\~/.isabelle/etc/components} file with the absolute path to |
|
134 |
E or SPASS. For example, if \texttt{\char`\~/.isabelle/etc/components} does not exist |
|
135 |
yet and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create |
|
136 |
the file \texttt{\char`\~/.isabelle/etc/components} with the single line |
|
137 |
||
138 |
\prew |
|
139 |
\texttt{/usr/local/spass-3.7} |
|
140 |
\postw |
|
141 |
||
142 |
\item[$\bullet$] If you prefer to build E or SPASS yourself, feel free to do so |
|
143 |
and set the environment variable \texttt{E\_HOME} or \texttt{SPASS\_HOME} to the |
|
144 |
directory that contains the \texttt{eproof} or \texttt{SPASS} executable, |
|
145 |
respectively. |
|
146 |
\end{enum} |
|
147 |
||
148 |
To check whether E and SPASS are installed, follow the example in |
|
149 |
\S\ref{first-steps}. |
|
150 |
||
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
151 |
Remote ATP invocation via the SystemOnTPTP web service requires Perl with the |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
152 |
World Wide Web Library (\texttt{libwww-perl}) installed. |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
153 |
|
36926 | 154 |
\section{First Steps} |
155 |
\label{first-steps} |
|
156 |
||
157 |
To illustrate Sledgehammer in context, let us start a theory file and |
|
158 |
attempt to prove a simple lemma: |
|
159 |
||
160 |
\prew |
|
161 |
\textbf{theory}~\textit{Scratch} \\ |
|
162 |
\textbf{imports}~\textit{Main} \\ |
|
163 |
\textbf{begin} \\[2\smallskipamount] |
|
164 |
% |
|
165 |
\textbf{lemma} ``$[a] = [b] \,\longleftrightarrow\, a = b$'' \\ |
|
166 |
\textbf{sledgehammer} |
|
167 |
\postw |
|
168 |
||
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
169 |
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
|
170 |
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
|
171 |
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
|
172 |
Either way, Sledgehammer produces the following output after a few seconds: |
36926 | 173 |
|
174 |
\prew |
|
175 |
\slshape |
|
176 |
Sledgehammer: ATP ``\textit{e}'' for subgoal 1: \\ |
|
177 |
$([a] = [b]) = (a = b)$ \\ |
|
178 |
Try this command: \textbf{by} (\textit{metis hd.simps}). \\ |
|
179 |
To minimize the number of lemmas, try this command: \\ |
|
180 |
\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount] |
|
181 |
% |
|
182 |
Sledgehammer: ATP ``\textit{spass}'' for subgoal 1: \\ |
|
183 |
$([a] = [b]) = (a = b)$ \\ |
|
184 |
Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\ |
|
185 |
To minimize the number of lemmas, try this command: \\ |
|
186 |
\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount] |
|
187 |
% |
|
188 |
Sledgehammer: ATP ``\textit{remote\_vampire}'' for subgoal 1: \\ |
|
189 |
$([a] = [b]) = (a = b)$ \\ |
|
190 |
Try this command: \textbf{by} (\textit{metis One\_nat\_def\_raw empty\_replicate} \\ |
|
191 |
\phantom{Try this command: \textbf{by} (\textit{metis~}}\textit{insert\_Nil last\_ConsL replicate\_Suc}). \\ |
|
192 |
To minimize the number of lemmas, try this command: \\ |
|
193 |
\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{remote\_vampire}] \\ |
|
194 |
\phantom{\textbf{sledgehammer}~}(\textit{One\_nat\_def\_raw empty\_replicate insert\_Nil} \\ |
|
195 |
\phantom{\textbf{sledgehammer}~(}\textit{last\_ConsL replicate\_Suc}). |
|
196 |
\postw |
|
197 |
||
198 |
Sledgehammer ran E, SPASS, and the remote version of Vampire in parallel. If E |
|
199 |
and SPASS are not installed (\S\ref{installation}), you will see references to |
|
200 |
their remote American cousins \textit{remote\_e} and \textit{remote\_spass} |
|
201 |
instead of \textit{e} and \textit{spass}. |
|
202 |
||
203 |
Based on each ATP proof, Sledgehammer gives a one-liner proof that uses the |
|
204 |
\textit{metis} method. You can click them and insert them into the theory text. |
|
205 |
You can click the ``\textbf{sledgehammer} \textit{minimize}'' command if you |
|
206 |
want to look for a shorter (and faster) proof. But here the proof found by E |
|
207 |
looks perfect, so click it to finish the proof. |
|
208 |
||
209 |
You can ask Sledgehammer for an Isar text proof by passing the |
|
210 |
\textit{isar\_proof} option: |
|
211 |
||
212 |
\prew |
|
213 |
\textbf{sledgehammer} [\textit{isar\_proof}] |
|
214 |
\postw |
|
215 |
||
216 |
When Isar proof construction is successful, it can yield proofs that are more |
|
217 |
readable and also faster than the \textit{metis} one-liners. This feature is |
|
218 |
experimental. |
|
219 |
||
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
220 |
\section{Hints} |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
221 |
\label{hints} |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
222 |
|
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
223 |
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
|
224 |
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
|
225 |
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
|
226 |
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
|
227 |
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
|
228 |
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
|
229 |
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
|
230 |
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
|
231 |
|
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
232 |
Note that problems can be easy for auto and difficult for ATPs, but the reverse |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
233 |
is also true, so don't be discouraged if your first attempts fail. Because the |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
234 |
system refers to all theorems known to Isabelle, it is particularly suitable |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
235 |
when your goal has a short proof from lemmas that you don't know about. |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
236 |
|
36926 | 237 |
\section{Command Syntax} |
238 |
\label{command-syntax} |
|
239 |
||
240 |
Sledgehammer can be invoked at any point when there is an open goal by entering |
|
241 |
the \textbf{sledgehammer} command in the theory file. Its general syntax is as |
|
242 |
follows: |
|
243 |
||
244 |
\prew |
|
245 |
\textbf{sledgehammer} \textit{subcommand\/$^?$ options\/$^?$ facts\_override\/$^?$ num\/$^?$} |
|
246 |
\postw |
|
247 |
||
248 |
For convenience, Sledgehammer is also available in the ``Commands'' submenu of |
|
249 |
the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c |
|
250 |
C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with |
|
251 |
no arguments in the theory text. |
|
252 |
||
253 |
In the general syntax, the \textit{subcommand} may be any of the following: |
|
254 |
||
255 |
\begin{enum} |
|
256 |
\item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on subgoal number |
|
257 |
\textit{num} (1 by default), with the given options and facts. |
|
258 |
||
259 |
\item[$\bullet$] \textbf{\textit{minimize}:} Attempts to minimize the provided facts |
|
260 |
(specified in the \textit{facts\_override} argument) to obtain a simpler proof |
|
261 |
involving fewer facts. The options and goal number are as for \textit{run}. |
|
262 |
||
263 |
\item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued by |
|
264 |
Sledgehammer. This allows you to examine results that might have been lost due |
|
265 |
to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a |
|
266 |
limit on the number of messages to display (5 by default). |
|
267 |
||
268 |
\item[$\bullet$] \textbf{\textit{available\_atps}:} Prints the list of installed ATPs. |
|
269 |
See \S\ref{installation} and \S\ref{mode-of-operation} for more information on |
|
270 |
how to install ATPs. |
|
271 |
||
272 |
\item[$\bullet$] \textbf{\textit{running\_atps}:} Prints information about currently |
|
273 |
running ATPs, including elapsed runtime and remaining time until timeout. |
|
274 |
||
275 |
\item[$\bullet$] \textbf{\textit{kill\_atps}:} Terminates all running ATPs. |
|
276 |
||
277 |
\item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote |
|
278 |
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}. |
|
279 |
\end{enum} |
|
280 |
||
281 |
Sledgehammer's behavior can be influenced by various \textit{options}, which can |
|
282 |
be specified in brackets after the \textbf{sledgehammer} command. The |
|
283 |
\textit{options} are a list of key--value pairs of the form ``[$k_1 = v_1, |
|
284 |
\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true}'' is optional. For |
|
285 |
example: |
|
286 |
||
287 |
\prew |
|
288 |
\textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120$\,s$] |
|
289 |
\postw |
|
290 |
||
291 |
Default values can be set using \textbf{sledgehammer\_\allowbreak params}: |
|
292 |
||
293 |
\prew |
|
294 |
\textbf{sledgehammer\_params} \textit{options} |
|
295 |
\postw |
|
296 |
||
297 |
The supported options are described in \S\ref{option-reference}. |
|
298 |
||
299 |
The \textit{facts\_override} argument lets you alter the set of facts that go |
|
300 |
through the relevance filter. It may be of the form ``(\textit{facts})'', where |
|
301 |
\textit{facts} is a space-separated list of Isabelle facts (theorems, local |
|
302 |
assumptions, etc.), in which case the relevance filter is bypassed and the given |
|
303 |
facts are used. It may also be of the form (\textit{add}:\ \textit{facts}$_1$), |
|
304 |
(\textit{del}:\ \textit{facts}$_2$), or (\textit{add}:\ \textit{facts}$_1$\ |
|
305 |
\textit{del}:\ \textit{facts}$_2$), where the relevance filter is instructed to |
|
306 |
proceed as usual except that it should consider \textit{facts}$_1$ |
|
307 |
highly-relevant and \textit{facts}$_2$ fully irrelevant. |
|
308 |
||
309 |
\section{Option Reference} |
|
310 |
\label{option-reference} |
|
311 |
||
312 |
\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}} |
|
313 |
\def\qty#1{$\left<\textit{#1}\right>$} |
|
314 |
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$} |
|
315 |
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} |
|
316 |
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} |
|
317 |
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} |
|
318 |
\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} |
|
319 |
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]} |
|
320 |
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]} |
|
321 |
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]} |
|
322 |
\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} |
|
323 |
\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} |
|
324 |
||
325 |
Sledgehammer's options are categorized as follows:\ mode of operation |
|
326 |
(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), output |
|
327 |
format (\S\ref{output-format}), and timeouts (\S\ref{timeouts}). |
|
328 |
||
329 |
The descriptions below refer to the following syntactic quantities: |
|
330 |
||
331 |
\begin{enum} |
|
332 |
\item[$\bullet$] \qtybf{string}: A string. |
|
333 |
\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}. |
|
334 |
\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}. |
|
335 |
\item[$\bullet$] \qtybf{int\/}: An integer. |
|
336 |
\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms} |
|
337 |
(milliseconds), or the keyword \textit{none} ($\infty$ years). |
|
338 |
\end{enum} |
|
339 |
||
340 |
Default values are indicated in square brackets. Boolean options have a negated |
|
341 |
counterpart (e.g., \textit{debug} vs.\ \textit{no\_debug}). When setting |
|
342 |
Boolean options, ``= \textit{true}'' may be omitted. |
|
343 |
||
344 |
\subsection{Mode of Operation} |
|
345 |
\label{mode-of-operation} |
|
346 |
||
347 |
\begin{enum} |
|
348 |
%\optrue{blocking}{non\_blocking} |
|
349 |
%Specifies whether the \textbf{sledgehammer} command should operate synchronously. |
|
350 |
%The asynchronous (non-blocking) mode lets the user start proving the putative |
|
351 |
%theorem while Sledgehammer looks for a counterexample, but it can also be more |
|
352 |
%confusing. For technical reasons, automatic runs currently always block. |
|
353 |
||
354 |
\opnodefault{atps}{string} |
|
355 |
Specifies the ATPs (automated theorem provers) to use as a space-separated list |
|
356 |
(e.g., ``\textit{e}~\textit{spass}''). The following ATPs are supported: |
|
357 |
||
358 |
\begin{enum} |
|
359 |
\item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz |
|
360 |
\cite{schulz-2002}. To use E, set the environment variable |
|
361 |
\texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable, |
|
362 |
or install the prebuilt E package from Isabelle's download page. See |
|
363 |
\S\ref{installation} for details. |
|
364 |
||
365 |
\item[$\bullet$] \textbf{\textit{spass}:} SPASS is an ATP developed by Christoph |
|
366 |
Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the |
|
367 |
environment variable \texttt{SPASS\_HOME} to the directory that contains the |
|
368 |
\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
|
369 |
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
|
370 |
\S\ref{installation} for details. |
36926 | 371 |
|
372 |
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by |
|
373 |
Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use |
|
374 |
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory |
|
375 |
that contains the \texttt{vampire} executable. |
|
376 |
||
377 |
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E executes |
|
378 |
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. |
|
379 |
||
380 |
\item[$\bullet$] \textbf{\textit{remote\_spass}:} The remote version of SPASS |
|
381 |
executes on Geoff Sutcliffe's Miami servers. |
|
382 |
||
383 |
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of |
|
384 |
Vampire executes on Geoff Sutcliffe's Miami servers. Version 9 is used. |
|
385 |
||
386 |
\end{enum} |
|
387 |
||
388 |
By default, Sledgehammer will run E, SPASS, and Vampire in parallel. For E and |
|
389 |
SPASS, it will use any locally installed version if available, falling back |
|
390 |
on the remote versions if necessary. For historical reasons, the default value |
|
391 |
of this option can be overridden using the option ``Sledgehammer: ATPs'' from |
|
392 |
the ``Isabelle'' menu in Proof General. |
|
393 |
||
394 |
It is a good idea to run several ATPs in parallel, although it could slow down |
|
395 |
your machine. Tobias Nipkow observed that running E, SPASS, and Vampire together |
|
396 |
for 5 seconds yields the same success rate as running the most effective of |
|
397 |
these (Vampire) for 120 seconds \cite{boehme-nipkow-2010}. |
|
398 |
||
399 |
\opnodefault{atp}{string} |
|
400 |
Alias for \textit{atps}. |
|
401 |
||
402 |
\opfalse{overlord}{no\_overlord} |
|
403 |
Specifies whether Sledgehammer should put its temporary files in |
|
404 |
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for |
|
405 |
debugging Sledgehammer but also unsafe if several instances of the tool are run |
|
406 |
simultaneously. The files are identified by the prefix \texttt{prob\_}; you may |
|
407 |
safely remove them after Sledgehammer has run. |
|
408 |
||
409 |
\nopagebreak |
|
410 |
{\small See also \textit{debug} (\S\ref{output-format}).} |
|
411 |
\end{enum} |
|
412 |
||
413 |
\subsection{Problem Encoding} |
|
414 |
\label{problem-encoding} |
|
415 |
||
416 |
\begin{enum} |
|
417 |
\opfalse{explicit\_apply}{implicit\_apply} |
|
418 |
Specifies whether function application should be encoded as an explicit |
|
419 |
``apply'' operator. If the option is set to \textit{false}, each function will |
|
420 |
be directly applied to as many arguments as possible. Enabling this option can |
|
421 |
sometimes help discover higher-order proofs that otherwise would not be found. |
|
422 |
||
423 |
\opfalse{full\_types}{partial\_types} |
|
424 |
Specifies whether full-type information is exported. Enabling this option can |
|
425 |
prevent the discovery of type-incorrect proofs, but it also tends to slow down |
|
426 |
the ATPs significantly. For historical reasons, the default value of this option |
|
427 |
can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle'' |
|
428 |
menu in Proof General. |
|
429 |
||
430 |
\opdefault{relevance\_threshold}{int}{50} |
|
431 |
Specifies the threshold above which facts are considered relevant by the |
|
432 |
relevance filter. The option ranges from 0 to 100, where 0 means that all |
|
433 |
theorems are relevant. |
|
434 |
||
435 |
\opdefault{relevance\_convergence}{int}{320} |
|
436 |
Specifies the convergence quotient, multiplied by 100, used by the relevance |
|
437 |
filter. This quotient is used by the relevance filter to scale down the |
|
438 |
relevance of facts at each iteration of the filter. |
|
439 |
||
440 |
\opsmartx{theory\_relevant}{theory\_irrelevant} |
|
441 |
Specifies whether the theory from which a fact comes should be taken into |
|
442 |
consideration by the relevance filter. If the option is set to \textit{smart}, |
|
443 |
it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire, |
|
444 |
because empirical results suggest that these are the best settings. |
|
445 |
||
446 |
\opfalse{defs\_relevant}{defs\_irrelevant} |
|
447 |
Specifies whether the definition of constants occurring in the formula to prove |
|
448 |
should be considered particularly relevant. Enabling this option tends to lead |
|
449 |
to larger problems and typically slows down the ATPs. |
|
450 |
||
451 |
\optrue{respect\_no\_atp}{ignore\_no\_atp} |
|
452 |
Specifies whether Sledgehammer should honor the \textit{no\_atp} attributes. The |
|
453 |
\textit{no\_atp} attributes marks theorems that tend to confuse ATPs, typically |
|
454 |
because they can lead to unsound ATP proofs \cite{boehme-nipkow-2010}. It is |
|
455 |
normally a good idea to leave this option enabled, unless you are debugging |
|
456 |
Sledgehammer. |
|
457 |
||
458 |
\end{enum} |
|
459 |
||
460 |
\subsection{Output Format} |
|
461 |
\label{output-format} |
|
462 |
||
463 |
\begin{enum} |
|
464 |
||
465 |
\opfalse{verbose}{quiet} |
|
466 |
Specifies whether the \textbf{sledgehammer} command should explain what it does. |
|
467 |
||
468 |
\opfalse{debug}{no\_debug} |
|
469 |
Specifies whether Nitpick should display additional debugging information beyond |
|
470 |
what \textit{verbose} already displays. Enabling \textit{debug} also enables |
|
471 |
\textit{verbose} behind the scenes. |
|
472 |
||
473 |
\nopagebreak |
|
474 |
{\small See also \textit{overlord} (\S\ref{mode-of-operation}).} |
|
475 |
||
476 |
\opfalse{isar\_proof}{no\_isar\_proof} |
|
477 |
Specifies whether Isar proofs should be output in addition to one-liner |
|
478 |
\textit{metis} proofs. Isar proof construction is still experimental and often |
|
479 |
fails; however, they are usually faster and sometimes more robust than |
|
480 |
\textit{metis} proofs. |
|
481 |
||
482 |
\opdefault{isar\_shrink\_factor}{int}{1} |
|
483 |
Specifies the granularity of the Isar proof. A value of $n$ indicates that each |
|
484 |
Isar proof step should correspond to a group of up to $n$ consecutive proof |
|
485 |
steps in the ATP proof. |
|
486 |
||
487 |
\end{enum} |
|
488 |
||
489 |
\subsection{Timeouts} |
|
490 |
\label{timeouts} |
|
491 |
||
492 |
\begin{enum} |
|
493 |
\opdefault{timeout}{time}{$\mathbf{60}$ s} |
|
494 |
Specifies the maximum amount of time that the ATPs should spend looking for a |
|
495 |
proof. For historical reasons, the default value of this option can be |
|
496 |
overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle'' |
|
497 |
menu in Proof General. |
|
498 |
||
499 |
\opdefault{minimize\_timeout}{time}{$\mathbf{5}$\,s} |
|
500 |
Specifies the maximum amount of time that the ATPs should spend looking for a |
|
501 |
proof for \textbf{sledgehammer}~\textit{minimize}. |
|
502 |
\end{enum} |
|
503 |
||
504 |
\let\em=\sl |
|
505 |
\bibliography{../manual}{} |
|
506 |
\bibliographystyle{abbrv} |
|
507 |
||
508 |
\end{document} |