author  blanchet 
Thu, 28 Aug 2014 20:06:59 +0200  
changeset 58090  f8ddde112e54 
parent 57784  913b5dd101cb 
child 58497  20aaa307c0ff 
permissions  rwrr 
36926  1 
\documentclass[a4paper,12pt]{article} 
2 
\usepackage[T1]{fontenc} 

3 
\usepackage{amsmath} 

4 
\usepackage{amssymb} 

53091  5 
\usepackage[english]{babel} 
36926  6 
\usepackage{color} 
7 
\usepackage{footmisc} 

8 
\usepackage{graphicx} 

9 
%\usepackage{mathpazo} 

10 
\usepackage{multicol} 

11 
\usepackage{stmaryrd} 

12 
%\usepackage[scaled=.85]{beramono} 

48962
a1acc1cb0271
more standard document preparation within session context;
wenzelm
parents:
48803
diff
changeset

13 
\usepackage{isabelle,iman,pdfsetup} 
36926  14 

50929  15 
\newcommand\download{\url{http://isabelle.in.tum.de/components/}} 
46242  16 

57040  17 
\let\oldS=\S 
18 
\def\S{\oldS\,} 

19 

43216  20 
\def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}} 
21 
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$} 

22 

45516  23 
\newcommand\const[1]{\textsf{#1}} 
24 

36926  25 
%\oddsidemargin=4.6mm 
26 
%\evensidemargin=4.6mm 

27 
%\textwidth=150mm 

28 
%\topmargin=4.6mm 

29 
%\headheight=0mm 

30 
%\headsep=0mm 

31 
%\textheight=234mm 

32 

33 
\def\Colon{\mathord{:\mkern1.5mu:}} 

34 
%\def\lbrakk{\mathopen{\lbrack\mkern3.25mu\lbrack}} 

35 
%\def\rbrakk{\mathclose{\rbrack\mkern3.255mu\rbrack}} 

36 
\def\lparr{\mathopen{(\mkern4mu\mid}} 

37 
\def\rparr{\mathclose{\mid\mkern4mu)}} 

38 

39 
\def\unk{{?}} 

40 
\def\undef{(\lambda x.\; \unk)} 

41 
%\def\unr{\textit{others}} 

42 
\def\unr{\ldots} 

43 
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}} 

44 
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}} 

45 

46 
\urlstyle{tt} 

47 

55290  48 
\renewcommand\_{\hbox{\textunderscore\kern.05ex}} 
49 

36926  50 
\begin{document} 
51 

45516  52 
%%% TYPESETTING 
53 
%\renewcommand\labelitemi{$\bullet$} 

54 
\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}} 

55 

36926  56 
\title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex] 
57 
Hammering Away \\[\smallskipamount] 

58 
\Large A User's Guide to Sledgehammer for Isabelle/HOL} 

59 
\author{\hbox{} \\ 

60 
Jasmin Christian Blanchette \\ 

43002
e88fde86e4c2
mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents:
42996
diff
changeset

61 
{\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

62 
{\normalsize with contributions from} \\[4\smallskipamount] 
e88fde86e4c2
mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents:
42996
diff
changeset

63 
Lawrence C. Paulson \\ 
e88fde86e4c2
mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents:
42996
diff
changeset

64 
{\normalsize Computer Laboratory, University of Cambridge} \\ 
36926  65 
\hbox{}} 
66 

67 
\maketitle 

68 

69 
\tableofcontents 

70 

71 
\setlength{\parskip}{.7em plus .2em minus .1em} 

72 
\setlength{\parindent}{0pt} 

73 
\setlength{\abovedisplayskip}{\parskip} 

74 
\setlength{\abovedisplayshortskip}{.9\parskip} 

75 
\setlength{\belowdisplayskip}{\parskip} 

76 
\setlength{\belowdisplayshortskip}{.9\parskip} 

77 

52078  78 
% generalpurpose enum environment with correct spacing 
36926  79 
\newenvironment{enum}% 
80 
{\begin{list}{}{% 

81 
\setlength{\topsep}{.1\parskip}% 

82 
\setlength{\partopsep}{.1\parskip}% 

83 
\setlength{\itemsep}{\parskip}% 

84 
\advance\itemsep by\parsep}} 

85 
{\end{list}} 

86 

87 
\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin 

88 
\advance\rightskip by\leftmargin} 

89 
\def\post{\vskip0pt plus1ex\endgroup} 

90 

91 
\def\prew{\pre\advance\rightskip by\leftmargin} 

92 
\def\postw{\post} 

93 

94 
\section{Introduction} 

95 
\label{introduction} 

96 

42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

97 
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

98 
and satisfiabilitymodulotheories (SMT) solvers on the current goal.% 
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

99 
\footnote{The distinction between ATPs and SMT solvers is convenient but mostly 
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

100 
historical. The two communities are converging, with more and more ATPs 
47672  101 
supporting typical SMT features such as arithmetic and sorts, and a few SMT 
47561
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

102 
solvers parsing ATP syntaxes. There is also a strong technological connection 
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

103 
between instantiationbased ATPs (such as iProver and iProverEq) and SMT 
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

104 
solvers.} 
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

105 
% 
55334
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset

106 
The supported ATPs are AgsyHOL \cite{agsyHOL}, AltErgo \cite{altergo}, E 
52078  107 
\cite{schulz2002}, ESInE \cite{sine}, EToFoF \cite{tofof}, iProver 
108 
\cite{korovin2009}, iProverEq \cite{korovinsticksel2010}, LEOII 

109 
\cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS 

110 
\cite{weidenbachetal2009}, Vampire \cite{riazanovvoronkov2002}, and 

111 
Waldmeister \cite{waldmeister}. The ATPs are run either locally or remotely via 

57241  112 
the System\On\TPTP web service \cite{sutcliffe2000}. The supported SMT 
113 
solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, and Z3 \cite{z3}. These are 

114 
always run locally. 

36926  115 

57241  116 
The problem passed to the external provers (or solvers) consists of your current 
117 
goal together with a heuristic selection of hundreds of facts (theorems) from the 

52078  118 
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

119 

40073  120 
The result of a successful proof search is some source text that usually (but 
121 
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

122 
proof typically relies on the generalpurpose \textit{metis} proof method, which 
45380  123 
integrates the Metis ATP in Isabelle/HOL with explicit inferences going through 
124 
the kernel. Thus its results are correct by construction. 

36926  125 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

126 
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

127 
enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options > 
54114  128 
Isabelle > General.'' In this mode, a reduced version of Sledgehammer is run on 
129 
every newly entered theorem for a few seconds. 

39320  130 

36926  131 
\newbox\boxA 
46298  132 
\setbox\boxA=\hbox{\texttt{NOSPAM}} 
36926  133 

46298  134 
\newcommand\authoremail{\texttt{blan{\color{white}NOSPAM}\kern\wd\boxA{}chette@\allowbreak 
42763  135 
in.\allowbreak tum.\allowbreak de}} 
136 

40689  137 
To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is 
138 
importedthis is rarely a problem in practice since it is part of 

139 
\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's 

36926  140 
\texttt{src/HOL/Metis\_Examples} directory. 
141 
Comments and bug reports concerning Sledgehammer or this manual should be 

42883  142 
directed to the author at \authoremail. 
36926  143 

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

144 
%\vskip2.5\smallskipamount 
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

145 
% 
36926  146 
%\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for 
147 
%suggesting several textual improvements. 

148 

149 
\section{Installation} 

150 
\label{installation} 

151 

48387  152 
Sledgehammer is part of Isabelle, so you do not need to install it. However, it 
46242  153 
relies on thirdparty automatic provers (ATPs and SMT solvers). 
42763  154 

55334
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset

155 
Among the ATPs, AgsyHOL, AltErgo, E, LEOII, Satallax, SPASS, and Vampire can 
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset

156 
be run locally; in addition, AgsyHOL, E, ESInE, EToFoF, iProver, iProverEq, 
52078  157 
LEOII, Satallax, SNARK, Vampire, and Waldmeister are available remotely via 
158 
System\On\TPTP \cite{sutcliffe2000}. If you want better performance, you 

57241  159 
should at least install E and SPASS locally. The SMT solvers CVC3, CVC4, and Z3 
160 
can be run locally. 

36926  161 

46242  162 
There are three main ways to install automatic provers on your machine: 
36926  163 

46242  164 
\begin{sloppy} 
165 
\begin{enum} 

166 
\item[\labelitemi] If you installed an official Isabelle package, it should 

167 
already include properly setup executables for CVC3, E, SPASS, and Z3, ready to use.% 

57237
bc51864c2ac4
took out broken support for Yices from SMT2 stack  see 'NEWS' for rationale
blanchet
parents:
57211
diff
changeset

168 
\footnote{Vampire's license prevents us from doing the same for 
bc51864c2ac4
took out broken support for Yices from SMT2 stack  see 'NEWS' for rationale
blanchet
parents:
57211
diff
changeset

169 
this otherwise remarkable tool.} 
46242  170 
For Z3, you must additionally set the variable 
57028  171 
\texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a 
56119
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

172 
noncommercial usereither in the environment in which Isabelle is 
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

173 
launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or 
57028  174 
via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options 
56119
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

175 
> Isabelle > General'' in Isabelle/jEdit. 
46242  176 

177 
\item[\labelitemi] Alternatively, you can download the Isabelleaware CVC3, E, 

178 
SPASS, and Z3 binary packages from \download. Extract the archives, then add a 

179 
line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}% 

