doc-src/Sledgehammer/sledgehammer.tex
author boehmes
Tue, 07 Dec 2010 15:44:38 +0100
changeset 41064 0c447a17770a
parent 40942 e08fa125c268
child 41208 1b28c43a7074
permissions -rw-r--r--
updated SMT certificates
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     1
\documentclass[a4paper,12pt]{article}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     2
\usepackage[T1]{fontenc}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     3
\usepackage{amsmath}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     4
\usepackage{amssymb}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     5
\usepackage[english,french]{babel}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     6
\usepackage{color}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     7
\usepackage{footmisc}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     8
\usepackage{graphicx}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     9
%\usepackage{mathpazo}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    10
\usepackage{multicol}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    11
\usepackage{stmaryrd}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    12
%\usepackage[scaled=.85]{beramono}
40689
3a10ce7cd436 document requirement on theory import
blanchet
parents: 40343
diff changeset
    13
\usepackage{../isabelle,../iman,../pdfsetup}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    14
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    15
%\oddsidemargin=4.6mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    16
%\evensidemargin=4.6mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    17
%\textwidth=150mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    18
%\topmargin=4.6mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    19
%\headheight=0mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    20
%\headsep=0mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    21
%\textheight=234mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    22
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    23
\def\Colon{\mathord{:\mkern-1.5mu:}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    24
%\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    25
%\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    26
\def\lparr{\mathopen{(\mkern-4mu\mid}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    27
\def\rparr{\mathclose{\mid\mkern-4mu)}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    28
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    29
\def\unk{{?}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    30
\def\undef{(\lambda x.\; \unk)}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    31
%\def\unr{\textit{others}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    32
\def\unr{\ldots}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    33
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    34
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    35
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    36
\urlstyle{tt}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    37
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    38
\begin{document}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    39
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    40
\selectlanguage{english}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    41
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    42
\title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    43
Hammering Away \\[\smallskipamount]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    44
\Large A User's Guide to Sledgehammer for Isabelle/HOL}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    45
\author{\hbox{} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    46
Jasmin Christian Blanchette \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    47
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    48
\hbox{}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    49
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    50
\maketitle
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    51
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    52
\tableofcontents
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    53
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    54
\setlength{\parskip}{.7em plus .2em minus .1em}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    55
\setlength{\parindent}{0pt}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    56
\setlength{\abovedisplayskip}{\parskip}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    57
\setlength{\abovedisplayshortskip}{.9\parskip}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    58
\setlength{\belowdisplayskip}{\parskip}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    59
\setlength{\belowdisplayshortskip}{.9\parskip}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    60
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    61
% General-purpose enum environment with correct spacing
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    62
\newenvironment{enum}%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    63
    {\begin{list}{}{%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    64
        \setlength{\topsep}{.1\parskip}%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    65
        \setlength{\partopsep}{.1\parskip}%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    66
        \setlength{\itemsep}{\parskip}%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    67
        \advance\itemsep by-\parsep}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    68
    {\end{list}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    69
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    70
\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    71
\advance\rightskip by\leftmargin}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    72
\def\post{\vskip0pt plus1ex\endgroup}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    73
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    74
\def\prew{\pre\advance\rightskip by-\leftmargin}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    75
\def\postw{\post}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    76
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    77
\section{Introduction}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    78
\label{introduction}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    79
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    80
Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs)
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
    81
and satisfiability-modulo-theories (SMT) solvers on the current goal. The
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    82
supported ATPs are E \cite{schulz-2002}, SPASS \cite{weidenbach-et-al-2009},
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    83
Vampire \cite{riazanov-voronkov-2002}, SInE-E \cite{sine}, and SNARK
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    84
\cite{snark}. The ATPs are run either locally or remotely via the
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    85
System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs, the
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
    86
SMT solvers Z3 \cite{z3} is used, and you can tell Sledgehammer to try Yices
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
    87
\cite{yices} and CVC3 \cite{cvc3} as well.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    88
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    89
The problem passed to the automatic provers consists of your current goal
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    90
together with a heuristic selection of hundreds of facts (theorems) from the
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    91
current theory context, filtered by relevance. Because jobs are run in the
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    92
background, you can continue to work on your proof by other means. Provers can
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    93
be run in parallel. Any reply (which may arrive half a minute later) will appear
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    94
in the Proof General response buffer.
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    95
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    96
The result of a successful proof search is some source text that usually (but
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    97
not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    98
proof relies on the general-purpose Metis prover \cite{metis}, which is fully
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    99
integrated into Isabelle/HOL, with explicit inferences going through the kernel.
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   100
Thus its results are correct by construction.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   101
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   102
In this manual, we will explicitly invoke the \textbf{sledgehammer} command.
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   103
Sledgehammer also provides an automatic mode that can be enabled via the
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   104
``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof General. In
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   105
this mode, Sledgehammer is run on every newly entered theorem. The time limit
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   106
for Auto Sledgehammer and other automatic tools can be set using the ``Auto
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   107
Tools Time Limit'' option.
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   108
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   109
\newbox\boxA
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   110
\setbox\boxA=\hbox{\texttt{nospam}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   111
40689
3a10ce7cd436 document requirement on theory import
blanchet
parents: 40343
diff changeset
   112
To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is
3a10ce7cd436 document requirement on theory import
blanchet
parents: 40343
diff changeset
   113
imported---this is rarely a problem in practice since it is part of
3a10ce7cd436 document requirement on theory import
blanchet
parents: 40343
diff changeset
   114
\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   115
\texttt{src/HOL/Metis\_Examples} directory.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   116
Comments and bug reports concerning Sledgehammer or this manual should be
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   117
directed to
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   118
\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   119
in.\allowbreak tum.\allowbreak de}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   120
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   121
\vskip2.5\smallskipamount
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   122
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   123
%\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   124
%suggesting several textual improvements.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   125
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   126
\section{Installation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   127
\label{installation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   128
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   129
Sledgehammer is part of Isabelle, so you don't need to install it. However, it
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   130
relies on third-party automatic theorem provers (ATPs) and SAT solvers.
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   131
Currently, E, SPASS, and Vampire can be run locally; in addition, E, Vampire,
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   132
SInE-E, and SNARK are available remotely via SystemOnTPTP \cite{sutcliffe-2000}.
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   133
If you want better performance, you should install E and SPASS locally.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   134
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   135
There are three main ways to install ATPs on your machine:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   136
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   137
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   138
\item[$\bullet$] If you installed an official Isabelle package with everything
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   139
inside, it should already include properly setup executables for E and SPASS,
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   140
ready to use.%
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   141
\footnote{Vampire's license prevents us from doing the same for this otherwise
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   142
wonderful tool.}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   143
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   144
\item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   145
binary packages from Isabelle's download page. Extract the archives, then add a
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   146
line to your \texttt{\char`\~/.isabelle/etc/components} file with the absolute
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   147
path to E or SPASS. For example, if the \texttt{components} does not exist yet
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   148
and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create the
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   149
\texttt{components} file with the single line
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   150
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   151
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   152
\texttt{/usr/local/spass-3.7}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   153
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   154
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   155
in it.
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   156
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   157
\item[$\bullet$] If you prefer to build E or SPASS yourself, or obtained a
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   158
Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}),
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   159
set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   160
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
38063
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   161
\texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   162
with E 1.0 and 1.2, SPASS 3.5 and 3.7, and Vampire 1.0%
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   163
\footnote{Following the rewrite of Vampire, the counter for version numbers was
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   164
reset to 0; hence the new Vampire 1.0 is more recent than Vampire 11.5.}%
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   165
. Since the ATPs' output formats are neither documented nor stable, other
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   166
versions of the ATPs might or might not work well with Sledgehammer.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   167
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   168
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   169
To check whether E and SPASS are installed, follow the example in
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   170
\S\ref{first-steps}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   171
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   172
Remote ATP invocation via the SystemOnTPTP web service requires Perl with the
39152
f09b378cb252 make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents: 38997
diff changeset
   173
World Wide Web Library (\texttt{libwww-perl}) installed. If you must use a proxy
f09b378cb252 make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents: 38997
diff changeset
   174
server to access the Internet, set the \texttt{http\_proxy} environment variable
39153
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   175
to the proxy, either in the environment in which Isabelle is launched or in your
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   176
\texttt{\char`\~/.isabelle/etc/settings} file. Here are a few examples:
39152
f09b378cb252 make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents: 38997
diff changeset
   177
f09b378cb252 make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents: 38997
diff changeset
   178
\prew
39153
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   179
\texttt{http\_proxy=http://proxy.example.org} \\
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   180
\texttt{http\_proxy=http://proxy.example.org:8080} \\
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   181
\texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org}
39152
f09b378cb252 make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents: 38997
diff changeset
   182
\postw
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   183
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   184
\section{First Steps}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   185
\label{first-steps}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   186
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   187
To illustrate Sledgehammer in context, let us start a theory file and
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   188
attempt to prove a simple lemma:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   189
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   190
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   191
\textbf{theory}~\textit{Scratch} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   192
\textbf{imports}~\textit{Main} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   193
\textbf{begin} \\[2\smallskipamount]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   194
%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   195
\textbf{lemma} ``$[a] = [b] \,\longleftrightarrow\, a = b$'' \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   196
\textbf{sledgehammer}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   197
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   198
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   199
Instead of issuing the \textbf{sledgehammer} command, you can also find
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   200
Sledgehammer in the ``Commands'' submenu of the ``Isabelle'' menu in Proof
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   201
General or press the Emacs key sequence C-c C-a C-s.
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   202
Either way, Sledgehammer produces the following output after a few seconds:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   203
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   204
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   205
\slshape
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   206
Sledgehammer: ``\textit{e}'' for subgoal 1: \\
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   207
$([a] = [b]) = (a = b)$ \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   208
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   209
To minimize the number of lemmas, try this: \\
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   210
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   211
%
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   212
Sledgehammer: ``\textit{spass}'' for subgoal 1: \\
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   213
$([a] = [b]) = (a = b)$ \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   214
Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   215
To minimize the number of lemmas, try this: \\
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   216
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   217
%
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   218
Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   219
$([a] = [b]) = (a = b)$ \\
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   220
Try this command: \textbf{by} (\textit{metis eq\_commute last\_snoc}) \\
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   221
To minimize the number of lemmas, try this: \\
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   222
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}]~(\textit{eq\_commute last\_snoc}). \\[3\smallskipamount]
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   223
%
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   224
Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   225
$([a] = [b]) = (a = b)$ \\
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   226
Try this command: \textbf{by} (\textit{metis hd.simps}) \\
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   227
To minimize the number of lemmas, try this: \\
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   228
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   229
%
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   230
Sledgehammer: ``\textit{remote\_z3}'' for subgoal 1: \\
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   231
$([a] = [b]) = (a = b)$ \\
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   232
Try this command: \textbf{by} (\textit{metis hd.simps}) \\
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   233
To minimize the number of lemmas, try this: \\
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   234
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   235
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   236
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   237
Sledgehammer ran E, SPASS, Vampire, SInE-E, and Z3 in parallel. Depending on
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   238
which provers are installed and how many processor cores are available, some of
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   239
the provers might be missing or present with a \textit{remote\_} prefix.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   240
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   241
For each successful prover, Sledgehammer gives a one-liner proof that uses the
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   242
\textit{metis} or \textit{smt} method. You can click the proof to insert it into
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   243
the theory text. You can click the ``\textbf{sledgehammer} \textit{minimize}''
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   244
command if you want to look for a shorter (and probably faster) proof. But here
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   245
the proof found by E looks perfect, so click it to finish the proof.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   246
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   247
You can ask Sledgehammer for an Isar text proof by passing the
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   248
\textit{isar\_proof} option:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   249
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   250
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   251
\textbf{sledgehammer} [\textit{isar\_proof}]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   252
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   253
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   254
When Isar proof construction is successful, it can yield proofs that are more
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   255
readable and also faster than the \textit{metis} one-liners. This feature is
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   256
experimental and is only available for ATPs.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   257
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   258
\section{Hints}
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   259
\label{hints}
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   260
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   261
For best results, first simplify your problem by calling \textit{auto} or at
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   262
least \textit{safe} followed by \textit{simp\_all}. None of the ATPs contain
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   263
arithmetic decision procedures. They are not especially good at heavy rewriting,
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   264
but because they regard equations as undirected, they often prove theorems that
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   265
require the reverse orientation of a \textit{simp} rule. Higher-order problems
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   266
can be tackled, but the success rate is better for first-order problems. Hence,
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   267
you may get better results if you first simplify the problem to remove
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   268
higher-order features.
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   269
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   270
Note that problems can be easy for \textit{auto} and difficult for ATPs, but the
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   271
reverse is also true, so don't be discouraged if your first attempts fail.
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   272
Because the system refers to all theorems known to Isabelle, it is particularly
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   273
suitable when your goal has a short proof from lemmas that you don't 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
   274
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   275
\section{Command Syntax}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   276
\label{command-syntax}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   277
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   278
Sledgehammer can be invoked at any point when there is an open goal by entering
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   279
the \textbf{sledgehammer} command in the theory file. Its general syntax is as
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   280
follows:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   281
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   282
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   283
\textbf{sledgehammer} \textit{subcommand\/$^?$ options\/$^?$ facts\_override\/$^?$ num\/$^?$}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   284
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   285
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   286
For convenience, Sledgehammer is also available in the ``Commands'' submenu of
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   287
the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   288
C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   289
no arguments in the theory text.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   290
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   291
In the general syntax, the \textit{subcommand} may be any of the following:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   292
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   293
\begin{enum}
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   294
\item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   295
subgoal number \textit{num} (1 by default), with the given options and facts.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   296
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   297
\item[$\bullet$] \textbf{\textit{minimize}:} Attempts to minimize the provided facts
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   298
(specified in the \textit{facts\_override} argument) to obtain a simpler proof
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   299
involving fewer facts. The options and goal number are as for \textit{run}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   300
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   301
\item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   302
by Sledgehammer. This allows you to examine results that might have been lost
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   303
due to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   304
limit on the number of messages to display (5 by default).
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   305
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   306
\item[$\bullet$] \textbf{\textit{available\_provers}:} Prints the list of
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   307
installed provers. See \S\ref{installation} and \S\ref{mode-of-operation} for
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   308
more information on how to install automatic provers.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   309
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   310
\item[$\bullet$] \textbf{\textit{running\_provers}:} Prints information about
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   311
currently running automatic provers, including elapsed runtime and remaining
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   312
time until timeout.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   313
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   314
\item[$\bullet$] \textbf{\textit{kill\_provers}:} Terminates all running
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   315
automatic provers.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   316
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   317
\item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   318
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   319
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   320
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   321
Sledgehammer's behavior can be influenced by various \textit{options}, which can
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   322
be specified in brackets after the \textbf{sledgehammer} command. The
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   323
\textit{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   324
\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true}'' is optional. For
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   325
example:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   326
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   327
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   328
\textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120$\,s$]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   329
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   330
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   331
Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   332
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   333
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   334
\textbf{sledgehammer\_params} \textit{options}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   335
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   336
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   337
The supported options are described in \S\ref{option-reference}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   338
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   339
The \textit{facts\_override} argument lets you alter the set of facts that go
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   340
through the relevance filter. It may be of the form ``(\textit{facts})'', where
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   341
\textit{facts} is a space-separated list of Isabelle facts (theorems, local
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   342
assumptions, etc.), in which case the relevance filter is bypassed and the given
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   343
facts are used. It may also be of the form ``(\textit{add}:\ \textit{facts}$_1$)'',
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   344
``(\textit{del}:\ \textit{facts}$_2$)'', or ``(\textit{add}:\ \textit{facts}$_1$\
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   345
\textit{del}:\ \textit{facts}$_2$)'', where the relevance filter is instructed to
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   346
proceed as usual except that it should consider \textit{facts}$_1$
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   347
highly-relevant and \textit{facts}$_2$ fully irrelevant.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   348
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   349
You can instruct Sledgehammer to run automatically on newly entered theorems by
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   350
enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   351
General. For automatic runs, only the first prover set using \textit{provers}
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   352
(\S\ref{mode-of-operation}) is considered, \textit{verbose}
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   353
(\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled,
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   354
fewer facts are passed to the prover, and \textit{timeout}
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   355
(\S\ref{mode-of-operation}) is superseded by the ``Auto Tools Time Limit'' in
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   356
Proof General's ``Isabelle'' menu. Sledgehammer's output is also more concise.
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   357
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   358
\section{Option Reference}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   359
\label{option-reference}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   360
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   361
\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   362
\def\qty#1{$\left<\textit{#1}\right>$}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   363
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   364
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   365
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   366
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   367
\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   368
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   369
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   370
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   371
\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   372
\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   373
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   374
Sledgehammer's options are categorized as follows:\ mode of operation
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   375
(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   376
relevance filter (\S\ref{relevance-filter}), output format
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   377
(\S\ref{output-format}), and authentication (\S\ref{authentication}).
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   378
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   379
The descriptions below refer to the following syntactic quantities:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   380
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   381
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   382
\item[$\bullet$] \qtybf{string}: A string.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   383
\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   384
\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   385
\textit{smart}.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   386
\item[$\bullet$] \qtybf{int\/}: An integer.
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   387
\item[$\bullet$] \qtybf{float\_pair\/}: A pair of floating-point numbers
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   388
(e.g., 0.6 0.95).
38591
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   389
\item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   390
\item[$\bullet$] \qtybf{float\_or\_none\/}: An integer (e.g., 60) or
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   391
floating-point number (e.g., 0.5) expressing a number of seconds, or the keyword
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   392
\textit{none} ($\infty$ seconds).
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   393
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   394
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   395
Default values are indicated in square brackets. Boolean options have a negated
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   396
counterpart (e.g., \textit{blocking} vs.\ \textit{non\_blocking}). When setting
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   397
Boolean options, ``= \textit{true}'' may be omitted.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   398
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   399
\subsection{Mode of Operation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   400
\label{mode-of-operation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   401
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   402
\begin{enum}
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   403
\opnodefault{provers}{string}
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   404
Specifies the automatic provers to use as a space-separated list (e.g.,
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   405
``\textit{e}~\textit{spass}''). The following provers are supported:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   406
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   407
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   408
\item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   409
\cite{schulz-2002}. To use E, set the environment variable
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   410
\texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable,
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   411
or install the prebuilt E package from Isabelle's download page. See
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   412
\S\ref{installation} for details.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   413
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   414
\item[$\bullet$] \textbf{\textit{spass}:} SPASS is an ATP developed by Christoph
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   415
Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   416
environment variable \texttt{SPASS\_HOME} to the directory that contains the
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   417
\texttt{SPASS} executable, or install the prebuilt SPASS package from Isabelle's
37414
d0cea0796295 expect SPASS 3.7, and give a friendly warning if an older version is used
blanchet
parents: 36926
diff changeset
   418
download page. Sledgehammer requires version 3.5 or above. See
d0cea0796295 expect SPASS 3.7, and give a friendly warning if an older version is used
blanchet
parents: 36926
diff changeset
   419
\S\ref{installation} for details.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   420
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   421
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   422
Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   423
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   424
that contains the \texttt{vampire} executable. Sledgehammer has been tested with
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   425
versions 11, 0.6, and 1.0.
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   426
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   427
\item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   428
Microsoft Research \cite{z3}. To use Z3, set the environment variable
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   429
\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   430
name. Sledgehammer has been tested with 2.7 to 2.15.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   431
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   432
\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   433
SRI \cite{yices}. To use Yices, set the environment variable
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   434
\texttt{YICES\_SOLVER} to the complete path of the executable, including the
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   435
file name. Sledgehammer has been tested with version 1.0.
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   436
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   437
\item[$\bullet$] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   438
Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   439
set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   440
executable, including the file name. Sledgehammer has been tested with version
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   441
2.2.
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   442
38601
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   443
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   444
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   445
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   446
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
38601
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   447
Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   448
38601
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   449
\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   450
developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   451
SInE runs on Geoff Sutcliffe's Miami servers.
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   452
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   453
\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a prover
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   454
developed by Stickel et al.\ \cite{snark}. The remote version of
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   455
SNARK runs on Geoff Sutcliffe's Miami servers.
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   456
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   457
\item[$\bullet$] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   458
servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   459
point).
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   460
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   461
\item[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   462
on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   463
point).
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   464
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   465
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   466
By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   467
the SMT module's \emph{smt\_solver} configuration option is set to) in
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   468
parallel---either locally or remotely, depending on the number of processor
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   469
cores available. For historical reasons, the default value of this option can be
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   470
overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   471
in Proof General.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   472
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   473
It is a good idea to run several provers in parallel, although it could slow
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   474
down your machine. Running E, SPASS, Vampire, and SInE-E together for 5 seconds
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   475
yields a better success rate than running the most effective of these (Vampire)
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   476
for 120 seconds \cite{boehme-nipkow-2010}.
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   477
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   478
\opnodefault{prover}{string}
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   479
Alias for \textit{provers}.
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   480
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   481
\opnodefault{atps}{string}
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   482
Legacy alias for \textit{provers}.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   483
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   484
\opnodefault{atp}{string}
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   485
Legacy alias for \textit{provers}.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   486
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   487
\opdefault{timeout}{float\_or\_none}{\upshape 30}
40341
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40203
diff changeset
   488
Specifies the maximum number of seconds that the automatic provers should spend
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   489
searching for a proof. For historical reasons, the default value of this option
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   490
can be overridden using the option ``Sledgehammer: Time Limit'' from the
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   491
``Isabelle'' menu in Proof General.
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   492
38983
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   493
\opfalse{blocking}{non\_blocking}
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   494
Specifies whether the \textbf{sledgehammer} command should operate
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   495
synchronously. The asynchronous (non-blocking) mode lets the user start proving
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   496
the putative theorem manually while Sledgehammer looks for a proof, but it can
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   497
also be more confusing.
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   498
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   499
\opfalse{overlord}{no\_overlord}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   500
Specifies whether Sledgehammer should put its temporary files in
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   501
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   502
debugging Sledgehammer but also unsafe if several instances of the tool are run
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   503
simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   504
safely remove them after Sledgehammer has run.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   505
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   506
\nopagebreak
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   507
{\small See also \textit{debug} (\S\ref{output-format}).}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   508
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   509
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   510
\subsection{Problem Encoding}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   511
\label{problem-encoding}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   512
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   513
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   514
\opfalse{explicit\_apply}{implicit\_apply}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   515
Specifies whether function application should be encoded as an explicit
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   516
``apply'' operator in ATP problems. If the option is set to \textit{false}, each
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   517
function will be directly applied to as many arguments as possible. Enabling
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   518
this option can sometimes help discover higher-order proofs that otherwise would
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   519
not be found.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   520
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   521
\opfalse{full\_types}{partial\_types}
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   522
Specifies whether full-type information is encoded in ATP problems. Enabling
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   523
this option can prevent the discovery of type-incorrect proofs, but it also
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   524
tends to slow down the ATPs significantly. For historical reasons, the default
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   525
value of this option can be overridden using the option ``Sledgehammer: Full
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   526
Types'' from the ``Isabelle'' menu in Proof General.
38591
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   527
\end{enum}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   528
38591
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   529
\subsection{Relevance Filter}
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   530
\label{relevance-filter}
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   531
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   532
\begin{enum}
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   533
\opdefault{relevance\_thresholds}{float\_pair}{\upshape 0.45~0.85}
38746
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   534
Specifies the thresholds above which facts are considered relevant by the
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   535
relevance filter. The first threshold is used for the first iteration of the
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   536
relevance filter and the second threshold is used for the last iteration (if it
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   537
is reached). The effective threshold is quadratically interpolated for the other
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   538
iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   539
are relevant and 1 only theorems that refer to previously seen constants.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   540
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   541
\opsmart{max\_relevant}{int\_or\_smart}
38746
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   542
Specifies the maximum number of facts that may be returned by the relevance
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   543
filter. If the option is set to \textit{smart}, it is set to a value that was
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   544
empirically found to be appropriate for the prover. A typical value would be
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   545
300.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   546
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   547
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   548
\subsection{Output Format}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   549
\label{output-format}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   550
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   551
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   552
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   553
\opfalse{verbose}{quiet}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   554
Specifies whether the \textbf{sledgehammer} command should explain what it does.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   555
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   556
\opfalse{debug}{no\_debug}
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   557
Specifies whether Sledgehammer should display additional debugging information
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   558
beyond what \textit{verbose} already displays. Enabling \textit{debug} also
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   559
enables \textit{verbose} behind the scenes.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   560
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   561
\nopagebreak
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   562
{\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   563
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   564
\opfalse{isar\_proof}{no\_isar\_proof}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   565
Specifies whether Isar proofs should be output in addition to one-liner
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   566
\textit{metis} proofs. Isar proof construction is still experimental and often
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   567
fails; however, they are usually faster and sometimes more robust than
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   568
\textit{metis} proofs.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   569
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   570
\opdefault{isar\_shrink\_factor}{int}{\upshape 1}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   571
Specifies the granularity of the Isar proof. A value of $n$ indicates that each
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   572
Isar proof step should correspond to a group of up to $n$ consecutive proof
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   573
steps in the ATP proof.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   574
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   575
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   576
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   577
\subsection{Authentication}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   578
\label{authentication}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   579
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   580
\begin{enum}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   581
\opnodefault{expect}{string}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   582
Specifies the expected outcome, which must be one of the following:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   583
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   584
\begin{enum}
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   585
\item[$\bullet$] \textbf{\textit{some}:} Sledgehammer found a (potentially
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   586
unsound) proof.
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   587
\item[$\bullet$] \textbf{\textit{none}:} Sledgehammer found no proof.
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   588
\item[$\bullet$] \textbf{\textit{unknown}:} Sledgehammer encountered some
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   589
problem.
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   590
\end{enum}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   591
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   592
Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   593
(otherwise) if the actual outcome differs from the expected outcome. This option
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   594
is useful for regression testing.
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   595
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   596
\nopagebreak
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   597
{\small See also \textit{blocking} (\S\ref{mode-of-operation}).}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   598
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   599
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   600
\let\em=\sl
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   601
\bibliography{../manual}{}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   602
\bibliographystyle{abbrv}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   603
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   604
\end{document}