\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}

\newcommand\download{\url{http://www21.in.tum.de/~blanchet/\#software}}

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

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

\newcommand\const[1]{\textsf{#1}}

%\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}

%%% TYPESETTING

%\renewcommand\labelitemi{$\bullet$}

\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}

\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 Alt-Ergo \cite{alt-ergo}, CVC3 \cite{cvc3}, and Yices \cite{yices} as

well; these are run either locally or (for CVC3 and Z3) 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 \textit{metis} proof method, which

integrates the Metis ATP in 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 provers (ATPs and SMT solvers).

Among the ATPs, E, LEO-II, Satallax, SPASS, and Vampire can be run locally; in

addition, E, E-SInE, E-ToFoF, iProver, iProver-Eq, 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.

Among the SMT solvers, Alt-Ergo, CVC3, Yices, and Z3 can be run locally, and

CVC3 and Z3 can be run 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 without an Internet connection, you should at least install Z3

locally.

There are three main ways to install automatic provers on your machine:

\begin{sloppy}

\begin{enum}

\item[\labelitemi] If you installed an official Isabelle package, it should

already include properly setup executables for CVC3, E, SPASS, and Z3, ready to use.%

\footnote{Vampire's and Yices's licenses prevent us from doing the same for

these otherwise remarkable tools.}

For Z3, you must additionally set the variable

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

noncommercial user, either in the environment in which Isabelle is

launched or in your

\texttt{\char`\~/\$ISABELLE\_HOME\_USER/etc/settings} file.

\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, E,

SPASS, and Z3 binary packages from \download. Extract the archives, then add a

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

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

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

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

file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the

\texttt{components} file does not exist yet and you extracted SPASS to

\texttt{/usr/local/spass-3.7}, create it with the single line

\prew

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

\postw

(including an invisible newline character) in it.

\item[\labelitemi] If you prefer to build E, LEO-II, Satallax, or SPASS

manually, or found a Vampire executable somewhere (e.g.,

\url{http://www.vprover.org/}), set the environment variable \texttt{E\_HOME},

\texttt{LEO2\_HOME}, \texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or

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

\texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable.

Sledgehammer has been tested with E 1.0 to 1.4, LEO-II 1.2.9, Satallax 2.2,

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 9.0 or 11.5.}%

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

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

also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},

\texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or

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

Similarly, if you want to build Alt-Ergo or CVC3, or found a

Yices or Z3 executable somewhere (e.g.,

\url{http://yices.csl.sri.com/download.shtml} or

\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html}),

set the environment variable \texttt{CVC3\_\allowbreak SOLVER},

\texttt{YICES\_SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of

the executable, \emph{including the file name}. Sledgehammer has been tested

with Alt-Ergo 0.93, CVC3 2.2, Yices 1.0.28, and Z3 3.0 to 3.2.

Since the SMT solvers' output formats are somewhat unstable, other

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

also set \texttt{CVC3\_VERSION}, \texttt{YICES\_VERSION}, or

\texttt{Z3\_VERSION} to the solver's version number (e.g., ``3.2'').

\end{enum}

\end{sloppy}

To check whether E, SPASS, Vampire, and/or Z3 are successfully installed, try

out the example in \S\ref{first-steps}. If the remote versions of any of these

provers is used (identified by the prefix ``\emph{remote\_\/}''), or if the

local versions fail to solve the easy goal presented there, something must be

wrong with the installation.

Remote prover invocation 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

\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{z3\/}'' on goal \\

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

Try this: \textbf{by} (\textit{metis list.inject}) (20 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).

\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

the \textit{metis} or \textit{smt} proof method. 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 \textit{metis} or \textit{smt} 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. Frequently asked questions are answered in

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

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

\newcommand\point[1]{\subsection{\emph{#1}}}

\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 E, SPASS, Vampire, and Z3 are locally 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[\labelitemi] \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[\labelitemi] \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[\labelitemi] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies

that Isar proofs should be generated, instead of one-liner \textit{metis} or

\textit{smt} proofs. The length of the Isar proofs can be controlled by setting

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

\item[\labelitemi] \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{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 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[\labelitemi] Try the \textit{isar\_proof} option (\S\ref{output-format}) to

obtain a step-by-step Isar proof where each step is justified by \textit{metis}.

Since the steps are fairly small, \textit{metis} is more likely to be able to

replay them.

\item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}. It

is usually stronger, but you need to either 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[\labelitemi] 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, \textit{metis} fails fairly quickly, and you get the error

message

\prew

\slshape

One-line proof reconstruction failed.

\postw

This message indicates that Sledgehammer determined that the goal is provable,

but the proof is, for technical reasons, beyond \textit{metis}'s power. You can

then try again with the \textit{strict} option (\S\ref{problem-encoding}).

If the goal is actually unprovable and you did not specify an unsound encoding

using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are

strongly encouraged to report this to the author at \authoremail.

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

The current implementation of the Isar proof feature,

enabled by the \textit{isar\_proof} option (\S\ref{output-format}),

is highly experimental. 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{How can I tell whether a suggested proof is sound?}

Earlier versions of Sledgehammer often suggested unsound proofs---either proofs

of nontheorems or simply proofs that rely on type-unsound inferences. This

is a thing of the past, unless you explicitly specify an unsound encoding

using \textit{type\_enc} (\S\ref{problem-encoding}).

%

Officially, the only form of ``unsoundness'' that lurks in the sound

encodings is related to missing characteristic theorems of datatypes. For

example,

\prew

\textbf{lemma}~``$\exists \mathit{xs}.\; \mathit{xs} \neq []$'' \\

\textbf{sledgehammer} ()

\postw

suggests an argumentless \textit{metis} call that fails. However, the conjecture

does actually hold, and the \textit{metis} call can be repaired by adding

\textit{list.distinct}.

%

We hope to address this problem in a future version of Isabelle. In the

meantime, you can avoid it by passing the \textit{strict} option

(\S\ref{problem-encoding}).

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

\textit{mono\_tags} arguments to Metis?}

The \textit{metis}~(\textit{full\_types}) proof method

and its cousin \textit{metis}~(\textit{mono\_tags}) are 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 = \const{True} \mathrel{\lor} x = \const{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 3 seconds each time to ensure that the generated

one-line proofs actually work and to display timing information. This can be

configured using the \textit{preplay\_timeout} and \textit{dont\_preplay}

options (\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.

%

See the \textit{type\_enc} option (\S\ref{problem-encoding}) for details.

Incidentally, if you ever see warnings such as

\prew

\slshape

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

\postw

for a successful \textit{metis} proof, you can advantageously pass the

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

\point{And what are the \textit{lifting} and \textit{hide\_lams} arguments

to Metis?}

Orthogonally to the encoding of types, it is important to choose an appropriate

translation of $\lambda$-abstractions. Metis supports three translation schemes,

in decreasing order of power: Curry combinators (the default),

$\lambda$-lifting, and a ``hiding'' scheme that disables all reasoning under

$\lambda$-abstractions. The more powerful schemes also give the automatic

provers more rope to hang themselves. See the \textit{lam\_trans} option (\S\ref{problem-encoding}) for details.

\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, \textit{metis}, or

\textit{smt} 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 or preplay it).

In addition, some provers (e.g., 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 initially 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.

%

Automatic minimization can be forced or disabled using the \textit{minimize}

option (\S\ref{mode-of-operation}).

\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}

\subsection{Sledgehammer}

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[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on

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

\item[\labelitemi] \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[\labelitemi] \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[\labelitemi] \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[\labelitemi] \textbf{\textit{running\_provers}:} Prints information about

currently running automatic provers, including elapsed runtime and remaining

time until timeout.

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

automatic provers.

\item[\labelitemi] \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{slice} (\S\ref{mode-of-operation}) is disabled, \textit{strict}

(\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.

\subsection{Metis}

The \textit{metis} proof method has the syntax

\prew

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

\postw

where \qty{facts} is a list of arbitrary facts and \qty{options} is a

comma-separated list consisting of at most one $\lambda$ translation scheme

specification with the same semantics as Sledgehammer's \textit{lam\_trans}

option (\S\ref{problem-encoding}) and at most one type encoding specification

with the same semantics as Sledgehammer's \textit{type\_enc} option

(\S\ref{problem-encoding}).

%

The supported $\lambda$ translation schemes are \textit{hide\_lams},

\textit{lifting}, and \textit{combs} (the default).

%

All the untyped type encodings listed in \S\ref{problem-encoding} are supported.

For convenience, the following aliases are provided:

\begin{enum}

\item[\labelitemi] \textbf{\textit{full\_types}:} Synonym for \textit{poly\_guards\_query}.

\item[\labelitemi] \textbf{\textit{partial\_types}:} Synonym for \textit{poly\_args}.

\item[\labelitemi] \textbf{\textit{no\_types}:} Synonym for \textit{erased}.

\end{enum}

\section{Option Reference}

\label{option-reference}

\def\defl{\{}

\def\defr{\}}

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

\def\optrueonly#1{\flushitem{\textit{#1} $\bigl[$= \textit{true}$\bigr]$\enskip}\nopagebreak\\[\parskip]}

\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\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\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[\labelitemi] \qtybf{string}: A string.

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

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

\textit{smart}.

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

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

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

(e.g., 0.6 0.95).

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

\item[\labelitemi] \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\/}'').

Provers can be run locally or remotely; see \S\ref{installation} for

installation instructions.

The following local provers are supported:

\begin{enum}

\item[\labelitemi] \textbf{\textit{alt\_ergo}:} Alt-Ergo is a polymorphic

SMT solver developed by Bobot et al.\ \cite{alt-ergo}.

It supports the TPTP polymorphic typed first-order format (TFF1) via Why3

\cite{why3}. It is included for experimental purposes. To use Alt-Ergo, set the

environment variable \texttt{WHY3\_HOME} to the directory that contains the

\texttt{why3} executable. Sledgehammer has been tested with Alt-Ergo 0.93 and an

unidentified development version of Why3.

\item[\labelitemi] \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, or install the prebuilt CVC3 package from

\download. Sledgehammer has been tested with version 2.2.

\item[\labelitemi] \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 \download. Sledgehammer has

been tested with versions 1.0 to 1.4.

\item[\labelitemi] \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 typed higher-order syntax (THF0). To use LEO-II, set

the environment variable \texttt{LEO2\_HOME} to the directory that contains the

\texttt{leo} executable. Sledgehammer requires version 1.2.9 or above.

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

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

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

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

support for the TPTP typed higher-order syntax (THF0). To use Satallax, set the

environment variable \texttt{SATALLAX\_HOME} to the directory that contains the

\texttt{satallax} executable. Sledgehammer requires version 2.2 or above.

\item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt} proof method with the

current settings (usually:\ Z3 with proof reconstruction).

\item[\labelitemi] \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 \download. Sledgehammer requires version 3.5 or above.

\item[\labelitemi] \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.

Versions above 1.8 support the TPTP typed first-order format (TFF0).

\item[\labelitemi] \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.28.

\item[\labelitemi] \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 3.0 to 3.2.

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

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

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

requires version 3.0 or above. To use it, set the environment variable

\texttt{Z3\_HOME} to the directory that contains the \texttt{z3}

executable.

\end{enum}

The following remote provers are supported:

\begin{enum}

\item[\labelitemi] \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[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs

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

\item[\labelitemi] \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

E-SInE runs on Geoff Sutcliffe's Miami servers.

\item[\labelitemi] \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 typed first-order format (TFF0). The

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

\item[\labelitemi] \textbf{\textit{remote\_iprover}:} iProver is a pure

instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. The

remote version of iProver runs on Geoff Sutcliffe's Miami servers

\cite{sutcliffe-2000}.

\item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} iProver-Eq is an

instantiation-based prover with native support for equality developed by

Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. The

remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers

\cite{sutcliffe-2000}.

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

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

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

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

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

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

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

Geoff Sutcliffe's Miami servers.

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

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

\item[\labelitemi] \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[\labelitemi] \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[\labelitemi] \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}.

\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{slice}{dont\_slice}

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}).}

\opsmart{minimize}{dont\_minimize}

Specifies whether the minimization tool should be invoked automatically after

proof search. By default, automatic minimization takes place only if

it can be done in a reasonable amount of time (as determined by

the number of facts in the original proof and the time it took to find or

preplay it) or the proof involves an unreasonably large number of facts.

\nopagebreak

{\small See also \textit{preplay\_timeout} (\S\ref{timeouts})

and \textit{dont\_preplay} (\S\ref{timeouts}).}

\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}

\newcommand\comb[1]{\const{#1}}

\begin{enum}

\opdefault{lam\_trans}{string}{smart}

Specifies the $\lambda$ translation scheme to use in ATP problems. The supported

translation schemes are listed below:

\begin{enum}

\item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$-abstractions

by replacing them by unspecified fresh constants, effectively disabling all

reasoning under $\lambda$-abstractions.

\item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new

supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions,

defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting).

\item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry

combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators

enable the ATPs to synthesize $\lambda$-terms but tend to yield bulkier formulas

than $\lambda$-lifting: The translation is quadratic in the worst case, and the

equational definitions of the combinators are very prolific in the context of

resolution.