diff --git a/src/Doc/Sledgehammer/document/root.tex b/src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex +++ b/src/Doc/Sledgehammer/document/root.tex @@ -1,1340 +1,1336 @@ \documentclass[a4paper,12pt]{article} \usepackage[T1]{fontenc} \usepackage{amsmath} \usepackage{amssymb} \usepackage[english]{babel} \usepackage{color} \usepackage{footmisc} \usepackage{graphicx} %\usepackage{mathpazo} \usepackage{multicol} \usepackage{stmaryrd} %\usepackage[scaled=.85]{beramono} \usepackage{isabelle,iman,pdfsetup} \newcommand\download{\url{https://isabelle.in.tum.de/components/}} \let\oldS=\S \def\S{\oldS\,} \def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}} \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$} \newcommand\const[1]{\textsf{#1}} %\oddsidemargin=4.6mm %\evensidemargin=4.6mm %\textwidth=150mm %\topmargin=4.6mm %\headheight=0mm %\headsep=0mm %\textheight=234mm \def\Colon{\mathord{:\mkern-1.5mu:}} %\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}} %\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}} \def\lparr{\mathopen{(\mkern-4mu\mid}} \def\rparr{\mathclose{\mid\mkern-4mu)}} \def\unk{{?}} \def\undef{(\lambda x.\; \unk)} %\def\unr{\textit{others}} \def\unr{\ldots} \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}} \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}} \urlstyle{tt} \renewcommand\_{\hbox{\textunderscore\kern-.05ex}} \hyphenation{Isa-belle super-posi-tion zipper-posi-tion} \begin{document} %%% TYPESETTING %\renewcommand\labelitemi{$\bullet$} \renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}} \title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex] Hammering Away \\[\smallskipamount] \Large A User's Guide to Sledgehammer for Isabelle/HOL} \author{\hbox{} \\ Jasmin Blanchette \\ {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount] {\normalsize with contributions from} \\[4\smallskipamount] Martin Desharnais \\ {\normalsize Forschungsinstitut CODE, Universit\"at der Bundeswehr M\"unchen} \\[4\smallskipamount] Lawrence C. Paulson \\ {\normalsize Computer Laboratory, University of Cambridge} \\ \hbox{}} \maketitle \tableofcontents \setlength{\parskip}{.7em plus .2em minus .1em} \setlength{\parindent}{0pt} \setlength{\abovedisplayskip}{\parskip} \setlength{\abovedisplayshortskip}{.9\parskip} \setlength{\belowdisplayskip}{\parskip} \setlength{\belowdisplayshortskip}{.9\parskip} % general-purpose enum environment with correct spacing \newenvironment{enum}% {\begin{list}{}{% \setlength{\topsep}{.1\parskip}% \setlength{\partopsep}{.1\parskip}% \setlength{\itemsep}{\parskip}% \advance\itemsep by-\parsep}} {\end{list}} \def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin \advance\rightskip by\leftmargin} \def\post{\vskip0pt plus1ex\endgroup} \def\prew{\pre\advance\rightskip by-\leftmargin} \def\postw{\post} \section{Introduction} \label{introduction} Sledgehammer is a tool that applies automatic theorem provers (ATPs) and satisfiability-modulo-theories (SMT) solvers on the current goal.% \footnote{The distinction between ATPs and SMT solvers is convenient but mostly historical.} % The supported ATPs include agsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E -\cite{schulz-2002}, iProver \cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III +\cite{schulz-2019}, iProver \cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III \cite{leo3}, Satallax \cite{satallax}, SPASS \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}. The ATPs are run either locally or remotely via the System\-On\-TPTP web service \cite{sutcliffe-2000}. The supported SMT solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, veriT \cite{bouton-et-al-2009}, -and Z3 \cite{z3}. These are always run locally. +and Z3 \cite{de-moura-2008}. These are always run locally. The problem passed to the external provers (or solvers) consists of your current goal together with a heuristic selection of hundreds of facts (theorems) from the current theory context, filtered by relevance. The result of a successful proof search is some source text that typically reconstructs the proof within Isabelle. For ATPs, the reconstructed proof typically relies on the general-purpose \textit{metis} proof method, which integrates the Metis ATP in Isabelle/HOL with explicit inferences going through the kernel. Thus its results are correct by construction. For Isabelle/jEdit users, Sledgehammer provides an automatic mode that can be enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options > Isabelle > General.'' In this mode, a reduced version of Sledgehammer is run on every newly entered theorem for a few seconds. \newbox\boxA \setbox\boxA=\hbox{\texttt{NOSPAM}} \newcommand\authoremail{\texttt{jasmin.blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak google.\allowbreak com}} To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is imported---this is rarely a problem in practice since it is part of \textit{Main}. Examples of Sledgehammer use can be found in the \texttt{src/HOL/Metis\_Examples} directory. Comments and bug reports concerning Sledgehammer or this manual should be directed to the author at \authoremail. \section{Installation} \label{installation} Sledgehammer is part of Isabelle, so you do not need to install it. However, it relies on third-party automatic provers (ATPs and SMT solvers). Among the ATPs, agsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and Zipperposition can be run locally; in addition, agsyHOL, Alt-Ergo, E, iProver, LEO-II, Leo-III, Satallax, Vampire, Waldmeister, and Zipperposition are available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers CVC3, CVC4, veriT, and Z3 can be run locally. There are three main ways to install automatic provers on your machine: \begin{sloppy} \begin{enum} \item[\labelitemi] If you installed an official Isabelle package, it should -already include properly setup executables for CVC4, E, SPASS, Vampire, and Z3, -ready to use. To use Vampire, you must confirm that you are a noncommercial -user, as indicated by the message that is displayed when Sledgehammer is -invoked the first time. +already include properly set up executables for CVC4, E, SPASS, Vampire, veriT, +and Z3, ready to use. To use Vampire, you must confirm that you are a +noncommercial user, as indicated by the message that is displayed when +Sledgehammer is invoked the first time. \item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, -CVC4, E, SPASS, Vampire, and Z3 binary packages from \download. Extract the -archives, then add a line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash -components}% +CVC4, E, SPASS, Vampire, veriT, and Z3 binary packages from \download. Extract +the archives, then add a line to your \texttt{\$ISABELLE\_HOME\_USER\slash +etc\slash components}% \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at startup. Its value can be retrieved by executing \texttt{isabelle} \texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.} -file with the absolute path to CVC3, CVC4, E, SPASS, Vampire, or Z3. For -example, if the \texttt{components} file does not exist yet and you extracted -SPASS to \texttt{/usr/local/spass-3.8ds}, create it with the single line +file with the absolute path to the prover. For example, if the +\texttt{components} file does not exist yet and you extracted SPASS to +\texttt{/usr/local/spass-3.8ds}, create it with the single line \prew \texttt{/usr/local/spass-3.8ds} \postw in it. \item[\labelitemi] If you prefer to build agsyHOL, Alt-Ergo, E, LEO-II, Leo-III, or Satallax manually, set the environment variable \texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME}, \texttt{LEO3\_HOME}, or \texttt{SATALLAX\_HOME} to the directory that contains the \texttt{agsyHOL}, \texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}), \texttt{leo}, \texttt{leo3}, or \texttt{satallax} executable; for Alt-Ergo, set the environment variable \texttt{WHY3\_HOME} to the directory that contains the \texttt{why3} executable. Sledgehammer has been tested with agsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 2.0, LEO-II 1.3.4, Leo-III 1.1, and Satallax 2.7. Since the ATPs' output formats are neither documented nor stable, other versions might not work well with Sledgehammer. Ideally, you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION}, \texttt{LEO3\_VERSION}, or \texttt{SATALLAX\_VERSION} to the prover's version number (e.g., ``2.7''); this might help Sledgehammer invoke the prover optimally. Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER}, \texttt{VERIT\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of the executable, \emph{including the file name}. Sledgehammer has been tested -with CVC3 2.2 and 2.4.1, CVC4 1.5-prerelease, veriT smtcomp2019, and Z3 4.3.2. +with CVC3 2.2 and 2.4.1, CVC4 1.5-prerelease, veriT 2020.10-rmx, and Z3 4.3.2. Since Z3's output format is somewhat unstable, other versions of the solver might not work well with Sledgehammer. Ideally, also set \texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, \texttt{VERIT\_VERSION}, or \texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.4.0''). \end{enum} \end{sloppy} To check whether the provers are successfully installed, try out the example in \S\ref{first-steps}. If the remote versions of any of these provers is used (identified by the prefix ``\textit{remote\_\/}''), or if the local versions fail to solve the easy goal presented there, something must be wrong with the installation. Remote prover invocation requires Perl with the World Wide Web Library (\texttt{libwww-perl}) installed. If you must use a proxy server to access the Internet, set the \texttt{http\_proxy} environment variable to the proxy, either in the environment in which Isabelle is launched or in your \texttt{\$ISABELLE\_HOME\_USER/etc/\allowbreak settings} file. Here are a few examples: \prew \texttt{http\_proxy=http://proxy.example.org} \\ \texttt{http\_proxy=http://proxy.example.org:8080} \\ \texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org} \postw \section{First Steps} \label{first-steps} To illustrate Sledgehammer in context, let us start a theory file and attempt to prove a simple lemma: \prew \textbf{theory}~\textit{Scratch} \\ \textbf{imports}~\textit{Main} \\ \textbf{begin} \\[2\smallskipamount] % \textbf{lemma} ``$[a] = [b] \,\Longrightarrow\, a = b$'' \\ \textbf{sledgehammer} \postw Instead of issuing the \textbf{sledgehammer} command, you can also use the -Sledgehammer panel in Isabelle/jEdit. Sledgehammer produces the following output -after a few seconds: +Sledgehammer panel in Isabelle/jEdit. Sledgehammer might produce something like +the following output after a few seconds: \prew \slshape Proof found\ldots \\ ``\textit{e\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms) \\ % ``\textit{cvc4\/}'': Try this: \textbf{by} \textit{simp} (0.4 ms) \\ % ``\textit{z3\/}'': Try this: \textbf{by} \textit{simp} (0.5 ms) \\ % ``\textit{spass\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms) % \postw Sledgehammer ran CVC4, E, SPASS, and Z3 in parallel. Depending on which provers are installed and how many processor cores are available, some of the provers might be missing or present with a \textit{remote\_} prefix. -For each successful prover, Sledgehammer gives a one-line \textit{metis} or -\textit{smt} method call. Rough timings are shown in parentheses, indicating how -fast the call is. You can click the proof to insert it into the theory text. +For each successful prover, Sledgehammer gives a one-line Isabelle proof. Rough +timings are shown in parentheses, indicating how fast the call is. You can +click the proof to insert it into the theory text. In addition, you can ask Sledgehammer for an Isar text proof by enabling the \textit{isar\_proofs} option (\S\ref{output-format}): \prew \textbf{sledgehammer} [\textit{isar\_proofs}] \postw When Isar proof construction is successful, it can yield proofs that are more -readable and also faster than the \textit{metis} or \textit{smt} one-line -proofs. This feature is experimental and is only available for ATPs. +readable and also faster than \textit{metis} or \textit{smt} one-line +proofs. This feature is experimental. \section{Hints} \label{hints} This section presents a few hints that should help you get the most out of Sledgehammer. Frequently asked questions are answered in \S\ref{frequently-asked-questions}. %\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak} \newcommand\point[1]{\subsection{\emph{#1}}} \point{Presimplify the goal} For best results, first simplify your problem by calling \textit{auto} or at least \textit{safe} followed by \textit{simp\_all}. The SMT solvers provide arithmetic decision procedures, but the ATPs typically do not (or if they do, Sledgehammer does not use it yet). Apart from Waldmeister, they are not particularly good at heavy rewriting, but because they regard equations as undirected, they often prove theorems that require the reverse orientation of a \textit{simp} rule. Higher-order problems can be tackled, but the success rate is better for first-order problems. Hence, you may get better results if you first simplify the problem to remove higher-order features. \point{Familiarize yourself with the main options} Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of the options are very specialized, but serious users of the tool should at least familiarize themselves with the following options: \begin{enum} \item[\labelitemi] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies the automatic provers (ATPs and SMT solvers) that should be run whenever Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{cvc4 e spass vampire\/}''). For convenience, you can omit ``\textit{provers}~='' and simply write the prover names as a space-separated list (e.g., ``\textit{cvc4 e spass vampire\/}''). \item[\labelitemi] \textbf{\textit{max\_facts}} (\S\ref{relevance-filter}) specifies the maximum number of facts that should be passed to the provers. By default, the value is prover-dependent but varies between about 50 and 1000. If the provers time out, you can try lowering this value to, say, 25 or 50 and see if that helps. \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies that Isar proofs should be generated, in addition to one-line \textit{metis} or \textit{smt} proofs. The length of the Isar proofs can be controlled by setting \textit{compress} (\S\ref{output-format}). \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the provers' time limit. It is set to 30 seconds by default. \end{enum} Options can be set globally using \textbf{sledgehammer\_params} (\S\ref{command-syntax}). The command also prints the list of all available options with their current value. Fact selection can be influenced by specifying ``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} call to ensure that certain facts are included, or simply ``$(\textit{my\_facts})$'' to force Sledgehammer to run only with $\textit{my\_facts}$ (and any facts chained into the goal). \section{Frequently Asked Questions} \label{frequently-asked-questions} This sections answers frequently (and infrequently) asked questions about Sledgehammer. It is a good idea to skim over it now even if you do not have any questions at this stage. And if you have any further questions not listed here, send them to the author at \authoremail. \point{Which facts are passed to the automatic provers?} Sledgehammer heuristically selects a few hundred relevant lemmas from the currently loaded libraries. The component that performs this selection is called \emph{relevance filter} (\S\ref{relevance-filter}). \begin{enum} \item[\labelitemi] The traditional relevance filter, \emph{MePo} (\underline{Me}ng--\underline{Pau}lson), assigns a score to every available fact (lemma, theorem, definition, or axiom) based upon how many constants that fact shares with the conjecture. This process iterates to include facts relevant to those just accepted. The constants are weighted to give unusual ones greater significance. MePo copes best when the conjecture contains some unusual constants; if all the constants are common, it is unable to discriminate among the hundreds of facts that are picked up. The filter is also memoryless: It has no information about how many times a particular fact has been used in a proof, and it cannot learn. \item[\labelitemi] An alternative to MePo is \emph{MaSh} (\underline{Ma}chine Learner for \underline{S}ledge\underline{h}ammer). It applies machine learning to the problem of finding relevant facts. \item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh. This is the default. \end{enum} The number of facts included in a problem varies from prover to prover, since some provers get overwhelmed more easily than others. You can show the number of facts given using the \textit{verbose} option (\S\ref{output-format}) and the actual facts using \textit{debug} (\S\ref{output-format}). Sledgehammer is good at finding short proofs combining a handful of existing lemmas. If you are looking for longer proofs, you must typically restrict the number of facts, by setting the \textit{max\_facts} option (\S\ref{relevance-filter}) to, say, 25 or 50. You can also influence which facts are actually selected in a number of ways. If you simply want to ensure that a fact is included, you can specify it using the ``$(\textit{add}{:}~\textit{my\_facts})$'' syntax. For example: % \prew \textbf{sledgehammer} (\textit{add}: \textit{hd.simps} \textit{tl.simps}) \postw % The specified facts then replace the least relevant facts that would otherwise be included; the other selected facts remain the same. If you want to direct the selection in a particular direction, you can specify the facts via \textbf{using}: % \prew \textbf{using} \textit{hd.simps} \textit{tl.simps} \\ \textbf{sledgehammer} \postw % The facts are then more likely to be selected than otherwise, and if they are selected at iteration $j$ they also influence which facts are selected at iterations $j + 1$, $j + 2$, etc. To give them even more weight, try % \prew \textbf{using} \textit{hd.simps} \textit{tl.simps} \\ \textbf{apply}~\textbf{--} \\ \textbf{sledgehammer} \postw \point{Why does Metis fail to reconstruct the proof?} There are many reasons. If Metis runs seemingly forever, that is a sign that the proof is too difficult for it. Metis's search is complete for first-order logic with equality, so if the proof was found by a superposition-based ATP such as E, SPASS, or Vampire, Metis should eventually find it, but that is little consolation. In some rare cases, \textit{metis} fails fairly quickly, and you get the error message ``One-line proof reconstruction failed.'' This indicates that Sledgehammer determined that the goal is provable, but the proof is, for technical reasons, beyond \textit{metis}'s power. You can then try again with the \textit{strict} option (\S\ref{problem-encoding}). If the goal is actually unprovable and you did not specify an unsound encoding using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are strongly encouraged to report this to the author at \authoremail. \point{What are the \textit{full\_types}, \textit{no\_types}, and \\ \textit{mono\_tags} arguments to Metis?} The \textit{metis}~(\textit{full\_types}) proof method and its cousin \textit{metis}~(\textit{mono\_tags}) are fully-typed versions of Metis. It is somewhat slower than \textit{metis}, but the proof search is fully typed, and it also includes more powerful rules such as the axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in -higher-order places (e.g., in set comprehensions). The method is automatically -tried as a fallback when \textit{metis} fails, and it is sometimes -generated by Sledgehammer instead of \textit{metis} if the proof obviously -requires type information or if \textit{metis} failed when Sledgehammer -preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with -various sets of option for up to 1~second each time to ensure that the generated -one-line proofs actually work and to display timing information. This can be -configured using the \textit{preplay\_timeout} and \textit{dont\_preplay} -options (\S\ref{timeouts}).) +higher-order places (e.g., in set comprehensions). The method is tried as a +fallback when \textit{metis} fails, and it is sometimes generated by +Sledgehammer instead of \textit{metis} if the proof obviously requires type +information or if \textit{metis} failed when Sledgehammer preplayed the proof. % At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types}) uses no type information at all during the proof search, which is more efficient but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally generated by Sledgehammer. % See the \textit{type\_enc} option (\S\ref{problem-encoding}) for details. Incidentally, if you ever see warnings such as \prew \slshape Metis: Falling back on ``\textit{metis} (\textit{full\_types})'' \postw for a successful \textit{metis} proof, you can advantageously pass the \textit{full\_types} option to \textit{metis} directly. \point{And what are the \textit{lifting} and \textit{hide\_lams} \\ arguments to Metis?} Orthogonally to the encoding of types, it is important to choose an appropriate -translation of $\lambda$-abstractions. Metis supports three translation schemes, -in decreasing order of power: Curry combinators (the default), +translation of $\lambda$-abstractions. Metis supports three translation +schemes, in decreasing order of power: Curry combinators (the default), $\lambda$-lifting, and a ``hiding'' scheme that disables all reasoning under $\lambda$-abstractions. The more powerful schemes also give the automatic -provers more rope to hang themselves. See the \textit{lam\_trans} option (\S\ref{problem-encoding}) for details. +provers more rope to hang themselves. See the \textit{lam\_trans} option +(\S\ref{problem-encoding}) for details. \point{Are the generated proofs minimal?} Automatic provers frequently use many more facts than are necessary. -Sledgehammer includes a minimization tool that takes a set of facts returned by +Sledgehammer includes a proof minimization tool that takes a set of facts returned by a given prover and repeatedly calls a prover or proof method with subsets of those facts to find a minimal set. Reducing the number of facts typically helps reconstruction, while decluttering the proof scripts. \point{A strange error occurred---what should I do?} Sledgehammer tries to give informative error messages. Please report any strange error to the author at \authoremail. \point{Auto can solve it---why not Sledgehammer?} Problems can be easy for \textit{auto} and difficult for automatic provers, but the reverse is also true, so do not be discouraged if your first attempts fail. Because the system refers to all theorems known to Isabelle, it is particularly suitable when your goal has a short proof but requires lemmas that you do not know about. \point{Why are there so many options?} Sledgehammer's philosophy is that it should work out of the box, without user guidance. Most of the options are meant to be used by the Sledgehammer developers for experiments. \section{Command Syntax} \label{command-syntax} \subsection{Sledgehammer} \label{sledgehammer} Sledgehammer can be invoked at any point when there is an open goal by entering the \textbf{sledgehammer} command in the theory file. Its general syntax is as follows: \prew \textbf{sledgehammer} \qty{subcommand}$^?$ \qty{options}$^?$ \qty{facts\_override}$^?$ \qty{num}$^?$ \postw In the general syntax, the \qty{subcommand} may be any of the following: \begin{enum} \item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on subgoal number \qty{num} (1 by default), with the given options and facts. \item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of automatic provers supported by Sledgehammer. See \S\ref{installation} and \S\ref{mode-of-operation} for more information on how to install automatic provers. \item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}. \end{enum} In addition, the following subcommands provide finer control over machine learning with MaSh: \begin{enum} \item[\labelitemi] \textbf{\textit{unlearn}:} Resets MaSh, erasing any persistent state. \item[\labelitemi] \textbf{\textit{learn\_isar}:} Invokes MaSh on the current theory to process all the available facts, learning from their Isabelle/Isar proofs. This happens automatically at Sledgehammer invocations if the \textit{learn} option (\S\ref{relevance-filter}) is enabled. \item[\labelitemi] \textbf{\textit{learn\_prover}:} Invokes MaSh on the current theory to process all the available facts, learning from proofs generated by automatic provers. The prover to use and its timeout can be set using the \textit{prover} (\S\ref{mode-of-operation}) and \textit{timeout} (\S\ref{timeouts}) options. It is recommended to perform learning using a first-order ATP (such as E, SPASS, and Vampire) as opposed to a higher-order ATP or an SMT solver. \item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn} followed by \textit{learn\_isar}. \item[\labelitemi] \textbf{\textit{relearn\_prover}:} Same as \textit{unlearn} followed by \textit{learn\_prover}. \end{enum} Sledgehammer's behavior can be influenced by various \qty{options}, which can be specified in brackets after the \textbf{sledgehammer} command. The \qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1, \ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. For example: \prew \textbf{sledgehammer} [\textit{isar\_proofs}, \,\textit{timeout} = 120] \postw Default values can be set using \textbf{sledgehammer\_\allowbreak params}: \prew \textbf{sledgehammer\_params} \qty{options} \postw The supported options are described in \S\ref{option-reference}. The \qty{facts\_override} argument lets you alter the set of facts that go through the relevance filter. It may be of the form ``(\qty{facts})'', where \qty{facts} is a space-separated list of Isabelle facts (theorems, local assumptions, etc.), in which case the relevance filter is bypassed and the given facts are used. It may also be of the form ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}})'', ``(\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', or ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}}\ \textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', where the relevance filter is instructed to proceed as usual except that it should consider \qty{facts\/_{\mathrm{1}}} highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant. If you use Isabelle/jEdit, Sledgehammer also provides an automatic mode that can be enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options > Isabelle > General.'' For automatic runs, only the first prover set using \textit{provers} (\S\ref{mode-of-operation}) is considered (typically E), \textit{slice} (\S\ref{mode-of-operation}) is disabled, fewer facts are passed to the prover, \textit{fact\_filter} (\S\ref{relevance-filter}) is set to \textit{mepo}, \textit{strict} (\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled, and \textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Time Limit'' option in jEdit. Sledgehammer's output is also more concise. \subsection{Metis} \label{metis} The \textit{metis} proof method has the syntax \prew \textbf{\textit{metis}}~(\qty{options})${}^?$~\qty{facts}${}^?$ \postw where \qty{facts} is a list of arbitrary facts and \qty{options} is a comma-separated list consisting of at most one $\lambda$ translation scheme specification with the same semantics as Sledgehammer's \textit{lam\_trans} option (\S\ref{problem-encoding}) and at most one type encoding specification with the same semantics as Sledgehammer's \textit{type\_enc} option (\S\ref{problem-encoding}). % The supported $\lambda$ translation schemes are \textit{hide\_lams}, \textit{lifting}, and \textit{combs} (the default). % All the untyped type encodings listed in \S\ref{problem-encoding} are supported. For convenience, the following aliases are provided: \begin{enum} \item[\labelitemi] \textbf{\textit{full\_types}:} Alias for \textit{poly\_guards\_query}. \item[\labelitemi] \textbf{\textit{partial\_types}:} Alias for \textit{poly\_args}. \item[\labelitemi] \textbf{\textit{no\_types}:} Alias for \textit{erased}. \end{enum} \section{Option Reference} \label{option-reference} \def\defl{\{} \def\defr{\}} \def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}} \def\optrueonly#1{\flushitem{\textit{#1} $\bigl[$= \textit{true}$\bigr]$\enskip}\nopagebreak\\[\parskip]} \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]} \def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]} \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]} \def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]} \def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} \def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} Sledgehammer's options are categorized as follows:\ mode of operation (\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), relevance filter (\S\ref{relevance-filter}), output format (\S\ref{output-format}), regression testing (\S\ref{regression-testing}), and timeouts (\S\ref{timeouts}). The descriptions below refer to the following syntactic quantities: \begin{enum} \item[\labelitemi] \qtybf{string}: A string. \item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}. \item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or \textit{smart}. \item[\labelitemi] \qtybf{int\/}: An integer. \item[\labelitemi] \qtybf{float}: A floating-point number (e.g., 2.5 or 60) expressing a number of seconds. \item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers (e.g., 0.6 0.95). \item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}. \end{enum} Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options have a negative counterpart (e.g., \textit{minimize} vs.\ \textit{dont\_minimize}). When setting Boolean options or their negative counterparts, ``= \textit{true\/}'' may be omitted. \subsection{Mode of Operation} \label{mode-of-operation} \begin{enum} \opnodefaultbrk{provers}{string} Specifies the automatic provers to use as a space-separated list (e.g., ``\textit{cvc4}~\textit{e}~\textit{spass}~\textit{vampire\/}''). Provers can be run locally or remotely; see \S\ref{installation} for installation instructions. The following local provers are supported: \begin{sloppy} \begin{enum} \item[\labelitemi] \textbf{\textit{agsyhol}:} agsyHOL is an automatic higher-order prover developed by Fredrik Lindblad \cite{agsyHOL}. To use agsyHOL, set the environment variable \texttt{AGSYHOL\_HOME} to the directory that contains the \texttt{agsyHOL} executable. Sledgehammer has been tested with version 1.0. \item[\labelitemi] \textbf{\textit{alt\_ergo}:} Alt-Ergo is a polymorphic ATP developed by Bobot et al.\ \cite{alt-ergo}. It supports the TPTP polymorphic typed first-order format (TF1) via Why3 \cite{why3}. To use Alt-Ergo, set the environment variable \texttt{WHY3\_HOME} to the directory that contains the \texttt{why3} executable. Sledgehammer requires Alt-Ergo 0.95.2 and Why3 0.83. \item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3, set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the executable, including the file name, or install the prebuilt CVC3 package from \download. Sledgehammer has been tested with versions 2.2 and 2.4.1. \item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 \cite{cvc4} is the successor to CVC3. To use CVC4, set the environment variable \texttt{CVC4\_SOLVER} to the complete path of the executable, including the file name, or install the prebuilt CVC4 package from \download. Sledgehammer has been tested with version 1.5-prerelease. \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover -developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment +developed by Stephan Schulz \cite{schulz-2019}. To use E, set the environment variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or install the prebuilt E package from \download. Sledgehammer has been tested with versions 1.6 to 1.8. \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the directory that contains the \texttt{iproveropt} executable. Sledgehammer has been tested with version 2.8. iProver depends on E to clausify problems, so make sure that E is installed as well. \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, with support for the TPTP typed higher-order syntax (TH0). To use LEO-II, set the environment variable \texttt{LEO2\_HOME} to the directory that contains the -\texttt{leo} executable. Sledgehammer requires version 1.3.4 or above. +\texttt{leo} executable. Sledgehammer has been tested with version 1.3.4. \item[\labelitemi] \textbf{\textit{leo3}:} Leo-III is an automatic higher-order prover developed by Alexander Steen, Max Wisniewski, Christoph Benzm\"uller et al.\ \cite{leo3}, with support for the TPTP typed higher-order syntax (TH0). To use Leo-III, set the environment variable \texttt{LEO3\_HOME} to the directory that contains the -\texttt{leo3} executable. Sledgehammer requires version 1.1 or above. +\texttt{leo3} executable. Sledgehammer has been tested with version 1.1. \item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with support for the TPTP typed higher-order syntax (TH0). To use Satallax, set the environment variable \texttt{SATALLAX\_HOME} to the directory that contains the -\texttt{satallax} executable. Sledgehammer requires version 2.2 or above. +\texttt{satallax} executable. Sledgehammer has been tested with version 2.2. \item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from -\download. Sledgehammer requires version 3.8ds or above. +\download. Sledgehammer has been tested with version 3.8ds. \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution prover developed by Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire} executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``4.2.2''). Sledgehammer has been tested with versions 1.8 to 4.2.2 (in the post-2010 numbering scheme). \item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is an SMT solver developed by David D\'eharbe, Pascal Fontaine, and their colleagues. -It is specifically designed to produce detailed proofs for reconstruction in -proof assistants. To use veriT, set the environment variable -\texttt{VERIT\_SOLVER} to the complete path of the executable, including the -file name. Sledgehammer has been tested with version smtcomp2019. +It is designed to produce detailed proofs for reconstruction in proof +assistants. To use veriT, set the environment variable \texttt{VERIT\_SOLVER} +to the complete path of the executable, including the file name. Sledgehammer +has been tested with version 2020.10-rmx. \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at -Microsoft Research \cite{z3}. To use Z3, set the environment variable +Microsoft Research \cite{de-moura-2008}. To use Z3, set the environment variable \texttt{Z3\_SOLVER} to the complete path of the executable, including the file name. Sledgehammer has been tested with a pre-release version of 4.4.0. \item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to -be an ATP, exploiting Z3's support for the TPTP typed first-order format -(TF0). It is included for experimental purposes. It requires version 4.3.1 of -Z3 or above. To use it, set the environment variable \texttt{Z3\_TPTP\_HOME} +be an ATP, exploiting Z3's support for the TPTP typed first-order format (TF0). +It is included for experimental purposes. Sledgehammer has been tested with +version 4.3.1. To use it, set the environment variable \texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp} executable. \item[\labelitemi] \textbf{\textit{zipperposition}:} Zipperposition \cite{cruanes-2014} is a higher-order superposition prover developed by Simon Cruanes, Petar Vukmirovi\'c, and colleagues. To use Zipperposition, set the environment variable \texttt{ZIPPERPOSITION\_HOME} to the directory that contains the \texttt{zipperposition} executable and \texttt{ZIPPERPOSITION\_VERSION} to the version number (e.g., ``2.0.1''). Sledgehammer has been tested with version 2.0.1. \end{enum} \end{sloppy} Moreover, the following remote provers are supported: \begin{enum} \item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of agsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_alt\_ergo}:} The remote version of Alt-Ergo runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_iprover}:} The remote version of iProver runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of Vampire runs on Geoff Sutcliffe's Miami servers. \item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be used to prove universally quantified equations using unconditional equations, corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister runs on Geoff Sutcliffe's Miami servers. \item[\labelitemi] \textbf{\textit{remote\_zipperposition}:} The remote version of Zipperposition runs on Geoff Sutcliffe's Miami servers. \end{enum} By default, Sledgehammer runs a subset of CVC4, E, SPASS, Vampire, veriT, and Z3 in parallel, either locally or remotely---depending on the number of processor cores available and on which provers are actually installed. It is generally desirable to run several provers in parallel. \opnodefault{prover}{string} Alias for \textit{provers}. \optrue{slice}{dont\_slice} Specifies whether the time allocated to a prover should be sliced into several segments, each of which has its own set of possibly prover-dependent options. For SPASS and Vampire, the first slice tries the fast but incomplete set-of-support (SOS) strategy, whereas the second slice runs without it. For E, up to three slices are tried, with different weighted search strategies and number of facts. For SMT solvers, several slices are tried with the same options each time but fewer and fewer facts. According to benchmarks with a timeout of 30 seconds, slicing is a valuable optimization, and you should probably leave it enabled unless you are conducting experiments. \nopagebreak {\small See also \textit{verbose} (\S\ref{output-format}).} \optrue{minimize}{dont\_minimize} -Specifies whether the minimization tool should be invoked automatically after -proof search. +Specifies whether the proof minimization tool should be invoked automatically +after proof search. \nopagebreak {\small See also \textit{preplay\_timeout} (\S\ref{timeouts}) and \textit{dont\_preplay} (\S\ref{timeouts}).} \opfalse{spy}{dont\_spy} Specifies whether Sledgehammer should record statistics in \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak spy\_\allowbreak sledgehammer}. These statistics can be useful to the developers of Sledgehammer. If you are willing to have your interactions recorded in the name of science, please enable this feature and send the statistics file every now and then to the author of this manual (\authoremail). To change the default value of this option globally, set the environment variable \texttt{SLEDGEHAMMER\_SPY} to \textit{yes}. \nopagebreak {\small See also \textit{debug} (\S\ref{output-format}).} \opfalse{overlord}{no\_overlord} Specifies whether Sledgehammer should put its temporary files in \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for debugging Sledgehammer but also unsafe if several instances of the tool are run simultaneously. The files are identified by the prefixes \texttt{prob\_} and \texttt{mash\_}; you may safely remove them after Sledgehammer has run. \textbf{Warning:} This option is not thread-safe. Use at your own risks. \nopagebreak {\small See also \textit{debug} (\S\ref{output-format}).} \end{enum} \subsection{Relevance Filter} \label{relevance-filter} \begin{enum} \opdefault{fact\_filter}{string}{smart} Specifies the relevance filter to use. The following filters are available: \begin{enum} \item[\labelitemi] \textbf{\textit{mepo}:} The traditional memoryless MePo relevance filter. \item[\labelitemi] \textbf{\textit{mash}:} The MaSh machine learner. Three learning algorithms are provided: \begin{enum} \item[\labelitemi] \textbf{\textit{nb}} is an implementation of naive Bayes. \item[\labelitemi] \textbf{\textit{knn}} is an implementation of $k$-nearest neighbors. \item[\labelitemi] \textbf{\textit{nb\_knn}} (also called \textbf{\textit{yes}} and \textbf{\textit{sml}}) is a combination of naive Bayes and $k$-nearest neighbors. \end{enum} In addition, the special value \textit{none} is used to disable machine learning by default (cf.\ \textit{smart} below). The default algorithm is \textit{nb\_knn}. The algorithm can be selected by setting the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle > General'' in Isabelle/jEdit. Persistent data for both algorithms is stored in the directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak mash}. \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the rankings from MePo and MaSh. \item[\labelitemi] \textbf{\textit{smart}:} A combination of MePo, MaSh, and MeSh. If the learning algorithm is set to be \textit{none}, \textit{smart} behaves like MePo. \end{enum} \opdefault{max\_facts}{smart\_int}{smart} Specifies the maximum number of facts that may be returned by the relevance filter. If the option is set to \textit{smart} (the default), it effectively takes a value that was empirically found to be appropriate for the prover. Typical values lie between 50 and 1000. \opdefault{fact\_thresholds}{float\_pair}{\upshape 0.45~0.85} Specifies the thresholds above which facts are considered relevant by the relevance filter. The first threshold is used for the first iteration of the relevance filter and the second threshold is used for the last iteration (if it is reached). The effective threshold is quadratically interpolated for the other iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems are relevant and 1 only theorems that refer to previously seen constants. \optrue{learn}{dont\_learn} -Specifies whether MaSh should be run automatically by Sledgehammer to learn the +Specifies whether Sledgehammer invocations should run MaSh to learn the available theories (and hence provide more accurate results). Learning takes place only if MaSh is enabled. \opdefault{max\_new\_mono\_instances}{int}{smart} Specifies the maximum number of monomorphic instances to generate beyond \textit{max\_facts}. The higher this limit is, the more monomorphic instances are potentially generated. Whether monomorphization takes place depends on the type encoding used. If the option is set to \textit{smart} (the default), it takes a value that was empirically found to be appropriate for the prover. For most provers, this value is 100. \nopagebreak {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).} \opdefault{max\_mono\_iters}{int}{smart} Specifies the maximum number of iterations for the monomorphization fixpoint construction. The higher this limit is, the more monomorphic instances are potentially generated. Whether monomorphization takes place depends on the type encoding used. If the option is set to \textit{smart} (the default), it takes a value that was empirically found to be appropriate for the prover. For most provers, this value is 3. \nopagebreak {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).} \end{enum} \subsection{Problem Encoding} \label{problem-encoding} \newcommand\comb[1]{\const{#1}} \begin{enum} \opdefault{lam\_trans}{string}{smart} Specifies the $\lambda$ translation scheme to use in ATP problems. The supported translation schemes are listed below: \begin{enum} \item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$-abstractions by replacing them by unspecified fresh constants, effectively disabling all reasoning under $\lambda$-abstractions. \item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions, defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting). \item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators enable the ATPs to synthesize $\lambda$-terms but tend to yield bulkier formulas than $\lambda$-lifting: The translation is quadratic in the worst case, and the equational definitions of the combinators are very prolific in the context of resolution. \item[\labelitemi] \textbf{\textit{combs\_and\_lifting}:} Introduce a new supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators. \item[\labelitemi] \textbf{\textit{combs\_or\_lifting}:} For each cluster of $\lambda$-abstractions, heuristically choose between $\lambda$-lifting and Curry combinators. \item[\labelitemi] \textbf{\textit{keep\_lams}:} Keep the $\lambda$-abstractions in the generated problems. This is available only with provers that support the TH0 syntax. \item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used depends on the ATP and should be the most efficient scheme for that ATP. \end{enum} For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting}, irrespective of the value of this option. \opsmartx{uncurried\_aliases}{no\_uncurried\_aliases} Specifies whether fresh function symbols should be generated as aliases for applications of curried functions in ATP problems. \opdefault{type\_enc}{string}{smart} Specifies the type encoding to use in ATP problems. Some of the type encodings are unsound, meaning that they can give rise to spurious proofs (unreconstructible using \textit{metis}). The type encodings are listed below, with an indication of their soundness in parentheses. An asterisk (*) indicates that the encoding is slightly incomplete for reconstruction with \textit{metis}, unless the \textit{strict} option (described below) is enabled. \begin{enum} \item[\labelitemi] \textbf{\textit{erased} (unsound):} No type information is supplied to the ATP, not even to resolve overloading. Types are simply erased. \item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using a predicate \const{g}$(\tau, t)$ that guards bound variables. Constants are annotated with their types, supplied as extra arguments, to resolve overloading. \item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is tagged with its type using a function $\const{t\/}(\tau, t)$. \item[\labelitemi] \textbf{\textit{poly\_args} (unsound):} Like for \textit{poly\_guards} constants are annotated with their types to resolve overloading, but otherwise no type information is encoded. This is the default encoding used by the \textit{metis} proof method. \item[\labelitemi] \textbf{% \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\ \textit{raw\_mono\_args} (unsound):} \\ Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args}, respectively, but the problem is additionally monomorphized, meaning that type variables are instantiated with heuristically chosen ground types. Monomorphization can simplify reasoning but also leads to larger fact bases, which can slow down the ATPs. \item[\labelitemi] \textbf{% \textit{mono\_guards}, \textit{mono\_tags} (sound); \textit{mono\_args} \\ (unsound):} \\ Similar to \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and \textit{raw\_mono\_\allowbreak args}, respectively but types are mangled in constant names instead of being supplied as ground term arguments. The binary predicate $\const{g}(\tau, t)$ becomes a unary predicate $\const{g\_}\tau(t)$, and the binary function $\const{t}(\tau, t)$ becomes a unary function $\const{t\_}\tau(t)$. \item[\labelitemi] \textbf{\textit{mono\_native} (sound):} Exploits native first-order types if the prover supports the TF0, TF1, TH0, or TH1 syntax; otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized. \item[\labelitemi] \textbf{\textit{mono\_native\_fool} (sound):} Exploits native first-order types, including Booleans, if the prover supports the TFX0, TFX1, TH0, or TH1 syntax; otherwise, falls back on \textit{mono\_native}. The problem is monomorphized. \item[\labelitemi] \textbf{\textit{mono\_native\_higher}, \textit{mono\_native\_higher\_fool} \\ (sound):} Exploits native higher-order types, including Booleans if ending with ``\textit{\_fool}'', if the prover supports the TH0 syntax; otherwise, falls back on \textit{mono\_native} or \textit{mono\_native\_fool}. The problem is monomorphized. \item[\labelitemi] \textbf{\textit{poly\_native}, \textit{poly\_native\_fool}, \textit{poly\_native\_higher}, \\ \textit{poly\_native\_higher\_fool} (sound):} Exploits native first-order polymorphic types if the prover supports the TF1, TFX1, or TH1 syntax; otherwise, falls back on \textit{mono\_native}, \textit{mono\_native\_fool}, \textit{mono\_native\_higher}, or \textit{mono\_native\_higher\_fool}. \item[\labelitemi] \textbf{% \textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\ \textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\ \textit{mono\_native}? (sound*):} \\ The type encodings \textit{poly\_guards}, \textit{poly\_tags}, \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards}, \textit{mono\_tags}, and \textit{mono\_native} are fully typed and sound. For each of these, Sledgehammer also provides a lighter variant identified by a question mark (`\hbox{?}')\ that detects and erases monotonic types, notably infinite types. (For \textit{mono\_native}, the types are not actually erased but rather replaced by a shared uniform type of individuals.) As argument to the \textit{metis} proof method, the question mark is replaced by a \hbox{``\textit{\_query\/}''} suffix. \item[\labelitemi] \textbf{% \textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\ \textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\ (sound*):} \\ Even lighter versions of the `\hbox{?}' encodings. As argument to the \textit{metis} proof method, the `\hbox{??}' suffix is replaced by \hbox{``\textit{\_query\_query\/}''}. \item[\labelitemi] \textbf{% \textit{poly\_guards}@, \textit{poly\_tags}@, \textit{raw\_mono\_guards}@, \\ \textit{raw\_mono\_tags}@ (sound*):} \\ Alternative versions of the `\hbox{??}' encodings. As argument to the \textit{metis} proof method, the `\hbox{@}' suffix is replaced by \hbox{``\textit{\_at\/}''}. \item[\labelitemi] \textbf{\textit{poly\_args}?, \textit{raw\_mono\_args}? (unsound):} \\ Lighter versions of \textit{poly\_args} and \textit{raw\_mono\_args}. \item[\labelitemi] \textbf{\textit{smart}:} The actual encoding used depends on the ATP and should be the most efficient sound encoding for that ATP. \end{enum} For SMT solvers, the type encoding is always \textit{mono\_native}, irrespective of the value of this option. \nopagebreak {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter}) and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).} \opfalse{strict}{non\_strict} Specifies whether Sledgehammer should run in its strict mode. In that mode, sound type encodings marked with an asterisk (*) above are made complete for reconstruction with \textit{metis}, at the cost of some clutter in the generated problems. This option has no effect if \textit{type\_enc} is deliberately set to an unsound encoding. \end{enum} \subsection{Output Format} \label{output-format} \begin{enum} \opfalse{verbose}{quiet} Specifies whether the \textbf{sledgehammer} command should explain what it does. \opfalse{debug}{no\_debug} Specifies whether Sledgehammer should display additional debugging information beyond what \textit{verbose} already displays. Enabling \textit{debug} also enables \textit{verbose} behind the scenes. \nopagebreak {\small See also \textit{spy} (\S\ref{mode-of-operation}) and \textit{overlord} (\S\ref{mode-of-operation}).} \opsmart{isar\_proofs}{no\_isar\_proofs} Specifies whether Isar proofs should be output in addition to one-line proofs. The construction of Isar proof is still experimental and may sometimes fail; however, when they succeed they are usually faster and more intelligible than one-line proofs. If the option is set to \textit{smart} (the default), Isar proofs are only generated when no working one-line proof is available. \opdefault{compress}{int}{smart} Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs} is explicitly enabled. A value of $n$ indicates that each Isar proof step should correspond to a group of up to $n$ consecutive proof steps in the ATP proof. If the option is set to \textit{smart} (the default), the compression factor is 10 if the \textit{isar\_proofs} option is explicitly enabled; otherwise, it is $\infty$. \optrueonly{dont\_compress} Alias for ``\textit{compress} = 1''. \optrue{try0}{dont\_try0} Specifies whether standard proof methods such as \textit{auto} and \textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs. The collection of methods is roughly the same as for the \textbf{try0} command. \optrue{smt\_proofs}{no\_smt\_proofs} Specifies whether the \textit{smt} proof method should be tried in addition to Isabelle's built-in proof methods. \end{enum} \subsection{Regression Testing} \label{regression-testing} \begin{enum} \opnodefault{expect}{string} Specifies the expected outcome, which must be one of the following: \begin{enum} \item[\labelitemi] \textbf{\textit{some}:} Sledgehammer found a proof. \item[\labelitemi] \textbf{\textit{none}:} Sledgehammer found no proof. \item[\labelitemi] \textbf{\textit{timeout}:} Sledgehammer timed out. \item[\labelitemi] \textbf{\textit{unknown}:} Sledgehammer encountered some problem. \end{enum} Sledgehammer emits an error if the actual outcome differs from the expected outcome. This option is useful for regression testing. \nopagebreak {\small See also \textit{timeout} (\S\ref{timeouts}).} \end{enum} \subsection{Timeouts} \label{timeouts} \begin{enum} \opdefault{timeout}{float}{\upshape 30} Specifies the maximum number of seconds that the automatic provers should spend searching for a proof. This excludes problem preparation and is a soft limit. \opdefault{preplay\_timeout}{float}{\upshape 1} Specifies the maximum number of seconds that \textit{metis} or other proof methods should spend trying to ``preplay'' the found proof. If this option is set to 0, no preplaying takes place, and no timing information is displayed next to the suggested proof method calls. \nopagebreak {\small See also \textit{minimize} (\S\ref{mode-of-operation}).} \optrueonly{dont\_preplay} Alias for ``\textit{preplay\_timeout} = 0''. \end{enum} \section{Mirabelle Testing Tool} \label{mirabelle} The \texttt{isabelle mirabelle} tool executes Sledgehammer or other advisory tools (e.g., Nitpick) or tactics (e.g., \textit{auto}) on all subgoals emering in a theory. It is typically used to measure the success rate of a proof tool on some benchmark. Its command-line usage is as follows: {\small \begin{verbatim} isabelle mirabelle [OPTIONS] ACTIONS FILES Options are: -L LOGIC parent logic to use (default HOL) -O DIR output directory for test data (default None) -S FILE user-provided setup file (no actions required) -T THEORY parent theory to use (default Main) -d DIR include session directory -q be quiet (suppress output of Isabelle process) -t TIMEOUT timeout for each action in seconds (default 30) Apply the given actions at all proof steps in the given theory files. \end{verbatim} } Option \texttt{-L LOGIC} specifies the parent session to use. This is often a logic (e.g., \texttt{Pure}, \texttt{HOL}) but may be any session (e.g., from the AFP). Using multiple sessions is not supported. If a theory A needs to import theories from multiple sessions, this limitation can be overcome as follows: \begin{enumerate} \item Define a custom session \texttt{S} with a single theory \texttt{B}. \item Move all imports from \texttt{A} to \texttt{B}. \item Build the heap image of \texttt{S}. \item Import \texttt{S.B} from theory \texttt{A}. \item Execute Mirabelle with \texttt{C} as parent logic (i.e., with \texttt{-L S}). \end{enumerate} Option \texttt{-O DIR} specifies the output directory, which is created if needed. In this directory, one log file per theory records the position of each tested subgoal and the result of executing the action. Option \texttt{-t TIMEOUT} specifies a generic timeout that the actions may interpret differently. More specific documentation about the \texttt{ACTIONS} and \texttt{FILES} parameters and their corresponding options can be found in the Isabelle tool usage by entering \texttt{isabelle mirabelle -?} on the command line. \subsection{Example of Benchmarking Sledgehammer} \begin{verbatim} isabelle mirabelle -O output/ \ sledgehammer[prover=e,prover_timeout=10] Huffman.thy \end{verbatim} -This command specifies Sledgehammer as the action, using E as the prover with a +This command specifies Sledgehammer as the action, using the E prover with a timeout of 10 seconds. The results are written to \texttt{output/Huffman.log}. \subsection{Example of Benchmarking Another Tool} \begin{verbatim} isabelle mirabelle -O output/ -t 10 try0 Huffman.thy \end{verbatim} This command specifies the \textbf{try0} command as the action, with a timeout of 10 seconds. The results are written to \texttt{output/Huffman.log}. \subsection{Example of Generating TPTP Files} \begin{verbatim} isabelle mirabelle -O output/ \ sledgehammer[prover=e,prover_timeout=1,keep=/tptp/files/] \ Huffman.thy \end{verbatim} This command generates TPTP files using Sledgehammer. Since the file is generated at the very beginning of every Sledgehammer invocation, a timeout of one second making the prover fail faster speeds up processing the theory. The results are written in the specified directory (\texttt{/tptp/files/}), which must exist beforehand. A TPTP file is generated for each subgoal. \let\em=\sl \bibliography{manual}{} \bibliographystyle{abbrv} \end{document} diff --git a/src/Doc/manual.bib b/src/Doc/manual.bib --- a/src/Doc/manual.bib +++ b/src/Doc/manual.bib @@ -1,2513 +1,2565 @@ % BibTeX database for the Isabelle documentation %publishers @string{AP="Academic Press"} @string{CUP="Cambridge University Press"} @string{IEEE="IEEE Computer Society Press"} @string{LNCS="Lecture Notes in Computer Science"} @string{MIT="MIT Press"} @string{NH="North-Holland"} @string{Prentice="Prentice-Hall"} @string{PH="Prentice-Hall"} @string{Springer="Springer-Verlag"} %institutions @string{CUCL="Computer Laboratory, University of Cambridge"} @string{Edinburgh="Department of Computer Science, University of Edinburgh"} @string{TUM="Department of Informatics, Technical University of Munich"} %journals @string{AI="Artificial Intelligence"} @string{FAC="Formal Aspects of Computing"} @string{JAR="Journal of Automated Reasoning"} @string{JCS="Journal of Computer Security"} @string{JFP="Journal of Functional Programming"} @string{JLC="Journal of Logic and Computation"} @string{JLP="Journal of Logic Programming"} @string{JSC="Journal of Symbolic Computation"} @string{JSL="Journal of Symbolic Logic"} @string{PROYAL="Proceedings of the Royal Society of London"} @string{SIGPLAN="{SIGPLAN} Notices"} @string{TISSEC="ACM Transactions on Information and System Security"} %conferences @string{CADE="International Conference on Automated Deduction"} @string{POPL="Symposium on Principles of Programming Languages"} @string{TYPES="Types for Proofs and Programs"} %A @incollection{abramsky90, author = {Samson Abramsky}, title = {The Lazy Lambda Calculus}, pages = {65-116}, editor = {David A. Turner}, booktitle = {Research Topics in Functional Programming}, publisher = {Addison-Wesley}, year = 1990} @Unpublished{abrial93, author = {J. R. Abrial and G. Laffitte}, title = {Towards the Mechanization of the Proofs of Some Classical Theorems of Set Theory}, note = {preprint}, year = 1993, month = Feb} @incollection{aczel77, author = {Peter Aczel}, title = {An Introduction to Inductive Definitions}, pages = {739-782}, crossref = {barwise-handbk}} @Book{aczel88, author = {Peter Aczel}, title = {Non-Well-Founded Sets}, publisher = {CSLI}, year = 1988} @inproceedings{Aehlig-Haftmann-Nipkow:2008:nbe, author = {Klaus Aehlig and Florian Haftmann and Tobias Nipkow}, title = {A Compiled Implementation of Normalization by Evaluation}, booktitle = {TPHOLs '08: Proceedings of the 21th International Conference on Theorem Proving in Higher Order Logics}, year = {2008}, isbn = {978-3-540-71065-3}, pages = {352--367}, publisher = Springer, series = LNCS, volume = {5170}, editor = {Otmane A\"{\i}t Mohamed and C{\'e}sar Mu{\~n}oz and Sofi{\`e}ne Tahar} } @InProceedings{alf, author = {Lena Magnusson and Bengt {Nordstr\"{o}m}}, title = {The {ALF} Proof Editor and Its Proof Engine}, crossref = {types93}, pages = {213-237}} @inproceedings{andersson-1993, author = "Arne Andersson", title = "Balanced Search Trees Made Simple", editor = "F. K. H. A. Dehne and N. Santoro and S. Whitesides", booktitle = "WADS 1993", series = LNCS, volume = {709}, pages = "61--70", year = 1993, publisher = Springer} @book{andrews86, author = "Peter Andrews", title = "An Introduction to Mathematical Logic and Type Theory: to Truth through Proof", publisher = AP, series = "Computer Science and Applied Mathematics", year = 1986} @InProceedings{Aspinall:2000:eProof, author = {David Aspinall}, title = {Protocols for Interactive {e-Proof}}, booktitle = {Theorem Proving in Higher Order Logics (TPHOLs)}, year = 2000, note = {Unpublished work-in-progress paper, \url{http://homepages.inf.ed.ac.uk/da/papers/drafts/eproof.ps.gz}} } @InProceedings{Aspinall:TACAS:2000, author = {David Aspinall}, title = {{P}roof {G}eneral: A Generic Tool for Proof Development}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, year = 2000, publisher = Springer, series = LNCS, volume = 1785, pages = "38--42" } @Misc{isamode, author = {David Aspinall}, title = {Isamode --- {U}sing {I}sabelle with {E}macs}, note = {\url{http://homepages.inf.ed.ac.uk/da/Isamode/}} } @Misc{proofgeneral, author = {David Aspinall}, title = {{P}roof {G}eneral}, note = {\url{http://proofgeneral.inf.ed.ac.uk/}} } %B @inproceedings{backes-brown-2010, title = "Analytic Tableaux for Higher-Order Logic with Choice", author = "Julian Backes and Chad E. Brown", booktitle={Automated Reasoning: IJCAR 2010}, editor={J. Giesl and R. H\"ahnle}, publisher = Springer, series = LNCS, volume = 6173, pages = "76--90", year = 2010} @book{Baader-Nipkow,author={Franz Baader and Tobias Nipkow}, title="Term Rewriting and All That",publisher=CUP,year=1998} @manual{isabelle-locale, author = {Clemens Ballarin}, title = {Tutorial to Locales and Locale Interpretation}, institution = TUM, note = {\url{https://isabelle.in.tum.de/doc/locales.pdf}} } @article{Ballarin2014, author = {Ballarin, Clemens}, journal = JAR, publisher = Springer, title = {Locales: A Module System for Mathematical Theories}, volume = 52, number = 2, pages = {123--153}, url = {https://doi.org/10.1007/s10817-013-9284-7}, year = {2014}} @InCollection{Barendregt-Geuvers:2001, author = {H. Barendregt and H. Geuvers}, title = {Proof Assistants using Dependent Type Systems}, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier}, year = 2001, editor = {A. Robinson and A. Voronkov} } @inproceedings{cvc3, author = {Clark Barrett and Cesare Tinelli}, title = {{CVC3}}, booktitle = {CAV}, editor = {Werner Damm and Holger Hermanns}, volume = {4590}, series = LNCS, pages = {298--302}, publisher = {Springer}, year = {2007} } @inproceedings{cvc4, author = {Clark Barrett and Christopher L. Conway and Morgan Deters and Liana Hadarean and Dejan Jovanovic and Tim King and Andrew Reynolds and Cesare Tinelli}, title = {{CVC4}}, booktitle = {CAV 2011}, pages = {171--177}, editor = {Ganesh Gopalakrishnan and Shaz Qadeer}, publisher = {Springer}, series = LNCS, volume = {6806}, year = {2011} } @incollection{basin91, author = {David Basin and Matt Kaufmann}, title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental Comparison}, crossref = {huet-plotkin91}, pages = {89-119}} @Unpublished{HOL-Library, author = {Gertrud Bauer and Tobias Nipkow and Oheimb, David von and Lawrence C Paulson and Thomas M Rasmussen and Christophe Tabacznyj and Markus Wenzel}, title = {The Supplemental {Isabelle/HOL} Library}, note = {Part of the Isabelle distribution, \url{https://isabelle.in.tum.de/library/HOL/Library/document.pdf}}, year = 2002 } @InProceedings{Bauer-Wenzel:2000:HB, author = {Gertrud Bauer and Markus Wenzel}, title = {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in {I}sabelle/{I}sar}, booktitle = {Types for Proofs and Programs: TYPES'99}, editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m and Jan Smith}, series = {LNCS}, year = 2000 } @InProceedings{Bauer-Wenzel:2001, author = {Gertrud Bauer and Markus Wenzel}, title = {Calculational reasoning revisited --- an {Isabelle/Isar} experience}, crossref = {tphols2001}} @inproceedings{leo2, author = "Christoph Benzm{\"u}ller and Lawrence C. Paulson and Frank Theiss and Arnaud Fietzke", title = "{LEO-II}---A Cooperative Automatic Theorem Prover for Higher-Order Logic", editor = "Alessandro Armando and Peter Baumgartner and Gilles Dowek", booktitle = "Automated Reasoning: IJCAR 2008", publisher = Springer, series = LNCS, volume = 5195, pages = "162--170", year = 2008} @inProceedings{Berghofer-Bulwahn-Haftmann:2009:TPHOL, author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian}, booktitle = {Theorem Proving in Higher Order Logics}, pages = {131--146}, title = {Turning Inductive into Equational Specifications}, year = {2009} } @INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL, crossref = "tphols2000", title = "Proof terms for simply typed higher order logic", author = "Stefan Berghofer and Tobias Nipkow", pages = "38--52"} @inproceedings{berghofer-nipkow-2004, author = {Stefan Berghofer and Tobias Nipkow}, title = {Random Testing in {I}sabelle/{HOL}}, pages = {230--239}, editor = "J. Cuellar and Z. Liu", booktitle = {{SEFM} 2004}, publisher = IEEE, year = 2004} @InProceedings{Berghofer-Nipkow:2002, author = {Stefan Berghofer and Tobias Nipkow}, title = {Executing Higher Order Logic}, booktitle = {Types for Proofs and Programs: TYPES'2000}, editor = {P. Callaghan and Z. Luo and J. McKinna and R. Pollack}, series = LNCS, publisher = Springer, volume = 2277, year = 2002} @InProceedings{Berghofer-Wenzel:1999:TPHOL, author = {Stefan Berghofer and Markus Wenzel}, title = {Inductive datatypes in {HOL} --- lessons learned in {F}ormal-{L}ogic {E}ngineering}, crossref = {tphols99}} @InProceedings{Bezem-Coquand:2005, author = {M.A. Bezem and T. Coquand}, title = {Automating {Coherent Logic}}, booktitle = {LPAR-12}, year = 2005, editor = {G. Sutcliffe and A. Voronkov}, volume = 3835, series = LNCS, publisher = Springer} @manual{isabelle-datatypes, author = {Julian Biendarra and Jasmin Christian Blanchette and Martin Desharnais and Lorenz Panny and Andrei Popescu and Dmitriy Traytel}, title = {Defining (Co)datatypes and Primitively (Co)recursive Functions in {Isabelle\slash HOL}}, institution = {TU Munich}, note = {\url{https://isabelle.in.tum.de/doc/datatypes.pdf}}} @book{Bird-Wadler,author="Richard Bird and Philip Wadler", title="Introduction to Functional Programming",publisher=PH,year=1988} @book{Bird-Haskell,author="Richard Bird", title="Introduction to Functional Programming using Haskell", publisher=PH,year=1998} @manual{isabelle-nitpick, author = {Jasmin Christian Blanchette}, title = {Picking Nits: A User's Guide to {N}itpick for {I}sabelle\slash {HOL}}, institution = TUM, note = {\url{https://isabelle.in.tum.de/doc/nitpick.pdf}} } @manual{isabelle-sledgehammer, author = {Jasmin Christian Blanchette}, title = {Hammering Away: A User's Guide to {S}ledgehammer for {I}sabelle\slash {HOL}}, institution = TUM, note = {\url{https://isabelle.in.tum.de/doc/sledgehammer.pdf}} } @manual{isabelle-corec, author = {Jasmin Christian Blanchette and Andreas Lochbihler and Andrei Popescu and Dmitriy Traytel}, title = {Defining Nonprimitively Corecursive Functions in {Isabelle\slash HOL}}, institution = {TU Munich}, note = {\url{https://isabelle.in.tum.de/doc/corec.pdf}}} @inproceedings{blanchette-nipkow-2010, title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder", author = "Jasmin Christian Blanchette and Tobias Nipkow", crossref = {itp2010}} @inproceedings{blanchette-et-al-2015-wit, author = {Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel}, title = {Witnessing (Co)datatypes}, booktitle = {24th European Symposium on Programming, {ESOP} 2015}, pages = {359--382}, year = {2015}, editor = {Jan Vitek}, series = {LNCS}, volume = {9032}, publisher = {Springer} } @inproceedings{blanchette-et-al-2015-fouco, author = {Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel}, title = {Foundational extensible corecursion: A proof assistant perspective}, booktitle = {20th {ACM} {SIGPLAN} International Conference on Functional Programming, {ICFP} 2015}, pages = {192--204}, year = {2015}, editor = {Kathleen Fisher and John H. Reppy}, publisher = {{ACM}}, } @misc{blanchette-et-al-201x-amico, author = {Jasmin Christian Blanchette and Aymeric Bouzy and Andreas Lochbihler and Andrei Popescu and Dmitriy Traytel}, title = {Friends with benefits: Implementing corecursion in foundational proof assistants}, howpublished = "\url{http://www21.in.tum.de/~blanchet/amico.pdf}", year = 2016} @inproceedings{blanchette-et-al-2014-impl, author = "Jasmin Christian Blanchette and Johannes H{\"o}lzl and Andreas Lochbihler and Lorenz Panny and Andrei Popescu and Dmitriy Traytel", title = "Truly Modular (Co)datatypes for {I}sabelle/{HOL}", year = 2014, publisher = "Springer", editor = "Gerwin Klein and Ruben Gamboa", booktitle = {5th International Conference on Interactive Theorem Proving, ITP 2014}, series = LNCS, volume = 8558, pages = "93--110" } @inproceedings{why3, author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich}, title = {{Why3}: Shepherd Your Herd of Provers}, editor = "K. Rustan M. Leino and Micha\l{} Moskal", booktitle = {Boogie 2011}, pages = "53--64", year = 2011 } @inproceedings{alt-ergo, author = {Fran\c{c}ois Bobot and Sylvain Conchon and Evelyne Contejean and St\'ephane Lescuyer}, title = {Implementing Polymorphism in {SMT} Solvers}, booktitle = {SMT '08}, pages = "1--5", publisher = "ACM", series = "ICPS", year = 2008, editor = {Clark Barrett and Leonardo de Moura}} % /BPR % and Domagoj Babic and Amit Goel @inproceedings{boehme-nipkow-2010, author={Sascha B\"ohme and Tobias Nipkow}, title={Sledgehammer: Judgement Day}, booktitle={Automated Reasoning: IJCAR 2010}, editor={J. Giesl and R. H\"ahnle}, publisher=Springer, series=LNCS, volume = 6173, pages = "107--121", year=2010} @inproceedings{bouton-et-al-2009, author = {Thomas Bouton and Diego Caminha B. de Oliveira and David D{\'{e}}harbe and Pascal Fontaine}, title = {{veriT}: An Open, Trustable and Efficient {SMT}-Solver}, year = {2009}, pages = {151--156}, editor = {Renate A. Schmidt}, booktitle = {Automated Deduction --- CADE-22}, series = {Lecture Notes in Computer Science}, volume = {5663}, publisher = {Springer} } @Article{boyer86, author = {Robert Boyer and Ewing Lusk and William McCune and Ross Overbeek and Mark Stickel and Lawrence Wos}, title = {Set Theory in First-Order Logic: Clauses for {G\"{o}del's} Axioms}, journal = JAR, year = 1986, volume = 2, number = 3, pages = {287-327}} @book{bm79, author = {Robert S. Boyer and J Strother Moore}, title = {A Computational Logic}, publisher = {Academic Press}, year = 1979} @book{bm88book, author = {Robert S. Boyer and J Strother Moore}, title = {A Computational Logic Handbook}, publisher = {Academic Press}, year = 1988} @inproceedings{satallax, author = "Chad E. Brown", title = "Reducing Higher-Order Theorem Proving to a Sequence of {SAT} Problems", booktitle = {Automated Deduction --- CADE-23}, publisher = Springer, series = LNCS, volume = 6803, pages = "147--161", editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans", year = 2011} @Article{debruijn72, author = {N. G. de Bruijn}, title = {Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the {Church-Rosser Theorem}}, journal = {Indag. Math.}, volume = 34, pages = {381-392}, year = 1972} @InProceedings{bulwahnKN07, author = {Lukas Bulwahn and Alexander Krauss and Tobias Nipkow}, title = {Finding Lexicographic Orders for Termination Proofs in {Isabelle/HOL}}, crossref = {tphols2007}, pages = {38--53} } @InProceedings{bulwahn-et-al:2008:imperative, author = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erkök and John Matthews}, title = {Imperative Functional Programming with {Isabelle/HOL}}, crossref = {tphols2008}, } % pages = {38--53} @Article{ban89, author = {M. Burrows and M. Abadi and R. M. Needham}, title = {A Logic of Authentication}, journal = PROYAL, year = 1989, volume = 426, pages = {233-271}} %C @PhdThesis{Chaieb-thesis, author = {Amine Chaieb}, title = {Automated methods for formal proofs in simple arithmetics and algebra}, school = {Technische Universit\"at M\"unchen}, year = 2008, note = {\url{http://www4.in.tum.de/~chaieb/pubs/pdf/diss.pdf}}} @InProceedings{Chaieb-Wenzel:2007, author = {Amine Chaieb and Makarius Wenzel}, title = {Context aware Calculation and Deduction --- Ring Equalities via {Gr\"obner Bases} in {Isabelle}}, booktitle = {Towards Mechanized Mathematical Assistants (CALCULEMUS 2007)}, editor = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger}, series = "LNAI", volume = 4573, year = 2007, publisher = Springer } @TechReport{camilleri92, author = {J. Camilleri and T. F. Melham}, title = {Reasoning with Inductively Defined Relations in the {HOL} Theorem Prover}, institution = CUCL, year = 1992, number = 265, month = Aug} @Book{charniak80, author = {E. Charniak and C. K. Riesbeck and D. V. McDermott}, title = {Artificial Intelligence Programming}, publisher = {Lawrence Erlbaum Associates}, year = 1980} @article{church40, author = "Alonzo Church", title = "A Formulation of the Simple Theory of Types", journal = JSL, year = 1940, volume = 5, pages = "56-68"} @book{ClarkeGP-book,author="Edmund Clarke and Orna Grumberg and Doron Peled", title="Model Checking",publisher=MIT,year=1999} @PhdThesis{coen92, author = {Martin D. Coen}, title = {Interactive Program Derivation}, school = {University of Cambridge}, note = {Computer Laboratory Technical Report 272}, month = nov, year = 1992} @book{constable86, author = {R. L. Constable and others}, title = {Implementing Mathematics with the Nuprl Proof Development System}, publisher = Prentice, year = 1986} @inproceedings{cruanes-2014, author = "Simon Cruanes", title = "Logtk: A {Logic ToolKit} for Automated Reasoning, and its Implementation", booktitle = {4th Workshop on Practical Aspects of Automated Reasoning, PAAR@IJCAR 2014, Vienna, Austria, 2014}, year = 2014, note = {Presented at the Practical Aspects of Automated Reasoning (PAAR) workshop}} %D @Book{davey-priestley, author = {B. A. Davey and H. A. Priestley}, title = {Introduction to Lattices and Order}, publisher = CUP, year = 1990} +@inproceedings{de-moura-2008, + author = {Leonardo de Moura and + Nikolaj Bj{\o}rner}, + editor = {C. R. Ramakrishnan and + Jakob Rehof}, + title = {{Z3}: An Efficient {SMT} Solver}, + booktitle = {Tools and Algorithms for the Construction and Analysis of Systems --- TACAS 2008}, + series = {Lecture Notes in Computer Science}, + volume = {4963}, + pages = {337--340}, + publisher = {Springer}, + year = {2008}, + url = {https://doi.org/10.1007/978-3-540-78800-3\_24}, + doi = {10.1007/978-3-540-78800-3\_24}, + timestamp = {Tue, 14 May 2019 10:00:53 +0200}, + biburl = {https://dblp.org/rec/conf/tacas/MouraB08.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + @Book{devlin79, author = {Keith J. Devlin}, title = {Fundamentals of Contemporary Set Theory}, publisher = {Springer}, year = 1979} @inproceedings{di-gianantonio-miculan-2003, author = {Di Gianantonio, Pietro and Marino Miculan}, title = {A Unifying Approach to Recursive and Co-recursive Definitions}, booktitle = {TYPES 2002}, year = {2003}, pages = {148--161}, editor = {Herman Geuvers and Freek Wiedijk}, publisher = {Springer}, series = {LNCS}, volume = {2646} } @book{dummett, author = {Michael Dummett}, title = {Elements of Intuitionism}, year = 1977, publisher = {Oxford University Press}} @misc{yices, author = {Bruno Dutertre and Leonardo de Moura}, title = {The {Yices} {SMT} Solver}, howpublished = "\url{http://yices.csl.sri.com/tool-paper.pdf}", year = 2006} @incollection{dybjer91, author = {Peter Dybjer}, title = {Inductive Sets and Families in {Martin-L{\"o}f's} Type Theory and Their Set-Theoretic Semantics}, crossref = {huet-plotkin91}, pages = {280-306}} @Article{dyckhoff, author = {Roy Dyckhoff}, title = {Contraction-Free Sequent Calculi for Intuitionistic Logic}, journal = JSL, year = 1992, volume = 57, number = 3, pages = {795-807}} %F @Article{IMPS, author = {William M. Farmer and Joshua D. Guttman and F. Javier Thayer}, title = {{IMPS}: An Interactive Mathematical Proof System}, journal = JAR, volume = 11, number = 2, year = 1993, pages = {213-248}} @article{Farmer:2008, author = {William M. Farmer}, title = {The seven virtues of simple type theory}, journal = {J. Applied Logic}, volume = {6}, number = {3}, pages = {267--286}, year = {2008}, url = {https://doi.org/10.1016/j.jal.2007.11.001}, } @inproceedings{felty91a, author = {Amy Felty}, title = {A Logic Program for Transforming Sequent Proofs to Natural Deduction Proofs}, booktitle = {Extensions of Logic Programming, International Workshop, T{\"{u}}bingen, FRG, December 8-10, 1989, Proceedings}, pages = {157--178}, year = {1989}, url = {https://doi.org/10.1007/BFb0038694}, } @Article{fleuriot-jcm, author = {Jacques Fleuriot and Lawrence C. Paulson}, title = {Mechanizing Nonstandard Real Analysis}, journal = {LMS Journal of Computation and Mathematics}, year = 2000, volume = 3, pages = {140-190}, note = {\url{http://www.lms.ac.uk/jcm/3/lms1999-027/}} } @TechReport{frost93, author = {Jacob Frost}, title = {A Case Study of Co-induction in {Isabelle HOL}}, institution = CUCL, number = 308, year = 1993, month = Aug} %revised version of frost93 @TechReport{frost95, author = {Jacob Frost}, title = {A Case Study of Co-induction in {Isabelle}}, institution = CUCL, number = 359, year = 1995, month = Feb} @inproceedings{OBJ, author = {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud and J. Meseguer}, title = {Principles of {OBJ2}}, booktitle = POPL, year = 1985, pages = {52-66}} %G @book{gallier86, author = {J. H. Gallier}, title = {Logic for Computer Science: Foundations of Automatic Theorem Proving}, year = 1986, publisher = {Harper \& Row}} @Book{galton90, author = {Antony Galton}, title = {Logic for Information Technology}, publisher = {Wiley}, year = 1990} @Article{Gentzen:1935, author = {G. Gentzen}, title = {Untersuchungen {\"u}ber das logische {S}chlie{\ss}en}, journal = {Math. Zeitschrift}, year = 1935 } @InProceedings{gimenez-codifying, author = {Eduardo Gim{\'e}nez}, title = {Codifying Guarded Definitions with Recursive Schemes}, crossref = {types94}, pages = {39-59} } @book{girard89, author = {Jean-Yves Girard}, title = {Proofs and Types}, year = 1989, publisher = CUP, note = {Translated by Yves Lafont and Paul Taylor}} @TechReport{Gordon:1985:HOL, author = {M. J. C. Gordon}, title = {{HOL}: A machine oriented formulation of higher order logic}, institution = {University of Cambridge Computer Laboratory}, year = 1985, number = 68 } @Book{mgordon-hol, editor = {M. J. C. Gordon and T. F. Melham}, title = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic}, publisher = CUP, year = 1993} @book{mgordon79, author = {Michael J. C. Gordon and Robin Milner and Christopher P. Wadsworth}, title = {Edinburgh {LCF}: A Mechanised Logic of Computation}, year = 1979, publisher = {Springer}, series = LNCS, volume = 78} @inproceedings{Gunter-HOL92,author={Elsa L. Gunter}, title={Why we can't have {SML} style datatype declarations in {HOL}}, booktitle={Higher Order Logic Theorem Proving and its Applications: Proc.\ IFIP TC10/WG10.2 Intl. Workshop, 1992}, editor={L.J.M. Claesen and M.J.C. Gordon}, publisher=NH,year=1993,pages={561--568}} @InProceedings{gunter-trees, author = {Elsa L. Gunter}, title = {A Broader Class of Trees for Recursive Type Definitions for {HOL}}, crossref = {hug93}, pages = {141-154}} %H @inproceedings{Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement, author = {Florian Haftmann and Alexander Krauss and Ond\v{r}ej Kun\v{c}ar and Tobias Nipkow}, title = {Data Refinement in {Isabelle/HOL}}, booktitle = {Interactive Theorem Proving (ITP 2013)}, pages = {100-115}, year = 2013, publisher = Springer, series = {Lecture Notes in Computer Science}, volume = {7998}, editor = {S. Blazy and C. Paulin-Mohring and D. Pichardie} } @inproceedings{Haftmann-Nipkow:2010:code, author = {Florian Haftmann and Tobias Nipkow}, title = {Code Generation via Higher-Order Rewrite Systems}, booktitle = {Functional and Logic Programming: 10th International Symposium: FLOPS 2010}, year = 2010, publisher = Springer, series = LNCS, editor = {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal}, volume = 6009 } @InProceedings{Haftmann-Wenzel:2006:classes, author = {Florian Haftmann and Makarius Wenzel}, title = {Constructive Type Classes in {Isabelle}}, editor = {T. Altenkirch and C. McBride}, booktitle = {Types for Proofs and Programs, TYPES 2006}, publisher = {Springer}, series = {LNCS}, volume = {4502}, year = {2007} } @InProceedings{Haftmann-Wenzel:2009, author = {Florian Haftmann and Makarius Wenzel}, title = {Local theory specifications in {Isabelle/Isar}}, editor = {Stefano Berardi and Ferruccio Damiani and de Liguoro, Ugo}, booktitle = {Types for Proofs and Programs, TYPES 2008}, publisher = {Springer}, series = {LNCS}, volume = {5497}, year = {2009} } @inproceedings{hindleymilner, author = {L. Damas and H. Milner}, title = {Principal type schemes for functional programs}, booktitle = {ACM Symp. Principles of Programming Languages}, year = 1982 } @manual{isabelle-classes, author = {Florian Haftmann}, title = {Haskell-style type classes with {Isabelle}/{Isar}}, institution = TUM, note = {\url{https://isabelle.in.tum.de/doc/classes.pdf}} } @manual{isabelle-codegen, author = {Florian Haftmann}, title = {Code generation from Isabelle theories}, institution = TUM, note = {\url{https://isabelle.in.tum.de/doc/codegen.pdf}} } @Book{halmos60, author = {Paul R. Halmos}, title = {Naive Set Theory}, publisher = {Van Nostrand}, year = 1960} @book{HarelKT-DL,author={David Harel and Dexter Kozen and Jerzy Tiuryn}, title={Dynamic Logic},publisher=MIT,year=2000} @Book{hennessy90, author = {Matthew Hennessy}, title = {The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics}, publisher = {Wiley}, year = 1990} @article{waldmeister, author = {Thomas Hillenbrand and Arnim Buch and Rolan Vogt and Bernd L\"ochner}, title = "Waldmeister: High-Performance Equational Deduction", journal = JAR, volume = 18, number = 2, pages = {265--270}, year = 1997} @article{hinze10, author = {Hinze, Ralf}, title = {Concrete stream calculus---{A}n extended study}, journal = {J. Funct. Program.}, volume = {20}, issue = {Special Issue 5-6}, year = {2010}, issn = {1469-7653}, pages = {463--535} } @inproceedings{sine, author = "Kry\v{s}tof Hoder and Andrei Voronkov", title = "Sine Qua Non for Large Theory Reasoning", booktitle = {Automated Deduction --- CADE-23}, publisher = Springer, series = LNCS, volume = 6803, pages = "299--314", editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans", year = 2011} @book{HopcroftUllman,author={John E. Hopcroft and Jeffrey D. Ullman}, title={Introduction to Automata Theory, Languages, and Computation.}, publisher={Addison-Wesley},year=1979} @Article{haskell-report, author = {Paul Hudak and Simon Peyton Jones and Philip Wadler}, title = {Report on the Programming Language {Haskell}: A Non-strict, Purely Functional Language}, journal = SIGPLAN, year = 1992, volume = 27, number = 5, month = May, note = {Version 1.2}} @Article{haskell-tutorial, author = {Paul Hudak and Joseph H. Fasel}, title = {A Gentle Introduction to {Haskell}}, journal = SIGPLAN, year = 1992, volume = 27, number = 5, month = May} @inproceedings{Hoelzl-Huffman-Immler:2013:typeclasses, author = {Johannes H{\"o}lzl and Fabian Immler and Brian Huffman}, title = {Type Classes and Filters for Mathematical Analysis in {Isabelle/HOL}}, booktitle = {Interactive Theorem Proving (ITP 2013)}, editor = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David}, year = 2013, volume = 7998, series = LNCS, publisher = Springer, isbn = {978-3-642-39633-5}, pages = {279--294}} @book{Hudak-Haskell,author={Paul Hudak}, title={The Haskell School of Expression},publisher=CUP,year=2000} @article{huet75, author = {G. P. Huet}, title = {A Unification Algorithm for Typed $\lambda$-Calculus}, journal = TCS, volume = 1, year = 1975, pages = {27-57}} @article{huet78, author = {G. P. Huet and B. Lang}, title = {Proving and Applying Program Transformations Expressed with Second-Order Patterns}, journal = acta, volume = 11, year = 1978, pages = {31-55}} @inproceedings{huet88, author = {G{\'e}rard Huet}, title = {Induction Principles Formalized in the {Calculus of Constructions}}, booktitle = {Programming of Future Generation Computers}, editor = {K. Fuchi and M. Nivat}, year = 1988, pages = {205-216}, publisher = {Elsevier}} @inproceedings{Huffman-Kuncar:2013:lifting_transfer, author = {Brian Huffman and Ond\v{r}ej Kun\v{c}ar}, title = {{Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL}}, booktitle = {Certified Programs and Proofs (CPP 2013)}, year = 2013, publisher = Springer, series = {Lecture Notes in Computer Science}, volume = {8307}, } @Book{Huth-Ryan-book, author = {Michael Huth and Mark Ryan}, title = {Logic in Computer Science. Modelling and reasoning about systems}, publisher = CUP, year = 2000} @InProceedings{Harrison:1996:MizarHOL, author = {J. Harrison}, title = {A {Mizar} Mode for {HOL}}, pages = {203--220}, crossref = {tphols96}} @misc{metis, author = "Joe Hurd", title = "Metis Theorem Prover", note = "\url{http://www.gilith.com/software/metis/}"} %J @article{haskell-revised-report, author = {Simon {Peyton Jones} and others}, title = {The {Haskell} 98 Language and Libraries: The Revised Report}, journal = {Journal of Functional Programming}, volume = 13, number = 1, pages = {0--255}, month = {Jan}, year = 2003, note = {\url{http://www.haskell.org/definition/}}} @book{jackson-2006, author = "Daniel Jackson", title = "Software Abstractions: Logic, Language, and Analysis", publisher = MIT, year = 2006} %K @InProceedings{kammueller-locales, author = {Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson}, title = {Locales: A Sectioning Concept for {Isabelle}}, crossref = {tphols99}} @book{Knuth3-75, author={Donald E. Knuth}, title={The Art of Computer Programming, Volume 3: Sorting and Searching}, publisher={Addison-Wesley}, year=1975} @Article{korf85, author = {R. E. Korf}, title = {Depth-First Iterative-Deepening: an Optimal Admissible Tree Search}, journal = AI, year = 1985, volume = 27, pages = {97-109}} @inproceedings{korovin-2009, title = "Instantiation-Based Automated Reasoning: From Theory to Practice", author = "Konstantin Korovin", editor = "Renate A. Schmidt", booktitle = {Automated Deduction --- CADE-22}, series = "LNAI", volume = {5663}, pages = "163--166", year = 2009, publisher = "Springer"} @inproceedings{korovin-sticksel-2010, author = {Konstantin Korovin and Christoph Sticksel}, title = {{iP}rover-{E}q: An Instantiation-Based Theorem Prover with Equality}, pages = {196--202}, booktitle={Automated Reasoning: IJCAR 2010}, editor={J. Giesl and R. H\"ahnle}, publisher = Springer, series = LNCS, volume = 6173, year = 2010} @InProceedings{krauss2006, author = {Alexander Krauss}, title = {Partial Recursive Functions in {Higher-Order Logic}}, crossref = {ijcar2006}, pages = {589--603}} @PhdThesis{krauss_phd, author = {Alexander Krauss}, title = {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic}, school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen}, year = {2009}, address = {Germany} } @manual{isabelle-function, author = {Alexander Krauss}, title = {Defining Recursive Functions in {Isabelle/HOL}}, institution = TUM, note = {\url{https://isabelle.in.tum.de/doc/functions.pdf}} } @inproceedings{Kuncar:2015, author = {Ondrej Kuncar}, title = {Correctness of {Isabelle's} Cyclicity Checker: Implementability of Overloading in Proof Assistants}, booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs, {CPP} 2015, Mumbai, India, January 15-17, 2015}, year = {2015}, url = {http://doi.acm.org/10.1145/2676724.2693175}, doi = {10.1145/2676724.2693175}, } @inproceedings{Kuncar-Popescu:2015, author = {Ondrej Kuncar and Andrei Popescu}, title = {A Consistent Foundation for {Isabelle/HOL}}, editor = {Christian Urban and Xingyuan Zhang}, booktitle = {Interactive Theorem Proving - 6th International Conference, {ITP} 2015, Nanjing, China, August 24-27, 2015, Proceedings}, year = {2015}, url = {https://doi.org/10.1007/978-3-319-22102-1_16}, series = {Lecture Notes in Computer Science}, volume = {9236}, publisher = {Springer}, } @Book{kunen80, author = {Kenneth Kunen}, title = {Set Theory: An Introduction to Independence Proofs}, publisher = NH, year = 1980} %L @manual{OCaml, author = {Xavier Leroy and others}, title = {The Objective Caml system -- Documentation and user's manual}, note = {\url{http://caml.inria.fr/pub/docs/manual-ocaml/}}} -@misc{agsyHOL, - author = "Fredrik Lindblad", - title = "{agsyHOL}", - note = "\url{https://github.com/frelindb/agsyHOL}"} +@inproceedings{agsyHOL, + author = {Fredrik Lindblad}, + editor = {St{\'{e}}phane Demri and + Deepak Kapur and + Christoph Weidenbach}, + title = {A Focused Sequent Calculus for Higher-Order Logic}, + booktitle = {Automated Reasoning --- IJCAR 2014}, + series = {Lecture Notes in Computer Science}, + volume = {8562}, + pages = {61--75}, + publisher = {Springer}, + year = {2014}, + url = {https://doi.org/10.1007/978-3-319-08587-6\_5}, + doi = {10.1007/978-3-319-08587-6\_5}, + timestamp = {Tue, 14 May 2019 10:00:39 +0200}, + biburl = {https://dblp.org/rec/conf/cade/Lindblad14.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org}} @incollection{lochbihler-2010, title = "Coinductive", author = "Andreas Lochbihler", booktitle = "The Archive of Formal Proofs", editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson", publisher = "\url{https://isa-afp.org/entries/Coinductive.shtml}", month = "Feb.", year = 2010} @inproceedings{lochbihler-hoelzl-2014, author = {Andreas Lochbihler and Johannes H{\"{o}}lzl}, title = {Recursive Functions on Lazy Lists via Domains and Topologies}, booktitle = {Interactive Theorem Proving --- 5th International Conference, {ITP} 2014}, pages = {341--357}, year = {2014}, editor = {Gerwin Klein and Ruben Gamboa}, series = LNCS, volume = {8558}, publisher = {Springer}, } @book{loveland-78, author = "D. W. Loveland", title = "Automated Theorem Proving: A Logical Basis", year = 1978, publisher = "North-Holland Publishing Co."} @InProceedings{lowe-fdr, author = {Gavin Lowe}, title = {Breaking and Fixing the {Needham}-{Schroeder} Public-Key Protocol using {CSP} and {FDR}}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems: second international workshop, TACAS '96}, editor = {T. Margaria and B. Steffen}, series = {LNCS 1055}, year = 1996, publisher = {Springer}, pages = {147-166}} %M @Article{mw81, author = {Zohar Manna and Richard Waldinger}, title = {Deductive Synthesis of the Unification Algorithm}, journal = SCP, year = 1981, volume = 1, number = 1, pages = {5-48}} @InProceedings{martin-nipkow, author = {Ursula Martin and Tobias Nipkow}, title = {Ordered Rewriting and Confluence}, crossref = {cade10}, pages = {366-380}} @book{martinlof84, author = {Per Martin-L{\"o}f}, title = {Intuitionistic type theory}, year = 1984, publisher = {Bibliopolis}} @inproceedings{Matichuk-et-al:2014, author = {Daniel Matichuk and Makarius Wenzel and Toby C. Murray}, title = {An {Isabelle} Proof Method Language}, editor = {Gerwin Klein and Ruben Gamboa}, booktitle = {Interactive Theorem Proving - 5th International Conference, {ITP} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria}, year = {2014}, url = {https://doi.org/10.1007/978-3-319-08970-6_25}, doi = {10.1007/978-3-319-08970-6_25}, series = "LNCS", volume = {8558}, publisher = {Springer}, } @incollection{melham89, author = {Thomas F. Melham}, title = {Automating Recursive Type Definitions in Higher Order Logic}, pages = {341-386}, crossref = {birtwistle89}} @Article{Miller:1991, author = {Dale Miller}, title = {A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification}, journal = {Journal of Logic and Computation}, year = 1991, volume = 1, number = 4 } @Article{miller-mixed, Author = {Dale Miller}, Title = {Unification Under a Mixed Prefix}, journal = JSC, volume = 14, number = 4, pages = {321-358}, Year = 1992} @Article{milner78, author = {Robin Milner}, title = {A Theory of Type Polymorphism in Programming}, journal = "J. Comp.\ Sys.\ Sci.", year = 1978, volume = 17, pages = {348-375}} @TechReport{milner-ind, author = {Robin Milner}, title = {How to Derive Inductions in {LCF}}, institution = Edinburgh, year = 1980, type = {note}} @Article{milner-coind, author = {Robin Milner and Mads Tofte}, title = {Co-induction in Relational Semantics}, journal = TCS, year = 1991, volume = 87, pages = {209-220}} @Book{milner89, author = {Robin Milner}, title = {Communication and Concurrency}, publisher = Prentice, year = 1989} @book{SML,author="Robin Milner and Mads Tofte and Robert Harper", title="The Definition of Standard ML",publisher=MIT,year=1990} @PhdThesis{monahan84, author = {Brian Q. Monahan}, title = {Data Type Proofs using Edinburgh {LCF}}, school = {University of Edinburgh}, year = 1984} @article{MuellerNvOS99, author= {Olaf M{\"u}ller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch}, title={{HOLCF = HOL + LCF}},journal=JFP,year=1999,volume=9,pages={191--223}} @Manual{Muzalewski:Mizar, title = {An Outline of {PC} {Mizar}}, author = {Micha{\l} Muzalewski}, organization = {Fondation of Logic, Mathematics and Informatics --- Mizar Users Group}, year = 1993, note = {\url{http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz}} } %N @InProceedings{NaraschewskiW-TPHOLs98, author = {Wolfgang Naraschewski and Markus Wenzel}, title = {Object-Oriented Verification based on Record Subtyping in Higher-Order Logic}, crossref = {tphols98}} @inproceedings{nazareth-nipkow, author = {Dieter Nazareth and Tobias Nipkow}, title = {Formal Verification of Algorithm {W}: The Monomorphic Case}, crossref = {tphols96}, pages = {331-345}, year = 1996} @Article{needham-schroeder, author = "Roger M. Needham and Michael D. Schroeder", title = "Using Encryption for Authentication in Large Networks of Computers", journal = cacm, volume = 21, number = 12, pages = "993-999", month = dec, year = 1978} @inproceedings{nipkow-W, author = {Wolfgang Naraschewski and Tobias Nipkow}, title = {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}}, booktitle = {Types for Proofs and Programs: Intl. Workshop TYPES '96}, editor = {E. Gim{\'e}nez and C. Paulin-Mohring}, publisher = Springer, series = LNCS, volume = 1512, pages = {317-332}, year = 1998} @InCollection{nipkow-sorts93, author = {T. Nipkow}, title = {Order-Sorted Polymorphism in {Isabelle}}, booktitle = {Logical Environments}, publisher = CUP, year = 1993, editor = {G. Huet and G. Plotkin}, pages = {164--188} } @Misc{nipkow-types93, author = {Tobias Nipkow}, title = {Axiomatic Type Classes (in {I}sabelle)}, howpublished = {Presentation at the workshop \emph{Types for Proof and Programs}, Nijmegen}, year = 1993 } @inproceedings{Nipkow-CR, author = {Tobias Nipkow}, title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})}, booktitle = {Automated Deduction --- CADE-13}, editor = {M. McRobbie and J.K. Slaney}, publisher = Springer, series = LNCS, volume = 1104, pages = {733-747}, year = 1996} % WAS Nipkow-LICS-93 @InProceedings{nipkow-patterns, title = {Functional Unification of Higher-Order Patterns}, author = {Tobias Nipkow}, pages = {64-74}, crossref = {lics8}, url = {\url{ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html}}, keywords = {unification}} @article{nipkow-IMP, author = {Tobias Nipkow}, title = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook}, journal = FAC, volume = 10, pages = {171-186}, year = 1998} @inproceedings{Nipkow-TYPES02, author = {Tobias Nipkow}, title = {{Structured Proofs in Isar/HOL}}, booktitle = {Types for Proofs and Programs (TYPES 2002)}, editor = {H. Geuvers and F. Wiedijk}, year = 2003, publisher = Springer, series = LNCS, volume = 2646, pages = {259-278}} @manual{isabelle-HOL, author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, title = {{Isabelle}'s Logics: {HOL}}, institution = {Institut f{\"u}r Informatik, Technische Universi{\"a}t M{\"u}nchen and Computer Laboratory, University of Cambridge}, note = {\url{https://isabelle.in.tum.de/doc/logics-HOL.pdf}}} @article{nipkow-prehofer, author = {Tobias Nipkow and Christian Prehofer}, title = {Type Reconstruction for Type Classes}, journal = JFP, volume = 5, number = 2, year = 1995, pages = {201-224}} @InProceedings{Nipkow-Prehofer:1993, author = {T. Nipkow and C. Prehofer}, title = {Type checking type classes}, booktitle = {ACM Symp.\ Principles of Programming Languages}, year = 1993 } @Book{isa-tutorial, author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, title = {Isabelle/{HOL}: A Proof Assistant for Higher-Order Logic}, publisher = Springer, year = 2002, series = LNCS, volume = 2283} @Article{noel, author = {Philippe No{\"e}l}, title = {Experimenting with {Isabelle} in {ZF} Set Theory}, journal = JAR, volume = 10, number = 1, pages = {15-58}, year = 1993} @book{nordstrom90, author = {Bengt {Nordstr{\"o}m} and Kent Petersson and Jan Smith}, title = {Programming in {Martin-L{\"o}f}'s Type Theory. An Introduction}, publisher = {Oxford University Press}, year = 1990} %O @TechReport{scala-overview-tech-report, author = {Martin Odersky et al.}, title = {An Overview of the Scala Programming Language}, institution = {EPFL Lausanne, Switzerland}, year = 2004, number = {IC/2004/64} } @Article{Oppen:1980, author = {D. C. Oppen}, title = {Pretty Printing}, journal = {ACM Transactions on Programming Languages and Systems}, year = 1980, volume = 2, number = 4} @Manual{pvs-language, title = {The {PVS} specification language}, author = {S. Owre and N. Shankar and J. M. Rushby}, organization = {Computer Science Laboratory, SRI International}, address = {Menlo Park, CA}, note = {Beta release}, year = 1993, month = apr, url = {\url{http://www.csl.sri.com/reports/pvs-language.dvi.Z}}} %P @inproceedings{panny-et-al-2014, author = "Lorenz Panny and Jasmin Christian Blanchette and Dmitriy Traytel", title = "Primitively (co)recursive definitions for {I}sabelle/{HOL}", year = 2014, booktitle = "Isabelle Workshop 2014" } % replaces paulin92 @InProceedings{paulin-tlca, author = {Christine Paulin-Mohring}, title = {Inductive Definitions in the System {Coq}: Rules and Properties}, crossref = {tlca93}, pages = {328-345}} @Article{paulson:1983, author = {L. C. Paulson}, title = {A higher-order implementation of rewriting}, journal = {Science of Computer Programming}, year = 1983, volume = 3, pages = {119--149}, note = {\url{http://www.cl.cam.ac.uk/~lp15/papers/Reports/TR035-lcp-rewriting.pdf}}} @InProceedings{paulson-CADE, author = {Lawrence C. Paulson}, title = {A Fixedpoint Approach to Implementing (Co)Inductive Definitions}, pages = {148-161}, crossref = {cade12}} @InProceedings{paulson-COLOG, author = {Lawrence C. Paulson}, title = {A Formulation of the Simple Theory of Types (for {Isabelle})}, pages = {246-274}, crossref = {colog88}, url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}} @Article{paulson-coind, author = {Lawrence C. Paulson}, title = {Mechanizing Coinduction and Corecursion in Higher-Order Logic}, journal = JLC, year = 1997, volume = 7, number = 2, month = mar, pages = {175-204}} @article{paulson-numerical, author = {Lawrence C. Paulson}, title = {Organizing numerical theories using axiomatic type classes}, journal = JAR, year = 2004, volume = 33, number = 1, pages = {29-49}} @manual{isabelle-intro, author = {Lawrence C. Paulson}, title = {Old Introduction to {Isabelle}}, institution = CUCL, note = {\url{https://isabelle.in.tum.de/doc/intro.pdf}}} @manual{isabelle-logics, author = {Lawrence C. Paulson}, title = {{Isabelle's} Logics}, institution = CUCL, note = {\url{https://isabelle.in.tum.de/doc/logics.pdf}}} @manual{isabelle-ref, author = {Lawrence C. Paulson}, title = {The Old {Isabelle} Reference Manual}, institution = CUCL, note = {\url{https://isabelle.in.tum.de/doc/ref.pdf}}} @manual{isabelle-ZF, author = {Lawrence C. Paulson}, title = {{Isabelle}'s Logics: {FOL} and {ZF}}, institution = CUCL, note = {\url{https://isabelle.in.tum.de/doc/logics-ZF.pdf}}} @article{paulson-found, author = {Lawrence C. Paulson}, title = {The Foundation of a Generic Theorem Prover}, journal = JAR, volume = 5, number = 3, pages = {363-397}, year = 1989, url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}} %replaces paulson-final @Article{paulson-mscs, author = {Lawrence C. Paulson}, title = {Final Coalgebras as Greatest Fixed Points in {ZF} Set Theory}, journal = {Mathematical Structures in Computer Science}, year = 1999, volume = 9, number = 5, pages = {545-567}} @InCollection{paulson-generic, author = {Lawrence C. Paulson}, title = {Generic Automatic Proof Tools}, crossref = {wos-fest}, chapter = 3} @Article{paulson-gr, author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski}, title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice}, journal = JAR, year = 1996, volume = 17, number = 3, month = dec, pages = {291-323}} @InCollection{paulson-fixedpt-milner, author = {Lawrence C. Paulson}, title = {A Fixedpoint Approach to (Co)inductive and (Co)datatype Definitions}, pages = {187-211}, crossref = {milner-fest}} @book{milner-fest, title = {Proof, Language, and Interaction: Essays in Honor of {Robin Milner}}, booktitle = {Proof, Language, and Interaction: Essays in Honor of {Robin Milner}}, publisher = MIT, year = 2000, editor = {Gordon Plotkin and Colin Stirling and Mads Tofte}} @InCollection{paulson-handbook, author = {Lawrence C. Paulson}, title = {Designing a Theorem Prover}, crossref = {handbk-lics2}, pages = {415-475}} @Book{paulson-isa-book, author = {Lawrence C. Paulson}, title = {Isabelle: A Generic Theorem Prover}, publisher = {Springer}, year = 1994, note = {LNCS 828}} @Book{isabelle-hol-book, author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic}, publisher = {Springer}, year = 2002, note = {LNCS 2283}} @InCollection{paulson-markt, author = {Lawrence C. Paulson}, title = {Tool Support for Logics of Programs}, booktitle = {Mathematical Methods in Program Development: Summer School Marktoberdorf 1996}, publisher = {Springer}, pages = {461-498}, year = {Published 1997}, editor = {Manfred Broy}, series = {NATO ASI Series F}} %replaces Paulson-ML and paulson91 @book{paulson-ml2, author = {Lawrence C. Paulson}, title = {{ML} for the Working Programmer}, year = 1996, edition = {2nd}, publisher = CUP, note = {\url{https://www.cl.cam.ac.uk/~lp15/MLbook}}} @article{paulson-natural, author = {Lawrence C. Paulson}, title = {Natural Deduction as Higher-order Resolution}, journal = JLP, volume = 3, pages = {237-258}, year = 1986, url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}} @Article{paulson-set-I, author = {Lawrence C. Paulson}, title = {Set Theory for Verification: {I}. {From} Foundations to Functions}, journal = JAR, volume = 11, number = 3, pages = {353-389}, year = 1993, url = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Sets/set-I.pdf}}} @Article{paulson-set-II, author = {Lawrence C. Paulson}, title = {Set Theory for Verification: {II}. {Induction} and Recursion}, journal = JAR, volume = 15, number = 2, pages = {167-215}, year = 1995, url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}} @article{paulson85, author = {Lawrence C. Paulson}, title = {Verifying the Unification Algorithm in {LCF}}, journal = SCP, volume = 5, pages = {143-170}, year = 1985} %replaces Paulson-LCF @book{paulson87, author = {Lawrence C. Paulson}, title = {Logic and Computation: Interactive proof with Cambridge LCF}, year = 1987, publisher = CUP} @incollection{paulson700, author = {Lawrence C. Paulson}, title = {{Isabelle}: The Next 700 Theorem Provers}, crossref = {odifreddi90}, pages = {361-386}, url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}} % replaces paulson-ns and paulson-security @Article{paulson-jcs, author = {Lawrence C. Paulson}, title = {The Inductive Approach to Verifying Cryptographic Protocols}, journal = JCS, year = 1998, volume = 6, pages = {85-128}} @Article{paulson-tls, author = {Lawrence C. Paulson}, title = {Inductive Analysis of the {Internet} Protocol {TLS}}, journal = TISSEC, month = aug, year = 1999, volume = 2, number = 3, pages = {332-351}} @Article{paulson-yahalom, author = {Lawrence C. Paulson}, title = {Relations Between Secrets: Two Formal Analyses of the {Yahalom} Protocol}, journal = JCS, volume = 9, number = 3, pages = {197-216}, year = 2001}} @article{pelletier86, author = {F. J. Pelletier}, title = {Seventy-five Problems for Testing Automatic Theorem Provers}, journal = JAR, volume = 2, pages = {191-216}, year = 1986, note = {Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135}} @InCollection{pitts93, author = {A. Pitts}, title = {The {HOL} Logic}, editor = {M. J. C. Gordon and T. F. Melham}, booktitle = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic}, pages = {191--232}, publisher = CUP, year = 1993} @Article{pitts94, author = {Andrew M. Pitts}, title = {A Co-induction Principle for Recursively Defined Domains}, journal = TCS, volume = 124, pages = {195-219}, year = 1994} @Article{plaisted90, author = {David A. Plaisted}, title = {A Sequent-Style Model Elimination Strategy and a Positive Refinement}, journal = JAR, year = 1990, volume = 6, number = 4, pages = {389-402}} %Q @Article{quaife92, author = {Art Quaife}, title = {Automated Deduction in {von Neumann-Bernays-G\"{o}del} Set Theory}, journal = JAR, year = 1992, volume = 8, number = 1, pages = {91-147}} %R @TechReport{rasmussen95, author = {Ole Rasmussen}, title = {The {Church-Rosser} Theorem in {Isabelle}: A Proof Porting Experiment}, institution = {Computer Laboratory, University of Cambridge}, year = 1995, number = 364, month = may, url = {\url{http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}} @Book{reeves90, author = {Steve Reeves and Michael Clarke}, title = {Logic for Computer Science}, publisher = {Addison-Wesley}, year = 1990} @article{riazanov-voronkov-2002, author = "Alexander Riazanov and Andrei Voronkov", title = "The Design and Implementation of {Vampire}", journal = "Journal of AI Communications", year = 2002, volume = 15, number ="2/3", pages = "91--110"} @book{Rosen-DMA,author={Kenneth H. Rosen}, title={Discrete Mathematics and Its Applications}, publisher={McGraw-Hill},year=1998} @InProceedings{Rudnicki:1992:MizarOverview, author = {P. Rudnicki}, title = {An Overview of the {MIZAR} Project}, booktitle = {1992 Workshop on Types for Proofs and Programs}, year = 1992, organization = {Chalmers University of Technology}, publisher = {Bastad} } @article{rutten05, author = {Jan J. M. M. Rutten}, title = {A coinductive calculus of streams}, journal = {Math. Struct. Comp. Sci.}, volume = 15, number = 1, year = 2005, pages = {93--147}, } %S @inproceedings{saaltink-fme, author = {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and Dan Craigen and Irwin Meisels}, title = {An {EVES} Data Abstraction Example}, pages = {578-596}, crossref = {fme93}} @Article{Schroeder-Heister:1984, author = {Peter Schroeder-Heister}, title = {A Natural Extension of Natural Deduction}, journal = {Journal of Symbolic Logic}, year = 1984, volume = 49, number = 4 } -@article{schulz-2002, - author = "Stephan Schulz", - title = "E---A Brainiac Theorem Prover", - journal = "Journal of AI Communications", - year = 2002, - volume = 15, - number ="2/3", - pages = "111--126"} +@inproceedings{schulz-2019, + author = {Stephan Schulz and + Simon Cruanes and + Petar Vukmirovi\'c}, + editor = {Pascal Fontaine}, + title = {Faster, Higher, Stronger: {E} 2.3}, + booktitle = {Automated Deduction --- {CADE}-27}, + series = {Lecture Notes in Computer Science}, + volume = {11716}, + pages = {495--507}, + publisher = {Springer}, + year = {2019}, + url = {https://doi.org/10.1007/978-3-030-29436-6\_29}, + doi = {10.1007/978-3-030-29436-6\_29}, + timestamp = {Sat, 19 Oct 2019 20:28:03 +0200}, + biburl = {https://dblp.org/rec/conf/cade/0001CV19.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org}} @inproceedings{slind-tfl, author = {Konrad Slind}, title = {Function Definition in Higher Order Logic}, crossref = {tphols96}, pages = {381-397}} @inproceedings{leo3, Author = {Alexander Steen and Max Wisniewski and Christoph Benzm{\"u}ller}, Booktitle = {Mathematical Software -- ICMS 2016}, Editor = {G.-M. Greuel and T. Koch and P. Paule and A. Sommese}, Publisher = {Springer}, Series = {LNCS}, Title = {Agent-Based {HOL} Reasoning}, Volume = 9725, Year = 2016, Pages = {75-81} } @incollection{sternagel-thiemann-2015, title = "Deriving Class Instances for Datatypes", author = "Christian Sternagel and Ren\'e Thiemann", booktitle = "The Archive of Formal Proofs", editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson", publisher = "\url{https://isa-afp.org/entries/Deriving.shtml}", month = "March", year = 2015} @inproceedings{snark, author = {M. Stickel and R. Waldinger and M. Lowry and T. Pressburger and I. Underwood}, title = {Deductive composition of astronomical software from subroutine libraries}, pages = "341--355", crossref = {cade12}} @book{suppes72, author = {Patrick Suppes}, title = {Axiomatic Set Theory}, year = 1972, publisher = {Dover}} @inproceedings{sutcliffe-2000, author = "Geoff Sutcliffe", title = "System Description: {SystemOnTPTP}", editor = "David McAllester", booktitle = {Automated Deduction --- {CADE}-17 International Conference}, series = "Lecture Notes in Artificial Intelligence", volume = {1831}, pages = "406--410", year = 2000, publisher = Springer} @misc{tofof, author = "Geoff Sutcliffe", title = "{ToFoF}", note = "\url{http://www.cs.miami.edu/~tptp/ATPSystems/ToFoF/}"} @Article{Sutter:2005, author = {H. Sutter}, title = {The Free Lunch Is Over --- A Fundamental Turn Toward Concurrency in Software}, journal = {Dr. Dobb's Journal}, year = 2005, volume = 30, number = 3} @InCollection{szasz93, author = {Nora Szasz}, title = {A Machine Checked Proof that {Ackermann's} Function is not Primitive Recursive}, crossref = {huet-plotkin93}, pages = {317-338}} @TechReport{Syme:1997:DECLARE, author = {D. Syme}, title = {{DECLARE}: A Prototype Declarative Proof System for Higher Order Logic}, institution = {University of Cambridge Computer Laboratory}, year = 1997, number = 416 } @PhdThesis{Syme:1998:thesis, author = {D. Syme}, title = {Declarative Theorem Proving for Operational Semantics}, school = {University of Cambridge}, year = 1998, note = {Submitted} } @InProceedings{Syme:1999:TPHOL, author = {D. Syme}, title = {Three Tactic Theorem Proving}, crossref = {tphols99}} %T @book{takeuti87, author = {G. Takeuti}, title = {Proof Theory}, year = 1987, publisher = NH, edition = {2nd}} @Book{thompson91, author = {Simon Thompson}, title = {Type Theory and Functional Programming}, publisher = {Addison-Wesley}, year = 1991} @book{Thompson-Haskell,author={Simon Thompson}, title={Haskell: The Craft of Functional Programming}, publisher={Addison-Wesley},year=1999} @misc{kodkod-2009, author = "Emina Torlak", title = {Kodkod: Constraint Solver for Relational Logic}, note = "\url{http://alloy.mit.edu/kodkod/}"} @misc{kodkod-2009-options, author = "Emina Torlak", title = "Kodkod {API}: Class {Options}", note = "\url{http://alloy.mit.edu/kodkod/docs/kodkod/engine/config/Options.html}"} @inproceedings{torlak-jackson-2007, title = "Kodkod: A Relational Model Finder", author = "Emina Torlak and Daniel Jackson", editor = "Orna Grumberg and Michael Huth", booktitle = "TACAS 2007", series = LNCS, volume = {4424}, pages = "632--647", year = 2007, publisher = Springer} @inproceedings{traytel-berghofer-nipkow-2011, author = {Dmitriy Traytel and Stefan Berghofer and Tobias Nipkow}, title = {{Extending Hindley-Milner Type Inference with Coercive Structural Subtyping}}, year = 2011, editor = {Hongseok Yang}, booktitle = "APLAS 2011", series = LNCS, volume = {7078}, pages = "89--104"} @inproceedings{traytel-et-al-2012, author = "Dmitriy Traytel and Andrei Popescu and Jasmin Christian Blanchette", title = {Foundational, Compositional (Co)datatypes for Higher-Order Logic---{C}ategory Theory Applied to Theorem Proving}, year = {2012}, pages = {596--605}, booktitle = {27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012}, publisher = {IEEE} } @Unpublished{Trybulec:1993:MizarFeatures, author = {A. Trybulec}, title = {Some Features of the {Mizar} Language}, note = {Presented at a workshop in Turin, Italy}, year = 1993 } %V @Unpublished{voelker94, author = {Norbert V{\"o}lker}, title = {The Verification of a Timer Program using {Isabelle/HOL}}, note = {\url{ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz}}, year = 1994, month = aug} %W @inproceedings{wadler89how, author = {P. Wadler and S. Blott}, title = {How to make ad-hoc polymorphism less ad-hoc}, booktitle = {ACM Symp.\ Principles of Programming Languages}, year = 1989 } @phdthesis{weber-2008, author = "Tjark Weber", title = "SAT-Based Finite Model Generation for Higher-Order Logic", school = {Dept.\ of Informatics, T.U. M\"unchen}, type = "{Ph.D.}\ thesis", year = 2008} @Misc{x-symbol, author = {Christoph Wedler}, title = {Emacs package ``{X-Symbol}''}, note = {\url{http://x-symbol.sourceforge.net}} } -@misc{weidenbach-et-al-2009, - author = "Christoph Weidenbach and Dilyana Dimova and Arnaud Fietzke and Rohit Kumar and Martin Suda and Patrick Wischnewski", - title = "{SPASS} Version 3.5", - note = {\url{http://www.spass-prover.org/publications/spass.pdf}}} +@inproceedings{weidenbach-et-al-2009, + author = {Christoph Weidenbach and + Dilyana Dimova and + Arnaud Fietzke and + Rohit Kumar and + Martin Suda and + Patrick Wischnewski}, + editor = {Renate A. Schmidt}, + title = {{SPASS} Version 3.5}, + booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated + Deduction, Montreal, Canada, August 2-7, 2009. Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {5663}, + pages = {140--145}, + publisher = {Springer}, + year = {2009}, + url = {https://doi.org/10.1007/978-3-642-02959-2\_10}, + doi = {10.1007/978-3-642-02959-2\_10}, + timestamp = {Tue, 14 May 2019 10:00:39 +0200}, + biburl = {https://dblp.org/rec/conf/cade/WeidenbachDFKSW09.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} @manual{isabelle-system, author = {Makarius Wenzel}, title = {The {Isabelle} System Manual}, note = {\url{https://isabelle.in.tum.de/doc/system.pdf}}} @manual{isabelle-jedit, author = {Makarius Wenzel}, title = {{Isabelle/jEdit}}, note = {\url{https://isabelle.in.tum.de/doc/jedit.pdf}}} @manual{isabelle-isar-ref, author = {Makarius Wenzel}, title = {The {Isabelle/Isar} Reference Manual}, note = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}} @manual{isabelle-implementation, author = {Makarius Wenzel}, title = {The {Isabelle/Isar} Implementation}, note = {\url{https://isabelle.in.tum.de/doc/implementation.pdf}}} @InProceedings{Wenzel:1999:TPHOL, author = {Markus Wenzel}, title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents}, crossref = {tphols99}} @InProceedings{Wenzel:1997:TPHOL, author = {Markus Wenzel}, title = {Type Classes and Overloading in Higher-Order Logic}, crossref = {tphols97}} @phdthesis{Wenzel-PhD, author={Markus Wenzel}, title={Isabelle/Isar --- a versatile environment for human-readable formal proof documents}, school={Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen}, year=2002, note = {\url{https://mediatum.ub.tum.de/doc/601724/601724.pdf}}} @Article{Wenzel-Wiedijk:2002, author = {Freek Wiedijk and Markus Wenzel}, title = {A comparison of the mathematical proof languages {Mizar} and {Isar}.}, journal = {Journal of Automated Reasoning}, year = 2002, volume = 29, number = {3-4} } @InCollection{Wenzel-Paulson:2006, author = {Markus Wenzel and Lawrence C. Paulson}, title = {{Isabelle/Isar}}, booktitle = {The Seventeen Provers of the World}, year = 2006, editor = {F. Wiedijk}, series = {LNAI 3600}, publisher = Springer } @InCollection{Wenzel:2006:Festschrift, author = {Makarius Wenzel}, title = {{Isabelle/Isar} --- a generic framework for human-readable proof documents}, booktitle = {From Insight to Proof --- Festschrift in Honour of Andrzej Trybulec}, publisher = {University of Bia{\l}ystok}, year = 2007, editor = {R. Matuszewski and A. Zalewska}, volume = {10(23)}, series = {Studies in Logic, Grammar, and Rhetoric}, note = {\url{http://www.in.tum.de/~wenzelm/papers/isar-framework.pdf}} } @InProceedings{Wenzel-Chaieb:2007b, author = {Makarius Wenzel and Amine Chaieb}, title = {{SML} with antiquotations embedded into {Isabelle/Isar}}, booktitle = {Workshop on Programming Languages for Mechanized Mathematics (satellite of CALCULEMUS 2007). Hagenberg, Austria}, editor = {Jacques Carette and Freek Wiedijk}, month = {June}, year = {2007} } @InProceedings{Wenzel:2009, author = {M. Wenzel}, title = {Parallel Proof Checking in {Isabelle/Isar}}, booktitle = {ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009)}, year = 2009, editor = {Dos Reis, G. and L. Th\'ery}, publisher = {ACM Digital Library}} @InProceedings{Wenzel:2010, author = {Makarius Wenzel}, title = {Asynchronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}}, booktitle = {User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite Workshop}, year = 2010, editor = {C. Sacerdoti Coen and D. Aspinall}, series = {ENTCS}, month = {July}, publisher = {Elsevier}, url = {http://www.lri.fr/~wenzel/papers/async-isabelle-scala.pdf}} @InProceedings{Wenzel:2011:CICM, author = {M. Wenzel}, title = {Isabelle as Document-oriented Proof Assistant}, editor = {J. H. Davenport and W. M. Farmer and F. Rabe and J. Urban}, booktitle = {Conference on Intelligent Computer Mathematics / Mathematical Knowledge Management (CICM/MKM 2011)}, year = 2011, volume = {6824}, series = {LNAI}, publisher = {Springer}} @InProceedings{Wenzel:2012, author = {Makarius Wenzel}, title = {{Isabelle/jEdit} --- a {Prover IDE} within the {PIDE} framework}, booktitle = {Conference on Intelligent Computer Mathematics (CICM 2012)}, year = 2012, editor = {J. Jeuring and others}, volume = 7362, series = {LNAI}, publisher = {Springer}} @InProceedings{Wenzel:2012:UITP-EPTCS, author = {Makarius Wenzel}, title = {{READ-EVAL-PRINT} in Parallel and Asynchronous Proof-checking}, booktitle = {User Interfaces for Theorem Provers (UITP 2012)}, year = 2013, series = {EPTCS} } @inproceedings{Wenzel:2013:ITP, author = {Makarius Wenzel}, title = {Shared-Memory Multiprocessing for Interactive Theorem Proving}, booktitle = {Interactive Theorem Proving --- 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings}, editor = {Sandrine Blazy and Christine Paulin-Mohring and David Pichardie}, year = {2013}, ee = {https://doi.org/10.1007/978-3-642-39634-2_30}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {7998}, } @inproceedings{Wenzel:2014:ITP-PIDE, author = {Makarius Wenzel}, title = {Asynchronous User Interaction and Tool Integration in {Isabelle/PIDE}}, booktitle = {5th International Conference on Interactive Theorem Proving, ITP 2014}, editor = {Gerwin Klein and Ruben Gamboa}, year = {2014}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {8558}, } @InProceedings{Wenzel:2014:UITP, author = {Makarius Wenzel}, title = {System description: {Isabelle/jEdit} in 2014}, booktitle = {User Interfaces for Theorem Provers (UITP 2014)}, editor = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo, Bruno}, year = 2014, series = {EPTCS}, month = {July}, note = {\url{http://eptcs.web.cse.unsw.edu.au/paper.cgi?UITP2014:11}} } @InProceedings{Wenzel:2018:FIDE, author = {Makarius Wenzel}, title = {{Isabelle/jEdit} as {IDE} for domain-specific formal languages and informal text documents}, booktitle = {F-IDE Workshop 2018 (Oxford, UK)}, year = {2018}, editor = {Paolo Masci and Rosemary Monahan and Virgile Prevosto}, number = 284, series = {EPTCS}, note = {\url{http://eptcs.web.cse.unsw.edu.au/paper.cgi?FIDE2018.6}}, } @InProceedings{Wenzel:2019:MKM, author = {Makarius Wenzel}, title = {Interaction with Formal Mathematical Documents in {Isabelle/PIDE}}, booktitle = {Intelligent Computer Mathematics (CICM 2019)}, year = {2019}, editor = {Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Sacerdoti Coen, Claudio}, volume = {11617}, series = "LNAI", publisher = {Springer}, note = {\url{https://arxiv.org/abs/1905.01735}} } @book{principia, author = {A. N. Whitehead and B. Russell}, title = {Principia Mathematica}, year = 1962, publisher = CUP, note = {Paperback edition to *56, abridged from the 2nd edition (1927)}} @Misc{Wiedijk:1999:Mizar, author = {Freek Wiedijk}, title = {Mizar: An Impression}, howpublished = {Unpublished paper}, year = 1999, note = {\url{http://www.cs.kun.nl/~freek/mizar/mizarintro.ps.gz}} } @Misc{Wiedijk:2000:MV, author = {Freek Wiedijk}, title = {The Mathematical Vernacular}, howpublished = {Unpublished paper}, year = 2000, note = {\url{http://www.cs.kun.nl/~freek/notes/mv.ps.gz}} } @misc{wikipedia-2009-aa-trees, key = "Wikipedia", title = "Wikipedia: {AA} Tree", note = "\url{http://en.wikipedia.org/wiki/AA_tree}"} @book{winskel93, author = {Glynn Winskel}, title = {The Formal Semantics of Programming Languages}, publisher = MIT,year=1993} @InCollection{wos-bledsoe, author = {Larry Wos}, title = {Automated Reasoning and {Bledsoe's} Dream for the Field}, crossref = {bledsoe-fest}, pages = {297-342}} @InProceedings{Zammit:1999:TPHOL, author = {Vincent Zammit}, title = {On the Implementation of an Extensible Declarative Proof Language}, crossref = {tphols99}} -%Z - -@misc{z3, - key = "Z3", - title = "Z3: An Efficient {SMT} Solver", - note = "\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}"} - % CROSS REFERENCES @book{handbk-lics2, editor = {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum}, title = {Handbook of Logic in Computer Science}, booktitle = {Handbook of Logic in Computer Science}, publisher = {Oxford University Press}, year = 1992, volume = 2} @book{types93, editor = {Henk Barendregt and Tobias Nipkow}, title = TYPES # {: International Workshop {TYPES '93}}, booktitle = TYPES # {: International Workshop {TYPES '93}}, year = {published 1994}, publisher = {Springer}, series = {LNCS 806}} @book{barwise-handbk, editor = {J. Barwise}, title = {Handbook of Mathematical Logic}, booktitle = {Handbook of Mathematical Logic}, year = 1977, publisher = NH} @Proceedings{tlca93, title = {Typed Lambda Calculi and Applications}, booktitle = {Typed Lambda Calculi and Applications}, editor = {M. Bezem and J.F. Groote}, year = 1993, publisher = {Springer}, series = {LNCS 664}} @book{birtwistle89, editor = {Graham Birtwistle and P. A. Subrahmanyam}, title = {Current Trends in Hardware Verification and Automated Theorem Proving}, booktitle = {Current Trends in Hardware Verification and Automated Theorem Proving}, publisher = {Springer}, year = 1989} @book{bledsoe-fest, title = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}}, booktitle = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}}, publisher = {Kluwer Academic Publishers}, year = 1991, editor = {Robert S. Boyer}} @Proceedings{cade12, editor = {Alan Bundy}, title = {Automated Deduction --- {CADE}-12 International Conference}, booktitle = {Automated Deduction --- {CADE}-12 International Conference}, year = 1994, series = {LNAI 814}, publisher = {Springer}} @book{types94, editor = {Peter Dybjer and Bengt Nordstr{{\"o}m} and Jan Smith}, title = TYPES # {: International Workshop {TYPES '94}}, booktitle = TYPES # {: International Workshop {TYPES '94}}, year = 1995, publisher = {Springer}, series = {LNCS 996}} @book{huet-plotkin91, editor = {{G{\'e}rard} Huet and Gordon Plotkin}, title = {Logical Frameworks}, booktitle = {Logical Frameworks}, publisher = CUP, year = 1991} @book{huet-plotkin93, editor = {{G{\'e}rard} Huet and Gordon Plotkin}, title = {Logical Environments}, booktitle = {Logical Environments}, publisher = CUP, year = 1993} @Proceedings{hug93, editor = {J. Joyce and C. Seger}, title = {Higher Order Logic Theorem Proving and Its Applications: HUG '93}, booktitle = {Higher Order Logic Theorem Proving and Its Applications: HUG '93}, year = {Published 1994}, publisher = {Springer}, series = {LNCS 780}} @proceedings{colog88, editor = {P. Martin-L{\"o}f and G. Mints}, title = {COLOG-88: International Conference on Computer Logic}, booktitle = {COLOG-88: International Conference on Computer Logic}, year = {Published 1990}, publisher = {Springer}, organization = {Estonian Academy of Sciences}, address = {Tallinn}, series = {LNCS 417}} @book{odifreddi90, editor = {P. Odifreddi}, title = {Logic and Computer Science}, booktitle = {Logic and Computer Science}, publisher = {Academic Press}, year = 1990} @proceedings{cade10, editor = {Mark E. Stickel}, title = {10th } # CADE, booktitle = {10th } # CADE, year = 1990, publisher = {Springer}, series = {LNAI 449}} @Proceedings{lics8, editor = {M. Vardi}, title = {Eighth Annual Symposium on Logic in Computer Science}, booktitle = {Eighth Annual Symposium on Logic in Computer Science}, publisher = IEEE, year = 1993} @book{wos-fest, title = {Automated Reasoning and its Applications: Essays in Honor of {Larry Wos}}, booktitle = {Automated Reasoning and its Applications: Essays in Honor of {Larry Wos}}, publisher = MIT, year = 1997, editor = {Robert Veroff}} @proceedings{fme93, editor = {J. C. P. Woodcock and P. G. Larsen}, title = {FME '93: Industrial-Strength Formal Methods}, booktitle = {FME '93: Industrial-Strength Formal Methods}, year = 1993, publisher = Springer, series = LNCS, volume = 670} @Proceedings{tphols96, title = {Theorem Proving in Higher Order Logics: {TPHOLs} '96}, booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '96}, editor = {J. von Wright and J. Grundy and J. Harrison}, publisher = Springer, series = LNCS, volume = 1125, year = 1996} @Proceedings{tphols97, title = {Theorem Proving in Higher Order Logics: {TPHOLs} '97}, booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '97}, editor = {Elsa L. Gunter and Amy Felty}, publisher = Springer, series = LNCS, volume = 1275, year = 1997} @Proceedings{tphols98, title = {Theorem Proving in Higher Order Logics: {TPHOLs} '98}, booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '98}, editor = {Jim Grundy and Malcom Newey}, publisher = Springer, series = LNCS, volume = 1479, year = 1998} @Proceedings{tphols99, title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and Paulin, C. and Thery, L.}, publisher = Springer, series = LNCS, volume = 1690, year = 1999} @Proceedings{tphols2000, title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000}, booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000}, editor = {J. Harrison and M. Aagaard}, publisher = Springer, series = LNCS, volume = 1869, year = 2000} @Proceedings{tphols2001, title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001}, booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001}, editor = {R. J. Boulton and P. B. Jackson}, publisher = Springer, series = LNCS, volume = 2152, year = 2001} @Proceedings{ijcar2006, title = {Automated Reasoning: {IJCAR} 2006}, booktitle = {Automated Reasoning: {IJCAR} 2006}, editor = {U. Furbach and N. Shankar}, publisher = Springer, series = LNCS, volume = 4130, year = 2006} @Proceedings{tphols2007, title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2007}, booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2007}, editor = {K. Schneider and J. Brandt}, publisher = Springer, series = LNCS, volume = 4732, year = 2007} @Proceedings{tphols2008, title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008}, booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008}, editor = {Otmane A{\"{\i}}t Mohamed and C{\'{e}}sar A. Mu{\~{n}}oz and Sofi{\`{e}}ne Tahar}, publisher = Springer, series = LNCS, year = 2008} % editor = % volume = 4732, @Proceedings{itp2010, title = {Interactive Theorem Proving: {ITP}-10}, booktitle = {Interactive Theorem Proving: {ITP}-10}, editor = "Matt Kaufmann and Lawrence Paulson", publisher = Springer, series = LNCS, year = 2010} @unpublished{classes_modules, title = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison}, author = {Stefan Wehr and Manuel M. T. Chakravarty}, note = {\url{https://www.cse.unsw.edu.au/~chak/papers/modules-classes.pdf}} } @inproceedings{runciman-naylor-lindblad, author = {Runciman, Colin and Naylor, Matthew and Lindblad, Fredrik}, title = {Smallcheck and {Lazy Smallcheck}: Automatic Exhaustive Testing for Small Values}, booktitle = {Proceedings of the First ACM SIGPLAN Symposium on Haskell (Haskell 2008)}, year = {2008}, pages = {37--48}, publisher = {ACM}, }