src/Doc/Sledgehammer/document/root.tex
author blanchet
Thu, 28 Aug 2014 20:06:59 +0200
changeset 58090 f8ddde112e54
parent 57784 913b5dd101cb
child 58497 20aaa307c0ff
permissions -rw-r--r--
clarified docs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     1
\documentclass[a4paper,12pt]{article}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     2
\usepackage[T1]{fontenc}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     3
\usepackage{amsmath}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     4
\usepackage{amssymb}
53091
d2afb0eb82e2 removed french option to manuals
blanchet
parents: 52996
diff changeset
     5
\usepackage[english]{babel}
36926
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}
48962
a1acc1cb0271 more standard document preparation within session context;
wenzelm
parents: 48803
diff changeset
    13
\usepackage{isabelle,iman,pdfsetup}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    14
50929
7f0bc95af61c updated docs
blanchet
parents: 50720
diff changeset
    15
\newcommand\download{\url{http://isabelle.in.tum.de/components/}}
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
    16
57040
blanchet
parents: 57029
diff changeset
    17
\let\oldS=\S
blanchet
parents: 57029
diff changeset
    18
\def\S{\oldS\,}
blanchet
parents: 57029
diff changeset
    19
43216
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
    20
\def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}}
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
    21
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$}
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
    22
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
    23
