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}