41747
f58d4d202924
fix path to etc/settings and etc/components in doc
blanchet
parents:
41740
diff
changeset

180 
\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at 
46242  181 
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

182 
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.} 
46242  183 
file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the 
184 
\texttt{components} file does not exist yet and you extracted SPASS to 

47577  185 
\texttt{/usr/local/spass3.8ds}, create it with the single line 
36926  186 

187 
\prew 

47577  188 
\texttt{/usr/local/spass3.8ds} 
36926  189 
\postw 
190 

47561
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

191 
in it. 
38043  192 

55334
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset

193 
\item[\labelitemi] If you prefer to build AgsyHOL, AltErgo, E, LEOII, 
52078  194 
Satallax, or SPASS manually, or found a Vampire executable somewhere (e.g., 
195 
\url{http://www.vprover.org/}), set the environment variable 

196 
\texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME}, 

197 
\texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or 

52757  198 
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{agsyHOL}, 
199 
\texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}), 

52078  200 
\texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable; 
201 
for AltErgo, set the 

202 
environment variable \texttt{WHY3\_HOME} to the directory that contains the 

203 
\texttt{why3} executable. 

57636
3ab503b04bdb
stick to external proofs when invoking E, because they are more detailed and do not merge steps
blanchet
parents:
57566
diff
changeset

204 
Sledgehammer has been tested with AgsyHOL 1.0, AltErgo 0.95.2, E 1.6 to 1.8, 
52996  205 
LEOII 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 3.0.% 
38063  206 
\footnote{Following the rewrite of Vampire, the counter for version numbers was 
52996  207 
reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more 
48652  208 
recent than 9.0 or 11.5.}% 
48006  209 
Since the ATPs' output formats are neither documented nor stable, other 
47577  210 
versions might not work well with Sledgehammer. Ideally, 
211 
you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION}, 

46242  212 
\texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or 
56380
9bb2856cc845
don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
blanchet
parents:
56379
diff
changeset

213 
\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0''). 
36926  214 

57241  215 
Similarly, if you want to build CVC3 or CVC4, or found a 
57237
bc51864c2ac4
took out broken support for Yices from SMT2 stack  see 'NEWS' for rationale
blanchet
parents:
57211
diff
changeset

216 
Z3 executable somewhere (e.g., \url{http://z3.codeplex.com/}), 
57241  217 
set the environment variable \texttt{CVC3\_\allowbreak SOLVER}, 
218 
\texttt{CVC4\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path 

219 
of the executable, \emph{including the file name}. Sledgehammer has been tested 

220 
with CVC3 2.2 and 2.4.1, CVC4 1.2, and Z3 4.3.2. Since Z3's output format is 

221 
somewhat unstable, other versions of the solver might not work well with 

222 
Sledgehammer. Ideally, also set 

223 
\texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, or \texttt{Z3\_NEW\_VERSION} to 

224 
the solver's version number (e.g., ``4.3.2''). 

46242  225 
\end{enum} 
226 
\end{sloppy} 

36926  227 

46242  228 
To check whether E, SPASS, Vampire, and/or Z3 are successfully installed, try 
229 
out the example in \S\ref{firststeps}. If the remote versions of any of these 

56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

230 
provers is used (identified by the prefix ``\textit{remote\_\/}''), or if the 
46242  231 
local versions fail to solve the easy goal presented there, something must be 
232 
wrong with the installation. 

233 

234 
Remote prover invocation requires Perl with the World Wide Web Library 

235 
(\texttt{libwwwperl}) installed. If you must use a proxy server to access the 

236 
Internet, set the \texttt{http\_proxy} environment variable to the proxy, either 

237 
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

238 
\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few 
46242  239 
examples: 
39152
f09b378cb252
make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents:
38997
diff
changeset

240 

f09b378cb252
make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents:
38997
diff
changeset

241 
\prew 
39153  242 
\texttt{http\_proxy=http://proxy.example.org} \\ 
243 
\texttt{http\_proxy=http://proxy.example.org:8080} \\ 

244 
\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

245 
\postw 
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset

246 

36926  247 
\section{First Steps} 
248 
\label{firststeps} 

249 

250 
To illustrate Sledgehammer in context, let us start a theory file and 

251 
attempt to prove a simple lemma: 

252 

253 
\prew 

254 
\textbf{theory}~\textit{Scratch} \\ 

255 
\textbf{imports}~\textit{Main} \\ 

256 
\textbf{begin} \\[2\smallskipamount] 

257 
% 

42945  258 
\textbf{lemma} ``$[a] = [b] \,\Longrightarrow\, a = b$'' \\ 
36926  259 
\textbf{sledgehammer} 
260 
\postw 

261 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

262 
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

263 
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

264 
after a few seconds: 
36926  265 

266 
\prew 

267 
\slshape 

57053
46000c075d07
shorten Sledgehammer output, as suggested by Andrei Popescu
blanchet
parents:
57040
diff
changeset

268 
Sledgehammer: ``\textit{e\/}'' \\ 
43054  269 
Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount] 
42945  270 
% 
57053
46000c075d07
shorten Sledgehammer output, as suggested by Andrei Popescu
blanchet
parents:
57040
diff
changeset

271 
Sledgehammer: ``\textit{z3\/}'' \\ 
46242  272 
Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount] 
273 
% 

57053
46000c075d07
shorten Sledgehammer output, as suggested by Andrei Popescu
blanchet
parents:
57040
diff
changeset

274 
Sledgehammer: ``\textit{vampire\/}'' \\ 
43054  275 
Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount] 
36926  276 
% 
57053
46000c075d07
shorten Sledgehammer output, as suggested by Andrei Popescu
blanchet
parents:
57040
diff
changeset

277 
Sledgehammer: ``\textit{spass\/}'' \\ 
43054  278 
Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount] 
36926  279 
% 
57053
46000c075d07
shorten Sledgehammer output, as suggested by Andrei Popescu
blanchet
parents:
57040
diff
changeset

280 
Sledgehammer: ``\textit{remote\_e\_sine\/}'' \\ 
46242  281 
Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). 
36926  282 
\postw 
283 

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

284 
Sledgehammer ran E, ESInE, SPASS, Vampire, and Z3 in parallel. Depending on 
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

285 
which provers are installed and how many processor cores are available, some of 
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

286 
the provers might be missing or present with a \textit{remote\_} prefix. 
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

287 
Waldmeister is run only for unit equational problems, where the goal's 
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

288 
conclusion is a (universally quantified) equation. 
36926  289 

55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

290 
For each successful prover, Sledgehammer gives a oneline \textit{metis} or 
56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

291 
\textit{smt2} method call. Rough timings are shown in parentheses, indicating how 
48387  292 
fast the call is. You can click the proof to insert it into the theory text. 
36926  293 

51190
2654b3965c8d
made "isar_proofs" a 3way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51189
diff
changeset

294 
In addition, you can ask Sledgehammer for an Isar text proof by enabling the 
49919  295 
\textit{isar\_proofs} option (\S\ref{outputformat}): 
36926  296 

297 
\prew 

49919  298 
\textbf{sledgehammer} [\textit{isar\_proofs}] 
36926  299 
\postw 
300 

