1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Fri May 14 22:43:00 2010 +0200
1.3 @@ -0,0 +1,483 @@
1.4 +\documentclass[a4paper,12pt]{article}
1.5 +\usepackage[T1]{fontenc}
1.6 +\usepackage{amsmath}
1.7 +\usepackage{amssymb}
1.8 +\usepackage[english,french]{babel}
1.9 +\usepackage{color}
1.10 +\usepackage{footmisc}
1.11 +\usepackage{graphicx}
1.12 +%\usepackage{mathpazo}
1.13 +\usepackage{multicol}
1.14 +\usepackage{stmaryrd}
1.15 +%\usepackage[scaled=.85]{beramono}
1.16 +\usepackage{../iman,../pdfsetup}
1.17 +
1.18 +%\oddsidemargin=4.6mm
1.19 +%\evensidemargin=4.6mm
1.20 +%\textwidth=150mm
1.21 +%\topmargin=4.6mm
1.22 +%\headheight=0mm
1.23 +%\headsep=0mm
1.24 +%\textheight=234mm
1.25 +
1.26 +\def\Colon{\mathord{:\mkern-1.5mu:}}
1.27 +%\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
1.28 +%\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
1.29 +\def\lparr{\mathopen{(\mkern-4mu\mid}}
1.30 +\def\rparr{\mathclose{\mid\mkern-4mu)}}
1.31 +
1.32 +\def\unk{{?}}
1.33 +\def\undef{(\lambda x.\; \unk)}
1.34 +%\def\unr{\textit{others}}
1.35 +\def\unr{\ldots}
1.36 +\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
1.37 +\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
1.38 +
1.39 +\urlstyle{tt}
1.40 +
1.41 +\begin{document}
1.42 +
1.43 +\selectlanguage{english}
1.44 +
1.45 +\title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
1.46 +Hammering Away \\[\smallskipamount]
1.47 +\Large A User's Guide to Sledgehammer for Isabelle/HOL}
1.48 +\author{\hbox{} \\
1.49 +Jasmin Christian Blanchette \\
1.50 +{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
1.51 +\hbox{}}
1.52 +
1.53 +\maketitle
1.54 +
1.55 +\tableofcontents
1.56 +
1.57 +\setlength{\parskip}{.7em plus .2em minus .1em}
1.58 +\setlength{\parindent}{0pt}
1.59 +\setlength{\abovedisplayskip}{\parskip}
1.60 +\setlength{\abovedisplayshortskip}{.9\parskip}
1.61 +\setlength{\belowdisplayskip}{\parskip}
1.62 +\setlength{\belowdisplayshortskip}{.9\parskip}
1.63 +
1.64 +% General-purpose enum environment with correct spacing
1.65 +\newenvironment{enum}%
1.66 + {\begin{list}{}{%
1.67 + \setlength{\topsep}{.1\parskip}%
1.68 + \setlength{\partopsep}{.1\parskip}%
1.69 + \setlength{\itemsep}{\parskip}%
1.70 + \advance\itemsep by-\parsep}}
1.71 + {\end{list}}
1.72 +
1.73 +\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
1.74 +\advance\rightskip by\leftmargin}
1.75 +\def\post{\vskip0pt plus1ex\endgroup}
1.76 +
1.77 +\def\prew{\pre\advance\rightskip by-\leftmargin}
1.78 +\def\postw{\post}
1.79 +
1.80 +\section{Introduction}
1.81 +\label{introduction}
1.82 +
1.83 +Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs)
1.84 +on the current goal. The supported ATPs are E \cite{schulz-2002}, SPASS
1.85 +\cite{weidenbach-et-al-2009}, and Vampire \cite{riazanov-voronkov-2002}, which
1.86 +can be run locally or remotely via the SystemOnTPTP web service
1.87 +\cite{sutcliffe-2000}.
1.88 +
1.89 +The problem passed to ATPs consists of the current goal together with a
1.90 +heuristic selection of facts (theorems) from the current theory context,
1.91 +filtered by relevance. The result of a successful ATP proof search is some
1.92 +source text that usually (but not always) reconstructs the proof within
1.93 +Isabelle, without requiring the ATPs again. The reconstructed proof relies on
1.94 +the general-purpose Metis prover \cite{metis}, which is fully integrated into
1.95 +Isabelle/HOL, with explicit inferences going through the kernel. Thus its
1.96 +results are correct by construction.
1.97 +
1.98 +\newbox\boxA
1.99 +\setbox\boxA=\hbox{\texttt{nospam}}
1.100 +
1.101 +Examples of Sledgehammer use can be found in Isabelle's
1.102 +\texttt{src/HOL/Metis\_Examples} directory.
1.103 +Comments and bug reports concerning Sledgehammer or this manual should be
1.104 +directed to
1.105 +\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
1.106 +in.\allowbreak tum.\allowbreak de}.
1.107 +
1.108 +\vskip2.5\smallskipamount
1.109 +
1.110 +%\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
1.111 +%suggesting several textual improvements.
1.112 +
1.113 +\section{Installation}
1.114 +\label{installation}
1.115 +
1.116 +Sledgehammer is part of Isabelle, so you don't need to install it. However, it
1.117 +relies on third-party automatic theorem provers (ATPs). Currently, E, SPASS, and
1.118 +Vampire are supported. All of these are available remotely via SystemOnTPTP
1.119 +\cite{sutcliffe-2000}, but if you want better performance you will need to
1.120 +install at least E and SPASS locally.
1.121 +
1.122 +There are three main ways to install E and SPASS:
1.123 +
1.124 +\begin{enum}
1.125 +\item[$\bullet$] If you installed an official Isabelle package with everything
1.126 +inside, it should already include properly setup executables for E and SPASS,
1.127 +ready to use.
1.128 +
1.129 +\item[$\bullet$] Otherwise, you can download the Isabelle-aware E and SPASS
1.130 +binary packages from Isabelle's download page. Extract the archives, then add a
1.131 +line to your \texttt{\char`\~/.isabelle/etc/components} file with the absolute path to
1.132 +E or SPASS. For example, if \texttt{\char`\~/.isabelle/etc/components} does not exist
1.133 +yet and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create
1.134 +the file \texttt{\char`\~/.isabelle/etc/components} with the single line
1.135 +
1.136 +\prew
1.137 +\texttt{/usr/local/spass-3.7}
1.138 +\postw
1.139 +
1.140 +\item[$\bullet$] If you prefer to build E or SPASS yourself, feel free to do so
1.141 +and set the environment variable \texttt{E\_HOME} or \texttt{SPASS\_HOME} to the
1.142 +directory that contains the \texttt{eproof} or \texttt{SPASS} executable,
1.143 +respectively.
1.144 +\end{enum}
1.145 +
1.146 +To check whether E and SPASS are installed, follow the example in
1.147 +\S\ref{first-steps}.
1.148 +
1.149 +\section{First Steps}
1.150 +\label{first-steps}
1.151 +
1.152 +To illustrate Sledgehammer in context, let us start a theory file and
1.153 +attempt to prove a simple lemma:
1.154 +
1.155 +\prew
1.156 +\textbf{theory}~\textit{Scratch} \\
1.157 +\textbf{imports}~\textit{Main} \\
1.158 +\textbf{begin} \\[2\smallskipamount]
1.159 +%
1.160 +\textbf{lemma} ``$[a] = [b] \,\longleftrightarrow\, a = b$'' \\
1.161 +\textbf{sledgehammer}
1.162 +\postw
1.163 +
1.164 +After a few seconds, Sledgehammer produces the following output:
1.165 +
1.166 +\prew
1.167 +\slshape
1.168 +Sledgehammer: ATP ``\textit{e}'' for subgoal 1: \\
1.169 +$([a] = [b]) = (a = b)$ \\
1.170 +Try this command: \textbf{by} (\textit{metis hd.simps}). \\
1.171 +To minimize the number of lemmas, try this command: \\
1.172 +\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
1.173 +%
1.174 +Sledgehammer: ATP ``\textit{spass}'' for subgoal 1: \\
1.175 +$([a] = [b]) = (a = b)$ \\
1.176 +Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
1.177 +To minimize the number of lemmas, try this command: \\
1.178 +\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
1.179 +%
1.180 +Sledgehammer: ATP ``\textit{remote\_vampire}'' for subgoal 1: \\
1.181 +$([a] = [b]) = (a = b)$ \\
1.182 +Try this command: \textbf{by} (\textit{metis One\_nat\_def\_raw empty\_replicate} \\
1.183 +\phantom{Try this command: \textbf{by} (\textit{metis~}}\textit{insert\_Nil last\_ConsL replicate\_Suc}). \\
1.184 +To minimize the number of lemmas, try this command: \\
1.185 +\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{remote\_vampire}] \\
1.186 +\phantom{\textbf{sledgehammer}~}(\textit{One\_nat\_def\_raw empty\_replicate insert\_Nil} \\
1.187 +\phantom{\textbf{sledgehammer}~(}\textit{last\_ConsL replicate\_Suc}).
1.188 +\postw
1.189 +
1.190 +Sledgehammer ran E, SPASS, and the remote version of Vampire in parallel. If E
1.191 +and SPASS are not installed (\S\ref{installation}), you will see references to
1.192 +their remote American cousins \textit{remote\_e} and \textit{remote\_spass}
1.193 +instead of \textit{e} and \textit{spass}.
1.194 +
1.195 +Based on each ATP proof, Sledgehammer gives a one-liner proof that uses the
1.196 +\textit{metis} method. You can click them and insert them into the theory text.
1.197 +You can click the ``\textbf{sledgehammer} \textit{minimize}'' command if you
1.198 +want to look for a shorter (and faster) proof. But here the proof found by E
1.199 +looks perfect, so click it to finish the proof.
1.200 +
1.201 +You can ask Sledgehammer for an Isar text proof by passing the
1.202 +\textit{isar\_proof} option:
1.203 +
1.204 +\prew
1.205 +\textbf{sledgehammer} [\textit{isar\_proof}]
1.206 +\postw
1.207 +
1.208 +When Isar proof construction is successful, it can yield proofs that are more
1.209 +readable and also faster than the \textit{metis} one-liners. This feature is
1.210 +experimental.
1.211 +
1.212 +\section{Command Syntax}
1.213 +\label{command-syntax}
1.214 +
1.215 +Sledgehammer can be invoked at any point when there is an open goal by entering
1.216 +the \textbf{sledgehammer} command in the theory file. Its general syntax is as
1.217 +follows:
1.218 +
1.219 +\prew
1.220 +\textbf{sledgehammer} \textit{subcommand\/$^?$ options\/$^?$ facts\_override\/$^?$ num\/$^?$}
1.221 +\postw
1.222 +
1.223 +For convenience, Sledgehammer is also available in the ``Commands'' submenu of
1.224 +the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c
1.225 +C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with
1.226 +no arguments in the theory text.
1.227 +
1.228 +In the general syntax, the \textit{subcommand} may be any of the following:
1.229 +
1.230 +\begin{enum}
1.231 +\item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on subgoal number
1.232 +\textit{num} (1 by default), with the given options and facts.
1.233 +
1.234 +\item[$\bullet$] \textbf{\textit{minimize}:} Attempts to minimize the provided facts
1.235 +(specified in the \textit{facts\_override} argument) to obtain a simpler proof
1.236 +involving fewer facts. The options and goal number are as for \textit{run}.
1.237 +
1.238 +\item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued by
1.239 +Sledgehammer. This allows you to examine results that might have been lost due
1.240 +to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
1.241 +limit on the number of messages to display (5 by default).
1.242 +
1.243 +\item[$\bullet$] \textbf{\textit{available\_atps}:} Prints the list of installed ATPs.
1.244 +See \S\ref{installation} and \S\ref{mode-of-operation} for more information on
1.245 +how to install ATPs.
1.246 +
1.247 +\item[$\bullet$] \textbf{\textit{running\_atps}:} Prints information about currently
1.248 +running ATPs, including elapsed runtime and remaining time until timeout.
1.249 +
1.250 +\item[$\bullet$] \textbf{\textit{kill\_atps}:} Terminates all running ATPs.
1.251 +
1.252 +\item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
1.253 +ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
1.254 +\end{enum}
1.255 +
1.256 +Sledgehammer's behavior can be influenced by various \textit{options}, which can
1.257 +be specified in brackets after the \textbf{sledgehammer} command. The
1.258 +\textit{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
1.259 +\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true}'' is optional. For
1.260 +example:
1.261 +
1.262 +\prew
1.263 +\textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120$\,s$]
1.264 +\postw
1.265 +
1.266 +Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
1.267 +
1.268 +\prew
1.269 +\textbf{sledgehammer\_params} \textit{options}
1.270 +\postw
1.271 +
1.272 +The supported options are described in \S\ref{option-reference}.
1.273 +
1.274 +The \textit{facts\_override} argument lets you alter the set of facts that go
1.275 +through the relevance filter. It may be of the form ``(\textit{facts})'', where
1.276 +\textit{facts} is a space-separated list of Isabelle facts (theorems, local
1.277 +assumptions, etc.), in which case the relevance filter is bypassed and the given
1.278 +facts are used. It may also be of the form (\textit{add}:\ \textit{facts}$_1$),
1.279 +(\textit{del}:\ \textit{facts}$_2$), or (\textit{add}:\ \textit{facts}$_1$\
1.280 +\textit{del}:\ \textit{facts}$_2$), where the relevance filter is instructed to
1.281 +proceed as usual except that it should consider \textit{facts}$_1$
1.282 +highly-relevant and \textit{facts}$_2$ fully irrelevant.
1.283 +
1.284 +\section{Option Reference}
1.285 +\label{option-reference}
1.286 +
1.287 +\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
1.288 +\def\qty#1{$\left<\textit{#1}\right>$}
1.289 +\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
1.290 +\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1.291 +\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1.292 +\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1.293 +\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1.294 +\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
1.295 +\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
1.296 +\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
1.297 +\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
1.298 +\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
1.299 +
1.300 +Sledgehammer's options are categorized as follows:\ mode of operation
1.301 +(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), output
1.302 +format (\S\ref{output-format}), and timeouts (\S\ref{timeouts}).
1.303 +
1.304 +The descriptions below refer to the following syntactic quantities:
1.305 +
1.306 +\begin{enum}
1.307 +\item[$\bullet$] \qtybf{string}: A string.
1.308 +\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
1.309 +\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
1.310 +\item[$\bullet$] \qtybf{int\/}: An integer.
1.311 +\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
1.312 +(milliseconds), or the keyword \textit{none} ($\infty$ years).
1.313 +\end{enum}
1.314 +
1.315 +Default values are indicated in square brackets. Boolean options have a negated
1.316 +counterpart (e.g., \textit{debug} vs.\ \textit{no\_debug}). When setting
1.317 +Boolean options, ``= \textit{true}'' may be omitted.
1.318 +
1.319 +\subsection{Mode of Operation}
1.320 +\label{mode-of-operation}
1.321 +
1.322 +\begin{enum}
1.323 +%\optrue{blocking}{non\_blocking}
1.324 +%Specifies whether the \textbf{sledgehammer} command should operate synchronously.
1.325 +%The asynchronous (non-blocking) mode lets the user start proving the putative
1.326 +%theorem while Sledgehammer looks for a counterexample, but it can also be more
1.327 +%confusing. For technical reasons, automatic runs currently always block.
1.328 +
1.329 +\opnodefault{atps}{string}
1.330 +Specifies the ATPs (automated theorem provers) to use as a space-separated list
1.331 +(e.g., ``\textit{e}~\textit{spass}''). The following ATPs are supported:
1.332 +
1.333 +\begin{enum}
1.334 +\item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz
1.335 +\cite{schulz-2002}. To use E, set the environment variable
1.336 +\texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable,
1.337 +or install the prebuilt E package from Isabelle's download page. See
1.338 +\S\ref{installation} for details.
1.339 +
1.340 +\item[$\bullet$] \textbf{\textit{spass}:} SPASS is an ATP developed by Christoph
1.341 +Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the
1.342 +environment variable \texttt{SPASS\_HOME} to the directory that contains the
1.343 +\texttt{SPASS} executable, or install the prebuilt SPASS package from Isabelle's
1.344 +download page. See \S\ref{installation} for details.
1.345 +
1.346 +\item[$\bullet$] \textbf{\textit{spass\_tptp}:} Same as the above, except that
1.347 +Sledgehammer communicates with SPASS using the TPTP syntax rather than the
1.348 +native DFG syntax. This ATP is provided for experimental purposes.
1.349 +
1.350 +\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
1.351 +Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
1.352 +Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
1.353 +that contains the \texttt{vampire} executable.
1.354 +
1.355 +\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E executes
1.356 +on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
1.357 +
1.358 +\item[$\bullet$] \textbf{\textit{remote\_spass}:} The remote version of SPASS
1.359 +executes on Geoff Sutcliffe's Miami servers.
1.360 +
1.361 +\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
1.362 +Vampire executes on Geoff Sutcliffe's Miami servers. Version 9 is used.
1.363 +
1.364 +\end{enum}
1.365 +
1.366 +By default, Sledgehammer will run E, SPASS, and Vampire in parallel. For E and
1.367 +SPASS, it will use any locally installed version if available, falling back
1.368 +on the remote versions if necessary. For historical reasons, the default value
1.369 +of this option can be overridden using the option ``Sledgehammer: ATPs'' from
1.370 +the ``Isabelle'' menu in Proof General.
1.371 +
1.372 +It is a good idea to run several ATPs in parallel, although it could slow down
1.373 +your machine. Tobias Nipkow observed that running E, SPASS, and Vampire together
1.374 +for 5 seconds yields the same success rate as running the most effective of
1.375 +these (Vampire) for 120 seconds \cite{boehme-nipkow-2010}.
1.376 +
1.377 +\opnodefault{atp}{string}
1.378 +Alias for \textit{atps}.
1.379 +
1.380 +\opfalse{overlord}{no\_overlord}
1.381 +Specifies whether Sledgehammer should put its temporary files in
1.382 +\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
1.383 +debugging Sledgehammer but also unsafe if several instances of the tool are run
1.384 +simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
1.385 +safely remove them after Sledgehammer has run.
1.386 +
1.387 +\nopagebreak
1.388 +{\small See also \textit{debug} (\S\ref{output-format}).}
1.389 +\end{enum}
1.390 +
1.391 +\subsection{Problem Encoding}
1.392 +\label{problem-encoding}
1.393 +
1.394 +\begin{enum}
1.395 +\opfalse{explicit\_apply}{implicit\_apply}
1.396 +Specifies whether function application should be encoded as an explicit
1.397 +``apply'' operator. If the option is set to \textit{false}, each function will
1.398 +be directly applied to as many arguments as possible. Enabling this option can
1.399 +sometimes help discover higher-order proofs that otherwise would not be found.
1.400 +
1.401 +\opfalse{full\_types}{partial\_types}
1.402 +Specifies whether full-type information is exported. Enabling this option can
1.403 +prevent the discovery of type-incorrect proofs, but it also tends to slow down
1.404 +the ATPs significantly. For historical reasons, the default value of this option
1.405 +can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle''
1.406 +menu in Proof General.
1.407 +
1.408 +\opdefault{relevance\_threshold}{int}{50}
1.409 +Specifies the threshold above which facts are considered relevant by the
1.410 +relevance filter. The option ranges from 0 to 100, where 0 means that all
1.411 +theorems are relevant.
1.412 +
1.413 +\opdefault{relevance\_convergence}{int}{320}
1.414 +Specifies the convergence quotient, multiplied by 100, used by the relevance
1.415 +filter. This quotient is used by the relevance filter to scale down the
1.416 +relevance of facts at each iteration of the filter.
1.417 +
1.418 +\opsmartx{theory\_relevant}{theory\_irrelevant}
1.419 +Specifies whether the theory from which a fact comes should be taken into
1.420 +consideration by the relevance filter. If the option is set to \textit{smart},
1.421 +it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire,
1.422 +because empirical results suggest that these are the best settings.
1.423 +
1.424 +\opfalse{defs\_relevant}{defs\_irrelevant}
1.425 +Specifies whether the definition of constants occurring in the formula to prove
1.426 +should be considered particularly relevant. Enabling this option tends to lead
1.427 +to larger problems and typically slows down the ATPs.
1.428 +
1.429 +\optrue{respect\_no\_atp}{ignore\_no\_atp}
1.430 +Specifies whether Sledgehammer should honor the \textit{no\_atp} attributes. The
1.431 +\textit{no\_atp} attributes marks theorems that tend to confuse ATPs, typically
1.432 +because they can lead to unsound ATP proofs \cite{boehme-nipkow-2010}. It is
1.433 +normally a good idea to leave this option enabled, unless you are debugging
1.434 +Sledgehammer.
1.435 +
1.436 +\end{enum}
1.437 +
1.438 +\subsection{Output Format}
1.439 +\label{output-format}
1.440 +
1.441 +\begin{enum}
1.442 +
1.443 +\opfalse{verbose}{quiet}
1.444 +Specifies whether the \textbf{sledgehammer} command should explain what it does.
1.445 +
1.446 +\opfalse{debug}{no\_debug}
1.447 +Specifies whether Nitpick should display additional debugging information beyond
1.448 +what \textit{verbose} already displays. Enabling \textit{debug} also enables
1.449 +\textit{verbose} behind the scenes.
1.450 +
1.451 +\nopagebreak
1.452 +{\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
1.453 +
1.454 +\opfalse{isar\_proof}{no\_isar\_proof}
1.455 +Specifies whether Isar proofs should be output in addition to one-liner
1.456 +\textit{metis} proofs. Isar proof construction is still experimental and often
1.457 +fails; however, they are usually faster and sometimes more robust than
1.458 +\textit{metis} proofs.
1.459 +
1.460 +\opdefault{isar\_shrink\_factor}{int}{1}
1.461 +Specifies the granularity of the Isar proof. A value of $n$ indicates that each
1.462 +Isar proof step should correspond to a group of up to $n$ consecutive proof
1.463 +steps in the ATP proof.
1.464 +
1.465 +\end{enum}
1.466 +
1.467 +\subsection{Timeouts}
1.468 +\label{timeouts}
1.469 +
1.470 +\begin{enum}
1.471 +\opdefault{timeout}{time}{$\mathbf{60}$ s}
1.472 +Specifies the maximum amount of time that the ATPs should spend looking for a
1.473 +proof. For historical reasons, the default value of this option can be
1.474 +overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle''
1.475 +menu in Proof General.
1.476 +
1.477 +\opdefault{minimize\_timeout}{time}{$\mathbf{5}$\,s}
1.478 +Specifies the maximum amount of time that the ATPs should spend looking for a
1.479 +proof for \textbf{sledgehammer}~\textit{minimize}.
1.480 +\end{enum}
1.481 +
1.482 +\let\em=\sl
1.483 +\bibliography{../manual}{}
1.484 +\bibliographystyle{abbrv}
1.485 +
1.486 +\end{document}