\newcommand\const[1]{\textsf{#1}}
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
    24
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    25
%\oddsidemargin=4.6mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    26
%\evensidemargin=4.6mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    27
%\textwidth=150mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    28
%\topmargin=4.6mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    29
%\headheight=0mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    30
%\headsep=0mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    31
%\textheight=234mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    32
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    33
\def\Colon{\mathord{:\mkern-1.5mu:}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    34
%\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    35
%\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    36
\def\lparr{\mathopen{(\mkern-4mu\mid}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    37
\def\rparr{\mathclose{\mid\mkern-4mu)}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    38
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    39
\def\unk{{?}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    40
\def\undef{(\lambda x.\; \unk)}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    41
%\def\unr{\textit{others}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    42
\def\unr{\ldots}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    43
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    44
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    45
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    46
\urlstyle{tt}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    47
55290
3951ced4156c searchable underscores
blanchet
parents: 55289
diff changeset
    48
\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
3951ced4156c searchable underscores
blanchet
parents: 55289
diff changeset
    49
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    50
\begin{document}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    51
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
    52
%%% TYPESETTING
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
    53
%\renewcommand\labelitemi{$\bullet$}
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
    54
\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
    55
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    56
\title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    57
Hammering Away \\[\smallskipamount]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    58
\Large A User's Guide to Sledgehammer for Isabelle/HOL}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    59
\author{\hbox{} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    60
Jasmin Christian Blanchette \\
43002
e88fde86e4c2 mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents: 42996
diff changeset
    61
{\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
    62
{\normalsize with contributions from} \\[4\smallskipamount]
e88fde86e4c2 mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents: 42996
diff changeset
    63
Lawrence C. Paulson \\
e88fde86e4c2 mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents: 42996
diff changeset
    64
{\normalsize Computer Laboratory, University of Cambridge} \\
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    65
\hbox{}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    66
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    67
\maketitle
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    68
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    69
\tableofcontents
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    70
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    71
\setlength{\parskip}{.7em plus .2em minus .1em}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    72
\setlength{\parindent}{0pt}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    73
\setlength{\abovedisplayskip}{\parskip}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    74
\setlength{\abovedisplayshortskip}{.9\parskip}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    75
\setlength{\belowdisplayskip}{\parskip}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    76
\setlength{\belowdisplayshortskip}{.9\parskip}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    77
52078
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
    78
% general-purpose enum environment with correct spacing
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    79
\newenvironment{enum}%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    80
    {\begin{list}{}{%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    81
        \setlength{\topsep}{.1\parskip}%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    82
        \setlength{\partopsep}{.1\parskip}%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    83
        \setlength{\itemsep}{\parskip}%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    84
        \advance\itemsep by-\parsep}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    85
    {\end{list}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    86
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    87
\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    88
\advance\rightskip by\leftmargin}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    89
\def\post{\vskip0pt plus1ex\endgroup}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    90
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    91
\def\prew{\pre\advance\rightskip by-\leftmargin}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    92
\def\postw{\post}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    93
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    94
\section{Introduction}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    95
\label{introduction}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    96
42964
bf45fd2488a2 document primitive support for LEO-II and Satallax
blanchet
parents: 42945
diff changeset
    97
Sledgehammer is a tool that applies automatic theorem provers (ATPs)
47561
92d88c89efff update documentation (mostly based on feedback by Makarius)
blanchet
parents: 47530
diff changeset
    98
and satisfiability-modulo-theories (SMT) solvers on the current goal.%
92d88c89efff update documentation (mostly based on feedback by Makarius)
blanchet
parents: 47530
diff changeset
    99
\footnote{The distinction between ATPs and SMT solvers is convenient but mostly
92d88c89efff update documentation (mostly based on feedback by Makarius)
blanchet
parents: 47530
diff changeset
   100
historical. The two communities are converging, with more and more ATPs
47672
1bf4fa90cd03 fixed typos
blanchet
parents: 47642
diff changeset
   101
supporting typical SMT features such as arithmetic and sorts, and a few SMT
47561
92d88c89efff update documentation (mostly based on feedback by Makarius)
blanchet
parents: 47530
diff changeset
   102
solvers parsing ATP syntaxes. There is also a strong technological connection
92d88c89efff update documentation (mostly based on feedback by Makarius)
blanchet
parents: 47530
diff changeset
   103
between instantiation-based ATPs (such as iProver and iProver-Eq) and SMT
92d88c89efff update documentation (mostly based on feedback by Makarius)
blanchet
parents: 47530
diff changeset
   104
solvers.}
92d88c89efff update documentation (mostly based on feedback by Makarius)
blanchet
parents: 47530
diff changeset
   105
%
55334
5f5104069b33 agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents: 55297
diff changeset
   106
The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
52078
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   107
\cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF \cite{tofof}, iProver
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   108
\cite{korovin-2009}, iProver-Eq \cite{korovin-sticksel-2010}, LEO-II
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   109
\cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   110
\cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, and
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   111
Waldmeister \cite{waldmeister}. The ATPs are run either locally or remotely via
57241
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   112
the System\-On\-TPTP web service \cite{sutcliffe-2000}. The supported SMT
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   113
solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, and Z3 \cite{z3}. These are
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   114
always run locally.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   115
57241
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   116
The problem passed to the external provers (or solvers) consists of your current
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   117
goal together with a heuristic selection of hundreds of facts (theorems) from the
52078
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   118
current theory context, filtered by relevance.
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   119
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   120
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
   121
not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
55297
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55290
diff changeset
   122
proof typically relies on the general-purpose \textit{metis} proof method, which
45380
c33a37ccd187 updated documentation
blanchet
parents: 45339
diff changeset
   123
integrates the Metis ATP in Isabelle/HOL with explicit inferences going through
c33a37ccd187 updated documentation
blanchet
parents: 45339
diff changeset
   124
the kernel. Thus its results are correct by construction.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   125
53760
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53759
diff changeset
   126
For Isabelle/jEdit users, Sledgehammer provides an automatic mode that can be
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53759
diff changeset
   127
enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options >
54114
84791e3fdcde updated S/H docs
blanchet
parents: 54015
diff changeset
   128
Isabelle > General.'' In this mode, a reduced version of Sledgehammer is run on
84791e3fdcde updated S/H docs
blanchet
parents: 54015
diff changeset
   129
every newly entered theorem for a few seconds.
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   130
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   131
\newbox\boxA
46298
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   132
\setbox\boxA=\hbox{\texttt{NOSPAM}}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   133
46298
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   134
\newcommand\authoremail{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   135
in.\allowbreak tum.\allowbreak de}}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   136
40689
3a10ce7cd436 document requirement on theory import
blanchet
parents: 40343
diff changeset
   137
To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is
3a10ce7cd436 document requirement on theory import
blanchet
parents: 40343
diff changeset
   138
imported---this is rarely a problem in practice since it is part of
3a10ce7cd436 document requirement on theory import
blanchet
parents: 40343
diff changeset
   139
\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   140
\texttt{src/HOL/Metis\_Examples} directory.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   141
Comments and bug reports concerning Sledgehammer or this manual should be
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   142
directed to the author at \authoremail.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   143
53759
a198ce71de11 took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents: 53757
diff changeset
   144
%\vskip2.5\smallskipamount
a198ce71de11 took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents: 53757
diff changeset
   145
%
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   146
%\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   147
%suggesting several textual improvements.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   148
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   149
\section{Installation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   150
\label{installation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   151
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   152
Sledgehammer is part of Isabelle, so you do not need to install it. However, it
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   153
relies on third-party automatic provers (ATPs and SMT solvers).
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   154
55334
5f5104069b33 agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents: 55297
diff changeset
   155
Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Satallax, SPASS, and Vampire can
5f5104069b33 agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents: 55297
diff changeset
   156
be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF, iProver, iProver-Eq,
52078
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   157
LEO-II, Satallax, SNARK, Vampire, and Waldmeister are available remotely via
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   158
System\-On\-TPTP \cite{sutcliffe-2000}. If you want better performance, you
57241
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   159
should at least install E and SPASS locally. The SMT solvers CVC3, CVC4, and Z3
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   160
can be run locally.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   161
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   162
There are three main ways to install automatic provers on your machine:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   163
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   164
\begin{sloppy}
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   165
\begin{enum}
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   166
\item[\labelitemi] If you installed an official Isabelle package, it should
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   167
already include properly setup executables for CVC3, E, SPASS, and Z3, ready to use.%
57237
bc51864c2ac4 took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
blanchet
parents: 57211
diff changeset
   168
\footnote{Vampire's license prevents us from doing the same for
bc51864c2ac4 took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
blanchet
parents: 57211
diff changeset
   169
this otherwise remarkable tool.}
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   170
For Z3, you must additionally set the variable
57028
e5466055e94f added Isabelle system option 'mash'
blanchet
parents: 57019
diff changeset
   171
\texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a
56119
2e44053fee87 updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents: 55334
diff changeset
   172
noncommercial user---either in the environment in which Isabelle is
2e44053fee87 updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents: 55334
diff changeset
   173
launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or
57028
e5466055e94f added Isabelle system option 'mash'
blanchet
parents: 57019
diff changeset
   174
via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
56119
2e44053fee87 updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents: 55334
diff changeset
   175
> Isabelle > General'' in Isabelle/jEdit.
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   176
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   177
\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, E,
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   178
SPASS, and Z3 binary packages from \download. Extract the archives, then add a
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   179
line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}%
41747
f58d4d202924 fix path to etc/settings and etc/components in doc
blanchet
parents: 41740
diff changeset
   180
\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   181
startup. Its value can be retrieved by executing \texttt{isabelle}
41747
f58d4d202924 fix path to etc/settings and etc/components in doc
blanchet
parents: 41740
diff changeset
   182
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   183
file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   184
\texttt{components} file does not exist yet and you extracted SPASS to
47577
b8f33b19e20b doc update
blanchet
parents: 47561
diff changeset
   185
\texttt{/usr/local/spass-3.8ds}, create it with the single line
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   186
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   187
\prew
47577
b8f33b19e20b doc update
blanchet
parents: 47561
diff changeset
   188
\texttt{/usr/local/spass-3.8ds}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   189
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   190
47561
92d88c89efff update documentation (mostly based on feedback by Makarius)
blanchet
parents: 47530
diff changeset
   191
in it.
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   192
55334
5f5104069b33 agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents: 55297
diff changeset
   193
\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II,
52078
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   194
Satallax, or SPASS manually, or found a Vampire executable somewhere (e.g.,
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   195
\url{http://www.vprover.org/}), set the environment variable
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   196
\texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME},
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   197
\texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or
52757
ea7cf7b14fdd updated Sledgehammer prover versions
blanchet
parents: 52078
diff changeset
   198
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{agsyHOL},
ea7cf7b14fdd updated Sledgehammer prover versions
blanchet
parents: 52078
diff changeset
   199
\texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}),
52078
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   200
\texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable;
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   201
for Alt-Ergo, set the
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   202
environment variable \texttt{WHY3\_HOME} to the directory that contains the
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   203
\texttt{why3} executable.
57636
3ab503b04bdb stick to external proofs when invoking E, because they are more detailed and do not merge steps
blanchet
parents: 57566
diff changeset
   204
Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 1.8,
52996
9a47c8256054 updated Vampire version numbers
blanchet
parents: 52757
diff changeset
   205
LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 3.0.%
38063
458c4578761f mention version numbers
blanchet
parents: 38043
diff changeset
   206
\footnote{Following the rewrite of Vampire, the counter for version numbers was
52996
9a47c8256054 updated Vampire version numbers
blanchet
parents: 52757
diff changeset
   207
reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more
48652
15f0cf52deea document E-MaLeS
blanchet
parents: 48540
diff changeset
   208
recent than 9.0 or 11.5.}%
48006
8d989b9c8e4f update docs
blanchet
parents: 47963
diff changeset
   209
Since the ATPs' output formats are neither documented nor stable, other
47577
b8f33b19e20b doc update
blanchet
parents: 47561
diff changeset
   210
versions might not work well with Sledgehammer. Ideally,
b8f33b19e20b doc update
blanchet
parents: 47561
diff changeset
   211
you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   212
\texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
56380
9bb2856cc845 don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
blanchet
parents: 56379
diff changeset
   213
\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0'').
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   214
57241
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   215
Similarly, if you want to build CVC3 or CVC4, or found a
57237
bc51864c2ac4 took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
blanchet
parents: 57211
diff changeset
   216
Z3 executable somewhere (e.g., \url{http://z3.codeplex.com/}),
57241
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   217
set the environment variable \texttt{CVC3\_\allowbreak SOLVER},
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   218
\texttt{CVC4\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   219
of the executable, \emph{including the file name}. Sledgehammer has been tested
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   220
with CVC3 2.2 and 2.4.1, CVC4 1.2, and Z3 4.3.2. Since Z3's output format is
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   221
somewhat unstable, other versions of the solver might not work well with
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   222
Sledgehammer. Ideally, also set
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   223
\texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, or \texttt{Z3\_NEW\_VERSION} to
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   224
the solver's version number (e.g., ``4.3.2'').
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   225
\end{enum}
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   226
\end{sloppy}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   227
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   228
To check whether E, SPASS, Vampire, and/or Z3 are successfully installed, try
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   229
out the example in \S\ref{first-steps}. If the remote versions of any of these
56120
04c37dfef684 updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents: 56119
diff changeset
   230
provers is used (identified by the prefix ``\textit{remote\_\/}''), or if the
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   231
local versions fail to solve the easy goal presented there, something must be
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   232
wrong with the installation.
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   233
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   234
Remote prover invocation requires Perl with the World Wide Web Library
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   235
(\texttt{libwww-perl}) installed. If you must use a proxy server to access the
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   236
Internet, set the \texttt{http\_proxy} environment variable to the proxy, either
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   237
in the environment in which Isabelle is launched or in your
47561
92d88c89efff update documentation (mostly based on feedback by Makarius)
blanchet
parents: 47530
diff changeset
   238
\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   239
examples:
39152
f09b378cb252 make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents: 38997
diff changeset
   240
f09b378cb252 make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents: 38997
diff changeset
   241
\prew
39153
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   242
\texttt{http\_proxy=http://proxy.example.org} \\
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   243
\texttt{http\_proxy=http://proxy.example.org:8080} \\
b1c2c03fd9d7 mention ~/.isabelle/etc/settings file
blanchet
parents: 39152
diff changeset
   244
\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
   245
\postw
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   246
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   247
\section{First Steps}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   248
\label{first-steps}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   249
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   250
To illustrate Sledgehammer in context, let us start a theory file and
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   251
attempt to prove a simple lemma:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   252
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   253
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   254
\textbf{theory}~\textit{Scratch} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   255
\textbf{imports}~\textit{Main} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   256
\textbf{begin} \\[2\smallskipamount]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   257
%
42945
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   258
\textbf{lemma} ``$[a] = [b] \,\Longrightarrow\, a = b$'' \\
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   259
\textbf{sledgehammer}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   260
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   261
53760
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53759
diff changeset
   262
Instead of issuing the \textbf{sledgehammer} command, you can also use the
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53759
diff changeset
   263
Sledgehammer panel in Isabelle/jEdit. Sledgehammer produces the following output
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53759
diff changeset
   264
after a few seconds:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   265
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   266
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   267
\slshape
57053
46000c075d07 shorten Sledgehammer output, as suggested by Andrei Popescu
blanchet
parents: 57040
diff changeset
   268
Sledgehammer: ``\textit{e\/}'' \\
43054
f1864c0bd165 update minimization documentation
blanchet
parents: 43053
diff changeset
   269
Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]
42945
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   270
%
57053
46000c075d07 shorten Sledgehammer output, as suggested by Andrei Popescu
blanchet
parents: 57040
diff changeset
   271
Sledgehammer: ``\textit{z3\/}'' \\
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   272
Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount]
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   273
%
57053
46000c075d07 shorten Sledgehammer output, as suggested by Andrei Popescu
blanchet
parents: 57040
diff changeset
   274
Sledgehammer: ``\textit{vampire\/}'' \\
43054
f1864c0bd165 update minimization documentation
blanchet
parents: 43053
diff changeset
   275
Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   276
%
57053
46000c075d07 shorten Sledgehammer output, as suggested by Andrei Popescu
blanchet
parents: 57040
diff changeset
   277
Sledgehammer: ``\textit{spass\/}'' \\
43054
f1864c0bd165 update minimization documentation
blanchet
parents: 43053
diff changeset
   278
Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   279
%
57053
46000c075d07 shorten Sledgehammer output, as suggested by Andrei Popescu
blanchet
parents: 57040
diff changeset
   280
Sledgehammer: ``\textit{remote\_e\_sine\/}'' \\
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   281
Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms).
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   282
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   283
53759
a198ce71de11 took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents: 53757
diff changeset
   284
Sledgehammer ran E, E-SInE, SPASS, Vampire, and Z3 in parallel. Depending on
a198ce71de11 took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents: 53757
diff changeset
   285
which provers are installed and how many processor cores are available, some of
a198ce71de11 took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents: 53757
diff changeset
   286
the provers might be missing or present with a \textit{remote\_} prefix.
a198ce71de11 took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents: 53757
diff changeset
   287
Waldmeister is run only for unit equational problems, where the goal's
a198ce71de11 took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents: 53757
diff changeset
   288
conclusion is a (universally quantified) equation.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   289
55297
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55290
diff changeset
   290
For each successful prover, Sledgehammer gives a one-line \textit{metis} or
56120
04c37dfef684 updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents: 56119
diff changeset
   291
\textit{smt2} method call. Rough timings are shown in parentheses, indicating how
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   292
fast the call is. You can click the proof to insert it into the theory text.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   293
51190
2654b3965c8d made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents: 51189
diff changeset
   294
In addition, you can ask Sledgehammer for an Isar text proof by enabling the
49919
54ec43352eb1 updated docs
blanchet
parents: 49365
diff changeset
   295
\textit{isar\_proofs} option (\S\ref{output-format}):
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   296
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   297
\prew
49919
54ec43352eb1 updated docs
blanchet
parents: 49365
diff changeset
   298
\textbf{sledgehammer} [\textit{isar\_proofs}]
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   299
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   300
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   301
When Isar proof construction is successful, it can yield proofs that are more
56120
04c37dfef684 updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents: 56119
diff changeset
   302
readable and also faster than the \textit{metis} or \textit{smt2} one-line
04c37dfef684 updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents: 56119
diff changeset
   303
proofs. This feature is experimental and is only available for ATPs.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   304
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   305
\section{Hints}
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   306
\label{hints}
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   307
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   308
This section presents a few hints that should help you get the most out of
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46640
diff changeset
   309
Sledgehammer. Frequently asked questions are answered in
45380
c33a37ccd187 updated documentation
blanchet
parents: 45339
diff changeset
   310
\S\ref{frequently-asked-questions}.
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   311
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   312
%\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak}
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   313
\newcommand\point[1]{\subsection{\emph{#1}}}
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   314
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   315
\point{Presimplify the goal}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   316
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   317
For best results, first simplify your problem by calling \textit{auto} or at
42945
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   318
least \textit{safe} followed by \textit{simp\_all}. The SMT solvers provide
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   319
arithmetic decision procedures, but the ATPs typically do not (or if they do,
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   320
Sledgehammer does not use it yet). Apart from Waldmeister, they are not
53759
a198ce71de11 took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents: 53757
diff changeset
   321
particularly good at heavy rewriting, but because they regard equations as
42945
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   322
undirected, they often prove theorems that require the reverse orientation of a
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   323
\textit{simp} rule. Higher-order problems can be tackled, but the success rate
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   324
is better for first-order problems. Hence, you may get better results if you
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   325
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
   326
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   327
\point{Make sure E, SPASS, Vampire, and Z3 are locally installed}
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   328
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   329
Locally installed provers are faster and more reliable than those running on
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   330
servers. See \S\ref{installation} for details on how to install them.
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   331
53760
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53759
diff changeset
   332
\point{Familiarize yourself with the main options}
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   333
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   334
Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   335
the options are very specialized, but serious users of the tool should at least
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   336
familiarize themselves with the following options:
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   337
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   338
\begin{enum}
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   339
\item[\labelitemi] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   340
the automatic provers (ATPs and SMT solvers) that should be run whenever
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   341
Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   342
remote\_vampire\/}''). For convenience, you can omit ``\textit{provers}~=''
43014
0dca147765f4 minor fixes to Sledgehammer docs
blanchet
parents: 43010
diff changeset
   343
and simply write the prover names as a space-separated list (e.g., ``\textit{e
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   344
spass remote\_vampire\/}'').
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   345
48294
2b0c5553dc46 doc updates
blanchet
parents: 48184
diff changeset
   346
\item[\labelitemi] \textbf{\textit{max\_facts}} (\S\ref{relevance-filter})
42884
75c94e3319ae more doc fiddling
blanchet
parents: 42883
diff changeset
   347
specifies the maximum number of facts that should be passed to the provers. By
48294
2b0c5553dc46 doc updates
blanchet
parents: 48184
diff changeset
   348
default, the value is prover-dependent but varies between about 50 and 1000. If
2b0c5553dc46 doc updates
blanchet
parents: 48184
diff changeset
   349
the provers time out, you can try lowering this value to, say, 25 or 50 and see
42884
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
49919
54ec43352eb1 updated docs
blanchet
parents: 49365
diff changeset
   352
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
55297
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55290
diff changeset
   353
that Isar proofs should be generated, in addition to one-line \textit{metis} or
56120
04c37dfef684 updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents: 56119
diff changeset
   354
\textit{smt2} proofs. The length of the Isar proofs can be controlled by setting
57245
f6bf6d5341ee renamed Sledgehammer options
blanchet
parents: 57241
diff changeset
   355
\textit{compress} (\S\ref{output-format}).
43038
07ebc2398731 new timeout section (cf. Nitpick manual)
blanchet
parents: 43036
diff changeset
   356
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   357
\item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
43038
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})$''
58090
f8ddde112e54 clarified docs
blanchet
parents: 57784
diff changeset
   368
to force Sledgehammer to run only with $\textit{my\_facts}$ (and any facts
f8ddde112e54 clarified docs
blanchet
parents: 57784
diff changeset
   369
chained into the goal).
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   370
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   371
\section{Frequently Asked Questions}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   372
\label{frequently-asked-questions}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   373
42945
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   374
This sections answers frequently (and infrequently) asked questions about
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   375
Sledgehammer. It is a good idea to skim over it now even if you do not have any
42945
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   376
questions at this stage. And if you have any further questions not listed here,
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   377
send them to the author at \authoremail.
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   378
43008
bb212c2ad238 renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents: 43007
diff changeset
   379
\point{Which facts are passed to the automatic provers?}
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   380
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   381
Sledgehammer heuristically selects a few hundred relevant lemmas from the
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   382
currently loaded libraries. The component that performs this selection is
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   383
called \emph{relevance filter}.
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   384
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   385
\begin{enum}
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   386
\item[\labelitemi]
48388
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
   387
The traditional relevance filter, called \emph{MePo}
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
   388
(\underline{Me}ng--\underline{Pau}lson), assigns a score to every available fact
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
   389
(lemma, theorem, definition, or axiom) based upon how many constants that fact
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
   390
shares with the conjecture. This process iterates to include facts relevant to
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
   391
those just accepted. The constants are weighted to give unusual ones greater
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
   392
significance. MePo copes best when the conjecture contains some unusual
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
   393
constants; if all the constants are common, it is unable to discriminate among
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
   394
the hundreds of facts that are picked up. The filter is also memoryless: It has
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
   395
no information about how many times a particular fact has been used in a proof,
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
   396
and it cannot learn.
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   397
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   398
\item[\labelitemi]
57272
fd539459a112 enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
blanchet
parents: 57245
diff changeset
   399
An alternative to MePo is \emph{MaSh} (\underline{Ma}chine Learner for
fd539459a112 enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
blanchet
parents: 57245
diff changeset
   400
\underline{S}ledge\underline{h}ammer). It applies machine learning to the
fd539459a112 enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
blanchet
parents: 57245
diff changeset
   401
problem of finding relevant facts.
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   402
50459
52ec07a7f304 changed capitalization of MeSh filter
blanchet
parents: 50221
diff changeset
   403
\item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh.
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   404
\end{enum}
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   405
50459
52ec07a7f304 changed capitalization of MeSh filter
blanchet
parents: 50221
diff changeset
   406
The default is either MePo or MeSh, depending on whether the environment
50221
355aaa57ac39 updated MaSh doc
blanchet
parents: 50020
diff changeset
   407
variable \texttt{MASH} is set and what class of provers the target prover
355aaa57ac39 updated MaSh doc
blanchet
parents: 50020
diff changeset
   408
belongs to (\S\ref{relevance-filter}).
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   409
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   410
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
   411
some provers get overwhelmed more easily than others. You can show the number of
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   412
facts given using the \textit{verbose} option (\S\ref{output-format}) and the
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   413
actual facts using \textit{debug} (\S\ref{output-format}).
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   414
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   415
Sledgehammer is good at finding short proofs combining a handful of existing
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   416
lemmas. If you are looking for longer proofs, you must typically restrict the
48294
2b0c5553dc46 doc updates
blanchet
parents: 48184
diff changeset
   417
number of facts, by setting the \textit{max\_facts} option
43574
940b714bd35e document "sound" option
blanchet
parents: 43571
diff changeset
   418
(\S\ref{relevance-filter}) to, say, 25 or 50.
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   419
42996
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   420
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
   421
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
   422
``$(\textit{add}{:}~\textit{my\_facts})$'' syntax. For example:
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   423
%
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   424
\prew
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   425
\textbf{sledgehammer} (\textit{add}: \textit{hd.simps} \textit{tl.simps})
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   426
\postw
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   427
%
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   428
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
   429
included; the other selected facts remain the same.
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   430
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
   431
the facts via \textbf{using}:
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   432
%
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   433
\prew
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   434
\textbf{using} \textit{hd.simps} \textit{tl.simps} \\
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   435
\textbf{sledgehammer}
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   436
\postw
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   437
%
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   438
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
   439
selected at iteration $j$ they also influence which facts are selected at
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   440
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
   441
%
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   442
\prew
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   443
\textbf{using} \textit{hd.simps} \textit{tl.simps} \\
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   444
\textbf{apply}~\textbf{--} \\
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   445
\textbf{sledgehammer}
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   446
\postw
29be053ec75b document relevance filter a bit more
blanchet
parents: 42995
diff changeset
   447
46300
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   448
\point{Why does Metis fail to reconstruct the proof?}
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   449
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   450
There are many reasons. If Metis runs seemingly forever, that is a sign that the
57736
5f37ef22f9af update documentation after removal of 'min' subcommand
blanchet
parents: 57733
diff changeset
   451
proof is too difficult for it. Metis's search is complete for first-order logic
5f37ef22f9af update documentation after removal of 'min' subcommand
blanchet
parents: 57733
diff changeset
   452
with equality, so if the proof was found by an ATP such as E, SPASS, or Vampire,
5f37ef22f9af update documentation after removal of 'min' subcommand
blanchet
parents: 57733
diff changeset
   453
Metis should eventually find it, but that's little consolation.
46300
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   454
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   455
In some rare cases, \textit{metis} fails fairly quickly, and you get the error
57736
5f37ef22f9af update documentation after removal of 'min' subcommand
blanchet
parents: 57733
diff changeset
   456
message ``One-line proof reconstruction failed.'' This indicates that
5f37ef22f9af update documentation after removal of 'min' subcommand
blanchet
parents: 57733
diff changeset
   457
Sledgehammer determined that the goal is provable, but the proof is, for
5f37ef22f9af update documentation after removal of 'min' subcommand
blanchet
parents: 57733
diff changeset
   458
technical reasons, beyond \textit{metis}'s power. You can then try again with
5f37ef22f9af update documentation after removal of 'min' subcommand
blanchet
parents: 57733
diff changeset
   459
the \textit{strict} option (\S\ref{problem-encoding}).
46300
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   460
46640
622691cec7c3 doc fixes (thanks to Nik)
blanchet
parents: 46435
diff changeset
   461
If the goal is actually unprovable and you did not specify an unsound encoding
46300
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   462
using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   463
strongly encouraged to report this to the author at \authoremail.
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   464
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   465
\point{How can I tell whether a suggested proof is sound?}
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   466
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   467
Earlier versions of Sledgehammer often suggested unsound proofs---either proofs
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   468
of nontheorems or simply proofs that rely on type-unsound inferences. This
46640
622691cec7c3 doc fixes (thanks to Nik)
blanchet
parents: 46435
diff changeset
   469
is a thing of the past, unless you explicitly specify an unsound encoding
46300
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   470
using \textit{type\_enc} (\S\ref{problem-encoding}).
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   471
%
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   472
Officially, the only form of ``unsoundness'' that lurks in the sound
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   473
encodings is related to missing characteristic theorems of datatypes. For
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   474
example,
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   475
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   476
\prew
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   477
\textbf{lemma}~``$\exists \mathit{xs}.\; \mathit{xs} \neq []$'' \\
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   478
\textbf{sledgehammer} ()
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   479
\postw
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   480
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   481
suggests an argumentless \textit{metis} call that fails. However, the conjecture
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   482
does actually hold, and the \textit{metis} call can be repaired by adding
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   483
\textit{list.distinct}.
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   484
%
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   485
We hope to address this problem in a future version of Isabelle. In the
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   486
meantime, you can avoid it by passing the \textit{strict} option
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   487
(\S\ref{problem-encoding}).
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
   488
46298
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   489
\point{What are the \textit{full\_types}, \textit{no\_types}, and
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   490
\textit{mono\_tags} arguments to Metis?}
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   491
46298
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   492
The \textit{metis}~(\textit{full\_types}) proof method
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   493
and its cousin \textit{metis}~(\textit{mono\_tags}) are fully-typed
53760
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53759
diff changeset
   494
versions of Metis. It is somewhat slower than \textit{metis}, but the proof
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
   495
search is fully typed, and it also includes more powerful rules such as the
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   496
axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in
55297
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55290
diff changeset
   497
higher-order places (e.g., in set comprehensions). The method is automatically
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55290
diff changeset
   498
tried as a fallback when \textit{metis} fails, and it is sometimes
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
   499
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
   500
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
   501
preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with
57719
249f13fed1a6 reduced preplay timeout to 1 s
blanchet
parents: 57659
diff changeset
   502
various sets of option for up to 1~second each time to ensure that the generated
46298
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   503
one-line proofs actually work and to display timing information. This can be
47036
fc958d7138be document "dont_preplay"
blanchet
parents: 46643
diff changeset
   504
configured using the \textit{preplay\_timeout} and \textit{dont\_preplay}
fc958d7138be document "dont_preplay"
blanchet
parents: 46643
diff changeset
   505
options (\S\ref{timeouts}).)
46298
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   506
%
43229
443708f05bb2 documentation tweaks
blanchet
parents: 43228
diff changeset
   507
At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})
443708f05bb2 documentation tweaks
blanchet
parents: 43228
diff changeset
   508
uses no type information at all during the proof search, which is more efficient
443708f05bb2 documentation tweaks
blanchet
parents: 43228
diff changeset
   509
but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally
443708f05bb2 documentation tweaks
blanchet
parents: 43228
diff changeset
   510
generated by Sledgehammer.
46298
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   511
%
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   512
See the \textit{type\_enc} option (\S\ref{problem-encoding}) for details.
43229
443708f05bb2 documentation tweaks
blanchet
parents: 43228
diff changeset
   513
46298
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   514
Incidentally, if you ever see warnings such as
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   515
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   516
\prew
43007
b48aa3492f0b minor doc adjustments
blanchet
parents: 43005
diff changeset
   517
\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
   518
Metis: Falling back on ``\textit{metis} (\textit{full\_types})''.
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   519
\postw
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   520
45380
c33a37ccd187 updated documentation
blanchet
parents: 45339
diff changeset
   521
for a successful \textit{metis} proof, you can advantageously pass the
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
   522
\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
   523
46366
2ded91a6cbd5 docs and news
blanchet
parents: 46302
diff changeset
   524
\point{And what are the \textit{lifting} and \textit{hide\_lams} arguments
46298
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   525
to Metis?}
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   526
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   527
Orthogonally to the encoding of types, it is important to choose an appropriate
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   528
translation of $\lambda$-abstractions. Metis supports three translation schemes,
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   529
in decreasing order of power: Curry combinators (the default),
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   530
$\lambda$-lifting, and a ``hiding'' scheme that disables all reasoning under
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   531
$\lambda$-abstractions. The more powerful schemes also give the automatic
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   532
provers more rope to hang themselves. See the \textit{lam\_trans} option (\S\ref{problem-encoding}) for details.
e9a2d81fa725 updated docs
blanchet
parents: 46242
diff changeset
   533
43054
f1864c0bd165 update minimization documentation
blanchet
parents: 43053
diff changeset
   534
\point{Are generated proofs minimal?}
43036
0ef380310863 more Sledgehammer documentation updates
blanchet
parents: 43035
diff changeset
   535
43054
f1864c0bd165 update minimization documentation
blanchet
parents: 43053
diff changeset
   536
Automatic provers frequently use many more facts than are necessary.
57722
2c2d5b7f29aa updated docs
blanchet
parents: 57719
diff changeset
   537
Sledgehammer includes a minimization tool that takes a set of facts returned by
2c2d5b7f29aa updated docs
blanchet
parents: 57719
diff changeset
   538
a given prover and repeatedly calls a prover or proof method with subsets of
2c2d5b7f29aa updated docs
blanchet
parents: 57719
diff changeset
   539
those facts to find a minimal set. Reducing the number of facts typically helps
2c2d5b7f29aa updated docs
blanchet
parents: 57719
diff changeset
   540
reconstruction, while also removing superfluous clutter from the proof scripts.
43036
0ef380310863 more Sledgehammer documentation updates
blanchet
parents: 43035
diff changeset
   541
43229
443708f05bb2 documentation tweaks
blanchet
parents: 43228
diff changeset
   542
In earlier versions of Sledgehammer, generated proofs were systematically
443708f05bb2 documentation tweaks
blanchet
parents: 43228
diff changeset
   543
accompanied by a suggestion to invoke the minimization tool. This step is now
57722
2c2d5b7f29aa updated docs
blanchet
parents: 57719
diff changeset
   544
performed by default but can be disabled using the \textit{minimize} option
2c2d5b7f29aa updated docs
blanchet
parents: 57719
diff changeset
   545
(\S\ref{mode-of-operation}).
43036
0ef380310863 more Sledgehammer documentation updates
blanchet
parents: 43035
diff changeset
   546
43008
bb212c2ad238 renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents: 43007
diff changeset
   547
\point{A strange error occurred---what should I do?}
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   548
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   549
Sledgehammer tries to give informative error messages. Please report any strange
53224
f13c49dd9805 tuned messages
blanchet
parents: 53102
diff changeset
   550
error to the author at \authoremail. This applies doubly if you get the message
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   551
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   552
\prew
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   553
\slshape
53224
f13c49dd9805 tuned messages
blanchet
parents: 53102
diff changeset
   554
The prover derived ``\textit{False}'' using ``\textit{foo\/}'',
f13c49dd9805 tuned messages
blanchet
parents: 53102
diff changeset
   555
``\textit{bar\/}'', and ``\textit{baz\/}''.
f13c49dd9805 tuned messages
blanchet
parents: 53102
diff changeset
   556
This could be due to inconsistent axioms (including ``\textbf{sorry}''s) or to
f13c49dd9805 tuned messages
blanchet
parents: 53102
diff changeset
   557
a bug in Sledgehammer. If the problem persists, please contact the
f13c49dd9805 tuned messages
blanchet
parents: 53102
diff changeset
   558
Isabelle developers.
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   559
\postw
42763
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   560
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   561
\point{Auto can solve it---why not Sledgehammer?}
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   562
e588d3e8ad91 added hints and FAQs
blanchet
parents: 42753
diff changeset
   563
Problems can be easy for \textit{auto} and difficult for automatic provers, but
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   564
the reverse is also true, so do not be discouraged if your first attempts fail.
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   565
Because the system refers to all theorems known to Isabelle, it is particularly
57040
blanchet
parents: 57029
diff changeset
   566
suitable when your goal has a short proof but requires lemmas that you do not
blanchet
parents: 57029
diff changeset
   567
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
   568
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   569
\point{Why are there so many options?}
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   570
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   571
Sledgehammer's philosophy should work out of the box, without user guidance.
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   572
Many of the options are meant to be used mostly by the Sledgehammer developers
53102
45a7bfd99b45 doc tuning
blanchet
parents: 53091
diff changeset
   573
for experiments. Of course, feel free to try them out if you are so inclined.
42883
ec1ea24d49bc more FAQs
blanchet
parents: 42877
diff changeset
   574
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   575
\section{Command Syntax}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   576
\label{command-syntax}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   577
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   578
\subsection{Sledgehammer}
57040
blanchet
parents: 57029
diff changeset
   579
\label{sledgehammer}
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   580
36926
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
43216
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
   589
In the general syntax, the \qty{subcommand} may be any of the following:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   590
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   591
\begin{enum}
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   592
\item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on
43216
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
   593
subgoal number \qty{num} (1 by default), with the given options and facts.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   594
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   595
\item[\labelitemi] \textbf{\textit{messages}:} Redisplays recent messages issued
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   596
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
   597
due to Sledgehammer's asynchronous nature. The \qty{num} argument specifies a
47530
9ad8c4315f92 doc update
blanchet
parents: 47075
diff changeset
   598
limit on the number of messages to display (10 by default).
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   599
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   600
\item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of
41724
14d135c09bec transformed lie into truth
blanchet
parents: 41208
diff changeset
   601
automatic provers supported by Sledgehammer. See \S\ref{installation} and
14d135c09bec transformed lie into truth
blanchet
parents: 41208
diff changeset
   602
\S\ref{mode-of-operation} for more information on how to install automatic
14d135c09bec transformed lie into truth
blanchet
parents: 41208
diff changeset
   603
provers.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   604
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   605
\item[\labelitemi] \textbf{\textit{running\_provers}:} Prints information about
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   606
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
   607
time until timeout.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   608
50720
834847691d99 updated docs
blanchet
parents: 50484
diff changeset
   609
\item[\labelitemi] \textbf{\textit{kill\_all}:} Terminates all running
49365
8aebe857aaaa merged two commands
blanchet
parents: 48985
diff changeset
   610
threads (automatic provers and machine learners).
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   611
48393
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   612
\item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   613
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   614
\end{enum}
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   615
49365
8aebe857aaaa merged two commands
blanchet
parents: 48985
diff changeset
   616
In addition, the following subcommands provide finer control over machine
48393
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   617
learning with MaSh:
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   618
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   619
\begin{enum}
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   620
\item[\labelitemi] \textbf{\textit{unlearn}:} Resets MaSh, erasing any
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   621
persistent state.
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   622
48393
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   623
\item[\labelitemi] \textbf{\textit{learn\_isar}:} Invokes MaSh on the current
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   624
theory to process all the available facts, learning from their Isabelle/Isar
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   625
proofs. This happens automatically at Sledgehammer invocations if the
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   626
\textit{learn} option (\S\ref{relevance-filter}) is enabled.
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   627
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50459
diff changeset
   628
\item[\labelitemi] \textbf{\textit{learn\_prover}:} Invokes MaSh on the current
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50459
diff changeset
   629
theory to process all the available facts, learning from proofs generated by
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50459
diff changeset
   630
automatic provers. The prover to use and its timeout can be set using the
48393
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   631
\textit{prover} (\S\ref{mode-of-operation}) and \textit{timeout}
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   632
(\S\ref{timeouts}) options. It is recommended to perform learning using an
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   633
efficient first-order ATP (such as E, SPASS, and Vampire) as opposed to a
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   634
higher-order ATP or an SMT solver.
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   635
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   636
\item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn}
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   637
followed by \textit{learn\_isar}.
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   638
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50459
diff changeset
   639
\item[\labelitemi] \textbf{\textit{relearn\_prover}:} Same as \textit{unlearn}
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50459
diff changeset
   640
followed by \textit{learn\_prover}.
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   641
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   642
\item[\labelitemi] \textbf{\textit{running\_learners}:} Prints information about
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   643
currently running machine learners, including elapsed runtime and remaining
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   644
time until timeout.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   645
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   646
43216
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
   647
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
   648
specified in brackets after the \textbf{sledgehammer} command. The
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
   649
\qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50459
diff changeset
   650
\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional.
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50459
diff changeset
   651
For example:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   652
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   653
\prew
49919
54ec43352eb1 updated docs
blanchet
parents: 49365
diff changeset
   654
\textbf{sledgehammer} [\textit{isar\_proofs}, \,\textit{timeout} = 120]
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   655
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   656
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   657
Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   658
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   659
\prew
43216
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
   660
\textbf{sledgehammer\_params} \qty{options}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   661
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   662
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   663
The supported options are described in \S\ref{option-reference}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   664
43216
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
   665
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
   666
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
   667
\qty{facts} is a space-separated list of Isabelle facts (theorems, local
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   668
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
   669
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
   670
``(\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
   671
\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
   672
proceed as usual except that it should consider \qty{facts\/_{\mathrm{1}}}
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
   673
highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   674
53760
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53759
diff changeset
   675
If you use Isabelle/jEdit, Sledgehammer also provides an automatic mode that can
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53759
diff changeset
   676
be enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53759
diff changeset
   677
> Isabelle > General.'' For automatic runs, only the first prover set using
54114
84791e3fdcde updated S/H docs
blanchet
parents: 54015
diff changeset
   678
\textit{provers} (\S\ref{mode-of-operation}) is considered (typically E),
84791e3fdcde updated S/H docs
blanchet
parents: 54015
diff changeset
   679
\textit{slice} (\S\ref{mode-of-operation}) is disabled,
84791e3fdcde updated S/H docs
blanchet
parents: 54015
diff changeset
   680
\textit{minimize} (\S\ref{mode-of-operation}) is disabled, fewer facts are
84791e3fdcde updated S/H docs
blanchet
parents: 54015
diff changeset
   681
passed to the prover, \textit{fact\_filter} (\S\ref{relevance-filter}) is set to
84791e3fdcde updated S/H docs
blanchet
parents: 54015
diff changeset
   682
\textit{mepo}, \textit{strict} (\S\ref{problem-encoding}) is enabled,
84791e3fdcde updated S/H docs
blanchet
parents: 54015
diff changeset
   683
\textit{verbose} (\S\ref{output-format}) and \textit{debug}
84791e3fdcde updated S/H docs
blanchet
parents: 54015
diff changeset
   684
(\S\ref{output-format}) are disabled, \textit{preplay\_timeout}
84791e3fdcde updated S/H docs
blanchet
parents: 54015
diff changeset
   685
(\S\ref{timeouts}) is set to 0, and \textit{timeout} (\S\ref{timeouts}) is
84791e3fdcde updated S/H docs
blanchet
parents: 54015
diff changeset
   686
superseded by the ``Auto Time Limit'' option in jEdit. Sledgehammer's output is
84791e3fdcde updated S/H docs
blanchet
parents: 54015
diff changeset
   687
also more concise.
39320
5d578004be23 added Auto Sledgehammer docs
blanchet
parents: 39153
diff changeset
   688
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   689
\subsection{Metis}
57040
blanchet
parents: 57029
diff changeset
   690
\label{metis}
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   691
43216
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
   692
The \textit{metis} proof method has the syntax
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
   693
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
   694
\prew
45518
8ca7e3f25ee4 document metis options better
blanchet
parents: 45516
diff changeset
   695
\textbf{\textit{metis}}~(\qty{options})${}^?$~\qty{facts}${}^?$
43216
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
   696
\postw
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
   697
45518
8ca7e3f25ee4 document metis options better
blanchet
parents: 45516
diff changeset
   698
where \qty{facts} is a list of arbitrary facts and \qty{options} is a
8ca7e3f25ee4 document metis options better
blanchet
parents: 45516
diff changeset
   699
comma-separated list consisting of at most one $\lambda$ translation scheme
8ca7e3f25ee4 document metis options better
blanchet
parents: 45516
diff changeset
   700
specification with the same semantics as Sledgehammer's \textit{lam\_trans}
8ca7e3f25ee4 document metis options better
blanchet
parents: 45516
diff changeset
   701
option (\S\ref{problem-encoding}) and at most one type encoding specification
8ca7e3f25ee4 document metis options better
blanchet
parents: 45516
diff changeset
   702
with the same semantics as Sledgehammer's \textit{type\_enc} option
8ca7e3f25ee4 document metis options better
blanchet
parents: 45516
diff changeset
   703
(\S\ref{problem-encoding}).
8ca7e3f25ee4 document metis options better
blanchet
parents: 45516
diff changeset
   704
%
8ca7e3f25ee4 document metis options better
blanchet
parents: 45516
diff changeset
   705
The supported $\lambda$ translation schemes are \textit{hide\_lams},
46366
2ded91a6cbd5 docs and news
blanchet
parents: 46302
diff changeset
   706
\textit{lifting}, and \textit{combs} (the default).
45518
8ca7e3f25ee4 document metis options better
blanchet
parents: 45516
diff changeset
   707
%
8ca7e3f25ee4 document metis options better
blanchet
parents: 45516
diff changeset
   708
All the untyped type encodings listed in \S\ref{problem-encoding} are supported.
8ca7e3f25ee4 document metis options better
blanchet
parents: 45516
diff changeset
   709
For convenience, the following aliases are provided:
8ca7e3f25ee4 document metis options better
blanchet
parents: 45516
diff changeset
   710
\begin{enum}
48393
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   711
\item[\labelitemi] \textbf{\textit{full\_types}:} Alias for \textit{poly\_guards\_query}.
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   712
\item[\labelitemi] \textbf{\textit{partial\_types}:} Alias for \textit{poly\_args}.
db3db32c9195 MaSh docs
blanchet
parents: 48390
diff changeset
   713
\item[\labelitemi] \textbf{\textit{no\_types}:} Alias for \textit{erased}.
45518
8ca7e3f25ee4 document metis options better
blanchet
parents: 45516
diff changeset
   714
\end{enum}
43216
7b89836fd607 document metis better in Sledgehammer docs
blanchet
parents: 43204
diff changeset
   715
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   716
\section{Option Reference}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   717
\label{option-reference}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   718
43014
0dca147765f4 minor fixes to Sledgehammer docs
blanchet
parents: 43010
diff changeset
   719
\def\defl{\{}
0dca147765f4 minor fixes to Sledgehammer docs
blanchet
parents: 43010
diff changeset
   720
\def\defr{\}}
0dca147765f4 minor fixes to Sledgehammer docs
blanchet
parents: 43010
diff changeset
   721
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   722
\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
47036
fc958d7138be document "dont_preplay"
blanchet
parents: 46643
diff changeset
   723
\def\optrueonly#1{\flushitem{\textit{#1} $\bigl[$= \textit{true}$\bigr]$\enskip}\nopagebreak\\[\parskip]}
43014
0dca147765f4 minor fixes to Sledgehammer docs
blanchet
parents: 43010
diff changeset
   724
\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
   725
\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
   726
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46366
diff changeset
   727
\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   728
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
43014
0dca147765f4 minor fixes to Sledgehammer docs
blanchet
parents: 43010
diff changeset
   729
\def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]}
0dca147765f4 minor fixes to Sledgehammer docs
blanchet
parents: 43010
diff changeset
   730
\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
   731
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   732
\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
   733
\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
   734
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   735
Sledgehammer's options are categorized as follows:\ mode of operation
38984
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   736
(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),
ca7ac998bb36 update docs
blanchet
parents: 38983
diff changeset
   737
relevance filter (\S\ref{relevance-filter}), output format
57241
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   738
(\S\ref{output-format}), regression testing (\S\ref{regression-testing}),
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   739
and timeouts (\S\ref{timeouts}).
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   740
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   741
The descriptions below refer to the following syntactic quantities:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   742
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   743
\begin{enum}
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   744
\item[\labelitemi] \qtybf{string}: A string.
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   745
\item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}.
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   746
\item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or
40203
aff7d1471b62 "Nitpick" -> "Sledgehammer";
blanchet
parents: 40073
diff changeset
   747
\textit{smart}.
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   748
\item[\labelitemi] \qtybf{int\/}: An integer.
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54788
diff changeset
   749
\item[\labelitemi] \qtybf{float}: A floating-point number (e.g., 2.5 or 60)
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54788
diff changeset
   750
expressing a number of seconds.
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   751
\item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers
40343
4521d56aef63 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents: 40341
diff changeset
   752
(e.g., 0.6 0.95).
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   753
\item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   754
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   755
43217
37d507be3014 minor: curly brackets, not square brackets
blanchet
parents: 43216
diff changeset
   756
Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
47963
46c73ad5f7c0 doc updates
blanchet
parents: 47672
diff changeset
   757
have a negative counterpart (e.g., \textit{blocking} vs.\
46c73ad5f7c0 doc updates
blanchet
parents: 47672
diff changeset
   758
\textit{non\_blocking}). When setting Boolean options or their negative
46c73ad5f7c0 doc updates
blanchet
parents: 47672
diff changeset
   759
counterparts, ``= \textit{true\/}'' may be omitted.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   760
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   761
\subsection{Mode of Operation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   762
\label{mode-of-operation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   763
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   764
\begin{enum}
43014
0dca147765f4 minor fixes to Sledgehammer docs
blanchet
parents: 43010
diff changeset
   765
\opnodefaultbrk{provers}{string}
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   766
Specifies the automatic provers to use as a space-separated list (e.g.,
46299
14459b9671a1 more doc updates
blanchet
parents: 46298
diff changeset
   767
``\textit{e}~\textit{spass}~\textit{remote\_vampire\/}'').
14459b9671a1 more doc updates
blanchet
parents: 46298
diff changeset
   768
Provers can be run locally or remotely; see \S\ref{installation} for
14459b9671a1 more doc updates
blanchet
parents: 46298
diff changeset
   769
installation instructions.
14459b9671a1 more doc updates
blanchet
parents: 46298
diff changeset
   770
14459b9671a1 more doc updates
blanchet
parents: 46298
diff changeset
   771
The following local provers are supported:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   772
48701
3b414244acb1 documentation
blanchet
parents: 48652
diff changeset
   773
\begin{sloppy}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   774
\begin{enum}
55334
5f5104069b33 agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents: 55297
diff changeset
   775
\item[\labelitemi] \textbf{\textit{agsyhol}:} AgsyHOL is an automatic
52078
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   776
higher-order prover developed by Fredrik Lindblad \cite{agsyHOL},
55334
5f5104069b33 agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents: 55297
diff changeset
   777
with support for the TPTP typed higher-order syntax (THF0). To use AgsyHOL, set
52078
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   778
the environment variable \texttt{AGSYHOL\_HOME} to the directory that contains
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   779
the \texttt{agsyHOL} executable. Sledgehammer has been tested with version 1.0.
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   780
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46640
diff changeset
   781
\item[\labelitemi] \textbf{\textit{alt\_ergo}:} Alt-Ergo is a polymorphic
52078
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   782
ATP developed by Bobot et al.\ \cite{alt-ergo}.
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46640
diff changeset
   783
It supports the TPTP polymorphic typed first-order format (TFF1) via Why3
53102
45a7bfd99b45 doc tuning
blanchet
parents: 53091
diff changeset
   784
\cite{why3}. To use Alt-Ergo, set the environment variable \texttt{WHY3\_HOME}
56379
d8ecce5d51cd use Alt-Ergo 0.95.2, the latest and greatest version
blanchet
parents: 56378
diff changeset
   785
to the directory that contains the \texttt{why3} executable. Sledgehammer
d8ecce5d51cd use Alt-Ergo 0.95.2, the latest and greatest version
blanchet
parents: 56378
diff changeset
   786
requires Alt-Ergo 0.95.2 and Why3 0.83.
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46640
diff changeset
   787
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   788
\item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
42945
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   789
Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   790
set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   791
executable, including the file name, or install the prebuilt CVC3 package from
57241
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   792
\download. Sledgehammer has been tested with versions 2.2 and 2.4.1.
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   793
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   794
\item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 \cite{cvc4} is the successor to
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   795
CVC3. To use CVC4, set the environment variable \texttt{CVC4\_SOLVER} to the
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   796
complete path of the executable, including the file name, or install the
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   797
prebuilt CVC4 package from \download. Sledgehammer has been tested with version
7fca4159117f updated docs
blanchet
parents: 57237
diff changeset
   798
1.2.
42945
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   799
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   800
\item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
42964
bf45fd2488a2 document primitive support for LEO-II and Satallax
blanchet
parents: 42945
diff changeset
   801
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
   802
variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
52757
ea7cf7b14fdd updated Sledgehammer prover versions
blanchet
parents: 52078
diff changeset
   803
executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or
47056
6f8dfe6c1aea doc update
blanchet
parents: 47036
diff changeset
   804
install the prebuilt E package from \download. Sledgehammer has been tested with
57636
3ab503b04bdb stick to external proofs when invoking E, because they are more detailed and do not merge steps
blanchet
parents: 57566
diff changeset
   805
versions 1.6 to 1.8.
48652
15f0cf52deea document E-MaLeS
blanchet
parents: 48540
diff changeset
   806
15f0cf52deea document E-MaLeS
blanchet
parents: 48540
diff changeset
   807
\item[\labelitemi] \textbf{\textit{e\_males}:} E-MaLeS is a metaprover developed
15f0cf52deea document E-MaLeS
blanchet
parents: 48540
diff changeset
   808
by Daniel K\"uhlwein that implements strategy scheduling on top of E. To use
15f0cf52deea document E-MaLeS
blanchet
parents: 48540
diff changeset
   809
E-MaLeS, set the environment variable \texttt{E\_MALES\_HOME} to the directory
15f0cf52deea document E-MaLeS
blanchet
parents: 48540
diff changeset
   810
that contains the \texttt{emales.py} script. Sledgehammer has been tested with
15f0cf52deea document E-MaLeS
blanchet
parents: 48540
diff changeset
   811
version 1.1.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   812
54694
af9cdb4989c7 added warning to documentation, based on isabelle-users thread
blanchet
parents: 54139
diff changeset
   813
\item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is an experimental metaprover
af9cdb4989c7 added warning to documentation, based on isabelle-users thread
blanchet
parents: 54139
diff changeset
   814
developed by Josef Urban that implements strategy scheduling on top of E. To use
af9cdb4989c7 added warning to documentation, based on isabelle-users thread
blanchet
parents: 54139
diff changeset
   815
E-Par, set the environment variable \texttt{E\_HOME} to the directory that
af9cdb4989c7 added warning to documentation, based on isabelle-users thread
blanchet
parents: 54139
diff changeset
   816
contains the \texttt{runepar.pl} script and the \texttt{eprover} and
50929
7f0bc95af61c updated docs
blanchet
parents: 50720
diff changeset
   817
\texttt{epclextract} executables, or use the prebuilt E package from \download.
54694
af9cdb4989c7 added warning to documentation, based on isabelle-users thread
blanchet
parents: 54139
diff changeset
   818
Be aware that E-Par is experimental software. It has been known to generate
af9cdb4989c7 added warning to documentation, based on isabelle-users thread
blanchet
parents: 54139
diff changeset
   819
zombie processes. Use at your own risks.
50929
7f0bc95af61c updated docs
blanchet
parents: 50720
diff changeset
   820
48701
3b414244acb1 documentation
blanchet
parents: 48652
diff changeset
   821
\item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure
3b414244acb1 documentation
blanchet
parents: 48652
diff changeset
   822
instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}.
3b414244acb1 documentation
blanchet
parents: 48652
diff changeset
   823
To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the
48714
56b633faec99 documentation
blanchet
parents: 48701
diff changeset
   824
directory that contains the \texttt{iprover} and \texttt{vclausify\_rel}
56b633faec99 documentation
blanchet
parents: 48701
diff changeset
   825
executables. Sledgehammer has been tested with version 0.99.
48701
3b414244acb1 documentation
blanchet
parents: 48652
diff changeset
   826
3b414244acb1 documentation
blanchet
parents: 48652
diff changeset
   827
\item[\labelitemi] \textbf{\textit{iprover\_eq}:} iProver-Eq is an
3b414244acb1 documentation
blanchet
parents: 48652
diff changeset
   828
instantiation-based prover with native support for equality developed by
3b414244acb1 documentation
blanchet
parents: 48652
diff changeset
   829
Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. To use
3b414244acb1 documentation
blanchet
parents: 48652
diff changeset
   830
iProver-Eq, set the environment variable \texttt{IPROVER\_EQ\_HOME} to the
48714
56b633faec99 documentation
blanchet
parents: 48701
diff changeset
   831
directory that contains the \texttt{iprover-eq} and \texttt{vclausify\_rel}
56b633faec99 documentation
blanchet
parents: 48701
diff changeset
   832
executables. Sledgehammer has been tested with version 0.8.
48701
3b414244acb1 documentation
blanchet
parents: 48652
diff changeset
   833
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   834
\item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
44098
45078c8f5c1e document local HOATPs
blanchet
parents: 44091
diff changeset
   835
higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   836
with support for the TPTP typed higher-order syntax (THF0). To use LEO-II, set
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   837
the environment variable \texttt{LEO2\_HOME} to the directory that contains the
52757
ea7cf7b14fdd updated Sledgehammer prover versions
blanchet
parents: 52078
diff changeset
   838
\texttt{leo} executable. Sledgehammer requires version 1.3.4 or above.
44098
45078c8f5c1e document local HOATPs
blanchet
parents: 44091
diff changeset
   839
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   840
\item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
44098
45078c8f5c1e document local HOATPs
blanchet
parents: 44091
diff changeset
   841
higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
46242
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   842
support for the TPTP typed higher-order syntax (THF0). To use Satallax, set the
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   843
environment variable \texttt{SATALLAX\_HOME} to the directory that contains the
99a2a541c125 improve installation instructions
blanchet
parents: 45950
diff changeset
   844
\texttt{satallax} executable. Sledgehammer requires version 2.2 or above.
44098
45078c8f5c1e document local HOATPs
blanchet
parents: 44091
diff changeset
   845
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   846
\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
42964
bf45fd2488a2 document primitive support for LEO-II and Satallax
blanchet
parents: 42945
diff changeset
   847
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
   848
To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
47056
6f8dfe6c1aea doc update
blanchet
parents: 47036
diff changeset
   849
that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the
47577
b8f33b19e20b doc update
blanchet
parents: 47561
diff changeset
   850
version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from
48006
8d989b9c8e4f update docs
blanchet
parents: 47963
diff changeset
   851
\download. Sledgehammer requires version 3.8ds or above.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   852
48652
15f0cf52deea document E-MaLeS
blanchet
parents: 48540
diff changeset
   853
\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order
15f0cf52deea document E-MaLeS
blanchet
parents: 48540
diff changeset
   854
resolution prover developed by Andrei Voronkov and his colleagues
42964
bf45fd2488a2 document primitive support for LEO-II and Satallax
blanchet
parents: 42945
diff changeset
   855
\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
   856
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
48006
8d989b9c8e4f update docs
blanchet
parents: 47963
diff changeset
   857
executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g.,
56380
9bb2856cc845 don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
blanchet
parents: 56379
diff changeset
   858
``3.0''). Sledgehammer has been tested with versions 0.6 to 3.0.
52996
9a47c8256054 updated Vampire version numbers
blanchet
parents: 52757
diff changeset
   859
Versions strictly above 1.8 support the TPTP typed first-order format (TFF0).
40942
e08fa125c268 update documentation
blanchet
parents: 40689
diff changeset
   860
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   861
\item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   862
Microsoft Research \cite{z3}. To use Z3, set the environment variable
57211
cc59d49bdf64 updated docs w.r.t. Z3
blanchet
parents: 57107
diff changeset
   863
\texttt{Z3\_NEW\_SOLVER} to the complete path of the executable, including the file
57028
e5466055e94f added Isabelle system option 'mash'
blanchet
parents: 57019
diff changeset
   864
name, and set \texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a
56119
2e44053fee87 updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents: 55334
diff changeset
   865
noncommercial user---either in the environment in which Isabelle is
2e44053fee87 updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents: 55334
diff changeset
   866
launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or
57028
e5466055e94f added Isabelle system option 'mash'
blanchet
parents: 57019
diff changeset
   867
via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
56119
2e44053fee87 updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents: 55334
diff changeset
   868
> Isabelle > General'' in Isabelle/jEdit. Sledgehammer has been tested with
57211
cc59d49bdf64 updated docs w.r.t. Z3
blanchet
parents: 57107
diff changeset
   869
a pre-release version of 4.3.2.
56378
8fb4515818f7 updated Z3 TPTP to 4.3.1+
blanchet
parents: 56377
diff changeset
   870
8fb4515818f7 updated Z3 TPTP to 4.3.1+
blanchet
parents: 56377
diff changeset
   871
\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
8fb4515818f7 updated Z3 TPTP to 4.3.1+
blanchet
parents: 56377
diff changeset
   872
an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
8fb4515818f7 updated Z3 TPTP to 4.3.1+
blanchet
parents: 56377
diff changeset
   873
formats (FOF and TFF0). It is included for experimental purposes. It requires
56725
1ca7fd5f83bb updated Z3 version number
blanchet
parents: 56380
diff changeset
   874
version 4.3.1 of Z3 or above. To use it, set the environment variable
56378
8fb4515818f7 updated Z3 TPTP to 4.3.1+
blanchet
parents: 56377
diff changeset
   875
\texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp}
8fb4515818f7 updated Z3 TPTP to 4.3.1+
blanchet
parents: 56377
diff changeset
   876
executable.
57536
5e8317c5b689 improved docs
blanchet
parents: 57532
diff changeset
   877
\end{enum}
56378
8fb4515818f7 updated Z3 TPTP to 4.3.1+
blanchet
parents: 56377
diff changeset
   878
48701
3b414244acb1 documentation
blanchet
parents: 48652
diff changeset
   879
\end{sloppy}
42945
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   880
57536
5e8317c5b689 improved docs
blanchet
parents: 57532
diff changeset
   881
Moreover, the following remote provers are supported:
42945
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   882
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   883
\begin{enum}
52078
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   884
\item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of
55334
5f5104069b33 agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents: 55297
diff changeset
   885
AgsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
52078
d9c04fb297e1 updated Sledgehammer docs
blanchet
parents: 51205
diff changeset
   886
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   887
\item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   888
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   889
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   890
\item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover
47075
9f0b67fc07a8 doc update
blanchet
parents: 47056
diff changeset
   891
developed by Kry\v stof Hoder \cite{sine} based on E. It runs on Geoff
9f0b67fc07a8 doc update
blanchet
parents: 47056
diff changeset
   892
Sutcliffe's Miami servers.
44091
d40e5c72b346 updated Sledgehammer docs
blanchet
parents: 43990
diff changeset
   893
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   894
\item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
44091
d40e5c72b346 updated Sledgehammer docs
blanchet
parents: 43990
diff changeset
   895
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   896
servers. This ATP supports the TPTP typed first-order format (TFF0). The
44091
d40e5c72b346 updated Sledgehammer docs
blanchet
parents: 43990
diff changeset
   897
remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
d40e5c72b346 updated Sledgehammer docs
blanchet
parents: 43990
diff changeset
   898
48701
3b414244acb1 documentation
blanchet
parents: 48652
diff changeset
   899
\item[\labelitemi] \textbf{\textit{remote\_iprover}:} The
45339
4f6ae5423311 document new experimental provers
blanchet
parents: 45300
diff changeset
   900
remote version of iProver runs on Geoff Sutcliffe's Miami servers
4f6ae5423311 document new experimental provers
blanchet
parents: 45300
diff changeset
   901
\cite{sutcliffe-2000}.
4f6ae5423311 document new experimental provers
blanchet
parents: 45300
diff changeset
   902
48701
3b414244acb1 documentation
blanchet
parents: 48652
diff changeset
   903
\item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} The
45339
4f6ae5423311 document new experimental provers
blanchet
parents: 45300
diff changeset
   904
remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers
4f6ae5423311 document new experimental provers
blanchet
parents: 45300
diff changeset
   905
\cite{sutcliffe-2000}.
4f6ae5423311 document new experimental provers
blanchet
parents: 45300
diff changeset
   906
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   907
\item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
44098
45078c8f5c1e document local HOATPs
blanchet
parents: 44091
diff changeset
   908
runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
42964
bf45fd2488a2 document primitive support for LEO-II and Satallax
blanchet
parents: 42945
diff changeset
   909
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   910
\item[\labelitemi] \textbf{\textit{remote\_satallax}:} The remote version of
44098
45078c8f5c1e document local HOATPs
blanchet
parents: 44091
diff changeset
   911
Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
42964
bf45fd2488a2 document primitive support for LEO-II and Satallax
blanchet
parents: 42945
diff changeset
   912
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   913
\item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a first-order
43625
c3e28c869499 document "simple_higher" type encoding
blanchet
parents: 43574
diff changeset
   914
resolution prover developed by Stickel et al.\ \cite{snark}. It supports the
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   915
TPTP typed first-order format (TFF0). The remote version of SNARK runs on
43625
c3e28c869499 document "simple_higher" type encoding
blanchet
parents: 43574
diff changeset
   916
Geoff Sutcliffe's Miami servers.
40073
f167beebb527 added SMT solver to Sledgehammer docs
blanchet
parents: 40060
diff changeset
   917
54788
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54694
diff changeset
   918
\item[\labelitemi] \textbf{\textit{remote\_spass\_pirate}:} SPASS-Pirate is a
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54694
diff changeset
   919
highly experimental first-order resolution prover developed by Daniel Wand.
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54694
diff changeset
   920
The remote version of SPASS-Pirate run on a private server set up by Daniel
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54694
diff changeset
   921
Wand.
a898e15b522a primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents: 54694
diff changeset
   922
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   923
\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
48006
8d989b9c8e4f update docs
blanchet
parents: 47963
diff changeset
   924
Vampire runs on Geoff Sutcliffe's Miami servers.
42945
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   925
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
   926
\item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
42945
cb28abfde010 slightly improved documentation
blanchet
parents: 42940
diff changeset
   927
equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be
43625
c3e28c869499 document "simple_higher" type encoding
blanchet
parents: 43574
diff changeset
   928
used to prove universally quantified equations using unconditional equations,
c3e28c869499 document "simple_higher" type encoding
blanchet
parents: 43574
diff changeset
   929
corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister
c3e28c869499 document "simple_higher" type encoding
blanchet
parents: 43574
diff changeset
   930
runs on Geoff Sutcliffe's Miami servers.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   931
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   932
48405
7682bc885e8a use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents: 48393
diff changeset
   933
By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,
57237
bc51864c2ac4 took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
blanchet
parents: 57211
diff changeset
   934
and Z3 in parallel---either locally or remotely, depending on the number of
bc51864c2ac4 took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
blanchet
parents: 57211
diff changeset
   935
processor cores available.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   936
44743
804dfa6d35b6 updated Sledgehammer's docs
blanchet
parents: 44494
diff changeset
   937
It is generally a good idea to run several provers in parallel. Running E,
804dfa6d35b6 updated Sledgehammer's docs
blanchet
parents: 44494
diff changeset
   938
SPASS, and Vampire for 5~seconds yields a similar success rate to running the
804dfa6d35b6 updated Sledgehammer's docs
blanchet
parents: 44494
diff changeset
   939
most effective of these for 120~seconds \cite{boehme-nipkow-2010}.
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   940
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   941
\opnodefault{prover}{string}
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   942
Alias for \textit{provers}.
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39335
diff changeset
   943
38983
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   944
\opfalse{blocking}{non\_blocking}
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   945
Specifies whether the \textbf{sledgehammer} command should operate
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   946
synchronously. The asynchronous (non-blocking) mode lets the user start proving
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   947
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
   948
also be more confusing. Irrespective of the value of this option, Sledgehammer
53760
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53759
diff changeset
   949
is always run synchronously if \textit{debug} (\S\ref{output-format}) is
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53759
diff changeset
   950
enabled.
38983
5261cf6b57ca update docs
blanchet
parents: 38940
diff changeset
   951
45708
7c8bed80301f updated Sledgehammer docs with new/renamed options
blanchet
parents: 45555
diff changeset
   952
\optrue{slice}{dont\_slice}
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   953
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
   954
segments, each of which has its own set of possibly prover-dependent options.
42446
d105b1309a8d rewording
blanchet
parents: 42443
diff changeset
   955
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
   956
set-of-support (SOS) strategy, whereas the second slice runs without it. For E,
42446
d105b1309a8d rewording
blanchet
parents: 42443
diff changeset
   957
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
   958
number of facts. For SMT solvers, several slices are tried with the same options
42446
d105b1309a8d rewording
blanchet
parents: 42443
diff changeset
   959
each time but fewer and fewer facts. According to benchmarks with a timeout of
d105b1309a8d rewording
blanchet
parents: 42443
diff changeset
   960
30 seconds, slicing is a valuable optimization, and you should probably leave it
54114
84791e3fdcde updated S/H docs
blanchet
parents: 54015
diff changeset
   961
enabled unless you are conducting experiments.
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   962
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   963
\nopagebreak
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42442
diff changeset
   964
{\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
   965
57722
2c2d5b7f29aa updated docs
blanchet
parents: 57719
diff changeset
   966
\optrue{minimize}{dont\_minimize}
45708
7c8bed80301f updated Sledgehammer docs with new/renamed options
blanchet
parents: 45555
diff changeset
   967
Specifies whether the minimization tool should be invoked automatically after
57722
2c2d5b7f29aa updated docs
blanchet
parents: 57719
diff changeset
   968
proof search.
45708
7c8bed80301f updated Sledgehammer docs with new/renamed options
blanchet
parents: 45555
diff changeset
   969
7c8bed80301f updated Sledgehammer docs with new/renamed options
blanchet
parents: 45555
diff changeset
   970
\nopagebreak
47036
fc958d7138be document "dont_preplay"
blanchet
parents: 46643
diff changeset
   971
{\small See also \textit{preplay\_timeout} (\S\ref{timeouts})
fc958d7138be document "dont_preplay"
blanchet
parents: 46643
diff changeset
   972
and \textit{dont\_preplay} (\S\ref{timeouts}).}
45708
7c8bed80301f updated Sledgehammer docs with new/renamed options
blanchet
parents: 45555
diff changeset
   973
53801
342e371395c6 document "spy" option
blanchet
parents: 53782
diff changeset
   974
\opfalse{spy}{dont\_spy}
342e371395c6 document "spy" option
blanchet
parents: 53782
diff changeset
   975
Specifies whether Sledgehammer should record statistics in
342e371395c6 document "spy" option
blanchet
parents: 53782
diff changeset
   976
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak spy\_\allowbreak sledgehammer}.
342e371395c6 document "spy" option
blanchet
parents: 53782
diff changeset
   977
These statistics can be useful to the developers of Sledgehammer. If you are willing to have your
342e371395c6 document "spy" option
blanchet
parents: 53782
diff changeset
   978
interactions recorded in the name of science, please enable this feature and send the statistics
342e371395c6 document "spy" option
blanchet
parents: 53782
diff changeset
   979
file every now and then to the author of this manual (\authoremail).
342e371395c6 document "spy" option
blanchet
parents: 53782
diff changeset
   980
To change the default value of this option globally, set the environment variable
57107
2d502370ee99 changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)
blanchet
parents: 57095
diff changeset
   981