301 
When Isar proof construction is successful, it can yield proofs that are more 

56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

302 
readable and also faster than the \textit{metis} or \textit{smt2} oneline 
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

303 
proofs. This feature is experimental and is only available for ATPs. 
36926  304 

37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset

305 
\section{Hints} 
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset

306 
\label{hints} 
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset

307 

42884  308 
This section presents a few hints that should help you get the most out of 
46643
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset

309 
Sledgehammer. Frequently asked questions are answered in 
45380  310 
\S\ref{frequentlyaskedquestions}. 
42884  311 

46242  312 
%\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak} 
313 
\newcommand\point[1]{\subsection{\emph{#1}}} 

42763  314 

315 
\point{Presimplify the goal} 

316 

37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset

317 
For best results, first simplify your problem by calling \textit{auto} or at 
42945  318 
least \textit{safe} followed by \textit{simp\_all}. The SMT solvers provide 
319 
arithmetic decision procedures, but the ATPs typically do not (or if they do, 

320 
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

321 
particularly good at heavy rewriting, but because they regard equations as 
42945  322 
undirected, they often prove theorems that require the reverse orientation of a 
323 
\textit{simp} rule. Higherorder problems can be tackled, but the success rate 

324 
is better for firstorder problems. Hence, you may get better results if you 

325 
first simplify the problem to remove higherorder features. 

37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset

326 

46242  327 
\point{Make sure E, SPASS, Vampire, and Z3 are locally installed} 
42763  328 

329 
Locally installed provers are faster and more reliable than those running on 

330 
servers. See \S\ref{installation} for details on how to install them. 

331 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

332 
\point{Familiarize yourself with the main options} 
42763  333 

334 
Sledgehammer's options are fully documented in \S\ref{commandsyntax}. Many of 

335 
the options are very specialized, but serious users of the tool should at least 

336 
familiarize themselves with the following options: 

337 

338 
\begin{enum} 

45516  339 
\item[\labelitemi] \textbf{\textit{provers}} (\S\ref{modeofoperation}) specifies 
42884  340 
the automatic provers (ATPs and SMT solvers) that should be run whenever 
341 
Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass 

46242  342 
remote\_vampire\/}''). For convenience, you can omit ``\textit{provers}~='' 
43014  343 
and simply write the prover names as a spaceseparated list (e.g., ``\textit{e 
46242  344 
spass remote\_vampire\/}''). 
42763  345 

48294  346 
\item[\labelitemi] \textbf{\textit{max\_facts}} (\S\ref{relevancefilter}) 
42884  347 
specifies the maximum number of facts that should be passed to the provers. By 
48294  348 
default, the value is proverdependent but varies between about 50 and 1000. If 
349 
the provers time out, you can try lowering this value to, say, 25 or 50 and see 

42884  350 
if that helps. 
42763  351 

49919  352 
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{outputformat}) specifies 
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

353 
that Isar proofs should be generated, in addition to oneline \textit{metis} or 
56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

354 
\textit{smt2} proofs. The length of the Isar proofs can be controlled by setting 
57245  355 
\textit{compress} (\S\ref{outputformat}). 
43038  356 

45516  357 
\item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the 
43038  358 
provers' time limit. It is set to 30 seconds, but since Sledgehammer runs 
359 
asynchronously you should not hesitate to raise this limit to 60 or 120 seconds 

360 
if you are the kind of user who can think clearly while ATPs are active. 

42763  361 
\end{enum} 
362 

42884  363 
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

364 
(\S\ref{commandsyntax}). 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

365 
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

366 
``$(\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

367 
to ensure that certain facts are included, or simply ``$(\textit{my\_facts})$'' 
58090  368 
to force Sledgehammer to run only with $\textit{my\_facts}$ (and any facts 
369 
chained into the goal). 

42763  370 

371 
\section{Frequently Asked Questions} 

372 
\label{frequentlyaskedquestions} 

373 

42945  374 
This sections answers frequently (and infrequently) asked questions about 
48387  375 
Sledgehammer. It is a good idea to skim over it now even if you do not have any 
42945  376 
questions at this stage. And if you have any further questions not listed here, 
377 
send them to the author at \authoremail. 

378 

43008
bb212c2ad238
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents:
43007
diff
changeset

379 
\point{Which facts are passed to the automatic provers?} 
42883  380 

48387  381 
Sledgehammer heuristically selects a few hundred relevant lemmas from the 
382 
currently loaded libraries. The component that performs this selection is 

383 
called \emph{relevance filter}. 

384 

385 
\begin{enum} 

386 
\item[\labelitemi] 

48388  387 
The traditional relevance filter, called \emph{MePo} 
388 
(\underline{Me}ng\underline{Pau}lson), assigns a score to every available fact 

389 
(lemma, theorem, definition, or axiom) based upon how many constants that fact 

390 
shares with the conjecture. This process iterates to include facts relevant to 

391 
those just accepted. The constants are weighted to give unusual ones greater 

392 
significance. MePo copes best when the conjecture contains some unusual 

393 
constants; if all the constants are common, it is unable to discriminate among 

394 
the hundreds of facts that are picked up. The filter is also memoryless: It has 

395 
no information about how many times a particular fact has been used in a proof, 

396 
and it cannot learn. 

48387  397 

398 
\item[\labelitemi] 

57272
fd539459a112
enabled MaSh by default  set 'MaSh' to 'none' in Isabelle Plugin Options to disable
blanchet
parents:
57245
diff
changeset

399 
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

400 
\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

401 
problem of finding relevant facts. 
48387  402 

50459  403 
\item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh. 
48387  404 
\end{enum} 
405 

50459  406 
The default is either MePo or MeSh, depending on whether the environment 
50221  407 
variable \texttt{MASH} is set and what class of provers the target prover 
408 
belongs to (\S\ref{relevancefilter}). 

42763  409 

42883  410 
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

411 
some provers get overwhelmed more easily than others. You can show the number of 
42883  412 
facts given using the \textit{verbose} option (\S\ref{outputformat}) and the 
413 
actual facts using \textit{debug} (\S\ref{outputformat}). 

414 

415 
Sledgehammer is good at finding short proofs combining a handful of existing 

416 
lemmas. If you are looking for longer proofs, you must typically restrict the 

48294  417 
number of facts, by setting the \textit{max\_facts} option 
43574  418 
(\S\ref{relevancefilter}) to, say, 25 or 50. 
42883  419 

42996  420 
You can also influence which facts are actually selected in a number of ways. If 
421 
you simply want to ensure that a fact is included, you can specify it using the 

422 
``$(\textit{add}{:}~\textit{my\_facts})$'' syntax. For example: 

423 
% 

424 
\prew 

425 
\textbf{sledgehammer} (\textit{add}: \textit{hd.simps} \textit{tl.simps}) 

426 
\postw 

427 
% 

428 
The specified facts then replace the least relevant facts that would otherwise be 

429 
included; the other selected facts remain the same. 

430 
If you want to direct the selection in a particular direction, you can specify 

431 
the facts via \textbf{using}: 

432 
% 

433 
\prew 

434 
\textbf{using} \textit{hd.simps} \textit{tl.simps} \\ 

435 
\textbf{sledgehammer} 

436 
\postw 

437 
% 

438 
The facts are then more likely to be selected than otherwise, and if they are 

439 
selected at iteration $j$ they also influence which facts are selected at 

440 
iterations $j + 1$, $j + 2$, etc. To give them even more weight, try 

441 
% 

442 
\prew 

443 
\textbf{using} \textit{hd.simps} \textit{tl.simps} \\ 

444 
\textbf{apply}~\textbf{} \\ 

445 
\textbf{sledgehammer} 

446 
\postw 

447 

46300  448 
\point{Why does Metis fail to reconstruct the proof?} 
449 

450 
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

451 
proof is too difficult for it. Metis's search is complete for firstorder logic 
5f37ef22f9af
update documentation after removal of 'min' subcommand
blanchet
parents:
57733
diff
changeset

452 
with equality, so if the proof was found by an ATP such as E, SPASS, or Vampire, 
5f37ef22f9af
update documentation after removal of 'min' subcommand
blanchet
parents:
57733
diff
changeset

453 
Metis should eventually find it, but that's little consolation. 
46300  454 

455 
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

456 
message ``Oneline proof reconstruction failed.'' This indicates that 
5f37ef22f9af
update documentation after removal of 'min' subcommand
blanchet
parents:
57733
diff
changeset

457 
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

458 
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

459 
the \textit{strict} option (\S\ref{problemencoding}). 
46300  460 

46640  461 
If the goal is actually unprovable and you did not specify an unsound encoding 
46300  462 
using \textit{type\_enc} (\S\ref{problemencoding}), this is a bug, and you are 
463 
strongly encouraged to report this to the author at \authoremail. 

464 

465 
\point{How can I tell whether a suggested proof is sound?} 

466 

467 
Earlier versions of Sledgehammer often suggested unsound proofseither proofs 

468 
of nontheorems or simply proofs that rely on typeunsound inferences. This 

46640  469 
is a thing of the past, unless you explicitly specify an unsound encoding 
46300  470 
using \textit{type\_enc} (\S\ref{problemencoding}). 
471 
% 

472 
Officially, the only form of ``unsoundness'' that lurks in the sound 

473 
encodings is related to missing characteristic theorems of datatypes. For 

474 
example, 

475 

476 
\prew 

477 
\textbf{lemma}~``$\exists \mathit{xs}.\; \mathit{xs} \neq []$'' \\ 

478 
\textbf{sledgehammer} () 

479 
\postw 

480 

481 
suggests an argumentless \textit{metis} call that fails. However, the conjecture 

482 
does actually hold, and the \textit{metis} call can be repaired by adding 

483 
\textit{list.distinct}. 

484 
% 

485 
We hope to address this problem in a future version of Isabelle. In the 

486 
meantime, you can avoid it by passing the \textit{strict} option 

487 
(\S\ref{problemencoding}). 

488 

46298  489 
\point{What are the \textit{full\_types}, \textit{no\_types}, and 
490 
\textit{mono\_tags} arguments to Metis?} 

42883  491 

46298  492 
The \textit{metis}~(\textit{full\_types}) proof method 
493 
and its cousin \textit{metis}~(\textit{mono\_tags}) are fullytyped 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

494 
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

495 
search is fully typed, and it also includes more powerful rules such as the 
45516  496 
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

497 
higherorder 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

498 
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

499 
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

500 
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

501 
preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with 
57719  502 
various sets of option for up to 1~second each time to ensure that the generated 
46298  503 
oneline proofs actually work and to display timing information. This can be 
47036  504 
configured using the \textit{preplay\_timeout} and \textit{dont\_preplay} 
505 
options (\S\ref{timeouts}).) 

46298  506 
% 
43229  507 
At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types}) 
508 
uses no type information at all during the proof search, which is more efficient 

