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