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.

ABSTRACT. Vampire is a complex software that has been developing for decades. In the following, we discuss the process of converting theoretical inovation into applicable code. We discuss documentation, testing, profiling and benchmarking, based on the experience gained while developing a new subsumption resolution module.

ABSTRACT. During proof search in saturation systems, instances of a generalising term may appear repeatedly in the search space. Detecting and rewriting this class of instances with a new definition may be beneficial. An approximate online method based on anti-unification for efficiently computing generalising terms as instances appear is described. Once identified, a definition for the generalising term is added to the search space, where it eliminates the class. The technique is implemented in the first-order system Vampire.

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 had to incorporate it into the prover's architecture. In this submission, we describe the considerations of integrating our synthesis technique with the AVATAR splitting framework. 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.

ABSTRACT. In inductive reasoning, apart from guessing inductive lemmas that imply the current conjecture, a great deal of difficulty is attributed to proving these lemmas by valid induction axioms. One axis of freedom in generating these axioms is deciding which variable to induct upon, i.e. which variable to use for case distinction in the axiom antecedent. In this work, we impose syntactic criteria on selecting induction terms based on the current induction schemes and the underlying inference system, reducing the space of induction axioms. We apply these criteria in combination with efficient methods from saturation-based theorem proving. Our experiments show a significant reduction of the search space leading to proofs of hundreds of more problems.

ABSTRACT. We describe an automated reasoning framework in Vampire allowing to fully automate the verification of functional properties of sorting algorithms.

ABSTRACT. Since the automatic theorem prover Vampire uses a variety of techniques to find proofs, it is a complex piece of software with a large trusted code base. To enhance trust in the the proofs Vampire produces, they could be checked with an interactive theorem prover with a small kernel and thus a much smaller trusted part. We report on work in progress to verify Vampire proofs in $\lambda \Pi$-calculus Modulo Theories, the underlying type theory of Dedukti.

ABSTRACT. This paper is an extended abstract, there is no separate abstract.

ABSTRACT. Modern first-order theorem provers using saturation algorithms use a number of options to control proof-search. As an extreme example, Vampire has 212 such options. Even if all of these options were boolean, it would result in up to 2^212 different strategies, which is a very large number.

It is well-known that there is no silver bullet strategy or a small collection of strategies that could be used to solve a high percentage of currently available theorem prover benchmarks. To tackle this problem, one puts together schedules, that is sequences or other collections of strategies. For example, Vampire has a portfolio mode in which it runs schedules, which depend on the input problem, time limit and the number of available cores.

Creating powerful schedules is a challenging problem. This paper describes the system Spider used to train Vampire and put together schedules. Spider was used since 2010 and has been a secret weapon behind Vampire's success at the CASC competitions. It was also probably the most useful tool for Vampire's support and development.

In this paper we describe the ideas, architecture and the learning algorithm used in Spider. We also explain other uses of Spider and problems in working with large sets of options.