Quelle  root.tex

\documentclass[11pt,a4paper]{report}
\usepackage[T1]{fontenc}
\usepackage{amssymb}
\usepackage{isabelle,isabellesym}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

\newcommand{\isactrlfunctorUNDERSCOREinstance}{\isakeywordcontrol{functor{\isacharunderscore}instance}}
\newcommand{\isactrleval}{\isakeywordcontrol{eval}}
\newcommand{\isactrlimap}{\isakeywordcontrol{imap}}

\begin{document}

\title{Zippy -- Generic White-Box Proof Search with Zippers}
\author{Kevin Kappelmann}
\maketitle

\begin{abstract}
This entry contains \emph{Zippy}, a framework for tree-based searches.
Zippy is largely independent of concrete search tree representations, search-algorithms, states and effects.
It is designed to create analysable and navigable searches that are open to customisation and extensions by users.
An accompanying arXiv preprint is available~\cite{zippy}.

This entry also provides a concrete instantiation of the framework in the form of a general purpose white-box prover, called \emph{zip}.
The prover performs a proof tree search with customisable expansion actions and search strategies,
including A${}^{*}$, breadth-first, depth-first, and best-first search.
By default, it integrates the classical reasoner, simplifier, the blast and metis prover,
and supports resolution with higher-order and proof-producing unification, conditional substitutions, case splitting, and induction,
among other things.
Users are free to extend the prover with additional expansion actions and search strategies.
We demonstrate the capabilities of zip in an examples theory.

In most cases, zip can be used as a drop-in replacement for Isabelle's classical methods, including
auto, fastforce, force, fast, etc. We demonstrate this with a benchmark containing 2267 method calls
from Isabelle's standard library, where zip achieves a success rate of 99.82\% (2263/2267).

The Zippy framework is founded on concepts from functional programming theory, particularly zippers, arrows,
monads, lenses, and coroutines. This entry contains a library of mentioned concepts for Isabelle/ML.
\end{abstract}

\tableofcontents

% include generated text of all theories
\input{session}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}