doc-src/Sledgehammer/sledgehammer.tex
author blanchet
Fri, 20 May 2011 12:47:59 +0200
changeset 42887 771be1dcfef6
parent 42884 75c94e3319ae
child 42888 4da581400b69
permissions -rw-r--r--
document new type system and soundness properties of the different systems
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}
42511
bf89455ccf9d eliminated copies of isabelle style files;
wenzelm
parents: 42446
diff changeset
    13
\usepackage{../../lib/texinputs/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},
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
    83
Vampire \cite{riazanov-voronkov-2002}, SInE-E \cite{sine}, SNARK
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
    84
\cite{snark}, and ToFoF-E \cite{tofof}. The ATPs are run either locally or
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
    85
remotely via the System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
    86
to the ATPs, the SMT solvers Z3 \cite{z3} is used by default, and you can tell
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
    87
Sledgehammer to try Yices \cite{yices} and CVC3 \cite{cvc3} as well; these
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
    88
are run either locally or on a server in Munich.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    89
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    90
The problem passed to the automatic provers consists of your current goal
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    91
together with a heuristic selection of hundreds of facts (theorems) from the
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    92
current theory context, filtered by relevance. Because jobs are run in the
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    93
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
    94
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
    95
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
    96
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    97
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
    98
not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    99
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
   100
integrated into Isabelle/HOL, with explicit inferences going through the kernel.
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   101
Thus its results are correct by construction.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   102
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   103
In this manual, we will explicitly invoke the \textbf{sledgehammer} command.
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   104
Sledgehammer also provides an automatic mode that can be enabled via the
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   105
``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof General. In
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   106
this mode, Sledgehammer is run on every newly entered theorem. The time limit
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   107
for Auto Sledgehammer and other automatic tools can be set using the ``Auto
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   108
Tools Time Limit'' option.
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   109
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   110
\newbox\boxA
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   111
\setbox\boxA=\hbox{\texttt{nospam}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   112
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   113
\newcommand\authoremail{\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   114
in.\allowbreak tum.\allowbreak de}}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   115
40689
3a10ce7cd436 document requirement on theory import
blanchet
parents: 40343
diff changeset
   116
To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is
3a10ce7cd436 document requirement on theory import
blanchet
parents: 40343
diff changeset
   117
imported---this is rarely a problem in practice since it is part of
3a10ce7cd436 document requirement on theory import
blanchet
parents: 40343
diff changeset
   118
\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   119
\texttt{src/HOL/Metis\_Examples} directory.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   120
Comments and bug reports concerning Sledgehammer or this manual should be
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   121
directed to the author at \authoremail.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   122
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   123
\vskip2.5\smallskipamount
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   124
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   125
%\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   126
%suggesting several textual improvements.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   127
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   128
\section{Installation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   129
\label{installation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   130
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   131
Sledgehammer is part of Isabelle, so you don't need to install it. However, it
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   132
relies on third-party automatic theorem provers (ATPs) and SMT solvers.
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   133
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   134
\subsection{Installing ATPs}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   135
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   136
Currently, E, SPASS, and Vampire can be run locally; in addition, E, Vampire,
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   137
SInE-E, SNARK, and ToFoF-E are available remotely via System\-On\-TPTP
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   138
\cite{sutcliffe-2000}. If you want better performance, you should at least
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   139
install E and SPASS locally.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   140
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   141
There are three main ways to install ATPs on your machine:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   142
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   143
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   144
\item[$\bullet$] If you installed an official Isabelle package with everything
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   145
inside, it should already include properly setup executables for E and SPASS,
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   146
ready to use.%
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   147
\footnote{Vampire's license prevents us from doing the same for this otherwise
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   148
wonderful tool.}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   149
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   150
\item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   151
binary packages from Isabelle's download page. Extract the archives, then add a
41747
f58d4d202924 fix path to etc/settings and etc/components in doc
blanchet
parents: 41740
diff changeset
   152
line to your \texttt{\$ISABELLE\_HOME\_USER/etc/components}%
f58d4d202924 fix path to etc/settings and etc/components in doc
blanchet
parents: 41740
diff changeset
   153
\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
f58d4d202924 fix path to etc/settings and etc/components in doc
blanchet
parents: 41740
diff changeset
   154
startup. Its value can be retrieved by invoking \texttt{isabelle}
f58d4d202924 fix path to etc/settings and etc/components in doc
blanchet
parents: 41740
diff changeset
   155
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
f58d4d202924 fix path to etc/settings and etc/components in doc
blanchet
parents: 41740
diff changeset
   156
file with the absolute
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   157
path to E or SPASS. For example, if the \texttt{components} does not exist yet
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   158
and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create the
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   159
\texttt{components} file with the single line
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   160
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   161
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   162
\texttt{/usr/local/spass-3.7}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   163
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   164
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   165
in it.
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   166
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   167
\item[$\bullet$] If you prefer to build E or SPASS yourself, or obtained a
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   168
Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}),
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   169
set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   170
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
38063
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   171
\texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
42845
94c69e441440 mention version 0.6 of Vampire, since that's what's currently available for download
blanchet
parents: 42763
diff changeset
   172
with E 1.0 and 1.2, SPASS 3.5 and 3.7, and Vampire 0.6 and 1.0%
38063
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   173
\footnote{Following the rewrite of Vampire, the counter for version numbers was
42845
94c69e441440 mention version 0.6 of Vampire, since that's what's currently available for download
blanchet
parents: 42763
diff changeset
   174
reset to 0; hence the (new) Vampire versions 0.6 and 1.0 are more recent than,
94c69e441440 mention version 0.6 of Vampire, since that's what's currently available for download
blanchet
parents: 42763
diff changeset
   175
say, Vampire 11.5.}%
38063
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   176
. Since the ATPs' output formats are neither documented nor stable, other
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   177
versions of the ATPs might or might not work well with Sledgehammer. Ideally,
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   178
also set \texttt{E\_VERSION}, \texttt{SPASS\_VERSION}, or
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   179
\texttt{VAMPIRE\_VERSION} to the ATP's version number (e.g., ``1.2'').
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   180
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   181
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   182
To check whether E and SPASS are successfully installed, follow the example in
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   183
\S\ref{first-steps}. If the remote versions of E and SPASS are used (identified
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   184
by the prefix ``\emph{remote\_}''), or if the local versions fail to solve the
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   185
easy goal presented there, this is a sign that something is wrong with your
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   186
installation.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   187
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   188
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
   189
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
   190
