A Higher-Order Vampire (Short Paper)

TL;DR

This paper discusses recent developments in Vampire theorem prover's support for higher-order reasoning, including new theoretical ideas, implementation details, and empirical performance results.

Contribution

It introduces a reworked approach to higher-order reasoning in Vampire with new theoretical concepts, implementation, and strategy scheduling.

Findings

Implementation of higher-order calculus in Vampire

Empirical performance statistics show improvements

Discussion of ongoing theoretical development

Abstract

The support for higher-order reasoning in the Vampire theorem prover has recently been completely reworked. This rework consists of new theoretical ideas, a new implementation, and a dedicated strategy schedule. The theoretical ideas are still under development, so we discuss them at a high level in this paper. We also describe the implementation of the calculus in the Vampire theorem prover, the strategy schedule construction and several empirical performance statistics.