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