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@36918
|
15 |
%\oddsidemargin=4.6mm
|
blanchet@36918
|
16 |
%\evensidemargin=4.6mm
|
blanchet@36918
|
17 |
%\textwidth=150mm
|
blanchet@36918
|
18 |
%\topmargin=4.6mm
|
blanchet@36918
|
19 |
%\headheight=0mm
|
blanchet@36918
|
20 |
%\headsep=0mm
|
blanchet@36918
|
21 |
%\textheight=234mm
|
blanchet@36918
|
22 |
|
blanchet@36918
|
23 |
\def\Colon{\mathord{:\mkern-1.5mu:}}
|
blanchet@36918
|
24 |
%\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
|
blanchet@36918
|
25 |
%\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
|
blanchet@36918
|
26 |
\def\lparr{\mathopen{(\mkern-4mu\mid}}
|
blanchet@36918
|
27 |
\def\rparr{\mathclose{\mid\mkern-4mu)}}
|
blanchet@36918
|
28 |
|
blanchet@36918
|
29 |
\def\unk{{?}}
|
blanchet@36918
|
30 |
\def\undef{(\lambda x.\; \unk)}
|
blanchet@36918
|
31 |
%\def\unr{\textit{others}}
|
blanchet@36918
|
32 |
\def\unr{\ldots}
|
blanchet@36918
|
33 |
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
|
blanchet@36918
|
34 |
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
|
blanchet@36918
|
35 |
|
blanchet@36918
|
36 |
\urlstyle{tt}
|
blanchet@36918
|
37 |
|
blanchet@36918
|
38 |
\begin{document}
|
blanchet@36918
|
39 |
|
blanchet@36918
|
40 |
\selectlanguage{english}
|
blanchet@36918
|
41 |
|
blanchet@36918
|
42 |
\title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
|
blanchet@36918
|
43 |
Hammering Away \\[\smallskipamount]
|
blanchet@36918
|
44 |
\Large A User's Guide to Sledgehammer for Isabelle/HOL}
|
blanchet@36918
|
45 |
\author{\hbox{} \\
|
blanchet@36918
|
46 |
Jasmin Christian Blanchette \\
|
blanchet@36918
|
47 |
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
|
blanchet@36918
|
48 |
\hbox{}}
|
blanchet@36918
|
49 |
|
blanchet@36918
|
50 |
\maketitle
|
blanchet@36918
|
51 |
|
blanchet@36918
|
52 |
\tableofcontents
|
blanchet@36918
|
53 |
|
blanchet@36918
|
54 |
\setlength{\parskip}{.7em plus .2em minus .1em}
|
blanchet@36918
|
55 |
\setlength{\parindent}{0pt}
|
blanchet@36918
|
56 |
\setlength{\abovedisplayskip}{\parskip}
|
blanchet@36918
|
57 |
\setlength{\abovedisplayshortskip}{.9\parskip}
|
blanchet@36918
|
58 |
\setlength{\belowdisplayskip}{\parskip}
|
blanchet@36918
|
59 |
\setlength{\belowdisplayshortskip}{.9\parskip}
|
blanchet@36918
|
60 |
|
blanchet@36918
|
61 |
% General-purpose enum environment with correct spacing
|
blanchet@36918
|
62 |
\newenvironment{enum}%
|
blanchet@36918
|
63 |
{\begin{list}{}{%
|
blanchet@36918
|
64 |
\setlength{\topsep}{.1\parskip}%
|
blanchet@36918
|
65 |
\setlength{\partopsep}{.1\parskip}%
|
blanchet@36918
|
66 |
\setlength{\itemsep}{\parskip}%
|
blanchet@36918
|
67 |
\advance\itemsep by-\parsep}}
|
blanchet@36918
|
68 |
{\end{list}}
|
blanchet@36918
|
69 |
|
blanchet@36918
|
70 |
\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
|
blanchet@36918
|
71 |
\advance\rightskip by\leftmargin}
|
blanchet@36918
|
72 |
\def\post{\vskip0pt plus1ex\endgroup}
|
blanchet@36918
|
73 |
|
blanchet@36918
|
74 |
\def\prew{\pre\advance\rightskip by-\leftmargin}
|
blanchet@36918
|
75 |
\def\postw{\post}
|
blanchet@36918
|
76 |
|
blanchet@36918
|
77 |
\section{Introduction}
|
blanchet@36918
|
78 |
\label{introduction}
|
blanchet@36918
|
79 |
|
blanchet@36918
|
80 |
Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs)
|
blanchet@41190
|
81 |
and satisfiability-modulo-theories (SMT) solvers on the current goal. The
|
blanchet@40254
|
82 |
supported ATPs are E \cite{schulz-2002}, SPASS \cite{weidenbach-et-al-2009},
|
blanchet@40254
|
83 |
Vampire \cite{riazanov-voronkov-2002}, SInE-E \cite{sine}, and SNARK
|
blanchet@40254
|
84 |
\cite{snark}. The ATPs are run either locally or remotely via the
|
blanchet@40254
|
85 |
System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs, the
|
blanchet@41190
|
86 |
SMT solvers Z3 \cite{z3} is used, and you can tell Sledgehammer to try Yices
|
blanchet@41190
|
87 |
\cite{yices} and CVC3 \cite{cvc3} as well.
|
blanchet@36918
|
88 |
|
blanchet@40254
|
89 |
The problem passed to the automatic provers consists of your current goal
|
blanchet@40254
|
90 |
together with a heuristic selection of hundreds of facts (theorems) from the
|
blanchet@40254
|
91 |
current theory context, filtered by relevance. Because jobs are run in the
|
blanchet@40254
|
92 |
background, you can continue to work on your proof by other means. Provers can
|
blanchet@40254
|
93 |
be run in parallel. Any reply (which may arrive half a minute later) will appear
|
blanchet@40254
|
94 |
in the Proof General response buffer.
|
blanchet@37517
|
95 |
|
blanchet@40254
|
96 |
The result of a successful proof search is some source text that usually (but
|
blanchet@40254
|
97 |
not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
|
blanchet@40254
|
98 |
proof relies on the general-purpose Metis prover \cite{metis}, which is fully
|
blanchet@40254
|
99 |
integrated into Isabelle/HOL, with explicit inferences going through the kernel.
|
blanchet@40254
|
100 |
Thus its results are correct by construction.
|
blanchet@36918
|
101 |
|
blanchet@39566
|
102 |
In this manual, we will explicitly invoke the \textbf{sledgehammer} command.
|
blanchet@39566
|
103 |
Sledgehammer also provides an automatic mode that can be enabled via the
|
blanchet@39566
|
104 |
``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof General. In
|
blanchet@39566
|
105 |
this mode, Sledgehammer is run on every newly entered theorem. The time limit
|
blanchet@39566
|
106 |
for Auto Sledgehammer and other automatic tools can be set using the ``Auto
|
blanchet@39566
|
107 |
Tools Time Limit'' option.
|
blanchet@39566
|
108 |
|
blanchet@36918
|
109 |
\newbox\boxA
|
blanchet@36918
|
110 |
\setbox\boxA=\hbox{\texttt{nospam}}
|
blanchet@36918
|
111 |
|
blanchet@40937
|
112 |
To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is
|
blanchet@40937
|
113 |
imported---this is rarely a problem in practice since it is part of
|
blanchet@40937
|
114 |
\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's
|
blanchet@36918
|
115 |
\texttt{src/HOL/Metis\_Examples} directory.
|
blanchet@36918
|
116 |
Comments and bug reports concerning Sledgehammer or this manual should be
|
blanchet@36918
|
117 |
directed to
|
blanchet@36918
|
118 |
\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
|
blanchet@36918
|
119 |
in.\allowbreak tum.\allowbreak de}.
|
blanchet@36918
|
120 |
|
blanchet@36918
|
121 |
\vskip2.5\smallskipamount
|
blanchet@36918
|
122 |
|
blanchet@36918
|
123 |
%\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
|
blanchet@36918
|
124 |
%suggesting several textual improvements.
|
blanchet@36918
|
125 |
|
blanchet@36918
|
126 |
\section{Installation}
|
blanchet@36918
|
127 |
\label{installation}
|
blanchet@36918
|
128 |
|
blanchet@36918
|
129 |
Sledgehammer is part of Isabelle, so you don't need to install it. However, it
|
blanchet@40254
|
130 |
relies on third-party automatic theorem provers (ATPs) and SAT solvers.
|
blanchet@40254
|
131 |
Currently, E, SPASS, and Vampire can be run locally; in addition, E, Vampire,
|
blanchet@40254
|
132 |
SInE-E, and SNARK are available remotely via SystemOnTPTP \cite{sutcliffe-2000}.
|
blanchet@40254
|
133 |
If you want better performance, you should install E and SPASS locally.
|
blanchet@36918
|
134 |
|
blanchet@38289
|
135 |
There are three main ways to install ATPs on your machine:
|
blanchet@36918
|
136 |
|
blanchet@36918
|
137 |
\begin{enum}
|
blanchet@36918
|
138 |
\item[$\bullet$] If you installed an official Isabelle package with everything
|
blanchet@36918
|
139 |
inside, it should already include properly setup executables for E and SPASS,
|
blanchet@38289
|
140 |
ready to use.%
|
blanchet@38289
|
141 |
\footnote{Vampire's license prevents us from doing the same for this otherwise
|
blanchet@38289
|
142 |
wonderful tool.}
|
blanchet@36918
|
143 |
|
blanchet@38289
|
144 |
\item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS
|
blanchet@36918
|
145 |
binary packages from Isabelle's download page. Extract the archives, then add a
|
blanchet@42618
|
146 |
line to your \texttt{\$ISABELLE\_HOME\_USER/etc/components}%
|
blanchet@42618
|
147 |
\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
|
blanchet@42618
|
148 |
startup. Its value can be retrieved by invoking \texttt{isabelle}
|
blanchet@42618
|
149 |
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
|
blanchet@42618
|
150 |
file with the absolute
|
blanchet@40444
|
151 |
path to E or SPASS. For example, if the \texttt{components} does not exist yet
|
blanchet@40444
|
152 |
and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create the
|
blanchet@40444
|
153 |
\texttt{components} file with the single line
|
blanchet@36918
|
154 |
|
blanchet@36918
|
155 |
\prew
|
blanchet@36918
|
156 |
\texttt{/usr/local/spass-3.7}
|
blanchet@36918
|
157 |
\postw
|
blanchet@36918
|
158 |
|
blanchet@38289
|
159 |
in it.
|
blanchet@38289
|
160 |
|
blanchet@38289
|
161 |
\item[$\bullet$] If you prefer to build E or SPASS yourself, or obtained a
|
blanchet@38289
|
162 |
Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}),
|
blanchet@38289
|
163 |
set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
|
blanchet@38289
|
164 |
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
|
blanchet@38309
|
165 |
\texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
|
blanchet@38309
|
166 |
with E 1.0 and 1.2, SPASS 3.5 and 3.7, and Vampire 1.0%
|
blanchet@38309
|
167 |
\footnote{Following the rewrite of Vampire, the counter for version numbers was
|
blanchet@38309
|
168 |
reset to 0; hence the new Vampire 1.0 is more recent than Vampire 11.5.}%
|
blanchet@38309
|
169 |
. Since the ATPs' output formats are neither documented nor stable, other
|
blanchet@38309
|
170 |
versions of the ATPs might or might not work well with Sledgehammer.
|
blanchet@36918
|
171 |
\end{enum}
|
blanchet@36918
|
172 |
|
blanchet@36918
|
173 |
To check whether E and SPASS are installed, follow the example in
|
blanchet@36918
|
174 |
\S\ref{first-steps}.
|
blanchet@36918
|
175 |
|
blanchet@37517
|
176 |
Remote ATP invocation via the SystemOnTPTP web service requires Perl with the
|
blanchet@39388
|
177 |
World Wide Web Library (\texttt{libwww-perl}) installed. If you must use a proxy
|
blanchet@39388
|
178 |
server to access the Internet, set the \texttt{http\_proxy} environment variable
|
blanchet@39389
|
179 |
to the proxy, either in the environment in which Isabelle is launched or in your
|
blanchet@42618
|
180 |
\texttt{\char`\~/\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few examples:
|
blanchet@39388
|
181 |
|
blanchet@39388
|
182 |
\prew
|
blanchet@39389
|
183 |
\texttt{http\_proxy=http://proxy.example.org} \\
|
blanchet@39389
|
184 |
\texttt{http\_proxy=http://proxy.example.org:8080} \\
|
blanchet@39389
|
185 |
\texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org}
|
blanchet@39388
|
186 |
\postw
|
blanchet@37517
|
187 |
|
blanchet@36918
|
188 |
\section{First Steps}
|
blanchet@36918
|
189 |
\label{first-steps}
|
blanchet@36918
|
190 |
|
blanchet@36918
|
191 |
To illustrate Sledgehammer in context, let us start a theory file and
|
blanchet@36918
|
192 |
attempt to prove a simple lemma:
|
blanchet@36918
|
193 |
|
blanchet@36918
|
194 |
\prew
|
blanchet@36918
|
195 |
\textbf{theory}~\textit{Scratch} \\
|
blanchet@36918
|
196 |
\textbf{imports}~\textit{Main} \\
|
blanchet@36918
|
197 |
\textbf{begin} \\[2\smallskipamount]
|
blanchet@36918
|
198 |
%
|
blanchet@36918
|
199 |
\textbf{lemma} ``$[a] = [b] \,\longleftrightarrow\, a = b$'' \\
|
blanchet@36918
|
200 |
\textbf{sledgehammer}
|
blanchet@36918
|
201 |
\postw
|
blanchet@36918
|
202 |
|
blanchet@37517
|
203 |
Instead of issuing the \textbf{sledgehammer} command, you can also find
|
blanchet@37517
|
204 |
Sledgehammer in the ``Commands'' submenu of the ``Isabelle'' menu in Proof
|
blanchet@37517
|
205 |
General or press the Emacs key sequence C-c C-a C-s.
|
blanchet@37517
|
206 |
Either way, Sledgehammer produces the following output after a few seconds:
|
blanchet@36918
|
207 |
|
blanchet@36918
|
208 |
\prew
|
blanchet@36918
|
209 |
\slshape
|
blanchet@40241
|
210 |
Sledgehammer: ``\textit{e}'' for subgoal 1: \\
|
blanchet@36918
|
211 |
$([a] = [b]) = (a = b)$ \\
|
blanchet@36918
|
212 |
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
|
blanchet@38289
|
213 |
To minimize the number of lemmas, try this: \\
|
blanchet@40240
|
214 |
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
|
blanchet@36918
|
215 |
%
|
blanchet@40241
|
216 |
Sledgehammer: ``\textit{spass}'' for subgoal 1: \\
|
blanchet@36918
|
217 |
$([a] = [b]) = (a = b)$ \\
|
blanchet@36918
|
218 |
Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
|
blanchet@38289
|
219 |
To minimize the number of lemmas, try this: \\
|
blanchet@40240
|
220 |
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
|
blanchet@36918
|
221 |
%
|
blanchet@40254
|
222 |
Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\
|
blanchet@36918
|
223 |
$([a] = [b]) = (a = b)$ \\
|
blanchet@40254
|
224 |
Try this command: \textbf{by} (\textit{metis eq\_commute last\_snoc}) \\
|
blanchet@38289
|
225 |
To minimize the number of lemmas, try this: \\
|
blanchet@40254
|
226 |
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}]~(\textit{eq\_commute last\_snoc}). \\[3\smallskipamount]
|
blanchet@40254
|
227 |
%
|
blanchet@40254
|
228 |
Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\
|
blanchet@40254
|
229 |
$([a] = [b]) = (a = b)$ \\
|
blanchet@40254
|
230 |
Try this command: \textbf{by} (\textit{metis hd.simps}) \\
|
blanchet@40254
|
231 |
To minimize the number of lemmas, try this: \\
|
blanchet@40444
|
232 |
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
|
blanchet@41190
|
233 |
%
|
blanchet@41190
|
234 |
Sledgehammer: ``\textit{remote\_z3}'' for subgoal 1: \\
|
blanchet@41190
|
235 |
$([a] = [b]) = (a = b)$ \\
|
blanchet@41190
|
236 |
Try this command: \textbf{by} (\textit{metis hd.simps}) \\
|
blanchet@41190
|
237 |
To minimize the number of lemmas, try this: \\
|
blanchet@41190
|
238 |
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
|
blanchet@36918
|
239 |
\postw
|
blanchet@36918
|
240 |
|
blanchet@41190
|
241 |
Sledgehammer ran E, SPASS, Vampire, SInE-E, and Z3 in parallel. Depending on
|
blanchet@41190
|
242 |
which provers are installed and how many processor cores are available, some of
|
blanchet@41190
|
243 |
the provers might be missing or present with a \textit{remote\_} prefix.
|
blanchet@36918
|
244 |
|
blanchet@40254
|
245 |
For each successful prover, Sledgehammer gives a one-liner proof that uses the
|
blanchet@40254
|
246 |
\textit{metis} or \textit{smt} method. You can click the proof to insert it into
|
blanchet@40254
|
247 |
the theory text. You can click the ``\textbf{sledgehammer} \textit{minimize}''
|
blanchet@40254
|
248 |
command if you want to look for a shorter (and probably faster) proof. But here
|
blanchet@40254
|
249 |
the proof found by E looks perfect, so click it to finish the proof.
|
blanchet@36918
|
250 |
|
blanchet@36918
|
251 |
You can ask Sledgehammer for an Isar text proof by passing the
|
blanchet@36918
|
252 |
\textit{isar\_proof} option:
|
blanchet@36918
|
253 |
|
blanchet@36918
|
254 |
\prew
|
blanchet@36918
|
255 |
\textbf{sledgehammer} [\textit{isar\_proof}]
|
blanchet@36918
|
256 |
\postw
|
blanchet@36918
|
257 |
|
blanchet@36918
|
258 |
When Isar proof construction is successful, it can yield proofs that are more
|
blanchet@36918
|
259 |
readable and also faster than the \textit{metis} one-liners. This feature is
|
blanchet@40254
|
260 |
experimental and is only available for ATPs.
|
blanchet@36918
|
261 |
|
blanchet@37517
|
262 |
\section{Hints}
|
blanchet@37517
|
263 |
\label{hints}
|
blanchet@37517
|
264 |
|
blanchet@37517
|
265 |
For best results, first simplify your problem by calling \textit{auto} or at
|
blanchet@37517
|
266 |
least \textit{safe} followed by \textit{simp\_all}. None of the ATPs contain
|
blanchet@37517
|
267 |
arithmetic decision procedures. They are not especially good at heavy rewriting,
|
blanchet@37517
|
268 |
but because they regard equations as undirected, they often prove theorems that
|
blanchet@37517
|
269 |
require the reverse orientation of a \textit{simp} rule. Higher-order problems
|
blanchet@37517
|
270 |
can be tackled, but the success rate is better for first-order problems. Hence,
|
blanchet@37517
|
271 |
you may get better results if you first simplify the problem to remove
|
blanchet@37517
|
272 |
higher-order features.
|
blanchet@37517
|
273 |
|
blanchet@39566
|
274 |
Note that problems can be easy for \textit{auto} and difficult for ATPs, but the
|
blanchet@39566
|
275 |
reverse is also true, so don't be discouraged if your first attempts fail.
|
blanchet@39566
|
276 |
Because the system refers to all theorems known to Isabelle, it is particularly
|
blanchet@39566
|
277 |
suitable when your goal has a short proof from lemmas that you don't know about.
|
blanchet@37517
|
278 |
|
blanchet@36918
|
279 |
\section{Command Syntax}
|
blanchet@36918
|
280 |
\label{command-syntax}
|
blanchet@36918
|
281 |
|
blanchet@36918
|
282 |
Sledgehammer can be invoked at any point when there is an open goal by entering
|
blanchet@36918
|
283 |
the \textbf{sledgehammer} command in the theory file. Its general syntax is as
|
blanchet@36918
|
284 |
follows:
|
blanchet@36918
|
285 |
|
blanchet@36918
|
286 |
\prew
|
blanchet@36918
|
287 |
\textbf{sledgehammer} \textit{subcommand\/$^?$ options\/$^?$ facts\_override\/$^?$ num\/$^?$}
|
blanchet@36918
|
288 |
\postw
|
blanchet@36918
|
289 |
|
blanchet@36918
|
290 |
For convenience, Sledgehammer is also available in the ``Commands'' submenu of
|
blanchet@36918
|
291 |
the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c
|
blanchet@36918
|
292 |
C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with
|
blanchet@36918
|
293 |
no arguments in the theory text.
|
blanchet@36918
|
294 |
|
blanchet@36918
|
295 |
In the general syntax, the \textit{subcommand} may be any of the following:
|
blanchet@36918
|
296 |
|
blanchet@36918
|
297 |
\begin{enum}
|
blanchet@40444
|
298 |
\item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on
|
blanchet@40444
|
299 |
subgoal number \textit{num} (1 by default), with the given options and facts.
|
blanchet@36918
|
300 |
|
blanchet@36918
|
301 |
\item[$\bullet$] \textbf{\textit{minimize}:} Attempts to minimize the provided facts
|
blanchet@36918
|
302 |
(specified in the \textit{facts\_override} argument) to obtain a simpler proof
|
blanchet@36918
|
303 |
involving fewer facts. The options and goal number are as for \textit{run}.
|
blanchet@36918
|
304 |
|
blanchet@40444
|
305 |
\item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued
|
blanchet@40444
|
306 |
by Sledgehammer. This allows you to examine results that might have been lost
|
blanchet@40444
|
307 |
due to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
|
blanchet@36918
|
308 |
limit on the number of messages to display (5 by default).
|
blanchet@36918
|
309 |
|
blanchet@42591
|
310 |
\item[$\bullet$] \textbf{\textit{supported\_provers}:} Prints the list of
|
blanchet@42588
|
311 |
automatic provers supported by Sledgehammer. See \S\ref{installation} and
|
blanchet@42588
|
312 |
\S\ref{mode-of-operation} for more information on how to install automatic
|
blanchet@42588
|
313 |
provers.
|
blanchet@36918
|
314 |
|
blanchet@40240
|
315 |
\item[$\bullet$] \textbf{\textit{running\_provers}:} Prints information about
|
blanchet@40240
|
316 |
currently running automatic provers, including elapsed runtime and remaining
|
blanchet@40240
|
317 |
time until timeout.
|
blanchet@36918
|
318 |
|
blanchet@40240
|
319 |
\item[$\bullet$] \textbf{\textit{kill\_provers}:} Terminates all running
|
blanchet@40240
|
320 |
automatic provers.
|
blanchet@36918
|
321 |
|
blanchet@36918
|
322 |
\item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
|
blanchet@36918
|
323 |
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
|
blanchet@36918
|
324 |
\end{enum}
|
blanchet@36918
|
325 |
|
blanchet@36918
|
326 |
Sledgehammer's behavior can be influenced by various \textit{options}, which can
|
blanchet@36918
|
327 |
be specified in brackets after the \textbf{sledgehammer} command. The
|
blanchet@36918
|
328 |
\textit{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
|
blanchet@36918
|
329 |
\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true}'' is optional. For
|
blanchet@36918
|
330 |
example:
|
blanchet@36918
|
331 |
|
blanchet@36918
|
332 |
\prew
|
blanchet@36918
|
333 |
\textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120$\,s$]
|
blanchet@36918
|
334 |
\postw
|
blanchet@36918
|
335 |
|
blanchet@36918
|
336 |
Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
|
blanchet@36918
|
337 |
|
blanchet@36918
|
338 |
\prew
|
blanchet@36918
|
339 |
\textbf{sledgehammer\_params} \textit{options}
|
blanchet@36918
|
340 |
\postw
|
blanchet@36918
|
341 |
|
blanchet@36918
|
342 |
The supported options are described in \S\ref{option-reference}.
|
blanchet@36918
|
343 |
|
blanchet@36918
|
344 |
The \textit{facts\_override} argument lets you alter the set of facts that go
|
blanchet@36918
|
345 |
through the relevance filter. It may be of the form ``(\textit{facts})'', where
|
blanchet@36918
|
346 |
\textit{facts} is a space-separated list of Isabelle facts (theorems, local
|
blanchet@36918
|
347 |
assumptions, etc.), in which case the relevance filter is bypassed and the given
|
blanchet@39566
|
348 |
facts are used. It may also be of the form ``(\textit{add}:\ \textit{facts}$_1$)'',
|
blanchet@39566
|
349 |
``(\textit{del}:\ \textit{facts}$_2$)'', or ``(\textit{add}:\ \textit{facts}$_1$\
|
blanchet@39566
|
350 |
\textit{del}:\ \textit{facts}$_2$)'', where the relevance filter is instructed to
|
blanchet@36918
|
351 |
proceed as usual except that it should consider \textit{facts}$_1$
|
blanchet@36918
|
352 |
highly-relevant and \textit{facts}$_2$ fully irrelevant.
|
blanchet@36918
|
353 |
|
blanchet@39566
|
354 |
You can instruct Sledgehammer to run automatically on newly entered theorems by
|
blanchet@39566
|
355 |
enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof
|
blanchet@40240
|
356 |
General. For automatic runs, only the first prover set using \textit{provers}
|
blanchet@43601
|
357 |
(\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover,
|
blanchet@43601
|
358 |
\textit{slicing} (\S\ref{mode-of-operation}) is disabled, \textit{timeout}
|
blanchet@40254
|
359 |
(\S\ref{mode-of-operation}) is superseded by the ``Auto Tools Time Limit'' in
|
blanchet@43601
|
360 |
Proof General's ``Isabelle'' menu, \textit{full\_types}
|
blanchet@43601
|
361 |
(\S\ref{problem-encoding}) is enabled, and \textit{verbose}
|
blanchet@43601
|
362 |
(\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled.
|
blanchet@43601
|
363 |
Sledgehammer's output is also more concise.
|
blanchet@39566
|
364 |
|
blanchet@36918
|
365 |
\section{Option Reference}
|
blanchet@36918
|
366 |
\label{option-reference}
|
blanchet@36918
|
367 |
|
blanchet@36918
|
368 |
\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
|
blanchet@36918
|
369 |
\def\qty#1{$\left<\textit{#1}\right>$}
|
blanchet@36918
|
370 |
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
|
blanchet@36918
|
371 |
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
|
blanchet@36918
|
372 |
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
|
blanchet@36918
|
373 |
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
|
blanchet@36918
|
374 |
\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
|
blanchet@36918
|
375 |
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
|
blanchet@36918
|
376 |
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
|
blanchet@36918
|
377 |
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
|
blanchet@36918
|
378 |
\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
|
blanchet@36918
|
379 |
\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
|
blanchet@36918
|
380 |
|
blanchet@36918
|
381 |
Sledgehammer's options are categorized as follows:\ mode of operation
|
blanchet@39228
|
382 |
(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),
|
blanchet@39228
|
383 |
relevance filter (\S\ref{relevance-filter}), output format
|
blanchet@39228
|
384 |
(\S\ref{output-format}), and authentication (\S\ref{authentication}).
|
blanchet@36918
|
385 |
|
blanchet@36918
|
386 |
The descriptions below refer to the following syntactic quantities:
|
blanchet@36918
|
387 |
|
blanchet@36918
|
388 |
\begin{enum}
|
blanchet@36918
|
389 |
\item[$\bullet$] \qtybf{string}: A string.
|
blanchet@36918
|
390 |
\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
|
blanchet@40444
|
391 |
\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or
|
blanchet@40444
|
392 |
\textit{smart}.
|
blanchet@36918
|
393 |
\item[$\bullet$] \qtybf{int\/}: An integer.
|
blanchet@43589
|
394 |
%\item[$\bullet$] \qtybf{float\/}: A floating-point number (e.g., 2.5).
|
blanchet@40584
|
395 |
\item[$\bullet$] \qtybf{float\_pair\/}: A pair of floating-point numbers
|
blanchet@40584
|
396 |
(e.g., 0.6 0.95).
|
blanchet@38814
|
397 |
\item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
|
blanchet@40584
|
398 |
\item[$\bullet$] \qtybf{float\_or\_none\/}: An integer (e.g., 60) or
|
blanchet@40584
|
399 |
floating-point number (e.g., 0.5) expressing a number of seconds, or the keyword
|
blanchet@40584
|
400 |
\textit{none} ($\infty$ seconds).
|
blanchet@36918
|
401 |
\end{enum}
|
blanchet@36918
|
402 |
|
blanchet@36918
|
403 |
Default values are indicated in square brackets. Boolean options have a negated
|
blanchet@39228
|
404 |
counterpart (e.g., \textit{blocking} vs.\ \textit{non\_blocking}). When setting
|
blanchet@36918
|
405 |
Boolean options, ``= \textit{true}'' may be omitted.
|
blanchet@36918
|
406 |
|
blanchet@36918
|
407 |
\subsection{Mode of Operation}
|
blanchet@36918
|
408 |
\label{mode-of-operation}
|
blanchet@36918
|
409 |
|
blanchet@36918
|
410 |
\begin{enum}
|
blanchet@40240
|
411 |
\opnodefault{provers}{string}
|
blanchet@40240
|
412 |
Specifies the automatic provers to use as a space-separated list (e.g.,
|
blanchet@40240
|
413 |
``\textit{e}~\textit{spass}''). The following provers are supported:
|
blanchet@36918
|
414 |
|
blanchet@36918
|
415 |
\begin{enum}
|
blanchet@36918
|
416 |
\item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz
|
blanchet@36918
|
417 |
\cite{schulz-2002}. To use E, set the environment variable
|
blanchet@36918
|
418 |
\texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable,
|
blanchet@36918
|
419 |
or install the prebuilt E package from Isabelle's download page. See
|
blanchet@36918
|
420 |
\S\ref{installation} for details.
|
blanchet@36918
|
421 |
|
blanchet@36918
|
422 |
\item[$\bullet$] \textbf{\textit{spass}:} SPASS is an ATP developed by Christoph
|
blanchet@36918
|
423 |
Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the
|
blanchet@36918
|
424 |
environment variable \texttt{SPASS\_HOME} to the directory that contains the
|
blanchet@36918
|
425 |
\texttt{SPASS} executable, or install the prebuilt SPASS package from Isabelle's
|
blanchet@37389
|
426 |
download page. Sledgehammer requires version 3.5 or above. See
|
blanchet@37389
|
427 |
\S\ref{installation} for details.
|
blanchet@36918
|
428 |
|
blanchet@36918
|
429 |
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
|
blanchet@36918
|
430 |
Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
|
blanchet@36918
|
431 |
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
|
blanchet@41190
|
432 |
that contains the \texttt{vampire} executable. Sledgehammer has been tested with
|
blanchet@41190
|
433 |
versions 11, 0.6, and 1.0.
|
blanchet@36918
|
434 |
|
blanchet@42611
|
435 |
\item[$\bullet$] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
|
blanchet@42611
|
436 |
Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
|
blanchet@42611
|
437 |
set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
|
blanchet@42611
|
438 |
executable, including the file name. Sledgehammer has been tested with version
|
blanchet@42611
|
439 |
2.2.
|
blanchet@41190
|
440 |
|
blanchet@41190
|
441 |
\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
|
blanchet@41190
|
442 |
SRI \cite{yices}. To use Yices, set the environment variable
|
blanchet@41190
|
443 |
\texttt{YICES\_SOLVER} to the complete path of the executable, including the
|
blanchet@41190
|
444 |
file name. Sledgehammer has been tested with version 1.0.
|
blanchet@41190
|
445 |
|
blanchet@42611
|
446 |
\item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
|
blanchet@42611
|
447 |
Microsoft Research \cite{z3}. To use Z3, set the environment variable
|
blanchet@42611
|
448 |
\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
|
blanchet@42611
|
449 |
name. Sledgehammer has been tested with versions 2.7 to 2.18.
|
blanchet@42611
|
450 |
|
blanchet@42611
|
451 |
\item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
|
blanchet@42611
|
452 |
ATP, exploiting Z3's undocumented support for the TPTP format. It is included
|
blanchet@43313
|
453 |
for experimental purposes. It requires version 2.18 or above.
|
blanchet@40254
|
454 |
|
blanchet@38824
|
455 |
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
|
blanchet@36918
|
456 |
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
|
blanchet@36918
|
457 |
|
blanchet@36918
|
458 |
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
|
blanchet@38824
|
459 |
Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
|
blanchet@36918
|
460 |
|
blanchet@43406
|
461 |
\item[$\bullet$] \textbf{\textit{remote\_tofof\_e}:} ToFoF-E is a metaprover
|
blanchet@43406
|
462 |
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
|
blanchet@43406
|
463 |
servers. This ATP supports a fragment of the TPTP many-typed first-order format
|
blanchet@43406
|
464 |
(TFF). It is supported primarily for experimenting with the
|
blanchet@43587
|
465 |
\textit{type\_sys} $=$ \textit{simple\_types} option (\S\ref{problem-encoding}).
|
blanchet@43406
|
466 |
|
blanchet@38824
|
467 |
\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
|
blanchet@38824
|
468 |
developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
|
blanchet@38824
|
469 |
SInE runs on Geoff Sutcliffe's Miami servers.
|
blanchet@38824
|
470 |
|
blanchet@38824
|
471 |
\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a prover
|
blanchet@38824
|
472 |
developed by Stickel et al.\ \cite{snark}. The remote version of
|
blanchet@38824
|
473 |
SNARK runs on Geoff Sutcliffe's Miami servers.
|
blanchet@40254
|
474 |
|
blanchet@42609
|
475 |
\item[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
|
blanchet@42609
|
476 |
on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
|
blanchet@42609
|
477 |
point).
|
blanchet@42609
|
478 |
|
blanchet@41190
|
479 |
\item[$\bullet$] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
|
blanchet@41190
|
480 |
servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
|
blanchet@41190
|
481 |
point).
|
blanchet@40254
|
482 |
|
blanchet@42611
|
483 |
\item[$\bullet$] \textbf{\textit{remote\_z3\_atp}:} The remote version of ``Z3
|
blanchet@42611
|
484 |
as an ATP'' runs on Geoff Sutcliffe's Miami servers.
|
blanchet@36918
|
485 |
\end{enum}
|
blanchet@36918
|
486 |
|
blanchet@41190
|
487 |
By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever
|
blanchet@43089
|
488 |
the SMT module's \textit{smt\_solver} configuration option is set to) in
|
blanchet@40254
|
489 |
parallel---either locally or remotely, depending on the number of processor
|
blanchet@40254
|
490 |
cores available. For historical reasons, the default value of this option can be
|
blanchet@40254
|
491 |
overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu
|
blanchet@40254
|
492 |
in Proof General.
|
blanchet@36918
|
493 |
|
blanchet@40240
|
494 |
It is a good idea to run several provers in parallel, although it could slow
|
blanchet@40254
|
495 |
down your machine. Running E, SPASS, Vampire, and SInE-E together for 5 seconds
|
blanchet@40254
|
496 |
yields a better success rate than running the most effective of these (Vampire)
|
blanchet@40254
|
497 |
for 120 seconds \cite{boehme-nipkow-2010}.
|
blanchet@40240
|
498 |
|
blanchet@40240
|
499 |
\opnodefault{prover}{string}
|
blanchet@40240
|
500 |
Alias for \textit{provers}.
|
blanchet@40240
|
501 |
|
blanchet@40240
|
502 |
\opnodefault{atps}{string}
|
blanchet@40240
|
503 |
Legacy alias for \textit{provers}.
|
blanchet@36918
|
504 |
|
blanchet@36918
|
505 |
\opnodefault{atp}{string}
|
blanchet@40240
|
506 |
Legacy alias for \textit{provers}.
|
blanchet@36918
|
507 |
|
blanchet@40584
|
508 |
\opdefault{timeout}{float\_or\_none}{\upshape 30}
|
blanchet@40582
|
509 |
Specifies the maximum number of seconds that the automatic provers should spend
|
blanchet@40240
|
510 |
searching for a proof. For historical reasons, the default value of this option
|
blanchet@40240
|
511 |
can be overridden using the option ``Sledgehammer: Time Limit'' from the
|
blanchet@40240
|
512 |
``Isabelle'' menu in Proof General.
|
blanchet@39228
|
513 |
|
blanchet@39227
|
514 |
\opfalse{blocking}{non\_blocking}
|
blanchet@39227
|
515 |
Specifies whether the \textbf{sledgehammer} command should operate
|
blanchet@39227
|
516 |
synchronously. The asynchronous (non-blocking) mode lets the user start proving
|
blanchet@39227
|
517 |
the putative theorem manually while Sledgehammer looks for a proof, but it can
|
blanchet@39227
|
518 |
also be more confusing.
|
blanchet@39227
|
519 |
|
blanchet@43314
|
520 |
\optrue{slicing}{no\_slicing}
|
blanchet@43314
|
521 |
Specifies whether the time allocated to a prover should be sliced into several
|
blanchet@43314
|
522 |
segments, each of which has its own set of possibly prover-dependent options.
|
blanchet@43317
|
523 |
For SPASS and Vampire, the first slice tries the fast but incomplete
|
blanchet@43314
|
524 |
set-of-support (SOS) strategy, whereas the second slice runs without it. For E,
|
blanchet@43317
|
525 |
up to three slices are tried, with different weighted search strategies and
|
blanchet@43314
|
526 |
number of facts. For SMT solvers, several slices are tried with the same options
|
blanchet@43317
|
527 |
each time but fewer and fewer facts. According to benchmarks with a timeout of
|
blanchet@43317
|
528 |
30 seconds, slicing is a valuable optimization, and you should probably leave it
|
blanchet@43317
|
529 |
enabled unless you are conducting experiments. This option is implicitly
|
blanchet@43314
|
530 |
disabled for (short) automatic runs.
|
blanchet@43314
|
531 |
|
blanchet@43314
|
532 |
\nopagebreak
|
blanchet@43314
|
533 |
{\small See also \textit{verbose} (\S\ref{output-format}).}
|
blanchet@43314
|
534 |
|
blanchet@36918
|
535 |
\opfalse{overlord}{no\_overlord}
|
blanchet@36918
|
536 |
Specifies whether Sledgehammer should put its temporary files in
|
blanchet@36918
|
537 |
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
|
blanchet@36918
|
538 |
debugging Sledgehammer but also unsafe if several instances of the tool are run
|
blanchet@36918
|
539 |
simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
|
blanchet@36918
|
540 |
safely remove them after Sledgehammer has run.
|
blanchet@36918
|
541 |
|
blanchet@36918
|
542 |
\nopagebreak
|
blanchet@36918
|
543 |
{\small See also \textit{debug} (\S\ref{output-format}).}
|
blanchet@36918
|
544 |
\end{enum}
|
blanchet@36918
|
545 |
|
blanchet@36918
|
546 |
\subsection{Problem Encoding}
|
blanchet@36918
|
547 |
\label{problem-encoding}
|
blanchet@36918
|
548 |
|
blanchet@36918
|
549 |
\begin{enum}
|
blanchet@36918
|
550 |
\opfalse{explicit\_apply}{implicit\_apply}
|
blanchet@36918
|
551 |
Specifies whether function application should be encoded as an explicit
|
blanchet@40254
|
552 |
``apply'' operator in ATP problems. If the option is set to \textit{false}, each
|
blanchet@40254
|
553 |
function will be directly applied to as many arguments as possible. Enabling
|
blanchet@40254
|
554 |
this option can sometimes help discover higher-order proofs that otherwise would
|
blanchet@40254
|
555 |
not be found.
|
blanchet@36918
|
556 |
|
blanchet@36918
|
557 |
\opfalse{full\_types}{partial\_types}
|
blanchet@43551
|
558 |
Specifies whether full type information is encoded in ATP problems. Enabling
|
blanchet@43601
|
559 |
this option prevents the discovery of type-incorrect proofs, but it can slow
|
blanchet@43601
|
560 |
down the ATP slightly. This option is implicitly enabled for automatic runs. For
|
blanchet@43601
|
561 |
historical reasons, the default value of this option can be overridden using the
|
blanchet@43601
|
562 |
option ``Sledgehammer: Full Types'' from the ``Isabelle'' menu in Proof General.
|
blanchet@43089
|
563 |
|
blanchet@43089
|
564 |
\opdefault{type\_sys}{string}{smart}
|
blanchet@43089
|
565 |
Specifies the type system to use in ATP problems. The option can take the
|
blanchet@43089
|
566 |
following values:
|
blanchet@43089
|
567 |
|
blanchet@43089
|
568 |
\begin{enum}
|
blanchet@43587
|
569 |
%\item[$\bullet$] \textbf{\textit{poly\_types}:} Use the prover's support for
|
blanchet@43587
|
570 |
%polymorphic first-order logic if available; otherwise, fall back on
|
blanchet@43587
|
571 |
%\textit{poly\_preds}.
|
blanchet@43453
|
572 |
|
blanchet@43587
|
573 |
\item[$\bullet$] \textbf{\textit{poly\_preds}:} Types are encoded using a predicate
|
blanchet@43460
|
574 |
$\mathit{has\_type\/}(\tau, t)$ that restricts the range of bound variables.
|
blanchet@43460
|
575 |
Constants are annotated with their types, supplied as extra arguments, to
|
blanchet@43460
|
576 |
resolve overloading.
|
blanchet@43453
|
577 |
|
blanchet@43587
|
578 |
\item[$\bullet$] \textbf{\textit{poly\_tags}:} Each term and subterm is tagged with
|
blanchet@43555
|
579 |
its type using a function $\mathit{type\_info\/}(\tau, t)$.
|
blanchet@43555
|
580 |
|
blanchet@43587
|
581 |
\item[$\bullet$] \textbf{\textit{poly\_args}:}
|
blanchet@43587
|
582 |
Like for the other sound encodings, constants are annotated with their types to
|
blanchet@43587
|
583 |
resolve overloading, but otherwise no type information is encoded.
|
blanchet@43555
|
584 |
|
blanchet@43587
|
585 |
\item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to
|
blanchet@43587
|
586 |
the ATP. Types are simply erased.
|
blanchet@43453
|
587 |
|
blanchet@43587
|
588 |
\item[$\bullet$]
|
blanchet@43587
|
589 |
\textbf{%
|
blanchet@43587
|
590 |
\textit{mono\_preds},
|
blanchet@43587
|
591 |
\textit{mono\_tags},
|
blanchet@43587
|
592 |
\textit{mono\_args}:} \\
|
blanchet@43587
|
593 |
Similar to \textit{poly\_preds}, \textit{poly\_tags}, and \textit{poly\_args},
|
blanchet@43587
|
594 |
respectively, but the problem is additionally monomorphized, meaning that type
|
blanchet@43587
|
595 |
variables are instantiated with heuristically chosen ground types.
|
blanchet@43587
|
596 |
Monomorphization can simplify reasoning but also leads to larger fact bases,
|
blanchet@43587
|
597 |
which can slow down the ATPs.
|
blanchet@43453
|
598 |
|
blanchet@43587
|
599 |
\item[$\bullet$] \textbf{\textit{simple\_types}:} Use the prover's support for
|
blanchet@43587
|
600 |
simply typed first-order logic if available; otherwise, fall back on
|
blanchet@43587
|
601 |
\textit{mangled\_preds}. The problem is monomorphized.
|
blanchet@43587
|
602 |
|
blanchet@43587
|
603 |
\item[$\bullet$]
|
blanchet@43587
|
604 |
\textbf{%
|
blanchet@43587
|
605 |
\textit{mangled\_preds},
|
blanchet@43587
|
606 |
\textit{mangled\_tags},
|
blanchet@43587
|
607 |
\textit{mangled\_args}:} \\
|
blanchet@43587
|
608 |
Similar to
|
blanchet@43587
|
609 |
\textit{mono\_preds}, \textit{mono\_tags}, and \textit{mono\_args},
|
blanchet@43587
|
610 |
respectively but types are mangled in constant names instead of being supplied
|
blanchet@43587
|
611 |
as ground term arguments. The binary predicate $\mathit{has\_type\/}(\tau, t)$
|
blanchet@43587
|
612 |
becomes a unary predicate $\mathit{has\_type\_}\tau(t)$, and the binary function
|
blanchet@43460
|
613 |
$\mathit{type\_info\/}(\tau, t)$ becomes a unary function
|
blanchet@43460
|
614 |
$\mathit{type\_info\_}\tau(t)$.
|
blanchet@43453
|
615 |
|
blanchet@43453
|
616 |
\item[$\bullet$]
|
blanchet@43453
|
617 |
\textbf{%
|
blanchet@43587
|
618 |
\textit{simple\_types}?,
|
blanchet@43587
|
619 |
\{\textit{poly},\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}?:} \\
|
blanchet@43587
|
620 |
The type systems \textit{poly\_preds}, \textit{poly\_tags},
|
blanchet@43587
|
621 |
\textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types},
|
blanchet@43587
|
622 |
\textit{mangled\_preds}, and \textit{mangled\_tags} are fully typed and
|
blanchet@43587
|
623 |
virtually sound---except for pathological cases, all found proofs are
|
blanchet@43587
|
624 |
type-correct. For each of these, Sledgehammer also provides a just-as-sound
|
blanchet@43587
|
625 |
partially typed variant identified by a question mark (`{?}')\ that detects and
|
blanchet@43587
|
626 |
erases monotonic types, notably infinite types. (For \textit{simple\_types}, the
|
blanchet@43587
|
627 |
types are not actually erased but rather replaced by a shared uniform type.)
|
blanchet@43551
|
628 |
|
blanchet@43551
|
629 |
\item[$\bullet$]
|
blanchet@43551
|
630 |
\textbf{%
|
blanchet@43587
|
631 |
\textit{simple\_types}!,
|
blanchet@43587
|
632 |
\{\textit{poly},\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}!:} \\
|
blanchet@43553
|
633 |
If the question mark (`{?}')\ is replaced by an exclamation mark (`{!}'),\ the
|
blanchet@43551
|
634 |
translation erases all types except those that are clearly finite (e.g.,
|
blanchet@43551
|
635 |
\textit{bool}). This encoding is unsound.
|
blanchet@43460
|
636 |
|
blanchet@43098
|
637 |
\item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
|
blanchet@43460
|
638 |
uses a fully typed, virtually sound encoding; otherwise, uses any encoding. The
|
blanchet@43460
|
639 |
actual encoding used depends on the ATP and should be the most efficient for
|
blanchet@43460
|
640 |
that ATP.
|
blanchet@43089
|
641 |
\end{enum}
|
blanchet@43089
|
642 |
|
blanchet@43587
|
643 |
For SMT solvers and ToFoF-E, the type system is always \textit{simple\_types}.
|
blanchet@43394
|
644 |
|
blanchet@43589
|
645 |
\opdefault{max\_mono\_iters}{int}{\upshape 4}
|
blanchet@43394
|
646 |
Specifies the maximum number of iterations for the monomorphization fixpoint
|
blanchet@43394
|
647 |
construction. The higher this limit is, the more monomorphic instances are
|
blanchet@43462
|
648 |
potentially generated. Whether monomorphization takes place depends on the
|
blanchet@43462
|
649 |
type system used.
|
blanchet@43589
|
650 |
|
blanchet@43589
|
651 |
\opdefault{max\_mono\_instances}{int}{\upshape 500}
|
blanchet@43589
|
652 |
Specifies the maximum number of monomorphic instances to generate as a soft
|
blanchet@43589
|
653 |
limit. The higher this limit is, the more monomorphic instances are potentially
|
blanchet@43589
|
654 |
generated. Whether monomorphization takes place depends on the type system used.
|
blanchet@38814
|
655 |
\end{enum}
|
blanchet@36918
|
656 |
|
blanchet@38814
|
657 |
\subsection{Relevance Filter}
|
blanchet@38814
|
658 |
\label{relevance-filter}
|
blanchet@38814
|
659 |
|
blanchet@38814
|
660 |
\begin{enum}
|
blanchet@40584
|
661 |
\opdefault{relevance\_thresholds}{float\_pair}{\upshape 0.45~0.85}
|
blanchet@38985
|
662 |
Specifies the thresholds above which facts are considered relevant by the
|
blanchet@38985
|
663 |
relevance filter. The first threshold is used for the first iteration of the
|
blanchet@38985
|
664 |
relevance filter and the second threshold is used for the last iteration (if it
|
blanchet@38985
|
665 |
is reached). The effective threshold is quadratically interpolated for the other
|
blanchet@40584
|
666 |
iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
|
blanchet@40584
|
667 |
are relevant and 1 only theorems that refer to previously seen constants.
|
blanchet@36918
|
668 |
|
blanchet@40584
|
669 |
\opsmart{max\_relevant}{int\_or\_smart}
|
blanchet@38985
|
670 |
Specifies the maximum number of facts that may be returned by the relevance
|
blanchet@38985
|
671 |
filter. If the option is set to \textit{smart}, it is set to a value that was
|
blanchet@40240
|
672 |
empirically found to be appropriate for the prover. A typical value would be
|
blanchet@40240
|
673 |
300.
|
blanchet@43051
|
674 |
|
blanchet@36918
|
675 |
\end{enum}
|
blanchet@36918
|
676 |
|
blanchet@36918
|
677 |
\subsection{Output Format}
|
blanchet@36918
|
678 |
\label{output-format}
|
blanchet@36918
|
679 |
|
blanchet@36918
|
680 |
\begin{enum}
|
blanchet@36918
|
681 |
|
blanchet@36918
|
682 |
\opfalse{verbose}{quiet}
|
blanchet@36918
|
683 |
Specifies whether the \textbf{sledgehammer} command should explain what it does.
|
blanchet@41456
|
684 |
This option is implicitly disabled for automatic runs.
|
blanchet@36918
|
685 |
|
blanchet@36918
|
686 |
\opfalse{debug}{no\_debug}
|
blanchet@40444
|
687 |
Specifies whether Sledgehammer should display additional debugging information
|
blanchet@40444
|
688 |
beyond what \textit{verbose} already displays. Enabling \textit{debug} also
|
blanchet@41456
|
689 |
enables \textit{verbose} and \textit{blocking} (\S\ref{mode-of-operation})
|
blanchet@41456
|
690 |
behind the scenes. The \textit{debug} option is implicitly disabled for
|
blanchet@41456
|
691 |
automatic runs.
|
blanchet@36918
|
692 |
|
blanchet@36918
|
693 |
\nopagebreak
|
blanchet@36918
|
694 |
{\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
|
blanchet@36918
|
695 |
|
blanchet@36918
|
696 |
\opfalse{isar\_proof}{no\_isar\_proof}
|
blanchet@36918
|
697 |
Specifies whether Isar proofs should be output in addition to one-liner
|
blanchet@36918
|
698 |
\textit{metis} proofs. Isar proof construction is still experimental and often
|
blanchet@36918
|
699 |
fails; however, they are usually faster and sometimes more robust than
|
blanchet@36918
|
700 |
\textit{metis} proofs.
|
blanchet@36918
|
701 |
|
blanchet@40584
|
702 |
\opdefault{isar\_shrink\_factor}{int}{\upshape 1}
|
blanchet@36918
|
703 |
Specifies the granularity of the Isar proof. A value of $n$ indicates that each
|
blanchet@36918
|
704 |
Isar proof step should correspond to a group of up to $n$ consecutive proof
|
blanchet@36918
|
705 |
steps in the ATP proof.
|
blanchet@36918
|
706 |
|
blanchet@36918
|
707 |
\end{enum}
|
blanchet@36918
|
708 |
|
blanchet@39228
|
709 |
\subsection{Authentication}
|
blanchet@39228
|
710 |
\label{authentication}
|
blanchet@36918
|
711 |
|
blanchet@36918
|
712 |
\begin{enum}
|
blanchet@39228
|
713 |
\opnodefault{expect}{string}
|
blanchet@39228
|
714 |
Specifies the expected outcome, which must be one of the following:
|
blanchet@39228
|
715 |
|
blanchet@39228
|
716 |
\begin{enum}
|
blanchet@40444
|
717 |
\item[$\bullet$] \textbf{\textit{some}:} Sledgehammer found a (potentially
|
blanchet@40444
|
718 |
unsound) proof.
|
blanchet@39228
|
719 |
\item[$\bullet$] \textbf{\textit{none}:} Sledgehammer found no proof.
|
blanchet@40444
|
720 |
\item[$\bullet$] \textbf{\textit{unknown}:} Sledgehammer encountered some
|
blanchet@40444
|
721 |
problem.
|
blanchet@39228
|
722 |
\end{enum}
|
blanchet@39228
|
723 |
|
blanchet@39228
|
724 |
Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning
|
blanchet@39228
|
725 |
(otherwise) if the actual outcome differs from the expected outcome. This option
|
blanchet@39228
|
726 |
is useful for regression testing.
|
blanchet@39228
|
727 |
|
blanchet@39228
|
728 |
\nopagebreak
|
blanchet@39228
|
729 |
{\small See also \textit{blocking} (\S\ref{mode-of-operation}).}
|
blanchet@36918
|
730 |
\end{enum}
|
blanchet@36918
|
731 |
|
blanchet@36918
|
732 |
\let\em=\sl
|
blanchet@36918
|
733 |
\bibliography{../manual}{}
|
blanchet@36918
|
734 |
\bibliographystyle{abbrv}
|
blanchet@36918
|
735 |
|
blanchet@36918
|
736 |
\end{document}
|