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}
|
blanchet@36918
|
13 |
\usepackage{../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@36918
|
81 |
on the current goal. The supported ATPs are E \cite{schulz-2002}, SPASS
|
blanchet@36918
|
82 |
\cite{weidenbach-et-al-2009}, and Vampire \cite{riazanov-voronkov-2002}, which
|
blanchet@36918
|
83 |
can be run locally or remotely via the SystemOnTPTP web service
|
blanchet@36918
|
84 |
\cite{sutcliffe-2000}.
|
blanchet@36918
|
85 |
|
blanchet@37517
|
86 |
The problem passed to ATPs consists of your current goal together with a
|
blanchet@37517
|
87 |
heuristic selection of hundreds of facts (theorems) from the current theory
|
blanchet@37517
|
88 |
context, filtered by relevance. Because jobs are run in the background, you can
|
blanchet@37517
|
89 |
continue to work on your proof by other means. Provers can be run in parallel.
|
blanchet@37517
|
90 |
Any reply (which may arrive minutes later) will appear in the Proof General
|
blanchet@37517
|
91 |
response buffer.
|
blanchet@37517
|
92 |
|
blanchet@37517
|
93 |
The result of a successful ATP proof search is some source text that usually
|
blanchet@37517
|
94 |
(but not always) reconstructs the proof within Isabelle, without requiring the
|
blanchet@37517
|
95 |
ATPs again. The reconstructed proof relies on the general-purpose Metis prover
|
blanchet@37517
|
96 |
\cite{metis}, which is fully integrated into Isabelle/HOL, with explicit
|
blanchet@37517
|
97 |
inferences going through the kernel. Thus its results are correct by
|
blanchet@37517
|
98 |
construction.
|
blanchet@36918
|
99 |
|
blanchet@36918
|
100 |
\newbox\boxA
|
blanchet@36918
|
101 |
\setbox\boxA=\hbox{\texttt{nospam}}
|
blanchet@36918
|
102 |
|
blanchet@36918
|
103 |
Examples of Sledgehammer use can be found in Isabelle's
|
blanchet@36918
|
104 |
\texttt{src/HOL/Metis\_Examples} directory.
|
blanchet@36918
|
105 |
Comments and bug reports concerning Sledgehammer or this manual should be
|
blanchet@36918
|
106 |
directed to
|
blanchet@36918
|
107 |
\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
|
blanchet@36918
|
108 |
in.\allowbreak tum.\allowbreak de}.
|
blanchet@36918
|
109 |
|
blanchet@36918
|
110 |
\vskip2.5\smallskipamount
|
blanchet@36918
|
111 |
|
blanchet@36918
|
112 |
%\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
|
blanchet@36918
|
113 |
%suggesting several textual improvements.
|
blanchet@36918
|
114 |
|
blanchet@36918
|
115 |
\section{Installation}
|
blanchet@36918
|
116 |
\label{installation}
|
blanchet@36918
|
117 |
|
blanchet@36918
|
118 |
Sledgehammer is part of Isabelle, so you don't need to install it. However, it
|
blanchet@36918
|
119 |
relies on third-party automatic theorem provers (ATPs). Currently, E, SPASS, and
|
blanchet@36918
|
120 |
Vampire are supported. All of these are available remotely via SystemOnTPTP
|
blanchet@36918
|
121 |
\cite{sutcliffe-2000}, but if you want better performance you will need to
|
blanchet@36918
|
122 |
install at least E and SPASS locally.
|
blanchet@36918
|
123 |
|
blanchet@38289
|
124 |
There are three main ways to install ATPs on your machine:
|
blanchet@36918
|
125 |
|
blanchet@36918
|
126 |
\begin{enum}
|
blanchet@36918
|
127 |
\item[$\bullet$] If you installed an official Isabelle package with everything
|
blanchet@36918
|
128 |
inside, it should already include properly setup executables for E and SPASS,
|
blanchet@38289
|
129 |
ready to use.%
|
blanchet@38289
|
130 |
\footnote{Vampire's license prevents us from doing the same for this otherwise
|
blanchet@38289
|
131 |
wonderful tool.}
|
blanchet@36918
|
132 |
|
blanchet@38289
|
133 |
\item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS
|
blanchet@36918
|
134 |
binary packages from Isabelle's download page. Extract the archives, then add a
|
blanchet@36918
|
135 |
line to your \texttt{\char`\~/.isabelle/etc/components} file with the absolute path to
|
blanchet@38289
|
136 |
E or SPASS. For example, if the \texttt{components} does not exist
|
blanchet@36918
|
137 |
yet and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create
|
blanchet@38289
|
138 |
the \texttt{components} file with the single line
|
blanchet@36918
|
139 |
|
blanchet@36918
|
140 |
\prew
|
blanchet@36918
|
141 |
\texttt{/usr/local/spass-3.7}
|
blanchet@36918
|
142 |
\postw
|
blanchet@36918
|
143 |
|
blanchet@38289
|
144 |
in it.
|
blanchet@38289
|
145 |
|
blanchet@38289
|
146 |
\item[$\bullet$] If you prefer to build E or SPASS yourself, or obtained a
|
blanchet@38289
|
147 |
Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}),
|
blanchet@38289
|
148 |
set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
|
blanchet@38289
|
149 |
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
|
blanchet@38309
|
150 |
\texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
|
blanchet@38309
|
151 |
with E 1.0 and 1.2, SPASS 3.5 and 3.7, and Vampire 1.0%
|
blanchet@38309
|
152 |
\footnote{Following the rewrite of Vampire, the counter for version numbers was
|
blanchet@38309
|
153 |
reset to 0; hence the new Vampire 1.0 is more recent than Vampire 11.5.}%
|
blanchet@38309
|
154 |
. Since the ATPs' output formats are neither documented nor stable, other
|
blanchet@38309
|
155 |
versions of the ATPs might or might not work well with Sledgehammer.
|
blanchet@36918
|
156 |
\end{enum}
|
blanchet@36918
|
157 |
|
blanchet@36918
|
158 |
To check whether E and SPASS are installed, follow the example in
|
blanchet@36918
|
159 |
\S\ref{first-steps}.
|
blanchet@36918
|
160 |
|
blanchet@37517
|
161 |
Remote ATP invocation via the SystemOnTPTP web service requires Perl with the
|
blanchet@37517
|
162 |
World Wide Web Library (\texttt{libwww-perl}) installed.
|
blanchet@37517
|
163 |
|
blanchet@36918
|
164 |
\section{First Steps}
|
blanchet@36918
|
165 |
\label{first-steps}
|
blanchet@36918
|
166 |
|
blanchet@36918
|
167 |
To illustrate Sledgehammer in context, let us start a theory file and
|
blanchet@36918
|
168 |
attempt to prove a simple lemma:
|
blanchet@36918
|
169 |
|
blanchet@36918
|
170 |
\prew
|
blanchet@36918
|
171 |
\textbf{theory}~\textit{Scratch} \\
|
blanchet@36918
|
172 |
\textbf{imports}~\textit{Main} \\
|
blanchet@36918
|
173 |
\textbf{begin} \\[2\smallskipamount]
|
blanchet@36918
|
174 |
%
|
blanchet@36918
|
175 |
\textbf{lemma} ``$[a] = [b] \,\longleftrightarrow\, a = b$'' \\
|
blanchet@36918
|
176 |
\textbf{sledgehammer}
|
blanchet@36918
|
177 |
\postw
|
blanchet@36918
|
178 |
|
blanchet@37517
|
179 |
Instead of issuing the \textbf{sledgehammer} command, you can also find
|
blanchet@37517
|
180 |
Sledgehammer in the ``Commands'' submenu of the ``Isabelle'' menu in Proof
|
blanchet@37517
|
181 |
General or press the Emacs key sequence C-c C-a C-s.
|
blanchet@37517
|
182 |
Either way, Sledgehammer produces the following output after a few seconds:
|
blanchet@36918
|
183 |
|
blanchet@36918
|
184 |
\prew
|
blanchet@36918
|
185 |
\slshape
|
blanchet@36918
|
186 |
Sledgehammer: ATP ``\textit{e}'' for subgoal 1: \\
|
blanchet@36918
|
187 |
$([a] = [b]) = (a = b)$ \\
|
blanchet@36918
|
188 |
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
|
blanchet@38289
|
189 |
To minimize the number of lemmas, try this: \\
|
blanchet@36918
|
190 |
\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
|
blanchet@36918
|
191 |
%
|
blanchet@36918
|
192 |
Sledgehammer: ATP ``\textit{spass}'' for subgoal 1: \\
|
blanchet@36918
|
193 |
$([a] = [b]) = (a = b)$ \\
|
blanchet@36918
|
194 |
Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
|
blanchet@38289
|
195 |
To minimize the number of lemmas, try this: \\
|
blanchet@36918
|
196 |
\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
|
blanchet@36918
|
197 |
%
|
blanchet@36918
|
198 |
Sledgehammer: ATP ``\textit{remote\_vampire}'' for subgoal 1: \\
|
blanchet@36918
|
199 |
$([a] = [b]) = (a = b)$ \\
|
blanchet@36918
|
200 |
Try this command: \textbf{by} (\textit{metis One\_nat\_def\_raw empty\_replicate} \\
|
blanchet@36918
|
201 |
\phantom{Try this command: \textbf{by} (\textit{metis~}}\textit{insert\_Nil last\_ConsL replicate\_Suc}). \\
|
blanchet@38289
|
202 |
To minimize the number of lemmas, try this: \\
|
blanchet@36918
|
203 |
\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{remote\_vampire}] \\
|
blanchet@36918
|
204 |
\phantom{\textbf{sledgehammer}~}(\textit{One\_nat\_def\_raw empty\_replicate insert\_Nil} \\
|
blanchet@36918
|
205 |
\phantom{\textbf{sledgehammer}~(}\textit{last\_ConsL replicate\_Suc}).
|
blanchet@36918
|
206 |
\postw
|
blanchet@36918
|
207 |
|
blanchet@36918
|
208 |
Sledgehammer ran E, SPASS, and the remote version of Vampire in parallel. If E
|
blanchet@38289
|
209 |
is not installed (\S\ref{installation}), you will see references to
|
blanchet@38289
|
210 |
its remote American cousin \textit{remote\_e} instead of
|
blanchet@38289
|
211 |
\textit{e}; and if SPASS is not installed, it will not appear in the output.
|
blanchet@36918
|
212 |
|
blanchet@36918
|
213 |
Based on each ATP proof, Sledgehammer gives a one-liner proof that uses the
|
blanchet@36918
|
214 |
\textit{metis} method. You can click them and insert them into the theory text.
|
blanchet@36918
|
215 |
You can click the ``\textbf{sledgehammer} \textit{minimize}'' command if you
|
blanchet@36918
|
216 |
want to look for a shorter (and faster) proof. But here the proof found by E
|
blanchet@36918
|
217 |
looks perfect, so click it to finish the proof.
|
blanchet@36918
|
218 |
|
blanchet@36918
|
219 |
You can ask Sledgehammer for an Isar text proof by passing the
|
blanchet@36918
|
220 |
\textit{isar\_proof} option:
|
blanchet@36918
|
221 |
|
blanchet@36918
|
222 |
\prew
|
blanchet@36918
|
223 |
\textbf{sledgehammer} [\textit{isar\_proof}]
|
blanchet@36918
|
224 |
\postw
|
blanchet@36918
|
225 |
|
blanchet@36918
|
226 |
When Isar proof construction is successful, it can yield proofs that are more
|
blanchet@36918
|
227 |
readable and also faster than the \textit{metis} one-liners. This feature is
|
blanchet@36918
|
228 |
experimental.
|
blanchet@36918
|
229 |
|
blanchet@37517
|
230 |
\section{Hints}
|
blanchet@37517
|
231 |
\label{hints}
|
blanchet@37517
|
232 |
|
blanchet@37517
|
233 |
For best results, first simplify your problem by calling \textit{auto} or at
|
blanchet@37517
|
234 |
least \textit{safe} followed by \textit{simp\_all}. None of the ATPs contain
|
blanchet@37517
|
235 |
arithmetic decision procedures. They are not especially good at heavy rewriting,
|
blanchet@37517
|
236 |
but because they regard equations as undirected, they often prove theorems that
|
blanchet@37517
|
237 |
require the reverse orientation of a \textit{simp} rule. Higher-order problems
|
blanchet@37517
|
238 |
can be tackled, but the success rate is better for first-order problems. Hence,
|
blanchet@37517
|
239 |
you may get better results if you first simplify the problem to remove
|
blanchet@37517
|
240 |
higher-order features.
|
blanchet@37517
|
241 |
|
blanchet@37517
|
242 |
Note that problems can be easy for auto and difficult for ATPs, but the reverse
|
blanchet@37517
|
243 |
is also true, so don't be discouraged if your first attempts fail. Because the
|
blanchet@37517
|
244 |
system refers to all theorems known to Isabelle, it is particularly suitable
|
blanchet@37517
|
245 |
when your goal has a short proof from lemmas that you don't know about.
|
blanchet@37517
|
246 |
|
blanchet@36918
|
247 |
\section{Command Syntax}
|
blanchet@36918
|
248 |
\label{command-syntax}
|
blanchet@36918
|
249 |
|
blanchet@36918
|
250 |
Sledgehammer can be invoked at any point when there is an open goal by entering
|
blanchet@36918
|
251 |
the \textbf{sledgehammer} command in the theory file. Its general syntax is as
|
blanchet@36918
|
252 |
follows:
|
blanchet@36918
|
253 |
|
blanchet@36918
|
254 |
\prew
|
blanchet@36918
|
255 |
\textbf{sledgehammer} \textit{subcommand\/$^?$ options\/$^?$ facts\_override\/$^?$ num\/$^?$}
|
blanchet@36918
|
256 |
\postw
|
blanchet@36918
|
257 |
|
blanchet@36918
|
258 |
For convenience, Sledgehammer is also available in the ``Commands'' submenu of
|
blanchet@36918
|
259 |
the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c
|
blanchet@36918
|
260 |
C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with
|
blanchet@36918
|
261 |
no arguments in the theory text.
|
blanchet@36918
|
262 |
|
blanchet@36918
|
263 |
In the general syntax, the \textit{subcommand} may be any of the following:
|
blanchet@36918
|
264 |
|
blanchet@36918
|
265 |
\begin{enum}
|
blanchet@36918
|
266 |
\item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on subgoal number
|
blanchet@36918
|
267 |
\textit{num} (1 by default), with the given options and facts.
|
blanchet@36918
|
268 |
|
blanchet@36918
|
269 |
\item[$\bullet$] \textbf{\textit{minimize}:} Attempts to minimize the provided facts
|
blanchet@36918
|
270 |
(specified in the \textit{facts\_override} argument) to obtain a simpler proof
|
blanchet@36918
|
271 |
involving fewer facts. The options and goal number are as for \textit{run}.
|
blanchet@36918
|
272 |
|
blanchet@36918
|
273 |
\item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued by
|
blanchet@36918
|
274 |
Sledgehammer. This allows you to examine results that might have been lost due
|
blanchet@36918
|
275 |
to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
|
blanchet@36918
|
276 |
limit on the number of messages to display (5 by default).
|
blanchet@36918
|
277 |
|
blanchet@36918
|
278 |
\item[$\bullet$] \textbf{\textit{available\_atps}:} Prints the list of installed ATPs.
|
blanchet@36918
|
279 |
See \S\ref{installation} and \S\ref{mode-of-operation} for more information on
|
blanchet@36918
|
280 |
how to install ATPs.
|
blanchet@36918
|
281 |
|
blanchet@36918
|
282 |
\item[$\bullet$] \textbf{\textit{running\_atps}:} Prints information about currently
|
blanchet@36918
|
283 |
running ATPs, including elapsed runtime and remaining time until timeout.
|
blanchet@36918
|
284 |
|
blanchet@36918
|
285 |
\item[$\bullet$] \textbf{\textit{kill\_atps}:} Terminates all running ATPs.
|
blanchet@36918
|
286 |
|
blanchet@36918
|
287 |
\item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
|
blanchet@36918
|
288 |
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
|
blanchet@36918
|
289 |
\end{enum}
|
blanchet@36918
|
290 |
|
blanchet@36918
|
291 |
Sledgehammer's behavior can be influenced by various \textit{options}, which can
|
blanchet@36918
|
292 |
be specified in brackets after the \textbf{sledgehammer} command. The
|
blanchet@36918
|
293 |
\textit{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
|
blanchet@36918
|
294 |
\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true}'' is optional. For
|
blanchet@36918
|
295 |
example:
|
blanchet@36918
|
296 |
|
blanchet@36918
|
297 |
\prew
|
blanchet@36918
|
298 |
\textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120$\,s$]
|
blanchet@36918
|
299 |
\postw
|
blanchet@36918
|
300 |
|
blanchet@36918
|
301 |
Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
|
blanchet@36918
|
302 |
|
blanchet@36918
|
303 |
\prew
|
blanchet@36918
|
304 |
\textbf{sledgehammer\_params} \textit{options}
|
blanchet@36918
|
305 |
\postw
|
blanchet@36918
|
306 |
|
blanchet@36918
|
307 |
The supported options are described in \S\ref{option-reference}.
|
blanchet@36918
|
308 |
|
blanchet@36918
|
309 |
The \textit{facts\_override} argument lets you alter the set of facts that go
|
blanchet@36918
|
310 |
through the relevance filter. It may be of the form ``(\textit{facts})'', where
|
blanchet@36918
|
311 |
\textit{facts} is a space-separated list of Isabelle facts (theorems, local
|
blanchet@36918
|
312 |
assumptions, etc.), in which case the relevance filter is bypassed and the given
|
blanchet@36918
|
313 |
facts are used. It may also be of the form (\textit{add}:\ \textit{facts}$_1$),
|
blanchet@36918
|
314 |
(\textit{del}:\ \textit{facts}$_2$), or (\textit{add}:\ \textit{facts}$_1$\
|
blanchet@36918
|
315 |
\textit{del}:\ \textit{facts}$_2$), where the relevance filter is instructed to
|
blanchet@36918
|
316 |
proceed as usual except that it should consider \textit{facts}$_1$
|
blanchet@36918
|
317 |
highly-relevant and \textit{facts}$_2$ fully irrelevant.
|
blanchet@36918
|
318 |
|
blanchet@36918
|
319 |
\section{Option Reference}
|
blanchet@36918
|
320 |
\label{option-reference}
|
blanchet@36918
|
321 |
|
blanchet@36918
|
322 |
\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
|
blanchet@36918
|
323 |
\def\qty#1{$\left<\textit{#1}\right>$}
|
blanchet@36918
|
324 |
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
|
blanchet@36918
|
325 |
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
|
blanchet@36918
|
326 |
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
|
blanchet@36918
|
327 |
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
|
blanchet@36918
|
328 |
\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
|
329 |
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
|
blanchet@36918
|
330 |
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
|
blanchet@36918
|
331 |
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
|
blanchet@36918
|
332 |
\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
|
blanchet@36918
|
333 |
\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
|
blanchet@36918
|
334 |
|
blanchet@36918
|
335 |
Sledgehammer's options are categorized as follows:\ mode of operation
|
blanchet@36918
|
336 |
(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), output
|
blanchet@36918
|
337 |
format (\S\ref{output-format}), and timeouts (\S\ref{timeouts}).
|
blanchet@36918
|
338 |
|
blanchet@36918
|
339 |
The descriptions below refer to the following syntactic quantities:
|
blanchet@36918
|
340 |
|
blanchet@36918
|
341 |
\begin{enum}
|
blanchet@36918
|
342 |
\item[$\bullet$] \qtybf{string}: A string.
|
blanchet@36918
|
343 |
\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
|
blanchet@36918
|
344 |
\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
|
blanchet@36918
|
345 |
\item[$\bullet$] \qtybf{int\/}: An integer.
|
blanchet@38814
|
346 |
\item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
|
blanchet@36918
|
347 |
\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
|
blanchet@36918
|
348 |
(milliseconds), or the keyword \textit{none} ($\infty$ years).
|
blanchet@36918
|
349 |
\end{enum}
|
blanchet@36918
|
350 |
|
blanchet@36918
|
351 |
Default values are indicated in square brackets. Boolean options have a negated
|
blanchet@36918
|
352 |
counterpart (e.g., \textit{debug} vs.\ \textit{no\_debug}). When setting
|
blanchet@36918
|
353 |
Boolean options, ``= \textit{true}'' may be omitted.
|
blanchet@36918
|
354 |
|
blanchet@36918
|
355 |
\subsection{Mode of Operation}
|
blanchet@36918
|
356 |
\label{mode-of-operation}
|
blanchet@36918
|
357 |
|
blanchet@36918
|
358 |
\begin{enum}
|
blanchet@36918
|
359 |
%\optrue{blocking}{non\_blocking}
|
blanchet@36918
|
360 |
%Specifies whether the \textbf{sledgehammer} command should operate synchronously.
|
blanchet@36918
|
361 |
%The asynchronous (non-blocking) mode lets the user start proving the putative
|
blanchet@36918
|
362 |
%theorem while Sledgehammer looks for a counterexample, but it can also be more
|
blanchet@36918
|
363 |
%confusing. For technical reasons, automatic runs currently always block.
|
blanchet@36918
|
364 |
|
blanchet@36918
|
365 |
\opnodefault{atps}{string}
|
blanchet@36918
|
366 |
Specifies the ATPs (automated theorem provers) to use as a space-separated list
|
blanchet@36918
|
367 |
(e.g., ``\textit{e}~\textit{spass}''). The following ATPs are supported:
|
blanchet@36918
|
368 |
|
blanchet@36918
|
369 |
\begin{enum}
|
blanchet@36918
|
370 |
\item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz
|
blanchet@36918
|
371 |
\cite{schulz-2002}. To use E, set the environment variable
|
blanchet@36918
|
372 |
\texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable,
|
blanchet@36918
|
373 |
or install the prebuilt E package from Isabelle's download page. See
|
blanchet@36918
|
374 |
\S\ref{installation} for details.
|
blanchet@36918
|
375 |
|
blanchet@36918
|
376 |
\item[$\bullet$] \textbf{\textit{spass}:} SPASS is an ATP developed by Christoph
|
blanchet@36918
|
377 |
Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the
|
blanchet@36918
|
378 |
environment variable \texttt{SPASS\_HOME} to the directory that contains the
|
blanchet@36918
|
379 |
\texttt{SPASS} executable, or install the prebuilt SPASS package from Isabelle's
|
blanchet@37389
|
380 |
download page. Sledgehammer requires version 3.5 or above. See
|
blanchet@37389
|
381 |
\S\ref{installation} for details.
|
blanchet@36918
|
382 |
|
blanchet@36918
|
383 |
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
|
blanchet@36918
|
384 |
Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
|
blanchet@36918
|
385 |
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
|
blanchet@36918
|
386 |
that contains the \texttt{vampire} executable.
|
blanchet@36918
|
387 |
|
blanchet@38824
|
388 |
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
|
blanchet@36918
|
389 |
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
|
blanchet@36918
|
390 |
|
blanchet@36918
|
391 |
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
|
blanchet@38824
|
392 |
Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
|
blanchet@36918
|
393 |
|
blanchet@38824
|
394 |
\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
|
blanchet@38824
|
395 |
developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
|
blanchet@38824
|
396 |
SInE runs on Geoff Sutcliffe's Miami servers.
|
blanchet@38824
|
397 |
|
blanchet@38824
|
398 |
\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a prover
|
blanchet@38824
|
399 |
developed by Stickel et al.\ \cite{snark}. The remote version of
|
blanchet@38824
|
400 |
SNARK runs on Geoff Sutcliffe's Miami servers.
|
blanchet@36918
|
401 |
\end{enum}
|
blanchet@36918
|
402 |
|
blanchet@38824
|
403 |
By default, Sledgehammer will run E, SPASS, Vampire, and SInE-E in parallel.
|
blanchet@38824
|
404 |
For at most two of E, SPASS, and Vampire, it will use any locally installed
|
blanchet@38824
|
405 |
version if available. For historical reasons, the default value of this option
|
blanchet@38824
|
406 |
can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle''
|
blanchet@38824
|
407 |
menu in Proof General.
|
blanchet@36918
|
408 |
|
blanchet@36918
|
409 |
It is a good idea to run several ATPs in parallel, although it could slow down
|
blanchet@38824
|
410 |
your machine. Running E, SPASS, and Vampire together for 5 seconds yields about
|
blanchet@38824
|
411 |
the same success rate as running the most effective of these (Vampire) for 120
|
blanchet@38824
|
412 |
seconds \cite{boehme-nipkow-2010}.
|
blanchet@36918
|
413 |
|
blanchet@36918
|
414 |
\opnodefault{atp}{string}
|
blanchet@36918
|
415 |
Alias for \textit{atps}.
|
blanchet@36918
|
416 |
|
blanchet@36918
|
417 |
\opfalse{overlord}{no\_overlord}
|
blanchet@36918
|
418 |
Specifies whether Sledgehammer should put its temporary files in
|
blanchet@36918
|
419 |
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
|
blanchet@36918
|
420 |
debugging Sledgehammer but also unsafe if several instances of the tool are run
|
blanchet@36918
|
421 |
simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
|
blanchet@36918
|
422 |
safely remove them after Sledgehammer has run.
|
blanchet@36918
|
423 |
|
blanchet@36918
|
424 |
\nopagebreak
|
blanchet@36918
|
425 |
{\small See also \textit{debug} (\S\ref{output-format}).}
|
blanchet@36918
|
426 |
\end{enum}
|
blanchet@36918
|
427 |
|
blanchet@36918
|
428 |
\subsection{Problem Encoding}
|
blanchet@36918
|
429 |
\label{problem-encoding}
|
blanchet@36918
|
430 |
|
blanchet@36918
|
431 |
\begin{enum}
|
blanchet@36918
|
432 |
\opfalse{explicit\_apply}{implicit\_apply}
|
blanchet@36918
|
433 |
Specifies whether function application should be encoded as an explicit
|
blanchet@36918
|
434 |
``apply'' operator. If the option is set to \textit{false}, each function will
|
blanchet@36918
|
435 |
be directly applied to as many arguments as possible. Enabling this option can
|
blanchet@36918
|
436 |
sometimes help discover higher-order proofs that otherwise would not be found.
|
blanchet@36918
|
437 |
|
blanchet@36918
|
438 |
\opfalse{full\_types}{partial\_types}
|
blanchet@36918
|
439 |
Specifies whether full-type information is exported. Enabling this option can
|
blanchet@36918
|
440 |
prevent the discovery of type-incorrect proofs, but it also tends to slow down
|
blanchet@36918
|
441 |
the ATPs significantly. For historical reasons, the default value of this option
|
blanchet@36918
|
442 |
can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle''
|
blanchet@36918
|
443 |
menu in Proof General.
|
blanchet@38814
|
444 |
\end{enum}
|
blanchet@36918
|
445 |
|
blanchet@38814
|
446 |
\subsection{Relevance Filter}
|
blanchet@38814
|
447 |
\label{relevance-filter}
|
blanchet@38814
|
448 |
|
blanchet@38814
|
449 |
\begin{enum}
|
blanchet@36918
|
450 |
\opdefault{relevance\_threshold}{int}{50}
|
blanchet@36918
|
451 |
Specifies the threshold above which facts are considered relevant by the
|
blanchet@36918
|
452 |
relevance filter. The option ranges from 0 to 100, where 0 means that all
|
blanchet@36918
|
453 |
theorems are relevant.
|
blanchet@36918
|
454 |
|
blanchet@36918
|
455 |
\opdefault{relevance\_convergence}{int}{320}
|
blanchet@36918
|
456 |
Specifies the convergence quotient, multiplied by 100, used by the relevance
|
blanchet@36918
|
457 |
filter. This quotient is used by the relevance filter to scale down the
|
blanchet@36918
|
458 |
relevance of facts at each iteration of the filter.
|
blanchet@36918
|
459 |
|
blanchet@38814
|
460 |
\opdefault{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}}
|
blanchet@38814
|
461 |
Specifies the maximum number of facts that may be added during one iteration of
|
blanchet@38814
|
462 |
the relevance filter. If the option is set to \textit{smart}, it is set to a
|
blanchet@38814
|
463 |
value that was empirically found to be appropriate for the ATP. A typical value
|
blanchet@38814
|
464 |
would be 50.
|
blanchet@38814
|
465 |
|
blanchet@36918
|
466 |
\opsmartx{theory\_relevant}{theory\_irrelevant}
|
blanchet@36918
|
467 |
Specifies whether the theory from which a fact comes should be taken into
|
blanchet@36918
|
468 |
consideration by the relevance filter. If the option is set to \textit{smart},
|
blanchet@36918
|
469 |
it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire,
|
blanchet@36918
|
470 |
because empirical results suggest that these are the best settings.
|
blanchet@36918
|
471 |
|
blanchet@36918
|
472 |
\opfalse{defs\_relevant}{defs\_irrelevant}
|
blanchet@36918
|
473 |
Specifies whether the definition of constants occurring in the formula to prove
|
blanchet@36918
|
474 |
should be considered particularly relevant. Enabling this option tends to lead
|
blanchet@36918
|
475 |
to larger problems and typically slows down the ATPs.
|
blanchet@36918
|
476 |
|
blanchet@36918
|
477 |
\end{enum}
|
blanchet@36918
|
478 |
|
blanchet@36918
|
479 |
\subsection{Output Format}
|
blanchet@36918
|
480 |
\label{output-format}
|
blanchet@36918
|
481 |
|
blanchet@36918
|
482 |
\begin{enum}
|
blanchet@36918
|
483 |
|
blanchet@36918
|
484 |
\opfalse{verbose}{quiet}
|
blanchet@36918
|
485 |
Specifies whether the \textbf{sledgehammer} command should explain what it does.
|
blanchet@36918
|
486 |
|
blanchet@36918
|
487 |
\opfalse{debug}{no\_debug}
|
blanchet@36918
|
488 |
Specifies whether Nitpick should display additional debugging information beyond
|
blanchet@36918
|
489 |
what \textit{verbose} already displays. Enabling \textit{debug} also enables
|
blanchet@36918
|
490 |
\textit{verbose} behind the scenes.
|
blanchet@36918
|
491 |
|
blanchet@36918
|
492 |
\nopagebreak
|
blanchet@36918
|
493 |
{\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
|
blanchet@36918
|
494 |
|
blanchet@36918
|
495 |
\opfalse{isar\_proof}{no\_isar\_proof}
|
blanchet@36918
|
496 |
Specifies whether Isar proofs should be output in addition to one-liner
|
blanchet@36918
|
497 |
\textit{metis} proofs. Isar proof construction is still experimental and often
|
blanchet@36918
|
498 |
fails; however, they are usually faster and sometimes more robust than
|
blanchet@36918
|
499 |
\textit{metis} proofs.
|
blanchet@36918
|
500 |
|
blanchet@36918
|
501 |
\opdefault{isar\_shrink\_factor}{int}{1}
|
blanchet@36918
|
502 |
Specifies the granularity of the Isar proof. A value of $n$ indicates that each
|
blanchet@36918
|
503 |
Isar proof step should correspond to a group of up to $n$ consecutive proof
|
blanchet@36918
|
504 |
steps in the ATP proof.
|
blanchet@36918
|
505 |
|
blanchet@36918
|
506 |
\end{enum}
|
blanchet@36918
|
507 |
|
blanchet@36918
|
508 |
\subsection{Timeouts}
|
blanchet@36918
|
509 |
\label{timeouts}
|
blanchet@36918
|
510 |
|
blanchet@36918
|
511 |
\begin{enum}
|
blanchet@36918
|
512 |
\opdefault{timeout}{time}{$\mathbf{60}$ s}
|
blanchet@36918
|
513 |
Specifies the maximum amount of time that the ATPs should spend looking for a
|
blanchet@36918
|
514 |
proof. For historical reasons, the default value of this option can be
|
blanchet@36918
|
515 |
overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle''
|
blanchet@36918
|
516 |
menu in Proof General.
|
blanchet@36918
|
517 |
\end{enum}
|
blanchet@36918
|
518 |
|
blanchet@36918
|
519 |
\let\em=\sl
|
blanchet@36918
|
520 |
\bibliography{../manual}{}
|
blanchet@36918
|
521 |
\bibliographystyle{abbrv}
|
blanchet@36918
|
522 |
|
blanchet@36918
|
523 |
\end{document}
|