\texttt{SLEDGEHAMMER\_SPY} to \textit{yes}.
53801
342e371395c6 document "spy" option
blanchet
parents: 53782
diff changeset
   982
342e371395c6 document "spy" option
blanchet
parents: 53782
diff changeset
   983
\nopagebreak
342e371395c6 document "spy" option
blanchet
parents: 53782
diff changeset
   984
{\small See also \textit{debug} (\S\ref{output-format}).}
342e371395c6 document "spy" option
blanchet
parents: 53782
diff changeset
   985
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   986
\opfalse{overlord}{no\_overlord}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   987
Specifies whether Sledgehammer should put its temporary files in
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   988
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   989
debugging Sledgehammer but also unsafe if several instances of the tool are run
48390
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48388
diff changeset
   990
simultaneously. The files are identified by the prefixes \texttt{prob\_} and
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48388
diff changeset
   991
\texttt{mash\_}; you may safely remove them after Sledgehammer has run.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   992
54139
c8ea98c1f4b2 added thread-safety warnings
blanchet
parents: 54114
diff changeset
   993
\textbf{Warning:} This option is not thread-safe. Use at your own risks.
c8ea98c1f4b2 added thread-safety warnings
blanchet
parents: 54114
diff changeset
   994
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   995
\nopagebreak
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   996
{\small See also \textit{debug} (\S\ref{output-format}).}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   997
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   998
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
   999
