author | wenzelm |
Wed, 18 Jul 2018 16:44:01 +0200 | |
changeset 68649 | f849fc1cb65e |
parent 68565 | 1b9462304e1d |
child 70818 | 13d6b561b0ea |
permissions | -rw-r--r-- |
36926 | 1 |
\documentclass[a4paper,12pt]{article} |
60185
cc71f01f9fde
prefer lmodern, which produces scalable T1 fonts even with Debian-ized TeXLive;
wenzelm
parents:
59963
diff
changeset
|
2 |
\usepackage{lmodern} |
36926 | 3 |
\usepackage[T1]{fontenc} |
4 |
\usepackage{amsmath} |
|
5 |
\usepackage{amssymb} |
|
53091 | 6 |
\usepackage[english]{babel} |
36926 | 7 |
\usepackage{color} |
8 |
\usepackage{footmisc} |
|
9 |
\usepackage{graphicx} |
|
10 |
%\usepackage{mathpazo} |
|
11 |
\usepackage{multicol} |
|
12 |
\usepackage{stmaryrd} |
|
13 |
%\usepackage[scaled=.85]{beramono} |
|
48962
a1acc1cb0271
more standard document preparation within session context;
wenzelm
parents:
48803
diff
changeset
|
14 |
\usepackage{isabelle,iman,pdfsetup} |
36926 | 15 |
|
68649 | 16 |
\newcommand\download{\url{https://isabelle.in.tum.de/components/}} |
46242 | 17 |
|
57040 | 18 |
\let\oldS=\S |
19 |
\def\S{\oldS\,} |
|
20 |
||
43216 | 21 |
\def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}} |
22 |
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$} |
|
23 |
||
45516 | 24 |
\newcommand\const[1]{\textsf{#1}} |
25 |
||
36926 | 26 |
%\oddsidemargin=4.6mm |
27 |
%\evensidemargin=4.6mm |
|
28 |
%\textwidth=150mm |
|
29 |
%\topmargin=4.6mm |
|
30 |
%\headheight=0mm |
|
31 |
%\headsep=0mm |
|
32 |
%\textheight=234mm |
|
33 |
||
34 |
\def\Colon{\mathord{:\mkern-1.5mu:}} |
|
35 |
%\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}} |
|
36 |
%\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}} |
|
37 |
\def\lparr{\mathopen{(\mkern-4mu\mid}} |
|
38 |
\def\rparr{\mathclose{\mid\mkern-4mu)}} |
|
39 |
||
40 |
\def\unk{{?}} |
|
41 |
\def\undef{(\lambda x.\; \unk)} |
|
42 |
%\def\unr{\textit{others}} |
|
43 |
\def\unr{\ldots} |
|
44 |
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}} |
|
45 |
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}} |
|
46 |
||
47 |
\urlstyle{tt} |
|
48 |
||
55290 | 49 |
\renewcommand\_{\hbox{\textunderscore\kern-.05ex}} |
50 |
||
36926 | 51 |
\begin{document} |
52 |
||
45516 | 53 |
%%% TYPESETTING |
54 |
%\renewcommand\labelitemi{$\bullet$} |
|
55 |
\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}} |
|
56 |
||
36926 | 57 |
\title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex] |
58 |
Hammering Away \\[\smallskipamount] |
|
59 |
\Large A User's Guide to Sledgehammer for Isabelle/HOL} |
|
60 |
\author{\hbox{} \\ |
|
61 |
Jasmin Christian Blanchette \\ |
|
43002
e88fde86e4c2
mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents:
42996
diff
changeset
|
62 |
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount] |
e88fde86e4c2
mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents:
42996
diff
changeset
|
63 |
{\normalsize with contributions from} \\[4\smallskipamount] |
e88fde86e4c2
mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents:
42996
diff
changeset
|
64 |
Lawrence C. Paulson \\ |
e88fde86e4c2
mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents:
42996
diff
changeset
|
65 |
{\normalsize Computer Laboratory, University of Cambridge} \\ |
36926 | 66 |
\hbox{}} |
67 |
||
68 |
\maketitle |
|
69 |
||
70 |
\tableofcontents |
|
71 |
||
72 |
\setlength{\parskip}{.7em plus .2em minus .1em} |
|
73 |
\setlength{\parindent}{0pt} |
|
74 |
\setlength{\abovedisplayskip}{\parskip} |
|
75 |
\setlength{\abovedisplayshortskip}{.9\parskip} |
|
76 |
\setlength{\belowdisplayskip}{\parskip} |
|
77 |
\setlength{\belowdisplayshortskip}{.9\parskip} |
|
78 |
||
52078 | 79 |
% general-purpose enum environment with correct spacing |
36926 | 80 |
\newenvironment{enum}% |
81 |
{\begin{list}{}{% |
|
82 |
\setlength{\topsep}{.1\parskip}% |
|
83 |
\setlength{\partopsep}{.1\parskip}% |
|
84 |
\setlength{\itemsep}{\parskip}% |
|
85 |
\advance\itemsep by-\parsep}} |
|
86 |
{\end{list}} |
|
87 |
||
88 |
\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin |
|
89 |
\advance\rightskip by\leftmargin} |
|
90 |
\def\post{\vskip0pt plus1ex\endgroup} |
|
91 |
||
92 |
\def\prew{\pre\advance\rightskip by-\leftmargin} |
|
93 |
\def\postw{\post} |
|
94 |
||
68565 | 95 |
|
36926 | 96 |
\section{Introduction} |
97 |
\label{introduction} |
|
98 |
||
42964
bf45fd2488a2
document primitive support for LEO-II and Satallax
blanchet
parents:
42945
diff
changeset
|
99 |
Sledgehammer is a tool that applies automatic theorem provers (ATPs) |
47561
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset
|
100 |
and satisfiability-modulo-theories (SMT) solvers on the current goal.% |
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset
|
101 |
\footnote{The distinction between ATPs and SMT solvers is convenient but mostly |
68565 | 102 |
historical.} |
47561
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset
|
103 |
% |
55334
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset
|
104 |
The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E |
52078 | 105 |
\cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF \cite{tofof}, iProver |
106 |
\cite{korovin-2009}, iProver-Eq \cite{korovin-sticksel-2010}, LEO-II |
|
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66735
diff
changeset
|
107 |
\cite{leo2}, Leo-III \cite{leo3}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS |
58497
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
108 |
\cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
109 |
Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}. |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
110 |
The ATPs are run either locally or remotely via the System\-On\-TPTP web service |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
111 |
\cite{sutcliffe-2000}. The supported SMT solvers are CVC3 \cite{cvc3}, CVC4 |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
112 |
\cite{cvc4}, veriT \cite{bouton-et-al-2009}, and Z3 \cite{z3}. These are always |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
113 |
run locally. |
36926 | 114 |
|
57241 | 115 |
The problem passed to the external provers (or solvers) consists of your current |
116 |
goal together with a heuristic selection of hundreds of facts (theorems) from the |
|
52078 | 117 |
current theory context, filtered by relevance. |
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
118 |
|
40073 | 119 |
The result of a successful proof search is some source text that usually (but |
120 |
not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
121 |
proof typically relies on the general-purpose \textit{metis} proof method, which |
45380 | 122 |
integrates the Metis ATP in Isabelle/HOL with explicit inferences going through |
123 |
the kernel. Thus its results are correct by construction. |
|
36926 | 124 |
|
53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset
|
125 |
For Isabelle/jEdit users, Sledgehammer provides an automatic mode that can be |
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset
|
126 |
enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options > |
54114 | 127 |
Isabelle > General.'' In this mode, a reduced version of Sledgehammer is run on |
128 |
every newly entered theorem for a few seconds. |
|
39320 | 129 |
|
36926 | 130 |
\newbox\boxA |
46298 | 131 |
\setbox\boxA=\hbox{\texttt{NOSPAM}} |
36926 | 132 |
|
46298 | 133 |
\newcommand\authoremail{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak |
42763 | 134 |
in.\allowbreak tum.\allowbreak de}} |
135 |
||
40689 | 136 |
To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is |
137 |
imported---this is rarely a problem in practice since it is part of |
|
138 |
\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's |
|
36926 | 139 |
\texttt{src/HOL/Metis\_Examples} directory. |
140 |
Comments and bug reports concerning Sledgehammer or this manual should be |
|
42883 | 141 |
directed to the author at \authoremail. |
36926 | 142 |
|
143 |
||
144 |
\section{Installation} |
|
145 |
\label{installation} |
|
146 |
||
48387 | 147 |
Sledgehammer is part of Isabelle, so you do not need to install it. However, it |
46242 | 148 |
relies on third-party automatic provers (ATPs and SMT solvers). |
42763 | 149 |
|
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66735
diff
changeset
|
150 |
Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and |
58497
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
151 |
Zipperposition can be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF, |
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66735
diff
changeset
|
152 |
iProver, iProver-Eq, LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are |
58497
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
153 |
available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
154 |
CVC3, CVC4, veriT, and Z3 can be run locally. |
36926 | 155 |
|
46242 | 156 |
There are three main ways to install automatic provers on your machine: |
36926 | 157 |
|
46242 | 158 |
\begin{sloppy} |
159 |
\begin{enum} |
|
160 |
\item[\labelitemi] If you installed an official Isabelle package, it should |
|
68565 | 161 |
already include properly setup executables for CVC4, E, SPASS, Vampire, veriT, |
162 |
and Z3, ready to use. To use Vampire, you must confirm that you are a |
|
163 |
noncommercial user, as indicated by the message that is displayed when |
|
164 |
Sledgehammer is invoked the first time. |
|
46242 | 165 |
|
59510 | 166 |
\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, |
68565 | 167 |
CVC4, E, SPASS, Vampire, and Z3 binary packages from \download. Extract the |
168 |
archives, then add a line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash |
|
59510 | 169 |
components}% |
41747
f58d4d202924
fix path to etc/settings and etc/components in doc
blanchet
parents:
41740
diff
changeset
|
170 |
\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at |
46242 | 171 |
startup. Its value can be retrieved by executing \texttt{isabelle} |
41747
f58d4d202924
fix path to etc/settings and etc/components in doc
blanchet
parents:
41740
diff
changeset
|
172 |
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.} |
68565 | 173 |
file with the absolute path to CVC3, CVC4, E, SPASS, Vampire, or Z3. For |
174 |
example, if the \texttt{components} file does not exist yet and you extracted |
|
175 |
SPASS to \texttt{/usr/local/spass-3.8ds}, create it with the single line |
|
36926 | 176 |
|
177 |
\prew |
|
47577 | 178 |
\texttt{/usr/local/spass-3.8ds} |
36926 | 179 |
\postw |
180 |
||
47561
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset
|
181 |
in it. |
38043 | 182 |
|
68565 | 183 |
\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II, |
184 |
Leo-III, or Satallax manually, set the environment variable |
|
52078 | 185 |
\texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME}, |
68565 | 186 |
\texttt{LEO3\_HOME}, or \texttt{SATALLAX\_HOME} |
187 |
to the directory that contains the \texttt{agsyHOL}, |
|
52757 | 188 |
\texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}), |
68565 | 189 |
\texttt{leo}, \texttt{leo3}, or \texttt{satallax} executable; |
190 |
for Alt-Ergo, set the environment variable \texttt{WHY3\_HOME} to the |
|
191 |
directory that contains the \texttt{why3} executable. Sledgehammer has been |
|
192 |
tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 2.0, LEO-II 1.3.4, Leo-III |
|
193 |
1.1, and Satallax 2.2 to 2.7. Since the ATPs' output formats are neither |
|
194 |
documented nor stable, other versions might not work well with Sledgehammer. |
|
195 |
Ideally, you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION}, |
|
196 |
\texttt{LEO3\_VERSION}, or \texttt{SATALLAX\_VERSION} to the prover's version |
|
197 |
number (e.g., ``2.7''). |
|
36926 | 198 |
|
58497
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
199 |
Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
200 |
variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER}, |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
201 |
\texttt{VERIT\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path |
57241 | 202 |
of the executable, \emph{including the file name}. Sledgehammer has been tested |
59034 | 203 |
with CVC3 2.2 and 2.4.1, CVC4 1.5-prerelease, veriT smtcomp2014, and Z3 4.3.2. |
204 |
Since Z3's output format is somewhat unstable, other versions of the solver |
|
205 |
might not work well with Sledgehammer. Ideally, also set |
|
58497
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
206 |
\texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, \texttt{VERIT\_VERSION}, or |
59961 | 207 |
\texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.4.0''). |
46242 | 208 |
\end{enum} |
209 |
\end{sloppy} |
|
36926 | 210 |
|
66735 | 211 |
To check whether the provers are successfully installed, try out the example |
212 |
in \S\ref{first-steps}. If the remote versions of any of these provers is used |
|
213 |
(identified by the prefix ``\textit{remote\_\/}''), or if the local versions |
|
214 |
fail to solve the easy goal presented there, something must be wrong with the |
|
215 |
installation. |
|
46242 | 216 |
|
217 |
Remote prover invocation requires Perl with the World Wide Web Library |
|
218 |
(\texttt{libwww-perl}) installed. If you must use a proxy server to access the |
|
219 |
Internet, set the \texttt{http\_proxy} environment variable to the proxy, either |
|
220 |
in the environment in which Isabelle is launched or in your |
|
47561
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset
|
221 |
\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few |
46242 | 222 |
examples: |
39152
f09b378cb252
make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents:
38997
diff
changeset
|
223 |
|
f09b378cb252
make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents:
38997
diff
changeset
|
224 |
\prew |
39153 | 225 |
\texttt{http\_proxy=http://proxy.example.org} \\ |
226 |
\texttt{http\_proxy=http://proxy.example.org:8080} \\ |
|
227 |
\texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org} |
|
39152
f09b378cb252
make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents:
38997
diff
changeset
|
228 |
\postw |
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
229 |
|
68565 | 230 |
|
36926 | 231 |
\section{First Steps} |
232 |
\label{first-steps} |
|
233 |
||
234 |
To illustrate Sledgehammer in context, let us start a theory file and |
|
235 |
attempt to prove a simple lemma: |
|
236 |
||
237 |
\prew |
|
238 |
\textbf{theory}~\textit{Scratch} \\ |
|
239 |
\textbf{imports}~\textit{Main} \\ |
|
240 |
\textbf{begin} \\[2\smallskipamount] |
|
241 |
% |
|
42945 | 242 |
\textbf{lemma} ``$[a] = [b] \,\Longrightarrow\, a = b$'' \\ |
36926 | 243 |
\textbf{sledgehammer} |
244 |
\postw |
|
245 |
||
53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset
|
246 |
Instead of issuing the \textbf{sledgehammer} command, you can also use the |
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset
|
247 |
Sledgehammer panel in Isabelle/jEdit. Sledgehammer produces the following output |
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset
|
248 |
after a few seconds: |
36926 | 249 |
|
250 |
\prew |
|
251 |
\slshape |
|
62737 | 252 |
Proof found\ldots \\ |
63729 | 253 |
``\textit{e\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms) \\ |
42945 | 254 |
% |
63729 | 255 |
``\textit{cvc4\/}'': Try this: \textbf{by} \textit{simp} (0.4 ms) \\ |
46242 | 256 |
% |
63729 | 257 |
``\textit{z3\/}'': Try this: \textbf{by} \textit{simp} (0.5 ms) \\ |
60568
a9b71c82647b
put E before (typically remote, hence less reliable) Vampire
blanchet
parents:
60306
diff
changeset
|
258 |
% |
63729 | 259 |
``\textit{spass\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms) |
62737 | 260 |
% |
36926 | 261 |
\postw |
262 |
||
60568
a9b71c82647b
put E before (typically remote, hence less reliable) Vampire
blanchet
parents:
60306
diff
changeset
|
263 |
Sledgehammer ran CVC4, E, SPASS, and Z3 in parallel. Depending on which |
59963 | 264 |
provers are installed and how many processor cores are available, some of the |
265 |
provers might be missing or present with a \textit{remote\_} prefix. |
|
36926 | 266 |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
267 |
For each successful prover, Sledgehammer gives a one-line \textit{metis} or |
61283 | 268 |
\textit{smt} method call. Rough timings are shown in parentheses, indicating how |
48387 | 269 |
fast the call is. You can click the proof to insert it into the theory text. |
36926 | 270 |
|
51190
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51189
diff
changeset
|
271 |
In addition, you can ask Sledgehammer for an Isar text proof by enabling the |
49919 | 272 |
\textit{isar\_proofs} option (\S\ref{output-format}): |
36926 | 273 |
|
274 |
\prew |
|
49919 | 275 |
\textbf{sledgehammer} [\textit{isar\_proofs}] |
36926 | 276 |
\postw |
277 |
||
278 |
When Isar proof construction is successful, it can yield proofs that are more |
|
61283 | 279 |
readable and also faster than the \textit{metis} or \textit{smt} one-line |
56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset
|
280 |
proofs. This feature is experimental and is only available for ATPs. |
36926 | 281 |
|
68565 | 282 |
|
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
283 |
\section{Hints} |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
284 |
\label{hints} |
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
285 |
|
42884 | 286 |
This section presents a few hints that should help you get the most out of |
46643
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset
|
287 |
Sledgehammer. Frequently asked questions are answered in |
45380 | 288 |
\S\ref{frequently-asked-questions}. |
42884 | 289 |
|
46242 | 290 |
%\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak} |
291 |
\newcommand\point[1]{\subsection{\emph{#1}}} |
|
42763 | 292 |
|
68565 | 293 |
|
42763 | 294 |
\point{Presimplify the goal} |
295 |
||
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
296 |
For best results, first simplify your problem by calling \textit{auto} or at |
42945 | 297 |
least \textit{safe} followed by \textit{simp\_all}. The SMT solvers provide |
298 |
arithmetic decision procedures, but the ATPs typically do not (or if they do, |
|
299 |
Sledgehammer does not use it yet). Apart from Waldmeister, they are not |
|
53759
a198ce71de11
took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents:
53757
diff
changeset
|
300 |
particularly good at heavy rewriting, but because they regard equations as |
42945 | 301 |
undirected, they often prove theorems that require the reverse orientation of a |
302 |
\textit{simp} rule. Higher-order problems can be tackled, but the success rate |
|
303 |
is better for first-order problems. Hence, you may get better results if you |
|
304 |
first simplify the problem to remove higher-order features. |
|
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
305 |
|
68565 | 306 |
|
53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset
|
307 |
\point{Familiarize yourself with the main options} |
42763 | 308 |
|
309 |
Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of |
|
310 |
the options are very specialized, but serious users of the tool should at least |
|
311 |
familiarize themselves with the following options: |
|
312 |
||
313 |
\begin{enum} |
|
45516 | 314 |
\item[\labelitemi] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies |
42884 | 315 |
the automatic provers (ATPs and SMT solvers) that should be run whenever |
68565 | 316 |
Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{cvc4 e spass |
317 |
vampire\/}''). For convenience, you can omit ``\textit{provers}~='' |
|
318 |
and simply write the prover names as a space-separated list (e.g., ``\textit{cvc4 e |
|
319 |
spass vampire\/}''). |
|
42763 | 320 |
|
48294 | 321 |
\item[\labelitemi] \textbf{\textit{max\_facts}} (\S\ref{relevance-filter}) |
42884 | 322 |
specifies the maximum number of facts that should be passed to the provers. By |
48294 | 323 |
default, the value is prover-dependent but varies between about 50 and 1000. If |
324 |
the provers time out, you can try lowering this value to, say, 25 or 50 and see |
|
42884 | 325 |
if that helps. |
42763 | 326 |
|
49919 | 327 |
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies |
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
328 |
that Isar proofs should be generated, in addition to one-line \textit{metis} or |
61283 | 329 |
\textit{smt} proofs. The length of the Isar proofs can be controlled by setting |
57245 | 330 |
\textit{compress} (\S\ref{output-format}). |
43038 | 331 |
|
45516 | 332 |
\item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the |
61317 | 333 |
provers' time limit. It is set to 30 seconds by default. |
42763 | 334 |
\end{enum} |
335 |
||
42884 | 336 |
Options can be set globally using \textbf{sledgehammer\_params} |
43010
a14cf580a5a5
readded Waldmeister as default to the documentation and other minor changes
blanchet
parents:
43008
diff
changeset
|
337 |
(\S\ref{command-syntax}). The command also prints the list of all available |
a14cf580a5a5
readded Waldmeister as default to the documentation and other minor changes
blanchet
parents:
43008
diff
changeset
|
338 |
options with their current value. Fact selection can be influenced by specifying |
a14cf580a5a5
readded Waldmeister as default to the documentation and other minor changes
blanchet
parents:
43008
diff
changeset
|
339 |
``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} call |
a14cf580a5a5
readded Waldmeister as default to the documentation and other minor changes
blanchet
parents:
43008
diff
changeset
|
340 |
to ensure that certain facts are included, or simply ``$(\textit{my\_facts})$'' |
58090 | 341 |
to force Sledgehammer to run only with $\textit{my\_facts}$ (and any facts |
342 |
chained into the goal). |
|
42763 | 343 |
|
68565 | 344 |
|
42763 | 345 |
\section{Frequently Asked Questions} |
346 |
\label{frequently-asked-questions} |
|
347 |
||
42945 | 348 |
This sections answers frequently (and infrequently) asked questions about |
48387 | 349 |
Sledgehammer. It is a good idea to skim over it now even if you do not have any |
42945 | 350 |
questions at this stage. And if you have any further questions not listed here, |
351 |
send them to the author at \authoremail. |
|
352 |
||
68565 | 353 |
|
43008
bb212c2ad238
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents:
43007
diff
changeset
|
354 |
\point{Which facts are passed to the automatic provers?} |
42883 | 355 |
|
48387 | 356 |
Sledgehammer heuristically selects a few hundred relevant lemmas from the |
357 |
currently loaded libraries. The component that performs this selection is |
|
61043 | 358 |
called \emph{relevance filter} (\S\ref{relevance-filter}). |
48387 | 359 |
|
360 |
\begin{enum} |
|
361 |
\item[\labelitemi] |
|
48388 | 362 |
The traditional relevance filter, called \emph{MePo} |
363 |
(\underline{Me}ng--\underline{Pau}lson), assigns a score to every available fact |
|
364 |
(lemma, theorem, definition, or axiom) based upon how many constants that fact |
|
365 |
shares with the conjecture. This process iterates to include facts relevant to |
|
366 |
those just accepted. The constants are weighted to give unusual ones greater |
|
367 |
significance. MePo copes best when the conjecture contains some unusual |
|
368 |
constants; if all the constants are common, it is unable to discriminate among |
|
369 |
the hundreds of facts that are picked up. The filter is also memoryless: It has |
|
370 |
no information about how many times a particular fact has been used in a proof, |
|
371 |
and it cannot learn. |
|
48387 | 372 |
|
373 |
\item[\labelitemi] |
|
57272
fd539459a112
enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
blanchet
parents:
57245
diff
changeset
|
374 |
An alternative to MePo is \emph{MaSh} (\underline{Ma}chine Learner for |
fd539459a112
enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
blanchet
parents:
57245
diff
changeset
|
375 |
\underline{S}ledge\underline{h}ammer). It applies machine learning to the |
fd539459a112
enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
blanchet
parents:
57245
diff
changeset
|
376 |
problem of finding relevant facts. |
48387 | 377 |
|
61043 | 378 |
\item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh. This is |
379 |
the default. |
|
48387 | 380 |
\end{enum} |
381 |
||
42883 | 382 |
The number of facts included in a problem varies from prover to prover, since |
43008
bb212c2ad238
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents:
43007
diff
changeset
|
383 |
some provers get overwhelmed more easily than others. You can show the number of |
42883 | 384 |
facts given using the \textit{verbose} option (\S\ref{output-format}) and the |
385 |
actual facts using \textit{debug} (\S\ref{output-format}). |
|
386 |
||
387 |
Sledgehammer is good at finding short proofs combining a handful of existing |
|
388 |
lemmas. If you are looking for longer proofs, you must typically restrict the |
|
48294 | 389 |
number of facts, by setting the \textit{max\_facts} option |
43574 | 390 |
(\S\ref{relevance-filter}) to, say, 25 or 50. |
42883 | 391 |
|
42996 | 392 |
You can also influence which facts are actually selected in a number of ways. If |
393 |
you simply want to ensure that a fact is included, you can specify it using the |
|
394 |
``$(\textit{add}{:}~\textit{my\_facts})$'' syntax. For example: |
|
395 |
% |
|
396 |
\prew |
|
397 |
\textbf{sledgehammer} (\textit{add}: \textit{hd.simps} \textit{tl.simps}) |
|
398 |
\postw |
|
399 |
% |
|
400 |
The specified facts then replace the least relevant facts that would otherwise be |
|
401 |
included; the other selected facts remain the same. |
|
402 |
If you want to direct the selection in a particular direction, you can specify |
|
403 |
the facts via \textbf{using}: |
|
404 |
% |
|
405 |
\prew |
|
406 |
\textbf{using} \textit{hd.simps} \textit{tl.simps} \\ |
|
407 |
\textbf{sledgehammer} |
|
408 |
\postw |
|
409 |
% |
|
410 |
The facts are then more likely to be selected than otherwise, and if they are |
|
411 |
selected at iteration $j$ they also influence which facts are selected at |
|
412 |
iterations $j + 1$, $j + 2$, etc. To give them even more weight, try |
|
413 |
% |
|
414 |
\prew |
|
415 |
\textbf{using} \textit{hd.simps} \textit{tl.simps} \\ |
|
416 |
\textbf{apply}~\textbf{--} \\ |
|
417 |
\textbf{sledgehammer} |
|
418 |
\postw |
|
419 |
||
68565 | 420 |
|
46300 | 421 |
\point{Why does Metis fail to reconstruct the proof?} |
422 |
||
423 |
There are many reasons. If Metis runs seemingly forever, that is a sign that the |
|
57736
5f37ef22f9af
update documentation after removal of 'min' subcommand
blanchet
parents:
57733
diff
changeset
|
424 |
proof is too difficult for it. Metis's search is complete for first-order logic |
68565 | 425 |
with equality, so if the proof was found by a superposition-based ATP such as |
426 |
E, SPASS, or Vampire, Metis should eventually find it, but that is little |
|
427 |
consolation. |
|
46300 | 428 |
|
429 |
In some rare cases, \textit{metis} fails fairly quickly, and you get the error |
|
57736
5f37ef22f9af
update documentation after removal of 'min' subcommand
blanchet
parents:
57733
diff
changeset
|
430 |
message ``One-line proof reconstruction failed.'' This indicates that |
5f37ef22f9af
update documentation after removal of 'min' subcommand
blanchet
parents:
57733
diff
changeset
|
431 |
Sledgehammer determined that the goal is provable, but the proof is, for |
5f37ef22f9af
update documentation after removal of 'min' subcommand
blanchet
parents:
57733
diff
changeset
|
432 |
technical reasons, beyond \textit{metis}'s power. You can then try again with |
5f37ef22f9af
update documentation after removal of 'min' subcommand
blanchet
parents:
57733
diff
changeset
|
433 |
the \textit{strict} option (\S\ref{problem-encoding}). |
46300 | 434 |
|
46640 | 435 |
If the goal is actually unprovable and you did not specify an unsound encoding |
46300 | 436 |
using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are |
437 |
strongly encouraged to report this to the author at \authoremail. |
|
438 |
||
68565 | 439 |
|
46300 | 440 |
\point{How can I tell whether a suggested proof is sound?} |
441 |
||
442 |
Earlier versions of Sledgehammer often suggested unsound proofs---either proofs |
|
443 |
of nontheorems or simply proofs that rely on type-unsound inferences. This |
|
46640 | 444 |
is a thing of the past, unless you explicitly specify an unsound encoding |
46300 | 445 |
using \textit{type\_enc} (\S\ref{problem-encoding}). |
446 |
% |
|
447 |
Officially, the only form of ``unsoundness'' that lurks in the sound |
|
448 |
encodings is related to missing characteristic theorems of datatypes. For |
|
449 |
example, |
|
450 |
||
451 |
\prew |
|
452 |
\textbf{lemma}~``$\exists \mathit{xs}.\; \mathit{xs} \neq []$'' \\ |
|
453 |
\textbf{sledgehammer} () |
|
454 |
\postw |
|
455 |
||
456 |
suggests an argumentless \textit{metis} call that fails. However, the conjecture |
|
457 |
does actually hold, and the \textit{metis} call can be repaired by adding |
|
458 |
\textit{list.distinct}. |
|
459 |
% |
|
460 |
We hope to address this problem in a future version of Isabelle. In the |
|
461 |
meantime, you can avoid it by passing the \textit{strict} option |
|
462 |
(\S\ref{problem-encoding}). |
|
463 |
||
68565 | 464 |
|
46298 | 465 |
\point{What are the \textit{full\_types}, \textit{no\_types}, and |
466 |
\textit{mono\_tags} arguments to Metis?} |
|
42883 | 467 |
|
46298 | 468 |
The \textit{metis}~(\textit{full\_types}) proof method |
469 |
and its cousin \textit{metis}~(\textit{mono\_tags}) are fully-typed |
|
53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset
|
470 |
versions of Metis. It is somewhat slower than \textit{metis}, but the proof |
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43217
diff
changeset
|
471 |
search is fully typed, and it also includes more powerful rules such as the |
45516 | 472 |
axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in |
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
473 |
higher-order places (e.g., in set comprehensions). The method is automatically |
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
474 |
tried as a fallback when \textit{metis} fails, and it is sometimes |
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43217
diff
changeset
|
475 |
generated by Sledgehammer instead of \textit{metis} if the proof obviously |
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43217
diff
changeset
|
476 |
requires type information or if \textit{metis} failed when Sledgehammer |
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43217
diff
changeset
|
477 |
preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with |
57719 | 478 |
various sets of option for up to 1~second each time to ensure that the generated |
46298 | 479 |
one-line proofs actually work and to display timing information. This can be |
47036 | 480 |
configured using the \textit{preplay\_timeout} and \textit{dont\_preplay} |
481 |
options (\S\ref{timeouts}).) |
|
46298 | 482 |
% |
43229 | 483 |
At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types}) |
484 |
uses no type information at all during the proof search, which is more efficient |
|
485 |
but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally |
|
486 |
generated by Sledgehammer. |
|
46298 | 487 |
% |
488 |
See the \textit{type\_enc} option (\S\ref{problem-encoding}) for details. |
|
43229 | 489 |
|
46298 | 490 |
Incidentally, if you ever see warnings such as |
42883 | 491 |
|
492 |
\prew |
|
43007 | 493 |
\slshape |
63729 | 494 |
Metis: Falling back on ``\textit{metis} (\textit{full\_types})'' |
42883 | 495 |
\postw |
496 |
||
45380 | 497 |
for a successful \textit{metis} proof, you can advantageously pass the |
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43217
diff
changeset
|
498 |
\textit{full\_types} option to \textit{metis} directly. |
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43217
diff
changeset
|
499 |
|
68565 | 500 |
|
46366 | 501 |
\point{And what are the \textit{lifting} and \textit{hide\_lams} arguments |
46298 | 502 |
to Metis?} |
503 |
||
504 |
Orthogonally to the encoding of types, it is important to choose an appropriate |
|
505 |
translation of $\lambda$-abstractions. Metis supports three translation schemes, |
|
506 |
in decreasing order of power: Curry combinators (the default), |
|
507 |
$\lambda$-lifting, and a ``hiding'' scheme that disables all reasoning under |
|
508 |
$\lambda$-abstractions. The more powerful schemes also give the automatic |
|
509 |
provers more rope to hang themselves. See the \textit{lam\_trans} option (\S\ref{problem-encoding}) for details. |
|
510 |
||
68565 | 511 |
|
512 |
\point{Are the generated proofs minimal?} |
|
43036 | 513 |
|
43054 | 514 |
Automatic provers frequently use many more facts than are necessary. |
57722 | 515 |
Sledgehammer includes a minimization tool that takes a set of facts returned by |
516 |
a given prover and repeatedly calls a prover or proof method with subsets of |
|
517 |
those facts to find a minimal set. Reducing the number of facts typically helps |
|
518 |
reconstruction, while also removing superfluous clutter from the proof scripts. |
|
43036 | 519 |
|
43229 | 520 |
In earlier versions of Sledgehammer, generated proofs were systematically |
521 |
accompanied by a suggestion to invoke the minimization tool. This step is now |
|
57722 | 522 |
performed by default but can be disabled using the \textit{minimize} option |
523 |
(\S\ref{mode-of-operation}). |
|
43036 | 524 |
|
68565 | 525 |
|
43008
bb212c2ad238
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents:
43007
diff
changeset
|
526 |
\point{A strange error occurred---what should I do?} |
42763 | 527 |
|
528 |
Sledgehammer tries to give informative error messages. Please report any strange |
|
63729 | 529 |
error to the author at \authoremail. |
42763 | 530 |
|
68565 | 531 |
|
42763 | 532 |
\point{Auto can solve it---why not Sledgehammer?} |
533 |
||
534 |
Problems can be easy for \textit{auto} and difficult for automatic provers, but |
|
48387 | 535 |
the reverse is also true, so do not be discouraged if your first attempts fail. |
39320 | 536 |
Because the system refers to all theorems known to Isabelle, it is particularly |
57040 | 537 |
suitable when your goal has a short proof but requires lemmas that you do not |
538 |
know about. |
|
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset
|
539 |
|
68565 | 540 |
|
42883 | 541 |
\point{Why are there so many options?} |
542 |
||
543 |
Sledgehammer's philosophy should work out of the box, without user guidance. |
|
544 |
Many of the options are meant to be used mostly by the Sledgehammer developers |
|
53102 | 545 |
for experiments. Of course, feel free to try them out if you are so inclined. |
42883 | 546 |
|
68565 | 547 |
|
36926 | 548 |
\section{Command Syntax} |
549 |
\label{command-syntax} |
|
550 |
||
46242 | 551 |
\subsection{Sledgehammer} |
57040 | 552 |
\label{sledgehammer} |
46242 | 553 |
|
36926 | 554 |
Sledgehammer can be invoked at any point when there is an open goal by entering |
555 |
the \textbf{sledgehammer} command in the theory file. Its general syntax is as |
|
556 |
follows: |
|
557 |
||
558 |
\prew |
|
43216 | 559 |
\textbf{sledgehammer} \qty{subcommand}$^?$ \qty{options}$^?$ \qty{facts\_override}$^?$ \qty{num}$^?$ |
36926 | 560 |
\postw |
561 |
||
43216 | 562 |
In the general syntax, the \qty{subcommand} may be any of the following: |
36926 | 563 |
|
564 |
\begin{enum} |
|
45516 | 565 |
\item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on |
43216 | 566 |
subgoal number \qty{num} (1 by default), with the given options and facts. |
36926 | 567 |
|
45516 | 568 |
\item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of |
41724 | 569 |
automatic provers supported by Sledgehammer. See \S\ref{installation} and |
570 |
\S\ref{mode-of-operation} for more information on how to install automatic |
|
571 |
provers. |
|
36926 | 572 |
|
48393 | 573 |
\item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote |
574 |
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}. |
|
575 |
\end{enum} |
|
576 |
||
49365 | 577 |
In addition, the following subcommands provide finer control over machine |
48393 | 578 |
learning with MaSh: |
579 |
||
580 |
\begin{enum} |
|
581 |
\item[\labelitemi] \textbf{\textit{unlearn}:} Resets MaSh, erasing any |
|
582 |
persistent state. |
|
48387 | 583 |
|
48393 | 584 |
\item[\labelitemi] \textbf{\textit{learn\_isar}:} Invokes MaSh on the current |
585 |
theory to process all the available facts, learning from their Isabelle/Isar |
|
586 |
proofs. This happens automatically at Sledgehammer invocations if the |
|
587 |
\textit{learn} option (\S\ref{relevance-filter}) is enabled. |
|
48387 | 588 |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50459
diff
changeset
|
589 |
\item[\labelitemi] \textbf{\textit{learn\_prover}:} Invokes MaSh on the current |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50459
diff
changeset
|
590 |
theory to process all the available facts, learning from proofs generated by |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50459
diff
changeset
|
591 |
automatic provers. The prover to use and its timeout can be set using the |
48393 | 592 |
\textit{prover} (\S\ref{mode-of-operation}) and \textit{timeout} |
66735 | 593 |
(\S\ref{timeouts}) options. It is recommended to perform learning using a |
594 |
first-order ATP (such as E, SPASS, and Vampire) as opposed to a |
|
48393 | 595 |
higher-order ATP or an SMT solver. |
596 |
||
597 |
\item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn} |
|
598 |
followed by \textit{learn\_isar}. |
|
599 |
||
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50459
diff
changeset
|
600 |
\item[\labelitemi] \textbf{\textit{relearn\_prover}:} Same as \textit{unlearn} |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50459
diff
changeset
|
601 |
followed by \textit{learn\_prover}. |
36926 | 602 |
\end{enum} |
603 |
||
43216 | 604 |
Sledgehammer's behavior can be influenced by various \qty{options}, which can be |
605 |
specified in brackets after the \textbf{sledgehammer} command. The |
|
606 |
\qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1, |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50459
diff
changeset
|
607 |
\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50459
diff
changeset
|
608 |
For example: |
36926 | 609 |
|
610 |
\prew |
|
49919 | 611 |
\textbf{sledgehammer} [\textit{isar\_proofs}, \,\textit{timeout} = 120] |
36926 | 612 |
\postw |
613 |
||
614 |
Default values can be set using \textbf{sledgehammer\_\allowbreak params}: |
|
615 |
||
616 |
\prew |
|
43216 | 617 |
\textbf{sledgehammer\_params} \qty{options} |
36926 | 618 |
\postw |
619 |
||
620 |
The supported options are described in \S\ref{option-reference}. |
|
621 |
||
43216 | 622 |
The \qty{facts\_override} argument lets you alter the set of facts that go |
623 |
through the relevance filter. It may be of the form ``(\qty{facts})'', where |
|
624 |
\qty{facts} is a space-separated list of Isabelle facts (theorems, local |
|
36926 | 625 |
assumptions, etc.), in which case the relevance filter is bypassed and the given |
43216 | 626 |
facts are used. It may also be of the form ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}})'', |
627 |
``(\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', or ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}}\ |
|
628 |
\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', where the relevance filter is instructed to |
|
629 |
proceed as usual except that it should consider \qty{facts\/_{\mathrm{1}}} |
|
630 |
highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant. |
|
36926 | 631 |
|
53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset
|
632 |
If you use Isabelle/jEdit, Sledgehammer also provides an automatic mode that can |
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset
|
633 |
be enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options |
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset
|
634 |
> Isabelle > General.'' For automatic runs, only the first prover set using |
54114 | 635 |
\textit{provers} (\S\ref{mode-of-operation}) is considered (typically E), |
636 |
\textit{slice} (\S\ref{mode-of-operation}) is disabled, |
|
60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60185
diff
changeset
|
637 |
fewer facts are |
54114 | 638 |
passed to the prover, \textit{fact\_filter} (\S\ref{relevance-filter}) is set to |
639 |
\textit{mepo}, \textit{strict} (\S\ref{problem-encoding}) is enabled, |
|
640 |
\textit{verbose} (\S\ref{output-format}) and \textit{debug} |
|
60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60185
diff
changeset
|
641 |
(\S\ref{output-format}) are disabled, and \textit{timeout} (\S\ref{timeouts}) is |
54114 | 642 |
superseded by the ``Auto Time Limit'' option in jEdit. Sledgehammer's output is |
643 |
also more concise. |
|
39320 | 644 |
|
68565 | 645 |
|
46242 | 646 |
\subsection{Metis} |
57040 | 647 |
\label{metis} |
46242 | 648 |
|
43216 | 649 |
The \textit{metis} proof method has the syntax |
650 |
||
651 |
\prew |
|
45518 | 652 |
\textbf{\textit{metis}}~(\qty{options})${}^?$~\qty{facts}${}^?$ |
43216 | 653 |
\postw |
654 |
||
45518 | 655 |
where \qty{facts} is a list of arbitrary facts and \qty{options} is a |
656 |
comma-separated list consisting of at most one $\lambda$ translation scheme |
|
657 |
specification with the same semantics as Sledgehammer's \textit{lam\_trans} |
|
658 |
option (\S\ref{problem-encoding}) and at most one type encoding specification |
|
659 |
with the same semantics as Sledgehammer's \textit{type\_enc} option |
|
660 |
(\S\ref{problem-encoding}). |
|
661 |
% |
|
662 |
The supported $\lambda$ translation schemes are \textit{hide\_lams}, |
|
46366 | 663 |
\textit{lifting}, and \textit{combs} (the default). |
45518 | 664 |
% |
665 |
All the untyped type encodings listed in \S\ref{problem-encoding} are supported. |
|
666 |
For convenience, the following aliases are provided: |
|
667 |
\begin{enum} |
|
48393 | 668 |
\item[\labelitemi] \textbf{\textit{full\_types}:} Alias for \textit{poly\_guards\_query}. |
669 |
\item[\labelitemi] \textbf{\textit{partial\_types}:} Alias for \textit{poly\_args}. |
|
670 |
\item[\labelitemi] \textbf{\textit{no\_types}:} Alias for \textit{erased}. |
|
45518 | 671 |
\end{enum} |
43216 | 672 |
|
68565 | 673 |
|
36926 | 674 |
\section{Option Reference} |
675 |
\label{option-reference} |
|
676 |
||
43014 | 677 |
\def\defl{\{} |
678 |
\def\defr{\}} |
|
679 |
||
36926 | 680 |
\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}} |
47036 | 681 |
\def\optrueonly#1{\flushitem{\textit{#1} $\bigl[$= \textit{true}$\bigr]$\enskip}\nopagebreak\\[\parskip]} |
43014 | 682 |
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} |
683 |
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} |
|
684 |
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} |
|
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46366
diff
changeset
|
685 |
\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} |
36926 | 686 |
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]} |
43014 | 687 |
\def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]} |
688 |
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]} |
|
36926 | 689 |
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]} |
690 |
\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} |
|
43014 | 691 |
\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} |
36926 | 692 |
|
693 |
Sledgehammer's options are categorized as follows:\ mode of operation |
|
38984 | 694 |
(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), |
695 |
relevance filter (\S\ref{relevance-filter}), output format |
|
57241 | 696 |
(\S\ref{output-format}), regression testing (\S\ref{regression-testing}), |
697 |
and timeouts (\S\ref{timeouts}). |
|
36926 | 698 |
|
699 |
The descriptions below refer to the following syntactic quantities: |
|
700 |
||
701 |
\begin{enum} |
|
45516 | 702 |
\item[\labelitemi] \qtybf{string}: A string. |
703 |
\item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}. |
|
704 |
\item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or |
|
40203 | 705 |
\textit{smart}. |
45516 | 706 |
\item[\labelitemi] \qtybf{int\/}: An integer. |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54788
diff
changeset
|
707 |
\item[\labelitemi] \qtybf{float}: A floating-point number (e.g., 2.5 or 60) |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54788
diff
changeset
|
708 |
expressing a number of seconds. |
45516 | 709 |
\item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers |
40343
4521d56aef63
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset
|
710 |
(e.g., 0.6 0.95). |
45516 | 711 |
\item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}. |
36926 | 712 |
\end{enum} |
713 |
||
43217 | 714 |
Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options |
61317 | 715 |
have a negative counterpart (e.g., \textit{minimize} vs.\ |
716 |
\textit{dont\_minimize}). When setting Boolean options or their negative |
|
47963 | 717 |
counterparts, ``= \textit{true\/}'' may be omitted. |
36926 | 718 |
|
68565 | 719 |
|
36926 | 720 |
\subsection{Mode of Operation} |
721 |
\label{mode-of-operation} |
|
722 |
||
723 |
\begin{enum} |
|
43014 | 724 |
\opnodefaultbrk{provers}{string} |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
725 |
Specifies the automatic provers to use as a space-separated list (e.g., |
68565 | 726 |
``\textit{cvc4}~\textit{e}~\textit{spass}~\textit{vampire\/}''). |
46299 | 727 |
Provers can be run locally or remotely; see \S\ref{installation} for |
728 |
installation instructions. |
|
729 |
||
730 |
The following local provers are supported: |
|
36926 | 731 |
|
48701 | 732 |
\begin{sloppy} |
36926 | 733 |
\begin{enum} |
55334
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset
|
734 |
\item[\labelitemi] \textbf{\textit{agsyhol}:} AgsyHOL is an automatic |
52078 | 735 |
higher-order prover developed by Fredrik Lindblad \cite{agsyHOL}, |
55334
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset
|
736 |
with support for the TPTP typed higher-order syntax (THF0). To use AgsyHOL, set |
52078 | 737 |
the environment variable \texttt{AGSYHOL\_HOME} to the directory that contains |
738 |
the \texttt{agsyHOL} executable. Sledgehammer has been tested with version 1.0. |
|
739 |
||
46643
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset
|
740 |
\item[\labelitemi] \textbf{\textit{alt\_ergo}:} Alt-Ergo is a polymorphic |
52078 | 741 |
ATP developed by Bobot et al.\ \cite{alt-ergo}. |
46643
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset
|
742 |
It supports the TPTP polymorphic typed first-order format (TFF1) via Why3 |
53102 | 743 |
\cite{why3}. To use Alt-Ergo, set the environment variable \texttt{WHY3\_HOME} |
56379
d8ecce5d51cd
use Alt-Ergo 0.95.2, the latest and greatest version
blanchet
parents:
56378
diff
changeset
|
744 |
to the directory that contains the \texttt{why3} executable. Sledgehammer |
d8ecce5d51cd
use Alt-Ergo 0.95.2, the latest and greatest version
blanchet
parents:
56378
diff
changeset
|
745 |
requires Alt-Ergo 0.95.2 and Why3 0.83. |
46643
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset
|
746 |
|
45516 | 747 |
\item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by |
42945 | 748 |
Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3, |
749 |
set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the |
|
46242 | 750 |
executable, including the file name, or install the prebuilt CVC3 package from |
57241 | 751 |
\download. Sledgehammer has been tested with versions 2.2 and 2.4.1. |
752 |
||
753 |
\item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 \cite{cvc4} is the successor to |
|
754 |
CVC3. To use CVC4, set the environment variable \texttt{CVC4\_SOLVER} to the |
|
755 |
complete path of the executable, including the file name, or install the |
|
756 |
prebuilt CVC4 package from \download. Sledgehammer has been tested with version |
|
59034 | 757 |
1.5-prerelease. |
42945 | 758 |
|
45516 | 759 |
\item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover |
42964
bf45fd2488a2
document primitive support for LEO-II and Satallax
blanchet
parents:
42945
diff
changeset
|
760 |
developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment |
bf45fd2488a2
document primitive support for LEO-II and Satallax
blanchet
parents:
42945
diff
changeset
|
761 |
variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof} |
52757 | 762 |
executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or |
47056 | 763 |
install the prebuilt E package from \download. Sledgehammer has been tested with |
57636
3ab503b04bdb
stick to external proofs when invoking E, because they are more detailed and do not merge steps
blanchet
parents:
57566
diff
changeset
|
764 |
versions 1.6 to 1.8. |
48652 | 765 |
|
766 |
\item[\labelitemi] \textbf{\textit{e\_males}:} E-MaLeS is a metaprover developed |
|
767 |
by Daniel K\"uhlwein that implements strategy scheduling on top of E. To use |
|
768 |
E-MaLeS, set the environment variable \texttt{E\_MALES\_HOME} to the directory |
|
769 |
that contains the \texttt{emales.py} script. Sledgehammer has been tested with |
|
770 |
version 1.1. |
|
36926 | 771 |
|
54694
af9cdb4989c7
added warning to documentation, based on isabelle-users thread
blanchet
parents:
54139
diff
changeset
|
772 |
\item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is an experimental metaprover |
af9cdb4989c7
added warning to documentation, based on isabelle-users thread
blanchet
parents:
54139
diff
changeset
|
773 |
developed by Josef Urban that implements strategy scheduling on top of E. To use |
af9cdb4989c7
added warning to documentation, based on isabelle-users thread
blanchet
parents:
54139
diff
changeset
|
774 |
E-Par, set the environment variable \texttt{E\_HOME} to the directory that |
af9cdb4989c7
added warning to documentation, based on isabelle-users thread
blanchet
parents:
54139
diff
changeset
|
775 |
contains the \texttt{runepar.pl} script and the \texttt{eprover} and |
50929 | 776 |
\texttt{epclextract} executables, or use the prebuilt E package from \download. |
54694
af9cdb4989c7
added warning to documentation, based on isabelle-users thread
blanchet
parents:
54139
diff
changeset
|
777 |
Be aware that E-Par is experimental software. It has been known to generate |
af9cdb4989c7
added warning to documentation, based on isabelle-users thread
blanchet
parents:
54139
diff
changeset
|
778 |
zombie processes. Use at your own risks. |
50929 | 779 |
|
68250
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
67021
diff
changeset
|
780 |
\item[\labelitemi] \textbf{\textit{ehoh}:} Ehoh is an experimental version of |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
67021
diff
changeset
|
781 |
E that supports a $\lambda$-free fragment of higher-order logic. Use at your |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
67021
diff
changeset
|
782 |
own risks. |
c45067867860
added lambda-free HO output for Ehoh (higher-order E prototype)
blanchet
parents:
67021
diff
changeset
|
783 |
|
48701 | 784 |
\item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure |
785 |
instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. |
|
786 |
To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the |
|
48714 | 787 |
directory that contains the \texttt{iprover} and \texttt{vclausify\_rel} |
788 |
executables. Sledgehammer has been tested with version 0.99. |
|
48701 | 789 |
|
790 |
\item[\labelitemi] \textbf{\textit{iprover\_eq}:} iProver-Eq is an |
|
791 |
instantiation-based prover with native support for equality developed by |
|
792 |
Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. To use |
|
793 |
iProver-Eq, set the environment variable \texttt{IPROVER\_EQ\_HOME} to the |
|
48714 | 794 |
directory that contains the \texttt{iprover-eq} and \texttt{vclausify\_rel} |
795 |
executables. Sledgehammer has been tested with version 0.8. |
|
48701 | 796 |
|
45516 | 797 |
\item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic |
44098 | 798 |
higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, |
46242 | 799 |
with support for the TPTP typed higher-order syntax (THF0). To use LEO-II, set |
800 |
the environment variable \texttt{LEO2\_HOME} to the directory that contains the |
|
52757 | 801 |
\texttt{leo} executable. Sledgehammer requires version 1.3.4 or above. |
44098 | 802 |
|
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66735
diff
changeset
|
803 |
\item[\labelitemi] \textbf{\textit{leo3}:} Leo-III is an automatic |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66735
diff
changeset
|
804 |
higher-order prover developed by Alexander Steen, Max Wisniewski, Christoph |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66735
diff
changeset
|
805 |
Benzm\"uller et al.\ \cite{leo3}, |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66735
diff
changeset
|
806 |
with support for the TPTP typed higher-order syntax (THF0). To use Leo-III, set |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66735
diff
changeset
|
807 |
the environment variable \texttt{LEO3\_HOME} to the directory that contains the |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66735
diff
changeset
|
808 |
\texttt{leo3} executable. Sledgehammer requires version 1.1 or above. |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66735
diff
changeset
|
809 |
|
45516 | 810 |
\item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic |
44098 | 811 |
higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with |
46242 | 812 |
support for the TPTP typed higher-order syntax (THF0). To use Satallax, set the |
813 |
environment variable \texttt{SATALLAX\_HOME} to the directory that contains the |
|
814 |
\texttt{satallax} executable. Sledgehammer requires version 2.2 or above. |
|
44098 | 815 |
|
45516 | 816 |
\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution |
42964
bf45fd2488a2
document primitive support for LEO-II and Satallax
blanchet
parents:
42945
diff
changeset
|
817 |
prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}. |
bf45fd2488a2
document primitive support for LEO-II and Satallax
blanchet
parents:
42945
diff
changeset
|
818 |
To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory |
47056 | 819 |
that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the |
47577 | 820 |
version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from |
48006 | 821 |
\download. Sledgehammer requires version 3.8ds or above. |
36926 | 822 |
|
48652 | 823 |
\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order |
824 |
resolution prover developed by Andrei Voronkov and his colleagues |
|
42964
bf45fd2488a2
document primitive support for LEO-II and Satallax
blanchet
parents:
42945
diff
changeset
|
825 |
\cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable |
bf45fd2488a2
document primitive support for LEO-II and Satallax
blanchet
parents:
42945
diff
changeset
|
826 |
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire} |
48006 | 827 |
executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., |
68565 | 828 |
``4.2.2''). Sledgehammer has been tested with versions 1.8 to 4.2.2 (in the |
829 |
post-2010 numbering scheme). |
|
40942 | 830 |
|
59035
3a2153676705
renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names
blanchet
parents:
59034
diff
changeset
|
831 |
\item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is an |
65516 | 832 |
SMT solver developed by David D\'eharbe, Pascal Fontaine, and their colleagues. |
58497
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
833 |
It is specifically designed to produce detailed proofs for reconstruction in |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
834 |
proof assistants. To use veriT, set the environment variable |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
835 |
\texttt{VERIT\_SOLVER} to the complete path of the executable, including the |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
836 |
file name. Sledgehammer has been tested with version smtcomp2014. |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
837 |
|
45516 | 838 |
\item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at |
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset
|
839 |
Microsoft Research \cite{z3}. To use Z3, set the environment variable |
59961 | 840 |
\texttt{Z3\_SOLVER} to the complete path of the executable, including the |
841 |
file name. Sledgehammer has been tested with a pre-release version of 4.4.0. |
|
56378 | 842 |
|
843 |
\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be |
|
844 |
an ATP, exploiting Z3's support for the TPTP untyped and typed first-order |
|
845 |
formats (FOF and TFF0). It is included for experimental purposes. It requires |
|
56725 | 846 |
version 4.3.1 of Z3 or above. To use it, set the environment variable |
56378 | 847 |
\texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp} |
848 |
executable. |
|
58497
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
849 |
|
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
850 |
\item[\labelitemi] \textbf{\textit{zipperposition}:} Zipperposition |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
851 |
\cite{cruanes-2014} is an experimental first-order resolution prover developed |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
852 |
by Simon Cruane. To use Zipperposition, set the environment variable |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
853 |
\texttt{ZIPPERPOSITION\_HOME} to the directory that contains the |
20aaa307c0ff
updated docs with two provers: veriT and Zipperposition
blanchet
parents:
58090
diff
changeset
|
854 |
\texttt{zipperposition} executable. |
57536 | 855 |
\end{enum} |
56378 | 856 |
|
48701 | 857 |
\end{sloppy} |
42945 | 858 |
|
57536 | 859 |
Moreover, the following remote provers are supported: |
42945 | 860 |
|
861 |
\begin{enum} |
|
52078 | 862 |
\item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of |
55334
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset
|
863 |
AgsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. |
52078 | 864 |
|
45516 | 865 |
\item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs |
36926 | 866 |
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. |
867 |
||
45516 | 868 |
\item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover |
47075 | 869 |
developed by Kry\v stof Hoder \cite{sine} based on E. It runs on Geoff |
870 |
Sutcliffe's Miami servers. |
|
44091 | 871 |
|
45516 | 872 |
\item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover |
44091 | 873 |
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami |
45516 | 874 |
servers. This ATP supports the TPTP typed first-order format (TFF0). The |
44091 | 875 |
remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers. |
876 |
||
48701 | 877 |
\item[\labelitemi] \textbf{\textit{remote\_iprover}:} The |
45339 | 878 |
remote version of iProver runs on Geoff Sutcliffe's Miami servers |
879 |
\cite{sutcliffe-2000}. |
|
880 |
||
48701 | 881 |
\item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} The |
45339 | 882 |
remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers |
883 |
\cite{sutcliffe-2000}. |
|
884 |
||
45516 | 885 |
\item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II |
44098 | 886 |
runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. |
42964
bf45fd2488a2
document primitive support for LEO-II and Satallax
blanchet
parents:
42945
diff
changeset
|
887 |
|
67021
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66735
diff
changeset
|
888 |
\item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66735
diff
changeset
|
889 |
runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. |
41f1f8c4259b
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
blanchet
parents:
66735
diff
changeset
|
890 |
|
59577 | 891 |
\item[\labelitemi] \textbf{\textit{remote\_pirate}:} Pirate is a |
892 |
highly experimental first-order resolution prover developed by Daniel Wand. |
|
893 |
The remote version of Pirate run on a private server he generously set up. |
|
894 |
||
45516 | 895 |
\item[\labelitemi] \textbf{\textit{remote\_satallax}:} The remote version of |
44098 | 896 |
Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. |
42964
bf45fd2488a2
document primitive support for LEO-II and Satallax
blanchet
parents:
42945
diff
changeset
|
897 |
|
45516 | 898 |
\item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a first-order |
43625 | 899 |
resolution prover developed by Stickel et al.\ \cite{snark}. It supports the |
45516 | 900 |
TPTP typed first-order format (TFF0). The remote version of SNARK runs on |
43625 | 901 |
Geoff Sutcliffe's Miami servers. |
40073 | 902 |
|
45516 | 903 |
\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of |
48006 | 904 |
Vampire runs on Geoff Sutcliffe's Miami servers. |
42945 | 905 |
|
45516 | 906 |
\item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit |
42945 | 907 |
equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be |
43625 | 908 |
used to prove universally quantified equations using unconditional equations, |
909 |
corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister |
|
910 |
runs on Geoff Sutcliffe's Miami servers. |
|
36926 | 911 |
\end{enum} |
912 |
||
59510 | 913 |
By default, Sledgehammer runs a subset of CVC4, E, E-SInE, SPASS, Vampire, |
59577 | 914 |
veriT, and Z3 in parallel, either locally or remotely---depending on the number |
915 |
of processor cores available and on which provers are actually installed. It is |
|
916 |
generally a good idea to run several provers in parallel. |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
917 |
|
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
918 |
\opnodefault{prover}{string} |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
919 |
Alias for \textit{provers}. |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset
|
920 |
|
45708
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset
|
921 |
\optrue{slice}{dont\_slice} |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset
|
922 |
Specifies whether the time allocated to a prover should be sliced into several |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset
|
923 |
segments, each of which has its own set of possibly prover-dependent options. |
42446 | 924 |
For SPASS and Vampire, the first slice tries the fast but incomplete |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset
|
925 |
set-of-support (SOS) strategy, whereas the second slice runs without it. For E, |
42446 | 926 |
up to three slices are tried, with different weighted search strategies and |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset
|
927 |
number of facts. For SMT solvers, several slices are tried with the same options |
42446 | 928 |
each time but fewer and fewer facts. According to benchmarks with a timeout of |
929 |
30 seconds, slicing is a valuable optimization, and you should probably leave it |
|
54114 | 930 |
enabled unless you are conducting experiments. |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset
|
931 |
|
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset
|
932 |
\nopagebreak |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset
|
933 |
{\small See also \textit{verbose} (\S\ref{output-format}).} |
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset
|
934 |
|
57722 | 935 |
\optrue{minimize}{dont\_minimize} |
45708
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset
|
936 |
Specifies whether the minimization tool should be invoked automatically after |
57722 | 937 |
proof search. |
45708
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset
|
938 |
|
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset
|
939 |
\nopagebreak |
47036 | 940 |
{\small See also \textit{preplay\_timeout} (\S\ref{timeouts}) |
941 |
and \textit{dont\_preplay} (\S\ref{timeouts}).} |
|
45708
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset
|
942 |
|
53801 | 943 |
\opfalse{spy}{dont\_spy} |
944 |
Specifies whether Sledgehammer should record statistics in |
|
945 |
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak spy\_\allowbreak sledgehammer}. |
|
946 |
These statistics can be useful to the developers of Sledgehammer. If you are willing to have your |
|
947 |
interactions recorded in the name of science, please enable this feature and send the statistics |
|
948 |
file every now and then to the author of this manual (\authoremail). |
|
949 |
To change the default value of this option globally, set the environment variable |
|
57107
2d502370ee99
changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)
blanchet
parents:
57095
diff
changeset
|
950 |
\texttt{SLEDGEHAMMER\_SPY} to \textit{yes}. |
53801 | 951 |
|
952 |
\nopagebreak |
|
953 |
{\small See also \textit{debug} (\S\ref{output-format}).} |
|
954 |
||
36926 | 955 |
\opfalse{overlord}{no\_overlord} |
956 |
Specifies whether Sledgehammer should put its temporary files in |
|
957 |
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for |
|
958 |
debugging Sledgehammer but also unsafe if several instances of the tool are run |
|
48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48388
diff
changeset
|
959 |
simultaneously. The files are identified by the prefixes \texttt{prob\_} and |
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48388
diff
changeset
|
960 |
\texttt{mash\_}; you may safely remove them after Sledgehammer has run. |
36926 | 961 |
|
54139 | 962 |
\textbf{Warning:} This option is not thread-safe. Use at your own risks. |
963 |
||
36926 | 964 |
\nopagebreak |
965 |
{\small See also \textit{debug} (\S\ref{output-format}).} |
|
966 |
\end{enum} |
|
967 |
||
68565 | 968 |
|
48387 | 969 |
\subsection{Relevance Filter} |
970 |
\label{relevance-filter} |
|
971 |
||
972 |
\begin{enum} |
|
48388 | 973 |
\opdefault{fact\_filter}{string}{smart} |
974 |
Specifies the relevance filter to use. The following filters are available: |
|
975 |
||
976 |
\begin{enum} |
|
977 |
\item[\labelitemi] \textbf{\textit{mepo}:} |
|
978 |
The traditional memoryless MePo relevance filter. |
|
979 |
||
980 |
\item[\labelitemi] \textbf{\textit{mash}:} |
|
57532 | 981 |
The MaSh machine learner. Three learning algorithms are provided: |
57019 | 982 |
|
983 |
\begin{enum} |
|
57463 | 984 |
\item[\labelitemi] \textbf{\textit{nb}} is an implementation of naive Bayes. |
57019 | 985 |
|
57463 | 986 |
\item[\labelitemi] \textbf{\textit{knn}} is an implementation of $k$-nearest |
987 |
neighbors. |
|
988 |
||
57659
b246943b3aa3
reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents:
57636
diff
changeset
|
989 |
\item[\labelitemi] \textbf{\textit{nb\_knn}} (also called \textbf{\textit{yes}} |
b246943b3aa3
reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents:
57636
diff
changeset
|
990 |
and \textbf{\textit{sml}}) is a combination of naive Bayes and $k$-nearest |
b246943b3aa3
reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents:
57636
diff
changeset
|
991 |
neighbors. |
57019 | 992 |
\end{enum} |
993 |
||
57272
fd539459a112
enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
blanchet
parents:
57245
diff
changeset
|
994 |
In addition, the special value \textit{none} is used to disable machine learning by |
fd539459a112
enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
blanchet
parents:
57245
diff
changeset
|
995 |
default (cf.\ \textit{smart} below). |
fd539459a112
enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
blanchet
parents:
57245
diff
changeset
|
996 |
|
57659
b246943b3aa3
reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents:
57636
diff
changeset
|
997 |
The default algorithm is \textit{nb\_knn}. The algorithm can be selected by |
61043 | 998 |
setting the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle > |
57532 | 999 |
General'' in Isabelle/jEdit. Persistent data for both algorithms is stored in |
1000 |
the directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak |
|
1001 |
mash}. |
|
48388 | 1002 |
|
51024
98fb341d32e3
distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
blanchet
parents:
50929
diff
changeset
|
1003 |
\item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the |
98fb341d32e3
distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
blanchet
parents:
50929
diff
changeset
|
1004 |
rankings from MePo and MaSh. |
48388 | 1005 |
|
57659
b246943b3aa3
reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents:
57636
diff
changeset
|
1006 |
\item[\labelitemi] \textbf{\textit{smart}:} A combination of MePo, MaSh, and |
b246943b3aa3
reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents:
57636
diff
changeset
|
1007 |
MeSh. If the learning algorithm is set to be \textit{none}, \textit{smart} |
b246943b3aa3
reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents:
57636
diff
changeset
|
1008 |
behaves like MePo. |
48388 | 1009 |
\end{enum} |
1010 |
||
48387 | 1011 |
\opdefault{max\_facts}{smart\_int}{smart} |
1012 |
Specifies the maximum number of facts that may be returned by the relevance |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1013 |
filter. If the option is set to \textit{smart} (the default), it effectively |
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1014 |
takes a value that was empirically found to be appropriate for the prover. |
57107
2d502370ee99
changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)
blanchet
parents:
57095
diff
changeset
|
1015 |
Typical values lie between 50 and 1000. |
53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53518
diff
changeset
|
1016 |
|
48387 | 1017 |
\opdefault{fact\_thresholds}{float\_pair}{\upshape 0.45~0.85} |
1018 |
Specifies the thresholds above which facts are considered relevant by the |
|
1019 |
relevance filter. The first threshold is used for the first iteration of the |
|
1020 |
relevance filter and the second threshold is used for the last iteration (if it |
|
1021 |
is reached). The effective threshold is quadratically interpolated for the other |
|
1022 |
iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems |
|
1023 |
are relevant and 1 only theorems that refer to previously seen constants. |
|
1024 |
||
48388 | 1025 |
\optrue{learn}{dont\_learn} |
1026 |
Specifies whether MaSh should be run automatically by Sledgehammer to learn the |
|
53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset
|
1027 |
available theories (and hence provide more accurate results). Learning takes |
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset
|
1028 |
place only if MaSh is enabled. |
48388 | 1029 |
|
48387 | 1030 |
\opdefault{max\_new\_mono\_instances}{int}{smart} |
1031 |
Specifies the maximum number of monomorphic instances to generate beyond |
|
1032 |
\textit{max\_facts}. The higher this limit is, the more monomorphic instances |
|
1033 |
are potentially generated. Whether monomorphization takes place depends on the |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1034 |
type encoding used. If the option is set to \textit{smart} (the default), it |
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1035 |
takes a value that was empirically found to be appropriate for the prover. For |
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1036 |
most provers, this value is 100. |
48387 | 1037 |
|
1038 |
\nopagebreak |
|
1039 |
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).} |
|
1040 |
||
1041 |
\opdefault{max\_mono\_iters}{int}{smart} |
|
1042 |
Specifies the maximum number of iterations for the monomorphization fixpoint |
|
1043 |
construction. The higher this limit is, the more monomorphic instances are |
|
1044 |
potentially generated. Whether monomorphization takes place depends on the |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1045 |
type encoding used. If the option is set to \textit{smart} (the default), it |
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1046 |
takes a value that was empirically found to be appropriate for the prover. |
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1047 |
For most provers, this value is 3. |
48387 | 1048 |
|
1049 |
\nopagebreak |
|
1050 |
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).} |
|
1051 |
\end{enum} |
|
1052 |
||
68565 | 1053 |
|
36926 | 1054 |
\subsection{Problem Encoding} |
1055 |
\label{problem-encoding} |
|
1056 |
||
45516 | 1057 |
\newcommand\comb[1]{\const{#1}} |
1058 |
||
36926 | 1059 |
\begin{enum} |
45516 | 1060 |
\opdefault{lam\_trans}{string}{smart} |
1061 |
Specifies the $\lambda$ translation scheme to use in ATP problems. The supported |
|
1062 |
translation schemes are listed below: |
|
1063 |
||
1064 |
\begin{enum} |
|
1065 |
\item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$-abstractions |
|
1066 |
by replacing them by unspecified fresh constants, effectively disabling all |
|
1067 |
reasoning under $\lambda$-abstractions. |
|
1068 |
||
46366 | 1069 |
\item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new |
45516 | 1070 |
supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions, |
1071 |
defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting). |
|
1072 |
||
46366 | 1073 |
\item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry |
45516 | 1074 |
combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators |
1075 |
enable the ATPs to synthesize $\lambda$-terms but tend to yield bulkier formulas |
|
1076 |
than $\lambda$-lifting: The translation is quadratic in the worst case, and the |
|
1077 |
equational definitions of the combinators are very prolific in the context of |
|
1078 |
resolution. |
|
1079 |
||
46366 | 1080 |
\item[\labelitemi] \textbf{\textit{combs\_and\_lifting}:} Introduce a new |
45516 | 1081 |
supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a |
1082 |
lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators. |
|
1083 |
||
46366 | 1084 |
\item[\labelitemi] \textbf{\textit{combs\_or\_lifting}:} For each cluster of |
1085 |
$\lambda$-abstractions, heuristically choose between $\lambda$-lifting and Curry |
|
1086 |
combinators. |
|
1087 |
||
45516 | 1088 |
\item[\labelitemi] \textbf{\textit{keep\_lams}:} |
1089 |
Keep the $\lambda$-abstractions in the generated problems. This is available |
|
1090 |
only with provers that support the THF0 syntax. |
|
1091 |
||
1092 |
\item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used |
|
1093 |
depends on the ATP and should be the most efficient scheme for that ATP. |
|
1094 |
\end{enum} |
|
1095 |
||
46366 | 1096 |
For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting}, |
1097 |
irrespective of the value of this option. |
|
45516 | 1098 |
|
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46366
diff
changeset
|
1099 |
\opsmartx{uncurried\_aliases}{no\_uncurried\_aliases} |
46411 | 1100 |
Specifies whether fresh function symbols should be generated as aliases for |
1101 |
applications of curried functions in ATP problems. |
|
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46366
diff
changeset
|
1102 |
|
43627
ecd4bb7a8bc0
update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
blanchet
parents:
43625
diff
changeset
|
1103 |
\opdefault{type\_enc}{string}{smart} |
ecd4bb7a8bc0
update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
blanchet
parents:
43625
diff
changeset
|
1104 |
Specifies the type encoding to use in ATP problems. Some of the type encodings |
ecd4bb7a8bc0
update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
blanchet
parents:
43625
diff
changeset
|
1105 |
are unsound, meaning that they can give rise to spurious proofs |
48093 | 1106 |
(unreconstructible using \textit{metis}). The type encodings are |
46300 | 1107 |
listed below, with an indication of their soundness in parentheses. |
48093 | 1108 |
An asterisk (*) indicates that the encoding is slightly incomplete for |
56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset
|
1109 |
reconstruction with \textit{metis}, unless the \textit{strict} option (described |
46302 | 1110 |
below) is enabled. |
42228 | 1111 |
|
1112 |
\begin{enum} |
|
48090 | 1113 |
\item[\labelitemi] \textbf{\textit{erased} (unsound):} No type information is |
46300 | 1114 |
supplied to the ATP, not even to resolve overloading. Types are simply erased. |
42582 | 1115 |
|
45516 | 1116 |
\item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using |
46300 | 1117 |
a predicate \const{g}$(\tau, t)$ that guards bound |
48090 | 1118 |
variables. Constants are annotated with their types, supplied as extra |
42887
771be1dcfef6
document new type system and soundness properties of the different systems
blanchet
parents:
42884
diff
changeset
|
1119 |
arguments, to resolve overloading. |
42685 | 1120 |
|
45516 | 1121 |
\item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is |
46300 | 1122 |
tagged with its type using a function $\const{t\/}(\tau, t)$. |
42887
771be1dcfef6
document new type system and soundness properties of the different systems
blanchet
parents:
42884
diff
changeset
|
1123 |
|
45516 | 1124 |
\item[\labelitemi] \textbf{\textit{poly\_args} (unsound):} |
43990 | 1125 |
Like for \textit{poly\_guards} constants are annotated with their types to |
43002
e88fde86e4c2
mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents:
42996
diff
changeset
|
1126 |
resolve overloading, but otherwise no type information is encoded. This |
57040 | 1127 |
is the default encoding used by the \textit{metis} proof method. |
42685 | 1128 |
|
45516 | 1129 |
\item[\labelitemi] |
42722 | 1130 |
\textbf{% |
44494
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset
|
1131 |
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\ |
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset
|
1132 |
\textit{raw\_mono\_args} (unsound):} \\ |
43990 | 1133 |
Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args}, |
42722 | 1134 |
respectively, but the problem is additionally monomorphized, meaning that type |
1135 |
variables are instantiated with heuristically chosen ground types. |
|
1136 |
Monomorphization can simplify reasoning but also leads to larger fact bases, |
|
1137 |
which can slow down the ATPs. |
|
42582 | 1138 |
|
45516 | 1139 |
\item[\labelitemi] |
42722 | 1140 |
\textbf{% |
44494
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset
|
1141 |
\textit{mono\_guards}, \textit{mono\_tags} (sound); |
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset
|
1142 |
\textit{mono\_args} (unsound):} \\ |
42722 | 1143 |
Similar to |
44494
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset
|
1144 |
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and |
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset
|
1145 |
\textit{raw\_mono\_args}, respectively but types are mangled in constant names |
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset
|
1146 |
instead of being supplied as ground term arguments. The binary predicate |
46300 | 1147 |
$\const{g}(\tau, t)$ becomes a unary predicate |
1148 |
$\const{g\_}\tau(t)$, and the binary function |
|
1149 |
$\const{t}(\tau, t)$ becomes a unary function |
|
1150 |
$\const{t\_}\tau(t)$. |
|
42589
9f7c48463645
restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42582
diff
changeset
|
1151 |
|
46435 | 1152 |
\item[\labelitemi] \textbf{\textit{mono\_native} (sound):} Exploits native |
46643
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset
|
1153 |
first-order types if the prover supports the TFF0, TFF1, or THF0 syntax; |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset
|
1154 |
otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized. |
43625 | 1155 |
|
46435 | 1156 |
\item[\labelitemi] \textbf{\textit{mono\_native\_higher} (sound):} Exploits |
1157 |
native higher-order types if the prover supports the THF0 syntax; otherwise, |
|
1158 |
falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is |
|
1159 |
monomorphized. |
|
42681 | 1160 |
|
46643
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset
|
1161 |
\item[\labelitemi] \textbf{\textit{poly\_native} (sound):} Exploits native |
48078 | 1162 |
first-order polymorphic types if the prover supports the TFF1 syntax; otherwise, |
46643
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset
|
1163 |
falls back on \textit{mono\_native}. |
a88bccd2b567
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset
|
1164 |
|
45516 | 1165 |
\item[\labelitemi] |
42681 | 1166 |
\textbf{% |
44494
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset
|
1167 |
\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\ |
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset
|
1168 |
\textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\ |
46435 | 1169 |
\textit{mono\_native}? (sound*):} \\ |
43990 | 1170 |
The type encodings \textit{poly\_guards}, \textit{poly\_tags}, |
44494
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset
|
1171 |
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards}, |
47036 | 1172 |
\textit{mono\_tags}, and \textit{mono\_native} are fully typed and sound. For |
1173 |
each of these, Sledgehammer also provides a lighter variant identified by a |
|
1174 |
question mark (`\hbox{?}')\ that detects and erases monotonic types, notably |
|
1175 |
infinite types. (For \textit{mono\_native}, the types are not actually erased |
|
1176 |
but rather replaced by a shared uniform type of individuals.) As argument to the |
|
1177 |
\textit{metis} proof method, the question mark is replaced by a |
|
1178 |
\hbox{``\textit{\_query\/}''} suffix. |
|
42582 | 1179 |
|
45516 | 1180 |
\item[\labelitemi] |
42887
771be1dcfef6
document new type system and soundness properties of the different systems
blanchet
parents:
42884
diff
changeset
|
1181 |
\textbf{% |
44769 | 1182 |
\textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\ |
1183 |
\textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\ |
|
46300 | 1184 |
(sound*):} \\ |
44816 | 1185 |
Even lighter versions of the `\hbox{?}' encodings. As argument to the |
1186 |
\textit{metis} proof method, the `\hbox{??}' suffix is replaced by |
|
46242 | 1187 |
\hbox{``\textit{\_query\_query\/}''}. |
44816 | 1188 |
|
45516 | 1189 |
\item[\labelitemi] |
44816 | 1190 |
\textbf{% |
48184 | 1191 |
\textit{poly\_guards}@, \textit{poly\_tags}@, \textit{raw\_mono\_guards}@, \\ |
1192 |
\textit{raw\_mono\_tags}@ (sound*):} \\ |
|
44816 | 1193 |
Alternative versions of the `\hbox{??}' encodings. As argument to the |
48184 | 1194 |
\textit{metis} proof method, the `\hbox{@}' suffix is replaced by |
1195 |
\hbox{``\textit{\_at\/}''}. |
|
44769 | 1196 |
|
48093 | 1197 |
\item[\labelitemi] \textbf{\textit{poly\_args}?, \textit{raw\_mono\_args}? (unsound):} \\ |
1198 |
Lighter versions of \textit{poly\_args} and \textit{raw\_mono\_args}. |
|
1199 |
||
45516 | 1200 |
\item[\labelitemi] \textbf{\textit{smart}:} The actual encoding used depends on |
47036 | 1201 |
the ATP and should be the most efficient sound encoding for that ATP. |
42228 | 1202 |
\end{enum} |
1203 |
||
46435 | 1204 |
For SMT solvers, the type encoding is always \textit{mono\_native}, irrespective |
44743 | 1205 |
of the value of this option. |
42888 | 1206 |
|
1207 |
\nopagebreak |
|
1208 |
{\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter}) |
|
1209 |
and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).} |
|
43574 | 1210 |
|
46302 | 1211 |
\opfalse{strict}{non\_strict} |
46300 | 1212 |
Specifies whether Sledgehammer should run in its strict mode. In that mode, |
46302 | 1213 |
sound type encodings marked with an asterisk (*) above are made complete |
46300 | 1214 |
for reconstruction with \textit{metis}, at the cost of some clutter in the |
1215 |
generated problems. This option has no effect if \textit{type\_enc} is |
|
1216 |
deliberately set to an unsound encoding. |
|
38591 | 1217 |
\end{enum} |
36926 | 1218 |
|
68565 | 1219 |
|
36926 | 1220 |
\subsection{Output Format} |
1221 |
\label{output-format} |
|
1222 |
||
1223 |
\begin{enum} |
|
1224 |
||
1225 |
\opfalse{verbose}{quiet} |
|
1226 |
Specifies whether the \textbf{sledgehammer} command should explain what it does. |
|
1227 |
||
1228 |
\opfalse{debug}{no\_debug} |
|
40203 | 1229 |
Specifies whether Sledgehammer should display additional debugging information |
1230 |
beyond what \textit{verbose} already displays. Enabling \textit{debug} also |
|
61317 | 1231 |
enables \textit{verbose} behind the scenes. |
36926 | 1232 |
|
1233 |
\nopagebreak |
|
53801 | 1234 |
{\small See also \textit{spy} (\S\ref{mode-of-operation}) and |
1235 |
\textit{overlord} (\S\ref{mode-of-operation}).} |
|
36926 | 1236 |
|
51190
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51189
diff
changeset
|
1237 |
\opsmart{isar\_proofs}{no\_isar\_proofs} |
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1238 |
Specifies whether Isar proofs should be output in addition to one-line proofs. |
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1239 |
The construction of Isar proof is still experimental and may sometimes fail; |
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1240 |
however, when they succeed they are usually faster and more intelligible than |
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1241 |
one-line proofs. If the option is set to \textit{smart} (the default), Isar |
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1242 |
proofs are only generated when no working one-line proof is available. |
36926 | 1243 |
|
57784 | 1244 |
\opdefault{compress}{int}{smart} |
49919 | 1245 |
Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs} |
51190
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51189
diff
changeset
|
1246 |
is explicitly enabled. A value of $n$ indicates that each Isar proof step should |
57784 | 1247 |
correspond to a group of up to $n$ consecutive proof steps in the ATP proof. If |
1248 |
the option is set to \textit{smart} (the default), the compression factor is 10 |
|
1249 |
if the \textit{isar\_proofs} option is explicitly enabled; otherwise, it is |
|
1250 |
$\infty$. |
|
51189 | 1251 |
|
57245 | 1252 |
\optrueonly{dont\_compress} |
57784 | 1253 |
Alias for ``\textit{compress} = 1''. |
51189 | 1254 |
|
57245 | 1255 |
\optrue{try0}{dont\_try0} |
53765 | 1256 |
Specifies whether standard proof methods such as \textit{auto} and |
55289 | 1257 |
\textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs. |
1258 |
The collection of methods is roughly the same as for the \textbf{try0} command. |
|
1259 |
||
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1260 |
\opsmart{smt\_proofs}{no\_smt\_proofs} |
61283 | 1261 |
Specifies whether the \textit{smt} proof method should be tried in addition to |
57733 | 1262 |
Isabelle's other proof methods. If the option is set to \textit{smart} (the |
61283 | 1263 |
default), the \textit{smt} method is used for one-line proofs but not in Isar |
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1264 |
proofs. |
36926 | 1265 |
\end{enum} |
1266 |
||
68565 | 1267 |
|
57241 | 1268 |
\subsection{Regression Testing} |
1269 |
\label{regression-testing} |
|
38984 | 1270 |
|
1271 |
\begin{enum} |
|
1272 |
\opnodefault{expect}{string} |
|
1273 |
Specifies the expected outcome, which must be one of the following: |
|
36926 | 1274 |
|
1275 |
\begin{enum} |
|
46300 | 1276 |
\item[\labelitemi] \textbf{\textit{some}:} Sledgehammer found a proof. |
45516 | 1277 |
\item[\labelitemi] \textbf{\textit{none}:} Sledgehammer found no proof. |
1278 |
\item[\labelitemi] \textbf{\textit{timeout}:} Sledgehammer timed out. |
|
1279 |
\item[\labelitemi] \textbf{\textit{unknown}:} Sledgehammer encountered some |
|
40203 | 1280 |
problem. |
38984 | 1281 |
\end{enum} |
1282 |
||
61317 | 1283 |
Sledgehammer emits an error if the actual outcome differs from the expected outcome. This option is |
1284 |
useful for regression testing. |
|
38984 | 1285 |
|
1286 |
\nopagebreak |
|
61317 | 1287 |
{\small See also \textit{timeout} (\S\ref{timeouts}).} |
43038 | 1288 |
\end{enum} |
1289 |
||
68565 | 1290 |
|
43038 | 1291 |
\subsection{Timeouts} |
1292 |
\label{timeouts} |
|
1293 |
||
1294 |
\begin{enum} |
|
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54788
diff
changeset
|
1295 |
\opdefault{timeout}{float}{\upshape 30} |
43038 | 1296 |
Specifies the maximum number of seconds that the automatic provers should spend |
1297 |
searching for a proof. This excludes problem preparation and is a soft limit. |
|
1298 |
||
57719 | 1299 |
\opdefault{preplay\_timeout}{float}{\upshape 1} |
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1300 |
Specifies the maximum number of seconds that \textit{metis} or other proof |
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1301 |
methods should spend trying to ``preplay'' the found proof. If this option |
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1302 |
is set to 0, no preplaying takes place, and no timing information is displayed |
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset
|
1303 |
next to the suggested proof method calls. |
45708
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset
|
1304 |
|
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset
|
1305 |
\nopagebreak |
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset
|
1306 |
{\small See also \textit{minimize} (\S\ref{mode-of-operation}).} |
47036 | 1307 |
|
1308 |
\optrueonly{dont\_preplay} |
|
1309 |
Alias for ``\textit{preplay\_timeout} = 0''. |
|
1310 |
||
36926 | 1311 |
\end{enum} |
1312 |
||
1313 |
\let\em=\sl |
|
48962
a1acc1cb0271
more standard document preparation within session context;
wenzelm
parents:
48803
diff
changeset
|
1314 |
\bibliography{manual}{} |
36926 | 1315 |
\bibliographystyle{abbrv} |
1316 |
||
1317 |
\end{document} |