doc-src/Sledgehammer/sledgehammer.tex
author blanchet
Wed, 28 Jul 2010 18:45:18 +0200
changeset 38043 f31ddd5da4e3
parent 37582 f329e1b99ce6
child 38063 458c4578761f
permissions -rw-r--r--
updated Sledgehammer docs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     1
\documentclass[a4paper,12pt]{article}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     2
\usepackage[T1]{fontenc}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     3
\usepackage{amsmath}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     4
\usepackage{amssymb}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     5
\usepackage[english,french]{babel}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     6
\usepackage{color}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     7
\usepackage{footmisc}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     8
\usepackage{graphicx}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
     9
%\usepackage{mathpazo}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    10
\usepackage{multicol}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    11
\usepackage{stmaryrd}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    12
%\usepackage[scaled=.85]{beramono}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    13
\usepackage{../iman,../pdfsetup}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    14
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    15
%\oddsidemargin=4.6mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    16
%\evensidemargin=4.6mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    17
%\textwidth=150mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    18
%\topmargin=4.6mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    19
%\headheight=0mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    20
%\headsep=0mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    21
%\textheight=234mm
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    22
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    23
\def\Colon{\mathord{:\mkern-1.5mu:}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    24
%\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    25
%\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    26
\def\lparr{\mathopen{(\mkern-4mu\mid}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    27
\def\rparr{\mathclose{\mid\mkern-4mu)}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    28
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    29
\def\unk{{?}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    30
\def\undef{(\lambda x.\; \unk)}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    31
%\def\unr{\textit{others}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    32
\def\unr{\ldots}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    33
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    34
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    35
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    36
\urlstyle{tt}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    37
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    38
\begin{document}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    39
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    40
\selectlanguage{english}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    41
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    42
\title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    43
Hammering Away \\[\smallskipamount]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    44
\Large A User's Guide to Sledgehammer for Isabelle/HOL}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    45
\author{\hbox{} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    46
Jasmin Christian Blanchette \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    47
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    48
\hbox{}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    49
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    50
\maketitle
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    51
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    52
\tableofcontents
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    53
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    54
\setlength{\parskip}{.7em plus .2em minus .1em}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    55
\setlength{\parindent}{0pt}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    56
\setlength{\abovedisplayskip}{\parskip}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    57
\setlength{\abovedisplayshortskip}{.9\parskip}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    58
\setlength{\belowdisplayskip}{\parskip}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    59
\setlength{\belowdisplayshortskip}{.9\parskip}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    60
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    61
% General-purpose enum environment with correct spacing
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    62
\newenvironment{enum}%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    63
    {\begin{list}{}{%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    64
        \setlength{\topsep}{.1\parskip}%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    65
        \setlength{\partopsep}{.1\parskip}%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    66
        \setlength{\itemsep}{\parskip}%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    67
        \advance\itemsep by-\parsep}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    68
    {\end{list}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    69
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    70
\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    71
\advance\rightskip by\leftmargin}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    72
\def\post{\vskip0pt plus1ex\endgroup}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    73
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    74
\def\prew{\pre\advance\rightskip by-\leftmargin}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    75
\def\postw{\post}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    76
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    77
\section{Introduction}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    78
\label{introduction}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    79
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    80
Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs)
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    81
on the current goal. The supported ATPs are E \cite{schulz-2002}, SPASS
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    82
\cite{weidenbach-et-al-2009}, and Vampire \cite{riazanov-voronkov-2002}, which
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    83
can be run locally or remotely via the SystemOnTPTP web service
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    84
\cite{sutcliffe-2000}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    85
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    86
The problem passed to ATPs consists of your current goal together with a
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    87
heuristic selection of hundreds of facts (theorems) from the current theory
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    88
context, filtered by relevance. Because jobs are run in the background, you can
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    89
continue to work on your proof by other means. Provers can be run in parallel.
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    90
Any reply (which may arrive minutes later) will appear in the Proof General
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    91
response buffer.
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    92
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    93
The result of a successful ATP proof search is some source text that usually
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    94
(but not always) reconstructs the proof within Isabelle, without requiring the
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    95
ATPs again. The reconstructed proof relies on the general-purpose Metis prover
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    96
\cite{metis}, which is fully integrated into Isabelle/HOL, with explicit
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    97
inferences going through the kernel. Thus its results are correct by
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
    98
construction.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
    99
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   100
\newbox\boxA
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   101
\setbox\boxA=\hbox{\texttt{nospam}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   102
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   103
Examples of Sledgehammer use can be found in Isabelle's
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   104
\texttt{src/HOL/Metis\_Examples} directory.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   105
Comments and bug reports concerning Sledgehammer or this manual should be
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   106
directed to
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   107
\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   108
in.\allowbreak tum.\allowbreak de}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   109
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   110
\vskip2.5\smallskipamount
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   111
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   112
%\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   113
%suggesting several textual improvements.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   114
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   115
\section{Installation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   116
\label{installation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   117
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   118
Sledgehammer is part of Isabelle, so you don't need to install it. However, it
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   119
relies on third-party automatic theorem provers (ATPs). Currently, E, SPASS, and
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   120
Vampire are supported. All of these are available remotely via SystemOnTPTP
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   121
\cite{sutcliffe-2000}, but if you want better performance you will need to
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   122
install at least E and SPASS locally.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   123
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   124
There are three main ways to install ATPs on your machine:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   125
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   126
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   127
\item[$\bullet$] If you installed an official Isabelle package with everything
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   128
inside, it should already include properly setup executables for E and SPASS,
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   129
ready to use.%
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   130
\footnote{Vampire's license prevents us from doing the same for this otherwise
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   131
wonderful tool.}
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   132
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   133
\item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   134
binary packages from Isabelle's download page. Extract the archives, then add a
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   135
line to your \texttt{\char`\~/.isabelle/etc/components} file with the absolute path to
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   136
E or SPASS. For example, if the \texttt{components} does not exist
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   137
yet and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   138
the \texttt{components} file with the single line
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   139
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   140
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   141
\texttt{/usr/local/spass-3.7}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   142
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   143
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   144
in it.
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   145
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   146
\item[$\bullet$] If you prefer to build E or SPASS yourself, or obtained a
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   147
Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}),
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   148
set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   149
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   150
\texttt{SPASS}, or \texttt{vampire} executable.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   151
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   152
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   153
To check whether E and SPASS are installed, follow the example in
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   154
\S\ref{first-steps}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   155
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   156
Remote ATP invocation via the SystemOnTPTP web service requires Perl with the
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   157
World Wide Web Library (\texttt{libwww-perl}) installed.
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   158
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   159
\section{First Steps}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   160
\label{first-steps}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   161
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   162
To illustrate Sledgehammer in context, let us start a theory file and
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   163
attempt to prove a simple lemma:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   164
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   165
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   166
\textbf{theory}~\textit{Scratch} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   167
\textbf{imports}~\textit{Main} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   168
\textbf{begin} \\[2\smallskipamount]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   169
%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   170
\textbf{lemma} ``$[a] = [b] \,\longleftrightarrow\, a = b$'' \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   171
\textbf{sledgehammer}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   172
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   173
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   174
Instead of issuing the \textbf{sledgehammer} command, you can also find
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   175
Sledgehammer in the ``Commands'' submenu of the ``Isabelle'' menu in Proof
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   176
General or press the Emacs key sequence C-c C-a C-s.
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   177
Either way, Sledgehammer produces the following output after a few seconds:
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   178
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   179
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   180
\slshape
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   181
Sledgehammer: ATP ``\textit{e}'' for subgoal 1: \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   182
$([a] = [b]) = (a = b)$ \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   183
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   184
To minimize the number of lemmas, try this: \\
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   185
\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   186
%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   187
Sledgehammer: ATP ``\textit{spass}'' for subgoal 1: \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   188
$([a] = [b]) = (a = b)$ \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   189
Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   190
To minimize the number of lemmas, try this: \\
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   191
\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   192
%
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   193
Sledgehammer: ATP ``\textit{remote\_vampire}'' for subgoal 1: \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   194
$([a] = [b]) = (a = b)$ \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   195
Try this command: \textbf{by} (\textit{metis One\_nat\_def\_raw empty\_replicate} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   196
\phantom{Try this command: \textbf{by} (\textit{metis~}}\textit{insert\_Nil last\_ConsL replicate\_Suc}). \\
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   197
To minimize the number of lemmas, try this: \\
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   198
\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{remote\_vampire}] \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   199
\phantom{\textbf{sledgehammer}~}(\textit{One\_nat\_def\_raw empty\_replicate insert\_Nil} \\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   200
\phantom{\textbf{sledgehammer}~(}\textit{last\_ConsL replicate\_Suc}).
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   201
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   202
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   203
Sledgehammer ran E, SPASS, and the remote version of Vampire in parallel. If E
38043
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   204
is not installed (\S\ref{installation}), you will see references to
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   205
its remote American cousin \textit{remote\_e} instead of
f31ddd5da4e3 updated Sledgehammer docs
blanchet
parents: 37582
diff changeset
   206
\textit{e}; and if SPASS is not installed, it will not appear in the output.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   207
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   208
Based on each ATP proof, Sledgehammer gives a one-liner proof that uses the
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   209
\textit{metis} method. You can click them and insert them into the theory text.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   210
You can click the ``\textbf{sledgehammer} \textit{minimize}'' command if you
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   211
want to look for a shorter (and faster) proof. But here the proof found by E
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   212
looks perfect, so click it to finish the proof.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   213
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   214
You can ask Sledgehammer for an Isar text proof by passing the
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   215
\textit{isar\_proof} option:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   216
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   217
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   218
\textbf{sledgehammer} [\textit{isar\_proof}]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   219
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   220
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   221
When Isar proof construction is successful, it can yield proofs that are more
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   222
readable and also faster than the \textit{metis} one-liners. This feature is
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   223
experimental.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   224
37517
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   225
\section{Hints}
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   226
\label{hints}
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   227
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   228
For best results, first simplify your problem by calling \textit{auto} or at
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   229
least \textit{safe} followed by \textit{simp\_all}. None of the ATPs contain
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   230
arithmetic decision procedures. They are not especially good at heavy rewriting,
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   231
but because they regard equations as undirected, they often prove theorems that
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   232
require the reverse orientation of a \textit{simp} rule. Higher-order problems
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   233
can be tackled, but the success rate is better for first-order problems. Hence,
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   234
you may get better results if you first simplify the problem to remove
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   235
higher-order features.
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   236
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   237
Note that problems can be easy for auto and difficult for ATPs, but the reverse
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   238
is also true, so don't be discouraged if your first attempts fail. Because the
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   239
system refers to all theorems known to Isabelle, it is particularly suitable
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   240
when your goal has a short proof from lemmas that you don't know about.
19ba7ec5f1e3 steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents: 37498
diff changeset
   241
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   242
\section{Command Syntax}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   243
\label{command-syntax}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   244
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   245
Sledgehammer can be invoked at any point when there is an open goal by entering
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   246
the \textbf{sledgehammer} command in the theory file. Its general syntax is as
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   247
follows:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   248
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   249
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   250
\textbf{sledgehammer} \textit{subcommand\/$^?$ options\/$^?$ facts\_override\/$^?$ num\/$^?$}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   251
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   252
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   253
For convenience, Sledgehammer is also available in the ``Commands'' submenu of
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   254
the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   255
C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   256
no arguments in the theory text.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   257
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   258
In the general syntax, the \textit{subcommand} may be any of the following:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   259
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   260
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   261
\item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on subgoal number
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   262
\textit{num} (1 by default), with the given options and facts.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   263
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   264
\item[$\bullet$] \textbf{\textit{minimize}:} Attempts to minimize the provided facts
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   265
(specified in the \textit{facts\_override} argument) to obtain a simpler proof
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   266
involving fewer facts. The options and goal number are as for \textit{run}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   267
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   268
\item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued by
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   269
Sledgehammer. This allows you to examine results that might have been lost due
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   270
to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   271
limit on the number of messages to display (5 by default).
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   272
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   273
\item[$\bullet$] \textbf{\textit{available\_atps}:} Prints the list of installed ATPs.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   274
See \S\ref{installation} and \S\ref{mode-of-operation} for more information on
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   275
how to install ATPs.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   276
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   277
\item[$\bullet$] \textbf{\textit{running\_atps}:} Prints information about currently
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   278
running ATPs, including elapsed runtime and remaining time until timeout.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   279
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   280
\item[$\bullet$] \textbf{\textit{kill\_atps}:} Terminates all running ATPs.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   281
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   282
\item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   283
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   284
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   285
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   286
Sledgehammer's behavior can be influenced by various \textit{options}, which can
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   287
be specified in brackets after the \textbf{sledgehammer} command. The
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   288
\textit{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   289
\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true}'' is optional. For
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   290
example:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   291
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   292
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   293
\textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120$\,s$]
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   294
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   295
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   296
Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   297
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   298
\prew
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   299
\textbf{sledgehammer\_params} \textit{options}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   300
\postw
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   301
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   302
The supported options are described in \S\ref{option-reference}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   303
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   304
The \textit{facts\_override} argument lets you alter the set of facts that go
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   305
through the relevance filter. It may be of the form ``(\textit{facts})'', where
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   306
\textit{facts} is a space-separated list of Isabelle facts (theorems, local
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   307
assumptions, etc.), in which case the relevance filter is bypassed and the given
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   308
facts are used. It may also be of the form (\textit{add}:\ \textit{facts}$_1$),
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   309
(\textit{del}:\ \textit{facts}$_2$), or (\textit{add}:\ \textit{facts}$_1$\
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   310
\textit{del}:\ \textit{facts}$_2$), where the relevance filter is instructed to
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   311
proceed as usual except that it should consider \textit{facts}$_1$
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   312
highly-relevant and \textit{facts}$_2$ fully irrelevant.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   313
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   314
\section{Option Reference}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   315
\label{option-reference}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   316
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   317
\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   318
\def\qty#1{$\left<\textit{#1}\right>$}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   319
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   320
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   321
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   322
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   323
\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   324
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   325
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   326
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   327
\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   328
\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   329
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   330
Sledgehammer's options are categorized as follows:\ mode of operation
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   331
(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), output
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   332
format (\S\ref{output-format}), and timeouts (\S\ref{timeouts}).
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   333
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   334
The descriptions below refer to the following syntactic quantities:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   335
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   336
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   337
\item[$\bullet$] \qtybf{string}: A string.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   338
\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   339
\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   340
\item[$\bullet$] \qtybf{int\/}: An integer.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   341
\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   342
(milliseconds), or the keyword \textit{none} ($\infty$ years).
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   343
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   344
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   345
Default values are indicated in square brackets. Boolean options have a negated
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   346
counterpart (e.g., \textit{debug} vs.\ \textit{no\_debug}). When setting
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   347
Boolean options, ``= \textit{true}'' may be omitted.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   348
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   349
\subsection{Mode of Operation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   350
\label{mode-of-operation}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   351
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   352
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   353
%\optrue{blocking}{non\_blocking}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   354
%Specifies whether the \textbf{sledgehammer} command should operate synchronously.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   355
%The asynchronous (non-blocking) mode lets the user start proving the putative
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   356
%theorem while Sledgehammer looks for a counterexample, but it can also be more
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   357
%confusing. For technical reasons, automatic runs currently always block.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   358
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   359
\opnodefault{atps}{string}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   360
Specifies the ATPs (automated theorem provers) to use as a space-separated list
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   361
(e.g., ``\textit{e}~\textit{spass}''). The following ATPs are supported:
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   362
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   363
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   364
\item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   365
\cite{schulz-2002}. To use E, set the environment variable
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   366
\texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable,
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   367
or install the prebuilt E package from Isabelle's download page. See
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   368
\S\ref{installation} for details.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   369
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   370
\item[$\bullet$] \textbf{\textit{spass}:} SPASS is an ATP developed by Christoph
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   371
Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   372
environment variable \texttt{SPASS\_HOME} to the directory that contains the
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   373
\texttt{SPASS} executable, or install the prebuilt SPASS package from Isabelle's
37414
d0cea0796295 expect SPASS 3.7, and give a friendly warning if an older version is used
blanchet
parents: 36926
diff changeset
   374
download page. Sledgehammer requires version 3.5 or above. See
d0cea0796295 expect SPASS 3.7, and give a friendly warning if an older version is used
blanchet
parents: 36926
diff changeset
   375
\S\ref{installation} for details.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   376
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   377
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   378
Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   379
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   380
that contains the \texttt{vampire} executable.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   381
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   382
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E executes
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   383
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   384
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   385
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   386
Vampire executes on Geoff Sutcliffe's Miami servers. Version 9 is used.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   387
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   388
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   389
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   390
By default, Sledgehammer will run E, SPASS, and Vampire in parallel. For E and
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   391
SPASS, it will use any locally installed version if available, falling back
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   392
on the remote versions if necessary. For historical reasons, the default value
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   393
of this option can be overridden using the option ``Sledgehammer: ATPs'' from
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   394
the ``Isabelle'' menu in Proof General.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   395
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   396
It is a good idea to run several ATPs in parallel, although it could slow down
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   397
your machine. Tobias Nipkow observed that running E, SPASS, and Vampire together
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   398
for 5 seconds yields the same success rate as running the most effective of
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   399
these (Vampire) for 120 seconds \cite{boehme-nipkow-2010}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   400
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   401
\opnodefault{atp}{string}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   402
Alias for \textit{atps}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   403
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   404
\opfalse{overlord}{no\_overlord}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   405
Specifies whether Sledgehammer should put its temporary files in
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   406
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   407
debugging Sledgehammer but also unsafe if several instances of the tool are run
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   408
simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   409
safely remove them after Sledgehammer has run.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   410
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   411
\nopagebreak
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   412
{\small See also \textit{debug} (\S\ref{output-format}).}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   413
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   414
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   415
\subsection{Problem Encoding}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   416
\label{problem-encoding}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   417
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   418
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   419
\opfalse{explicit\_apply}{implicit\_apply}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   420
Specifies whether function application should be encoded as an explicit
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   421
``apply'' operator. If the option is set to \textit{false}, each function will
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   422
be directly applied to as many arguments as possible. Enabling this option can
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   423
sometimes help discover higher-order proofs that otherwise would not be found.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   424
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   425
\opfalse{full\_types}{partial\_types}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   426
Specifies whether full-type information is exported. Enabling this option can
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   427
prevent the discovery of type-incorrect proofs, but it also tends to slow down
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   428
the ATPs significantly. For historical reasons, the default value of this option
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   429
can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle''
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   430
menu in Proof General.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   431
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   432
\opdefault{relevance\_threshold}{int}{50}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   433
Specifies the threshold above which facts are considered relevant by the
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   434
relevance filter. The option ranges from 0 to 100, where 0 means that all
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   435
theorems are relevant.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   436
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   437
\opdefault{relevance\_convergence}{int}{320}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   438
Specifies the convergence quotient, multiplied by 100, used by the relevance
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   439
filter. This quotient is used by the relevance filter to scale down the
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   440
relevance of facts at each iteration of the filter.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   441
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   442
\opsmartx{theory\_relevant}{theory\_irrelevant}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   443
Specifies whether the theory from which a fact comes should be taken into
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   444
consideration by the relevance filter. If the option is set to \textit{smart},
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   445
it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire,
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   446
because empirical results suggest that these are the best settings.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   447
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   448
\opfalse{defs\_relevant}{defs\_irrelevant}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   449
Specifies whether the definition of constants occurring in the formula to prove
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   450
should be considered particularly relevant. Enabling this option tends to lead
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   451
to larger problems and typically slows down the ATPs.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   452
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   453
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   454
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   455
\subsection{Output Format}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   456
\label{output-format}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   457
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   458
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   459
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   460
\opfalse{verbose}{quiet}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   461
Specifies whether the \textbf{sledgehammer} command should explain what it does.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   462
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   463
\opfalse{debug}{no\_debug}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   464
Specifies whether Nitpick should display additional debugging information beyond
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   465
what \textit{verbose} already displays. Enabling \textit{debug} also enables
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   466
\textit{verbose} behind the scenes.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   467
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   468
\nopagebreak
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   469
{\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   470
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   471
\opfalse{isar\_proof}{no\_isar\_proof}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   472
Specifies whether Isar proofs should be output in addition to one-liner
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   473
\textit{metis} proofs. Isar proof construction is still experimental and often
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   474
fails; however, they are usually faster and sometimes more robust than
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   475
\textit{metis} proofs.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   476
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   477
\opdefault{isar\_shrink\_factor}{int}{1}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   478
Specifies the granularity of the Isar proof. A value of $n$ indicates that each
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   479
Isar proof step should correspond to a group of up to $n$ consecutive proof
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   480
steps in the ATP proof.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   481
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   482
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   483
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   484
\subsection{Timeouts}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   485
\label{timeouts}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   486
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   487
\begin{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   488
\opdefault{timeout}{time}{$\mathbf{60}$ s}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   489
Specifies the maximum amount of time that the ATPs should spend looking for a
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   490
proof. For historical reasons, the default value of this option can be
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   491
overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle''
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   492
menu in Proof General.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   493
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   494
\opdefault{minimize\_timeout}{time}{$\mathbf{5}$\,s}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   495
Specifies the maximum amount of time that the ATPs should spend looking for a
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   496
proof for \textbf{sledgehammer}~\textit{minimize}.
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   497
\end{enum}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   498
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   499
\let\em=\sl
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   500
\bibliography{../manual}{}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   501
\bibliographystyle{abbrv}
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   502
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents:
diff changeset
   503
\end{document}