509 
but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally 

510 
generated by Sledgehammer. 

46298  511 
% 
512 
See the \textit{type\_enc} option (\S\ref{problemencoding}) for details. 

43229  513 

46298  514 
Incidentally, if you ever see warnings such as 
42883  515 

516 
\prew 

43007  517 
\slshape 
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

518 
Metis: Falling back on ``\textit{metis} (\textit{full\_types})''. 
42883  519 
\postw 
520 

45380  521 
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

522 
\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

523 

46366  524 
\point{And what are the \textit{lifting} and \textit{hide\_lams} arguments 
46298  525 
to Metis?} 
526 

527 
Orthogonally to the encoding of types, it is important to choose an appropriate 

528 
translation of $\lambda$abstractions. Metis supports three translation schemes, 

529 
in decreasing order of power: Curry combinators (the default), 

530 
$\lambda$lifting, and a ``hiding'' scheme that disables all reasoning under 

531 
$\lambda$abstractions. The more powerful schemes also give the automatic 

532 
provers more rope to hang themselves. See the \textit{lam\_trans} option (\S\ref{problemencoding}) for details. 

533 

43054  534 
\point{Are generated proofs minimal?} 
43036  535 

43054  536 
Automatic provers frequently use many more facts than are necessary. 
57722  537 
Sledgehammer includes a minimization tool that takes a set of facts returned by 
538 
a given prover and repeatedly calls a prover or proof method with subsets of 

539 
those facts to find a minimal set. Reducing the number of facts typically helps 

540 
reconstruction, while also removing superfluous clutter from the proof scripts. 

43036  541 

43229  542 
In earlier versions of Sledgehammer, generated proofs were systematically 
543 
accompanied by a suggestion to invoke the minimization tool. This step is now 

57722  544 
performed by default but can be disabled using the \textit{minimize} option 
545 
(\S\ref{modeofoperation}). 

43036  546 

43008
bb212c2ad238
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents:
43007
diff
changeset

547 
\point{A strange error occurredwhat should I do?} 
42763  548 

549 
Sledgehammer tries to give informative error messages. Please report any strange 

53224  550 
error to the author at \authoremail. This applies doubly if you get the message 
42763  551 

42883  552 
\prew 
42763  553 
\slshape 
53224  554 
The prover derived ``\textit{False}'' using ``\textit{foo\/}'', 
555 
``\textit{bar\/}'', and ``\textit{baz\/}''. 

556 
This could be due to inconsistent axioms (including ``\textbf{sorry}''s) or to 

557 
a bug in Sledgehammer. If the problem persists, please contact the 

558 
Isabelle developers. 

42883  559 
\postw 
42763  560 

561 
\point{Auto can solve itwhy not Sledgehammer?} 

562 

563 
Problems can be easy for \textit{auto} and difficult for automatic provers, but 

48387  564 
the reverse is also true, so do not be discouraged if your first attempts fail. 
39320  565 
Because the system refers to all theorems known to Isabelle, it is particularly 
57040  566 
suitable when your goal has a short proof but requires lemmas that you do not 
567 
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

568 

42883  569 
\point{Why are there so many options?} 
570 

571 
Sledgehammer's philosophy should work out of the box, without user guidance. 

572 
Many of the options are meant to be used mostly by the Sledgehammer developers 

53102  573 
for experiments. Of course, feel free to try them out if you are so inclined. 
42883  574 

36926  575 
\section{Command Syntax} 
576 
\label{commandsyntax} 

577 

46242  578 
\subsection{Sledgehammer} 
57040  579 
\label{sledgehammer} 
46242  580 

36926  581 
Sledgehammer can be invoked at any point when there is an open goal by entering 
582 
the \textbf{sledgehammer} command in the theory file. Its general syntax is as 

583 
follows: 

584 

585 
\prew 

43216  586 
\textbf{sledgehammer} \qty{subcommand}$^?$ \qty{options}$^?$ \qty{facts\_override}$^?$ \qty{num}$^?$ 
36926  587 
\postw 
588 

43216  589 
In the general syntax, the \qty{subcommand} may be any of the following: 
36926  590 

591 
\begin{enum} 

45516  592 
\item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on 
43216  593 
subgoal number \qty{num} (1 by default), with the given options and facts. 
36926  594 

45516  595 
\item[\labelitemi] \textbf{\textit{messages}:} Redisplays recent messages issued 
40203  596 
by Sledgehammer. This allows you to examine results that might have been lost 
43216  597 
due to Sledgehammer's asynchronous nature. The \qty{num} argument specifies a 
47530  598 
limit on the number of messages to display (10 by default). 
36926  599 

45516  600 
\item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of 
41724  601 
automatic provers supported by Sledgehammer. See \S\ref{installation} and 
602 
\S\ref{modeofoperation} for more information on how to install automatic 

603 
provers. 

36926  604 

45516  605 
\item[\labelitemi] \textbf{\textit{running\_provers}:} Prints information about 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

606 
currently running automatic provers, including elapsed runtime and remaining 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

607 
time until timeout. 
36926  608 

50720  609 
\item[\labelitemi] \textbf{\textit{kill\_all}:} Terminates all running 
49365  610 
threads (automatic provers and machine learners). 
36926  611 

48393  612 
\item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote 
613 
ATPs available at System\On\TPTP \cite{sutcliffe2000}. 

614 
\end{enum} 

615 

49365  616 
In addition, the following subcommands provide finer control over machine 
48393  617 
learning with MaSh: 
618 

619 
\begin{enum} 

620 
\item[\labelitemi] \textbf{\textit{unlearn}:} Resets MaSh, erasing any 

621 
persistent state. 

48387  622 

48393  623 
\item[\labelitemi] \textbf{\textit{learn\_isar}:} Invokes MaSh on the current 
624 
theory to process all the available facts, learning from their Isabelle/Isar 

