
blanchet@36918: \documentclass[a4paper,12pt]{article}
blanchet@36918: \usepackage[T1]{fontenc}
blanchet@36918: \usepackage{amsmath}
blanchet@36918: \usepackage{amssymb}
blanchet@36918: \usepackage[english,french]{babel}
blanchet@36918: \usepackage{color}
blanchet@36918: \usepackage{footmisc}
blanchet@36918: \usepackage{graphicx}
blanchet@36918: %\usepackage{mathpazo}
blanchet@36918: \usepackage{multicol}
blanchet@36918: \usepackage{stmaryrd}
blanchet@36918: %\usepackage[scaled=.85]{beramono}
blanchet@36918: \usepackage{../iman,../pdfsetup}
blanchet@36918: 
blanchet@36918: %\oddsidemargin=4.6mm
blanchet@36918: %\evensidemargin=4.6mm
blanchet@36918: %\textwidth=150mm
blanchet@36918: %\topmargin=4.6mm
blanchet@36918: %\headheight=0mm
blanchet@36918: %\headsep=0mm
blanchet@36918: %\textheight=234mm
blanchet@36918: 
blanchet@36918: \def\Colon{\mathord{:\mkern-1.5mu:}}
blanchet@36918: %\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
blanchet@36918: %\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
blanchet@36918: \def\lparr{\mathopen{(\mkern-4mu\mid}}
blanchet@36918: \def\rparr{\mathclose{\mid\mkern-4mu)}}
blanchet@36918: 
blanchet@36918: \def\unk{{?}}
blanchet@36918: \def\undef{(\lambda x.\; \unk)}
blanchet@36918: %\def\unr{\textit{others}}
blanchet@36918: \def\unr{\ldots}
blanchet@36918: \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
blanchet@36918: \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
blanchet@36918: 
blanchet@36918: \urlstyle{tt}
blanchet@36918: 
blanchet@36918: \begin{document}
blanchet@36918: 
blanchet@36918: \selectlanguage{english}
blanchet@36918: 
blanchet@36918: \title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
blanchet@36918: Hammering Away \\[\smallskipamount]
blanchet@36918: \Large A User's Guide to Sledgehammer for Isabelle/HOL}
blanchet@36918: \author{\hbox{} \\
blanchet@36918: Jasmin Christian Blanchette \\
blanchet@36918: {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
blanchet@36918: \hbox{}}
blanchet@36918: 
blanchet@36918: \maketitle
blanchet@36918: 
blanchet@36918: \tableofcontents
blanchet@36918: 
blanchet@36918: \setlength{\parskip}{.7em plus .2em minus .1em}
blanchet@36918: \setlength{\parindent}{0pt}
blanchet@36918: \setlength{\abovedisplayskip}{\parskip}
blanchet@36918: \setlength{\abovedisplayshortskip}{.9\parskip}
blanchet@36918: \setlength{\belowdisplayskip}{\parskip}
blanchet@36918: \setlength{\belowdisplayshortskip}{.9\parskip}
blanchet@36918: 
blanchet@36918: % General-purpose enum environment with correct spacing
blanchet@36918: \newenvironment{enum}%
blanchet@36918:     {\begin{list}{}{%
blanchet@36918:         \setlength{\topsep}{.1\parskip}%
blanchet@36918:         \setlength{\partopsep}{.1\parskip}%
blanchet@36918:         \setlength{\itemsep}{\parskip}%
blanchet@36918:         \advance\itemsep by-\parsep}}
blanchet@36918:     {\end{list}}
blanchet@36918: 
blanchet@36918: \def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
blanchet@36918: \advance\rightskip by\leftmargin}
blanchet@36918: \def\post{\vskip0pt plus1ex\endgroup}
blanchet@36918: 
blanchet@36918: \def\prew{\pre\advance\rightskip by-\leftmargin}
blanchet@36918: \def\postw{\post}
blanchet@36918: 
blanchet@36918: \section{Introduction}
blanchet@36918: \label{introduction}
blanchet@36918: 
blanchet@36918: Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs)
blanchet@36918: on the current goal. The supported ATPs are E \cite{schulz-2002}, SPASS
blanchet@36918: \cite{weidenbach-et-al-2009}, and Vampire \cite{riazanov-voronkov-2002}, which
blanchet@36918: can be run locally or remotely via the SystemOnTPTP web service
blanchet@36918: \cite{sutcliffe-2000}.
blanchet@36918: 
blanchet@36918: The problem passed to ATPs consists of the current goal together with a
blanchet@36918: heuristic selection of facts (theorems) from the current theory context,
blanchet@36918: filtered by relevance. The result of a successful ATP proof search is some
blanchet@36918: source text that usually (but not always) reconstructs the proof within
blanchet@36918: Isabelle, without requiring the ATPs again. The reconstructed proof relies on
blanchet@36918: the general-purpose Metis prover \cite{metis}, which is fully integrated into
blanchet@36918: Isabelle/HOL, with explicit inferences going through the kernel. Thus its
blanchet@36918: results are correct by construction.
blanchet@36918: 
blanchet@36918: \newbox\boxA
blanchet@36918: \setbox\boxA=\hbox{\texttt{nospam}}
blanchet@36918: 
blanchet@36918: Examples of Sledgehammer use can be found in Isabelle's
blanchet@36918: \texttt{src/HOL/Metis\_Examples} directory.
blanchet@36918: Comments and bug reports concerning Sledgehammer or this manual should be
blanchet@36918: directed to
blanchet@36918: \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
blanchet@36918: in.\allowbreak tum.\allowbreak de}.
blanchet@36918: 
blanchet@36918: \vskip2.5\smallskipamount
blanchet@36918: 
blanchet@36918: %\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
blanchet@36918: %suggesting several textual improvements.
blanchet@36918: 
blanchet@36918: \section{Installation}
blanchet@36918: \label{installation}
blanchet@36918: 
blanchet@36918: Sledgehammer is part of Isabelle, so you don't need to install it. However, it
blanchet@36918: relies on third-party automatic theorem provers (ATPs). Currently, E, SPASS, and
blanchet@36918: Vampire are supported. All of these are available remotely via SystemOnTPTP
blanchet@36918: \cite{sutcliffe-2000}, but if you want better performance you will need to
blanchet@36918: install at least E and SPASS locally.
blanchet@36918: 
blanchet@36918: There are three main ways to install E and SPASS:
blanchet@36918: 
blanchet@36918: \begin{enum}
blanchet@36918: \item[$\bullet$] If you installed an official Isabelle package with everything
blanchet@36918: inside, it should already include properly setup executables for E and SPASS,
blanchet@36918: ready to use.
blanchet@36918: 
blanchet@36918: \item[$\bullet$] Otherwise, you can download the Isabelle-aware E and SPASS
blanchet@36918: binary packages from Isabelle's download page. Extract the archives, then add a
blanchet@36918: line to your \texttt{\char`\~/.isabelle/etc/components} file with the absolute path to
blanchet@36918: E or SPASS. For example, if \texttt{\char`\~/.isabelle/etc/components} does not exist
blanchet@36918: yet and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create
blanchet@36918: the file \texttt{\char`\~/.isabelle/etc/components} with the single line
blanchet@36918: 
blanchet@36918: \prew
blanchet@36918: \texttt{/usr/local/spass-3.7}
blanchet@36918: \postw
blanchet@36918: 
blanchet@36918: \item[$\bullet$] If you prefer to build E or SPASS yourself, feel free to do so
blanchet@36918: and set the environment variable \texttt{E\_HOME} or \texttt{SPASS\_HOME} to the
blanchet@36918: directory that contains the \texttt{eproof} or \texttt{SPASS} executable,
blanchet@36918: respectively.
blanchet@36918: \end{enum}
blanchet@36918: 
blanchet@36918: To check whether E and SPASS are installed, follow the example in
blanchet@36918: \S\ref{first-steps}.
blanchet@36918: 
blanchet@36918: \section{First Steps}
blanchet@36918: \label{first-steps}
blanchet@36918: 
blanchet@36918: To illustrate Sledgehammer in context, let us start a theory file and
blanchet@36918: attempt to prove a simple lemma:
blanchet@36918: 
blanchet@36918: \prew
blanchet@36918: \textbf{theory}~\textit{Scratch} \\
blanchet@36918: \textbf{imports}~\textit{Main} \\
blanchet@36918: \textbf{begin} \\[2\smallskipamount]
blanchet@36918: %
blanchet@36918: \textbf{lemma} ``$[a] = [b] \,\longleftrightarrow\, a = b$'' \\
blanchet@36918: \textbf{sledgehammer}
blanchet@36918: \postw
blanchet@36918: 
blanchet@36918: After a few seconds, Sledgehammer produces the following output:
blanchet@36918: 
blanchet@36918: \prew
blanchet@36918: \slshape
blanchet@36918: Sledgehammer: ATP ``\textit{e}'' for subgoal 1: \\
blanchet@36918: $([a] = [b]) = (a = b)$ \\
blanchet@36918: Try this command: \textbf{by} (\textit{metis hd.simps}). \\
blanchet@36918: To minimize the number of lemmas, try this command: \\
blanchet@36918: \textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
blanchet@36918: %
blanchet@36918: Sledgehammer: ATP ``\textit{spass}'' for subgoal 1: \\
blanchet@36918: $([a] = [b]) = (a = b)$ \\
blanchet@36918: Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
blanchet@36918: To minimize the number of lemmas, try this command: \\
blanchet@36918: \textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
blanchet@36918: %
blanchet@36918: Sledgehammer: ATP ``\textit{remote\_vampire}'' for subgoal 1: \\
blanchet@36918: $([a] = [b]) = (a = b)$ \\
blanchet@36918: Try this command: \textbf{by} (\textit{metis One\_nat\_def\_raw empty\_replicate} \\
blanchet@36918: \phantom{Try this command: \textbf{by} (\textit{metis~}}\textit{insert\_Nil last\_ConsL replicate\_Suc}). \\
blanchet@36918: To minimize the number of lemmas, try this command: \\
blanchet@36918: \textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{remote\_vampire}] \\
blanchet@36918: \phantom{\textbf{sledgehammer}~}(\textit{One\_nat\_def\_raw empty\_replicate insert\_Nil} \\
blanchet@36918: \phantom{\textbf{sledgehammer}~(}\textit{last\_ConsL replicate\_Suc}).
blanchet@36918: \postw
blanchet@36918: 
blanchet@36918: Sledgehammer ran E, SPASS, and the remote version of Vampire in parallel. If E
blanchet@36918: and SPASS are not installed (\S\ref{installation}), you will see references to
blanchet@36918: their remote American cousins \textit{remote\_e} and \textit{remote\_spass}
blanchet@36918: instead of \textit{e} and \textit{spass}.
blanchet@36918: 
blanchet@36918: Based on each ATP proof, Sledgehammer gives a one-liner proof that uses the
blanchet@36918: \textit{metis} method. You can click them and insert them into the theory text.
blanchet@36918: You can click the ``\textbf{sledgehammer} \textit{minimize}'' command if you
blanchet@36918: want to look for a shorter (and faster) proof. But here the proof found by E
blanchet@36918: looks perfect, so click it to finish the proof.
blanchet@36918: 
blanchet@36918: You can ask Sledgehammer for an Isar text proof by passing the
blanchet@36918: \textit{isar\_proof} option:
blanchet@36918: 
blanchet@36918: \prew
blanchet@36918: \textbf{sledgehammer} [\textit{isar\_proof}]
blanchet@36918: \postw
blanchet@36918: 
blanchet@36918: When Isar proof construction is successful, it can yield proofs that are more
blanchet@36918: readable and also faster than the \textit{metis} one-liners. This feature is
blanchet@36918: experimental.
blanchet@36918: 
blanchet@36918: \section{Command Syntax}
blanchet@36918: \label{command-syntax}
blanchet@36918: 
blanchet@36918: Sledgehammer can be invoked at any point when there is an open goal by entering
blanchet@36918: the \textbf{sledgehammer} command in the theory file. Its general syntax is as
blanchet@36918: follows:
blanchet@36918: 
blanchet@36918: \prew
blanchet@36918: \textbf{sledgehammer} \textit{subcommand\/$^?$ options\/$^?$ facts\_override\/$^?$ num\/$^?$}
blanchet@36918: \postw
blanchet@36918: 
blanchet@36918: For convenience, Sledgehammer is also available in the ``Commands'' submenu of
blanchet@36918: the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c
blanchet@36918: C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with
blanchet@36918: no arguments in the theory text.
blanchet@36918: 
blanchet@36918: In the general syntax, the \textit{subcommand} may be any of the following:
blanchet@36918: 
blanchet@36918: \begin{enum}
blanchet@36918: \item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on subgoal number
blanchet@36918: \textit{num} (1 by default), with the given options and facts.
blanchet@36918: 
blanchet@36918: \item[$\bullet$] \textbf{\textit{minimize}:} Attempts to minimize the provided facts
blanchet@36918: (specified in the \textit{facts\_override} argument) to obtain a simpler proof
blanchet@36918: involving fewer facts. The options and goal number are as for \textit{run}.
blanchet@36918: 
blanchet@36918: \item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued by
blanchet@36918: Sledgehammer. This allows you to examine results that might have been lost due
blanchet@36918: to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
blanchet@36918: limit on the number of messages to display (5 by default).
blanchet@36918: 
blanchet@36918: \item[$\bullet$] \textbf{\textit{available\_atps}:} Prints the list of installed ATPs.
blanchet@36918: See \S\ref{installation} and \S\ref{mode-of-operation} for more information on
blanchet@36918: how to install ATPs.
blanchet@36918: 
blanchet@36918: \item[$\bullet$] \textbf{\textit{running\_atps}:} Prints information about currently
blanchet@36918: running ATPs, including elapsed runtime and remaining time until timeout.
blanchet@36918: 
blanchet@36918: \item[$\bullet$] \textbf{\textit{kill\_atps}:} Terminates all running ATPs.
blanchet@36918: 
blanchet@36918: \item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
blanchet@36918: ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
blanchet@36918: \end{enum}
blanchet@36918: 
blanchet@36918: Sledgehammer's behavior can be influenced by various \textit{options}, which can
blanchet@36918: be specified in brackets after the \textbf{sledgehammer} command. The
blanchet@36918: \textit{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
blanchet@36918: \ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true}'' is optional. For
blanchet@36918: example:
blanchet@36918: 
blanchet@36918: \prew
blanchet@36918: \textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120$\,s$]
blanchet@36918: \postw
blanchet@36918: 
blanchet@36918: Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
blanchet@36918: 
blanchet@36918: \prew
blanchet@36918: \textbf{sledgehammer\_params} \textit{options}
blanchet@36918: \postw
blanchet@36918: 
blanchet@36918: The supported options are described in \S\ref{option-reference}.
blanchet@36918: 
blanchet@36918: The \textit{facts\_override} argument lets you alter the set of facts that go
blanchet@36918: through the relevance filter. It may be of the form ``(\textit{facts})'', where
blanchet@36918: \textit{facts} is a space-separated list of Isabelle facts (theorems, local
blanchet@36918: assumptions, etc.), in which case the relevance filter is bypassed and the given
blanchet@36918: facts are used. It may also be of the form (\textit{add}:\ \textit{facts}$_1$),
blanchet@36918: (\textit{del}:\ \textit{facts}$_2$), or (\textit{add}:\ \textit{facts}$_1$\
blanchet@36918: \textit{del}:\ \textit{facts}$_2$), where the relevance filter is instructed to
blanchet@36918: proceed as usual except that it should consider \textit{facts}$_1$
blanchet@36918: highly-relevant and \textit{facts}$_2$ fully irrelevant.
blanchet@36918: 
blanchet@36918: \section{Option Reference}
blanchet@36918: \label{option-reference}
blanchet@36918: 
blanchet@36918: \def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
blanchet@36918: \def\qty#1{$\left<\textit{#1}\right>$}
blanchet@36918: \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
blanchet@36918: \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
blanchet@36918: \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
blanchet@36918: \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
blanchet@36918: \def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
blanchet@36918: \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
blanchet@36918: \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
blanchet@36918: \def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
blanchet@36918: \def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
blanchet@36918: \def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
blanchet@36918: 
blanchet@36918: Sledgehammer's options are categorized as follows:\ mode of operation
blanchet@36918: (\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), output
blanchet@36918: format (\S\ref{output-format}), and timeouts (\S\ref{timeouts}).
blanchet@36918: 
blanchet@36918: The descriptions below refer to the following syntactic quantities:
blanchet@36918: 
blanchet@36918: \begin{enum}
blanchet@36918: \item[$\bullet$] \qtybf{string}: A string.
blanchet@36918: \item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
blanchet@36918: \item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
blanchet@36918: \item[$\bullet$] \qtybf{int\/}: An integer.
blanchet@36918: \item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
blanchet@36918: (milliseconds), or the keyword \textit{none} ($\infty$ years).
blanchet@36918: \end{enum}
blanchet@36918: 
blanchet@36918: Default values are indicated in square brackets. Boolean options have a negated
blanchet@36918: counterpart (e.g., \textit{debug} vs.\ \textit{no\_debug}). When setting
blanchet@36918: Boolean options, ``= \textit{true}'' may be omitted.
blanchet@36918: 
blanchet@36918: \subsection{Mode of Operation}
blanchet@36918: \label{mode-of-operation}
blanchet@36918: 
blanchet@36918: \begin{enum}
blanchet@36918: %\optrue{blocking}{non\_blocking}
blanchet@36918: %Specifies whether the \textbf{sledgehammer} command should operate synchronously.
blanchet@36918: %The asynchronous (non-blocking) mode lets the user start proving the putative
blanchet@36918: %theorem while Sledgehammer looks for a counterexample, but it can also be more
blanchet@36918: %confusing. For technical reasons, automatic runs currently always block.
blanchet@36918: 
blanchet@36918: \opnodefault{atps}{string}
blanchet@36918: Specifies the ATPs (automated theorem provers) to use as a space-separated list
blanchet@36918: (e.g., ``\textit{e}~\textit{spass}''). The following ATPs are supported:
blanchet@36918: 
blanchet@36918: \begin{enum}
blanchet@36918: \item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz
blanchet@36918: \cite{schulz-2002}. To use E, set the environment variable
blanchet@36918: \texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable,
blanchet@36918: or install the prebuilt E package from Isabelle's download page. See
blanchet@36918: \S\ref{installation} for details.
blanchet@36918: 
blanchet@36918: \item[$\bullet$] \textbf{\textit{spass}:} SPASS is an ATP developed by Christoph
blanchet@36918: Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the
blanchet@36918: environment variable \texttt{SPASS\_HOME} to the directory that contains the
blanchet@36918: \texttt{SPASS} executable, or install the prebuilt SPASS package from Isabelle's
blanchet@36918: download page. See \S\ref{installation} for details.
blanchet@36918: 
blanchet@36918: \item[$\bullet$] \textbf{\textit{spass\_tptp}:} Same as the above, except that
blanchet@36918: Sledgehammer communicates with SPASS using the TPTP syntax rather than the
blanchet@36918: native DFG syntax. This ATP is provided for experimental purposes.
blanchet@36918: 
blanchet@36918: \item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
blanchet@36918: Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
blanchet@36918: Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
blanchet@36918: that contains the \texttt{vampire} executable.
blanchet@36918: 
blanchet@36918: \item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E executes
blanchet@36918: on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
blanchet@36918: 
blanchet@36918: \item[$\bullet$] \textbf{\textit{remote\_spass}:} The remote version of SPASS
blanchet@36918: executes on Geoff Sutcliffe's Miami servers.
blanchet@36918: 
blanchet@36918: \item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
blanchet@36918: Vampire executes on Geoff Sutcliffe's Miami servers. Version 9 is used.
blanchet@36918: 
blanchet@36918: \end{enum}
blanchet@36918: 
blanchet@36918: By default, Sledgehammer will run E, SPASS, and Vampire in parallel. For E and
blanchet@36918: SPASS, it will use any locally installed version if available, falling back
blanchet@36918: on the remote versions if necessary. For historical reasons, the default value
blanchet@36918: of this option can be overridden using the option ``Sledgehammer: ATPs'' from
blanchet@36918: the ``Isabelle'' menu in Proof General.
blanchet@36918: 
blanchet@36918: It is a good idea to run several ATPs in parallel, although it could slow down
blanchet@36918: your machine. Tobias Nipkow observed that running E, SPASS, and Vampire together
blanchet@36918: for 5 seconds yields the same success rate as running the most effective of
blanchet@36918: these (Vampire) for 120 seconds \cite{boehme-nipkow-2010}.
blanchet@36918: 
blanchet@36918: \opnodefault{atp}{string}
blanchet@36918: Alias for \textit{atps}.
blanchet@36918: 
blanchet@36918: \opfalse{overlord}{no\_overlord}
blanchet@36918: Specifies whether Sledgehammer should put its temporary files in
blanchet@36918: \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
blanchet@36918: debugging Sledgehammer but also unsafe if several instances of the tool are run
blanchet@36918: simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
blanchet@36918: safely remove them after Sledgehammer has run.
blanchet@36918: 
blanchet@36918: \nopagebreak
blanchet@36918: {\small See also \textit{debug} (\S\ref{output-format}).}
blanchet@36918: \end{enum}
blanchet@36918: 
blanchet@36918: \subsection{Problem Encoding}
blanchet@36918: \label{problem-encoding}
blanchet@36918: 
blanchet@36918: \begin{enum}
blanchet@36918: \opfalse{explicit\_apply}{implicit\_apply}
blanchet@36918: Specifies whether function application should be encoded as an explicit
blanchet@36918: ``apply'' operator. If the option is set to \textit{false}, each function will
blanchet@36918: be directly applied to as many arguments as possible. Enabling this option can
blanchet@36918: sometimes help discover higher-order proofs that otherwise would not be found.
blanchet@36918: 
blanchet@36918: \opfalse{full\_types}{partial\_types}
blanchet@36918: Specifies whether full-type information is exported. Enabling this option can
blanchet@36918: prevent the discovery of type-incorrect proofs, but it also tends to slow down
blanchet@36918: the ATPs significantly. For historical reasons, the default value of this option
blanchet@36918: can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle''
blanchet@36918: menu in Proof General.
blanchet@36918: 
blanchet@36918: \opdefault{relevance\_threshold}{int}{50}
blanchet@36918: Specifies the threshold above which facts are considered relevant by the
blanchet@36918: relevance filter. The option ranges from 0 to 100, where 0 means that all
blanchet@36918: theorems are relevant.
blanchet@36918: 
blanchet@36918: \opdefault{relevance\_convergence}{int}{320}
blanchet@36918: Specifies the convergence quotient, multiplied by 100, used by the relevance
blanchet@36918: filter. This quotient is used by the relevance filter to scale down the
blanchet@36918: relevance of facts at each iteration of the filter.
blanchet@36918: 
blanchet@36918: \opsmartx{theory\_relevant}{theory\_irrelevant}
blanchet@36918: Specifies whether the theory from which a fact comes should be taken into
blanchet@36918: consideration by the relevance filter. If the option is set to \textit{smart},
blanchet@36918: it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire,
blanchet@36918: because empirical results suggest that these are the best settings.
blanchet@36918: 
blanchet@36918: \opfalse{defs\_relevant}{defs\_irrelevant}
blanchet@36918: Specifies whether the definition of constants occurring in the formula to prove
blanchet@36918: should be considered particularly relevant. Enabling this option tends to lead
blanchet@36918: to larger problems and typically slows down the ATPs.
blanchet@36918: 
blanchet@36918: \optrue{respect\_no\_atp}{ignore\_no\_atp}
blanchet@36918: Specifies whether Sledgehammer should honor the \textit{no\_atp} attributes. The
blanchet@36918: \textit{no\_atp} attributes marks theorems that tend to confuse ATPs, typically
blanchet@36918: because they can lead to unsound ATP proofs \cite{boehme-nipkow-2010}. It is
blanchet@36918: normally a good idea to leave this option enabled, unless you are debugging
blanchet@36918: Sledgehammer.
blanchet@36918: 
blanchet@36918: \end{enum}
blanchet@36918: 
blanchet@36918: \subsection{Output Format}
blanchet@36918: \label{output-format}
blanchet@36918: 
blanchet@36918: \begin{enum}
blanchet@36918: 
blanchet@36918: \opfalse{verbose}{quiet}
blanchet@36918: Specifies whether the \textbf{sledgehammer} command should explain what it does.
blanchet@36918: 
blanchet@36918: \opfalse{debug}{no\_debug}
blanchet@36918: Specifies whether Nitpick should display additional debugging information beyond
blanchet@36918: what \textit{verbose} already displays. Enabling \textit{debug} also enables
blanchet@36918: \textit{verbose} behind the scenes.
blanchet@36918: 
blanchet@36918: \nopagebreak
blanchet@36918: {\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
blanchet@36918: 
blanchet@36918: \opfalse{isar\_proof}{no\_isar\_proof}
blanchet@36918: Specifies whether Isar proofs should be output in addition to one-liner
blanchet@36918: \textit{metis} proofs. Isar proof construction is still experimental and often
blanchet@36918: fails; however, they are usually faster and sometimes more robust than
blanchet@36918: \textit{metis} proofs.
blanchet@36918: 
blanchet@36918: \opdefault{isar\_shrink\_factor}{int}{1}
blanchet@36918: Specifies the granularity of the Isar proof. A value of $n$ indicates that each
blanchet@36918: Isar proof step should correspond to a group of up to $n$ consecutive proof
blanchet@36918: steps in the ATP proof.
blanchet@36918: 
blanchet@36918: \end{enum}
blanchet@36918: 
blanchet@36918: \subsection{Timeouts}
blanchet@36918: \label{timeouts}
blanchet@36918: 
blanchet@36918: \begin{enum}
blanchet@36918: \opdefault{timeout}{time}{$\mathbf{60}$ s}
blanchet@36918: Specifies the maximum amount of time that the ATPs should spend looking for a
blanchet@36918: proof. For historical reasons, the default value of this option can be
blanchet@36918: overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle''
blanchet@36918: menu in Proof General.
blanchet@36918: 
blanchet@36918: \opdefault{minimize\_timeout}{time}{$\mathbf{5}$\,s}
blanchet@36918: Specifies the maximum amount of time that the ATPs should spend looking for a
blanchet@36918: proof for \textbf{sledgehammer}~\textit{minimize}.
blanchet@36918: \end{enum}
blanchet@36918: 
blanchet@36918: \let\em=\sl
blanchet@36918: \bibliography{../manual}{}
blanchet@36918: \bibliographystyle{abbrv}
blanchet@36918: 
blanchet@36918: \end{document}




