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