\subsection{Relevance Filter}
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1000
\label{relevance-filter}
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1001
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1002
\begin{enum}
48388
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1003
\opdefault{fact\_filter}{string}{smart}
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1004
Specifies the relevance filter to use. The following filters are available:
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1005
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1006
\begin{enum}
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1007
\item[\labelitemi] \textbf{\textit{mepo}:}
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1008
The traditional memoryless MePo relevance filter.
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1009
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1010
\item[\labelitemi] \textbf{\textit{mash}:}
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57463
diff changeset
  1011
The MaSh machine learner. Three learning algorithms are provided:
57019
f013e3a830c3 updated docs
blanchet
parents: 56725
diff changeset
  1012
f013e3a830c3 updated docs
blanchet
parents: 56725
diff changeset
  1013
\begin{enum}
57463
d6df9b63d385 updated docs
blanchet
parents: 57431
diff changeset
  1014
\item[\labelitemi] \textbf{\textit{nb}} is an implementation of naive Bayes.
57019
f013e3a830c3 updated docs
blanchet
parents: 56725
diff changeset
  1015
57463
d6df9b63d385 updated docs
blanchet
parents: 57431
diff changeset
  1016
\item[\labelitemi] \textbf{\textit{knn}} is an implementation of $k$-nearest
d6df9b63d385 updated docs
blanchet
parents: 57431
diff changeset
  1017
