1 \documentclass[a4paper,12pt]{article}
2 \usepackage[T1]{fontenc}
5 \usepackage[english,french]{babel}
12 %\usepackage[scaled=.85]{beramono}
13 \usepackage{../../lib/texinputs/isabelle,../iman,../pdfsetup}
15 \newcommand\download{\url{http://www21.in.tum.de/~blanchet/\#software}}
17 \def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}}
18 \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$}
20 \newcommand\const[1]{\textsf{#1}}
23 %\evensidemargin=4.6mm
30 \def\Colon{\mathord{:\mkern-1.5mu:}}
31 %\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
32 %\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
33 \def\lparr{\mathopen{(\mkern-4mu\mid}}
34 \def\rparr{\mathclose{\mid\mkern-4mu)}}
37 \def\undef{(\lambda x.\; \unk)}
38 %\def\unr{\textit{others}}
40 \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
41 \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
48 %\renewcommand\labelitemi{$\bullet$}
49 \renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}
51 \selectlanguage{english}
53 \title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
54 Hammering Away \\[\smallskipamount]
55 \Large A User's Guide to Sledgehammer for Isabelle/HOL}
57 Jasmin Christian Blanchette \\
58 {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount]
59 {\normalsize with contributions from} \\[4\smallskipamount]
60 Lawrence C. Paulson \\
61 {\normalsize Computer Laboratory, University of Cambridge} \\
68 \setlength{\parskip}{.7em plus .2em minus .1em}
69 \setlength{\parindent}{0pt}
70 \setlength{\abovedisplayskip}{\parskip}
71 \setlength{\abovedisplayshortskip}{.9\parskip}
72 \setlength{\belowdisplayskip}{\parskip}
73 \setlength{\belowdisplayshortskip}{.9\parskip}
75 % General-purpose enum environment with correct spacing
76 \newenvironment{enum}%
78 \setlength{\topsep}{.1\parskip}%
79 \setlength{\partopsep}{.1\parskip}%
80 \setlength{\itemsep}{\parskip}%
81 \advance\itemsep by-\parsep}}
84 \def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
85 \advance\rightskip by\leftmargin}
86 \def\post{\vskip0pt plus1ex\endgroup}
88 \def\prew{\pre\advance\rightskip by-\leftmargin}
91 \section{Introduction}
94 Sledgehammer is a tool that applies automatic theorem provers (ATPs)
95 and satisfiability-modulo-theories (SMT) solvers on the current goal.%
96 \footnote{The distinction between ATPs and SMT solvers is convenient but mostly
97 historical. The two communities are converging, with more and more ATPs
98 supporting typical SMT features such as arithmetic and sorts, and a few SMT
99 solvers parsing ATP syntaxes. There is also a strong technological connection
100 between instantiation-based ATPs (such as iProver and iProver-Eq) and SMT
103 The supported ATPs are E \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF
104 \cite{tofof}, iProver \cite{korovin-2009}, iProver-Eq
105 \cite{korovin-sticksel-2010}, LEO-II \cite{leo2}, Satallax \cite{satallax},
106 SNARK \cite{snark}, SPASS \cite{weidenbach-et-al-2009}, Vampire
107 \cite{riazanov-voronkov-2002}, and Waldmeister \cite{waldmeister}. The ATPs are
108 run either locally or remotely via the System\-On\-TPTP web service
109 \cite{sutcliffe-2000}. In addition to the ATPs, the SMT solvers Z3 \cite{z3} is
110 used by default, and you can tell Sledgehammer to try Alt-Ergo \cite{alt-ergo},
111 CVC3 \cite{cvc3}, and Yices \cite{yices} as well; these are run either locally
112 or (for CVC3 and Z3) on a server at the TU M\"unchen.
114 The problem passed to the automatic provers consists of your current goal
115 together with a heuristic selection of hundreds of facts (theorems) from the
116 current theory context, filtered by relevance. Because jobs are run in the
117 background, you can continue to work on your proof by other means. Provers can
118 be run in parallel. Any reply (which may arrive half a minute later) will appear
119 in the Proof General response buffer.
121 The result of a successful proof search is some source text that usually (but
122 not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
123 proof relies on the general-purpose \textit{metis} proof method, which
124 integrates the Metis ATP in Isabelle/HOL with explicit inferences going through
125 the kernel. Thus its results are correct by construction.
127 In this manual, we will explicitly invoke the \textbf{sledgehammer} command.
128 Sledgehammer also provides an automatic mode that can be enabled via the ``Auto
129 Sledgehammer'' option in Proof General's ``Isabelle'' menu. In this mode,
130 Sledgehammer is run on every newly entered theorem. The time limit for Auto
131 Sledgehammer and other automatic tools can be set using the ``Auto Tools Time
135 \setbox\boxA=\hbox{\texttt{NOSPAM}}
137 \newcommand\authoremail{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
138 in.\allowbreak tum.\allowbreak de}}
140 To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is
141 imported---this is rarely a problem in practice since it is part of
142 \textit{Main}. Examples of Sledgehammer use can be found in Isabelle's
143 \texttt{src/HOL/Metis\_Examples} directory.
144 Comments and bug reports concerning Sledgehammer or this manual should be
145 directed to the author at \authoremail.
147 \vskip2.5\smallskipamount
149 %\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
150 %suggesting several textual improvements.
152 \section{Installation}
155 Sledgehammer is part of Isabelle, so you don't need to install it. However, it
156 relies on third-party automatic provers (ATPs and SMT solvers).
158 Among the ATPs, E, LEO-II, Satallax, SPASS, and Vampire can be run locally; in
159 addition, E, E-SInE, E-ToFoF, iProver, iProver-Eq, LEO-II, Satallax, SNARK,
160 Vampire, and Waldmeister are available remotely via System\-On\-TPTP
161 \cite{sutcliffe-2000}. If you want better performance, you should at least
162 install E and SPASS locally.
164 Among the SMT solvers, Alt-Ergo, CVC3, Yices, and Z3 can be run locally, and
165 CVC3 and Z3 can be run remotely on a TU M\"unchen server. If you want better
166 performance and get the ability to replay proofs that rely on the \emph{smt}
167 proof method without an Internet connection, you should at least install Z3
170 There are three main ways to install automatic provers on your machine:
174 \item[\labelitemi] If you installed an official Isabelle package, it should
175 already include properly setup executables for CVC3, E, SPASS, and Z3, ready to use.%
176 \footnote{Vampire's and Yices's licenses prevent us from doing the same for
177 these otherwise remarkable tools.}
178 For Z3, you must additionally set the variable
179 \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
180 noncommercial user, either in the environment in which Isabelle is
182 \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file.
184 \item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, E,
185 SPASS, and Z3 binary packages from \download. Extract the archives, then add a
186 line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}%
187 \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
188 startup. Its value can be retrieved by executing \texttt{isabelle}
189 \texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
190 file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the
191 \texttt{components} file does not exist yet and you extracted SPASS to
192 \texttt{/usr/local/spass-3.8ds}, create it with the single line
195 \texttt{/usr/local/spass-3.8ds}
200 \item[\labelitemi] If you prefer to build E, LEO-II, Satallax, or SPASS
201 manually, or found a Vampire executable somewhere (e.g.,
202 \url{http://www.vprover.org/}), set the environment variable \texttt{E\_HOME},
203 \texttt{LEO2\_HOME}, \texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or
204 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
205 \texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable.
206 Sledgehammer has been tested with E 1.0 to 1.4, LEO-II 1.3.4, Satallax 2.2, 2.3,
207 and 2.4, SPASS 3.8ds, and Vampire 0.6, 1.0, and 1.8.%
208 \footnote{Following the rewrite of Vampire, the counter for version numbers was
209 reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent
211 Since the ATPs' output formats are neither documented nor stable, other
212 versions might not work well with Sledgehammer. Ideally,
213 you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
214 \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
215 \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.4'').
217 Similarly, if you want to build Alt-Ergo or CVC3, or found a
218 Yices or Z3 executable somewhere (e.g.,
219 \url{http://yices.csl.sri.com/download.shtml} or
220 \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html}),
221 set the environment variable \texttt{CVC3\_\allowbreak SOLVER},
222 \texttt{YICES\_SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of
223 the executable, \emph{including the file name}. Sledgehammer has been tested
224 with Alt-Ergo 0.93, CVC3 2.2 and 2.4.1, Yices 1.0.28 and 1.0.33, and Z3 3.0,
225 3.1, 3.2, and 4.0. Since the SMT solvers' output formats are somewhat unstable,
226 other versions of the solvers might not work well with Sledgehammer. Ideally,
227 also set \texttt{CVC3\_VERSION}, \texttt{YICES\_VERSION}, or
228 \texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.0'').
232 To check whether E, SPASS, Vampire, and/or Z3 are successfully installed, try
233 out the example in \S\ref{first-steps}. If the remote versions of any of these
234 provers is used (identified by the prefix ``\emph{remote\_\/}''), or if the
235 local versions fail to solve the easy goal presented there, something must be
236 wrong with the installation.
238 Remote prover invocation requires Perl with the World Wide Web Library
239 (\texttt{libwww-perl}) installed. If you must use a proxy server to access the
240 Internet, set the \texttt{http\_proxy} environment variable to the proxy, either
241 in the environment in which Isabelle is launched or in your
242 \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few
246 \texttt{http\_proxy=http://proxy.example.org} \\
247 \texttt{http\_proxy=http://proxy.example.org:8080} \\
248 \texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org}
251 \section{First Steps}
254 To illustrate Sledgehammer in context, let us start a theory file and
255 attempt to prove a simple lemma:
258 \textbf{theory}~\textit{Scratch} \\
259 \textbf{imports}~\textit{Main} \\
260 \textbf{begin} \\[2\smallskipamount]
262 \textbf{lemma} ``$[a] = [b] \,\Longrightarrow\, a = b$'' \\
263 \textbf{sledgehammer}
266 Instead of issuing the \textbf{sledgehammer} command, you can also find
267 Sledgehammer in the ``Commands'' submenu of the ``Isabelle'' menu in Proof
268 General or press the Emacs key sequence C-c C-a C-s.
269 Either way, Sledgehammer produces the following output after a few seconds:
273 Sledgehammer: ``\textit{e\/}'' on goal \\
274 $[a] = [b] \,\Longrightarrow\, a = b$ \\
275 Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]
277 Sledgehammer: ``\textit{z3\/}'' on goal \\
278 $[a] = [b] \,\Longrightarrow\, a = b$ \\
279 Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount]
281 Sledgehammer: ``\textit{vampire\/}'' on goal \\
282 $[a] = [b] \,\Longrightarrow\, a = b$ \\
283 Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
285 Sledgehammer: ``\textit{spass\/}'' on goal \\
286 $[a] = [b] \,\Longrightarrow\, a = b$ \\
287 Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
289 Sledgehammer: ``\textit{remote\_waldmeister\/}'' on goal \\
290 $[a] = [b] \,\Longrightarrow\, a = b$ \\
291 Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
293 Sledgehammer: ``\textit{remote\_e\_sine\/}'' on goal \\
294 $[a] = [b] \,\Longrightarrow\, a = b$ \\
295 Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms).
298 Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel.
299 Depending on which provers are installed and how many processor cores are
300 available, some of the provers might be missing or present with a
301 \textit{remote\_} prefix. Waldmeister is run only for unit equational problems,
302 where the goal's conclusion is a (universally quantified) equation.
304 For each successful prover, Sledgehammer gives a one-liner proof that uses
305 the \textit{metis} or \textit{smt} proof method. Approximate timings are shown
306 in parentheses, indicating how fast the call is. You can click the proof to
307 insert it into the theory text.
309 In addition, you can ask Sledgehammer for an Isar text proof by passing the
310 \textit{isar\_proof} option (\S\ref{output-format}):
313 \textbf{sledgehammer} [\textit{isar\_proof}]
316 When Isar proof construction is successful, it can yield proofs that are more
317 readable and also faster than the \textit{metis} or \textit{smt} one-liners.
318 This feature is experimental and is only available for ATPs.
323 This section presents a few hints that should help you get the most out of
324 Sledgehammer. Frequently asked questions are answered in
325 \S\ref{frequently-asked-questions}.
327 %\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak}
328 \newcommand\point[1]{\subsection{\emph{#1}}}
330 \point{Presimplify the goal}
332 For best results, first simplify your problem by calling \textit{auto} or at
333 least \textit{safe} followed by \textit{simp\_all}. The SMT solvers provide
334 arithmetic decision procedures, but the ATPs typically do not (or if they do,
335 Sledgehammer does not use it yet). Apart from Waldmeister, they are not
336 especially good at heavy rewriting, but because they regard equations as
337 undirected, they often prove theorems that require the reverse orientation of a
338 \textit{simp} rule. Higher-order problems can be tackled, but the success rate
339 is better for first-order problems. Hence, you may get better results if you
340 first simplify the problem to remove higher-order features.
342 \point{Make sure E, SPASS, Vampire, and Z3 are locally installed}
344 Locally installed provers are faster and more reliable than those running on
345 servers. See \S\ref{installation} for details on how to install them.
347 \point{Familiarize yourself with the most important options}
349 Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of
350 the options are very specialized, but serious users of the tool should at least
351 familiarize themselves with the following options:
354 \item[\labelitemi] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies
355 the automatic provers (ATPs and SMT solvers) that should be run whenever
356 Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass
357 remote\_vampire\/}''). For convenience, you can omit ``\textit{provers}~=''
358 and simply write the prover names as a space-separated list (e.g., ``\textit{e
359 spass remote\_vampire\/}'').
361 \item[\labelitemi] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
362 specifies the maximum number of facts that should be passed to the provers. By
363 default, the value is prover-dependent but varies between about 150 and 1000. If
364 the provers time out, you can try lowering this value to, say, 100 or 50 and see
367 \item[\labelitemi] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies
368 that Isar proofs should be generated, instead of one-liner \textit{metis} or
369 \textit{smt} proofs. The length of the Isar proofs can be controlled by setting
370 \textit{isar\_shrink\_factor} (\S\ref{output-format}).
372 \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
373 provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
374 asynchronously you should not hesitate to raise this limit to 60 or 120 seconds
375 if you are the kind of user who can think clearly while ATPs are active.
378 Options can be set globally using \textbf{sledgehammer\_params}
379 (\S\ref{command-syntax}). The command also prints the list of all available
380 options with their current value. Fact selection can be influenced by specifying
381 ``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} call
382 to ensure that certain facts are included, or simply ``$(\textit{my\_facts})$''
383 to force Sledgehammer to run only with $\textit{my\_facts}$.
385 \section{Frequently Asked Questions}
386 \label{frequently-asked-questions}
388 This sections answers frequently (and infrequently) asked questions about
389 Sledgehammer. It is a good idea to skim over it now even if you don't have any
390 questions at this stage. And if you have any further questions not listed here,
391 send them to the author at \authoremail.
393 \point{Which facts are passed to the automatic provers?}
395 The relevance filter assigns a score to every available fact (lemma, theorem,
396 definition, or axiom) based upon how many constants that fact shares with the
397 conjecture. This process iterates to include facts relevant to those just
398 accepted, but with a decay factor to ensure termination. The constants are
399 weighted to give unusual ones greater significance. The relevance filter copes
400 best when the conjecture contains some unusual constants; if all the constants
401 are common, it is unable to discriminate among the hundreds of facts that are
402 picked up. The relevance filter is also memoryless: It has no information about
403 how many times a particular fact has been used in a proof, and it cannot learn.
405 The number of facts included in a problem varies from prover to prover, since
406 some provers get overwhelmed more easily than others. You can show the number of
407 facts given using the \textit{verbose} option (\S\ref{output-format}) and the
408 actual facts using \textit{debug} (\S\ref{output-format}).
410 Sledgehammer is good at finding short proofs combining a handful of existing
411 lemmas. If you are looking for longer proofs, you must typically restrict the
412 number of facts, by setting the \textit{max\_relevant} option
413 (\S\ref{relevance-filter}) to, say, 25 or 50.
415 You can also influence which facts are actually selected in a number of ways. If
416 you simply want to ensure that a fact is included, you can specify it using the
417 ``$(\textit{add}{:}~\textit{my\_facts})$'' syntax. For example:
420 \textbf{sledgehammer} (\textit{add}: \textit{hd.simps} \textit{tl.simps})
423 The specified facts then replace the least relevant facts that would otherwise be
424 included; the other selected facts remain the same.
425 If you want to direct the selection in a particular direction, you can specify
426 the facts via \textbf{using}:
429 \textbf{using} \textit{hd.simps} \textit{tl.simps} \\
430 \textbf{sledgehammer}
433 The facts are then more likely to be selected than otherwise, and if they are
434 selected at iteration $j$ they also influence which facts are selected at
435 iterations $j + 1$, $j + 2$, etc. To give them even more weight, try
438 \textbf{using} \textit{hd.simps} \textit{tl.simps} \\
439 \textbf{apply}~\textbf{--} \\
440 \textbf{sledgehammer}
443 \point{Why does Metis fail to reconstruct the proof?}
445 There are many reasons. If Metis runs seemingly forever, that is a sign that the
446 proof is too difficult for it. Metis's search is complete, so it should
447 eventually find it, but that's little consolation. There are several possible
451 \item[\labelitemi] Try the \textit{isar\_proof} option (\S\ref{output-format}) to
452 obtain a step-by-step Isar proof where each step is justified by \textit{metis}.
453 Since the steps are fairly small, \textit{metis} is more likely to be able to
456 \item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}. It
457 is usually stronger, but you need to either have Z3 available to replay the
458 proofs, trust the SMT solver, or use certificates. See the documentation in the
459 \emph{SMT} theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}) for details.
461 \item[\labelitemi] Try the \textit{blast} or \textit{auto} proof methods, passing
462 the necessary facts via \textbf{unfolding}, \textbf{using}, \textit{intro}{:},
463 \textit{elim}{:}, \textit{dest}{:}, or \textit{simp}{:}, as appropriate.
466 In some rare cases, \textit{metis} fails fairly quickly, and you get the error
471 One-line proof reconstruction failed.
474 This message indicates that Sledgehammer determined that the goal is provable,
475 but the proof is, for technical reasons, beyond \textit{metis}'s power. You can
476 then try again with the \textit{strict} option (\S\ref{problem-encoding}).
478 If the goal is actually unprovable and you did not specify an unsound encoding
479 using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are
480 strongly encouraged to report this to the author at \authoremail.
482 \point{Why are the generated Isar proofs so ugly/broken?}
484 The current implementation of the Isar proof feature,
485 enabled by the \textit{isar\_proof} option (\S\ref{output-format}),
486 is highly experimental. Work on a new implementation has begun. There is a large body of
487 research into transforming resolution proofs into natural deduction proofs (such
488 as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
489 set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
490 value or to try several provers and keep the nicest-looking proof.
492 \point{How can I tell whether a suggested proof is sound?}
494 Earlier versions of Sledgehammer often suggested unsound proofs---either proofs
495 of nontheorems or simply proofs that rely on type-unsound inferences. This
496 is a thing of the past, unless you explicitly specify an unsound encoding
497 using \textit{type\_enc} (\S\ref{problem-encoding}).
499 Officially, the only form of ``unsoundness'' that lurks in the sound
500 encodings is related to missing characteristic theorems of datatypes. For
504 \textbf{lemma}~``$\exists \mathit{xs}.\; \mathit{xs} \neq []$'' \\
505 \textbf{sledgehammer} ()
508 suggests an argumentless \textit{metis} call that fails. However, the conjecture
509 does actually hold, and the \textit{metis} call can be repaired by adding
510 \textit{list.distinct}.
512 We hope to address this problem in a future version of Isabelle. In the
513 meantime, you can avoid it by passing the \textit{strict} option
514 (\S\ref{problem-encoding}).
516 \point{What are the \textit{full\_types}, \textit{no\_types}, and
517 \textit{mono\_tags} arguments to Metis?}
519 The \textit{metis}~(\textit{full\_types}) proof method
520 and its cousin \textit{metis}~(\textit{mono\_tags}) are fully-typed
521 version of Metis. It is somewhat slower than \textit{metis}, but the proof
522 search is fully typed, and it also includes more powerful rules such as the
523 axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in
524 higher-order places (e.g., in set comprehensions). The method kicks in
525 automatically as a fallback when \textit{metis} fails, and it is sometimes
526 generated by Sledgehammer instead of \textit{metis} if the proof obviously
527 requires type information or if \textit{metis} failed when Sledgehammer
528 preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with
529 various options for up to 3 seconds each time to ensure that the generated
530 one-line proofs actually work and to display timing information. This can be
531 configured using the \textit{preplay\_timeout} and \textit{dont\_preplay}
532 options (\S\ref{timeouts}).)
534 At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})
535 uses no type information at all during the proof search, which is more efficient
536 but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally
537 generated by Sledgehammer.
539 See the \textit{type\_enc} option (\S\ref{problem-encoding}) for details.
541 Incidentally, if you ever see warnings such as
545 Metis: Falling back on ``\textit{metis} (\textit{full\_types})''.
548 for a successful \textit{metis} proof, you can advantageously pass the
549 \textit{full\_types} option to \textit{metis} directly.
551 \point{And what are the \textit{lifting} and \textit{hide\_lams} arguments
554 Orthogonally to the encoding of types, it is important to choose an appropriate
555 translation of $\lambda$-abstractions. Metis supports three translation schemes,
556 in decreasing order of power: Curry combinators (the default),
557 $\lambda$-lifting, and a ``hiding'' scheme that disables all reasoning under
558 $\lambda$-abstractions. The more powerful schemes also give the automatic
559 provers more rope to hang themselves. See the \textit{lam\_trans} option (\S\ref{problem-encoding}) for details.
561 \point{Are generated proofs minimal?}
563 Automatic provers frequently use many more facts than are necessary.
564 Sledgehammer inclues a minimization tool that takes a set of facts returned by a
565 given prover and repeatedly calls the same prover, \textit{metis}, or
566 \textit{smt} with subsets of those axioms in order to find a minimal set.
567 Reducing the number of axioms typically improves Metis's speed and success rate,
568 while also removing superfluous clutter from the proof scripts.
570 In earlier versions of Sledgehammer, generated proofs were systematically
571 accompanied by a suggestion to invoke the minimization tool. This step is now
572 performed implicitly if it can be done in a reasonable amount of time (something
573 that can be guessed from the number of facts in the original proof and the time
574 it took to find or preplay it).
576 In addition, some provers (e.g., Yices) do not provide proofs or sometimes
577 produce incomplete proofs. The minimizer is then invoked to find out which facts
578 are actually needed from the (large) set of facts that was initially given to
579 the prover. Finally, if a prover returns a proof with lots of facts, the
580 minimizer is invoked automatically since Metis would be unlikely to re-find the
583 Automatic minimization can be forced or disabled using the \textit{minimize}
584 option (\S\ref{mode-of-operation}).
586 \point{A strange error occurred---what should I do?}
588 Sledgehammer tries to give informative error messages. Please report any strange
589 error to the author at \authoremail. This applies double if you get the message
593 The prover found a type-unsound proof involving ``\textit{foo\/}'',
594 ``\textit{bar\/}'', and ``\textit{baz\/}'' even though a supposedly type-sound
595 encoding was used (or, less likely, your axioms are inconsistent). You might
596 want to report this to the Isabelle developers.
599 \point{Auto can solve it---why not Sledgehammer?}
601 Problems can be easy for \textit{auto} and difficult for automatic provers, but
602 the reverse is also true, so don't be discouraged if your first attempts fail.
603 Because the system refers to all theorems known to Isabelle, it is particularly
604 suitable when your goal has a short proof from lemmas that you don't know about.
606 \point{Why are there so many options?}
608 Sledgehammer's philosophy should work out of the box, without user guidance.
609 Many of the options are meant to be used mostly by the Sledgehammer developers
610 for experimentation purposes. Of course, feel free to experiment with them if
613 \section{Command Syntax}
614 \label{command-syntax}
616 \subsection{Sledgehammer}
618 Sledgehammer can be invoked at any point when there is an open goal by entering
619 the \textbf{sledgehammer} command in the theory file. Its general syntax is as
623 \textbf{sledgehammer} \qty{subcommand}$^?$ \qty{options}$^?$ \qty{facts\_override}$^?$ \qty{num}$^?$
626 For convenience, Sledgehammer is also available in the ``Commands'' submenu of
627 the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c
628 C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with
629 no arguments in the theory text.
631 In the general syntax, the \qty{subcommand} may be any of the following:
634 \item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on
635 subgoal number \qty{num} (1 by default), with the given options and facts.
637 \item[\labelitemi] \textbf{\textit{min}:} Attempts to minimize the facts
638 specified in the \qty{facts\_override} argument to obtain a simpler proof
639 involving fewer facts. The options and goal number are as for \textit{run}.
641 \item[\labelitemi] \textbf{\textit{messages}:} Redisplays recent messages issued
642 by Sledgehammer. This allows you to examine results that might have been lost
643 due to Sledgehammer's asynchronous nature. The \qty{num} argument specifies a
644 limit on the number of messages to display (10 by default).
646 \item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of
647 automatic provers supported by Sledgehammer. See \S\ref{installation} and
648 \S\ref{mode-of-operation} for more information on how to install automatic
651 \item[\labelitemi] \textbf{\textit{running\_provers}:} Prints information about
652 currently running automatic provers, including elapsed runtime and remaining
655 \item[\labelitemi] \textbf{\textit{kill\_provers}:} Terminates all running
658 \item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
659 ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
662 Sledgehammer's behavior can be influenced by various \qty{options}, which can be
663 specified in brackets after the \textbf{sledgehammer} command. The
664 \qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
665 \ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. For
669 \textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120]
672 Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
675 \textbf{sledgehammer\_params} \qty{options}
678 The supported options are described in \S\ref{option-reference}.
680 The \qty{facts\_override} argument lets you alter the set of facts that go
681 through the relevance filter. It may be of the form ``(\qty{facts})'', where
682 \qty{facts} is a space-separated list of Isabelle facts (theorems, local
683 assumptions, etc.), in which case the relevance filter is bypassed and the given
684 facts are used. It may also be of the form ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}})'',
685 ``(\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', or ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}}\
686 \textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', where the relevance filter is instructed to
687 proceed as usual except that it should consider \qty{facts\/_{\mathrm{1}}}
688 highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant.
690 You can instruct Sledgehammer to run automatically on newly entered theorems by
691 enabling the ``Auto Sledgehammer'' option in Proof General's ``Isabelle'' menu.
692 For automatic runs, only the first prover set using \textit{provers}
693 (\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover,
694 \textit{slice} (\S\ref{mode-of-operation}) is disabled, \textit{strict}
695 (\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format})
696 and \textit{debug} (\S\ref{output-format}) are disabled, and \textit{timeout}
697 (\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in Proof
698 General's ``Isabelle'' menu. Sledgehammer's output is also more concise.
702 The \textit{metis} proof method has the syntax
705 \textbf{\textit{metis}}~(\qty{options})${}^?$~\qty{facts}${}^?$
708 where \qty{facts} is a list of arbitrary facts and \qty{options} is a
709 comma-separated list consisting of at most one $\lambda$ translation scheme
710 specification with the same semantics as Sledgehammer's \textit{lam\_trans}
711 option (\S\ref{problem-encoding}) and at most one type encoding specification
712 with the same semantics as Sledgehammer's \textit{type\_enc} option
713 (\S\ref{problem-encoding}).
715 The supported $\lambda$ translation schemes are \textit{hide\_lams},
716 \textit{lifting}, and \textit{combs} (the default).
718 All the untyped type encodings listed in \S\ref{problem-encoding} are supported.
719 For convenience, the following aliases are provided:
721 \item[\labelitemi] \textbf{\textit{full\_types}:} Synonym for \textit{poly\_guards\_query}.
722 \item[\labelitemi] \textbf{\textit{partial\_types}:} Synonym for \textit{poly\_args}.
723 \item[\labelitemi] \textbf{\textit{no\_types}:} Synonym for \textit{erased}.
726 \section{Option Reference}
727 \label{option-reference}
732 \def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
733 \def\optrueonly#1{\flushitem{\textit{#1} $\bigl[$= \textit{true}$\bigr]$\enskip}\nopagebreak\\[\parskip]}
734 \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
735 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
736 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
737 \def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
738 \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
739 \def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]}
740 \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]}
741 \def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
742 \def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
743 \def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
745 Sledgehammer's options are categorized as follows:\ mode of operation
746 (\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),
747 relevance filter (\S\ref{relevance-filter}), output format
748 (\S\ref{output-format}), authentication (\S\ref{authentication}), and timeouts
751 The descriptions below refer to the following syntactic quantities:
754 \item[\labelitemi] \qtybf{string}: A string.
755 \item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}.
756 \item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or
758 \item[\labelitemi] \qtybf{int\/}: An integer.
759 %\item[\labelitemi] \qtybf{float\/}: A floating-point number (e.g., 2.5).
760 \item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers
762 \item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}.
763 \item[\labelitemi] \qtybf{float\_or\_none\/}: A floating-point number (e.g., 60 or
764 0.5) expressing a number of seconds, or the keyword \textit{none} ($\infty$
768 Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
769 have a negative counterpart (e.g., \textit{blocking} vs.\
770 \textit{non\_blocking}). When setting Boolean options or their negative
771 counterparts, ``= \textit{true\/}'' may be omitted.
773 \subsection{Mode of Operation}
774 \label{mode-of-operation}
777 \opnodefaultbrk{provers}{string}
778 Specifies the automatic provers to use as a space-separated list (e.g.,
779 ``\textit{e}~\textit{spass}~\textit{remote\_vampire\/}'').
780 Provers can be run locally or remotely; see \S\ref{installation} for
781 installation instructions.
783 The following local provers are supported:
786 \item[\labelitemi] \textbf{\textit{alt\_ergo}:} Alt-Ergo is a polymorphic
787 SMT solver developed by Bobot et al.\ \cite{alt-ergo}.
788 It supports the TPTP polymorphic typed first-order format (TFF1) via Why3
789 \cite{why3}. It is included for experimental purposes. To use Alt-Ergo, set the
790 environment variable \texttt{WHY3\_HOME} to the directory that contains the
791 \texttt{why3} executable. Sledgehammer has been tested with Alt-Ergo 0.93 and an
792 unidentified development version of Why3.
794 \item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
795 Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
796 set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
797 executable, including the file name, or install the prebuilt CVC3 package from
798 \download. Sledgehammer has been tested with version 2.2 and 2.4.1.
800 \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
801 developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment
802 variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
803 executable and \texttt{E\_VERSION} to the version number (e.g., ``1.4''), or
804 install the prebuilt E package from \download. Sledgehammer has been tested with
807 \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
808 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
809 with support for the TPTP typed higher-order syntax (THF0). To use LEO-II, set
810 the environment variable \texttt{LEO2\_HOME} to the directory that contains the
811 \texttt{leo} executable. Sledgehammer requires version 1.2.9 or above.
813 \item[\labelitemi] \textbf{\textit{metis}:} Although it is much less powerful than
814 the external provers, Metis itself can be used for proof search.
816 \item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
817 higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
818 support for the TPTP typed higher-order syntax (THF0). To use Satallax, set the
819 environment variable \texttt{SATALLAX\_HOME} to the directory that contains the
820 \texttt{satallax} executable. Sledgehammer requires version 2.2 or above.
822 \item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt} proof method with the
823 current settings (usually:\ Z3 with proof reconstruction).
825 \item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
826 prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
827 To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
828 that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the
829 version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from
830 \download. Sledgehammer requires version 3.8ds or above.
832 \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution
833 prover developed by Andrei Voronkov and his colleagues
834 \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
835 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
836 executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g.,
837 ``1.8rev1435''). Sledgehammer has been tested with versions 0.6, 1.0, and 1.8.
838 Versions strictly above 1.8 (e.g., ``1.8rev1435'') support the TPTP typed
839 first-order format (TFF0).
841 \item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at
842 SRI \cite{yices}. To use Yices, set the environment variable
843 \texttt{YICES\_SOLVER} to the complete path of the executable, including the
844 file name. Sledgehammer has been tested with version 1.0.28.
846 \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
847 Microsoft Research \cite{z3}. To use Z3, set the environment variable
848 \texttt{Z3\_SOLVER} to the complete path of the executable, including the file
849 name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
850 noncommercial user. Sledgehammer has been tested with versions 3.0, 3.1, 3.2,
853 \item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
854 an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
855 formats (FOF and TFF0). It is included for experimental purposes. It
856 requires version 3.0 or above. To use it, set the environment variable
857 \texttt{Z3\_HOME} to the directory that contains the \texttt{z3}
861 The following remote provers are supported:
864 \item[\labelitemi] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
865 on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
868 \item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs
869 on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
871 \item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover
872 developed by Kry\v stof Hoder \cite{sine} based on E. It runs on Geoff
873 Sutcliffe's Miami servers.
875 \item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
876 developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
877 servers. This ATP supports the TPTP typed first-order format (TFF0). The
878 remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
880 \item[\labelitemi] \textbf{\textit{remote\_iprover}:} iProver is a pure
881 instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. The
882 remote version of iProver runs on Geoff Sutcliffe's Miami servers
883 \cite{sutcliffe-2000}.
885 \item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} iProver-Eq is an
886 instantiation-based prover with native support for equality developed by
887 Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. The
888 remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers
889 \cite{sutcliffe-2000}.
891 \item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
892 runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
894 \item[\labelitemi] \textbf{\textit{remote\_satallax}:} The remote version of
895 Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
897 \item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a first-order
898 resolution prover developed by Stickel et al.\ \cite{snark}. It supports the
899 TPTP typed first-order format (TFF0). The remote version of SNARK runs on
900 Geoff Sutcliffe's Miami servers.
902 \item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
903 Vampire runs on Geoff Sutcliffe's Miami servers.
905 \item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
906 equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be
907 used to prove universally quantified equations using unconditional equations,
908 corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister
909 runs on Geoff Sutcliffe's Miami servers.
911 \item[\labelitemi] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
912 servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
915 \item[\labelitemi] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3
916 with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
919 By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever
920 the SMT module's \textit{smt\_solver} configuration option is set to), and (if
921 appropriate) Waldmeister in parallel---either locally or remotely, depending on
922 the number of processor cores available. For historical reasons, the default
923 value of this option can be overridden using the option ``Sledgehammer:
924 Provers'' in Proof General's ``Isabelle'' menu.
926 It is generally a good idea to run several provers in parallel. Running E,
927 SPASS, and Vampire for 5~seconds yields a similar success rate to running the
928 most effective of these for 120~seconds \cite{boehme-nipkow-2010}.
930 For the \textit{min} subcommand, the default prover is \textit{metis}. If
931 several provers are set, the first one is used.
933 \opnodefault{prover}{string}
934 Alias for \textit{provers}.
936 \opfalse{blocking}{non\_blocking}
937 Specifies whether the \textbf{sledgehammer} command should operate
938 synchronously. The asynchronous (non-blocking) mode lets the user start proving
939 the putative theorem manually while Sledgehammer looks for a proof, but it can
940 also be more confusing. Irrespective of the value of this option, Sledgehammer
941 is always run synchronously for the new jEdit-based user interface or if
942 \textit{debug} (\S\ref{output-format}) is enabled.
944 \optrue{slice}{dont\_slice}
945 Specifies whether the time allocated to a prover should be sliced into several
946 segments, each of which has its own set of possibly prover-dependent options.
947 For SPASS and Vampire, the first slice tries the fast but incomplete
948 set-of-support (SOS) strategy, whereas the second slice runs without it. For E,
949 up to three slices are tried, with different weighted search strategies and
950 number of facts. For SMT solvers, several slices are tried with the same options
951 each time but fewer and fewer facts. According to benchmarks with a timeout of
952 30 seconds, slicing is a valuable optimization, and you should probably leave it
953 enabled unless you are conducting experiments. This option is implicitly
954 disabled for (short) automatic runs.
957 {\small See also \textit{verbose} (\S\ref{output-format}).}
959 \opsmart{minimize}{dont\_minimize}
960 Specifies whether the minimization tool should be invoked automatically after
961 proof search. By default, automatic minimization takes place only if
962 it can be done in a reasonable amount of time (as determined by
963 the number of facts in the original proof and the time it took to find or
964 preplay it) or the proof involves an unreasonably large number of facts.
967 {\small See also \textit{preplay\_timeout} (\S\ref{timeouts})
968 and \textit{dont\_preplay} (\S\ref{timeouts}).}
970 \opfalse{overlord}{no\_overlord}
971 Specifies whether Sledgehammer should put its temporary files in
972 \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
973 debugging Sledgehammer but also unsafe if several instances of the tool are run
974 simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
975 safely remove them after Sledgehammer has run.
978 {\small See also \textit{debug} (\S\ref{output-format}).}
981 \subsection{Problem Encoding}
982 \label{problem-encoding}
984 \newcommand\comb[1]{\const{#1}}
987 \opdefault{lam\_trans}{string}{smart}
988 Specifies the $\lambda$ translation scheme to use in ATP problems. The supported
989 translation schemes are listed below:
992 \item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$-abstractions
993 by replacing them by unspecified fresh constants, effectively disabling all
994 reasoning under $\lambda$-abstractions.
996 \item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new
997 supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions,
998 defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting).
1000 \item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry
1001 combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators
1002 enable the ATPs to synthesize $\lambda$-terms but tend to yield bulkier formulas
1003 than $\lambda$-lifting: The translation is quadratic in the worst case, and the
1004 equational definitions of the combinators are very prolific in the context of
1007 \item[\labelitemi] \textbf{\textit{combs\_and\_lifting}:} Introduce a new
1008 supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a
1009 lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators.
1011 \item[\labelitemi] \textbf{\textit{combs\_or\_lifting}:} For each cluster of
1012 $\lambda$-abstractions, heuristically choose between $\lambda$-lifting and Curry
1015 \item[\labelitemi] \textbf{\textit{keep\_lams}:}
1016 Keep the $\lambda$-abstractions in the generated problems. This is available
1017 only with provers that support the THF0 syntax.
1019 \item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used
1020 depends on the ATP and should be the most efficient scheme for that ATP.
1023 For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting},
1024 irrespective of the value of this option.
1026 \opsmartx{uncurried\_aliases}{no\_uncurried\_aliases}
1027 Specifies whether fresh function symbols should be generated as aliases for
1028 applications of curried functions in ATP problems.
1030 \opdefault{type\_enc}{string}{smart}
1031 Specifies the type encoding to use in ATP problems. Some of the type encodings
1032 are unsound, meaning that they can give rise to spurious proofs
1033 (unreconstructible using \textit{metis}). The supported type encodings are
1034 listed below, with an indication of their soundness in parentheses.
1035 An asterisk (*) means that the encoding is slightly incomplete for
1036 reconstruction with \textit{metis}, unless the \emph{strict} option (described
1040 \item[\labelitemi] \textbf{\textit{erased} (very unsound):} No type information is
1041 supplied to the ATP, not even to resolve overloading. Types are simply erased.
1043 \item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using
1044 a predicate \const{g}$(\tau, t)$ that guards bound
1045 variables. Constants are annotated with their types, supplied as additional
1046 arguments, to resolve overloading.
1048 \item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
1049 tagged with its type using a function $\const{t\/}(\tau, t)$.
1051 \item[\labelitemi] \textbf{\textit{poly\_args} (unsound):}
1052 Like for \textit{poly\_guards} constants are annotated with their types to
1053 resolve overloading, but otherwise no type information is encoded. This
1054 coincides with the default encoding used by the \textit{metis} command.
1058 \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\
1059 \textit{raw\_mono\_args} (unsound):} \\
1060 Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args},
1061 respectively, but the problem is additionally monomorphized, meaning that type
1062 variables are instantiated with heuristically chosen ground types.
1063 Monomorphization can simplify reasoning but also leads to larger fact bases,
1064 which can slow down the ATPs.
1068 \textit{mono\_guards}, \textit{mono\_tags} (sound);
1069 \textit{mono\_args} (unsound):} \\
1071 \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and
1072 \textit{raw\_mono\_args}, respectively but types are mangled in constant names
1073 instead of being supplied as ground term arguments. The binary predicate
1074 $\const{g}(\tau, t)$ becomes a unary predicate
1075 $\const{g\_}\tau(t)$, and the binary function
1076 $\const{t}(\tau, t)$ becomes a unary function
1077 $\const{t\_}\tau(t)$.
1079 \item[\labelitemi] \textbf{\textit{mono\_native} (sound):} Exploits native
1080 first-order types if the prover supports the TFF0, TFF1, or THF0 syntax;
1081 otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized.
1083 \item[\labelitemi] \textbf{\textit{mono\_native\_higher} (sound):} Exploits
1084 native higher-order types if the prover supports the THF0 syntax; otherwise,
1085 falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is
1088 \item[\labelitemi] \textbf{\textit{poly\_native} (sound):} Exploits native
1089 polymorphic first-order types if the prover supports the TFF1 syntax; otherwise,
1090 falls back on \textit{mono\_native}.
1094 \textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\
1095 \textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
1096 \textit{mono\_native}? (sound*):} \\
1097 The type encodings \textit{poly\_guards}, \textit{poly\_tags},
1098 \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
1099 \textit{mono\_tags}, and \textit{mono\_native} are fully typed and sound. For
1100 each of these, Sledgehammer also provides a lighter variant identified by a
1101 question mark (`\hbox{?}')\ that detects and erases monotonic types, notably
1102 infinite types. (For \textit{mono\_native}, the types are not actually erased
1103 but rather replaced by a shared uniform type of individuals.) As argument to the
1104 \textit{metis} proof method, the question mark is replaced by a
1105 \hbox{``\textit{\_query\/}''} suffix.
1109 \textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\
1110 \textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\
1112 Even lighter versions of the `\hbox{?}' encodings. As argument to the
1113 \textit{metis} proof method, the `\hbox{??}' suffix is replaced by
1114 \hbox{``\textit{\_query\_query\/}''}.
1118 \textit{poly\_guards}@?, \textit{raw\_mono\_guards}@? (sound*):} \\
1119 Alternative versions of the `\hbox{??}' encodings. As argument to the
1120 \textit{metis} proof method, the `\hbox{@?}' suffix is replaced by
1121 \hbox{``\textit{\_at\_query\/}''}.
1125 \textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
1126 \textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
1127 \textit{mono\_native}!, \textit{mono\_native\_higher}! (mildly unsound):} \\
1128 The type encodings \textit{poly\_guards}, \textit{poly\_tags},
1129 \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
1130 \textit{mono\_tags}, \textit{mono\_native}, and \textit{mono\_native\_higher}
1131 also admit a mildly unsound (but very efficient) variant identified by an
1132 exclamation mark (`\hbox{!}') that detects and erases erases all types except
1133 those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_native}
1134 and \textit{mono\_native\_higher}, the types are not actually erased but rather
1135 replaced by a shared uniform type of individuals.) As argument to the
1136 \textit{metis} proof method, the exclamation mark is replaced by the suffix
1137 \hbox{``\textit{\_bang\/}''}.
1141 \textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\
1142 \textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\
1143 (mildly unsound):} \\
1144 Even lighter versions of the `\hbox{!}' encodings. As argument to the
1145 \textit{metis} proof method, the `\hbox{!!}' suffix is replaced by
1146 \hbox{``\textit{\_bang\_bang\/}''}.
1150 \textit{poly\_guards}@!, \textit{raw\_mono\_guards}@! (mildly unsound):} \\
1151 Alternative versions of the `\hbox{!!}' encodings. As argument to the
1152 \textit{metis} proof method, the `\hbox{@!}' suffix is replaced by
1153 \hbox{``\textit{\_at\_bang\/}''}.
1155 \item[\labelitemi] \textbf{\textit{smart}:} The actual encoding used depends on
1156 the ATP and should be the most efficient sound encoding for that ATP.
1159 For SMT solvers, the type encoding is always \textit{mono\_native}, irrespective
1160 of the value of this option.
1163 {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
1164 and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).}
1166 \opfalse{strict}{non\_strict}
1167 Specifies whether Sledgehammer should run in its strict mode. In that mode,
1168 sound type encodings marked with an asterisk (*) above are made complete
1169 for reconstruction with \textit{metis}, at the cost of some clutter in the
1170 generated problems. This option has no effect if \textit{type\_enc} is
1171 deliberately set to an unsound encoding.
1174 \subsection{Relevance Filter}
1175 \label{relevance-filter}
1178 \opdefault{relevance\_thresholds}{float\_pair}{\upshape 0.45~0.85}
1179 Specifies the thresholds above which facts are considered relevant by the
1180 relevance filter. The first threshold is used for the first iteration of the
1181 relevance filter and the second threshold is used for the last iteration (if it
1182 is reached). The effective threshold is quadratically interpolated for the other
1183 iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
1184 are relevant and 1 only theorems that refer to previously seen constants.
1186 \opdefault{max\_relevant}{smart\_int}{smart}
1187 Specifies the maximum number of facts that may be returned by the relevance
1188 filter. If the option is set to \textit{smart}, it is set to a value that was
1189 empirically found to be appropriate for the prover. Typical values range between
1192 \opdefault{max\_new\_mono\_instances}{int}{smart}
1193 Specifies the maximum number of monomorphic instances to generate beyond
1194 \textit{max\_relevant}. The higher this limit is, the more monomorphic instances
1195 are potentially generated. Whether monomorphization takes place depends on the
1196 type encoding used. If the option is set to \textit{smart}, it is set to a value
1197 that was empirically found to be appropriate for the prover. For most provers,
1201 {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
1203 \opdefault{max\_mono\_iters}{int}{smart}
1204 Specifies the maximum number of iterations for the monomorphization fixpoint
1205 construction. The higher this limit is, the more monomorphic instances are
1206 potentially generated. Whether monomorphization takes place depends on the
1207 type encoding used. If the option is set to \textit{smart}, it is set to a value
1208 that was empirically found to be appropriate for the prover. For most provers,
1212 {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
1215 \subsection{Output Format}
1216 \label{output-format}
1220 \opfalse{verbose}{quiet}
1221 Specifies whether the \textbf{sledgehammer} command should explain what it does.
1222 This option is implicitly disabled for automatic runs.
1224 \opfalse{debug}{no\_debug}
1225 Specifies whether Sledgehammer should display additional debugging information
1226 beyond what \textit{verbose} already displays. Enabling \textit{debug} also
1227 enables \textit{verbose} and \textit{blocking} (\S\ref{mode-of-operation})
1228 behind the scenes. The \textit{debug} option is implicitly disabled for
1232 {\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
1234 \opfalse{isar\_proof}{no\_isar\_proof}
1235 Specifies whether Isar proofs should be output in addition to one-liner
1236 \textit{metis} proofs. Isar proof construction is still experimental and often
1237 fails; however, they are usually faster and sometimes more robust than
1238 \textit{metis} proofs.
1240 \opdefault{isar\_shrink\_factor}{int}{\upshape 1}
1241 Specifies the granularity of the Isar proof. A value of $n$ indicates that each
1242 Isar proof step should correspond to a group of up to $n$ consecutive proof
1243 steps in the ATP proof.
1246 \subsection{Authentication}
1247 \label{authentication}
1250 \opnodefault{expect}{string}
1251 Specifies the expected outcome, which must be one of the following:
1254 \item[\labelitemi] \textbf{\textit{some}:} Sledgehammer found a proof.
1255 \item[\labelitemi] \textbf{\textit{none}:} Sledgehammer found no proof.
1256 \item[\labelitemi] \textbf{\textit{timeout}:} Sledgehammer timed out.
1257 \item[\labelitemi] \textbf{\textit{unknown}:} Sledgehammer encountered some
1261 Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning
1262 (otherwise) if the actual outcome differs from the expected outcome. This option
1263 is useful for regression testing.
1266 {\small See also \textit{blocking} (\S\ref{mode-of-operation}) and
1267 \textit{timeout} (\S\ref{timeouts}).}
1270 \subsection{Timeouts}
1274 \opdefault{timeout}{float\_or\_none}{\upshape 30}
1275 Specifies the maximum number of seconds that the automatic provers should spend
1276 searching for a proof. This excludes problem preparation and is a soft limit.
1277 For historical reasons, the default value of this option can be overridden using
1278 the option ``Sledgehammer: Time Limit'' in Proof General's ``Isabelle'' menu.
1280 \opdefault{preplay\_timeout}{float\_or\_none}{\upshape 3}
1281 Specifies the maximum number of seconds that \textit{metis} or \textit{smt}
1282 should spend trying to ``preplay'' the found proof. If this option is set to 0,
1283 no preplaying takes place, and no timing information is displayed next to the
1284 suggested \textit{metis} calls.
1287 {\small See also \textit{minimize} (\S\ref{mode-of-operation}).}
1289 \optrueonly{dont\_preplay}
1290 Alias for ``\textit{preplay\_timeout} = 0''.
1295 \bibliography{../manual}{}
1296 \bibliographystyle{abbrv}