doc-src/Sledgehammer/sledgehammer.tex
author blanchet
Sun, 01 May 2011 18:57:45 +0200
changeset 42591 f139d0ac2d44
parent 42589 9f7c48463645
child 42681 281cc069282c
permissions -rw-r--r--
minor doc fixes
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},
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    83
Vampire \cite{riazanov-voronkov-2002}, SInE-E \cite{sine}, and SNARK
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    84
\cite{snark}. The ATPs are run either locally or remotely via the
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    85
System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs, the
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
    86
SMT solvers Z3 \cite{z3} is used, and you can tell Sledgehammer to try Yices
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
    87
\cite{yices} and CVC3 \cite{cvc3} as well.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    88
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    89
The problem passed to the automatic provers consists of your current goal
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    90
together with a heuristic selection of hundreds of facts (theorems) from the
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    91
current theory context, filtered by relevance. Because jobs are run in the
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    92
background, you can continue to work on your proof by other means. Provers can
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    93
be run in parallel. Any reply (which may arrive half a minute later) will appear
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    94
in the Proof General response buffer.
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    95
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    96
The result of a successful proof search is some source text that usually (but
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    97
not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    98
proof relies on the general-purpose Metis prover \cite{metis}, which is fully
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
    99
integrated into Isabelle/HOL, with explicit inferences going through the kernel.
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   100
Thus its results are correct by construction.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   101
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   102
In this manual, we will explicitly invoke the \textbf{sledgehammer} command.
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   103
Sledgehammer also provides an automatic mode that can be enabled via the
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   104
``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof General. In
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   105
this mode, Sledgehammer is run on every newly entered theorem. The time limit
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   106
for Auto Sledgehammer and other automatic tools can be set using the ``Auto
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   107
Tools Time Limit'' option.
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   108
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   109
\newbox\boxA
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   110
\setbox\boxA=\hbox{\texttt{nospam}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   111
40689
3a10ce7cd436 document requirement on theory import
blanchet
parents: 40343
diff changeset
   112
To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is
3a10ce7cd436 document requirement on theory import
blanchet
parents: 40343
diff changeset
   113
imported---this is rarely a problem in practice since it is part of
3a10ce7cd436 document requirement on theory import
blanchet
parents: 40343
diff changeset
   114
\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   115
\texttt{src/HOL/Metis\_Examples} directory.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   116
Comments and bug reports concerning Sledgehammer or this manual should be
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   117
directed to
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   118
\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   119
in.\allowbreak tum.\allowbreak de}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   120
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   121
\vskip2.5\smallskipamount
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   122
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   123
%\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   124
%suggesting several textual improvements.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   125
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   126
\section{Installation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   127
\label{installation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   128
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   129
Sledgehammer is part of Isabelle, so you don't need to install it. However, it
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   130
relies on third-party automatic theorem provers (ATPs) and SAT solvers.
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   131
Currently, E, SPASS, and Vampire can be run locally; in addition, E, Vampire,
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   132
SInE-E, and SNARK are available remotely via SystemOnTPTP \cite{sutcliffe-2000}.
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   133
If you want better performance, you should install E and SPASS locally.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   134
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   135
There are three main ways to install ATPs on your machine:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   136
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   137
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   138
\item[$\bullet$] If you installed an official Isabelle package with everything
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   139
inside, it should already include properly setup executables for E and SPASS,
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   140
ready to use.%
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   141
\footnote{Vampire's license prevents us from doing the same for this otherwise
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   142
wonderful tool.}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   143
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   144
\item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   145
binary packages from Isabelle's download page. Extract the archives, then add a
41747
f58d4d202924 fix path to etc/settings and etc/components in doc
blanchet
parents: 41740
diff changeset
   146
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
   147
\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
   148
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
   149
\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
   150
file with the absolute
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   151
path to E or SPASS. For example, if the \texttt{components} does not exist yet
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   152
and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create the
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   153
\texttt{components} file with the single line
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   154
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   155
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   156
\texttt{/usr/local/spass-3.7}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   157
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   158
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   159
in it.
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   160
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   161
\item[$\bullet$] If you prefer to build E or SPASS yourself, or obtained a
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   162
Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}),
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   163
set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   164
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
38063
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   165
\texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   166
with E 1.0 and 1.2, SPASS 3.5 and 3.7, and Vampire 1.0%
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   167
\footnote{Following the rewrite of Vampire, the counter for version numbers was
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   168
reset to 0; hence the new Vampire 1.0 is more recent than Vampire 11.5.}%
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   169
. Since the ATPs' output formats are neither documented nor stable, other
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   170
versions of the ATPs might or might not work well with Sledgehammer.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   171
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   172
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   173
To check whether E and SPASS are installed, follow the example in
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   174
\S\ref{first-steps}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   175
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   176
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
   177
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
   178
server to access the Internet, set the \texttt{http\_proxy} environment variable
39153
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   179
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
   180
\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
   181
f09b378cb252 make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents: 38997
diff changeset
   182
\prew
39153
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   183
\texttt{http\_proxy=http://proxy.example.org} \\
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   184
\texttt{http\_proxy=http://proxy.example.org:8080} \\
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   185
\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
   186
\postw
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   187
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   188
\section{First Steps}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   189
\label{first-steps}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   190
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   191
To illustrate Sledgehammer in context, let us start a theory file and
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   192
attempt to prove a simple lemma:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   193
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   194
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   195
\textbf{theory}~\textit{Scratch} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   196
\textbf{imports}~\textit{Main} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   197
\textbf{begin} \\[2\smallskipamount]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   198
%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   199
\textbf{lemma} ``$[a] = [b] \,\longleftrightarrow\, a = b$'' \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   200
\textbf{sledgehammer}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   201
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   202
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   203
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
   204
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
   205
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
   206
Either way, Sledgehammer produces the following output after a few seconds:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   207
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   208
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   209
\slshape
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   210
Sledgehammer: ``\textit{e}'' for subgoal 1: \\
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   211
$([a] = [b]) = (a = b)$ \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   212
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   213
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
   214
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   215
%
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   216
Sledgehammer: ``\textit{spass}'' for subgoal 1: \\
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   217
$([a] = [b]) = (a = b)$ \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   218
Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   219
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
   220
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   221
%
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   222
Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   223
$([a] = [b]) = (a = b)$ \\
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   224
Try this command: \textbf{by} (\textit{metis eq\_commute last\_snoc}) \\
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   225
To minimize the number of lemmas, try this: \\
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   226
\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
   227
%
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   228
Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   229
$([a] = [b]) = (a = b)$ \\
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   230
Try this command: \textbf{by} (\textit{metis hd.simps}) \\
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   231
To minimize the number of lemmas, try this: \\
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   232
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   233
%
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   234
Sledgehammer: ``\textit{remote\_z3}'' for subgoal 1: \\
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   235
$([a] = [b]) = (a = b)$ \\
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   236
Try this command: \textbf{by} (\textit{metis hd.simps}) \\
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   237
To minimize the number of lemmas, try this: \\
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   238
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   239
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   240
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   241
Sledgehammer ran E, SPASS, Vampire, SInE-E, and Z3 in parallel. Depending on
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   242
which provers are installed and how many processor cores are available, some of
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   243
the provers might be missing or present with a \textit{remote\_} prefix.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   244
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   245
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
   246
\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
   247
the theory text. You can click the ``\textbf{sledgehammer} \textit{minimize}''
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   248
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
   249
the proof found by E looks perfect, so click it to finish the proof.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   250
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   251
You can ask Sledgehammer for an Isar text proof by passing the
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   252
\textit{isar\_proof} option:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   253
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   254
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   255
\textbf{sledgehammer} [\textit{isar\_proof}]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   256
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   257
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   258
When Isar proof construction is successful, it can yield proofs that are more
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   259
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
   260
experimental and is only available for ATPs.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   261
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   262
\section{Hints}
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   263
\label{hints}
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   264
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   265
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
   266
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
   267
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
   268
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
   269
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
   270
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
   271
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
   272
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
   273
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   274
Note that problems can be easy for \textit{auto} and difficult for ATPs, but the
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   275
reverse is also true, so don't be discouraged if your first attempts fail.
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   276
Because the system refers to all theorems known to Isabelle, it is particularly
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   277
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
   278
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   279
\section{Command Syntax}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   280
\label{command-syntax}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   281
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   282
Sledgehammer can be invoked at any point when there is an open goal by entering
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   283
the \textbf{sledgehammer} command in the theory file. Its general syntax is as
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   284
follows:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   285
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   286
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   287
\textbf{sledgehammer} \textit{subcommand\/$^?$ options\/$^?$ facts\_override\/$^?$ num\/$^?$}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   288
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   289
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   290
For convenience, Sledgehammer is also available in the ``Commands'' submenu of
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   291
the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   292
C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   293
no arguments in the theory text.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   294
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   295
In the general syntax, the \textit{subcommand} may be any of the following:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   296
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   297
\begin{enum}
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   298
\item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   299
subgoal number \textit{num} (1 by default), with the given options and facts.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   300
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   301
\item[$\bullet$] \textbf{\textit{minimize}:} Attempts to minimize the provided facts
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   302
(specified in the \textit{facts\_override} argument) to obtain a simpler proof
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   303
involving fewer facts. The options and goal number are as for \textit{run}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   304
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   305
\item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   306
by Sledgehammer. This allows you to examine results that might have been lost
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   307
due to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   308
limit on the number of messages to display (5 by default).
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   309
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41724
diff changeset
   310
\item[$\bullet$] \textbf{\textit{supported\_provers}:} Prints the list of
41724
14d135c09bec transformed lie into truth
blanchet
parents: 41208
diff changeset
   311
automatic provers supported by Sledgehammer. See \S\ref{installation} and
14d135c09bec transformed lie into truth
blanchet
parents: 41208
diff changeset
   312
\S\ref{mode-of-operation} for more information on how to install automatic
14d135c09bec transformed lie into truth
blanchet
parents: 41208
diff changeset
   313
provers.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   314
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   315
\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
   316
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
   317
time until timeout.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   318
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   319
\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
   320
automatic provers.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   321
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   322
\item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   323
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   324
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   325
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   326
Sledgehammer's behavior can be influenced by various \textit{options}, which can
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   327
be specified in brackets after the \textbf{sledgehammer} command. The
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   328
\textit{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   329
\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true}'' is optional. For
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   330
example:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   331
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   332
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   333
\textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120$\,s$]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   334
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   335
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   336
Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   337
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   338
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   339
\textbf{sledgehammer\_params} \textit{options}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   340
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   341
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   342
The supported options are described in \S\ref{option-reference}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   343
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   344
The \textit{facts\_override} argument lets you alter the set of facts that go
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   345
through the relevance filter. It may be of the form ``(\textit{facts})'', where
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   346
\textit{facts} is a space-separated list of Isabelle facts (theorems, local
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   347
assumptions, etc.), in which case the relevance filter is bypassed and the given
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   348
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
   349
``(\textit{del}:\ \textit{facts}$_2$)'', or ``(\textit{add}:\ \textit{facts}$_1$\
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   350
\textit{del}:\ \textit{facts}$_2$)'', where the relevance filter is instructed to
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   351
proceed as usual except that it should consider \textit{facts}$_1$
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   352
highly-relevant and \textit{facts}$_2$ fully irrelevant.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   353
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   354
You can instruct Sledgehammer to run automatically on newly entered theorems by
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   355
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
   356
General. For automatic runs, only the first prover set using \textit{provers}
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   357
(\S\ref{mode-of-operation}) is considered, \textit{verbose}
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   358
(\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled,
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   359
fewer facts are passed to the prover, \textit{slicing}
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   360
(\S\ref{mode-of-operation}) is disabled, and \textit{timeout}
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   361
(\S\ref{mode-of-operation}) is superseded by the ``Auto Tools Time Limit'' in
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   362
Proof General's ``Isabelle'' menu. Sledgehammer's output is also more concise.
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   363
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   364
\section{Option Reference}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   365
\label{option-reference}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   366
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   367
\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   368
\def\qty#1{$\left<\textit{#1}\right>$}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   369
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   370
\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
   371
\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
   372
\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
   373
\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
   374
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   375
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   376
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   377
\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
   378
\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
   379
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   380
Sledgehammer's options are categorized as follows:\ mode of operation
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   381
(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   382
relevance filter (\S\ref{relevance-filter}), output format
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   383
(\S\ref{output-format}), and authentication (\S\ref{authentication}).
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   384
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   385
The descriptions below refer to the following syntactic quantities:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   386
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   387
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   388
\item[$\bullet$] \qtybf{string}: A string.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   389
\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   390
\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   391
\textit{smart}.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   392
\item[$\bullet$] \qtybf{int\/}: An integer.
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   393
\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
   394
(e.g., 0.6 0.95).
38591
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   395
\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
   396
\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
   397
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
   398
\textit{none} ($\infty$ seconds).
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   399
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   400
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   401
Default values are indicated in square brackets. Boolean options have a negated
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   402
counterpart (e.g., \textit{blocking} vs.\ \textit{non\_blocking}). When setting
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   403
Boolean options, ``= \textit{true}'' may be omitted.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   404
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   405
\subsection{Mode of Operation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   406
\label{mode-of-operation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   407
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   408
\begin{enum}
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   409
\opnodefault{provers}{string}
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   410
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
   411
``\textit{e}~\textit{spass}''). The following provers are supported:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   412
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   413
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   414
\item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   415
\cite{schulz-2002}. To use E, set the environment variable
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   416
\texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable,
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   417
or install the prebuilt E package from Isabelle's download page. See
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   418
\S\ref{installation} for details.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   419
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   420
\item[$\bullet$] \textbf{\textit{spass}:} SPASS is an ATP developed by Christoph
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   421
Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   422
environment variable \texttt{SPASS\_HOME} to the directory that contains the
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   423
\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
   424
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
   425
\S\ref{installation} for details.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   426
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   427
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   428
Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   429
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   430
that contains the \texttt{vampire} executable. Sledgehammer has been tested with
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   431
versions 11, 0.6, and 1.0.
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   432
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   433
\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
   434
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
   435
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
   436
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
   437
2.2.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   438
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   439
\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   440
SRI \cite{yices}. To use Yices, set the environment variable
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   441
\texttt{YICES\_SOLVER} to the complete path of the executable, including the
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   442
file name. Sledgehammer has been tested with version 1.0.
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   443
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   444
\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
   445
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
   446
\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
   447
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
   448
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   449
\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
   450
ATP, exploiting Z3's undocumented support for the TPTP format. It is included
42442
036142bd0302 fixed typo in documentation
blanchet
parents: 42237
diff changeset
   451
for experimental purposes. It requires version 2.18 or above.
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   452
38601
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   453
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   454
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   455
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   456
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
38601
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   457
Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   458
42535
3c1f302b3ee6 added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
blanchet
parents: 42523
diff changeset
   459
\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
   460
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
   461
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
   462
(TFF). It is supported primarily for experimenting with the
3c1f302b3ee6 added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
blanchet
parents: 42523
diff changeset
   463
\textit{type\_sys} $=$ \textit{many\_typed} option (\S\ref{problem-encoding}).
3c1f302b3ee6 added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
blanchet
parents: 42523
diff changeset
   464
38601
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   465
\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   466
developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   467
SInE runs on Geoff Sutcliffe's Miami servers.
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   468
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   469
\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a prover
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   470
developed by Stickel et al.\ \cite{snark}. The remote version of
0da6db609c1f update docs
blanchet
parents: 38591
diff changeset
   471
SNARK runs on Geoff Sutcliffe's Miami servers.
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   472
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
   473
\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
   474
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
   475
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
   476
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   477
\item[$\bullet$] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   478
servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   479
point).
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   480
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   481
\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
   482
as an ATP'' runs on Geoff Sutcliffe's Miami servers.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   483
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   484
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   485
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
   486
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
   487
parallel---either locally or remotely, depending on the number of processor
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   488
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
   489
overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   490
in Proof General.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   491
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   492
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
   493
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
   494
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
   495
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
   496
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   497
\opnodefault{prover}{string}
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   498
Alias for \textit{provers}.
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   499
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   500
\opnodefault{atps}{string}
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   501
Legacy alias for \textit{provers}.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   502
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   503
\opnodefault{atp}{string}
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   504
Legacy alias for \textit{provers}.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   505
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   506
\opdefault{timeout}{float\_or\_none}{\upshape 30}
40341
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40203
diff changeset
   507
Specifies the maximum number of seconds that the automatic provers should spend
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   508
searching for a proof. For historical reasons, the default value of this option
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   509
can be overridden using the option ``Sledgehammer: Time Limit'' from the
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   510
``Isabelle'' menu in Proof General.
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   511
38983
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   512
\opfalse{blocking}{non\_blocking}
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   513
Specifies whether the \textbf{sledgehammer} command should operate
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   514
synchronously. The asynchronous (non-blocking) mode lets the user start proving
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   515
the putative theorem manually while Sledgehammer looks for a proof, but it can
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   516
also be more confusing.
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   517
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   518
\optrue{slicing}{no\_slicing}
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   519
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
   520
segments, each of which has its own set of possibly prover-dependent options.
42446
d105b1309a8d rewording
blanchet
parents: 42443
diff changeset
   521
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
   522
set-of-support (SOS) strategy, whereas the second slice runs without it. For E,
42446
d105b1309a8d rewording
blanchet
parents: 42443
diff changeset
   523
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
   524
number of facts. For SMT solvers, several slices are tried with the same options
42446
d105b1309a8d rewording
blanchet
parents: 42443
diff changeset
   525
each time but fewer and fewer facts. According to benchmarks with a timeout of
d105b1309a8d rewording
blanchet
parents: 42443
diff changeset
   526
30 seconds, slicing is a valuable optimization, and you should probably leave it
d105b1309a8d rewording
blanchet
parents: 42443
diff changeset
   527
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
   528
disabled for (short) automatic runs.
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   529
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   530
\nopagebreak
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   531
{\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
   532
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   533
\opfalse{overlord}{no\_overlord}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   534
Specifies whether Sledgehammer should put its temporary files in
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   535
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   536
debugging Sledgehammer but also unsafe if several instances of the tool are run
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   537
simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   538
safely remove them after Sledgehammer has run.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   539
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   540
\nopagebreak
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   541
{\small See also \textit{debug} (\S\ref{output-format}).}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   542
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   543
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   544
\subsection{Problem Encoding}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   545
\label{problem-encoding}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   546
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   547
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   548
\opfalse{explicit\_apply}{implicit\_apply}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   549
Specifies whether function application should be encoded as an explicit
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   550
``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
   551
function will be directly applied to as many arguments as possible. Enabling
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   552
this option can sometimes help discover higher-order proofs that otherwise would
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   553
not be found.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   554
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   555
\opfalse{full\_types}{partial\_types}
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   556
Specifies whether full-type information is encoded in ATP problems. Enabling
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   557
this option can prevent the discovery of type-incorrect proofs, but it also
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   558
tends to slow down the ATPs significantly. For historical reasons, the default
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   559
value of this option can be overridden using the option ``Sledgehammer: Full
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   560
Types'' from the ``Isabelle'' menu in Proof General.
42228
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   561
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   562
\opfalse{full\_types}{partial\_types}
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   563
Specifies whether full-type information is encoded in ATP problems. Enabling
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   564
this option can prevent the discovery of type-incorrect proofs, but it also
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   565
tends to slow down the ATPs significantly. For historical reasons, the default
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   566
value of this option can be overridden using the option ``Sledgehammer: Full
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   567
Types'' from the ``Isabelle'' menu in Proof General.
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   568
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   569
\opdefault{type\_sys}{string}{smart}
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   570
Specifies the type system to use in ATP problems. The option can take the
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   571
following values:
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   572
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   573
\begin{enum}
42523
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42511
diff changeset
   574
\item[$\bullet$] \textbf{\textit{many\_typed}:} Use the prover's support for
42535
3c1f302b3ee6 added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
blanchet
parents: 42523
diff changeset
   575
many-typed first-order logic if available; otherwise, fall back on
42591
f139d0ac2d44 minor doc fixes
blanchet
parents: 42589
diff changeset
   576
\textit{mangled\_preds}. The problem is monomorphized, meaning that the
f139d0ac2d44 minor doc fixes
blanchet
parents: 42589
diff changeset
   577
problem's type variables are instantiated with heuristically chosen ground
f139d0ac2d44 minor doc fixes
blanchet
parents: 42589
diff changeset
   578
types. Monomorphization can simplify reasoning but also leads to larger fact
f139d0ac2d44 minor doc fixes
blanchet
parents: 42589
diff changeset
   579
bases, which can slow down the ATPs.
42582
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   580
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
   581
\item[$\bullet$] \textbf{\textit{preds}:} Types are encoded using a binary predicate
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
   582
$\mathit{has\_type\/}(\tau, t)$ that restricts the range of bound variables.
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
   583
Constants are annotated with their types, supplied as extra arguments, to
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
   584
resolve overloading.
42582
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   585
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
   586
\item[$\bullet$] \textbf{\textit{mono\_preds}:} Similar to \textit{preds}, but
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
   587
the problem is additionally monomorphized. This corresponds to the traditional
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
   588
encoding of types in an untyped logic without overloading (e.g., such as
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
   589
performed by the ToFoF-E wrapper).
42582
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   590
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
   591
\item[$\bullet$] \textbf{\textit{mangled\_preds}:} Similar to
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
   592
\textit{mono\_preds}, but types are mangled in constant names instead of being
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
   593
supplied as ground term arguments. The binary predicate
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
   594
$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate
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
   595
$\mathit{has\_type\_}\tau(t)$.
42582
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   596
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
   597
\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with
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
   598
its type using a function $\mathit{type\_info\/}(\tau, t)$.
42582
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   599
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   600
\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   601
the problem is additionally monomorphized.
42228
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   602
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
   603
\item[$\bullet$] \textbf{\textit{mangled\_tags}:} Similar to
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
   604
\textit{mono\_tags}, but types are mangled in constant names instead of being
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
   605
supplied as ground term arguments. The binary 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
   606
$\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
   607
$\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
   608
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
   609
\item[$\bullet$]
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
   610
\textbf{%
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
   611
\textit{preds}!,
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
   612
\textit{mono\_preds}!,
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
   613
\textit{mangled\_preds}!, \\
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
   614
\textit{tags}!,
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
   615
\textit{mono\_tags}!,
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
   616
\textit{mangled\_tags}!:} \\
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
   617
The type systems \textit{preds}, \textit{mono\_preds}, \textit{mangled\_preds},
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
   618
\textit{tags}, \textit{mono\_tags}, and \textit{mangled\_tags} are fully typed
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
   619
and virtually sound. For each of these, Sledgehammer also provides a mildly
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
   620
unsound variant identified by an exclamation mark (!)\ that types only finite
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
   621
(and hence especially dangerous) types.
42582
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   622
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   623
\item[$\bullet$]
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   624
\textbf{%
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
   625
\textit{preds}?,
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
   626
\textit{mono\_preds}?,
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
   627
\textit{mangled\_preds}?, \\
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
   628
\textit{tags}?,
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
   629
\textit{mono\_tags}?,
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
   630
\textit{mangled\_tags}?:} \\
42591
f139d0ac2d44 minor doc fixes
blanchet
parents: 42589
diff changeset
   631
If the exclamation mark (!)\ is replaced by an question mark (?),\ the type
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
   632
systems type only nonmonotonic (and hence especially dangerous) types. Not
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
   633
implemented yet.
42582
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   634
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
   635
\item[$\bullet$] \textbf{\textit{const\_args}:}
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
   636
Constants are annotated with their types, supplied as extra arguments, to
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
   637
resolve overloading. Variables are unbounded.
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
   638
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
   639
\item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to
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
   640
the ATP. Types are simply erased.
42228
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   641
42237
e645d7255bd4 renamed "const_args" option value to "args"
blanchet
parents: 42234
diff changeset
   642
\item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
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
   643
uses a fully typed, virtually sound encoding; otherwise, uses any encoding. The
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
   644
actual encoding used depends on the ATP and should be the most efficient for
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
   645
that ATP.
42228
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   646
\end{enum}
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
   647
42582
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
   648
For SMT solvers and ToFoF-E, the type system is always \textit{many\_typed}.
42523
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42511
diff changeset
   649
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42511
diff changeset
   650
\opdefault{monomorphize\_limit}{int}{\upshape 4}
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42511
diff changeset
   651
Specifies the maximum number of iterations for the monomorphization fixpoint
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42511
diff changeset
   652
construction. The higher this limit is, the more monomorphic instances are
42591
f139d0ac2d44 minor doc fixes
blanchet
parents: 42589
diff changeset
   653
potentially generated. Whether monomorphization takes place depends on the
f139d0ac2d44 minor doc fixes
blanchet
parents: 42589
diff changeset
   654
type system used.
38591
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   655
\end{enum}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   656
38591
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   657
\subsection{Relevance Filter}
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   658
\label{relevance-filter}
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   659
7400530ab1d0 update docs
blanchet
parents: 38063
diff changeset
   660
\begin{enum}
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   661
\opdefault{relevance\_thresholds}{float\_pair}{\upshape 0.45~0.85}
38746
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   662
Specifies the thresholds above which facts are considered relevant by the
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   663
relevance filter. The first threshold is used for the first iteration of the
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   664
relevance filter and the second threshold is used for the last iteration (if it
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   665
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
   666
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
   667
are relevant and 1 only theorems that refer to previously seen constants.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   668
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   669
\opsmart{max\_relevant}{int\_or\_smart}
38746
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   670
Specifies the maximum number of facts that may be returned by the relevance
9b465a288c62 update docs
blanchet
parents: 38741
diff changeset
   671
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
   672
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
   673
300.
42180
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 41747
diff changeset
   674
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   675
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   676
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   677
\subsection{Output Format}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   678
\label{output-format}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   679
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   680
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   681
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   682
\opfalse{verbose}{quiet}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   683
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
   684
This option is implicitly disabled for automatic runs.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   685
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   686
\opfalse{debug}{no\_debug}
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   687
Specifies whether Sledgehammer should display additional debugging information
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   688
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
   689
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
   690
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
   691
automatic runs.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   692
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   693
\nopagebreak
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   694
{\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   695
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   696
\opfalse{isar\_proof}{no\_isar\_proof}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   697
Specifies whether Isar proofs should be output in addition to one-liner
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   698
\textit{metis} proofs. Isar proof construction is still experimental and often
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   699
fails; however, they are usually faster and sometimes more robust than
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   700
\textit{metis} proofs.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   701
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   702
\opdefault{isar\_shrink\_factor}{int}{\upshape 1}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   703
Specifies the granularity of the Isar proof. A value of $n$ indicates that each
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   704
Isar proof step should correspond to a group of up to $n$ consecutive proof
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   705
steps in the ATP proof.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   706
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   707
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   708
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   709
\subsection{Authentication}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   710
\label{authentication}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   711
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   712
\begin{enum}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   713
\opnodefault{expect}{string}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   714
Specifies the expected outcome, which must be one of the following:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   715
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   716
\begin{enum}
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   717
\item[$\bullet$] \textbf{\textit{some}:} Sledgehammer found a (potentially
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   718
unsound) proof.
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   719
\item[$\bullet$] \textbf{\textit{none}:} Sledgehammer found no proof.
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   720
\item[$\bullet$] \textbf{\textit{unknown}:} Sledgehammer encountered some
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   721
problem.
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   722
\end{enum}
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   723
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   724
Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   725
(otherwise) if the actual outcome differs from the expected outcome. This option
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   726
is useful for regression testing.
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   727
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   728
\nopagebreak
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   729
{\small See also \textit{blocking} (\S\ref{mode-of-operation}).}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   730
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   731
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   732
\let\em=\sl
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   733
\bibliography{../manual}{}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   734
\bibliographystyle{abbrv}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   735
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   736
\end{document}