blanchet@36918
|
1 |
\documentclass[a4paper,12pt]{article}
|
blanchet@36918
|
2 |
\usepackage[T1]{fontenc}
|
blanchet@36918
|
3 |
\usepackage{amsmath}
|
blanchet@36918
|
4 |
\usepackage{amssymb}
|
blanchet@36918
|
5 |
\usepackage[english,french]{babel}
|
blanchet@36918
|
6 |
\usepackage{color}
|
blanchet@36918
|
7 |
\usepackage{footmisc}
|
blanchet@36918
|
8 |
\usepackage{graphicx}
|
blanchet@36918
|
9 |
%\usepackage{mathpazo}
|
blanchet@36918
|
10 |
\usepackage{multicol}
|
blanchet@36918
|
11 |
\usepackage{stmaryrd}
|
blanchet@36918
|
12 |
%\usepackage[scaled=.85]{beramono}
|
wenzelm@43382
|
13 |
\usepackage{../../lib/texinputs/isabelle,../iman,../pdfsetup}
|
blanchet@36918
|
14 |
|
blanchet@47113
|
15 |
\newcommand\download{\url{http://www21.in.tum.de/~blanchet/\#software}}
|
blanchet@47113
|
16 |
|
blanchet@44057
|
17 |
\def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}}
|
blanchet@44057
|
18 |
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$}
|
blanchet@44057
|
19 |
|
blanchet@46387
|
20 |
\newcommand\const[1]{\textsf{#1}}
|
blanchet@46387
|
21 |
|
blanchet@36918
|
22 |
%\oddsidemargin=4.6mm
|
blanchet@36918
|
23 |
%\evensidemargin=4.6mm
|
blanchet@36918
|
24 |
%\textwidth=150mm
|
blanchet@36918
|
25 |
%\topmargin=4.6mm
|
blanchet@36918
|
26 |
%\headheight=0mm
|
blanchet@36918
|
27 |
%\headsep=0mm
|
blanchet@36918
|
28 |
%\textheight=234mm
|
blanchet@36918
|
29 |
|
blanchet@36918
|
30 |
\def\Colon{\mathord{:\mkern-1.5mu:}}
|
blanchet@36918
|
31 |
%\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
|
blanchet@36918
|
32 |
%\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
|
blanchet@36918
|
33 |
\def\lparr{\mathopen{(\mkern-4mu\mid}}
|
blanchet@36918
|
34 |
\def\rparr{\mathclose{\mid\mkern-4mu)}}
|
blanchet@36918
|
35 |
|
blanchet@36918
|
36 |
\def\unk{{?}}
|
blanchet@36918
|
37 |
\def\undef{(\lambda x.\; \unk)}
|
blanchet@36918
|
38 |
%\def\unr{\textit{others}}
|
blanchet@36918
|
39 |
\def\unr{\ldots}
|
blanchet@36918
|
40 |
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
|
blanchet@36918
|
41 |
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
|
blanchet@36918
|
42 |
|
blanchet@36918
|
43 |
\urlstyle{tt}
|
blanchet@36918
|
44 |
|
blanchet@36918
|
45 |
\begin{document}
|
blanchet@36918
|
46 |
|
blanchet@46387
|
47 |
%%% TYPESETTING
|
blanchet@46387
|
48 |
%\renewcommand\labelitemi{$\bullet$}
|
blanchet@46387
|
49 |
\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}
|
blanchet@46387
|
50 |
|
blanchet@36918
|
51 |
\selectlanguage{english}
|
blanchet@36918
|
52 |
|
blanchet@36918
|
53 |
\title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
|
blanchet@36918
|
54 |
Hammering Away \\[\smallskipamount]
|
blanchet@36918
|
55 |
\Large A User's Guide to Sledgehammer for Isabelle/HOL}
|
blanchet@36918
|
56 |
\author{\hbox{} \\
|
blanchet@36918
|
57 |
Jasmin Christian Blanchette \\
|
blanchet@43843
|
58 |
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount]
|
blanchet@43843
|
59 |
{\normalsize with contributions from} \\[4\smallskipamount]
|
blanchet@43843
|
60 |
Lawrence C. Paulson \\
|
blanchet@43843
|
61 |
{\normalsize Computer Laboratory, University of Cambridge} \\
|
blanchet@36918
|
62 |
\hbox{}}
|
blanchet@36918
|
63 |
|
blanchet@36918
|
64 |
\maketitle
|
blanchet@36918
|
65 |
|
blanchet@36918
|
66 |
\tableofcontents
|
blanchet@36918
|
67 |
|
blanchet@36918
|
68 |
\setlength{\parskip}{.7em plus .2em minus .1em}
|
blanchet@36918
|
69 |
\setlength{\parindent}{0pt}
|
blanchet@36918
|
70 |
\setlength{\abovedisplayskip}{\parskip}
|
blanchet@36918
|
71 |
\setlength{\abovedisplayshortskip}{.9\parskip}
|
blanchet@36918
|
72 |
\setlength{\belowdisplayskip}{\parskip}
|
blanchet@36918
|
73 |
\setlength{\belowdisplayshortskip}{.9\parskip}
|
blanchet@36918
|
74 |
|
blanchet@36918
|
75 |
% General-purpose enum environment with correct spacing
|
blanchet@36918
|
76 |
\newenvironment{enum}%
|
blanchet@36918
|
77 |
{\begin{list}{}{%
|
blanchet@36918
|
78 |
\setlength{\topsep}{.1\parskip}%
|
blanchet@36918
|
79 |
\setlength{\partopsep}{.1\parskip}%
|
blanchet@36918
|
80 |
\setlength{\itemsep}{\parskip}%
|
blanchet@36918
|
81 |
\advance\itemsep by-\parsep}}
|
blanchet@36918
|
82 |
{\end{list}}
|
blanchet@36918
|
83 |
|
blanchet@36918
|
84 |
\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
|
blanchet@36918
|
85 |
\advance\rightskip by\leftmargin}
|
blanchet@36918
|
86 |
\def\post{\vskip0pt plus1ex\endgroup}
|
blanchet@36918
|
87 |
|
blanchet@36918
|
88 |
\def\prew{\pre\advance\rightskip by-\leftmargin}
|
blanchet@36918
|
89 |
\def\postw{\post}
|
blanchet@36918
|
90 |
|
blanchet@36918
|
91 |
\section{Introduction}
|
blanchet@36918
|
92 |
\label{introduction}
|
blanchet@36918
|
93 |
|
blanchet@43805
|
94 |
Sledgehammer is a tool that applies automatic theorem provers (ATPs)
|
blanchet@41190
|
95 |
and satisfiability-modulo-theories (SMT) solvers on the current goal. The
|
blanchet@44962
|
96 |
supported ATPs are E \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF
|
blanchet@44962
|
97 |
\cite{tofof}, LEO-II \cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark},
|
blanchet@44962
|
98 |
SPASS \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, and
|
blanchet@44962
|
99 |
Waldmeister \cite{waldmeister}. The ATPs are run either locally or remotely via
|
blanchet@44962
|
100 |
the System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs,
|
blanchet@44962
|
101 |
the SMT solvers Z3 \cite{z3} is used by default, and you can tell Sledgehammer
|
blanchet@44962
|
102 |
to try CVC3 \cite{cvc3} and Yices \cite{yices} as well; these are run either
|
blanchet@44962
|
103 |
locally or on a server at the TU M\"unchen.
|
blanchet@36918
|
104 |
|
blanchet@40254
|
105 |
The problem passed to the automatic provers consists of your current goal
|
blanchet@40254
|
106 |
together with a heuristic selection of hundreds of facts (theorems) from the
|
blanchet@40254
|
107 |
current theory context, filtered by relevance. Because jobs are run in the
|
blanchet@40254
|
108 |
background, you can continue to work on your proof by other means. Provers can
|
blanchet@40254
|
109 |
be run in parallel. Any reply (which may arrive half a minute later) will appear
|
blanchet@40254
|
110 |
in the Proof General response buffer.
|
blanchet@37517
|
111 |
|
blanchet@40254
|
112 |
The result of a successful proof search is some source text that usually (but
|
blanchet@40254
|
113 |
not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
|
blanchet@46251
|
114 |
proof relies on the general-purpose \textit{metis} proof method, which
|
blanchet@46251
|
115 |
integrates the Metis ATP in Isabelle/HOL with explicit inferences going through
|
blanchet@46251
|
116 |
the kernel. Thus its results are correct by construction.
|
blanchet@36918
|
117 |
|
blanchet@39566
|
118 |
In this manual, we will explicitly invoke the \textbf{sledgehammer} command.
|
blanchet@45607
|
119 |
Sledgehammer also provides an automatic mode that can be enabled via the ``Auto
|
blanchet@45607
|
120 |
Sledgehammer'' option in Proof General's ``Isabelle'' menu. In this mode,
|
blanchet@45607
|
121 |
Sledgehammer is run on every newly entered theorem. The time limit for Auto
|
blanchet@45607
|
122 |
Sledgehammer and other automatic tools can be set using the ``Auto Tools Time
|
blanchet@45607
|
123 |
Limit'' option.
|
blanchet@39566
|
124 |
|
blanchet@36918
|
125 |
\newbox\boxA
|
blanchet@47126
|
126 |
\setbox\boxA=\hbox{\texttt{NOSPAM}}
|
blanchet@36918
|
127 |
|
blanchet@47126
|
128 |
\newcommand\authoremail{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
|
blanchet@43628
|
129 |
in.\allowbreak tum.\allowbreak de}}
|
blanchet@43628
|
130 |
|
blanchet@40937
|
131 |
To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is
|
blanchet@40937
|
132 |
imported---this is rarely a problem in practice since it is part of
|
blanchet@40937
|
133 |
\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's
|
blanchet@36918
|
134 |
\texttt{src/HOL/Metis\_Examples} directory.
|
blanchet@36918
|
135 |
Comments and bug reports concerning Sledgehammer or this manual should be
|
blanchet@43752
|
136 |
directed to the author at \authoremail.
|
blanchet@36918
|
137 |
|
blanchet@36918
|
138 |
\vskip2.5\smallskipamount
|
blanchet@36918
|
139 |
|
blanchet@36918
|
140 |
%\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
|
blanchet@36918
|
141 |
%suggesting several textual improvements.
|
blanchet@36918
|
142 |
|
blanchet@36918
|
143 |
\section{Installation}
|
blanchet@36918
|
144 |
\label{installation}
|
blanchet@36918
|
145 |
|
blanchet@36918
|
146 |
Sledgehammer is part of Isabelle, so you don't need to install it. However, it
|
blanchet@47113
|
147 |
relies on third-party automatic provers (ATPs and SMT solvers).
|
blanchet@43628
|
148 |
|
blanchet@47113
|
149 |
Among the ATPs, E, LEO-II, Satallax, SPASS, and Vampire can be run locally; in
|
blanchet@46210
|
150 |
addition, E, E-SInE, E-ToFoF, iProver, iProver-Eq, LEO-II, Satallax, SNARK,
|
blanchet@46210
|
151 |
Waldmeister, and Vampire are available remotely via System\-On\-TPTP
|
blanchet@46210
|
152 |
\cite{sutcliffe-2000}. If you want better performance, you should at least
|
blanchet@46210
|
153 |
install E and SPASS locally.
|
blanchet@36918
|
154 |
|
blanchet@47113
|
155 |
Among the SMT solvers, CVC3, Yices, and Z3 can be run locally, and CVC3 and Z3
|
blanchet@47113
|
156 |
can be run remotely on a TU M\"unchen server. If you want better performance and
|
blanchet@47113
|
157 |
get the ability to replay proofs that rely on the \emph{smt} proof method
|
blanchet@47113
|
158 |
without an Internet connection, you should at least install Z3 locally.
|
blanchet@36918
|
159 |
|
blanchet@47113
|
160 |
There are three main ways to install automatic provers on your machine:
|
blanchet@47113
|
161 |
|
blanchet@47113
|
162 |
\begin{sloppy}
|
blanchet@36918
|
163 |
\begin{enum}
|
blanchet@47113
|
164 |
\item[\labelitemi] If you installed an official Isabelle package, it should
|
blanchet@47113
|
165 |
already include properly setup executables for CVC3, E, SPASS, and Z3, ready to use.%
|
blanchet@47113
|
166 |
\footnote{Vampire's and Yices's licenses prevent us from doing the same for
|
blanchet@47113
|
167 |
these otherwise remarkable tools.}
|
blanchet@47113
|
168 |
For Z3, you must additionally set the variable
|
blanchet@47113
|
169 |
\texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
|
blanchet@47113
|
170 |
noncommercial user, either in the environment in which Isabelle is
|
blanchet@47113
|
171 |
launched or in your
|
blanchet@47113
|
172 |
\texttt{\char`\~/\$ISABELLE\_HOME\_USER/etc/settings} file.
|
blanchet@36918
|
173 |
|
blanchet@47113
|
174 |
\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, E,
|
blanchet@47113
|
175 |
SPASS, and Z3 binary packages from \download. Extract the archives, then add a
|
blanchet@47113
|
176 |
line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}%
|
blanchet@42618
|
177 |
\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
|
blanchet@47113
|
178 |
startup. Its value can be retrieved by executing \texttt{isabelle}
|
blanchet@42618
|
179 |
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
|
blanchet@47113
|
180 |
file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the
|
blanchet@47113
|
181 |
\texttt{components} file does not exist yet and you extracted SPASS to
|
blanchet@47113
|
182 |
\texttt{/usr/local/spass-3.7}, create it with the single line
|
blanchet@36918
|
183 |
|
blanchet@36918
|
184 |
\prew
|
blanchet@36918
|
185 |
\texttt{/usr/local/spass-3.7}
|
blanchet@36918
|
186 |
\postw
|
blanchet@36918
|
187 |
|
blanchet@47113
|
188 |
(including an invisible newline character) in it.
|
blanchet@38289
|
189 |
|
blanchet@47113
|
190 |
\item[\labelitemi] If you prefer to build E, LEO-II, Satallax, or SPASS
|
blanchet@47113
|
191 |
manually, or found a Vampire executable somewhere (e.g.,
|
blanchet@47113
|
192 |
\url{http://www.vprover.org/}), set the environment variable \texttt{E\_HOME},
|
blanchet@47113
|
193 |
\texttt{LEO2\_HOME}, \texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or
|
blanchet@38289
|
194 |
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
|
blanchet@47113
|
195 |
\texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable.
|
blanchet@47113
|
196 |
Sledgehammer has been tested with E 1.0 to 1.4, LEO-II 1.2.9, Satallax 2.2,
|
blanchet@47113
|
197 |
SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8%
|
blanchet@38309
|
198 |
\footnote{Following the rewrite of Vampire, the counter for version numbers was
|
blanchet@45278
|
199 |
reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent
|
blanchet@47113
|
200 |
than 9.0 or 11.5.}%
|
blanchet@38309
|
201 |
. Since the ATPs' output formats are neither documented nor stable, other
|
blanchet@46731
|
202 |
versions of the ATPs might not work well with Sledgehammer. Ideally,
|
blanchet@47113
|
203 |
also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
|
blanchet@47113
|
204 |
\texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
|
blanchet@47113
|
205 |
\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.4'').
|
blanchet@47113
|
206 |
|
blanchet@47113
|
207 |
Similarly, if you want to build CVC3, or found a
|
blanchet@47113
|
208 |
Yices or Z3 executable somewhere (e.g.,
|
blanchet@47113
|
209 |
\url{http://yices.csl.sri.com/download.shtml} or
|
blanchet@47113
|
210 |
\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html}),
|
blanchet@47113
|
211 |
set the environment variable \texttt{CVC3\_\allowbreak SOLVER},
|
blanchet@47113
|
212 |
\texttt{YICES\_SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of
|
blanchet@47113
|
213 |
the executable, \emph{including the file name}. Sledgehammer has been tested
|
blanchet@47113
|
214 |
with CVC3 2.2, Yices 1.0.28, and Z3 3.0 to 3.2.
|
blanchet@47113
|
215 |
Since the SMT solvers' output formats are somewhat unstable, other
|
blanchet@47113
|
216 |
versions of the solvers might not work well with Sledgehammer. Ideally,
|
blanchet@47113
|
217 |
also set \texttt{CVC3\_VERSION}, \texttt{YICES\_VERSION}, or
|
blanchet@47113
|
218 |
\texttt{Z3\_VERSION} to the solver's version number (e.g., ``3.2'').
|
blanchet@36918
|
219 |
\end{enum}
|
blanchet@47113
|
220 |
\end{sloppy}
|
blanchet@36918
|
221 |
|
blanchet@47113
|
222 |
To check whether E, SPASS, Vampire, and/or Z3 are successfully installed, try
|
blanchet@47113
|
223 |
out the example in \S\ref{first-steps}. If the remote versions of any of these
|
blanchet@47113
|
224 |
provers is used (identified by the prefix ``\emph{remote\_\/}''), or if the
|
blanchet@47113
|
225 |
local versions fail to solve the easy goal presented there, something must be
|
blanchet@47113
|
226 |
wrong with the installation.
|
blanchet@36918
|
227 |
|
blanchet@47113
|
228 |
Remote prover invocation requires Perl with the World Wide Web Library
|
blanchet@47113
|
229 |
(\texttt{libwww-perl}) installed. If you must use a proxy server to access the
|
blanchet@47113
|
230 |
Internet, set the \texttt{http\_proxy} environment variable to the proxy, either
|
blanchet@47113
|
231 |
in the environment in which Isabelle is launched or in your
|
blanchet@47113
|
232 |
\texttt{\char`\~/\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few
|
blanchet@47113
|
233 |
examples:
|
blanchet@39388
|
234 |
|
blanchet@39388
|
235 |
\prew
|
blanchet@39389
|
236 |
\texttt{http\_proxy=http://proxy.example.org} \\
|
blanchet@39389
|
237 |
\texttt{http\_proxy=http://proxy.example.org:8080} \\
|
blanchet@39389
|
238 |
\texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org}
|
blanchet@39388
|
239 |
\postw
|
blanchet@37517
|
240 |
|
blanchet@36918
|
241 |
\section{First Steps}
|
blanchet@36918
|
242 |
\label{first-steps}
|
blanchet@36918
|
243 |
|
blanchet@36918
|
244 |
To illustrate Sledgehammer in context, let us start a theory file and
|
blanchet@36918
|
245 |
attempt to prove a simple lemma:
|
blanchet@36918
|
246 |
|
blanchet@36918
|
247 |
\prew
|
blanchet@36918
|
248 |
\textbf{theory}~\textit{Scratch} \\
|
blanchet@36918
|
249 |
\textbf{imports}~\textit{Main} \\
|
blanchet@36918
|
250 |
\textbf{begin} \\[2\smallskipamount]
|
blanchet@36918
|
251 |
%
|
blanchet@43786
|
252 |
\textbf{lemma} ``$[a] = [b] \,\Longrightarrow\, a = b$'' \\
|
blanchet@36918
|
253 |
\textbf{sledgehammer}
|
blanchet@36918
|
254 |
\postw
|
blanchet@36918
|
255 |
|
blanchet@37517
|
256 |
Instead of issuing the \textbf{sledgehammer} command, you can also find
|
blanchet@37517
|
257 |
Sledgehammer in the ``Commands'' submenu of the ``Isabelle'' menu in Proof
|
blanchet@37517
|
258 |
General or press the Emacs key sequence C-c C-a C-s.
|
blanchet@37517
|
259 |
Either way, Sledgehammer produces the following output after a few seconds:
|
blanchet@36918
|
260 |
|
blanchet@36918
|
261 |
\prew
|
blanchet@36918
|
262 |
\slshape
|
blanchet@47113
|
263 |
Sledgehammer: ``\textit{e\/}'' on goal \\
|
blanchet@43786
|
264 |
$[a] = [b] \,\Longrightarrow\, a = b$ \\
|
blanchet@43895
|
265 |
Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]
|
blanchet@43786
|
266 |
%
|
blanchet@47113
|
267 |
Sledgehammer: ``\textit{z3\/}'' on goal \\
|
blanchet@47113
|
268 |
$[a] = [b] \,\Longrightarrow\, a = b$ \\
|
blanchet@47113
|
269 |
Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount]
|
blanchet@47113
|
270 |
%
|
blanchet@47113
|
271 |
Sledgehammer: ``\textit{vampire\/}'' on goal \\
|
blanchet@43786
|
272 |
$[a] = [b] \,\Longrightarrow\, a = b$ \\
|
blanchet@43895
|
273 |
Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
|
blanchet@36918
|
274 |
%
|
blanchet@47113
|
275 |
Sledgehammer: ``\textit{spass\/}'' on goal \\
|
blanchet@43786
|
276 |
$[a] = [b] \,\Longrightarrow\, a = b$ \\
|
blanchet@43895
|
277 |
Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
|
blanchet@36918
|
278 |
%
|
blanchet@47113
|
279 |
Sledgehammer: ``\textit{remote\_waldmeister\/}'' on goal \\
|
blanchet@43851
|
280 |
$[a] = [b] \,\Longrightarrow\, a = b$ \\
|
blanchet@43895
|
281 |
Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
|
blanchet@40254
|
282 |
%
|
blanchet@47113
|
283 |
Sledgehammer: ``\textit{remote\_e\_sine\/}'' on goal \\
|
blanchet@45929
|
284 |
$[a] = [b] \,\Longrightarrow\, a = b$ \\
|
blanchet@47113
|
285 |
Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms).
|
blanchet@36918
|
286 |
\postw
|
blanchet@36918
|
287 |
|
blanchet@45929
|
288 |
Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel.
|
blanchet@43786
|
289 |
Depending on which provers are installed and how many processor cores are
|
blanchet@43786
|
290 |
available, some of the provers might be missing or present with a
|
blanchet@43851
|
291 |
\textit{remote\_} prefix. Waldmeister is run only for unit equational problems,
|
blanchet@43851
|
292 |
where the goal's conclusion is a (universally quantified) equation.
|
blanchet@36918
|
293 |
|
blanchet@46251
|
294 |
For each successful prover, Sledgehammer gives a one-liner proof that uses
|
blanchet@46251
|
295 |
the \textit{metis} or \textit{smt} proof method. Approximate timings are shown
|
blanchet@46251
|
296 |
in parentheses, indicating how fast the call is. You can click the proof to
|
blanchet@46251
|
297 |
insert it into the theory text.
|
blanchet@36918
|
298 |
|
blanchet@43895
|
299 |
In addition, you can ask Sledgehammer for an Isar text proof by passing the
|
blanchet@43752
|
300 |
\textit{isar\_proof} option (\S\ref{output-format}):
|
blanchet@36918
|
301 |
|
blanchet@36918
|
302 |
\prew
|
blanchet@36918
|
303 |
\textbf{sledgehammer} [\textit{isar\_proof}]
|
blanchet@36918
|
304 |
\postw
|
blanchet@36918
|
305 |
|
blanchet@36918
|
306 |
When Isar proof construction is successful, it can yield proofs that are more
|
blanchet@46251
|
307 |
readable and also faster than the \textit{metis} or \textit{smt} one-liners.
|
blanchet@46251
|
308 |
This feature is experimental and is only available for ATPs.
|
blanchet@36918
|
309 |
|
blanchet@37517
|
310 |
\section{Hints}
|
blanchet@37517
|
311 |
\label{hints}
|
blanchet@37517
|
312 |
|
blanchet@43753
|
313 |
This section presents a few hints that should help you get the most out of
|
blanchet@46251
|
314 |
Sledgehammer. Frequently (and infrequently) asked questions are answered in
|
blanchet@46251
|
315 |
\S\ref{frequently-asked-questions}.
|
blanchet@43753
|
316 |
|
blanchet@47113
|
317 |
%\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak}
|
blanchet@47113
|
318 |
\newcommand\point[1]{\subsection{\emph{#1}}}
|
blanchet@43628
|
319 |
|
blanchet@43628
|
320 |
\point{Presimplify the goal}
|
blanchet@43628
|
321 |
|
blanchet@37517
|
322 |
For best results, first simplify your problem by calling \textit{auto} or at
|
blanchet@43786
|
323 |
least \textit{safe} followed by \textit{simp\_all}. The SMT solvers provide
|
blanchet@43786
|
324 |
arithmetic decision procedures, but the ATPs typically do not (or if they do,
|
blanchet@43786
|
325 |
Sledgehammer does not use it yet). Apart from Waldmeister, they are not
|
blanchet@43786
|
326 |
especially good at heavy rewriting, but because they regard equations as
|
blanchet@43786
|
327 |
undirected, they often prove theorems that require the reverse orientation of a
|
blanchet@43786
|
328 |
\textit{simp} rule. Higher-order problems can be tackled, but the success rate
|
blanchet@43786
|
329 |
is better for first-order problems. Hence, you may get better results if you
|
blanchet@43786
|
330 |
first simplify the problem to remove higher-order features.
|
blanchet@37517
|
331 |
|
blanchet@47113
|
332 |
\point{Make sure E, SPASS, Vampire, and Z3 are locally installed}
|
blanchet@43628
|
333 |
|
blanchet@43628
|
334 |
Locally installed provers are faster and more reliable than those running on
|
blanchet@43628
|
335 |
servers. See \S\ref{installation} for details on how to install them.
|
blanchet@43628
|
336 |
|
blanchet@43628
|
337 |
\point{Familiarize yourself with the most important options}
|
blanchet@43628
|
338 |
|
blanchet@43628
|
339 |
Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of
|
blanchet@43628
|
340 |
the options are very specialized, but serious users of the tool should at least
|
blanchet@43628
|
341 |
familiarize themselves with the following options:
|
blanchet@43628
|
342 |
|
blanchet@43628
|
343 |
\begin{enum}
|
blanchet@46387
|
344 |
\item[\labelitemi] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies
|
blanchet@43753
|
345 |
the automatic provers (ATPs and SMT solvers) that should be run whenever
|
blanchet@43753
|
346 |
Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass
|
blanchet@47113
|
347 |
remote\_vampire\/}''). For convenience, you can omit ``\textit{provers}~=''
|
blanchet@43855
|
348 |
and simply write the prover names as a space-separated list (e.g., ``\textit{e
|
blanchet@47113
|
349 |
spass remote\_vampire\/}'').
|
blanchet@43628
|
350 |
|
blanchet@46387
|
351 |
\item[\labelitemi] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
|
blanchet@43753
|
352 |
specifies the maximum number of facts that should be passed to the provers. By
|
blanchet@43753
|
353 |
default, the value is prover-dependent but varies between about 150 and 1000. If
|
blanchet@43753
|
354 |
the provers time out, you can try lowering this value to, say, 100 or 50 and see
|
blanchet@43753
|
355 |
if that helps.
|
blanchet@43628
|
356 |
|
blanchet@46387
|
357 |
\item[\labelitemi] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies
|
blanchet@46251
|
358 |
that Isar proofs should be generated, instead of one-liner \textit{metis} or
|
blanchet@46251
|
359 |
\textit{smt} proofs. The length of the Isar proofs can be controlled by setting
|
blanchet@43753
|
360 |
\textit{isar\_shrink\_factor} (\S\ref{output-format}).
|
blanchet@43879
|
361 |
|
blanchet@46387
|
362 |
\item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
|
blanchet@43879
|
363 |
provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
|
blanchet@43879
|
364 |
asynchronously you should not hesitate to raise this limit to 60 or 120 seconds
|
blanchet@43879
|
365 |
if you are the kind of user who can think clearly while ATPs are active.
|
blanchet@43628
|
366 |
\end{enum}
|
blanchet@43628
|
367 |
|
blanchet@43753
|
368 |
Options can be set globally using \textbf{sledgehammer\_params}
|
blanchet@43851
|
369 |
(\S\ref{command-syntax}). The command also prints the list of all available
|
blanchet@43851
|
370 |
options with their current value. Fact selection can be influenced by specifying
|
blanchet@43851
|
371 |
``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} call
|
blanchet@43851
|
372 |
to ensure that certain facts are included, or simply ``$(\textit{my\_facts})$''
|
blanchet@43851
|
373 |
to force Sledgehammer to run only with $\textit{my\_facts}$.
|
blanchet@43628
|
374 |
|
blanchet@43628
|
375 |
\section{Frequently Asked Questions}
|
blanchet@43628
|
376 |
\label{frequently-asked-questions}
|
blanchet@43628
|
377 |
|
blanchet@43786
|
378 |
This sections answers frequently (and infrequently) asked questions about
|
blanchet@43786
|
379 |
Sledgehammer. It is a good idea to skim over it now even if you don't have any
|
blanchet@43786
|
380 |
questions at this stage. And if you have any further questions not listed here,
|
blanchet@43786
|
381 |
send them to the author at \authoremail.
|
blanchet@43786
|
382 |
|
blanchet@43849
|
383 |
\point{Which facts are passed to the automatic provers?}
|
blanchet@43752
|
384 |
|
blanchet@43849
|
385 |
The relevance filter assigns a score to every available fact (lemma, theorem,
|
blanchet@47128
|
386 |
definition, or axiom) based upon how many constants that fact shares with the
|
blanchet@43849
|
387 |
conjecture. This process iterates to include facts relevant to those just
|
blanchet@43849
|
388 |
accepted, but with a decay factor to ensure termination. The constants are
|
blanchet@43752
|
389 |
weighted to give unusual ones greater significance. The relevance filter copes
|
blanchet@43752
|
390 |
best when the conjecture contains some unusual constants; if all the constants
|
blanchet@43752
|
391 |
are common, it is unable to discriminate among the hundreds of facts that are
|
blanchet@43752
|
392 |
picked up. The relevance filter is also memoryless: It has no information about
|
blanchet@43752
|
393 |
how many times a particular fact has been used in a proof, and it cannot learn.
|
blanchet@43752
|
394 |
|
blanchet@43752
|
395 |
The number of facts included in a problem varies from prover to prover, since
|
blanchet@43849
|
396 |
some provers get overwhelmed more easily than others. You can show the number of
|
blanchet@43752
|
397 |
facts given using the \textit{verbose} option (\S\ref{output-format}) and the
|
blanchet@43752
|
398 |
actual facts using \textit{debug} (\S\ref{output-format}).
|
blanchet@43752
|
399 |
|
blanchet@43752
|
400 |
Sledgehammer is good at finding short proofs combining a handful of existing
|
blanchet@43752
|
401 |
lemmas. If you are looking for longer proofs, you must typically restrict the
|
blanchet@43753
|
402 |
number of facts, by setting the \textit{max\_relevant} option
|
blanchet@44436
|
403 |
(\S\ref{relevance-filter}) to, say, 25 or 50.
|
blanchet@43752
|
404 |
|
blanchet@43837
|
405 |
You can also influence which facts are actually selected in a number of ways. If
|
blanchet@43837
|
406 |
you simply want to ensure that a fact is included, you can specify it using the
|
blanchet@43837
|
407 |
``$(\textit{add}{:}~\textit{my\_facts})$'' syntax. For example:
|
blanchet@43837
|
408 |
%
|
blanchet@43837
|
409 |
\prew
|
blanchet@43837
|
410 |
\textbf{sledgehammer} (\textit{add}: \textit{hd.simps} \textit{tl.simps})
|
blanchet@43837
|
411 |
\postw
|
blanchet@43837
|
412 |
%
|
blanchet@43837
|
413 |
The specified facts then replace the least relevant facts that would otherwise be
|
blanchet@43837
|
414 |
included; the other selected facts remain the same.
|
blanchet@43837
|
415 |
If you want to direct the selection in a particular direction, you can specify
|
blanchet@43837
|
416 |
the facts via \textbf{using}:
|
blanchet@43837
|
417 |
%
|
blanchet@43837
|
418 |
\prew
|
blanchet@43837
|
419 |
\textbf{using} \textit{hd.simps} \textit{tl.simps} \\
|
blanchet@43837
|
420 |
\textbf{sledgehammer}
|
blanchet@43837
|
421 |
\postw
|
blanchet@43837
|
422 |
%
|
blanchet@43837
|
423 |
The facts are then more likely to be selected than otherwise, and if they are
|
blanchet@43837
|
424 |
selected at iteration $j$ they also influence which facts are selected at
|
blanchet@43837
|
425 |
iterations $j + 1$, $j + 2$, etc. To give them even more weight, try
|
blanchet@43837
|
426 |
%
|
blanchet@43837
|
427 |
\prew
|
blanchet@43837
|
428 |
\textbf{using} \textit{hd.simps} \textit{tl.simps} \\
|
blanchet@43837
|
429 |
\textbf{apply}~\textbf{--} \\
|
blanchet@43837
|
430 |
\textbf{sledgehammer}
|
blanchet@43837
|
431 |
\postw
|
blanchet@43837
|
432 |
|
blanchet@47128
|
433 |
\point{Why does Metis fail to reconstruct the proof?}
|
blanchet@47128
|
434 |
|
blanchet@47128
|
435 |
There are many reasons. If Metis runs seemingly forever, that is a sign that the
|
blanchet@47128
|
436 |
proof is too difficult for it. Metis's search is complete, so it should
|
blanchet@47128
|
437 |
eventually find it, but that's little consolation. There are several possible
|
blanchet@47128
|
438 |
solutions:
|
blanchet@47128
|
439 |
|
blanchet@47128
|
440 |
\begin{enum}
|
blanchet@47128
|
441 |
\item[\labelitemi] Try the \textit{isar\_proof} option (\S\ref{output-format}) to
|
blanchet@47128
|
442 |
obtain a step-by-step Isar proof where each step is justified by \textit{metis}.
|
blanchet@47128
|
443 |
Since the steps are fairly small, \textit{metis} is more likely to be able to
|
blanchet@47128
|
444 |
replay them.
|
blanchet@47128
|
445 |
|
blanchet@47128
|
446 |
\item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}. It
|
blanchet@47128
|
447 |
is usually stronger, but you need to either have Z3 available to replay the
|
blanchet@47128
|
448 |
proofs, trust the SMT solver, or use certificates. See the documentation in the
|
blanchet@47128
|
449 |
\emph{SMT} theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}) for details.
|
blanchet@47128
|
450 |
|
blanchet@47128
|
451 |
\item[\labelitemi] Try the \textit{blast} or \textit{auto} proof methods, passing
|
blanchet@47128
|
452 |
the necessary facts via \textbf{unfolding}, \textbf{using}, \textit{intro}{:},
|
blanchet@47128
|
453 |
\textit{elim}{:}, \textit{dest}{:}, or \textit{simp}{:}, as appropriate.
|
blanchet@47128
|
454 |
\end{enum}
|
blanchet@47128
|
455 |
|
blanchet@47128
|
456 |
In some rare cases, \textit{metis} fails fairly quickly, and you get the error
|
blanchet@47128
|
457 |
message
|
blanchet@47128
|
458 |
|
blanchet@47128
|
459 |
\prew
|
blanchet@47128
|
460 |
\slshape
|
blanchet@47128
|
461 |
One-line proof reconstruction failed.
|
blanchet@47128
|
462 |
\postw
|
blanchet@47128
|
463 |
|
blanchet@47128
|
464 |
This message indicates that Sledgehammer determined that the goal is provable,
|
blanchet@47128
|
465 |
but the proof is, for technical reasons, beyond \textit{metis}'s power. You can
|
blanchet@47128
|
466 |
then try again with the \textit{strict} option (\S\ref{problem-encoding}).
|
blanchet@47128
|
467 |
|
blanchet@47128
|
468 |
If the goal is actually unprovable are you did not specify an unsound encoding
|
blanchet@47128
|
469 |
using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are
|
blanchet@47128
|
470 |
strongly encouraged to report this to the author at \authoremail.
|
blanchet@47128
|
471 |
|
blanchet@47113
|
472 |
\point{Why are the generated Isar proofs so ugly/broken?}
|
blanchet@43752
|
473 |
|
blanchet@47128
|
474 |
The current implementation of the Isar proof feature,
|
blanchet@47128
|
475 |
enabled by the \textit{isar\_proof} option (\S\ref{output-format}),
|
blanchet@47128
|
476 |
is highly experimental. Work on a new implementation has begun. There is a large body of
|
blanchet@43752
|
477 |
research into transforming resolution proofs into natural deduction proofs (such
|
blanchet@43752
|
478 |
as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
|
blanchet@43752
|
479 |
set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
|
blanchet@43752
|
480 |
value or to try several provers and keep the nicest-looking proof.
|
blanchet@43752
|
481 |
|
blanchet@47128
|
482 |
\point{How can I tell whether a suggested proof is sound?}
|
blanchet@47128
|
483 |
|
blanchet@47128
|
484 |
Earlier versions of Sledgehammer often suggested unsound proofs---either proofs
|
blanchet@47128
|
485 |
of nontheorems or simply proofs that rely on type-unsound inferences. This
|
blanchet@47128
|
486 |
is a thing of the pass, unless you explicitly specify an unsound encoding
|
blanchet@47128
|
487 |
using \textit{type\_enc} (\S\ref{problem-encoding}).
|
blanchet@47128
|
488 |
%
|
blanchet@47128
|
489 |
Officially, the only form of ``unsoundness'' that lurks in the sound
|
blanchet@47128
|
490 |
encodings is related to missing characteristic theorems of datatypes. For
|
blanchet@47128
|
491 |
example,
|
blanchet@47128
|
492 |
|
blanchet@47128
|
493 |
\prew
|
blanchet@47128
|
494 |
\textbf{lemma}~``$\exists \mathit{xs}.\; \mathit{xs} \neq []$'' \\
|
blanchet@47128
|
495 |
\textbf{sledgehammer} ()
|
blanchet@47128
|
496 |
\postw
|
blanchet@47128
|
497 |
|
blanchet@47128
|
498 |
suggests an argumentless \textit{metis} call that fails. However, the conjecture
|
blanchet@47128
|
499 |
does actually hold, and the \textit{metis} call can be repaired by adding
|
blanchet@47128
|
500 |
\textit{list.distinct}.
|
blanchet@47128
|
501 |
%
|
blanchet@47128
|
502 |
We hope to address this problem in a future version of Isabelle. In the
|
blanchet@47128
|
503 |
meantime, you can avoid it by passing the \textit{strict} option
|
blanchet@47128
|
504 |
(\S\ref{problem-encoding}).
|
blanchet@47128
|
505 |
|
blanchet@47126
|
506 |
\point{What are the \textit{full\_types}, \textit{no\_types}, and
|
blanchet@47126
|
507 |
\textit{mono\_tags} arguments to Metis?}
|
blanchet@43752
|
508 |
|
blanchet@47126
|
509 |
The \textit{metis}~(\textit{full\_types}) proof method
|
blanchet@47126
|
510 |
and its cousin \textit{metis}~(\textit{mono\_tags}) are fully-typed
|
blanchet@44069
|
511 |
version of Metis. It is somewhat slower than \textit{metis}, but the proof
|
blanchet@44069
|
512 |
search is fully typed, and it also includes more powerful rules such as the
|
blanchet@46387
|
513 |
axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in
|
blanchet@44069
|
514 |
higher-order places (e.g., in set comprehensions). The method kicks in
|
blanchet@44069
|
515 |
automatically as a fallback when \textit{metis} fails, and it is sometimes
|
blanchet@44069
|
516 |
generated by Sledgehammer instead of \textit{metis} if the proof obviously
|
blanchet@44069
|
517 |
requires type information or if \textit{metis} failed when Sledgehammer
|
blanchet@44069
|
518 |
preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with
|
blanchet@47126
|
519 |
various options for up to 3 seconds each time to ensure that the generated
|
blanchet@47126
|
520 |
one-line proofs actually work and to display timing information. This can be
|
blanchet@47126
|
521 |
configured using the \textit{preplay\_timeout} option (\S\ref{timeouts}).)
|
blanchet@47126
|
522 |
%
|
blanchet@44070
|
523 |
At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})
|
blanchet@44070
|
524 |
uses no type information at all during the proof search, which is more efficient
|
blanchet@44070
|
525 |
but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally
|
blanchet@44070
|
526 |
generated by Sledgehammer.
|
blanchet@47126
|
527 |
%
|
blanchet@47126
|
528 |
See the \textit{type\_enc} option (\S\ref{problem-encoding}) for details.
|
blanchet@44070
|
529 |
|
blanchet@47126
|
530 |
Incidentally, if you ever see warnings such as
|
blanchet@43752
|
531 |
|
blanchet@43752
|
532 |
\prew
|
blanchet@43848
|
533 |
\slshape
|
blanchet@44069
|
534 |
Metis: Falling back on ``\textit{metis} (\textit{full\_types})''.
|
blanchet@43752
|
535 |
\postw
|
blanchet@43752
|
536 |
|
blanchet@46251
|
537 |
for a successful \textit{metis} proof, you can advantageously pass the
|
blanchet@44069
|
538 |
\textit{full\_types} option to \textit{metis} directly.
|
blanchet@44069
|
539 |
|
blanchet@47194
|
540 |
\point{And what are the \textit{lifting} and \textit{hide\_lams} arguments
|
blanchet@47126
|
541 |
to Metis?}
|
blanchet@47126
|
542 |
|
blanchet@47126
|
543 |
Orthogonally to the encoding of types, it is important to choose an appropriate
|
blanchet@47126
|
544 |
translation of $\lambda$-abstractions. Metis supports three translation schemes,
|
blanchet@47126
|
545 |
in decreasing order of power: Curry combinators (the default),
|
blanchet@47126
|
546 |
$\lambda$-lifting, and a ``hiding'' scheme that disables all reasoning under
|
blanchet@47126
|
547 |
$\lambda$-abstractions. The more powerful schemes also give the automatic
|
blanchet@47126
|
548 |
provers more rope to hang themselves. See the \textit{lam\_trans} option (\S\ref{problem-encoding}) for details.
|
blanchet@47126
|
549 |
|
blanchet@43895
|
550 |
\point{Are generated proofs minimal?}
|
blanchet@43877
|
551 |
|
blanchet@43895
|
552 |
Automatic provers frequently use many more facts than are necessary.
|
blanchet@43895
|
553 |
Sledgehammer inclues a minimization tool that takes a set of facts returned by a
|
blanchet@46251
|
554 |
given prover and repeatedly calls the same prover, \textit{metis}, or
|
blanchet@46251
|
555 |
\textit{smt} with subsets of those axioms in order to find a minimal set.
|
blanchet@46251
|
556 |
Reducing the number of axioms typically improves Metis's speed and success rate,
|
blanchet@46251
|
557 |
while also removing superfluous clutter from the proof scripts.
|
blanchet@43877
|
558 |
|
blanchet@44070
|
559 |
In earlier versions of Sledgehammer, generated proofs were systematically
|
blanchet@44070
|
560 |
accompanied by a suggestion to invoke the minimization tool. This step is now
|
blanchet@44070
|
561 |
performed implicitly if it can be done in a reasonable amount of time (something
|
blanchet@44070
|
562 |
that can be guessed from the number of facts in the original proof and the time
|
blanchet@46579
|
563 |
it took to find or preplay it).
|
blanchet@43877
|
564 |
|
blanchet@46034
|
565 |
In addition, some provers (e.g., Yices) do not provide proofs or sometimes
|
blanchet@46034
|
566 |
produce incomplete proofs. The minimizer is then invoked to find out which facts
|
blanchet@46034
|
567 |
are actually needed from the (large) set of facts that was initinally given to
|
blanchet@46034
|
568 |
the prover. Finally, if a prover returns a proof with lots of facts, the
|
blanchet@46034
|
569 |
minimizer is invoked automatically since Metis would be unlikely to re-find the
|
blanchet@46034
|
570 |
proof.
|
blanchet@46579
|
571 |
%
|
blanchet@46579
|
572 |
Automatic minimization can be forced or disabled using the \textit{minimize}
|
blanchet@46579
|
573 |
option (\S\ref{mode-of-operation}).
|
blanchet@43877
|
574 |
|
blanchet@43849
|
575 |
\point{A strange error occurred---what should I do?}
|
blanchet@43628
|
576 |
|
blanchet@43628
|
577 |
Sledgehammer tries to give informative error messages. Please report any strange
|
blanchet@43752
|
578 |
error to the author at \authoremail. This applies double if you get the message
|
blanchet@43628
|
579 |
|
blanchet@43752
|
580 |
\prew
|
blanchet@43628
|
581 |
\slshape
|
blanchet@47113
|
582 |
The prover found a type-unsound proof involving ``\textit{foo\/}'',
|
blanchet@47113
|
583 |
``\textit{bar\/}'', and ``\textit{baz\/}'' even though a supposedly type-sound
|
blanchet@43846
|
584 |
encoding was used (or, less likely, your axioms are inconsistent). You might
|
blanchet@43846
|
585 |
want to report this to the Isabelle developers.
|
blanchet@43752
|
586 |
\postw
|
blanchet@43628
|
587 |
|
blanchet@43628
|
588 |
\point{Auto can solve it---why not Sledgehammer?}
|
blanchet@43628
|
589 |
|
blanchet@43628
|
590 |
Problems can be easy for \textit{auto} and difficult for automatic provers, but
|
blanchet@43628
|
591 |
the reverse is also true, so don't be discouraged if your first attempts fail.
|
blanchet@39566
|
592 |
Because the system refers to all theorems known to Isabelle, it is particularly
|
blanchet@39566
|
593 |
suitable when your goal has a short proof from lemmas that you don't know about.
|
blanchet@37517
|
594 |
|
blanchet@43752
|
595 |
\point{Why are there so many options?}
|
blanchet@43752
|
596 |
|
blanchet@43752
|
597 |
Sledgehammer's philosophy should work out of the box, without user guidance.
|
blanchet@43752
|
598 |
Many of the options are meant to be used mostly by the Sledgehammer developers
|
blanchet@43752
|
599 |
for experimentation purposes. Of course, feel free to experiment with them if
|
blanchet@43752
|
600 |
you are so inclined.
|
blanchet@43752
|
601 |
|
blanchet@36918
|
602 |
\section{Command Syntax}
|
blanchet@36918
|
603 |
\label{command-syntax}
|
blanchet@36918
|
604 |
|
blanchet@47113
|
605 |
\subsection{Sledgehammer}
|
blanchet@47113
|
606 |
|
blanchet@36918
|
607 |
Sledgehammer can be invoked at any point when there is an open goal by entering
|
blanchet@36918
|
608 |
the \textbf{sledgehammer} command in the theory file. Its general syntax is as
|
blanchet@36918
|
609 |
follows:
|
blanchet@36918
|
610 |
|
blanchet@36918
|
611 |
\prew
|
blanchet@44057
|
612 |
\textbf{sledgehammer} \qty{subcommand}$^?$ \qty{options}$^?$ \qty{facts\_override}$^?$ \qty{num}$^?$
|
blanchet@36918
|
613 |
\postw
|
blanchet@36918
|
614 |
|
blanchet@36918
|
615 |
For convenience, Sledgehammer is also available in the ``Commands'' submenu of
|
blanchet@36918
|
616 |
the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c
|
blanchet@36918
|
617 |
C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with
|
blanchet@36918
|
618 |
no arguments in the theory text.
|
blanchet@36918
|
619 |
|
blanchet@44057
|
620 |
In the general syntax, the \qty{subcommand} may be any of the following:
|
blanchet@36918
|
621 |
|
blanchet@36918
|
622 |
\begin{enum}
|
blanchet@46387
|
623 |
\item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on
|
blanchet@44057
|
624 |
subgoal number \qty{num} (1 by default), with the given options and facts.
|
blanchet@36918
|
625 |
|
blanchet@46387
|
626 |
\item[\labelitemi] \textbf{\textit{min}:} Attempts to minimize the facts
|
blanchet@44057
|
627 |
specified in the \qty{facts\_override} argument to obtain a simpler proof
|
blanchet@36918
|
628 |
involving fewer facts. The options and goal number are as for \textit{run}.
|
blanchet@36918
|
629 |
|
blanchet@46387
|
630 |
\item[\labelitemi] \textbf{\textit{messages}:} Redisplays recent messages issued
|
blanchet@40444
|
631 |
by Sledgehammer. This allows you to examine results that might have been lost
|
blanchet@44057
|
632 |
due to Sledgehammer's asynchronous nature. The \qty{num} argument specifies a
|
blanchet@36918
|
633 |
limit on the number of messages to display (5 by default).
|
blanchet@36918
|
634 |
|
blanchet@46387
|
635 |
\item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of
|
blanchet@42588
|
636 |
automatic provers supported by Sledgehammer. See \S\ref{installation} and
|
blanchet@42588
|
637 |
\S\ref{mode-of-operation} for more information on how to install automatic
|
blanchet@42588
|
638 |
provers.
|
blanchet@36918
|
639 |
|
blanchet@46387
|
640 |
\item[\labelitemi] \textbf{\textit{running\_provers}:} Prints information about
|
blanchet@40240
|
641 |
currently running automatic provers, including elapsed runtime and remaining
|
blanchet@40240
|
642 |
time until timeout.
|
blanchet@36918
|
643 |
|
blanchet@46387
|
644 |
\item[\labelitemi] \textbf{\textit{kill\_provers}:} Terminates all running
|
blanchet@40240
|
645 |
automatic provers.
|
blanchet@36918
|
646 |
|
blanchet@46387
|
647 |
\item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
|
blanchet@36918
|
648 |
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
|
blanchet@36918
|
649 |
\end{enum}
|
blanchet@36918
|
650 |
|
blanchet@44057
|
651 |
Sledgehammer's behavior can be influenced by various \qty{options}, which can be
|
blanchet@44057
|
652 |
specified in brackets after the \textbf{sledgehammer} command. The
|
blanchet@44057
|
653 |
\qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
|
blanchet@47113
|
654 |
\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. For
|
blanchet@36918
|
655 |
example:
|
blanchet@36918
|
656 |
|
blanchet@36918
|
657 |
\prew
|
blanchet@44057
|
658 |
\textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120]
|
blanchet@36918
|
659 |
\postw
|
blanchet@36918
|
660 |
|
blanchet@36918
|
661 |
Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
|
blanchet@36918
|
662 |
|
blanchet@36918
|
663 |
\prew
|
blanchet@44057
|
664 |
\textbf{sledgehammer\_params} \qty{options}
|
blanchet@36918
|
665 |
\postw
|
blanchet@36918
|
666 |
|
blanchet@36918
|
667 |
The supported options are described in \S\ref{option-reference}.
|
blanchet@36918
|
668 |
|
blanchet@44057
|
669 |
The \qty{facts\_override} argument lets you alter the set of facts that go
|
blanchet@44057
|
670 |
through the relevance filter. It may be of the form ``(\qty{facts})'', where
|
blanchet@44057
|
671 |
\qty{facts} is a space-separated list of Isabelle facts (theorems, local
|
blanchet@36918
|
672 |
assumptions, etc.), in which case the relevance filter is bypassed and the given
|
blanchet@44057
|
673 |
facts are used. It may also be of the form ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}})'',
|
blanchet@44057
|
674 |
``(\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', or ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}}\
|
blanchet@44057
|
675 |
\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', where the relevance filter is instructed to
|
blanchet@44057
|
676 |
proceed as usual except that it should consider \qty{facts\/_{\mathrm{1}}}
|
blanchet@44057
|
677 |
highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant.
|
blanchet@36918
|
678 |
|
blanchet@39566
|
679 |
You can instruct Sledgehammer to run automatically on newly entered theorems by
|
blanchet@45607
|
680 |
enabling the ``Auto Sledgehammer'' option in Proof General's ``Isabelle'' menu.
|
blanchet@45607
|
681 |
For automatic runs, only the first prover set using \textit{provers}
|
blanchet@43601
|
682 |
(\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover,
|
blanchet@47128
|
683 |
\textit{slice} (\S\ref{mode-of-operation}) is disabled, \textit{strict}
|
blanchet@44436
|
684 |
(\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format})
|
blanchet@43879
|
685 |
and \textit{debug} (\S\ref{output-format}) are disabled, and \textit{timeout}
|
blanchet@43879
|
686 |
(\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in Proof
|
blanchet@43879
|
687 |
General's ``Isabelle'' menu. Sledgehammer's output is also more concise.
|
blanchet@39566
|
688 |
|
blanchet@47113
|
689 |
\subsection{Metis}
|
blanchet@47113
|
690 |
|
blanchet@44057
|
691 |
The \textit{metis} proof method has the syntax
|
blanchet@44057
|
692 |
|
blanchet@44057
|
693 |
\prew
|
blanchet@46389
|
694 |
\textbf{\textit{metis}}~(\qty{options})${}^?$~\qty{facts}${}^?$
|
blanchet@44057
|
695 |
\postw
|
blanchet@44057
|
696 |
|
blanchet@46389
|
697 |
where \qty{facts} is a list of arbitrary facts and \qty{options} is a
|
blanchet@46389
|
698 |
comma-separated list consisting of at most one $\lambda$ translation scheme
|
blanchet@46389
|
699 |
specification with the same semantics as Sledgehammer's \textit{lam\_trans}
|
blanchet@46389
|
700 |
option (\S\ref{problem-encoding}) and at most one type encoding specification
|
blanchet@46389
|
701 |
with the same semantics as Sledgehammer's \textit{type\_enc} option
|
blanchet@46389
|
702 |
(\S\ref{problem-encoding}).
|
blanchet@46389
|
703 |
%
|
blanchet@46389
|
704 |
The supported $\lambda$ translation schemes are \textit{hide\_lams},
|
blanchet@47194
|
705 |
\textit{lifting}, and \textit{combs} (the default).
|
blanchet@46389
|
706 |
%
|
blanchet@46389
|
707 |
All the untyped type encodings listed in \S\ref{problem-encoding} are supported.
|
blanchet@46389
|
708 |
For convenience, the following aliases are provided:
|
blanchet@46389
|
709 |
\begin{enum}
|
blanchet@47128
|
710 |
\item[\labelitemi] \textbf{\textit{full\_types}:} Synonym for \textit{poly\_guards\_query}.
|
blanchet@46389
|
711 |
\item[\labelitemi] \textbf{\textit{partial\_types}:} Synonym for \textit{poly\_args}.
|
blanchet@46389
|
712 |
\item[\labelitemi] \textbf{\textit{no\_types}:} Synonym for \textit{erased}.
|
blanchet@46389
|
713 |
\end{enum}
|
blanchet@44057
|
714 |
|
blanchet@36918
|
715 |
\section{Option Reference}
|
blanchet@36918
|
716 |
\label{option-reference}
|
blanchet@36918
|
717 |
|
blanchet@43855
|
718 |
\def\defl{\{}
|
blanchet@43855
|
719 |
\def\defr{\}}
|
blanchet@43855
|
720 |
|
blanchet@36918
|
721 |
\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
|
blanchet@43855
|
722 |
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
|
blanchet@43855
|
723 |
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
|
blanchet@43855
|
724 |
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
|
blanchet@36918
|
725 |
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
|
blanchet@43855
|
726 |
\def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]}
|
blanchet@43855
|
727 |
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]}
|
blanchet@36918
|
728 |
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
|
blanchet@36918
|
729 |
\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
|
blanchet@43855
|
730 |
\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
|
blanchet@36918
|
731 |
|
blanchet@36918
|
732 |
Sledgehammer's options are categorized as follows:\ mode of operation
|
blanchet@39228
|
733 |
(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),
|
blanchet@39228
|
734 |
relevance filter (\S\ref{relevance-filter}), output format
|
blanchet@43879
|
735 |
(\S\ref{output-format}), authentication (\S\ref{authentication}), and timeouts
|
blanchet@43879
|
736 |
(\S\ref{timeouts}).
|
blanchet@36918
|
737 |
|
blanchet@36918
|
738 |
The descriptions below refer to the following syntactic quantities:
|
blanchet@36918
|
739 |
|
blanchet@36918
|
740 |
\begin{enum}
|
blanchet@46387
|
741 |
\item[\labelitemi] \qtybf{string}: A string.
|
blanchet@46387
|
742 |
\item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}.
|
blanchet@46387
|
743 |
\item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or
|
blanchet@40444
|
744 |
\textit{smart}.
|
blanchet@46387
|
745 |
\item[\labelitemi] \qtybf{int\/}: An integer.
|
blanchet@46387
|
746 |
%\item[\labelitemi] \qtybf{float\/}: A floating-point number (e.g., 2.5).
|
blanchet@46387
|
747 |
\item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers
|
blanchet@40584
|
748 |
(e.g., 0.6 0.95).
|
blanchet@46387
|
749 |
\item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}.
|
blanchet@46387
|
750 |
\item[\labelitemi] \qtybf{float\_or\_none\/}: A floating-point number (e.g., 60 or
|
blanchet@43877
|
751 |
0.5) expressing a number of seconds, or the keyword \textit{none} ($\infty$
|
blanchet@43877
|
752 |
seconds).
|
blanchet@36918
|
753 |
\end{enum}
|
blanchet@36918
|
754 |
|
blanchet@44058
|
755 |
Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
|
blanchet@44058
|
756 |
have a negated counterpart (e.g., \textit{blocking} vs.\
|
blanchet@47113
|
757 |
\textit{non\_blocking}). When setting them, ``= \textit{true\/}'' may be omitted.
|
blanchet@36918
|
758 |
|
blanchet@36918
|
759 |
\subsection{Mode of Operation}
|
blanchet@36918
|
760 |
\label{mode-of-operation}
|
blanchet@36918
|
761 |
|
blanchet@36918
|
762 |
\begin{enum}
|
blanchet@43855
|
763 |
\opnodefaultbrk{provers}{string}
|
blanchet@40240
|
764 |
Specifies the automatic provers to use as a space-separated list (e.g.,
|
blanchet@47127
|
765 |
``\textit{e}~\textit{spass}~\textit{remote\_vampire\/}'').
|
blanchet@47127
|
766 |
Provers can be run locally or remotely; see \S\ref{installation} for
|
blanchet@47127
|
767 |
installation instructions.
|
blanchet@47127
|
768 |
|
blanchet@47127
|
769 |
The following local provers are supported:
|
blanchet@36918
|
770 |
|
blanchet@36918
|
771 |
\begin{enum}
|
blanchet@46387
|
772 |
\item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
|
blanchet@43786
|
773 |
Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
|
blanchet@43786
|
774 |
set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
|
blanchet@47113
|
775 |
executable, including the file name, or install the prebuilt CVC3 package from
|
blanchet@47127
|
776 |
\download. Sledgehammer has been tested with version 2.2.
|
blanchet@43786
|
777 |
|
blanchet@46387
|
778 |
\item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
|
blanchet@43805
|
779 |
developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment
|
blanchet@43805
|
780 |
variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
|
blanchet@47113
|
781 |
executable, or install the prebuilt E package from \download. Sledgehammer has
|
blanchet@47127
|
782 |
been tested with versions 1.0 to 1.4.
|
blanchet@36918
|
783 |
|
blanchet@46387
|
784 |
\item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
|
blanchet@44969
|
785 |
higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
|
blanchet@47113
|
786 |
with support for the TPTP typed higher-order syntax (THF0). To use LEO-II, set
|
blanchet@47113
|
787 |
the environment variable \texttt{LEO2\_HOME} to the directory that contains the
|
blanchet@47113
|
788 |
\texttt{leo} executable. Sledgehammer requires version 1.2.9 or above.
|
blanchet@44969
|
789 |
|
blanchet@46387
|
790 |
\item[\labelitemi] \textbf{\textit{metis}:} Although it is much less powerful than
|
blanchet@44969
|
791 |
the external provers, Metis itself can be used for proof search.
|
blanchet@44969
|
792 |
|
blanchet@46387
|
793 |
\item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
|
blanchet@44969
|
794 |
higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
|
blanchet@47113
|
795 |
support for the TPTP typed higher-order syntax (THF0). To use Satallax, set the
|
blanchet@47113
|
796 |
environment variable \texttt{SATALLAX\_HOME} to the directory that contains the
|
blanchet@47113
|
797 |
\texttt{satallax} executable. Sledgehammer requires version 2.2 or above.
|
blanchet@44969
|
798 |
|
blanchet@46387
|
799 |
\item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt} proof method with the
|
blanchet@46426
|
800 |
current settings (usually:\ Z3 with proof reconstruction).
|
blanchet@46251
|
801 |
|
blanchet@46387
|
802 |
\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
|
blanchet@43805
|
803 |
prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
|
blanchet@43805
|
804 |
To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
|
blanchet@43805
|
805 |
that contains the \texttt{SPASS} executable, or install the prebuilt SPASS
|
blanchet@47127
|
806 |
package from \download. Sledgehammer requires version 3.5 or above.
|
blanchet@36918
|
807 |
|
blanchet@46387
|
808 |
\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution
|
blanchet@43805
|
809 |
prover developed by Andrei Voronkov and his colleagues
|
blanchet@43805
|
810 |
\cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
|
blanchet@43805
|
811 |
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
|
blanchet@45278
|
812 |
executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``1.8'').
|
blanchet@47113
|
813 |
Sledgehammer has been tested with versions 0.6, 1.0, and 1.8.
|
blanchet@47113
|
814 |
%Vampire 1.8 supports the TPTP typed first-order format (TFF0).
|
blanchet@36918
|
815 |
|
blanchet@46387
|
816 |
\item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at
|
blanchet@44969
|
817 |
SRI \cite{yices}. To use Yices, set the environment variable
|
blanchet@44969
|
818 |
\texttt{YICES\_SOLVER} to the complete path of the executable, including the
|
blanchet@46731
|
819 |
file name. Sledgehammer has been tested with version 1.0.28.
|
blanchet@44969
|
820 |
|
blanchet@46387
|
821 |
\item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
|
blanchet@42611
|
822 |
Microsoft Research \cite{z3}. To use Z3, set the environment variable
|
blanchet@42611
|
823 |
\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
|
blanchet@45280
|
824 |
name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
|
blanchet@46731
|
825 |
noncommercial user. Sledgehammer has been tested with versions 3.0 to 3.2.
|
blanchet@42611
|
826 |
|
blanchet@46387
|
827 |
\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
|
blanchet@46387
|
828 |
an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
|
blanchet@46731
|
829 |
formats (FOF and TFF0). It is included for experimental purposes. It
|
blanchet@46731
|
830 |
requires version 3.0 or above. To use it, set the environment variable
|
blanchet@46731
|
831 |
\texttt{Z3\_HOME} to the directory that contains the \texttt{z3}
|
blanchet@46731
|
832 |
executable.
|
blanchet@43786
|
833 |
\end{enum}
|
blanchet@43786
|
834 |
|
blanchet@47127
|
835 |
The following remote provers are supported:
|
blanchet@43786
|
836 |
|
blanchet@43786
|
837 |
\begin{enum}
|
blanchet@46387
|
838 |
\item[\labelitemi] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
|
blanchet@43786
|
839 |
on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
|
blanchet@43786
|
840 |
point).
|
blanchet@40254
|
841 |
|
blanchet@46387
|
842 |
\item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs
|
blanchet@36918
|
843 |
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
|
blanchet@36918
|
844 |
|
blanchet@46387
|
845 |
\item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover
|
blanchet@44962
|
846 |
developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
|
blanchet@44962
|
847 |
SInE runs on Geoff Sutcliffe's Miami servers.
|
blanchet@44962
|
848 |
|
blanchet@46387
|
849 |
\item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
|
blanchet@44962
|
850 |
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
|
blanchet@46387
|
851 |
servers. This ATP supports the TPTP typed first-order format (TFF0). The
|
blanchet@44962
|
852 |
remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
|
blanchet@44962
|
853 |
|
blanchet@46387
|
854 |
\item[\labelitemi] \textbf{\textit{remote\_iprover}:} iProver is a pure
|
blanchet@46210
|
855 |
instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. The
|
blanchet@46210
|
856 |
remote version of iProver runs on Geoff Sutcliffe's Miami servers
|
blanchet@46210
|
857 |
\cite{sutcliffe-2000}.
|
blanchet@46210
|
858 |
|
blanchet@46387
|
859 |
\item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} iProver-Eq is an
|
blanchet@46210
|
860 |
instantiation-based prover with native support for equality developed by
|
blanchet@46210
|
861 |
Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. The
|
blanchet@46210
|
862 |
remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers
|
blanchet@46210
|
863 |
\cite{sutcliffe-2000}.
|
blanchet@46210
|
864 |
|
blanchet@46210
|
865 |
The remote version of LEO-II
|
blanchet@46210
|
866 |
runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
|
blanchet@46210
|
867 |
|
blanchet@46387
|
868 |
\item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
|
blanchet@44969
|
869 |
runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
|
blanchet@43805
|
870 |
|
blanchet@46387
|
871 |
\item[\labelitemi] \textbf{\textit{remote\_satallax}:} The remote version of
|
blanchet@44969
|
872 |
Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
|
blanchet@43805
|
873 |
|
blanchet@46387
|
874 |
\item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a first-order
|
blanchet@44492
|
875 |
resolution prover developed by Stickel et al.\ \cite{snark}. It supports the
|
blanchet@46387
|
876 |
TPTP typed first-order format (TFF0). The remote version of SNARK runs on
|
blanchet@44492
|
877 |
Geoff Sutcliffe's Miami servers.
|
blanchet@40254
|
878 |
|
blanchet@46387
|
879 |
\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
|
blanchet@45278
|
880 |
Vampire runs on Geoff Sutcliffe's Miami servers. Version 1.8 is used.
|
blanchet@43786
|
881 |
|
blanchet@46387
|
882 |
\item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
|
blanchet@43786
|
883 |
equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be
|
blanchet@44492
|
884 |
used to prove universally quantified equations using unconditional equations,
|
blanchet@44492
|
885 |
corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister
|
blanchet@44492
|
886 |
runs on Geoff Sutcliffe's Miami servers.
|
blanchet@42609
|
887 |
|
blanchet@46387
|
888 |
\item[\labelitemi] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
|
blanchet@41190
|
889 |
servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
|
blanchet@41190
|
890 |
point).
|
blanchet@40254
|
891 |
|
blanchet@46387
|
892 |
\item[\labelitemi] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3
|
blanchet@45282
|
893 |
with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
|
blanchet@36918
|
894 |
\end{enum}
|
blanchet@36918
|
895 |
|
blanchet@45929
|
896 |
By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever
|
blanchet@44962
|
897 |
the SMT module's \textit{smt\_solver} configuration option is set to), and (if
|
blanchet@44962
|
898 |
appropriate) Waldmeister in parallel---either locally or remotely, depending on
|
blanchet@44962
|
899 |
the number of processor cores available. For historical reasons, the default
|
blanchet@44962
|
900 |
value of this option can be overridden using the option ``Sledgehammer:
|
blanchet@45607
|
901 |
Provers'' in Proof General's ``Isabelle'' menu.
|
blanchet@36918
|
902 |
|
blanchet@45607
|
903 |
It is generally a good idea to run several provers in parallel. Running E,
|
blanchet@45607
|
904 |
SPASS, and Vampire for 5~seconds yields a similar success rate to running the
|
blanchet@45607
|
905 |
most effective of these for 120~seconds \cite{boehme-nipkow-2010}.
|
blanchet@40240
|
906 |
|
blanchet@43894
|
907 |
For the \textit{min} subcommand, the default prover is \textit{metis}. If
|
blanchet@43894
|
908 |
several provers are set, the first one is used.
|
blanchet@43894
|
909 |
|
blanchet@40240
|
910 |
\opnodefault{prover}{string}
|
blanchet@40240
|
911 |
Alias for \textit{provers}.
|
blanchet@40240
|
912 |
|
blanchet@43753
|
913 |
%\opnodefault{atps}{string}
|
blanchet@43753
|
914 |
%Legacy alias for \textit{provers}.
|
blanchet@36918
|
915 |
|
blanchet@43753
|
916 |
%\opnodefault{atp}{string}
|
blanchet@43753
|
917 |
%Legacy alias for \textit{provers}.
|
blanchet@36918
|
918 |
|
blanchet@39227
|
919 |
\opfalse{blocking}{non\_blocking}
|
blanchet@39227
|
920 |
Specifies whether the \textbf{sledgehammer} command should operate
|
blanchet@39227
|
921 |
synchronously. The asynchronous (non-blocking) mode lets the user start proving
|
blanchet@39227
|
922 |
the putative theorem manually while Sledgehammer looks for a proof, but it can
|
blanchet@43836
|
923 |
also be more confusing. Irrespective of the value of this option, Sledgehammer
|
blanchet@43836
|
924 |
is always run synchronously for the new jEdit-based user interface or if
|
blanchet@43836
|
925 |
\textit{debug} (\S\ref{output-format}) is enabled.
|
blanchet@39227
|
926 |
|
blanchet@46579
|
927 |
\optrue{slice}{dont\_slice}
|
blanchet@43314
|
928 |
Specifies whether the time allocated to a prover should be sliced into several
|
blanchet@43314
|
929 |
segments, each of which has its own set of possibly prover-dependent options.
|
blanchet@43317
|
930 |
For SPASS and Vampire, the first slice tries the fast but incomplete
|
blanchet@43314
|
931 |
set-of-support (SOS) strategy, whereas the second slice runs without it. For E,
|
blanchet@43317
|
932 |
up to three slices are tried, with different weighted search strategies and
|
blanchet@43314
|
933 |
number of facts. For SMT solvers, several slices are tried with the same options
|
blanchet@43317
|
934 |
each time but fewer and fewer facts. According to benchmarks with a timeout of
|
blanchet@43317
|
935 |
30 seconds, slicing is a valuable optimization, and you should probably leave it
|
blanchet@43317
|
936 |
enabled unless you are conducting experiments. This option is implicitly
|
blanchet@43314
|
937 |
disabled for (short) automatic runs.
|
blanchet@43314
|
938 |
|
blanchet@43314
|
939 |
\nopagebreak
|
blanchet@43314
|
940 |
{\small See also \textit{verbose} (\S\ref{output-format}).}
|
blanchet@43314
|
941 |
|
blanchet@46579
|
942 |
\opsmart{minimize}{dont\_minimize}
|
blanchet@46579
|
943 |
Specifies whether the minimization tool should be invoked automatically after
|
blanchet@46579
|
944 |
proof search. By default, automatic minimization takes place only if
|
blanchet@46579
|
945 |
it can be done in a reasonable amount of time (as determined by
|
blanchet@46579
|
946 |
the number of facts in the original proof and the time it took to find or
|
blanchet@46579
|
947 |
preplay it) or the proof involves an unreasonably large number of facts.
|
blanchet@46579
|
948 |
|
blanchet@46579
|
949 |
\nopagebreak
|
blanchet@46579
|
950 |
{\small See also \textit{preplay\_timeout} (\S\ref{timeouts}).}
|
blanchet@46579
|
951 |
|
blanchet@36918
|
952 |
\opfalse{overlord}{no\_overlord}
|
blanchet@36918
|
953 |
Specifies whether Sledgehammer should put its temporary files in
|
blanchet@36918
|
954 |
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
|
blanchet@36918
|
955 |
debugging Sledgehammer but also unsafe if several instances of the tool are run
|
blanchet@36918
|
956 |
simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
|
blanchet@36918
|
957 |
safely remove them after Sledgehammer has run.
|
blanchet@36918
|
958 |
|
blanchet@36918
|
959 |
\nopagebreak
|
blanchet@36918
|
960 |
{\small See also \textit{debug} (\S\ref{output-format}).}
|
blanchet@36918
|
961 |
\end{enum}
|
blanchet@36918
|
962 |
|
blanchet@36918
|
963 |
\subsection{Problem Encoding}
|
blanchet@36918
|
964 |
\label{problem-encoding}
|
blanchet@36918
|
965 |
|
blanchet@46387
|
966 |
\newcommand\comb[1]{\const{#1}}
|
blanchet@46387
|
967 |
|
blanchet@36918
|
968 |
\begin{enum}
|
blanchet@46387
|
969 |
\opdefault{lam\_trans}{string}{smart}
|
blanchet@46387
|
970 |
Specifies the $\lambda$ translation scheme to use in ATP problems. The supported
|
blanchet@46387
|
971 |
translation schemes are listed below:
|
blanchet@46387
|
972 |
|
blanchet@46387
|
973 |
\begin{enum}
|
blanchet@46387
|
974 |
\item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$-abstractions
|
blanchet@46387
|
975 |
by replacing them by unspecified fresh constants, effectively disabling all
|
blanchet@46387
|
976 |
reasoning under $\lambda$-abstractions.
|
blanchet@46387
|
977 |
|
blanchet@47194
|
978 |
\item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new
|
blanchet@46387
|
979 |
supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions,
|
blanchet@46387
|
980 |
defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting).
|
blanchet@46387
|
981 |
|
blanchet@47194
|
982 |
\item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry
|
blanchet@46387
|
983 |
combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators
|
blanchet@46387
|
984 |
enable the ATPs to synthesize $\lambda$-terms but tend to yield bulkier formulas
|
blanchet@46387
|
985 |
than $\lambda$-lifting: The translation is quadratic in the worst case, and the
|
blanchet@46387
|
986 |
equational definitions of the combinators are very prolific in the context of
|
blanchet@46387
|
987 |
resolution.
|
blanchet@46387
|
988 |
|
blanchet@47194
|
989 |
\item[\labelitemi] \textbf{\textit{combs\_and\_lifting}:} Introduce a new
|
blanchet@46387
|
990 |
supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a
|
blanchet@46387
|
991 |
lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators.
|
blanchet@46387
|
992 |
|
blanchet@47194
|
993 |
\item[\labelitemi] \textbf{\textit{combs\_or\_lifting}:} For each cluster of
|
blanchet@47194
|
994 |
$\lambda$-abstractions, heuristically choose between $\lambda$-lifting and Curry
|
blanchet@47194
|
995 |
combinators.
|
blanchet@47194
|
996 |
|
blanchet@46387
|
997 |
\item[\labelitemi] \textbf{\textit{keep\_lams}:}
|
blanchet@46387
|
998 |
Keep the $\lambda$-abstractions in the generated problems. This is available
|
blanchet@46387
|
999 |
only with provers that support the THF0 syntax.
|
blanchet@46387
|
1000 |
|
blanchet@46387
|
1001 |
\item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used
|
blanchet@46387
|
1002 |
depends on the ATP and should be the most efficient scheme for that ATP.
|
blanchet@46387
|
1003 |
\end{enum}
|
blanchet@46387
|
1004 |
|
blanchet@47194
|
1005 |
For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting},
|
blanchet@47194
|
1006 |
irrespective of the value of this option.
|
blanchet@46387
|
1007 |
|
blanchet@44494
|
1008 |
\opdefault{type\_enc}{string}{smart}
|
blanchet@44494
|
1009 |
Specifies the type encoding to use in ATP problems. Some of the type encodings
|
blanchet@44494
|
1010 |
are unsound, meaning that they can give rise to spurious proofs
|
blanchet@46251
|
1011 |
(unreconstructible using \textit{metis}). The supported type encodings are
|
blanchet@47128
|
1012 |
listed below, with an indication of their soundness in parentheses.
|
blanchet@47130
|
1013 |
An asterisk (*) means that the encoding is slightly incomplete for
|
blanchet@47130
|
1014 |
reconstruction with \textit{metis}, unless the \emph{strict} option (described
|
blanchet@47130
|
1015 |
below) is enabled.
|
blanchet@43089
|
1016 |
|
blanchet@43089
|
1017 |
\begin{enum}
|
blanchet@46387
|
1018 |
\item[\labelitemi] \textbf{\textit{erased} (very unsound):} No type information is
|
blanchet@47128
|
1019 |
supplied to the ATP, not even to resolve overloading. Types are simply erased.
|
blanchet@43453
|
1020 |
|
blanchet@46387
|
1021 |
\item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using
|
blanchet@47128
|
1022 |
a predicate \const{g}$(\tau, t)$ that guards bound
|
blanchet@44861
|
1023 |
variables. Constants are annotated with their types, supplied as additional
|
blanchet@43756
|
1024 |
arguments, to resolve overloading.
|
blanchet@43555
|
1025 |
|
blanchet@46387
|
1026 |
\item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
|
blanchet@47128
|
1027 |
tagged with its type using a function $\const{t\/}(\tau, t)$.
|
blanchet@43756
|
1028 |
|
blanchet@46387
|
1029 |
\item[\labelitemi] \textbf{\textit{poly\_args} (unsound):}
|
blanchet@44861
|
1030 |
Like for \textit{poly\_guards} constants are annotated with their types to
|
blanchet@43843
|
1031 |
resolve overloading, but otherwise no type information is encoded. This
|
blanchet@44069
|
1032 |
coincides with the default encoding used by the \textit{metis} command.
|
blanchet@43555
|
1033 |
|
blanchet@46387
|
1034 |
\item[\labelitemi]
|
blanchet@43587
|
1035 |
\textbf{%
|
blanchet@45349
|
1036 |
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\
|
blanchet@45349
|
1037 |
\textit{raw\_mono\_args} (unsound):} \\
|
blanchet@44861
|
1038 |
Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args},
|
blanchet@43587
|
1039 |
respectively, but the problem is additionally monomorphized, meaning that type
|
blanchet@43587
|
1040 |
variables are instantiated with heuristically chosen ground types.
|
blanchet@43587
|
1041 |
Monomorphization can simplify reasoning but also leads to larger fact bases,
|
blanchet@43587
|
1042 |
which can slow down the ATPs.
|
blanchet@43453
|
1043 |
|
blanchet@46387
|
1044 |
\item[\labelitemi]
|
blanchet@43587
|
1045 |
\textbf{%
|
blanchet@45349
|
1046 |
\textit{mono\_guards}, \textit{mono\_tags} (sound);
|
blanchet@45349
|
1047 |
\textit{mono\_args} (unsound):} \\
|
blanchet@43587
|
1048 |
Similar to
|
blanchet@45349
|
1049 |
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and
|
blanchet@45349
|
1050 |
\textit{raw\_mono\_args}, respectively but types are mangled in constant names
|
blanchet@45349
|
1051 |
instead of being supplied as ground term arguments. The binary predicate
|
blanchet@47128
|
1052 |
$\const{g}(\tau, t)$ becomes a unary predicate
|
blanchet@47128
|
1053 |
$\const{g\_}\tau(t)$, and the binary function
|
blanchet@47128
|
1054 |
$\const{t}(\tau, t)$ becomes a unary function
|
blanchet@47128
|
1055 |
$\const{t\_}\tau(t)$.
|
blanchet@43453
|
1056 |
|
blanchet@46387
|
1057 |
\item[\labelitemi] \textbf{\textit{mono\_simple} (sound):} Exploits simple
|
blanchet@45607
|
1058 |
first-order types if the prover supports the TFF0 or THF0 syntax; otherwise,
|
blanchet@45640
|
1059 |
falls back on \textit{mono\_guards}. The problem is monomorphized.
|
blanchet@44492
|
1060 |
|
blanchet@46387
|
1061 |
\item[\labelitemi] \textbf{\textit{mono\_simple\_higher} (sound):} Exploits simple
|
blanchet@45607
|
1062 |
higher-order types if the prover supports the THF0 syntax; otherwise, falls back
|
blanchet@45640
|
1063 |
on \textit{mono\_simple} or \textit{mono\_guards}. The problem is monomorphized.
|
blanchet@43551
|
1064 |
|
blanchet@46387
|
1065 |
\item[\labelitemi]
|
blanchet@43551
|
1066 |
\textbf{%
|
blanchet@45349
|
1067 |
\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\
|
blanchet@45349
|
1068 |
\textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
|
blanchet@47128
|
1069 |
\textit{mono\_simple}? (sound*):} \\
|
blanchet@44861
|
1070 |
The type encodings \textit{poly\_guards}, \textit{poly\_tags},
|
blanchet@45349
|
1071 |
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
|
blanchet@45607
|
1072 |
\textit{mono\_tags}, and \textit{mono\_simple} are fully
|
blanchet@44492
|
1073 |
typed and sound. For each of these, Sledgehammer also provides a lighter,
|
blanchet@45678
|
1074 |
virtually sound variant identified by a question mark (`\hbox{?}')\ that detects
|
blanchet@45678
|
1075 |
and erases monotonic types, notably infinite types. (For \textit{mono\_simple},
|
blanchet@45678
|
1076 |
the types are not actually erased but rather replaced by a shared uniform type
|
blanchet@45678
|
1077 |
of individuals.) As argument to the \textit{metis} proof method, the question
|
blanchet@47128
|
1078 |
mark is replaced by a \hbox{``\textit{\_query\/}''} suffix.
|
blanchet@43460
|
1079 |
|
blanchet@46387
|
1080 |
\item[\labelitemi]
|
blanchet@43756
|
1081 |
\textbf{%
|
blanchet@45640
|
1082 |
\textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\
|
blanchet@45640
|
1083 |
\textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\
|
blanchet@47128
|
1084 |
(sound*):} \\
|
blanchet@45678
|
1085 |
Even lighter versions of the `\hbox{?}' encodings. As argument to the
|
blanchet@45678
|
1086 |
\textit{metis} proof method, the `\hbox{??}' suffix is replaced by
|
blanchet@47113
|
1087 |
\hbox{``\textit{\_query\_query\/}''}.
|
blanchet@45678
|
1088 |
|
blanchet@46387
|
1089 |
\item[\labelitemi]
|
blanchet@45678
|
1090 |
\textbf{%
|
blanchet@47128
|
1091 |
\textit{poly\_guards}@?, \textit{raw\_mono\_guards}@? (sound*):} \\
|
blanchet@45678
|
1092 |
Alternative versions of the `\hbox{??}' encodings. As argument to the
|
blanchet@45678
|
1093 |
\textit{metis} proof method, the `\hbox{@?}' suffix is replaced by
|
blanchet@47113
|
1094 |
\hbox{``\textit{\_at\_query\/}''}.
|
blanchet@45640
|
1095 |
|
blanchet@46387
|
1096 |
\item[\labelitemi]
|
blanchet@45640
|
1097 |
\textbf{%
|
blanchet@45349
|
1098 |
\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
|
blanchet@45607
|
1099 |
\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
|
blanchet@45607
|
1100 |
\textit{mono\_simple}!, \textit{mono\_simple\_higher}! (mildly unsound):} \\
|
blanchet@44861
|
1101 |
The type encodings \textit{poly\_guards}, \textit{poly\_tags},
|
blanchet@45349
|
1102 |
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
|
blanchet@45607
|
1103 |
\textit{mono\_tags}, \textit{mono\_simple}, and \textit{mono\_simple\_higher}
|
blanchet@45607
|
1104 |
also admit a mildly unsound (but very efficient) variant identified by an
|
blanchet@45678
|
1105 |
exclamation mark (`\hbox{!}') that detects and erases erases all types except
|
blanchet@45678
|
1106 |
those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple}
|
blanchet@45678
|
1107 |
and \textit{mono\_simple\_higher}, the types are not actually erased but rather
|
blanchet@45607
|
1108 |
replaced by a shared uniform type of individuals.) As argument to the
|
blanchet@45607
|
1109 |
\textit{metis} proof method, the exclamation mark is replaced by the suffix
|
blanchet@47113
|
1110 |
\hbox{``\textit{\_bang\/}''}.
|
blanchet@43756
|
1111 |
|
blanchet@46387
|
1112 |
\item[\labelitemi]
|
blanchet@45640
|
1113 |
\textbf{%
|
blanchet@45640
|
1114 |
\textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\
|
blanchet@45640
|
1115 |
\textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\
|
blanchet@45640
|
1116 |
(mildly unsound):} \\
|
blanchet@45678
|
1117 |
Even lighter versions of the `\hbox{!}' encodings. As argument to the
|
blanchet@45678
|
1118 |
\textit{metis} proof method, the `\hbox{!!}' suffix is replaced by
|
blanchet@47113
|
1119 |
\hbox{``\textit{\_bang\_bang\/}''}.
|
blanchet@45678
|
1120 |
|
blanchet@46387
|
1121 |
\item[\labelitemi]
|
blanchet@45678
|
1122 |
\textbf{%
|
blanchet@46821
|
1123 |
\textit{poly\_guards}@!, \textit{raw\_mono\_guards}@! (mildly unsound):} \\
|
blanchet@45678
|
1124 |
Alternative versions of the `\hbox{!!}' encodings. As argument to the
|
blanchet@45678
|
1125 |
\textit{metis} proof method, the `\hbox{@!}' suffix is replaced by
|
blanchet@47113
|
1126 |
\hbox{``\textit{\_at\_bang\/}''}.
|
blanchet@45640
|
1127 |
|
blanchet@46387
|
1128 |
\item[\labelitemi] \textbf{\textit{smart}:} The actual encoding used depends on
|
blanchet@44433
|
1129 |
the ATP and should be the most efficient virtually sound encoding for that ATP.
|
blanchet@43089
|
1130 |
\end{enum}
|
blanchet@43089
|
1131 |
|
blanchet@45607
|
1132 |
For SMT solvers, the type encoding is always \textit{mono\_simple}, irrespective
|
blanchet@45607
|
1133 |
of the value of this option.
|
blanchet@43757
|
1134 |
|
blanchet@43757
|
1135 |
\nopagebreak
|
blanchet@43757
|
1136 |
{\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
|
blanchet@43757
|
1137 |
and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).}
|
blanchet@44436
|
1138 |
|
blanchet@47130
|
1139 |
\opfalse{strict}{non\_strict}
|
blanchet@47128
|
1140 |
Specifies whether Sledgehammer should run in its strict mode. In that mode,
|
blanchet@47130
|
1141 |
sound type encodings marked with an asterisk (*) above are made complete
|
blanchet@47128
|
1142 |
for reconstruction with \textit{metis}, at the cost of some clutter in the
|
blanchet@47128
|
1143 |
generated problems. This option has no effect if \textit{type\_enc} is
|
blanchet@47128
|
1144 |
deliberately set to an unsound encoding.
|
blanchet@38814
|
1145 |
\end{enum}
|
blanchet@36918
|
1146 |
|
blanchet@38814
|
1147 |
\subsection{Relevance Filter}
|
blanchet@38814
|
1148 |
\label{relevance-filter}
|
blanchet@38814
|
1149 |
|
blanchet@38814
|
1150 |
\begin{enum}
|
blanchet@40584
|
1151 |
\opdefault{relevance\_thresholds}{float\_pair}{\upshape 0.45~0.85}
|
blanchet@38985
|
1152 |
Specifies the thresholds above which facts are considered relevant by the
|
blanchet@38985
|
1153 |
relevance filter. The first threshold is used for the first iteration of the
|
blanchet@38985
|
1154 |
relevance filter and the second threshold is used for the last iteration (if it
|
blanchet@38985
|
1155 |
is reached). The effective threshold is quadratically interpolated for the other
|
blanchet@40584
|
1156 |
iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
|
blanchet@40584
|
1157 |
are relevant and 1 only theorems that refer to previously seen constants.
|
blanchet@36918
|
1158 |
|
blanchet@43906
|
1159 |
\opdefault{max\_relevant}{smart\_int}{smart}
|
blanchet@38985
|
1160 |
Specifies the maximum number of facts that may be returned by the relevance
|
blanchet@38985
|
1161 |
filter. If the option is set to \textit{smart}, it is set to a value that was
|
blanchet@40240
|
1162 |
empirically found to be appropriate for the prover. A typical value would be
|
blanchet@43906
|
1163 |
250.
|
blanchet@43051
|
1164 |
|
blanchet@44218
|
1165 |
\opdefault{max\_new\_mono\_instances}{int}{\upshape 200}
|
blanchet@43753
|
1166 |
Specifies the maximum number of monomorphic instances to generate beyond
|
blanchet@43753
|
1167 |
\textit{max\_relevant}. The higher this limit is, the more monomorphic instances
|
blanchet@43753
|
1168 |
are potentially generated. Whether monomorphization takes place depends on the
|
blanchet@44494
|
1169 |
type encoding used.
|
blanchet@43753
|
1170 |
|
blanchet@43753
|
1171 |
\nopagebreak
|
blanchet@44494
|
1172 |
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
|
blanchet@43753
|
1173 |
|
blanchet@43753
|
1174 |
\opdefault{max\_mono\_iters}{int}{\upshape 3}
|
blanchet@43753
|
1175 |
Specifies the maximum number of iterations for the monomorphization fixpoint
|
blanchet@43753
|
1176 |
construction. The higher this limit is, the more monomorphic instances are
|
blanchet@43753
|
1177 |
potentially generated. Whether monomorphization takes place depends on the
|
blanchet@44494
|
1178 |
type encoding used.
|
blanchet@43753
|
1179 |
|
blanchet@43753
|
1180 |
\nopagebreak
|
blanchet@44494
|
1181 |
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
|
blanchet@36918
|
1182 |
\end{enum}
|
blanchet@36918
|
1183 |
|
blanchet@36918
|
1184 |
\subsection{Output Format}
|
blanchet@36918
|
1185 |
\label{output-format}
|
blanchet@36918
|
1186 |
|
blanchet@36918
|
1187 |
\begin{enum}
|
blanchet@36918
|
1188 |
|
blanchet@36918
|
1189 |
\opfalse{verbose}{quiet}
|
blanchet@36918
|
1190 |
Specifies whether the \textbf{sledgehammer} command should explain what it does.
|
blanchet@41456
|
1191 |
This option is implicitly disabled for automatic runs.
|
blanchet@36918
|
1192 |
|
blanchet@36918
|
1193 |
\opfalse{debug}{no\_debug}
|
blanchet@40444
|
1194 |
Specifies whether Sledgehammer should display additional debugging information
|
blanchet@40444
|
1195 |
beyond what \textit{verbose} already displays. Enabling \textit{debug} also
|
blanchet@41456
|
1196 |
enables \textit{verbose} and \textit{blocking} (\S\ref{mode-of-operation})
|
blanchet@41456
|
1197 |
behind the scenes. The \textit{debug} option is implicitly disabled for
|
blanchet@41456
|
1198 |
automatic runs.
|
blanchet@36918
|
1199 |
|
blanchet@36918
|
1200 |
\nopagebreak
|
blanchet@36918
|
1201 |
{\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
|
blanchet@36918
|
1202 |
|
blanchet@36918
|
1203 |
\opfalse{isar\_proof}{no\_isar\_proof}
|
blanchet@36918
|
1204 |
Specifies whether Isar proofs should be output in addition to one-liner
|
blanchet@36918
|
1205 |
\textit{metis} proofs. Isar proof construction is still experimental and often
|
blanchet@36918
|
1206 |
fails; however, they are usually faster and sometimes more robust than
|
blanchet@36918
|
1207 |
\textit{metis} proofs.
|
blanchet@36918
|
1208 |
|
blanchet@40584
|
1209 |
\opdefault{isar\_shrink\_factor}{int}{\upshape 1}
|
blanchet@36918
|
1210 |
Specifies the granularity of the Isar proof. A value of $n$ indicates that each
|
blanchet@36918
|
1211 |
Isar proof step should correspond to a group of up to $n$ consecutive proof
|
blanchet@36918
|
1212 |
steps in the ATP proof.
|
blanchet@36918
|
1213 |
\end{enum}
|
blanchet@36918
|
1214 |
|
blanchet@39228
|
1215 |
\subsection{Authentication}
|
blanchet@39228
|
1216 |
\label{authentication}
|
blanchet@36918
|
1217 |
|
blanchet@36918
|
1218 |
\begin{enum}
|
blanchet@39228
|
1219 |
\opnodefault{expect}{string}
|
blanchet@39228
|
1220 |
Specifies the expected outcome, which must be one of the following:
|
blanchet@39228
|
1221 |
|
blanchet@39228
|
1222 |
\begin{enum}
|
blanchet@47128
|
1223 |
\item[\labelitemi] \textbf{\textit{some}:} Sledgehammer found a proof.
|
blanchet@46387
|
1224 |
\item[\labelitemi] \textbf{\textit{none}:} Sledgehammer found no proof.
|
blanchet@46387
|
1225 |
\item[\labelitemi] \textbf{\textit{timeout}:} Sledgehammer timed out.
|
blanchet@46387
|
1226 |
\item[\labelitemi] \textbf{\textit{unknown}:} Sledgehammer encountered some
|
blanchet@40444
|
1227 |
problem.
|
blanchet@39228
|
1228 |
\end{enum}
|
blanchet@39228
|
1229 |
|
blanchet@39228
|
1230 |
Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning
|
blanchet@39228
|
1231 |
(otherwise) if the actual outcome differs from the expected outcome. This option
|
blanchet@39228
|
1232 |
is useful for regression testing.
|
blanchet@39228
|
1233 |
|
blanchet@39228
|
1234 |
\nopagebreak
|
blanchet@43879
|
1235 |
{\small See also \textit{blocking} (\S\ref{mode-of-operation}) and
|
blanchet@43879
|
1236 |
\textit{timeout} (\S\ref{timeouts}).}
|
blanchet@43879
|
1237 |
\end{enum}
|
blanchet@43879
|
1238 |
|
blanchet@43879
|
1239 |
\subsection{Timeouts}
|
blanchet@43879
|
1240 |
\label{timeouts}
|
blanchet@43879
|
1241 |
|
blanchet@43879
|
1242 |
\begin{enum}
|
blanchet@43879
|
1243 |
\opdefault{timeout}{float\_or\_none}{\upshape 30}
|
blanchet@43879
|
1244 |
Specifies the maximum number of seconds that the automatic provers should spend
|
blanchet@43879
|
1245 |
searching for a proof. This excludes problem preparation and is a soft limit.
|
blanchet@43879
|
1246 |
For historical reasons, the default value of this option can be overridden using
|
blanchet@45607
|
1247 |
the option ``Sledgehammer: Time Limit'' in Proof General's ``Isabelle'' menu.
|
blanchet@43879
|
1248 |
|
blanchet@47126
|
1249 |
\opdefault{preplay\_timeout}{float\_or\_none}{\upshape 3}
|
blanchet@46251
|
1250 |
Specifies the maximum number of seconds that \textit{metis} or \textit{smt}
|
blanchet@46251
|
1251 |
should spend trying to ``preplay'' the found proof. If this option is set to 0,
|
blanchet@46251
|
1252 |
no preplaying takes place, and no timing information is displayed next to the
|
blanchet@46251
|
1253 |
suggested \textit{metis} calls.
|
blanchet@46579
|
1254 |
|
blanchet@46579
|
1255 |
\nopagebreak
|
blanchet@46579
|
1256 |
{\small See also \textit{minimize} (\S\ref{mode-of-operation}).}
|
blanchet@36918
|
1257 |
\end{enum}
|
blanchet@36918
|
1258 |
|
blanchet@36918
|
1259 |
\let\em=\sl
|
blanchet@36918
|
1260 |
\bibliography{../manual}{}
|
blanchet@36918
|
1261 |
\bibliographystyle{abbrv}
|
blanchet@36918
|
1262 |
|
blanchet@36918
|
1263 |
\end{document}
|