server to access the Internet, set the \texttt{http\_proxy} environment variable
39153
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   191
to the proxy, either in the environment in which Isabelle is launched or in your
41747
f58d4d202924 fix path to etc/settings and etc/components in doc
blanchet
parents: 41740
diff changeset
   192
\texttt{\char`\~/\$ISABELLE\_HOME\_USER/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
   193
f09b378cb252 make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents: 38997
diff changeset
   194
\prew
39153
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   195
\texttt{http\_proxy=http://proxy.example.org} \\
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   196
\texttt{http\_proxy=http://proxy.example.org:8080} \\
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   197
\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
   198
\postw
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   199
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   200
\subsection{Installing SMT Solvers}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   201
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   202
CVC3, Yices, and Z3 can be run locally or remotely on a Munich server. If you
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   203
want better performance and get the ability to replay proofs that rely on the
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   204
\emph{smt} proof method, you should at least install Z3 locally.
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   205
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   206
There are two main ways of installing SMT solvers locally.
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   207
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   208
\begin{enum}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   209
\item[$\bullet$] If you installed an official Isabelle package with everything
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   210
inside, it should already include properly setup executables for CVC3 and Z3,
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   211
ready to use.%
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   212
\footnote{Yices's license prevents us from doing the same for this otherwise
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   213
wonderful tool.}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   214
For Z3, you additionally need to set the environment variable
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   215
\texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a noncommercial
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   216
user.
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   217
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   218
\item[$\bullet$] Otherwise, follow the instructions documented in the \emph{SMT}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   219
theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}).
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   220
\end{enum}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   221
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   222
\section{First Steps}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   223
\label{first-steps}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   224
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   225
To illustrate Sledgehammer in context, let us start a theory file and
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   226
attempt to prove a simple lemma:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   227
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   228
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   229
\textbf{theory}~\textit{Scratch} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   230
\textbf{imports}~\textit{Main} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   231
\textbf{begin} \\[2\smallskipamount]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   232
%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   233
\textbf{lemma} ``$[a] = [b] \,\longleftrightarrow\, a = b$'' \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   234
\textbf{sledgehammer}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   235
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   236
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   237
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
   238
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
   239
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
   240
Either way, Sledgehammer produces the following output after a few seconds:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   241
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   242
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   243
\slshape
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   244
Sledgehammer: ``\textit{e}'' for subgoal 1: \\
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   245
$([a] = [b]) = (a = b)$ \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   246
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   247
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
   248
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   249
%
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   250
Sledgehammer: ``\textit{spass}'' for subgoal 1: \\
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   251
$([a] = [b]) = (a = b)$ \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   252
Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   253
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
   254
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   255
%
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   256
Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   257
$([a] = [b]) = (a = b)$ \\
42846
dfed4dbe5596 minor doc fixes
blanchet
parents: 42845
diff changeset
   258
Try this command: \textbf{by} (\textit{metis eq\_commute last\_snoc}). \\
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   259
To minimize the number of lemmas, try this: \\
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   260
\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
   261
%
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   262
Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   263
$([a] = [b]) = (a = b)$ \\
42846
dfed4dbe5596 minor doc fixes
blanchet
parents: 42845
diff changeset
   264
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   265
To minimize the number of lemmas, try this: \\
42846
dfed4dbe5596 minor doc fixes
blanchet
parents: 42845
diff changeset
   266
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   267
%
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   268
Sledgehammer: ``\textit{remote\_z3}'' for subgoal 1: \\
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   269
$([a] = [b]) = (a = b)$ \\
42846
dfed4dbe5596 minor doc fixes
blanchet
parents: 42845
diff changeset
   270
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   271
To minimize the number of lemmas, try this: \\
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   272
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   273
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   274
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   275
Sledgehammer ran E, SPASS, Vampire, SInE-E, and Z3 in parallel. Depending on
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   276
which provers are installed and how many processor cores are available, some of
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   277
the provers might be missing or present with a \textit{remote\_} prefix.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   278
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   279
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
   280
\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
   281
the theory text. You can click the ``\textbf{sledgehammer} \textit{minimize}''
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   282
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
   283
the proof found by E looks perfect, so click it to finish the proof.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   284
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   285
You can ask Sledgehammer for an Isar text proof by passing the
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   286
\textit{isar\_proof} option (\S\ref{output-format}):
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   287
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   288
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   289
\textbf{sledgehammer} [\textit{isar\_proof}]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   290
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   291
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   292
When Isar proof construction is successful, it can yield proofs that are more
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   293
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
   294
experimental and is only available for ATPs.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   295
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   296
\section{Hints}
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   297
\label{hints}
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   298
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   299
This section presents a few hints that should help you get the most out of
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   300
Sledgehammer and Metis. Frequently (and infrequently) asked questions are
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   301
answered in \S\ref{frequently-asked-questions}.
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   302
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   303
\newcommand\point[1]{{\sl\bfseries#1}\par\nopagebreak}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   304
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   305
\point{Presimplify the goal}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   306
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   307
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
   308
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
   309
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
   310
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
   311
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
   312
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
   313
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
   314
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
   315
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   316
\point{Make sure at least E, SPASS, Vampire, and Z3 are installed}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   317
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   318
Locally installed provers are faster and more reliable than those running on
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   319
servers. See \S\ref{installation} for details on how to install them.
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   320
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   321
\point{Familiarize yourself with the most important options}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   322
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   323
Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   324
the options are very specialized, but serious users of the tool should at least
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   325
familiarize themselves with the following options:
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   326
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   327
\begin{enum}
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   328
\item[$\bullet$] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   329
the automatic provers (ATPs and SMT solvers) that should be run whenever
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   330
Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   331
remote\_vampire}'').
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   332
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   333
\item[$\bullet$] \textbf{\textit{timeout}} (\S\ref{mode-of-operation}) controls
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   334
the provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   335
asynchronously you should not hesitate to raise this limit to 60 or 120 seconds
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   336
if you are the kind of user who can think clearly while ATPs are active.
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   337
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   338
\item[$\bullet$] \textbf{\textit{full\_types}} (\S\ref{problem-encoding})
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   339
specifies whether type-sound encodings should be used. By default, Sledgehammer
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   340
employs a mixture of type-sound and type-unsound encodings, occasionally
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   341
yielding unsound ATP proofs. (SMT solver proofs should always be sound, although
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   342
we occasionally find soundness bugs in the solvers.)
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   343
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   344
\item[$\bullet$] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   345
specifies the maximum number of facts that should be passed to the provers. By
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   346
default, the value is prover-dependent but varies between about 150 and 1000. If
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   347
the provers time out, you can try lowering this value to, say, 100 or 50 and see
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   348
if that helps.
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   349
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   350
\item[$\bullet$] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   351
that Isar proofs should be generated, instead of one-liner Metis proofs. The
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   352
length of the Isar proofs can be controlled by setting
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   353
\textit{isar\_shrink\_factor} (\S\ref{output-format}).
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   354
\end{enum}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   355
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   356
Options can be set globally using \textbf{sledgehammer\_params}
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   357
(\S\ref{command-syntax}). Fact selection can be influenced by specifying
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   358
``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer}
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   359
call to ensure that certain facts are included, or simply
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   360
``$(\textit{my\_facts})$'' to force Sledgehammer to run only with
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   361
$\textit{my\_facts}$.
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   362
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   363
\section{Frequently Asked Questions}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   364
\label{frequently-asked-questions}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   365
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   366
\point{Why does Metis fail to reconstruct the proof?}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   367
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   368
There are many reasons. If Metis runs seemingly forever, that is a sign that the
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   369
proof is too difficult for it. Metis is complete, so it should eventually find
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   370
it, but that's little consolation. There are several possible solutions:
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   371
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   372
\begin{enum}
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   373
\item[$\bullet$] Try the \textit{isar\_proof} option (\S\ref{output-format}) to
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   374
obtain a step-by-step Isar proof where each step is justified by Metis. Since
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   375
the steps are fairly small, Metis is more likely to be able to replay them.
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   376
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   377
\item[$\bullet$] Try the \textit{smt} proof method instead of \textit{metis}. It
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   378
is usually stronger, but you need to have Z3 available to replay the proofs,
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   379
trust the SMT solver, or use certificates. See the documentation in the
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   380
\emph{SMT} theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}) for details.
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   381
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   382
\item[$\bullet$] Try the \textit{blast} or \textit{auto} proof methods, passing
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   383
facts via \textbf{unfolding}, \textbf{using}, \textit{intro}{:},
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   384
\textit{elim}{:}, \textit{dest}{:}, or \textit{simp}{:}, as appropriate.
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   385
\end{enum}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   386
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   387
In some rare cases, Metis fails fairly quickly. This usually indicates that
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   388
Sledgehammer found a type-incorrect proof. Sledgehammer erases some type
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   389
information to speed up the search. Try Sledgehammer again with full type
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   390
information: \textit{full\_types} (\S\ref{problem-encoding}), or choose a
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   391
specific type encoding with \textit{type\_sys} (\S\ref{problem-encoding}). Older
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   392
versions of Sledgehammer were frequent victims of this problem. Now this should
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   393
very seldom be an issue, but if you notice many unsound proofs, contact the
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   394
author at \authoremail.
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   395
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   396
\point{How can I tell whether a Sledgehammer proof is sound?}
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   397
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   398
First, if \emph{metis} (or \emph{metisFT}) can reconstruct it, the proof is
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   399
sound (modulo soundness of Isabelle's inference kernel). If it fails or runs
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   400
seemingly forever, you can try
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   401
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   402
\prew
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   403
\textbf{apply}~\textbf{--} \\
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   404
\textbf{sledgehammer} [\textit{type\_sys} = \textit{poly\_tags}] (\textit{metis\_facts})
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   405
\postw
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   406
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   407
where \textit{metis\_facts} is the list of facts appearing in the suggested
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   408
Metis call. The automatic provers should be able to refind the proof very
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   409
quickly if it is sound, and the \textit{type\_sys} $=$ \textit{poly\_tags}
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   410
option (\S\ref{problem-encoding}) ensures that no unsound proofs are found.
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   411
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   412
The \textit{full\_types} option (\S\ref{problem-encoding}) can also be used
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   413
here, but it is unsound in extremely rare degenerate cases such as the
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   414
following:
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   415
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   416
\prew
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   417
\textbf{lemma} ``$\forall x\> y\Colon{'}a.\ x = y \,\Longrightarrow \exists f\> g\Colon\mathit{nat} \Rightarrow {'}a.\ f \not= g$'' \\
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   418
\textbf{sledgehammer} [\textit{full\_types}] (\textit{nat.distinct\/}(1))
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   419
\postw
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   420
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   421
\point{How does Sledgehammer select the facts that should be passed to the
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   422
automatic provers?}
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   423
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   424
Briefly, the relevance filter assigns a score to every available fact (lemma,
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   425
theorem, definition, or axiom)\ based upon how many constants that fact shares
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   426
with the conjecture; this process iterates to include facts relevant to those
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   427
just accepted, but with a decay factor to ensure termination. The constants are
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   428
weighted to give unusual ones greater significance. The relevance filter copes
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   429
best when the conjecture contains some unusual constants; if all the constants
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   430
are common, it is unable to discriminate among the hundreds of facts that are
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   431
picked up. The relevance filter is also memoryless: It has no information about
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   432
how many times a particular fact has been used in a proof, and it cannot learn.
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   433
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   434
The number of facts included in a problem varies from prover to prover, since
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   435
some provers get overwhelmed quicker than others. You can show the number of
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   436
facts given using the \textit{verbose} option (\S\ref{output-format}) and the
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   437
actual facts using \textit{debug} (\S\ref{output-format}).
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   438
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   439
Sledgehammer is good at finding short proofs combining a handful of existing
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   440
lemmas. If you are looking for longer proofs, you must typically restrict the
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   441
number of facts, by setting the \textit{max\_relevant} option
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   442
(\S\ref{relevance-filter}) to, say, 50 or 100.
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   443
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   444
\point{Why are the Isar proofs generated by Sledgehammer so ugly?}
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   445
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   446
The current implementation is experimental and explodes exponentially in the
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   447
worst case. Work on a new implementation has begun. There is a large body of
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   448
research into transforming resolution proofs into natural deduction proofs (such
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   449
as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   450
set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   451
value or to try several provers and keep the nicest-looking proof.
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   452
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   453
\point{Should I let Sledgehammer minimize the number of lemmas?}
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   454
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   455
In general, minimization is a good idea, because proofs involving fewer lemmas
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   456
tend to be shorter as well, and hence easier to re-find by Metis. But the
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   457
opposite is sometimes the case.
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   458
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   459
\point{Why does the minimizer sometimes starts of its own?}
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   460
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   461
There are two scenarios in which this can happen. First, some provers (e.g.,
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   462
CVC3 and Yices) do not provide proofs or provide incomplete proofs. The
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   463
minimizer is then invoked to find out which facts are actually needed from the
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   464
(large) set of facts that was initinally given to the prover. Second, if a
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   465
prover returns a proof with lots of facts, the minimizer is invoked
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   466
automatically since Metis is unlikely to refind the proof.
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   467
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   468
\point{What is metisFT?}
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   469
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   470
The \textit{metisFT} proof method is the fully-typed version of Metis. It is
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   471
much slower than \textit{metis}, but the proof search is fully typed, and it
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   472
also includes more powerful rules such as the axiom ``$x = \mathit{True}
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   473
\mathrel{\lor} x = \mathit{False}$'' for reasoning in higher-order places (e.g.,
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   474
in set comprehensions). The method kicks in automatically as a fallback when
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   475
\textit{metis} fails, and it is sometimes generated by Sledgehammer instead of
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   476
\textit{metis} if the proof obviously requires type information.
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   477
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   478
If you see the warning
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   479
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   480
\prew
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   481
\textsl
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   482
Metis: Falling back on ``\textit{metisFT}''.
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   483
\postw
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   484
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   485
in a successful Metis proof, you can advantageously replace the \textit{metis}
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   486
call with \textit{metisFT}.
42850
c8709be8a40f distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job
blanchet
parents: 42846
diff changeset
   487
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   488
\point{I got a strange error from Sledgehammer---what should I do?}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   489
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   490
Sledgehammer tries to give informative error messages. Please report any strange
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   491
error to the author at \authoremail. This applies double if you get the message
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   492
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   493
\prew
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   494
\slshape
42877
d7447b8c4265 updated FAQ
blanchet
parents: 42856
diff changeset
   495
The prover found a type-unsound proof involving ``\textit{foo}'',
d7447b8c4265 updated FAQ
blanchet
parents: 42856
diff changeset
   496
``\textit{bar}'', ``\textit{baz}'' even though a supposedly type-sound encoding
d7447b8c4265 updated FAQ
blanchet
parents: 42856
diff changeset
   497
was used (or, less likely, your axioms are inconsistent). You might want to
d7447b8c4265 updated FAQ
blanchet
parents: 42856
diff changeset
   498
report this to the Isabelle developers.
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   499
\postw
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   500
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   501
\point{Auto can solve it---why not Sledgehammer?}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   502
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   503
Problems can be easy for \textit{auto} and difficult for automatic provers, but
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   504
the reverse is also true, so don't be discouraged if your first attempts fail.
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   505
Because the system refers to all theorems known to Isabelle, it is particularly
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   506
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
   507
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   508
\point{Why are there so many options?}
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   509
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   510
Sledgehammer's philosophy should work out of the box, without user guidance.
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   511
Many of the options are meant to be used mostly by the Sledgehammer developers
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   512
for experimentation purposes. Of course, feel free to experiment with them if
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   513
you are so inclined.
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   514
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   515
\section{Command Syntax}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   516
\label{command-syntax}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   517
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   518
Sledgehammer can be invoked at any point when there is an open goal by entering
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   519
the \textbf{sledgehammer} command in the theory file. Its general syntax is as
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   520
follows:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   521
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   522
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   523
\textbf{sledgehammer} \textit{subcommand\/$^?$ options\/$^?$ facts\_override\/$^?$ num\/$^?$}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   524
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   525
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   526
For convenience, Sledgehammer is also available in the ``Commands'' submenu of
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   527
the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   528
C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   529
no arguments in the theory text.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   530
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   531
In the general syntax, the \textit{subcommand} may be any of the following:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   532
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   533
\begin{enum}
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   534
\item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   535
subgoal number \textit{num} (1 by default), with the given options and facts.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   536
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   537
\item[$\bullet$] \textbf{\textit{minimize}:} Attempts to minimize the provided facts
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   538
(specified in the \textit{facts\_override} argument) to obtain a simpler proof
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   539
involving fewer facts. The options and goal number are as for \textit{run}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   540
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   541
\item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   542
by Sledgehammer. This allows you to examine results that might have been lost
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   543
due to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   544
limit on the number of messages to display (5 by default).
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   545
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41724
diff changeset
   546
\item[$\bullet$] \textbf{\textit{supported\_provers}:} Prints the list of
41724
14d135c09bec transformed lie into truth
blanchet
parents: 41208
diff changeset
   547
automatic provers supported by Sledgehammer. See \S\ref{installation} and
14d135c09bec transformed lie into truth
blanchet
parents: 41208
diff changeset
   548
\S\ref{mode-of-operation} for more information on how to install automatic
14d135c09bec transformed lie into truth
blanchet
parents: 41208
diff changeset
   549
provers.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   550
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   551
\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
   552
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
   553
time until timeout.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   554
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   555
\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
   556
automatic provers.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   557
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   558
\item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   559
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   560
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   561
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   562
Sledgehammer's behavior can be influenced by various \textit{options}, which can
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   563
be specified in brackets after the \textbf{sledgehammer} command. The
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   564
\textit{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   565
\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true}'' is optional. For
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   566
example:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   567
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   568
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   569
\textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120$\,s$]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   570
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   571
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   572
Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   573
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   574
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   575
\textbf{sledgehammer\_params} \textit{options}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   576
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   577
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   578
The supported options are described in \S\ref{option-reference}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   579
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   580
The \textit{facts\_override} argument lets you alter the set of facts that go
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   581
through the relevance filter. It may be of the form ``(\textit{facts})'', where
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   582
\textit{facts} is a space-separated list of Isabelle facts (theorems, local
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   583
assumptions, etc.), in which case the relevance filter is bypassed and the given
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   584
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
   585
``(\textit{del}:\ \textit{facts}$_2$)'', or ``(\textit{add}:\ \textit{facts}$_1$\
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   586
\textit{del}:\ \textit{facts}$_2$)'', where the relevance filter is instructed to
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   587
proceed as usual except that it should consider \textit{facts}$_1$
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   588
highly-relevant and \textit{facts}$_2$ fully irrelevant.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   589
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   590
You can instruct Sledgehammer to run automatically on newly entered theorems by
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   591
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
   592
General. For automatic runs, only the first prover set using \textit{provers}
42736
8005fc9b65ec ensure that Auto Sledgehammer is run with full type information
blanchet
parents: 42724
diff changeset
   593
(\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover,
8005fc9b65ec ensure that Auto Sledgehammer is run with full type information
blanchet
parents: 42724
diff changeset
   594
\textit{slicing} (\S\ref{mode-of-operation}) is disabled, \textit{timeout}
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   595
(\S\ref{mode-of-operation}) is superseded by the ``Auto Tools Time Limit'' in
42736
8005fc9b65ec ensure that Auto Sledgehammer is run with full type information
blanchet
parents: 42724
diff changeset
   596
Proof General's ``Isabelle'' menu, \textit{full\_types}
8005fc9b65ec ensure that Auto Sledgehammer is run with full type information
blanchet
parents: 42724
diff changeset
   597
(\S\ref{problem-encoding}) is enabled, and \textit{verbose}
8005fc9b65ec ensure that Auto Sledgehammer is run with full type information
blanchet
parents: 42724
diff changeset
   598
(\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled.
8005fc9b65ec ensure that Auto Sledgehammer is run with full type information
blanchet
parents: 42724
diff changeset
   599
Sledgehammer's output is also more concise.
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   600
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   601
\section{Option Reference}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   602
\label{option-reference}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   603
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   604
\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   605
\def\qty#1{$\left<\textit{#1}\right>$}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   606
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   607
\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
   608
\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
   609
\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
   610
\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
   611
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   612
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   613
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   614
\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
   615
\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
   616
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   617
Sledgehammer's options are categorized as follows:\ mode of operation
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   618
(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   619
relevance filter (\S\ref{relevance-filter}), output format
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   620
(\S\ref{output-format}), and authentication (\S\ref{authentication}).
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   621
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   622
The descriptions below refer to the following syntactic quantities:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   623
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   624
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   625
\item[$\bullet$] \qtybf{string}: A string.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   626
\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   627
\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   628
\textit{smart}.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   629
\item[$\bullet$] \qtybf{int\/}: An integer.
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42722
diff changeset
   630
%\item[$\bullet$] \qtybf{float\/}: A floating-point number (e.g., 2.5).
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   631
\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
   632
(e.g., 0.6 0.95).
38591
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   633
\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
   634
\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
   635
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
   636
\textit{none} ($\infty$ seconds).
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   637
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   638
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   639
Default values are indicated in square brackets. Boolean options have a negated
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   640
counterpart (e.g., \textit{blocking} vs.\ \textit{non\_blocking}). When setting
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   641
Boolean options, ``= \textit{true}'' may be omitted.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   642
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   643
\subsection{Mode of Operation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   644
\label{mode-of-operation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   645
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   646
\begin{enum}
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   647
\opnodefault{provers}{string}
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   648
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
   649
``\textit{e}~\textit{spass}''). The following provers are supported:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   650
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   651
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   652
\item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   653
\cite{schulz-2002}. To use E, set the environment variable
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   654
\texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable,
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   655
or install the prebuilt E package from Isabelle's download page. See
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   656
\S\ref{installation} for details.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   657
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   658
\item[$\bullet$] \textbf{\textit{spass}:} SPASS is an ATP developed by Christoph
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   659
Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   660
environment variable \texttt{SPASS\_HOME} to the directory that contains the
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   661
\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
   662
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
   663
\S\ref{installation} for details.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   664
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   665
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   666
Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   667
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   668
that contains the \texttt{vampire} executable. Sledgehammer has been tested with
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   669
versions 11, 0.6, and 1.0.
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   670
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   671
\item[$\bullet$] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   672
Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   673
set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   674
executable, including the file name. Sledgehammer has been tested with version
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   675
2.2.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   676
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   677
\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   678
SRI \cite{yices}. To use Yices, set the environment variable
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   679
\texttt{YICES\_SOLVER} to the complete path of the executable, including the
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   680
file name. Sledgehammer has been tested with version 1.0.
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   681
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   682
\item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   683
Microsoft Research \cite{z3}. To use Z3, set the environment variable
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   684
\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   685
name. Sledgehammer has been tested with versions 2.7 to 2.18.
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   686
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   687
\item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   688
ATP, exploiting Z3's undocumented support for the TPTP format. It is included
42442
036142bd0302 fixed typo in documentation
blanchet
parents: 42237
diff changeset
   689
for experimental purposes. It requires version 2.18 or above.
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   690
38601
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   691
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   692
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   693
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   694
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
38601
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   695
Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   696
42535
3c1f302b3ee6 added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
blanchet
parents: 42523
diff changeset
   697
\item[$\bullet$] \textbf{\textit{remote\_tofof\_e}:} ToFoF-E is a metaprover
3c1f302b3ee6 added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
blanchet
parents: 42523
diff changeset
   698
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
3c1f302b3ee6 added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
blanchet
parents: 42523
diff changeset
   699
servers. This ATP supports a fragment of the TPTP many-typed first-order format
3c1f302b3ee6 added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
blanchet
parents: 42523
diff changeset
   700
(TFF). It is supported primarily for experimenting with the
42856
9eef1dc200a8 updated option documentation
blanchet
parents: 42850
diff changeset
   701
\textit{type\_sys} $=$ \textit{simple} option (\S\ref{problem-encoding}).
42535
3c1f302b3ee6 added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
blanchet
parents: 42523
diff changeset
   702
38601
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   703
\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   704
developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   705
SInE runs on Geoff Sutcliffe's Miami servers.
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   706
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   707
\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a prover
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   708
developed by Stickel et al.\ \cite{snark}. The remote version of
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   709
SNARK runs on Geoff Sutcliffe's Miami servers.
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   710
41738
eb98c60a6cf0 added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents: 41727
diff changeset
   711
\item[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
eb98c60a6cf0 added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents: 41727
diff changeset
   712
on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
eb98c60a6cf0 added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents: 41727
diff changeset
   713
point).
eb98c60a6cf0 added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents: 41727
diff changeset
   714
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   715
\item[$\bullet$] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   716
servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   717
point).
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   718
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   719
\item[$\bullet$] \textbf{\textit{remote\_z3\_atp}:} The remote version of ``Z3
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   720
as an ATP'' runs on Geoff Sutcliffe's Miami servers.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   721
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   722
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   723
By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever
42228
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   724
the SMT module's \textit{smt\_solver} configuration option is set to) in
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   725
parallel---either locally or remotely, depending on the number of processor
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   726
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
   727
overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   728
in Proof General.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   729
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   730
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
   731
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
   732
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
   733
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
   734
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   735
\opnodefault{prover}{string}
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   736
Alias for \textit{provers}.
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   737
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   738
%\opnodefault{atps}{string}
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   739
%Legacy alias for \textit{provers}.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   740
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   741
%\opnodefault{atp}{string}
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   742
%Legacy alias for \textit{provers}.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   743
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   744
\opdefault{timeout}{float\_or\_none}{\upshape 30}
40341
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40203
diff changeset
   745
Specifies the maximum number of seconds that the automatic provers should spend
42850
c8709be8a40f distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job
blanchet
parents: 42846
diff changeset
   746
searching for a proof. This excludes problem preparation and is a soft limit.
c8709be8a40f distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job
blanchet
parents: 42846
diff changeset
   747
For historical reasons, the default value of this option can be overridden using
c8709be8a40f distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job
blanchet
parents: 42846
diff changeset
   748
the option ``Sledgehammer: Time Limit'' from the ``Isabelle'' menu in Proof
c8709be8a40f distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job
blanchet
parents: 42846
diff changeset
   749
General.
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   750
38983
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   751
\opfalse{blocking}{non\_blocking}
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   752
Specifies whether the \textbf{sledgehammer} command should operate
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   753
synchronously. The asynchronous (non-blocking) mode lets the user start proving
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   754
the putative theorem manually while Sledgehammer looks for a proof, but it can
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   755
also be more confusing.
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   756
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   757
\optrue{slicing}{no\_slicing}
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   758
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
   759
segments, each of which has its own set of possibly prover-dependent options.
42446
d105b1309a8d rewording
blanchet
parents: 42443
diff changeset
   760
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
   761
set-of-support (SOS) strategy, whereas the second slice runs without it. For E,
42446
d105b1309a8d rewording
blanchet
parents: 42443
diff changeset
   762
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
   763
number of facts. For SMT solvers, several slices are tried with the same options
42446
d105b1309a8d rewording
blanchet
parents: 42443
diff changeset
   764
each time but fewer and fewer facts. According to benchmarks with a timeout of
d105b1309a8d rewording
blanchet
parents: 42443
diff changeset
   765
30 seconds, slicing is a valuable optimization, and you should probably leave it
d105b1309a8d rewording
blanchet
parents: 42443
diff changeset
   766
enabled unless you are conducting experiments. This option is implicitly
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   767
disabled for (short) automatic runs.
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   768
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   769
\nopagebreak
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   770
{\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
   771
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   772
\opfalse{overlord}{no\_overlord}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   773
Specifies whether Sledgehammer should put its temporary files in
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   774
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   775
debugging Sledgehammer but also unsafe if several instances of the tool are run
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   776
simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   777
safely remove them after Sledgehammer has run.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   778
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   779
\nopagebreak
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   780
{\small See also \textit{debug} (\S\ref{output-format}).}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   781
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   782
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   783
\subsection{Problem Encoding}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   784
\label{problem-encoding}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   785
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   786
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   787
\opfalse{explicit\_apply}{implicit\_apply}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   788
Specifies whether function application should be encoded as an explicit
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   789
``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
   790
function will be directly applied to as many arguments as possible. Enabling
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   791
this option can sometimes help discover higher-order proofs that otherwise would
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   792
not be found.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   793
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   794
\opfalse{full\_types}{partial\_types}
42681
281cc069282c document monotonic type systems
blanchet
parents: 42591
diff changeset
   795
Specifies whether full type information is encoded in ATP problems. Enabling
42736
8005fc9b65ec ensure that Auto Sledgehammer is run with full type information
blanchet
parents: 42724
diff changeset
   796
this option prevents the discovery of type-incorrect proofs, but it can slow
8005fc9b65ec ensure that Auto Sledgehammer is run with full type information
blanchet
parents: 42724
diff changeset
   797
down the ATP slightly. This option is implicitly enabled for automatic runs. For
8005fc9b65ec ensure that Auto Sledgehammer is run with full type information
blanchet
parents: 42724
diff changeset
   798
historical reasons, the default value of this option can be overridden using the
8005fc9b65ec ensure that Auto Sledgehammer is run with full type information
blanchet
parents: 42724
diff changeset
   799
option ``Sledgehammer: Full Types'' from the ``Isabelle'' menu in Proof General.
42228
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   800
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   801
\opdefault{type\_sys}{string}{smart}
42887
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   802
Specifies the type system to use in ATP problems. Some of the type systems are
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   803
unsound, meaning that they can give rise to spurious proofs (unreconstructible
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   804
using Metis). The supported type systems are listed below, with an indication of
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   805
their soundness in parentheses:
42228
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   806
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   807
\begin{enum}
42887
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   808
\item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   809
supplied to the ATP. Types are simply erased.
42582
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   810
42887
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   811
\item[$\bullet$] \textbf{\textit{poly\_preds} (sound):} Types are encoded using
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   812
a predicate \textit{has\_\allowbreak type\/}$(\tau, t)$ that restricts the range
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   813
of bound variables. Constants are annotated with their types, supplied as extra
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   814
arguments, to resolve overloading.
42685
7a5116bd63b7 documentation tuning
blanchet
parents: 42683
diff changeset
   815
42887
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   816
\item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   817
tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$.
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   818
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   819
\item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   820
Like for \textit{poly\_preds} constants are annotated with their types to
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   821
resolve overloading, but otherwise no type information is encoded.
42685
7a5116bd63b7 documentation tuning
blanchet
parents: 42683
diff changeset
   822
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   823
\item[$\bullet$]
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   824
\textbf{%
42887
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   825
\textit{mono\_preds}, \textit{mono\_tags} (sound);
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   826
\textit{mono\_args} (unsound):} \\
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   827
Similar to \textit{poly\_preds}, \textit{poly\_tags}, and \textit{poly\_args},
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   828
respectively, but the problem is additionally monomorphized, meaning that type
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   829
variables are instantiated with heuristically chosen ground types.
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   830
Monomorphization can simplify reasoning but also leads to larger fact bases,
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   831
which can slow down the ATPs.
42582
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   832
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   833
\item[$\bullet$]
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   834
\textbf{%
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   835
\textit{mangled\_preds},
42887
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   836
\textit{mangled\_tags} (sound); \\
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   837
\textit{mangled\_args} (unsound):} \\
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   838
Similar to
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   839
\textit{mono\_preds}, \textit{mono\_tags}, and \textit{mono\_args},
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   840
respectively but types are mangled in constant names instead of being supplied
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   841
as ground term arguments. The binary predicate $\mathit{has\_type\/}(\tau, t)$
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
   842
becomes a unary predicate $\mathit{has\_type\_}\tau(t)$, and the binary function
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
   843
$\mathit{type\_info\/}(\tau, t)$ becomes a unary function
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
   844
$\mathit{type\_info\_}\tau(t)$.
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
   845
42887
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   846
\item[$\bullet$] \textbf{\textit{simple} (sound):} Use the prover's support for
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   847
simply typed first-order logic if available; otherwise, fall back on
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   848
\textit{mangled\_preds}. The problem is monomorphized.
42681
281cc069282c document monotonic type systems
blanchet
parents: 42591
diff changeset
   849
281cc069282c document monotonic type systems
blanchet
parents: 42591
diff changeset
   850
\item[$\bullet$]
281cc069282c document monotonic type systems
blanchet
parents: 42591
diff changeset
   851
\textbf{%
42887
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   852
\textit{poly\_preds}?, \textit{poly\_tags}?, \textit{mono\_preds}?, \textit{mono\_tags}?, \\
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   853
\textit{mangled\_preds}?, \textit{mangled\_tags}?, \textit{simple}? (quasi-sound):} \\
42743
b81127eb79f3 reflect option renaming in doc + do not document the type systems poly_preds? and poly_tags?, since they are virtually identical to the non-? versions
blanchet
parents: 42736
diff changeset
   854
The type systems \textit{poly\_preds}, \textit{poly\_tags},
42887
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   855
\textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds},
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   856
\textit{mangled\_tags}, and \textit{simple} are fully typed and sound. For each
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   857
of these, Sledgehammer also provides a lighter, virtually sound variant
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   858
identified by a question mark (`{?}')\ that detects and erases monotonic types,
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   859
notably infinite types. (For \textit{simple}, the types are not actually erased
42856
9eef1dc200a8 updated option documentation
blanchet
parents: 42850
diff changeset
   860
but rather replaced by a shared uniform type of individuals.)
42582
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   861
42887
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   862
\item[$\bullet$]
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   863
\textbf{%
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   864
\textit{poly\_preds}!, \textit{poly\_tags}!, \textit{mono\_preds}!, \textit{mono\_tags}!, \\
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   865
\textit{mangled\_preds}!, \textit{mangled\_tags}!, \textit{simple}! \\
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   866
(mildly unsound):} \\
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   867
The type systems \textit{poly\_preds}, \textit{poly\_tags},
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   868
\textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds},
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   869
\textit{mangled\_tags}, and \textit{simple} also admit a mildly unsound (but
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   870
very efficient) variant identified by an exclamation mark (`{!}') that detects
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   871
and erases erases all types except those that are clearly finite (e.g.,
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   872
\textit{bool}). (For \textit{simple}, the types are not actually erased but
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   873
rather replaced by a shared uniform type of individuals.)
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   874
42237
e645d7255bd4 renamed "const_args" option value to "args"
blanchet
parents: 42234
diff changeset
   875
\item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
42887
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   876
uses a sound or virtually sound encoding; otherwise, uses any encoding. The actual
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
   877
encoding used depends on the ATP and should be the most efficient for that ATP.
42228
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   878
\end{enum}
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   879
42856
9eef1dc200a8 updated option documentation
blanchet
parents: 42850
diff changeset
   880
In addition, all the \textit{preds} and \textit{tags} type systems are available
9eef1dc200a8 updated option documentation
blanchet
parents: 42850
diff changeset
   881
in two variants, a lightweight and a heavyweight variant. The lightweight
9eef1dc200a8 updated option documentation
blanchet
parents: 42850
diff changeset
   882
variants are generally more efficient and are the default; the heavyweight
9eef1dc200a8 updated option documentation
blanchet
parents: 42850
diff changeset
   883
variants are identified by a \textit{\_heavy} suffix (e.g.,
9eef1dc200a8 updated option documentation
blanchet
parents: 42850
diff changeset
   884
\textit{mangled\_preds\_heavy}{?}).
42523
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42511
diff changeset
   885
42856
9eef1dc200a8 updated option documentation
blanchet
parents: 42850
diff changeset
   886
For SMT solvers and ToFoF-E, the type system is always \textit{simple},
9eef1dc200a8 updated option documentation
blanchet
parents: 42850
diff changeset
   887
irrespective of the value of this option.
38591
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   888
\end{enum}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   889
38591
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   890
\subsection{Relevance Filter}
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   891
\label{relevance-filter}
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   892
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   893
\begin{enum}
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   894
\opdefault{relevance\_thresholds}{float\_pair}{\upshape 0.45~0.85}
38746
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   895
Specifies the thresholds above which facts are considered relevant by the
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   896
relevance filter. The first threshold is used for the first iteration of the
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   897
relevance filter and the second threshold is used for the last iteration (if it
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   898
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
   899
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
   900
are relevant and 1 only theorems that refer to previously seen constants.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   901
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   902
\opsmart{max\_relevant}{int\_or\_smart}
38746
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   903
Specifies the maximum number of facts that may be returned by the relevance
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   904
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
   905
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
   906
300.
42180
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 41747
diff changeset
   907
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   908
\opdefault{max\_new\_mono\_instances}{int}{\upshape 400}
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   909
Specifies the maximum number of monomorphic instances to generate beyond
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   910
\textit{max\_relevant}. The higher this limit is, the more monomorphic instances
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   911
are potentially generated. Whether monomorphization takes place depends on the
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   912
type system used.
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   913
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   914
\nopagebreak
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   915
{\small See also \textit{type\_sys} (\S\ref{problem-encoding}).}
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   916
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   917
\opdefault{max\_mono\_iters}{int}{\upshape 3}
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   918
Specifies the maximum number of iterations for the monomorphization fixpoint
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   919
construction. The higher this limit is, the more monomorphic instances are
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   920
potentially generated. Whether monomorphization takes place depends on the
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   921
type system used.
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   922
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   923
\nopagebreak
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   924
{\small See also \textit{type\_sys} (\S\ref{problem-encoding}).}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   925
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   927
\subsection{Output Format}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   928
\label{output-format}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   929
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   930
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   931
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   932
\opfalse{verbose}{quiet}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   933
Specifies whether the \textbf{sledgehammer} command should explain what it does.
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 40942
diff changeset
   934
This option is implicitly disabled for automatic runs.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   935
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   936
\opfalse{debug}{no\_debug}
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   937
Specifies whether Sledgehammer should display additional debugging information
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   938
beyond what \textit{verbose} already displays. Enabling \textit{debug} also
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 40942
diff changeset
   939
enables \textit{verbose} and \textit{blocking} (\S\ref{mode-of-operation})
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 40942
diff changeset
   940
behind the scenes. The \textit{debug} option is implicitly disabled for
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 40942
diff changeset
   941
automatic runs.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   942
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   943
\nopagebreak
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   944
{\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   945
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   946
\opfalse{isar\_proof}{no\_isar\_proof}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   947
Specifies whether Isar proofs should be output in addition to one-liner
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   948
\textit{metis} proofs. Isar proof construction is still experimental and often
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   949
fails; however, they are usually faster and sometimes more robust than
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   950
\textit{metis} proofs.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   951
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   952
\opdefault{isar\_shrink\_factor}{int}{\upshape 1}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   953
Specifies the granularity of the Isar proof. A value of $n$ indicates that each
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   954
Isar proof step should correspond to a group of up to $n$ consecutive proof
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   955
steps in the ATP proof.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   956
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   957
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   958
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   959
\subsection{Authentication}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   960
\label{authentication}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   961
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   962
\begin{enum}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   963
\opnodefault{expect}{string}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   964
Specifies the expected outcome, which must be one of the following:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   965
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   966
\begin{enum}
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   967
\item[$\bullet$] \textbf{\textit{some}:} Sledgehammer found a (potentially
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   968
unsound) proof.
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   969
\item[$\bullet$] \textbf{\textit{none}:} Sledgehammer found no proof.
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   970
\item[$\bullet$] \textbf{\textit{unknown}:} Sledgehammer encountered some
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   971
problem.
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   972
\end{enum}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   973
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   974
Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   975
(otherwise) if the actual outcome differs from the expected outcome. This option
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   976
is useful for regression testing.
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   977
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   978
\nopagebreak
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   979
{\small See also \textit{blocking} (\S\ref{mode-of-operation}).}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   980
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   981
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   982
\let\em=\sl
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   983
\bibliography{../manual}{}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   984
\bibliographystyle{abbrv}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   985
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   986
\end{document}