625 
proofs. This happens automatically at Sledgehammer invocations if the 

626 
\textit{learn} option (\S\ref{relevancefilter}) is enabled. 

48387  627 

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

628 
\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

629 
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

630 
automatic provers. The prover to use and its timeout can be set using the 
48393  631 
\textit{prover} (\S\ref{modeofoperation}) and \textit{timeout} 
632 
(\S\ref{timeouts}) options. It is recommended to perform learning using an 

633 
efficient firstorder ATP (such as E, SPASS, and Vampire) as opposed to a 

634 
higherorder ATP or an SMT solver. 

635 

636 
\item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn} 

637 
followed by \textit{learn\_isar}. 

638 

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

639 
\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

640 
followed by \textit{learn\_prover}. 
48387  641 

642 
\item[\labelitemi] \textbf{\textit{running\_learners}:} Prints information about 

643 
currently running machine learners, including elapsed runtime and remaining 

644 
time until timeout. 

36926  645 
\end{enum} 
646 

43216  647 
Sledgehammer's behavior can be influenced by various \qty{options}, which can be 
648 
specified in brackets after the \textbf{sledgehammer} command. The 

649 
\qty{options} are a list of keyvalue 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

650 
\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

651 
For example: 
36926  652 

653 
\prew 

49919  654 
\textbf{sledgehammer} [\textit{isar\_proofs}, \,\textit{timeout} = 120] 
36926  655 
\postw 
656 

657 
Default values can be set using \textbf{sledgehammer\_\allowbreak params}: 

658 

659 
\prew 

43216  660 
\textbf{sledgehammer\_params} \qty{options} 
36926  661 
\postw 
662 

663 
The supported options are described in \S\ref{optionreference}. 

664 

43216  665 
The \qty{facts\_override} argument lets you alter the set of facts that go 
666 
through the relevance filter. It may be of the form ``(\qty{facts})'', where 

667 
\qty{facts} is a spaceseparated list of Isabelle facts (theorems, local 

36926  668 
assumptions, etc.), in which case the relevance filter is bypassed and the given 
43216  669 
facts are used. It may also be of the form ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}})'', 
670 
``(\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', or ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}}\ 

671 
\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', where the relevance filter is instructed to 

672 
proceed as usual except that it should consider \qty{facts\/_{\mathrm{1}}} 

673 
highlyrelevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant. 

36926  674 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

675 
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

676 
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

677 
> Isabelle > General.'' For automatic runs, only the first prover set using 
54114  678 
\textit{provers} (\S\ref{modeofoperation}) is considered (typically E), 
679 
\textit{slice} (\S\ref{modeofoperation}) is disabled, 

680 
\textit{minimize} (\S\ref{modeofoperation}) is disabled, fewer facts are 

681 
passed to the prover, \textit{fact\_filter} (\S\ref{relevancefilter}) is set to 

682 
\textit{mepo}, \textit{strict} (\S\ref{problemencoding}) is enabled, 

683 
\textit{verbose} (\S\ref{outputformat}) and \textit{debug} 

684 
(\S\ref{outputformat}) are disabled, \textit{preplay\_timeout} 

685 
(\S\ref{timeouts}) is set to 0, and \textit{timeout} (\S\ref{timeouts}) is 

686 
superseded by the ``Auto Time Limit'' option in jEdit. Sledgehammer's output is 

687 
also more concise. 

39320  688 

46242  689 
\subsection{Metis} 
57040  690 
\label{metis} 
46242  691 

43216  692 
The \textit{metis} proof method has the syntax 
693 

694 
\prew 

45518  695 
\textbf{\textit{metis}}~(\qty{options})${}^?$~\qty{facts}${}^?$ 
43216  696 
\postw 
697 

45518  698 
where \qty{facts} is a list of arbitrary facts and \qty{options} is a 
699 
commaseparated list consisting of at most one $\lambda$ translation scheme 

700 
specification with the same semantics as Sledgehammer's \textit{lam\_trans} 

701 
option (\S\ref{problemencoding}) and at most one type encoding specification 

702 
with the same semantics as Sledgehammer's \textit{type\_enc} option 

703 
(\S\ref{problemencoding}). 

704 
% 

705 
The supported $\lambda$ translation schemes are \textit{hide\_lams}, 

46366  706 
\textit{lifting}, and \textit{combs} (the default). 
45518  707 
% 
708 
All the untyped type encodings listed in \S\ref{problemencoding} are supported. 

709 
For convenience, the following aliases are provided: 

710 
\begin{enum} 

48393  711 
\item[\labelitemi] \textbf{\textit{full\_types}:} Alias for \textit{poly\_guards\_query}. 
712 
\item[\labelitemi] \textbf{\textit{partial\_types}:} Alias for \textit{poly\_args}. 

713 
\item[\labelitemi] \textbf{\textit{no\_types}:} Alias for \textit{erased}. 

45518  714 
\end{enum} 
43216  715 

36926  716 
\section{Option Reference} 
717 
\label{optionreference} 

718 

43014  719 
\def\defl{\{} 
720 
\def\defr{\}} 

721 

36926  722 
\def\flushitem#1{\item[]\noindent\kern\leftmargin \textbf{#1}} 
47036  723 
\def\optrueonly#1{\flushitem{\textit{#1} $\bigl[$= \textit{true}$\bigr]$\enskip}\nopagebreak\\[\parskip]} 
43014  724 
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} 
725 
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} 

726 
\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

727 
\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  728 
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]} 
43014  729 
\def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]} 
730 
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]} 

36926  731 
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]} 
732 
\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} 

43014  733 
\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} 
36926  734 

735 
Sledgehammer's options are categorized as follows:\ mode of operation 

38984  736 
(\S\ref{modeofoperation}), problem encoding (\S\ref{problemencoding}), 
737 
relevance filter (\S\ref{relevancefilter}), output format 

57241  738 
(\S\ref{outputformat}), regression testing (\S\ref{regressiontesting}), 
739 
and timeouts (\S\ref{timeouts}). 

36926  740 

741 
The descriptions below refer to the following syntactic quantities: 

742 

743 
\begin{enum} 

45516  744 
\item[\labelitemi] \qtybf{string}: A string. 
745 
\item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}. 

746 
\item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or 

40203  747 
\textit{smart}. 
45516  748 
\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

749 
\item[\labelitemi] \qtybf{float}: A floatingpoint 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

750 
expressing a number of seconds. 
45516  751 
\item[\labelitemi] \qtybf{float\_pair\/}: A pair of floatingpoint numbers 
40343
4521d56aef63
use floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

752 
(e.g., 0.6 0.95). 
45516  753 
\item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}. 
36926  754 
\end{enum} 
755 

43217  756 
Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options 
47963  757 
have a negative counterpart (e.g., \textit{blocking} vs.\ 
758 
\textit{non\_blocking}). When setting Boolean options or their negative 

759 
counterparts, ``= \textit{true\/}'' may be omitted. 

36926  760 

761 
\subsection{Mode of Operation} 

762 
\label{modeofoperation} 

763 

764 
\begin{enum} 

43014  765 
\opnodefaultbrk{provers}{string} 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

766 
Specifies the automatic provers to use as a spaceseparated list (e.g., 
46299  767 
``\textit{e}~\textit{spass}~\textit{remote\_vampire\/}''). 
768 
Provers can be run locally or remotely; see \S\ref{installation} for 

769 
installation instructions. 

770 

771 
The following local provers are supported: 

36926  772 

48701  773 
\begin{sloppy} 
36926  774 
\begin{enum} 
55334
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset

775 
\item[\labelitemi] \textbf{\textit{agsyhol}:} AgsyHOL is an automatic 
52078  776 
higherorder 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

777 
with support for the TPTP typed higherorder syntax (THF0). To use AgsyHOL, set 
52078  778 
the environment variable \texttt{AGSYHOL\_HOME} to the directory that contains 
779 
the \texttt{agsyHOL} executable. Sledgehammer has been tested with version 1.0. 

780 

46643
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset

781 
\item[\labelitemi] \textbf{\textit{alt\_ergo}:} AltErgo is a polymorphic 
52078  782 
ATP developed by Bobot et al.\ \cite{altergo}. 
46643
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset

