summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Sledgehammer/sledgehammer.tex

author | boehmes |

Tue, 07 Dec 2010 15:44:38 +0100 | |

changeset 41064 | 0c447a17770a |

parent 40942 | e08fa125c268 |

child 41208 | 1b28c43a7074 |

permissions | -rw-r--r-- |

updated SMT certificates

\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{../isabelle,../iman,../pdfsetup} %\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} \\ \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 first-order automatic theorem provers (ATPs) and satisfiability-modulo-theories (SMT) solvers on the current goal. The supported ATPs are E \cite{schulz-2002}, SPASS \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, SInE-E \cite{sine}, and SNARK \cite{snark}. 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, and you can tell Sledgehammer to try Yices \cite{yices} and CVC3 \cite{cvc3} as well. 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 \cite{metis}, 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 from the ``Isabelle'' menu in Proof General. 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}} 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 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak in.\allowbreak tum.\allowbreak de}. \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 SAT solvers. Currently, E, SPASS, and Vampire can be run locally; in addition, E, Vampire, SInE-E, and SNARK are available remotely via SystemOnTPTP \cite{sutcliffe-2000}. If you want better performance, you should 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{\char`\~/.isabelle/etc/components} 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 and 1.2, SPASS 3.5 and 3.7, and Vampire 1.0% \footnote{Following the rewrite of Vampire, the counter for version numbers was reset to 0; hence the new Vampire 1.0 is more recent than Vampire 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. \end{enum} To check whether E and SPASS are installed, follow the example in \S\ref{first-steps}. 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/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] \,\longleftrightarrow\, 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}'' for subgoal 1: \\ $([a] = [b]) = (a = b)$ \\ Try this command: \textbf{by} (\textit{metis hd.simps}). \\ To minimize the number of lemmas, try this: \\ \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount] % Sledgehammer: ``\textit{spass}'' for subgoal 1: \\ $([a] = [b]) = (a = b)$ \\ Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\ To minimize the number of lemmas, try this: \\ \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount] % Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\ $([a] = [b]) = (a = b)$ \\ Try this command: \textbf{by} (\textit{metis eq\_commute last\_snoc}) \\ To minimize the number of lemmas, try this: \\ \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}]~(\textit{eq\_commute last\_snoc}). \\[3\smallskipamount] % Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\ $([a] = [b]) = (a = b)$ \\ Try this command: \textbf{by} (\textit{metis hd.simps}) \\ To minimize the number of lemmas, try this: \\ \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}). % Sledgehammer: ``\textit{remote\_z3}'' for subgoal 1: \\ $([a] = [b]) = (a = b)$ \\ Try this command: \textbf{by} (\textit{metis hd.simps}) \\ To minimize the number of lemmas, try this: \\ \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}). \postw Sledgehammer ran E, SPASS, Vampire, SInE-E, 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. For each successful prover, Sledgehammer gives a one-liner proof that uses the \textit{metis} or \textit{smt} method. You can click the proof to insert it into the theory text. You can click the ``\textbf{sledgehammer} \textit{minimize}'' command if you want to look for a shorter (and probably faster) proof. But here the proof found by E looks perfect, so click it to finish the proof. You can ask Sledgehammer for an Isar text proof by passing the \textit{isar\_proof} option: \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} one-liners. This feature is experimental and is only available for ATPs. \section{Hints} \label{hints} For best results, first simplify your problem by calling \textit{auto} or at least \textit{safe} followed by \textit{simp\_all}. None of the ATPs contain arithmetic decision procedures. 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. Note that problems can be easy for \textit{auto} and difficult for ATPs, 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. \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} \textit{subcommand\/$^?$ options\/$^?$ facts\_override\/$^?$ 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 \textit{subcommand} may be any of the following: \begin{enum} \item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on subgoal number \textit{num} (1 by default), with the given options and facts. \item[$\bullet$] \textbf{\textit{minimize}:} Attempts to minimize the provided facts (specified in the \textit{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 \textit{num} argument specifies a limit on the number of messages to display (5 by default). \item[$\bullet$] \textbf{\textit{available\_provers}:} Prints the list of installed provers. 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 \textit{options}, which can be specified in brackets after the \textbf{sledgehammer} command. The \textit{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$\,s$] \postw Default values can be set using \textbf{sledgehammer\_\allowbreak params}: \prew \textbf{sledgehammer\_params} \textit{options} \postw The supported options are described in \S\ref{option-reference}. The \textit{facts\_override} argument lets you alter the set of facts that go through the relevance filter. It may be of the form ``(\textit{facts})'', where \textit{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}:\ \textit{facts}$_1$)'', ``(\textit{del}:\ \textit{facts}$_2$)'', or ``(\textit{add}:\ \textit{facts}$_1$\ \textit{del}:\ \textit{facts}$_2$)'', where the relevance filter is instructed to proceed as usual except that it should consider \textit{facts}$_1$ highly-relevant and \textit{facts}$_2$ fully irrelevant. You can instruct Sledgehammer to run automatically on newly entered theorems by enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof General. For automatic runs, only the first prover set using \textit{provers} (\S\ref{mode-of-operation}) is considered, \textit{verbose} (\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled, fewer facts are passed to the prover, and \textit{timeout} (\S\ref{mode-of-operation}) is superseded by the ``Auto Tools Time Limit'' in Proof General's ``Isabelle'' menu. Sledgehammer's output is also more concise. \section{Option Reference} \label{option-reference} \def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}} \def\qty#1{$\left<\textit{#1}\right>$} \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$} \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]} \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \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{bool\_or\_smart}$\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}), and authentication (\S\ref{authentication}). 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{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}. \item[$\bullet$] \qtybf{int\/}: An integer. \item[$\bullet$] \qtybf{float\_pair\/}: A pair of floating-point numbers (e.g., 0.6 0.95). \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}. \item[$\bullet$] \qtybf{float\_or\_none\/}: An integer (e.g., 60) or floating-point number (e.g., 0.5) expressing a number of seconds, or the keyword \textit{none} ($\infty$ seconds). \end{enum} Default values are indicated in square brackets. Boolean options have a negated counterpart (e.g., \textit{blocking} vs.\ \textit{non\_blocking}). When setting Boolean options, ``= \textit{true}'' may be omitted. \subsection{Mode of Operation} \label{mode-of-operation} \begin{enum} \opnodefault{provers}{string} Specifies the automatic provers to use as a space-separated list (e.g., ``\textit{e}~\textit{spass}''). The following provers are supported: \begin{enum} \item[$\bullet$] \textbf{\textit{e}:} E is an ATP 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{spass}:} SPASS is an ATP 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 an ATP 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. Sledgehammer has been tested with versions 11, 0.6, and 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. Sledgehammer has been tested with 2.7 to 2.15. \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{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{remote\_e}:} The remote version of E runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used. \item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E 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\_snark}:} SNARK is a prover developed by Stickel et al.\ \cite{snark}. The remote version of SNARK 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\_cvc3}:} The remote version of CVC3 runs on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to point). \end{enum} By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever the SMT module's \emph{smt\_solver} configuration option is set to) 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'' from the ``Isabelle'' menu in Proof General. It is a good idea to run several provers in parallel, although it could slow down your machine. Running E, SPASS, Vampire, and SInE-E together for 5 seconds yields a better success rate than running the most effective of these (Vampire) for 120 seconds \cite{boehme-nipkow-2010}. \opnodefault{prover}{string} Alias for \textit{provers}. \opnodefault{atps}{string} Legacy alias for \textit{provers}. \opnodefault{atp}{string} Legacy alias for \textit{provers}. \opdefault{timeout}{float\_or\_none}{\upshape 30} Specifies the maximum number of seconds that the automatic provers should spend searching for a proof. For historical reasons, the default value of this option can be overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle'' menu in Proof General. \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. \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} \opfalse{explicit\_apply}{implicit\_apply} Specifies whether function application should be encoded as an explicit ``apply'' operator in ATP problems. If the option is set to \textit{false}, each function will be directly applied to as many arguments as possible. Enabling this option can sometimes help discover higher-order proofs that otherwise would not be found. \opfalse{full\_types}{partial\_types} Specifies whether full-type information is encoded in ATP problems. Enabling this option can prevent the discovery of type-incorrect proofs, but it also tends to slow down the ATPs significantly. For historical reasons, the default value of this option can be overridden using the option ``Sledgehammer: Full Types'' from the ``Isabelle'' menu in Proof General. \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. \opsmart{max\_relevant}{int\_or\_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 300. \end{enum} \subsection{Output Format} \label{output-format} \begin{enum} \opfalse{verbose}{quiet} Specifies whether the \textbf{sledgehammer} command should explain what it does. \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} behind the scenes. \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{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}).} \end{enum} \let\em=\sl \bibliography{../manual}{} \bibliographystyle{abbrv} \end{document}