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