neighbors.
d6df9b63d385 updated docs
blanchet
parents: 57431
diff changeset
  1018
57659
b246943b3aa3 reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents: 57636
diff changeset
  1019
\item[\labelitemi] \textbf{\textit{nb\_knn}} (also called \textbf{\textit{yes}}
b246943b3aa3 reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents: 57636
diff changeset
  1020
and \textbf{\textit{sml}}) is a combination of naive Bayes and $k$-nearest
b246943b3aa3 reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents: 57636
diff changeset
  1021
neighbors.
57019
f013e3a830c3 updated docs
blanchet
parents: 56725
diff changeset
  1022
\end{enum}
f013e3a830c3 updated docs
blanchet
parents: 56725
diff changeset
  1023
57272
fd539459a112 enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
blanchet
parents: 57245
diff changeset
  1024
In addition, the special value \textit{none} is used to disable machine learning by
fd539459a112 enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
blanchet
parents: 57245
diff changeset
  1025
default (cf.\ \textit{smart} below).
fd539459a112 enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
blanchet
parents: 57245
diff changeset
  1026
57659
b246943b3aa3 reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents: 57636
diff changeset
  1027
The default algorithm is \textit{nb\_knn}. The algorithm can be selected by
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57463
diff changeset
  1028
setting \texttt{MASH}---either in the environment in which Isabelle is launched,
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57463
diff changeset
  1029