783 
It supports the TPTP polymorphic typed firstorder format (TFF1) via Why3 
53102  784 
\cite{why3}. To use AltErgo, set the environment variable \texttt{WHY3\_HOME} 
56379
d8ecce5d51cd
use AltErgo 0.95.2, the latest and greatest version
blanchet
parents:
56378
diff
changeset

785 
to the directory that contains the \texttt{why3} executable. Sledgehammer 
d8ecce5d51cd
use AltErgo 0.95.2, the latest and greatest version
blanchet
parents:
56378
diff
changeset

786 
requires AltErgo 0.95.2 and Why3 0.83. 
46643
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset

787 

45516  788 
\item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by 
42945  789 
Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3, 
790 
set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the 

46242  791 
executable, including the file name, or install the prebuilt CVC3 package from 
57241  792 
\download. Sledgehammer has been tested with versions 2.2 and 2.4.1. 
793 

794 
\item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 \cite{cvc4} is the successor to 

795 
CVC3. To use CVC4, set the environment variable \texttt{CVC4\_SOLVER} to the 

796 
complete path of the executable, including the file name, or install the 

797 
prebuilt CVC4 package from \download. Sledgehammer has been tested with version 

798 
1.2. 

42945  799 

45516  800 
\item[\labelitemi] \textbf{\textit{e}:} E is a firstorder resolution prover 
42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

801 
developed by Stephan Schulz \cite{schulz2002}. To use E, set the environment 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

802 
variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof} 
52757  803 
executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or 
47056  804 
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

805 
versions 1.6 to 1.8. 
48652  806 

807 
\item[\labelitemi] \textbf{\textit{e\_males}:} EMaLeS is a metaprover developed 

808 
by Daniel K\"uhlwein that implements strategy scheduling on top of E. To use 

809 
EMaLeS, set the environment variable \texttt{E\_MALES\_HOME} to the directory 

810 
that contains the \texttt{emales.py} script. Sledgehammer has been tested with 

811 
version 1.1. 

36926  812 

54694
af9cdb4989c7
added warning to documentation, based on isabelleusers thread
blanchet
parents:
54139
diff
changeset

813 
\item[\labelitemi] \textbf{\textit{e\_par}:} EPar is an experimental metaprover 
af9cdb4989c7
added warning to documentation, based on isabelleusers thread
blanchet
parents:
54139
diff
changeset

814 
developed by Josef Urban that implements strategy scheduling on top of E. To use 
af9cdb4989c7
added warning to documentation, based on isabelleusers thread
blanchet
parents:
54139
diff
changeset

815 
EPar, set the environment variable \texttt{E\_HOME} to the directory that 
af9cdb4989c7
added warning to documentation, based on isabelleusers thread
blanchet
parents:
54139
diff
changeset

816 
contains the \texttt{runepar.pl} script and the \texttt{eprover} and 
50929  817 
\texttt{epclextract} executables, or use the prebuilt E package from \download. 
54694
af9cdb4989c7
added warning to documentation, based on isabelleusers thread
blanchet
parents:
54139
diff
changeset

818 
Be aware that EPar is experimental software. It has been known to generate 
af9cdb4989c7
added warning to documentation, based on isabelleusers thread
blanchet
parents:
54139
diff
changeset

819 
zombie processes. Use at your own risks. 
50929  820 

48701  821 
\item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure 
822 
instantiationbased prover developed by Konstantin Korovin \cite{korovin2009}. 

823 
To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the 

48714  824 
directory that contains the \texttt{iprover} and \texttt{vclausify\_rel} 
825 
executables. Sledgehammer has been tested with version 0.99. 

48701  826 

827 
\item[\labelitemi] \textbf{\textit{iprover\_eq}:} iProverEq is an 

828 
instantiationbased prover with native support for equality developed by 

829 
Konstantin Korovin and Christoph Sticksel \cite{korovinsticksel2010}. To use 

830 
iProverEq, set the environment variable \texttt{IPROVER\_EQ\_HOME} to the 

48714  831 
directory that contains the \texttt{iprovereq} and \texttt{vclausify\_rel} 
832 
executables. Sledgehammer has been tested with version 0.8. 

48701  833 

45516  834 
\item[\labelitemi] \textbf{\textit{leo2}:} LEOII is an automatic 
44098  835 
higherorder prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, 
46242  836 
with support for the TPTP typed higherorder syntax (THF0). To use LEOII, set 
837 
the environment variable \texttt{LEO2\_HOME} to the directory that contains the 

52757  838 
\texttt{leo} executable. Sledgehammer requires version 1.3.4 or above. 
44098  839 

45516  840 
\item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic 
44098  841 
higherorder prover developed by Chad Brown et al.\ \cite{satallax}, with 
46242  842 
support for the TPTP typed higherorder syntax (THF0). To use Satallax, set the 
843 
environment variable \texttt{SATALLAX\_HOME} to the directory that contains the 

844 
\texttt{satallax} executable. Sledgehammer requires version 2.2 or above. 

44098  845 

45516  846 
\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a firstorder resolution 
42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

847 
prover developed by Christoph Weidenbach et al.\ \cite{weidenbachetal2009}. 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

848 
To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory 
47056  849 
that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the 
47577  850 
version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from 
48006  851 
\download. Sledgehammer requires version 3.8ds or above. 
36926  852 

48652  853 
\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a firstorder 
854 
resolution prover developed by Andrei Voronkov and his colleagues 

42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

855 
\cite{riazanovvoronkov2002}. To use Vampire, set the environment variable 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

856 
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire} 
48006  857 
executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., 
56380
9bb2856cc845
don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
blanchet
parents:
56379
diff
changeset

858 
``3.0''). Sledgehammer has been tested with versions 0.6 to 3.0. 
52996  859 
Versions strictly above 1.8 support the TPTP typed firstorder format (TFF0). 
40942  860 

45516  861 
\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

862 
Microsoft Research \cite{z3}. To use Z3, set the environment variable 
57211  863 
\texttt{Z3\_NEW\_SOLVER} to the complete path of the executable, including the file 
57028  864 
name, and set \texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a 
56119
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

865 
noncommercial usereither in the environment in which Isabelle is 
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

866 
launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or 
57028  867 
via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options 
56119
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

868 
> Isabelle > General'' in Isabelle/jEdit. Sledgehammer has been tested with 
57211  869 
a prerelease version of 4.3.2. 
56378  870 

871 
\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be 

872 
an ATP, exploiting Z3's support for the TPTP untyped and typed firstorder 

873 
formats (FOF and TFF0). It is included for experimental purposes. It requires 

56725  874 
version 4.3.1 of Z3 or above. To use it, set the environment variable 
56378  875 
\texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp} 
876 
executable. 

57536  877 
\end{enum} 
56378  878 

48701  879 
\end{sloppy} 
42945  880 

57536  881 
Moreover, the following remote provers are supported: 
42945  882 

883 
\begin{enum} 

52078  884 
\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

885 
AgsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe2000}. 
52078  886 

45516  887 
\item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs 
36926  888 
on Geoff Sutcliffe's Miami servers \cite{sutcliffe2000}. 
889 

45516  890 
\item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} ESInE is a metaprover 
47075  891 
developed by Kry\v stof Hoder \cite{sine} based on E. It runs on Geoff 
892 
Sutcliffe's Miami servers. 

44091  893 

45516  894 
\item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} EToFoF is a metaprover 
44091  895 
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami 
45516  896 
servers. This ATP supports the TPTP typed firstorder format (TFF0). The 
44091  897 
remote version of EToFoF runs on Geoff Sutcliffe's Miami servers. 
898 

48701  899 
\item[\labelitemi] \textbf{\textit{remote\_iprover}:} The 
45339  900 
remote version of iProver runs on Geoff Sutcliffe's Miami servers 
901 
\cite{sutcliffe2000}. 

902 

48701  903 
\item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} The 
45339  904 
remote version of iProverEq runs on Geoff Sutcliffe's Miami servers 
905 
\cite{sutcliffe2000}. 

906 

45516  907 
\item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEOII 
44098  908 
runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe2000}. 
42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

909 

45516  910 
\item[\labelitemi] \textbf{\textit{remote\_satallax}:} The remote version of 
44098  911 
Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe2000}. 
42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

912 

45516  913 
\item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a firstorder 
43625  914 
resolution prover developed by Stickel et al.\ \cite{snark}. It supports the 
45516  915 
TPTP typed firstorder format (TFF0). The remote version of SNARK runs on 
43625  916 
Geoff Sutcliffe's Miami servers. 
40073  917 

