Things You Can't Do with a Vampire

Abstract

The Vampire Automated Theorem Proving (ATP) system has been very successful at proving theorems in first-order logic. Vampire has won the First-Order Form (FOF) division of the CADE ATP System Competition (CASC) for all except one of the last 15 years, and many papers highlighting Vampire's strengths have been published. This talk examines the flip side of the Vampire coin ... what kinds of problems are difficult or even impossible for the latest incarnation of Vampire. The talk will help users decide when to use Vampire, and when to use another ATP system, will help the Vampire developers direct their work, and provides the data required to build a portfolio ATP system with Vampire as a component.