Sledgehammer/document/root.tex

65 {\normalsize Computer Laboratory, University of Cambridge} \\
114 The problem passed to the external provers (or solvers) consists of your current
115 goal together with a heuristic selection of hundreds of facts (theorems) from the
118 The result of a successful proof search is some source text that usually (but
126 Isabelle > General.'' In this mode, a reduced version of Sledgehammer is run on
136 imported---this is rarely a problem in practice since it is part of
137 \textit{Main}. Examples of Sledgehammer use can be found in Isabelle's
146 Sledgehammer is part of Isabelle, so you do not need to install it. However, it
203 of the executable, \emph{including the file name}. Sledgehammer has been tested
205 Since Z3's output format is somewhat unstable, other versions of the solver
213 in \S\ref{first-steps}. If the remote versions of any of these provers is used
247 Instead of issuing the \textbf{sledgehammer} command, you can also use the
265 provers are installed and how many processor cores are available, some of the
287 This section presents a few hints that should help you get the most out of
302 undirected, they often prove theorems that require the reverse orientation of a
310 Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of
311 the options are very specialized, but serious users of the tool should at least
315 \item[\labelitemi] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies
323 specifies the maximum number of facts that should be passed to the provers. By
330 \textit{smt} proofs. The length of the Isar proofs can be controlled by setting
338 (\S\ref{command-syntax}). The command also prints the list of all available
370 the hundreds of facts that are picked up. The filter is also memoryless: It has
377 problem of finding relevant facts.
383 The number of facts included in a problem varies from prover to prover, since
384 some provers get overwhelmed more easily than others. You can show the number of
388 Sledgehammer is good at finding short proofs combining a handful of existing
390 number of facts, by setting the \textit{max\_facts} option
393 You can also influence which facts are actually selected in a number of ways. If
443 Earlier versions of Sledgehammer often suggested unsound proofs---either proofs
444 of nontheorems or simply proofs that rely on type-unsound inferences. This
445 is a thing of the past, unless you explicitly specify an unsound encoding
448 Officially, the only form of ``unsoundness'' that lurks in the sound
449 encodings is related to missing characteristic theorems of datatypes. For
461 We hope to address this problem in a future version of Isabelle. In the
471 versions of Metis. It is somewhat slower than \textit{metis}, but the proof
476 generated by Sledgehammer instead of \textit{metis} if the proof obviously
479 various sets of option for up to 1~second each time to ensure that the generated
484 At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})
505 Orthogonally to the encoding of types, it is important to choose an appropriate
506 translation of $\lambda$-abstractions. Metis supports three translation schemes,
507 in decreasing order of power: Curry combinators (the default),
516 Sledgehammer includes a minimization tool that takes a set of facts returned by
517 a given prover and repeatedly calls a prover or proof method with subsets of
518 those facts to find a minimal set. Reducing the number of facts typically helps
521 In earlier versions of Sledgehammer, generated proofs were systematically
524 (\S\ref{mode-of-operation}).
544 Sledgehammer's philosophy should work out of the box, without user guidance.
545 Many of the options are meant to be used mostly by the Sledgehammer developers
563 In the general syntax, the \qty{subcommand} may be any of the following:
569 \item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of
571 \S\ref{mode-of-operation} for more information on how to install automatic
574 \item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
593 \textit{prover} (\S\ref{mode-of-operation}) and \textit{timeout}
607 \qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
623 The \qty{facts\_override} argument lets you alter the set of facts that go
624 through the relevance filter. It may be of the form ``(\qty{facts})'', where
625 \qty{facts} is a space-separated list of Isabelle facts (theorems, local
627 facts are used. It may also be of the form ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}})'',
636 \textit{provers} (\S\ref{mode-of-operation}) is considered (typically E),
637 \textit{slice} (\S\ref{mode-of-operation}) is disabled,
656 where \qty{facts} is a list of arbitrary facts and \qty{options} is a
657 comma-separated list consisting of at most one $\lambda$ translation scheme
694 Sledgehammer's options are categorized as follows:\ mode of operation
695 (\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),
709 expressing a number of seconds.
710 \item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers
721 \subsection{Mode of Operation}
722 \label{mode-of-operation}
750 set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
756 complete path of the executable, including the file name, or install the
768 developed by Josef Urban that implements strategy scheduling on top of E. To use
775 \item[\labelitemi] \textbf{\textit{ehoh}:} Ehoh is an experimental version of
776 E that supports a $\lambda$-free fragment of higher-order logic. Use at your
824 \texttt{VERIT\_SOLVER} to the complete path of the executable, including the
829 \texttt{Z3\_SOLVER} to the complete path of the executable, including the
830 file name. Sledgehammer has been tested with a pre-release version of 4.4.0.
832 \item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to
834 (TF0). It is included for experimental purposes. It requires version 4.3.1 of
850 \item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of
853 \item[\labelitemi] \textbf{\textit{remote\_alt\_ergo}:} The remote version of
856 \item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs
860 remote version of iProver runs on Geoff Sutcliffe's Miami servers
863 \item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
866 \item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III
871 The remote version of Pirate run on a private server he generously set up.
875 version of SNARK runs on Geoff Sutcliffe's Miami servers.
877 \item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
883 corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister
887 version of Zipperposition runs on Geoff Sutcliffe's Miami servers.
890 By default, Sledgehammer runs a subset of CVC4, E, SPASS, Vampire, veriT, and
891 Z3 in parallel, either locally or remotely---depending on the number of
900 segments, each of which has its own set of possibly prover-dependent options.
902 set-of-support (SOS) strategy, whereas the second slice runs without it. For E,
904 number of facts. For SMT solvers, several slices are tried with the same options
905 each time but fewer and fewer facts. According to benchmarks with a timeout of
923 These statistics can be useful to the developers of Sledgehammer. If you are willing to have your
924 interactions recorded in the name of science, please enable this feature and send the statistics
925 file every now and then to the author of this manual (\authoremail).
926 To change the default value of this option globally, set the environment variable
935 debugging Sledgehammer but also unsafe if several instances of the tool are run
961 \item[\labelitemi] \textbf{\textit{nb}} is an implementation of naive Bayes.
963 \item[\labelitemi] \textbf{\textit{knn}} is an implementation of $k$-nearest
967 and \textbf{\textit{sml}}) is a combination of naive Bayes and $k$-nearest
983 \item[\labelitemi] \textbf{\textit{smart}:} A combination of MePo, MaSh, and
989 Specifies the maximum number of facts that may be returned by the relevance
996 relevance filter. The first threshold is used for the first iteration of the
1008 Specifies the maximum number of monomorphic instances to generate beyond
1019 Specifies the maximum number of iterations for the monomorphization fixpoint
1047 supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions,
1054 equational definitions of the combinators are very prolific in the context of
1058 supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a
1061 \item[\labelitemi] \textbf{\textit{combs\_or\_lifting}:} For each cluster of
1074 irrespective of the value of this option.
1078 applications of curried functions in ATP problems.
1081 Specifies the type encoding to use in ATP problems. Some of the type encodings
1084 listed below, with an indication of their soundness in parentheses.
1123 instead of being supplied as ground term arguments. The binary predicate
1150 each of these, Sledgehammer also provides a lighter variant identified by a
1153 but rather replaced by a shared uniform type of individuals.) As argument to the
1162 Even lighter versions of the `\hbox{?}' encodings. As argument to the
1170 Alternative versions of the `\hbox{??}' encodings. As argument to the
1175 Lighter versions of \textit{poly\_args} and \textit{raw\_mono\_args}.
1182 of the value of this option.
1191 for reconstruction with \textit{metis}, at the cost of some clutter in the
1211 {\small See also \textit{spy} (\S\ref{mode-of-operation}) and
1212 \textit{overlord} (\S\ref{mode-of-operation}).}
1216 The construction of Isar proof is still experimental and may sometimes fail;
1222 Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
1223 is explicitly enabled. A value of $n$ indicates that each Isar proof step should
1224 correspond to a group of up to $n$ consecutive proof steps in the ATP proof. If
1235 The collection of methods is roughly the same as for the \textbf{try0} command.
1250 Specifies the expected outcome, which must be one of the following:
1273 Specifies the maximum number of seconds that the automatic provers should spend
1277 Specifies the maximum number of seconds that \textit{metis} or other proof
1283 {\small See also \textit{minimize} (\S\ref{mode-of-operation}).}