54788
a898e15b522a
primitive support for SPASSPirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54694
diff
changeset

918 
\item[\labelitemi] \textbf{\textit{remote\_spass\_pirate}:} SPASSPirate is a 
a898e15b522a
primitive support for SPASSPirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54694
diff
changeset

919 
highly experimental firstorder resolution prover developed by Daniel Wand. 
a898e15b522a
primitive support for SPASSPirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54694
diff
changeset

920 
The remote version of SPASSPirate run on a private server set up by Daniel 
a898e15b522a
primitive support for SPASSPirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54694
diff
changeset

921 
Wand. 
a898e15b522a
primitive support for SPASSPirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54694
diff
changeset

922 

45516  923 
\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of 
48006  924 
Vampire runs on Geoff Sutcliffe's Miami servers. 
42945  925 

45516  926 
\item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit 
42945  927 
equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be 
43625  928 
used to prove universally quantified equations using unconditional equations, 
929 
corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister 

930 
runs on Geoff Sutcliffe's Miami servers. 

36926  931 
\end{enum} 
932 

48405
7682bc885e8a
use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents:
48393
diff
changeset

933 
By default, Sledgehammer runs a selection of CVC3, E, ESInE, SPASS, Vampire, 
57237
bc51864c2ac4
took out broken support for Yices from SMT2 stack  see 'NEWS' for rationale
blanchet
parents:
57211
diff
changeset

934 
and Z3 in paralleleither locally or remotely, depending on the number of 
bc51864c2ac4
took out broken support for Yices from SMT2 stack  see 'NEWS' for rationale
blanchet
parents:
57211
diff
changeset

935 
processor cores available. 
36926  936 

44743  937 
It is generally a good idea to run several provers in parallel. Running E, 
938 
SPASS, and Vampire for 5~seconds yields a similar success rate to running the 

939 
most effective of these for 120~seconds \cite{boehmenipkow2010}. 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

940 

6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

941 
\opnodefault{prover}{string} 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

942 
Alias for \textit{provers}. 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

943 

38983  944 
\opfalse{blocking}{non\_blocking} 
945 
Specifies whether the \textbf{sledgehammer} command should operate 

946 
synchronously. The asynchronous (nonblocking) mode lets the user start proving 

947 
the putative theorem manually while Sledgehammer looks for a proof, but it can 

42995
e23f61546cf0
always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
blanchet
parents:
42964
diff
changeset

948 
also be more confusing. Irrespective of the value of this option, Sledgehammer 
53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

949 
is always run synchronously if \textit{debug} (\S\ref{outputformat}) is 
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

950 
enabled. 
38983  951 

45708
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

952 
\optrue{slice}{dont\_slice} 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset

953 
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

954 
segments, each of which has its own set of possibly proverdependent options. 
42446  955 
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

956 
setofsupport (SOS) strategy, whereas the second slice runs without it. For E, 
42446  957 
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

958 
number of facts. For SMT solvers, several slices are tried with the same options 
42446  959 
each time but fewer and fewer facts. According to benchmarks with a timeout of 
960 
30 seconds, slicing is a valuable optimization, and you should probably leave it 

54114  961 
enabled unless you are conducting experiments. 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset

962 

724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset

963 
\nopagebreak 
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset

964 
{\small See also \textit{verbose} (\S\ref{outputformat}).} 
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset

965 

57722  966 
\optrue{minimize}{dont\_minimize} 
45708
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

967 
Specifies whether the minimization tool should be invoked automatically after 
57722  968 
proof search. 
45708
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

969 

7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

970 
\nopagebreak 
47036  971 
{\small See also \textit{preplay\_timeout} (\S\ref{timeouts}) 
972 
and \textit{dont\_preplay} (\S\ref{timeouts}).} 

45708
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

973 

53801  974 
\opfalse{spy}{dont\_spy} 
975 
Specifies whether Sledgehammer should record statistics in 

976 
\texttt{\$ISA\BELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak spy\_\allowbreak sledgehammer}. 

977 
These statistics can be useful to the developers of Sledgehammer. If you are willing to have your 

978 
interactions recorded in the name of science, please enable this feature and send the statistics 

979 
file every now and then to the author of this manual (\authoremail). 

980 
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

981 
\texttt{SLEDGEHAMMER\_SPY} to \textit{yes}. 
53801  982 

983 
\nopagebreak 

984 
{\small See also \textit{debug} (\S\ref{outputformat}).} 

985 

36926  986 
\opfalse{overlord}{no\_overlord} 
987 
Specifies whether Sledgehammer should put its temporary files in 

988 
\texttt{\$ISA\BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for 

989 
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

990 
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

991 
\texttt{mash\_}; you may safely remove them after Sledgehammer has run. 
36926  992 

54139  993 
\textbf{Warning:} This option is not threadsafe. Use at your own risks. 
994 

36926  995 
\nopagebreak 
996 
{\small See also \textit{debug} (\S\ref{outputformat}).} 

997 
\end{enum} 

998 

48387  999 
\subsection{Relevance Filter} 
1000 
\label{relevancefilter} 

1001 

1002 
\begin{enum} 

48388  1003 
\opdefault{fact\_filter}{string}{smart} 
1004 
Specifies the relevance filter to use. The following filters are available: 

1005 

1006 
\begin{enum} 

1007 
\item[\labelitemi] \textbf{\textit{mepo}:} 

1008 
The traditional memoryless MePo relevance filter. 

1009 

1010 
\item[\labelitemi] \textbf{\textit{mash}:} 

57532  1011 
The MaSh machine learner. Three learning algorithms are provided: 
57019  1012 

1013 
\begin{enum} 

57463  1014 
\item[\labelitemi] \textbf{\textit{nb}} is an implementation of naive Bayes. 
57019  1015 

57463  1016 
\item[\labelitemi] \textbf{\textit{knn}} is an implementation of $k$nearest 
1017 
neighbors. 

1018 

57659
b246943b3aa3
reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents:
57636
diff
changeset

1019 
\item[\labelitemi] \textbf{\textit{nb\_knn}} (also called \textbf{\textit{yes}} 
b246943b3aa3
reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents:
57636
diff
changeset

1020 
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

1021 
neighbors. 
57019  1022 
\end{enum} 
1023 

57272
fd539459a112
enabled MaSh by default  set 'MaSh' to 'none' in Isabelle Plugin Options to disable
blanchet
parents:
57245
diff
changeset

1024 
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

1025 
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

1026 

57659
b246943b3aa3
reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents:
57636
diff
changeset

1027 
The default algorithm is \textit{nb\_knn}. The algorithm can be selected by 
57532  1028 
setting \texttt{MASH}either in the environment in which Isabelle is launched, 
1029 
in your 

57463  1030 
\texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak etc/\allowbreak settings} 
1031 
file, or via the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle > 

57532  1032 
General'' in Isabelle/jEdit. Persistent data for both algorithms is stored in 
1033 
the directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak 

1034 
mash}. 

48388  1035 

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

1036 
\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

1037 
rankings from MePo and MaSh. 
48388  1038 

57659
b246943b3aa3
reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents:
57636
diff
changeset

1039 
\item[\labelitemi] \textbf{\textit{smart}:} A combination of MePo, MaSh, and 
b246943b3aa3
reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents:
57636
diff
changeset

1040 
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

1041 
behaves like MePo. 
48388  1042 
\end{enum} 
1043 

48387  1044 
\opdefault{max\_facts}{smart\_int}{smart} 
1045 
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

1046 
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

1047 
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

1048 
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

1049 

48387  1050 
\opdefault{fact\_thresholds}{float\_pair}{\upshape 0.45~0.85} 
1051 
Specifies the thresholds above which facts are considered relevant by the 

1052 
relevance filter. The first threshold is used for the first iteration of the 

1053 
relevance filter and the second threshold is used for the last iteration (if it 

1054 
is reached). The effective threshold is quadratically interpolated for the other 

1055 
iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems 

1056 
are relevant and 1 only theorems that refer to previously seen constants. 

1057 

48388  1058 
\optrue{learn}{dont\_learn} 
1059 
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

1060 
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

1061 
place only if MaSh is enabled. 
48388  1062 

