Zippy - Generic White-Box Proof Search with Zippers

This entry contains 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 here.

This entry also provides a concrete instantiation of the framework in the form of a general purpose white-box prover, called 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 certifying 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.