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