in your
57463
d6df9b63d385 updated docs
blanchet
parents: 57431
diff changeset
  1030
\texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak etc/\allowbreak settings}
d6df9b63d385 updated docs
blanchet
parents: 57431
diff changeset
  1031
file, or via the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle >
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57463
diff changeset
  1032
General'' in Isabelle/jEdit. Persistent data for both algorithms is stored in
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57463
diff changeset
  1033
the directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57463
diff changeset
  1034
mash}.
48388
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1035
51024
98fb341d32e3 distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
blanchet
parents: 50929
diff changeset
  1036
\item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
98fb341d32e3 distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
blanchet
parents: 50929
diff changeset
  1037
rankings from MePo and MaSh.
48388
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1038
57659
b246943b3aa3 reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents: 57636
diff changeset
  1039
\item[\labelitemi] \textbf{\textit{smart}:} A combination of MePo, MaSh, and
b246943b3aa3 reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents: 57636
diff changeset
  1040
MeSh. If the learning algorithm is set to be \textit{none}, \textit{smart}
b246943b3aa3 reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents: 57636
diff changeset
  1041
behaves like MePo.
48388
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1042
\end{enum}
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1043
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1044
\opdefault{max\_facts}{smart\_int}{smart}
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1045
Specifies the maximum number of facts that may be returned by the relevance
55297
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55290
diff changeset
  1046
