\documentclass[a4paper,12pt]{article}

 \usepackage[T1]{fontenc}

 \usepackage{amsmath}

 \usepackage{amssymb}

 \usepackage[english,french]{babel}

 \usepackage{color}

 \usepackage{footmisc}

 \usepackage{graphicx}

 %\usepackage{mathpazo}

 \usepackage{multicol}

 \usepackage{stmaryrd}

 %\usepackage[scaled=.85]{beramono}

 \usepackage{../../lib/texinputs/isabelle,../iman,../pdfsetup}

 \def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}}

 \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$}

 %\oddsidemargin=4.6mm

 %\evensidemargin=4.6mm

 %\textwidth=150mm

 %\topmargin=4.6mm

 %\headheight=0mm

 %\headsep=0mm

 %\textheight=234mm

 \def\Colon{\mathord{:\mkern-1.5mu:}}

 %\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}

 %\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}

 \def\lparr{\mathopen{(\mkern-4mu\mid}}

 \def\rparr{\mathclose{\mid\mkern-4mu)}}

 \def\unk{{?}}

 \def\undef{(\lambda x.\; \unk)}

 %\def\unr{\textit{others}}

 \def\unr{\ldots}

 \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}

 \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}

 \urlstyle{tt}

 \begin{document}

 \selectlanguage{english}

 \title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]

 Hammering Away \\[\smallskipamount]

 \Large A User's Guide to Sledgehammer for Isabelle/HOL}

 \author{\hbox{} \\

 Jasmin Christian Blanchette \\

 {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount]

 {\normalsize with contributions from} \\[4\smallskipamount]

 Lawrence C. Paulson \\

 {\normalsize Computer Laboratory, University of Cambridge} \\

 \hbox{}}

 \maketitle

 \tableofcontents

 \setlength{\parskip}{.7em plus .2em minus .1em}

 \setlength{\parindent}{0pt}

 \setlength{\abovedisplayskip}{\parskip}

 \setlength{\abovedisplayshortskip}{.9\parskip}

 \setlength{\belowdisplayskip}{\parskip}

 \setlength{\belowdisplayshortskip}{.9\parskip}

 % General-purpose enum environment with correct spacing

 \newenvironment{enum}%

     {\begin{list}{}{%

         \setlength{\topsep}{.1\parskip}%

         \setlength{\partopsep}{.1\parskip}%

         \setlength{\itemsep}{\parskip}%

         \advance\itemsep by-\parsep}}

     {\end{list}}

 \def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin

 \advance\rightskip by\leftmargin}

 \def\post{\vskip0pt plus1ex\endgroup}

 \def\prew{\pre\advance\rightskip by-\leftmargin}

 \def\postw{\post}

 \section{Introduction}

 \label{introduction}

 Sledgehammer is a tool that applies automatic theorem provers (ATPs)

 and satisfiability-modulo-theories (SMT) solvers on the current goal. The

 supported ATPs are E \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF

 \cite{tofof}, LEO-II \cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark},

 SPASS \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, and

 Waldmeister \cite{waldmeister}. The ATPs are run either locally or remotely via

 the System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs,

 the SMT solvers Z3 \cite{z3} is used by default, and you can tell Sledgehammer

 to try CVC3 \cite{cvc3} and Yices \cite{yices} as well; these are run either

 locally or on a server at the TU M\"unchen.

 The problem passed to the automatic provers consists of your current goal

 together with a heuristic selection of hundreds of facts (theorems) from the

 current theory context, filtered by relevance. Because jobs are run in the

 background, you can continue to work on your proof by other means. Provers can

 be run in parallel. Any reply (which may arrive half a minute later) will appear

 in the Proof General response buffer.

 The result of a successful proof search is some source text that usually (but

 not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed

 proof relies on the general-purpose Metis prover, which is fully integrated into

 Isabelle/HOL, with explicit inferences going through the kernel. Thus its

 results are correct by construction.

 In this manual, we will explicitly invoke the \textbf{sledgehammer} command.

 Sledgehammer also provides an automatic mode that can be enabled via the ``Auto

 Sledgehammer'' option in Proof General's ``Isabelle'' menu. In this mode,

 Sledgehammer is run on every newly entered theorem. The time limit for Auto

 Sledgehammer and other automatic tools can be set using the ``Auto Tools Time

 Limit'' option.

 \newbox\boxA

 \setbox\boxA=\hbox{\texttt{nospam}}

 \newcommand\authoremail{\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak

 in.\allowbreak tum.\allowbreak de}}

 To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is

 imported---this is rarely a problem in practice since it is part of

 \textit{Main}. Examples of Sledgehammer use can be found in Isabelle's

 \texttt{src/HOL/Metis\_Examples} directory.

 Comments and bug reports concerning Sledgehammer or this manual should be

 directed to the author at \authoremail.

 \vskip2.5\smallskipamount

 %\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for

 %suggesting several textual improvements.

 \section{Installation}

 \label{installation}

 Sledgehammer is part of Isabelle, so you don't need to install it. However, it

 relies on third-party automatic theorem provers (ATPs) and SMT solvers.

 \subsection{Installing ATPs}

 Currently, E, LEO-II, Satallax, SPASS, and Vampire can be run locally; in

 addition, E, E-SInE, E-ToFoF, LEO-II, Satallax, SNARK, Waldmeister, and Vampire

 are available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. If you want

 better performance, you should at least install E and SPASS locally.

 There are three main ways to install ATPs on your machine:

 \begin{enum}

 \item[$\bullet$] If you installed an official Isabelle package with everything

 inside, it should already include properly setup executables for E and SPASS,

 ready to use.%

 \footnote{Vampire's license prevents us from doing the same for this otherwise

 wonderful tool.}

 \item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS

 binary packages from Isabelle's download page. Extract the archives, then add a

 line to your \texttt{\$ISABELLE\_HOME\_USER/etc/components}%

 \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at

 startup. Its value can be retrieved by invoking \texttt{isabelle}

 \texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}

 file with the absolute

 path to E or SPASS. For example, if the \texttt{components} does not exist yet

 and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create the

 \texttt{components} file with the single line

 \prew

 \texttt{/usr/local/spass-3.7}

 \postw

 in it.

 \item[$\bullet$] If you prefer to build E or SPASS yourself, or obtained a

 Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}),

 set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or

 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},

 \texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested

 with E 1.0 to 1.4, SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8%

 \footnote{Following the rewrite of Vampire, the counter for version numbers was

 reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent

 than, say, Vampire 9.0 or 11.5.}%

 . Since the ATPs' output formats are neither documented nor stable, other

 versions of the ATPs might or might not work well with Sledgehammer. Ideally,

 also set \texttt{E\_VERSION}, \texttt{SPASS\_VERSION}, or

 \texttt{VAMPIRE\_VERSION} to the ATP's version number (e.g., ``1.4'').

 \end{enum}

 To check whether E and SPASS are successfully installed, follow the example in

 \S\ref{first-steps}. If the remote versions of E and SPASS are used (identified

 by the prefix ``\emph{remote\_}''), or if the local versions fail to solve the

 easy goal presented there, this is a sign that something is wrong with your

 installation.

 Remote ATP invocation via the SystemOnTPTP web service requires Perl with the

 World Wide Web Library (\texttt{libwww-perl}) installed. If you must use a proxy

 server to access the Internet, set the \texttt{http\_proxy} environment variable

 to the proxy, either in the environment in which Isabelle is launched or in your

 \texttt{\char`\~/\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few examples:

 \prew

 \texttt{http\_proxy=http://proxy.example.org} \\

 \texttt{http\_proxy=http://proxy.example.org:8080} \\

 \texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org}

 \postw

 \subsection{Installing SMT Solvers}

 CVC3, Yices, and Z3 can be run locally or (for CVC3 and Z3) remotely on a TU

 M\"unchen server. If you want better performance and get the ability to replay

 proofs that rely on the \emph{smt} proof method, you should at least install Z3

 locally.

 There are two main ways of installing SMT solvers locally.

 \begin{enum}

 \item[$\bullet$] If you installed an official Isabelle package with everything

 inside, it should already include properly setup executables for CVC3 and Z3,

 ready to use.%

 \footnote{Yices's license prevents us from doing the same for this otherwise

 wonderful tool.}

 For Z3, you additionally need to set the environment variable

 \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a noncommercial

 user.

 \item[$\bullet$] Otherwise, follow the instructions documented in the \emph{SMT}

 theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}).

 \end{enum}

 \section{First Steps}

 \label{first-steps}

 To illustrate Sledgehammer in context, let us start a theory file and

 attempt to prove a simple lemma:

 \prew

 \textbf{theory}~\textit{Scratch} \\

 \textbf{imports}~\textit{Main} \\

 \textbf{begin} \\[2\smallskipamount]

 %

 \textbf{lemma} ``$[a] = [b] \,\Longrightarrow\, a = b$'' \\

 \textbf{sledgehammer}

 \postw

 Instead of issuing the \textbf{sledgehammer} command, you can also find

 Sledgehammer in the ``Commands'' submenu of the ``Isabelle'' menu in Proof

 General or press the Emacs key sequence C-c C-a C-s.

 Either way, Sledgehammer produces the following output after a few seconds:

 \prew

 \slshape

 Sledgehammer: ``\textit{e}'' on goal \\

 $[a] = [b] \,\Longrightarrow\, a = b$ \\

 Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]

 %

 Sledgehammer: ``\textit{vampire}'' on goal \\

 $[a] = [b] \,\Longrightarrow\, a = b$ \\

 Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]

 %

 Sledgehammer: ``\textit{spass}'' on goal \\

 $[a] = [b] \,\Longrightarrow\, a = b$ \\

 Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]

 %

 Sledgehammer: ``\textit{remote\_waldmeister}'' on goal \\

 $[a] = [b] \,\Longrightarrow\, a = b$ \\

 Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]

 %

 Sledgehammer: ``\textit{remote\_e\_sine}'' on goal \\

 $[a] = [b] \,\Longrightarrow\, a = b$ \\

 Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). \\[3\smallskipamount]

 %

 Sledgehammer: ``\textit{remote\_z3}'' on goal \\

 $[a] = [b] \,\Longrightarrow\, a = b$ \\

 Try this: \textbf{by} (\textit{metis list.inject}) (20 ms).

 \postw

 Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel.

 Depending on which provers are installed and how many processor cores are

 available, some of the provers might be missing or present with a

 \textit{remote\_} prefix. Waldmeister is run only for unit equational problems,

 where the goal's conclusion is a (universally quantified) equation.

 For each successful prover, Sledgehammer gives a one-liner proof that uses Metis

 or the \textit{smt} proof method. For Metis, approximate timings are shown in

 parentheses, indicating how fast the call is. You can click the proof to insert

 it into the theory text.

 In addition, you can ask Sledgehammer for an Isar text proof by passing the

 \textit{isar\_proof} option (\S\ref{output-format}):

 \prew

 \textbf{sledgehammer} [\textit{isar\_proof}]

 \postw

 When Isar proof construction is successful, it can yield proofs that are more

 readable and also faster than the Metis one-liners. This feature is experimental

 and is only available for ATPs.

 \section{Hints}

 \label{hints}

 This section presents a few hints that should help you get the most out of

 Sledgehammer and Metis. Frequently (and infrequently) asked questions are

 answered in \S\ref{frequently-asked-questions}.

 \newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak}

 \point{Presimplify the goal}

 For best results, first simplify your problem by calling \textit{auto} or at

 least \textit{safe} followed by \textit{simp\_all}. The SMT solvers provide

 arithmetic decision procedures, but the ATPs typically do not (or if they do,

 Sledgehammer does not use it yet). Apart from Waldmeister, they are not

 especially good at heavy rewriting, but because they regard equations as

 undirected, they often prove theorems that require the reverse orientation of a

 \textit{simp} rule. Higher-order problems can be tackled, but the success rate

 is better for first-order problems. Hence, you may get better results if you

 first simplify the problem to remove higher-order features.

 \point{Make sure at least E, SPASS, Vampire, and Z3 are installed}

 Locally installed provers are faster and more reliable than those running on

 servers. See \S\ref{installation} for details on how to install them.

 \point{Familiarize yourself with the most important options}

 Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of

 the options are very specialized, but serious users of the tool should at least

 familiarize themselves with the following options:

 \begin{enum}

 \item[$\bullet$] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies

 the automatic provers (ATPs and SMT solvers) that should be run whenever

 Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass

 remote\_vampire}''). For convenience, you can omit ``\textit{provers}~=''

 and simply write the prover names as a space-separated list (e.g., ``\textit{e

 spass remote\_vampire}'').

 \item[$\bullet$] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})

 specifies the maximum number of facts that should be passed to the provers. By

 default, the value is prover-dependent but varies between about 150 and 1000. If

 the provers time out, you can try lowering this value to, say, 100 or 50 and see

 if that helps.

 \item[$\bullet$] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies

 that Isar proofs should be generated, instead of one-liner Metis proofs. The

 length of the Isar proofs can be controlled by setting

 \textit{isar\_shrink\_factor} (\S\ref{output-format}).

 \item[$\bullet$] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the

 provers' time limit. It is set to 30 seconds, but since Sledgehammer runs

 asynchronously you should not hesitate to raise this limit to 60 or 120 seconds

 if you are the kind of user who can think clearly while ATPs are active.

 \end{enum}

 Options can be set globally using \textbf{sledgehammer\_params}

 (\S\ref{command-syntax}). The command also prints the list of all available

 options with their current value. Fact selection can be influenced by specifying

 ``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} call

 to ensure that certain facts are included, or simply ``$(\textit{my\_facts})$''

 to force Sledgehammer to run only with $\textit{my\_facts}$.

 \section{Frequently Asked Questions}

 \label{frequently-asked-questions}

 This sections answers frequently (and infrequently) asked questions about

 Sledgehammer. It is a good idea to skim over it now even if you don't have any

 questions at this stage. And if you have any further questions not listed here,

 send them to the author at \authoremail.

 \point{Why does Metis fail to reconstruct the proof?}

 There are many reasons. If Metis runs seemingly forever, that is a sign that the

 proof is too difficult for it. Metis's search is complete, so it should

 eventually find it, but that's little consolation. There are several possible

 solutions:

 \begin{enum}

 \item[$\bullet$] Try the \textit{isar\_proof} option (\S\ref{output-format}) to

 obtain a step-by-step Isar proof where each step is justified by Metis. Since

 the steps are fairly small, Metis is more likely to be able to replay them.

 \item[$\bullet$] Try the \textit{smt} proof method instead of Metis. It is

 usually stronger, but you need to have Z3 available to replay the proofs, trust

 the SMT solver, or use certificates. See the documentation in the \emph{SMT}

 theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}) for details.

 \item[$\bullet$] Try the \textit{blast} or \textit{auto} proof methods, passing

 the necessary facts via \textbf{unfolding}, \textbf{using}, \textit{intro}{:},

 \textit{elim}{:}, \textit{dest}{:}, or \textit{simp}{:}, as appropriate.

 \end{enum}

 In some rare cases, Metis fails fairly quickly, and you get the error message

 \prew

 \slshape

 Proof reconstruction failed.

 \postw

 This message usually indicates that Sledgehammer found a type-incorrect proof.

 This was a frequent issue with older versions of Sledgehammer, which did not

 supply enough typing information to the ATPs by default. If you notice many

 unsound proofs and are not using \textit{type\_enc} (\S\ref{problem-encoding}),

 contact the author at \authoremail.

 \point{How can I tell whether a generated proof is sound?}

 First, if Metis can reconstruct it, the proof is sound (assuming Isabelle's

 inference kernel is sound). If it fails or runs seemingly forever, you can try

 \prew

 \textbf{apply}~\textbf{--} \\

 \textbf{sledgehammer} [\textit{sound}] (\textit{metis\_facts})

 \postw

 where \textit{metis\_facts} is the list of facts appearing in the suggested

 Metis call. The automatic provers should be able to re-find the proof quickly if

 it is sound, and the \textit{sound} option (\S\ref{problem-encoding}) ensures

 that no unsound proofs are found.

 \point{Which facts are passed to the automatic provers?}

 The relevance filter assigns a score to every available fact (lemma, theorem,

 definition, or axiom)\ based upon how many constants that fact shares with the

 conjecture. This process iterates to include facts relevant to those just

 accepted, but with a decay factor to ensure termination. The constants are

 weighted to give unusual ones greater significance. The relevance filter copes

 best when the conjecture contains some unusual constants; if all the constants

 are common, it is unable to discriminate among the hundreds of facts that are

 picked up. The relevance filter is also memoryless: It has no information about

 how many times a particular fact has been used in a proof, and it cannot learn.

 The number of facts included in a problem varies from prover to prover, since

 some provers get overwhelmed more easily than others. You can show the number of

 facts given using the \textit{verbose} option (\S\ref{output-format}) and the

 actual facts using \textit{debug} (\S\ref{output-format}).

 Sledgehammer is good at finding short proofs combining a handful of existing

 lemmas. If you are looking for longer proofs, you must typically restrict the

 number of facts, by setting the \textit{max\_relevant} option

 (\S\ref{relevance-filter}) to, say, 25 or 50.

 You can also influence which facts are actually selected in a number of ways. If

 you simply want to ensure that a fact is included, you can specify it using the

 ``$(\textit{add}{:}~\textit{my\_facts})$'' syntax. For example:

 %

 \prew

 \textbf{sledgehammer} (\textit{add}: \textit{hd.simps} \textit{tl.simps})

 \postw

 %

 The specified facts then replace the least relevant facts that would otherwise be

 included; the other selected facts remain the same.

 If you want to direct the selection in a particular direction, you can specify

 the facts via \textbf{using}:

 %

 \prew

 \textbf{using} \textit{hd.simps} \textit{tl.simps} \\

 \textbf{sledgehammer}

 \postw

 %

 The facts are then more likely to be selected than otherwise, and if they are

 selected at iteration $j$ they also influence which facts are selected at

 iterations $j + 1$, $j + 2$, etc. To give them even more weight, try

 %

 \prew

 \textbf{using} \textit{hd.simps} \textit{tl.simps} \\

 \textbf{apply}~\textbf{--} \\

 \textbf{sledgehammer}

 \postw

 \point{Why are the generated Isar proofs so ugly/detailed/broken?}

 The current implementation is experimental and explodes exponentially in the

 worst case. Work on a new implementation has begun. There is a large body of

 research into transforming resolution proofs into natural deduction proofs (such

 as Isar proofs), which we hope to leverage. In the meantime, a workaround is to

 set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger

 value or to try several provers and keep the nicest-looking proof.

 \point{What are the \textit{full\_types} and \textit{no\_types} arguments to

 Metis?}

 The \textit{metis}~(\textit{full\_types}) proof method is the fully-typed

 version of Metis. It is somewhat slower than \textit{metis}, but the proof

 search is fully typed, and it also includes more powerful rules such as the

 axiom ``$x = \mathit{True} \mathrel{\lor} x = \mathit{False}$'' for reasoning in

 higher-order places (e.g., in set comprehensions). The method kicks in

 automatically as a fallback when \textit{metis} fails, and it is sometimes

 generated by Sledgehammer instead of \textit{metis} if the proof obviously

 requires type information or if \textit{metis} failed when Sledgehammer

 preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with

 various options for up to 4 seconds to ensure that the generated one-line proofs

 actually work and to display timing information. This can be configured using

 the \textit{preplay\_timeout} option (\S\ref{timeouts}).)

 At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})

 uses no type information at all during the proof search, which is more efficient

 but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally

 generated by Sledgehammer.

 Incidentally, if you see the warning

 \prew

 \slshape

 Metis: Falling back on ``\textit{metis} (\textit{full\_types})''.

 \postw

 for a successful Metis proof, you can advantageously pass the

 \textit{full\_types} option to \textit{metis} directly.

 \point{Are generated proofs minimal?}

 Automatic provers frequently use many more facts than are necessary.

 Sledgehammer inclues a minimization tool that takes a set of facts returned by a

 given prover and repeatedly calls the same prover or Metis with subsets of those

 axioms in order to find a minimal set. Reducing the number of axioms typically

 improves Metis's speed and success rate, while also removing superfluous clutter

 from the proof scripts.

 In earlier versions of Sledgehammer, generated proofs were systematically

 accompanied by a suggestion to invoke the minimization tool. This step is now

 performed implicitly if it can be done in a reasonable amount of time (something

 that can be guessed from the number of facts in the original proof and the time

 it took to find it or replay it).

 In addition, some provers (notably CVC3, Satallax, and Yices) do not provide

 proofs or sometimes produce incomplete proofs. The minimizer is then invoked to

 find out which facts are actually needed from the (large) set of facts that was

 initinally given to the prover. Finally, if a prover returns a proof with lots

 of facts, the minimizer is invoked automatically since Metis would be unlikely

 to re-find the proof.

 \point{A strange error occurred---what should I do?}

 Sledgehammer tries to give informative error messages. Please report any strange

 error to the author at \authoremail. This applies double if you get the message

 \prew

 \slshape

 The prover found a type-unsound proof involving ``\textit{foo}'',

 ``\textit{bar}'', and ``\textit{baz}'' even though a supposedly type-sound

 encoding was used (or, less likely, your axioms are inconsistent). You might

 want to report this to the Isabelle developers.

 \postw

 \point{Auto can solve it---why not Sledgehammer?}

 Problems can be easy for \textit{auto} and difficult for automatic provers, but

 the reverse is also true, so don't be discouraged if your first attempts fail.

 Because the system refers to all theorems known to Isabelle, it is particularly

 suitable when your goal has a short proof from lemmas that you don't know about.

 \point{Why are there so many options?}

 Sledgehammer's philosophy should work out of the box, without user guidance.

 Many of the options are meant to be used mostly by the Sledgehammer developers

 for experimentation purposes. Of course, feel free to experiment with them if

 you are so inclined.

 \section{Command Syntax}

 \label{command-syntax}

 Sledgehammer can be invoked at any point when there is an open goal by entering

 the \textbf{sledgehammer} command in the theory file. Its general syntax is as

 follows:

 \prew

 \textbf{sledgehammer} \qty{subcommand}$^?$ \qty{options}$^?$ \qty{facts\_override}$^?$ \qty{num}$^?$

 \postw

 For convenience, Sledgehammer is also available in the ``Commands'' submenu of

 the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c

 C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with

 no arguments in the theory text.

 In the general syntax, the \qty{subcommand} may be any of the following:

 \begin{enum}

 \item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on

 subgoal number \qty{num} (1 by default), with the given options and facts.

 \item[$\bullet$] \textbf{\textit{min}:} Attempts to minimize the facts

 specified in the \qty{facts\_override} argument to obtain a simpler proof

 involving fewer facts. The options and goal number are as for \textit{run}.

 \item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued

 by Sledgehammer. This allows you to examine results that might have been lost

 due to Sledgehammer's asynchronous nature. The \qty{num} argument specifies a

 limit on the number of messages to display (5 by default).

 \item[$\bullet$] \textbf{\textit{supported\_provers}:} Prints the list of

 automatic provers supported by Sledgehammer. See \S\ref{installation} and

 \S\ref{mode-of-operation} for more information on how to install automatic

 provers.

 \item[$\bullet$] \textbf{\textit{running\_provers}:} Prints information about

 currently running automatic provers, including elapsed runtime and remaining

 time until timeout.

 \item[$\bullet$] \textbf{\textit{kill\_provers}:} Terminates all running

 automatic provers.

 \item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote

 ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.

 \end{enum}

 Sledgehammer's behavior can be influenced by various \qty{options}, which can be

 specified in brackets after the \textbf{sledgehammer} command. The

 \qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1,

 \ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true}'' is optional. For

 example:

 \prew

 \textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120]

 \postw

 Default values can be set using \textbf{sledgehammer\_\allowbreak params}:

 \prew

 \textbf{sledgehammer\_params} \qty{options}

 \postw

 The supported options are described in \S\ref{option-reference}.

 The \qty{facts\_override} argument lets you alter the set of facts that go

 through the relevance filter. It may be of the form ``(\qty{facts})'', where

 \qty{facts} is a space-separated list of Isabelle facts (theorems, local

 assumptions, etc.), in which case the relevance filter is bypassed and the given

 facts are used. It may also be of the form ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}})'',

 ``(\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', or ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}}\

 \textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', where the relevance filter is instructed to

 proceed as usual except that it should consider \qty{facts\/_{\mathrm{1}}}

 highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant.

 You can instruct Sledgehammer to run automatically on newly entered theorems by

 enabling the ``Auto Sledgehammer'' option in Proof General's ``Isabelle'' menu.

 For automatic runs, only the first prover set using \textit{provers}

 (\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover,

 \textit{slicing} (\S\ref{mode-of-operation}) is disabled, \textit{sound}

 (\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format})

 and \textit{debug} (\S\ref{output-format}) are disabled, and \textit{timeout}

 (\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in Proof

 General's ``Isabelle'' menu. Sledgehammer's output is also more concise.

 The \textit{metis} proof method has the syntax

 \prew

 \textbf{\textit{metis}}~(\qty{type\_enc})${}^?$~\qty{facts}${}^?$

 \postw

 where \qty{type\_enc} is a type encoding specification with the same semantics

 as Sledgehammer's \textit{type\_enc} option (\S\ref{problem-encoding}) and

 \qty{facts} is a list of arbitrary facts. In addition to the values listed in

 \S\ref{problem-encoding}, \qty{type\_enc} may also be \textit{full\_types}, in

 which case an appropriate type-sound encoding is chosen, \textit{partial\_types}

 (the default type-unsound encoding), or \textit{no\_types}, a synonym for

 \textit{erased}.

 \section{Option Reference}

 \label{option-reference}

 \def\defl{\{}

 \def\defr{\}}

 \def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}

 \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}

 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}

 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}

 \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}

 \def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]}

 \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]}

 \def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}

 \def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}

 \def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}

 Sledgehammer's options are categorized as follows:\ mode of operation

 (\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),

 relevance filter (\S\ref{relevance-filter}), output format

 (\S\ref{output-format}), authentication (\S\ref{authentication}), and timeouts

 (\S\ref{timeouts}).

 The descriptions below refer to the following syntactic quantities:

 \begin{enum}

 \item[$\bullet$] \qtybf{string}: A string.

 \item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.

 \item[$\bullet$] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or

 \textit{smart}.

 \item[$\bullet$] \qtybf{int\/}: An integer.

 %\item[$\bullet$] \qtybf{float\/}: A floating-point number (e.g., 2.5).

 \item[$\bullet$] \qtybf{float\_pair\/}: A pair of floating-point numbers

 (e.g., 0.6 0.95).

 \item[$\bullet$] \qtybf{smart\_int\/}: An integer or \textit{smart}.

 \item[$\bullet$] \qtybf{float\_or\_none\/}: A floating-point number (e.g., 60 or

 0.5) expressing a number of seconds, or the keyword \textit{none} ($\infty$

 seconds).

 \end{enum}

 Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options

 have a negated counterpart (e.g., \textit{blocking} vs.\

 \textit{non\_blocking}). When setting them, ``= \textit{true}'' may be omitted.

 \subsection{Mode of Operation}

 \label{mode-of-operation}

 \begin{enum}

 \opnodefaultbrk{provers}{string}

 Specifies the automatic provers to use as a space-separated list (e.g.,

 ``\textit{e}~\textit{spass}~\textit{remote\_vampire}''). The following local

 provers are supported:

 \begin{enum}

 \item[$\bullet$] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by

 Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,

 set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the

 executable, including the file name. Sledgehammer has been tested with version

 2.2.

 \item[$\bullet$] \textbf{\textit{e}:} E is a first-order resolution prover

 developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment

 variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}

 executable, or install the prebuilt E package from Isabelle's download page. See

 \S\ref{installation} for details.

 \item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic

 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},

 with support for the TPTP many-typed higher-order syntax (THF0).

 \item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than

 the external provers, Metis itself can be used for proof search.

 \item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of

 Metis, corresponding to \textit{metis} (\textit{full\_types}).

 \item[$\bullet$] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis,

 corresponding to \textit{metis} (\textit{no\_types}).

 \item[$\bullet$] \textbf{\textit{satallax}:} Satallax is an automatic

 higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with

 support for the TPTP many-typed higher-order syntax (THF0).

 \item[$\bullet$] \textbf{\textit{spass}:} SPASS is a first-order resolution

 prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.

 To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory

 that contains the \texttt{SPASS} executable, or install the prebuilt SPASS

 package from Isabelle's download page. Sledgehammer requires version 3.5 or

 above. See \S\ref{installation} for details.

 \item[$\bullet$] \textbf{\textit{vampire}:} Vampire is a first-order resolution

 prover developed by Andrei Voronkov and his colleagues

 \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable

 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}

 executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``1.8'').

 Sledgehammer has been tested with versions 0.6, 1.0, and 1.8. Vampire 1.8

 supports the TPTP many-typed first-order format (TFF0).

 \item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at

 SRI \cite{yices}. To use Yices, set the environment variable

 \texttt{YICES\_SOLVER} to the complete path of the executable, including the

 file name. Sledgehammer has been tested with version 1.0.

 \item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at

 Microsoft Research \cite{z3}. To use Z3, set the environment variable

 \texttt{Z3\_SOLVER} to the complete path of the executable, including the file

 name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a

 noncommercial user. Sledgehammer has been tested with versions 2.7 to 2.18.

 \item[$\bullet$] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be

 an ATP, exploiting Z3's support for the TPTP untyped and many-typed first-order

 formats (FOF and TFF0). It is included for experimental purposes. It requires

 version 3.0 or above.

 \end{enum}

 In addition, the following remote provers are supported:

 \begin{enum}

 \item[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs

 on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to

 point).

 \item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs

 on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.

 \item[$\bullet$] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover

 developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of

 SInE runs on Geoff Sutcliffe's Miami servers.

 \item[$\bullet$] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover

 developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami

 servers. This ATP supports the TPTP many-typed first-order format (TFF0). The

 remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.

 \item[$\bullet$] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II

 runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.

 \item[$\bullet$] \textbf{\textit{remote\_satallax}:} The remote version of

 Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.

 \item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a first-order

 resolution prover developed by Stickel et al.\ \cite{snark}. It supports the

 TPTP many-typed first-order format (TFF0). The remote version of SNARK runs on

 Geoff Sutcliffe's Miami servers.

 \item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of

 Vampire runs on Geoff Sutcliffe's Miami servers. Version 1.8 is used.

 \item[$\bullet$] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit

 equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be

 used to prove universally quantified equations using unconditional equations,

 corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister

 runs on Geoff Sutcliffe's Miami servers.

 \item[$\bullet$] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on

 servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to

 point).

 \item[$\bullet$] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3

 with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.

 \end{enum}

 By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever

 the SMT module's \textit{smt\_solver} configuration option is set to), and (if

 appropriate) Waldmeister in parallel---either locally or remotely, depending on

 the number of processor cores available. For historical reasons, the default

 value of this option can be overridden using the option ``Sledgehammer:

 Provers'' in Proof General's ``Isabelle'' menu.

 It is generally a good idea to run several provers in parallel. Running E,

 SPASS, and Vampire for 5~seconds yields a similar success rate to running the

 most effective of these for 120~seconds \cite{boehme-nipkow-2010}.

 For the \textit{min} subcommand, the default prover is \textit{metis}. If

 several provers are set, the first one is used.

 \opnodefault{prover}{string}

 Alias for \textit{provers}.

 %\opnodefault{atps}{string}

 %Legacy alias for \textit{provers}.

 %\opnodefault{atp}{string}

 %Legacy alias for \textit{provers}.

 \opfalse{blocking}{non\_blocking}

 Specifies whether the \textbf{sledgehammer} command should operate

 synchronously. The asynchronous (non-blocking) mode lets the user start proving

 the putative theorem manually while Sledgehammer looks for a proof, but it can

 also be more confusing. Irrespective of the value of this option, Sledgehammer

 is always run synchronously for the new jEdit-based user interface or if

 \textit{debug} (\S\ref{output-format}) is enabled.

 \optrue{slicing}{no\_slicing}

 Specifies whether the time allocated to a prover should be sliced into several

 segments, each of which has its own set of possibly prover-dependent options.

 For SPASS and Vampire, the first slice tries the fast but incomplete

 set-of-support (SOS) strategy, whereas the second slice runs without it. For E,

 up to three slices are tried, with different weighted search strategies and

 number of facts. For SMT solvers, several slices are tried with the same options

 each time but fewer and fewer facts. According to benchmarks with a timeout of

 30 seconds, slicing is a valuable optimization, and you should probably leave it

 enabled unless you are conducting experiments. This option is implicitly

 disabled for (short) automatic runs.

 \nopagebreak

 {\small See also \textit{verbose} (\S\ref{output-format}).}

 \opfalse{overlord}{no\_overlord}

 Specifies whether Sledgehammer should put its temporary files in

 \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for

 debugging Sledgehammer but also unsafe if several instances of the tool are run

 simultaneously. The files are identified by the prefix \texttt{prob\_}; you may

 safely remove them after Sledgehammer has run.

 \nopagebreak

 {\small See also \textit{debug} (\S\ref{output-format}).}

 \end{enum}

 \subsection{Problem Encoding}

 \label{problem-encoding}

 \begin{enum}

 \opdefault{type\_enc}{string}{smart}

 Specifies the type encoding to use in ATP problems. Some of the type encodings

 are unsound, meaning that they can give rise to spurious proofs

 (unreconstructible using Metis). The supported type encodings are listed below,

 with an indication of their soundness in parentheses:

 \begin{enum}

 \item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is

 supplied to the ATP. Types are simply erased.

 \item[$\bullet$] \textbf{\textit{poly\_guards} (sound):} Types are encoded using

 a predicate \textit{has\_\allowbreak type\/}$(\tau, t)$ that guards bound

 variables. Constants are annotated with their types, supplied as additional

 arguments, to resolve overloading.

 \item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is

 tagged with its type using a function $\mathit{type\/}(\tau, t)$.

 \item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}

 Like for \textit{poly\_guards} constants are annotated with their types to

 resolve overloading, but otherwise no type information is encoded. This

 coincides with the default encoding used by the \textit{metis} command.

 \item[$\bullet$]

 \textbf{%

 \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\

 \textit{raw\_mono\_args} (unsound):} \\

 Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args},

 respectively, but the problem is additionally monomorphized, meaning that type

 variables are instantiated with heuristically chosen ground types.

 Monomorphization can simplify reasoning but also leads to larger fact bases,

 which can slow down the ATPs.

 \item[$\bullet$]

 \textbf{%

 \textit{mono\_guards}, \textit{mono\_tags} (sound);

 \textit{mono\_args} (unsound):} \\

 Similar to

 \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and

 \textit{raw\_mono\_args}, respectively but types are mangled in constant names

 instead of being supplied as ground term arguments. The binary predicate

 $\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate

 $\mathit{has\_type\_}\tau(t)$, and the binary function

 $\mathit{type\/}(\tau, t)$ becomes a unary function

 $\mathit{type\_}\tau(t)$.

 \item[$\bullet$] \textbf{\textit{mono\_simple} (sound):} Exploits simple

 first-order types if the prover supports the TFF0 or THF0 syntax; otherwise,

 falls back on \textit{mono\_guards}. The problem is monomorphized.

 \item[$\bullet$] \textbf{\textit{mono\_simple\_higher} (sound):} Exploits simple

 higher-order types if the prover supports the THF0 syntax; otherwise, falls back

 on \textit{mono\_simple} or \textit{mono\_guards}. The problem is monomorphized.

 \item[$\bullet$]

 \textbf{%

 \textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\

 \textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\

 \textit{mono\_simple}? (quasi-sound):} \\

 The type encodings \textit{poly\_guards}, \textit{poly\_tags},

 \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},

 \textit{mono\_tags}, and \textit{mono\_simple} are fully

 typed and sound. For each of these, Sledgehammer also provides a lighter,

 virtually sound variant identified by a question mark (`\hbox{?}')\ that detects

 and erases monotonic types, notably infinite types. (For \textit{mono\_simple},

 the types are not actually erased but rather replaced by a shared uniform type

 of individuals.) As argument to the \textit{metis} proof method, the question

 mark is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound}

 option is enabled, these encodings are fully sound.

 \item[$\bullet$]

 \textbf{%

 \textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\

 \textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\

 (quasi-sound):} \\

 Even lighter versions of the `\hbox{?}' encodings. As argument to the

 \textit{metis} proof method, the `\hbox{??}' suffix is replaced by

 \hbox{``\textit{\_query\_query}''}.

 \item[$\bullet$]

 \textbf{%

 \textit{poly\_guards}@?, \textit{poly\_tags}@?, \textit{raw\_mono\_guards}@?, \\

 \textit{raw\_mono\_tags}@? (quasi-sound):} \\

 Alternative versions of the `\hbox{??}' encodings. As argument to the

 \textit{metis} proof method, the `\hbox{@?}' suffix is replaced by

 \hbox{``\textit{\_at\_query}''}.

 \item[$\bullet$]

 \textbf{%

 \textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\

 \textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\

 \textit{mono\_simple}!, \textit{mono\_simple\_higher}! (mildly unsound):} \\

 The type encodings \textit{poly\_guards}, \textit{poly\_tags},

 \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},

 \textit{mono\_tags}, \textit{mono\_simple}, and \textit{mono\_simple\_higher}

 also admit a mildly unsound (but very efficient) variant identified by an

 exclamation mark (`\hbox{!}') that detects and erases erases all types except

 those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple}

 and \textit{mono\_simple\_higher}, the types are not actually erased but rather

 replaced by a shared uniform type of individuals.) As argument to the

 \textit{metis} proof method, the exclamation mark is replaced by the suffix

 \hbox{``\textit{\_bang}''}.

 \item[$\bullet$]

 \textbf{%

 \textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\

 \textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\

 (mildly unsound):} \\

 Even lighter versions of the `\hbox{!}' encodings. As argument to the

 \textit{metis} proof method, the `\hbox{!!}' suffix is replaced by

 \hbox{``\textit{\_bang\_bang}''}.

 \item[$\bullet$]

 \textbf{%

 \textit{poly\_guards}@!, \textit{poly\_tags}@!, \textit{raw\_mono\_guards}@!, \\

 \textit{raw\_mono\_tags}@! (mildly unsound):} \\

 Alternative versions of the `\hbox{!!}' encodings. As argument to the

 \textit{metis} proof method, the `\hbox{@!}' suffix is replaced by

 \hbox{``\textit{\_at\_bang}''}.

 \item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on

 the ATP and should be the most efficient virtually sound encoding for that ATP.

 \end{enum}

 For SMT solvers, the type encoding is always \textit{mono\_simple}, irrespective

 of the value of this option.

 \nopagebreak

 {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})

 and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).}

 \opfalse{sound}{unsound}

 Specifies whether Sledgehammer should run in its fully sound mode. In that mode,

 quasi-sound type encodings (which are the default) are made fully sound, at the

 cost of some clutter in the generated problems. This option is ignored if

 \textit{type\_enc} is explicitly set to an unsound encoding.

 \end{enum}

 \subsection{Relevance Filter}

 \label{relevance-filter}

 \begin{enum}

 \opdefault{relevance\_thresholds}{float\_pair}{\upshape 0.45~0.85}

 Specifies the thresholds above which facts are considered relevant by the

 relevance filter. The first threshold is used for the first iteration of the

 relevance filter and the second threshold is used for the last iteration (if it

 is reached). The effective threshold is quadratically interpolated for the other

 iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems

 are relevant and 1 only theorems that refer to previously seen constants.

 \opdefault{max\_relevant}{smart\_int}{smart}

 Specifies the maximum number of facts that may be returned by the relevance

 filter. If the option is set to \textit{smart}, it is set to a value that was

 empirically found to be appropriate for the prover. A typical value would be

 250.

 \opdefault{max\_new\_mono\_instances}{int}{\upshape 200}

 Specifies the maximum number of monomorphic instances to generate beyond

 \textit{max\_relevant}. The higher this limit is, the more monomorphic instances

 are potentially generated. Whether monomorphization takes place depends on the

 type encoding used.

 \nopagebreak

 {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}

 \opdefault{max\_mono\_iters}{int}{\upshape 3}

 Specifies the maximum number of iterations for the monomorphization fixpoint

 construction. The higher this limit is, the more monomorphic instances are

 potentially generated. Whether monomorphization takes place depends on the

 type encoding used.

 \nopagebreak

 {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}

 \end{enum}

 \subsection{Output Format}

 \label{output-format}

 \begin{enum}

 \opfalse{verbose}{quiet}

 Specifies whether the \textbf{sledgehammer} command should explain what it does.

 This option is implicitly disabled for automatic runs.

 \opfalse{debug}{no\_debug}

 Specifies whether Sledgehammer should display additional debugging information

 beyond what \textit{verbose} already displays. Enabling \textit{debug} also

 enables \textit{verbose} and \textit{blocking} (\S\ref{mode-of-operation})

 behind the scenes. The \textit{debug} option is implicitly disabled for

 automatic runs.

 \nopagebreak

 {\small See also \textit{overlord} (\S\ref{mode-of-operation}).}

 \opfalse{isar\_proof}{no\_isar\_proof}

 Specifies whether Isar proofs should be output in addition to one-liner

 \textit{metis} proofs. Isar proof construction is still experimental and often

 fails; however, they are usually faster and sometimes more robust than

 \textit{metis} proofs.

 \opdefault{isar\_shrink\_factor}{int}{\upshape 1}

 Specifies the granularity of the Isar proof. A value of $n$ indicates that each

 Isar proof step should correspond to a group of up to $n$ consecutive proof

 steps in the ATP proof.

 \end{enum}

 \subsection{Authentication}

 \label{authentication}

 \begin{enum}

 \opnodefault{expect}{string}

 Specifies the expected outcome, which must be one of the following:

 \begin{enum}

 \item[$\bullet$] \textbf{\textit{some}:} Sledgehammer found a (potentially

 unsound) proof.

 \item[$\bullet$] \textbf{\textit{none}:} Sledgehammer found no proof.

 \item[$\bullet$] \textbf{\textit{timeout}:} Sledgehammer timed out.

 \item[$\bullet$] \textbf{\textit{unknown}:} Sledgehammer encountered some

 problem.

 \end{enum}

 Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning

 (otherwise) if the actual outcome differs from the expected outcome. This option

 is useful for regression testing.

 \nopagebreak

 {\small See also \textit{blocking} (\S\ref{mode-of-operation}) and

 \textit{timeout} (\S\ref{timeouts}).}

 \end{enum}

 \subsection{Timeouts}

 \label{timeouts}

 \begin{enum}

 \opdefault{timeout}{float\_or\_none}{\upshape 30}

 Specifies the maximum number of seconds that the automatic provers should spend

 searching for a proof. This excludes problem preparation and is a soft limit.

 For historical reasons, the default value of this option can be overridden using

 the option ``Sledgehammer: Time Limit'' in Proof General's ``Isabelle'' menu.

 \opdefault{preplay\_timeout}{float\_or\_none}{\upshape 4}

 Specifies the maximum number of seconds that Metis should be spent trying to

 ``preplay'' the found proof. If this option is set to 0, no preplaying takes

 place, and no timing information is displayed next to the suggested Metis calls.

 \end{enum}

 \let\em=\sl

 \bibliography{../manual}{}

 \bibliographystyle{abbrv}

 \end{document}