48387  1063 
\opdefault{max\_new\_mono\_instances}{int}{smart} 
1064 
Specifies the maximum number of monomorphic instances to generate beyond 

1065 
\textit{max\_facts}. The higher this limit is, the more monomorphic instances 

1066 
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

1067 
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

1068 
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

1069 
most provers, this value is 100. 
48387  1070 

1071 
\nopagebreak 

1072 
{\small See also \textit{type\_enc} (\S\ref{problemencoding}).} 

1073 

1074 
\opdefault{max\_mono\_iters}{int}{smart} 

1075 
Specifies the maximum number of iterations for the monomorphization fixpoint 

1076 
construction. The higher this limit is, the more monomorphic instances are 

1077 
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

1078 
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

1079 
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

1080 
For most provers, this value is 3. 
48387  1081 

1082 
\nopagebreak 

1083 
{\small See also \textit{type\_enc} (\S\ref{problemencoding}).} 

1084 
\end{enum} 

1085 

36926  1086 
\subsection{Problem Encoding} 
1087 
\label{problemencoding} 

1088 

45516  1089 
\newcommand\comb[1]{\const{#1}} 
1090 

36926  1091 
\begin{enum} 
45516  1092 
\opdefault{lam\_trans}{string}{smart} 
1093 
Specifies the $\lambda$ translation scheme to use in ATP problems. The supported 

1094 
translation schemes are listed below: 

1095 

1096 
\begin{enum} 

1097 
\item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$abstractions 

1098 
by replacing them by unspecified fresh constants, effectively disabling all 

1099 
reasoning under $\lambda$abstractions. 

1100 

46366  1101 
\item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new 
45516  1102 
supercombinator \const{c} for each cluster of $n$~$\lambda$abstractions, 
1103 
defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$lifting). 

1104 

46366  1105 
\item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry 
45516  1106 
combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators 
1107 
enable the ATPs to synthesize $\lambda$terms but tend to yield bulkier formulas 

1108 
than $\lambda$lifting: The translation is quadratic in the worst case, and the 

1109 
equational definitions of the combinators are very prolific in the context of 

1110 
resolution. 

1111 

46366  1112 
\item[\labelitemi] \textbf{\textit{combs\_and\_lifting}:} Introduce a new 
45516  1113 
supercombinator \const{c} for each cluster of $\lambda$abstractions and characterize it both using a 
1114 
lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators. 

1115 

46366  1116 
\item[\labelitemi] \textbf{\textit{combs\_or\_lifting}:} For each cluster of 
1117 
$\lambda$abstractions, heuristically choose between $\lambda$lifting and Curry 

1118 
combinators. 

1119 

45516  1120 
\item[\labelitemi] \textbf{\textit{keep\_lams}:} 
1121 
Keep the $\lambda$abstractions in the generated problems. This is available 

1122 
only with provers that support the THF0 syntax. 

1123 

1124 
\item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used 

1125 
depends on the ATP and should be the most efficient scheme for that ATP. 

1126 
\end{enum} 

1127 

46366  1128 
For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting}, 
1129 
irrespective of the value of this option. 

45516  1130 

46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46366
diff
changeset

1131 
\opsmartx{uncurried\_aliases}{no\_uncurried\_aliases} 
46411  1132 
Specifies whether fresh function symbols should be generated as aliases for 
1133 
applications of curried functions in ATP problems. 

46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46366
diff
changeset

1134 

43627
ecd4bb7a8bc0
update documentation after "type_enc" renaming + fixed a few other outofdate factlets
blanchet
parents:
43625
diff
changeset

1135 
\opdefault{type\_enc}{string}{smart} 
ecd4bb7a8bc0
update documentation after "type_enc" renaming + fixed a few other outofdate factlets
blanchet
parents:
43625
diff
changeset

1136 
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 outofdate factlets
blanchet
parents:
43625
diff
changeset

1137 
are unsound, meaning that they can give rise to spurious proofs 
48093  1138 
(unreconstructible using \textit{metis}). The type encodings are 
46300  1139 
listed below, with an indication of their soundness in parentheses. 
48093  1140 
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

1141 
reconstruction with \textit{metis}, unless the \textit{strict} option (described 
46302  1142 
below) is enabled. 
42228  1143 

1144 
\begin{enum} 

48090  1145 
\item[\labelitemi] \textbf{\textit{erased} (unsound):} No type information is 
46300  1146 
supplied to the ATP, not even to resolve overloading. Types are simply erased. 
42582  1147 

45516  1148 
\item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using 
46300  1149 
a predicate \const{g}$(\tau, t)$ that guards bound 
48090  1150 
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

1151 
arguments, to resolve overloading. 
42685  1152 

45516  1153 
\item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is 
46300  1154 
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

1155 

45516  1156 
\item[\labelitemi] \textbf{\textit{poly\_args} (unsound):} 
43990  1157 
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

1158 
resolve overloading, but otherwise no type information is encoded. This 
57040  1159 
is the default encoding used by the \textit{metis} proof method. 
42685  1160 

45516  1161 
\item[\labelitemi] 
42722  1162 
\textbf{% 
44494
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset

1163 
\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

1164 
\textit{raw\_mono\_args} (unsound):} \\ 
43990  1165 
Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args}, 
42722  1166 
respectively, but the problem is additionally monomorphized, meaning that type 
1167 
variables are instantiated with heuristically chosen ground types. 

1168 
Monomorphization can simplify reasoning but also leads to larger fact bases, 

1169 
which can slow down the ATPs. 

42582  1170 

45516  1171 
\item[\labelitemi] 
42722  1172 
\textbf{% 
44494
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset

1173 
\textit{mono\_guards}, \textit{mono\_tags} (sound); 
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset

1174 
\textit{mono\_args} (unsound):} \\ 
42722  1175 
Similar to 
44494
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset

1176 
\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

1177 
\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

1178 
instead of being supplied as ground term arguments. The binary predicate 
46300  1179 
$\const{g}(\tau, t)$ becomes a unary predicate 
1180 
$\const{g\_}\tau(t)$, and the binary function 

1181 
$\const{t}(\tau, t)$ becomes a unary function 

1182 
$\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

1183 

46435  1184 
\item[\labelitemi] \textbf{\textit{mono\_native} (sound):} Exploits native 
46643
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset

1185 
firstorder types if the prover supports the TFF0, TFF1, or THF0 syntax; 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset

1186 
otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized. 
43625  1187 

46435  1188 
\item[\labelitemi] \textbf{\textit{mono\_native\_higher} (sound):} Exploits 
1189 
native higherorder types if the prover supports the THF0 syntax; otherwise, 

1190 
falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is 

1191 
monomorphized. 

42681  1192 

46643
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset

1193 
\item[\labelitemi] \textbf{\textit{poly\_native} (sound):} Exploits native 
48078  1194 
firstorder polymorphic types if the prover supports the TFF1 syntax; otherwise, 
46643
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset

1195 
falls back on \textit{mono\_native}. 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset

1196 

45516  1197 
\item[\labelitemi] 
42681  1198 
\textbf{% 
44494
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset

1199 
\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

1200 
\textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\ 
46435  1201 
\textit{mono\_native}? (sound*):} \\ 
43990  1202 
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

1203 
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards}, 
47036  1204 
\textit{mono\_tags}, and \textit{mono\_native} are fully typed and sound. For 
1205 
each of these, Sledgehammer also provides a lighter variant identified by a 

1206 
question mark (`\hbox{?}')\ that detects and erases monotonic types, notably 

1207 
infinite types. (For \textit{mono\_native}, the types are not actually erased 

1208 
but rather replaced by a shared uniform type of individuals.) As argument to the 

1209 
\textit{metis} proof method, the question mark is replaced by a 

1210 
\hbox{``\textit{\_query\/}''} suffix. 

42582  1211 

45516  1212 
\item[\labelitemi] 
42887
771be1dcfef6
document new type system and soundness properties of the different systems
blanchet
parents:
42884
diff
changeset

1213 
\textbf{% 
44769  1214 
\textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\ 
1215 
\textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\ 

46300  1216 
(sound*):} \\ 
44816  1217 
Even lighter versions of the `\hbox{?}' encodings. As argument to the 
1218 
\textit{metis} proof method, the `\hbox{??}' suffix is replaced by 

46242
99a2a541c125
improve installation instructions
blanchet 