filter. If the option is set to \textit{smart} (the default), it effectively
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55290
diff changeset
  1047
takes a value that was empirically found to be appropriate for the prover.
57107
2d502370ee99 changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)
blanchet
parents: 57095
diff changeset
  1048
Typical values lie between 50 and 1000.
53757
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53518
diff changeset
  1049
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1050
\opdefault{fact\_thresholds}{float\_pair}{\upshape 0.45~0.85}
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1051
Specifies the thresholds above which facts are considered relevant by the
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1052
relevance filter. The first threshold is used for the first iteration of the
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1053
relevance filter and the second threshold is used for the last iteration (if it
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1054
is reached). The effective threshold is quadratically interpolated for the other
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1055
iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1056
are relevant and 1 only theorems that refer to previously seen constants.
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1057
48388
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1058
\optrue{learn}{dont\_learn}
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1059
Specifies whether MaSh should be run automatically by Sledgehammer to learn the
53760
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53759
diff changeset
  1060
available theories (and hence provide more accurate results). Learning takes
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53759
diff changeset
  1061
place only if MaSh is enabled.
48388
fd7958ebee96 more MaSh docs
blanchet
parents: 48387
diff changeset
  1062
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1063
\opdefault{max\_new\_mono\_instances}{int}{smart}
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1064
Specifies the maximum number of monomorphic instances to generate beyond
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1065
\textit{max\_facts}. The higher this limit is, the more monomorphic instances
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1066
are potentially generated. Whether monomorphization takes place depends on the
55297
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55290
diff changeset
  1067
type encoding used. If the option is set to \textit{smart} (the default), it
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55290
diff changeset
  1068
takes a value that was empirically found to be appropriate for the prover. For
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55290
diff changeset
  1069
most provers, this value is 100.
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1070
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1071
\nopagebreak
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1072
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1073
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1074
\opdefault{max\_mono\_iters}{int}{smart}
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1075
Specifies the maximum number of iterations for the monomorphization fixpoint
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1076
construction. The higher this limit is, the more monomorphic instances are
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1077
potentially generated. Whether monomorphization takes place depends on the
55297
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55290
diff changeset
  1078
type encoding used. If the option is set to \textit{smart} (the default), it
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55290
diff changeset
  1079
takes a value that was empirically found to be appropriate for the prover.
1dfcd49f5dcb renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents: 55290
diff changeset
  1080
