doc-src/Sledgehammer/sledgehammer.tex
author blanchet
Tue Jun 22 14:28:22 2010 +0200 (2010-06-22 ago)
changeset 37498 b426cbdb5a23
parent 37414 d0cea0796295
child 37517 19ba7ec5f1e3
permissions -rw-r--r--
removed Sledgehammer's support for the DFG syntax;
this removes 350 buggy lines from Sledgehammer. SPASS 3.5 and above support the TPTP syntax.
     1 \documentclass[a4paper,12pt]{article}
     2 \usepackage[T1]{fontenc}
     3 \usepackage{amsmath}
     4 \usepackage{amssymb}
     5 \usepackage[english,french]{babel}
     6 \usepackage{color}
     7 \usepackage{footmisc}
     8 \usepackage{graphicx}
     9 %\usepackage{mathpazo}
    10 \usepackage{multicol}
    11 \usepackage{stmaryrd}
    12 %\usepackage[scaled=.85]{beramono}
    13 \usepackage{../iman,../pdfsetup}
    14 
    15 %\oddsidemargin=4.6mm
    16 %\evensidemargin=4.6mm
    17 %\textwidth=150mm
    18 %\topmargin=4.6mm
    19 %\headheight=0mm
    20 %\headsep=0mm
    21 %\textheight=234mm
    22 
    23 \def\Colon{\mathord{:\mkern-1.5mu:}}
    24 %\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
    25 %\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
    26 \def\lparr{\mathopen{(\mkern-4mu\mid}}
    27 \def\rparr{\mathclose{\mid\mkern-4mu)}}
    28 
    29 \def\unk{{?}}
    30 \def\undef{(\lambda x.\; \unk)}
    31 %\def\unr{\textit{others}}
    32 \def\unr{\ldots}
    33 \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
    34 \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
    35 
    36 \urlstyle{tt}
    37 
    38 \begin{document}
    39 
    40 \selectlanguage{english}
    41 
    42 \title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
    43 Hammering Away \\[\smallskipamount]
    44 \Large A User's Guide to Sledgehammer for Isabelle/HOL}
    45 \author{\hbox{} \\
    46 Jasmin Christian Blanchette \\
    47 {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
    48 \hbox{}}
    49 
    50 \maketitle
    51 
    52 \tableofcontents
    53 
    54 \setlength{\parskip}{.7em plus .2em minus .1em}
    55 \setlength{\parindent}{0pt}
    56 \setlength{\abovedisplayskip}{\parskip}
    57 \setlength{\abovedisplayshortskip}{.9\parskip}
    58 \setlength{\belowdisplayskip}{\parskip}
    59 \setlength{\belowdisplayshortskip}{.9\parskip}
    60 
    61 % General-purpose enum environment with correct spacing
    62 \newenvironment{enum}%
    63     {\begin{list}{}{%
    64         \setlength{\topsep}{.1\parskip}%
    65         \setlength{\partopsep}{.1\parskip}%
    66         \setlength{\itemsep}{\parskip}%
    67         \advance\itemsep by-\parsep}}
    68     {\end{list}}
    69 
    70 \def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
    71 \advance\rightskip by\leftmargin}
    72 \def\post{\vskip0pt plus1ex\endgroup}
    73 
    74 \def\prew{\pre\advance\rightskip by-\leftmargin}
    75 \def\postw{\post}
    76 
    77 \section{Introduction}
    78 \label{introduction}
    79 
    80 Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs)
    81 on the current goal. The supported ATPs are E \cite{schulz-2002}, SPASS
    82 \cite{weidenbach-et-al-2009}, and Vampire \cite{riazanov-voronkov-2002}, which
    83 can be run locally or remotely via the SystemOnTPTP web service
    84 \cite{sutcliffe-2000}.
    85 
    86 The problem passed to ATPs consists of the current goal together with a
    87 heuristic selection of facts (theorems) from the current theory context,
    88 filtered by relevance. The result of a successful ATP proof search is some
    89 source text that usually (but not always) reconstructs the proof within
    90 Isabelle, without requiring the ATPs again. The reconstructed proof relies on
    91 the general-purpose Metis prover \cite{metis}, which is fully integrated into
    92 Isabelle/HOL, with explicit inferences going through the kernel. Thus its
    93 results are correct by construction.
    94 
    95 \newbox\boxA
    96 \setbox\boxA=\hbox{\texttt{nospam}}
    97 
    98 Examples of Sledgehammer use can be found in Isabelle's
    99 \texttt{src/HOL/Metis\_Examples} directory.
   100 Comments and bug reports concerning Sledgehammer or this manual should be
   101 directed to
   102 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
   103 in.\allowbreak tum.\allowbreak de}.
   104 
   105 \vskip2.5\smallskipamount
   106 
   107 %\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
   108 %suggesting several textual improvements.
   109 
   110 \section{Installation}
   111 \label{installation}
   112 
   113 Sledgehammer is part of Isabelle, so you don't need to install it. However, it
   114 relies on third-party automatic theorem provers (ATPs). Currently, E, SPASS, and
   115 Vampire are supported. All of these are available remotely via SystemOnTPTP
   116 \cite{sutcliffe-2000}, but if you want better performance you will need to
   117 install at least E and SPASS locally.
   118 
   119 There are three main ways to install E and SPASS:
   120 
   121 \begin{enum}
   122 \item[$\bullet$] If you installed an official Isabelle package with everything
   123 inside, it should already include properly setup executables for E and SPASS,
   124 ready to use.
   125 
   126 \item[$\bullet$] Otherwise, you can download the Isabelle-aware E and SPASS
   127 binary packages from Isabelle's download page. Extract the archives, then add a
   128 line to your \texttt{\char`\~/.isabelle/etc/components} file with the absolute path to
   129 E or SPASS. For example, if \texttt{\char`\~/.isabelle/etc/components} does not exist
   130 yet and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create
   131 the file \texttt{\char`\~/.isabelle/etc/components} with the single line
   132 
   133 \prew
   134 \texttt{/usr/local/spass-3.7}
   135 \postw
   136 
   137 \item[$\bullet$] If you prefer to build E or SPASS yourself, feel free to do so
   138 and set the environment variable \texttt{E\_HOME} or \texttt{SPASS\_HOME} to the
   139 directory that contains the \texttt{eproof} or \texttt{SPASS} executable,
   140 respectively.
   141 \end{enum}
   142 
   143 To check whether E and SPASS are installed, follow the example in
   144 \S\ref{first-steps}.
   145 
   146 \section{First Steps}
   147 \label{first-steps}
   148 
   149 To illustrate Sledgehammer in context, let us start a theory file and
   150 attempt to prove a simple lemma:
   151 
   152 \prew
   153 \textbf{theory}~\textit{Scratch} \\
   154 \textbf{imports}~\textit{Main} \\
   155 \textbf{begin} \\[2\smallskipamount]
   156 %
   157 \textbf{lemma} ``$[a] = [b] \,\longleftrightarrow\, a = b$'' \\
   158 \textbf{sledgehammer}
   159 \postw
   160 
   161 After a few seconds, Sledgehammer produces the following output:
   162 
   163 \prew
   164 \slshape
   165 Sledgehammer: ATP ``\textit{e}'' for subgoal 1: \\
   166 $([a] = [b]) = (a = b)$ \\
   167 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
   168 To minimize the number of lemmas, try this command: \\
   169 \textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
   170 %
   171 Sledgehammer: ATP ``\textit{spass}'' for subgoal 1: \\
   172 $([a] = [b]) = (a = b)$ \\
   173 Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
   174 To minimize the number of lemmas, try this command: \\
   175 \textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
   176 %
   177 Sledgehammer: ATP ``\textit{remote\_vampire}'' for subgoal 1: \\
   178 $([a] = [b]) = (a = b)$ \\
   179 Try this command: \textbf{by} (\textit{metis One\_nat\_def\_raw empty\_replicate} \\
   180 \phantom{Try this command: \textbf{by} (\textit{metis~}}\textit{insert\_Nil last\_ConsL replicate\_Suc}). \\
   181 To minimize the number of lemmas, try this command: \\
   182 \textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{remote\_vampire}] \\
   183 \phantom{\textbf{sledgehammer}~}(\textit{One\_nat\_def\_raw empty\_replicate insert\_Nil} \\
   184 \phantom{\textbf{sledgehammer}~(}\textit{last\_ConsL replicate\_Suc}).
   185 \postw
   186 
   187 Sledgehammer ran E, SPASS, and the remote version of Vampire in parallel. If E
   188 and SPASS are not installed (\S\ref{installation}), you will see references to
   189 their remote American cousins \textit{remote\_e} and \textit{remote\_spass}
   190 instead of \textit{e} and \textit{spass}.
   191 
   192 Based on each ATP proof, Sledgehammer gives a one-liner proof that uses the
   193 \textit{metis} method. You can click them and insert them into the theory text.
   194 You can click the ``\textbf{sledgehammer} \textit{minimize}'' command if you
   195 want to look for a shorter (and faster) proof. But here the proof found by E
   196 looks perfect, so click it to finish the proof.
   197 
   198 You can ask Sledgehammer for an Isar text proof by passing the
   199 \textit{isar\_proof} option:
   200 
   201 \prew
   202 \textbf{sledgehammer} [\textit{isar\_proof}]
   203 \postw
   204 
   205 When Isar proof construction is successful, it can yield proofs that are more
   206 readable and also faster than the \textit{metis} one-liners. This feature is
   207 experimental.
   208 
   209 \section{Command Syntax}
   210 \label{command-syntax}
   211 
   212 Sledgehammer can be invoked at any point when there is an open goal by entering
   213 the \textbf{sledgehammer} command in the theory file. Its general syntax is as
   214 follows:
   215 
   216 \prew
   217 \textbf{sledgehammer} \textit{subcommand\/$^?$ options\/$^?$ facts\_override\/$^?$ num\/$^?$}
   218 \postw
   219 
   220 For convenience, Sledgehammer is also available in the ``Commands'' submenu of
   221 the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c
   222 C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with
   223 no arguments in the theory text.
   224 
   225 In the general syntax, the \textit{subcommand} may be any of the following:
   226 
   227 \begin{enum}
   228 \item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on subgoal number
   229 \textit{num} (1 by default), with the given options and facts.
   230 
   231 \item[$\bullet$] \textbf{\textit{minimize}:} Attempts to minimize the provided facts
   232 (specified in the \textit{facts\_override} argument) to obtain a simpler proof
   233 involving fewer facts. The options and goal number are as for \textit{run}.
   234 
   235 \item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued by
   236 Sledgehammer. This allows you to examine results that might have been lost due
   237 to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
   238 limit on the number of messages to display (5 by default).
   239 
   240 \item[$\bullet$] \textbf{\textit{available\_atps}:} Prints the list of installed ATPs.
   241 See \S\ref{installation} and \S\ref{mode-of-operation} for more information on
   242 how to install ATPs.
   243 
   244 \item[$\bullet$] \textbf{\textit{running\_atps}:} Prints information about currently
   245 running ATPs, including elapsed runtime and remaining time until timeout.
   246 
   247 \item[$\bullet$] \textbf{\textit{kill\_atps}:} Terminates all running ATPs.
   248 
   249 \item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
   250 ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
   251 \end{enum}
   252 
   253 Sledgehammer's behavior can be influenced by various \textit{options}, which can
   254 be specified in brackets after the \textbf{sledgehammer} command. The
   255 \textit{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
   256 \ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true}'' is optional. For
   257 example:
   258 
   259 \prew
   260 \textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120$\,s$]
   261 \postw
   262 
   263 Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
   264 
   265 \prew
   266 \textbf{sledgehammer\_params} \textit{options}
   267 \postw
   268 
   269 The supported options are described in \S\ref{option-reference}.
   270 
   271 The \textit{facts\_override} argument lets you alter the set of facts that go
   272 through the relevance filter. It may be of the form ``(\textit{facts})'', where
   273 \textit{facts} is a space-separated list of Isabelle facts (theorems, local
   274 assumptions, etc.), in which case the relevance filter is bypassed and the given
   275 facts are used. It may also be of the form (\textit{add}:\ \textit{facts}$_1$),
   276 (\textit{del}:\ \textit{facts}$_2$), or (\textit{add}:\ \textit{facts}$_1$\
   277 \textit{del}:\ \textit{facts}$_2$), where the relevance filter is instructed to
   278 proceed as usual except that it should consider \textit{facts}$_1$
   279 highly-relevant and \textit{facts}$_2$ fully irrelevant.
   280 
   281 \section{Option Reference}
   282 \label{option-reference}
   283 
   284 \def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
   285 \def\qty#1{$\left<\textit{#1}\right>$}
   286 \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
   287 \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
   288 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
   289 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
   290 \def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
   291 \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
   292 \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
   293 \def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
   294 \def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
   295 \def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
   296 
   297 Sledgehammer's options are categorized as follows:\ mode of operation
   298 (\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), output
   299 format (\S\ref{output-format}), and timeouts (\S\ref{timeouts}).
   300 
   301 The descriptions below refer to the following syntactic quantities:
   302 
   303 \begin{enum}
   304 \item[$\bullet$] \qtybf{string}: A string.
   305 \item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
   306 \item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
   307 \item[$\bullet$] \qtybf{int\/}: An integer.
   308 \item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
   309 (milliseconds), or the keyword \textit{none} ($\infty$ years).
   310 \end{enum}
   311 
   312 Default values are indicated in square brackets. Boolean options have a negated
   313 counterpart (e.g., \textit{debug} vs.\ \textit{no\_debug}). When setting
   314 Boolean options, ``= \textit{true}'' may be omitted.
   315 
   316 \subsection{Mode of Operation}
   317 \label{mode-of-operation}
   318 
   319 \begin{enum}
   320 %\optrue{blocking}{non\_blocking}
   321 %Specifies whether the \textbf{sledgehammer} command should operate synchronously.
   322 %The asynchronous (non-blocking) mode lets the user start proving the putative
   323 %theorem while Sledgehammer looks for a counterexample, but it can also be more
   324 %confusing. For technical reasons, automatic runs currently always block.
   325 
   326 \opnodefault{atps}{string}
   327 Specifies the ATPs (automated theorem provers) to use as a space-separated list
   328 (e.g., ``\textit{e}~\textit{spass}''). The following ATPs are supported:
   329 
   330 \begin{enum}
   331 \item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz
   332 \cite{schulz-2002}. To use E, set the environment variable
   333 \texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable,
   334 or install the prebuilt E package from Isabelle's download page. See
   335 \S\ref{installation} for details.
   336 
   337 \item[$\bullet$] \textbf{\textit{spass}:} SPASS is an ATP developed by Christoph
   338 Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the
   339 environment variable \texttt{SPASS\_HOME} to the directory that contains the
   340 \texttt{SPASS} executable, or install the prebuilt SPASS package from Isabelle's
   341 download page. Sledgehammer requires version 3.5 or above. See
   342 \S\ref{installation} for details.
   343 
   344 \item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
   345 Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
   346 Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
   347 that contains the \texttt{vampire} executable.
   348 
   349 \item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E executes
   350 on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
   351 
   352 \item[$\bullet$] \textbf{\textit{remote\_spass}:} The remote version of SPASS
   353 executes on Geoff Sutcliffe's Miami servers.
   354 
   355 \item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
   356 Vampire executes on Geoff Sutcliffe's Miami servers. Version 9 is used.
   357 
   358 \end{enum}
   359 
   360 By default, Sledgehammer will run E, SPASS, and Vampire in parallel. For E and
   361 SPASS, it will use any locally installed version if available, falling back
   362 on the remote versions if necessary. For historical reasons, the default value
   363 of this option can be overridden using the option ``Sledgehammer: ATPs'' from
   364 the ``Isabelle'' menu in Proof General.
   365 
   366 It is a good idea to run several ATPs in parallel, although it could slow down
   367 your machine. Tobias Nipkow observed that running E, SPASS, and Vampire together
   368 for 5 seconds yields the same success rate as running the most effective of
   369 these (Vampire) for 120 seconds \cite{boehme-nipkow-2010}.
   370 
   371 \opnodefault{atp}{string}
   372 Alias for \textit{atps}.
   373 
   374 \opfalse{overlord}{no\_overlord}
   375 Specifies whether Sledgehammer should put its temporary files in
   376 \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
   377 debugging Sledgehammer but also unsafe if several instances of the tool are run
   378 simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
   379 safely remove them after Sledgehammer has run.
   380 
   381 \nopagebreak
   382 {\small See also \textit{debug} (\S\ref{output-format}).}
   383 \end{enum}
   384 
   385 \subsection{Problem Encoding}
   386 \label{problem-encoding}
   387 
   388 \begin{enum}
   389 \opfalse{explicit\_apply}{implicit\_apply}
   390 Specifies whether function application should be encoded as an explicit
   391 ``apply'' operator. If the option is set to \textit{false}, each function will
   392 be directly applied to as many arguments as possible. Enabling this option can
   393 sometimes help discover higher-order proofs that otherwise would not be found.
   394 
   395 \opfalse{full\_types}{partial\_types}
   396 Specifies whether full-type information is exported. Enabling this option can
   397 prevent the discovery of type-incorrect proofs, but it also tends to slow down
   398 the ATPs significantly. For historical reasons, the default value of this option
   399 can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle''
   400 menu in Proof General.
   401 
   402 \opdefault{relevance\_threshold}{int}{50}
   403 Specifies the threshold above which facts are considered relevant by the
   404 relevance filter. The option ranges from 0 to 100, where 0 means that all
   405 theorems are relevant.
   406 
   407 \opdefault{relevance\_convergence}{int}{320}
   408 Specifies the convergence quotient, multiplied by 100, used by the relevance
   409 filter. This quotient is used by the relevance filter to scale down the
   410 relevance of facts at each iteration of the filter.
   411 
   412 \opsmartx{theory\_relevant}{theory\_irrelevant}
   413 Specifies whether the theory from which a fact comes should be taken into
   414 consideration by the relevance filter. If the option is set to \textit{smart},
   415 it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire,
   416 because empirical results suggest that these are the best settings.
   417 
   418 \opfalse{defs\_relevant}{defs\_irrelevant}
   419 Specifies whether the definition of constants occurring in the formula to prove
   420 should be considered particularly relevant. Enabling this option tends to lead
   421 to larger problems and typically slows down the ATPs.
   422 
   423 \optrue{respect\_no\_atp}{ignore\_no\_atp}
   424 Specifies whether Sledgehammer should honor the \textit{no\_atp} attributes. The
   425 \textit{no\_atp} attributes marks theorems that tend to confuse ATPs, typically
   426 because they can lead to unsound ATP proofs \cite{boehme-nipkow-2010}. It is
   427 normally a good idea to leave this option enabled, unless you are debugging
   428 Sledgehammer.
   429 
   430 \end{enum}
   431 
   432 \subsection{Output Format}
   433 \label{output-format}
   434 
   435 \begin{enum}
   436 
   437 \opfalse{verbose}{quiet}
   438 Specifies whether the \textbf{sledgehammer} command should explain what it does.
   439 
   440 \opfalse{debug}{no\_debug}
   441 Specifies whether Nitpick should display additional debugging information beyond
   442 what \textit{verbose} already displays. Enabling \textit{debug} also enables
   443 \textit{verbose} behind the scenes.
   444 
   445 \nopagebreak
   446 {\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
   447 
   448 \opfalse{isar\_proof}{no\_isar\_proof}
   449 Specifies whether Isar proofs should be output in addition to one-liner
   450 \textit{metis} proofs. Isar proof construction is still experimental and often
   451 fails; however, they are usually faster and sometimes more robust than
   452 \textit{metis} proofs.
   453 
   454 \opdefault{isar\_shrink\_factor}{int}{1}
   455 Specifies the granularity of the Isar proof. A value of $n$ indicates that each
   456 Isar proof step should correspond to a group of up to $n$ consecutive proof
   457 steps in the ATP proof.
   458 
   459 \end{enum}
   460 
   461 \subsection{Timeouts}
   462 \label{timeouts}
   463 
   464 \begin{enum}
   465 \opdefault{timeout}{time}{$\mathbf{60}$ s}
   466 Specifies the maximum amount of time that the ATPs should spend looking for a
   467 proof. For historical reasons, the default value of this option can be
   468 overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle''
   469 menu in Proof General.
   470 
   471 \opdefault{minimize\_timeout}{time}{$\mathbf{5}$\,s}
   472 Specifies the maximum amount of time that the ATPs should spend looking for a
   473 proof for \textbf{sledgehammer}~\textit{minimize}.
   474 \end{enum}
   475 
   476 \let\em=\sl
   477 \bibliography{../manual}{}
   478 \bibliographystyle{abbrv}
   479 
   480 \end{document}