Vampire23: Papers with Abstracts

Abstract. The saturation framework by Leo Bachmair and Harald Ganzinger is the primary reference for proving the completeness of saturation-based calculi. In my invited talk, I presented a recent extension of this framework, its mechanisation in Isabelle/HOL and its various instances. Here I focus on the instances, using them to highlight various interesting features of the extended framework.

Abstract. Eager maintenance of invariants is often the first approach to implement high-performance data structures. We present a number of examples from the evolving implementation of the theorem prover E to demonstrate that a more relaxed, lazy implementation can have advantages for simplicity, performance, or both. Existing examples include shared rewriting, term cell garbage collection, and orphan removal, additional optimisations are identified for term index maintenance and clause selection.

Abstract. We recently introduced a framework for program synthesis based on functional specifications using a saturation-based theorem prover.
To make our synthesis technique efficient, we need to incorporate it into the prover's architecture.
In this paper, we describe the considerations of integrating our synthesis technique with the AVATAR splitting framework used in first-order theorem proving.
We present an example that illustrates the issues accompanying the integration and describe our solution: constraining the splitting and adding an additional inference rule replacing certain clauses with AVATAR assertions by assertion-free clauses.
Our experimental results indicate that the integration significantly improves the synthesis performance on some benchmarks.