For most provers, this value is 3.
48387
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1081
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1082
\nopagebreak
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1083
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1084
\end{enum}
302cf211fb3f mention MaSh in docs
blanchet
parents: 48294
diff changeset
  1085
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
  1086
\subsection{Problem Encoding}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
  1087
\label{problem-encoding}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
  1088
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1089
\newcommand\comb[1]{\const{#1}}
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1090
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
  1091
\begin{enum}
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1092
\opdefault{lam\_trans}{string}{smart}
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1093
Specifies the $\lambda$ translation scheme to use in ATP problems. The supported
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1094
translation schemes are listed below:
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1095
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1096
\begin{enum}
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1097
\item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$-abstractions
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1098
by replacing them by unspecified fresh constants, effectively disabling all
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1099
reasoning under $\lambda$-abstractions.
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1100
46366
2ded91a6cbd5 docs and news
blanchet
parents: 46302
diff changeset
  1101
\item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1102
supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions,
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1103
defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting).
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1104
46366
2ded91a6cbd5 docs and news
blanchet
parents: 46302
diff changeset
  1105
\item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1106
combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1107
enable the ATPs to synthesize $\lambda$-terms but tend to yield bulkier formulas
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1108
than $\lambda$-lifting: The translation is quadratic in the worst case, and the
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1109
equational definitions of the combinators are very prolific in the context of
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1110
resolution.
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1111
46366
2ded91a6cbd5 docs and news
blanchet
parents: 46302
diff changeset
  1112
\item[\labelitemi] \textbf{\textit{combs\_and\_lifting}:} Introduce a new
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1113
supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1114
lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators.
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1115
46366
2ded91a6cbd5 docs and news
blanchet
parents: 46302
diff changeset
  1116
\item[\labelitemi] \textbf{\textit{combs\_or\_lifting}:} For each cluster of
2ded91a6cbd5 docs and news
blanchet
parents: 46302
diff changeset
  1117
$\lambda$-abstractions, heuristically choose between $\lambda$-lifting and Curry
2ded91a6cbd5 docs and news
blanchet
parents: 46302
diff changeset
  1118
combinators.
2ded91a6cbd5 docs and news
blanchet
parents: 46302
diff changeset
  1119
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1120
\item[\labelitemi] \textbf{\textit{keep\_lams}:}
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1121
Keep the $\lambda$-abstractions in the generated problems. This is available
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1122
only with provers that support the THF0 syntax.
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1123
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1124
\item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1125
depends on the ATP and should be the most efficient scheme for that ATP.
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1126
\end{enum}
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1127
46366
2ded91a6cbd5 docs and news
blanchet
parents: 46302
diff changeset
  1128
For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting},
2ded91a6cbd5 docs and news
blanchet
parents: 46302
diff changeset
  1129
irrespective of the value of this option.
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1130
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46366
diff changeset
  1131
\opsmartx{uncurried\_aliases}{no\_uncurried\_aliases}
46411
cafa325419f6 fixed docs
blanchet
parents: 46409
diff changeset
  1132
Specifies whether fresh function symbols should be generated as aliases for
cafa325419f6 fixed docs
blanchet
parents: 46409
diff changeset
  1133
applications of curried functions in ATP problems.
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46366
diff changeset
  1134
43627
ecd4bb7a8bc0 update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
blanchet
parents: 43625
diff changeset
  1135
\opdefault{type\_enc}{string}{smart}
ecd4bb7a8bc0 update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
blanchet
parents: 43625
diff changeset
  1136
Specifies the type encoding to use in ATP problems. Some of the type encodings
ecd4bb7a8bc0 update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
blanchet
parents: 43625
diff changeset
  1137
are unsound, meaning that they can give rise to spurious proofs
48093
ebc75afed39a updated docs
blanchet
parents: 48090
diff changeset
  1138
(unreconstructible using \textit{metis}). The type encodings are
46300
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
  1139
listed below, with an indication of their soundness in parentheses.
48093
ebc75afed39a updated docs
blanchet
parents: 48090
diff changeset
  1140
An asterisk (*) indicates that the encoding is slightly incomplete for
56120
04c37dfef684 updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents: 56119
diff changeset
  1141
reconstruction with \textit{metis}, unless the \textit{strict} option (described
46302
adf10579fe43 minor edits in docs
blanchet
parents: 46300
diff changeset
  1142
below) is enabled.
42228
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
  1143
3bf2eea43dac document "type_sys" option
blanchet
parents: 42180
diff changeset
  1144
\begin{enum}
48090
433787f8145e updated docs
blanchet
parents: 48078
diff changeset
  1145
\item[\labelitemi] \textbf{\textit{erased} (unsound):} No type information is
46300
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
  1146
supplied to the ATP, not even to resolve overloading. Types are simply erased.
42582
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
  1147
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1148
\item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using
46300
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
  1149
a predicate \const{g}$(\tau, t)$ that guards bound
48090
433787f8145e updated docs
blanchet
parents: 48078
diff changeset
  1150
variables. Constants are annotated with their types, supplied as extra
42887
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
  1151
arguments, to resolve overloading.
42685
7a5116bd63b7 documentation tuning
blanchet
parents: 42683
diff changeset
  1152
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1153
\item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
46300
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
  1154
tagged with its type using a function $\const{t\/}(\tau, t)$.
42887
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
  1155
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1156
\item[\labelitemi] \textbf{\textit{poly\_args} (unsound):}
43990
3928b3448f38 updated Sledgehammer documentation
blanchet
parents: 43822
diff changeset
  1157
Like for \textit{poly\_guards} constants are annotated with their types to
43002
e88fde86e4c2 mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents: 42996
diff changeset
  1158
resolve overloading, but otherwise no type information is encoded. This
57040
blanchet
parents: 57029
diff changeset
  1159
is the default encoding used by the \textit{metis} proof method.
42685
7a5116bd63b7 documentation tuning
blanchet
parents: 42683
diff changeset
  1160
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1161
\item[\labelitemi]
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
  1162
\textbf{%
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44423
diff changeset
  1163
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44423
diff changeset
  1164
\textit{raw\_mono\_args} (unsound):} \\
43990
3928b3448f38 updated Sledgehammer documentation
blanchet
parents: 43822
diff changeset
  1165
Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args},
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
  1166
respectively, but the problem is additionally monomorphized, meaning that type
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
  1167
variables are instantiated with heuristically chosen ground types.
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
  1168
Monomorphization can simplify reasoning but also leads to larger fact bases,
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
  1169
which can slow down the ATPs.
42582
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
  1170
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1171
\item[\labelitemi]
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
  1172
\textbf{%
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44423
diff changeset
  1173
\textit{mono\_guards}, \textit{mono\_tags} (sound);
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44423
diff changeset
  1174
\textit{mono\_args} (unsound):} \\
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42685
diff changeset
  1175
Similar to
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44423
diff changeset
  1176
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44423
diff changeset
  1177
\textit{raw\_mono\_args}, respectively but types are mangled in constant names
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44423
diff changeset
  1178
instead of being supplied as ground term arguments. The binary predicate
46300
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
  1179
$\const{g}(\tau, t)$ becomes a unary predicate
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
  1180
$\const{g\_}\tau(t)$, and the binary function
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
  1181
$\const{t}(\tau, t)$ becomes a unary function
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
  1182
$\const{t\_}\tau(t)$.
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
  1183
46435
e9c90516bc0d renamed type encoding
blanchet
parents: 46411
diff changeset
  1184
\item[\labelitemi] \textbf{\textit{mono\_native} (sound):} Exploits native
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46640
diff changeset
  1185
first-order types if the prover supports the TFF0, TFF1, or THF0 syntax;
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46640
diff changeset
  1186
otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized.
43625
c3e28c869499 document "simple_higher" type encoding
blanchet
parents: 43574
diff changeset
  1187
46435
e9c90516bc0d renamed type encoding
blanchet
parents: 46411
diff changeset
  1188
\item[\labelitemi] \textbf{\textit{mono\_native\_higher} (sound):} Exploits
e9c90516bc0d renamed type encoding
blanchet
parents: 46411
diff changeset
  1189
native higher-order types if the prover supports the THF0 syntax; otherwise,
e9c90516bc0d renamed type encoding
blanchet
parents: 46411
diff changeset
  1190
falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is
e9c90516bc0d renamed type encoding
blanchet
parents: 46411
diff changeset
  1191
monomorphized.
42681
281cc069282c document monotonic type systems
blanchet
parents: 42591
diff changeset
  1192
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46640
diff changeset
  1193
\item[\labelitemi] \textbf{\textit{poly\_native} (sound):} Exploits native
48078
72b093caf048 swap adjectives (cf. Google)
blanchet
parents: 48006
diff changeset
  1194
first-order polymorphic types if the prover supports the TFF1 syntax; otherwise,
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46640
diff changeset
  1195
falls back on \textit{mono\_native}.
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46640
diff changeset
  1196
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1197
\item[\labelitemi]
42681
281cc069282c document monotonic type systems
blanchet
parents: 42591
diff changeset
  1198
\textbf{%
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44423
diff changeset
  1199
\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44423
diff changeset
  1200
\textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
46435
e9c90516bc0d renamed type encoding
blanchet
parents: 46411
diff changeset
  1201
\textit{mono\_native}? (sound*):} \\
43990
3928b3448f38 updated Sledgehammer documentation
blanchet
parents: 43822
diff changeset
  1202
The type encodings \textit{poly\_guards}, \textit{poly\_tags},
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44423
diff changeset
  1203
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
47036
fc958d7138be document "dont_preplay"
blanchet
parents: 46643
diff changeset
  1204
\textit{mono\_tags}, and \textit{mono\_native} are fully typed and sound. For
fc958d7138be document "dont_preplay"
blanchet
parents: 46643
diff changeset
  1205
each of these, Sledgehammer also provides a lighter variant identified by a
fc958d7138be document "dont_preplay"
blanchet
parents: 46643
diff changeset
  1206
question mark (`\hbox{?}')\ that detects and erases monotonic types, notably
fc958d7138be document "dont_preplay"
blanchet
parents: 46643
diff changeset
  1207
infinite types. (For \textit{mono\_native}, the types are not actually erased
fc958d7138be document "dont_preplay"
blanchet
parents: 46643
diff changeset
  1208
but rather replaced by a shared uniform type of individuals.) As argument to the
fc958d7138be document "dont_preplay"
blanchet
parents: 46643
diff changeset
  1209
\textit{metis} proof method, the question mark is replaced by a
fc958d7138be document "dont_preplay"
blanchet
parents: 46643
diff changeset
  1210
\hbox{``\textit{\_query\/}''} suffix.
42582
6321d0dc3d72 document new type system syntax
blanchet
parents: 42535
diff changeset
  1211
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45380
diff changeset
  1212
\item[\labelitemi]
42887
771be1dcfef6 document new type system and soundness properties of the different systems
blanchet
parents: 42884
diff changeset
  1213
\textbf{%
44769
15102294a166 updated Sledgehammer documentation
blanchet
parents: 44743
diff changeset
  1214
\textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\
15102294a166 updated Sledgehammer documentation
blanchet
parents: 44743
diff changeset
  1215
\textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\
46300
6ded25a6098a updated Sledge docs some more
blanchet
parents: 46299
diff changeset
  1216
(sound*):} \\
44816
efa1f532508b update Sledgehammer docs
blanchet
parents: 44769
diff changeset
  1217
Even lighter versions of the `\hbox{?}' encodings. As argument to the
efa1f532508b update Sledgehammer docs
blanchet
parents: 44769
diff changeset
  1218
\textit{metis} proof method, the `\hbox{??}' suffix is replaced by
46242
99a2a541c125 improve installation instructions
blanchet