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