ABSTRACT. The first version of the Vampire theorem prover was implemented 20 years ago, in 1994. Vampire has always been known for its fast and efficient implementation, for example it has won 30 world cup winner titles in first-order theorem proving.

In this talk we will first briefly overview the history of Vampire. Next, we address current results and trends in Vampire, with special focus on applications of reasoning in program analysis and verification. The current version of Vampire is faster than any of its previous versions and includes several new, non-standard features such as SAT/SMT solving, reasoning with theories, program analysis, consequence elimination, invariant generation, interpolation, and reasoning with very large theories.

ABSTRACT. In various applications of theorem proving, they not only check if a theorem holds true but also need a proof of the theorem, e.g., spurious counterexample analysis in verification.

The proofs can be presented in various formats to a user. Not all proof formats are conducive to the need of a user. The user may prefer one proof system over another. A user may prefer to have concise proofs, and other may like to have detailed proofs that allow inexpensive proof checking. Furthermore, there is no commonly acceptable API or file format for proof output. This situation allows the provers to produce proofs that are mutually incompatible and do not match the need of the users. Producing a proof after a run of an efficient and complex theorem prover is not a straight forward task. For example, the provers may apply various simplifications on input formulas before running the core proving algorithms. Such simplifications should be added as proof steps in the generated proofs. In long and arduous development process of a theorem prover, developers may forget to provide proper annotations to all the deduction steps such that a sufficiently detailed proof can be generated.

Currently, a Vampire proof only contains the information about the antecedents of the deduced clauses and the proof rule that is used to produce the clauses. This proof format leaves out various details. For example, an application of the superposition rule does not specify the terms that were unified to obtain the consequences. We propose to develop a comprehensive proof format and API that allows proofs with different level of granularity and are easy to use.

ABSTRACT. This paper presents and explores experimental results examining the usage of AVATAR (Advanced Vampire Architecture for Theories and Resolution). This architecture introduces a new method for splitting in first-order resolution and superposition theorem provers that makes use of a SAT (or SMT) solver to make splitting decisions. The architecture (as implemented in Vampire) has many options and components that can be varied and this paper explores the effects of these variations on the performance of the prover.

ABSTRACT. Sledgehammer integrates third-party automatic theorem provers in the proof assistant Isabelle/HOL. In the seven years since its first release in 2007, it has grown to become an essential part of most Isabelle users' workflow. Although a lot of effort has gone into tuning the system, the main reason for Sledgehammer's success is the impressive power of the external provers, especially E, SPASS, Vampire, and Z3. In this paper, I review Vampire's strengths and weaknesses in this context and propose a few directions for future work.

ABSTRACT. In order to better understand how well an external SAT solver would behave in the framework of a first order automated theorem prover we have decided to integrate in Vampire one of the best performing solvers available on the market, Lingeling. Although the process of integration is straight forward, by simply implementing some interfaces in order to make the two tools communicate and putting them together, there are a few problems that have to be overcome.

In this talk we are going to address both the issues that arise from integration of the two solver and present initial results obtained by using this combination. And also details about different strategies that are currently implemented.

ABSTRACT. Automated analysis and verification of programs requires proving properties in the combination of first-order theories of various data structures, such as integers, arrays, or lists.  Automated first-order theorem provers face new requirements from reasoning-based analysis and verification, and their efficiency largely depends on how programs are translated  into a collection of logical formulas capturing the program semantics. Recent extentions to the TPTP language, the input language of automated provers, support  new programming languages features aimed to keep translation-sensitive semantics on the level of the theorem prover. For example, TPTP has recently been extended with if-then-else and let-in constructs over terms and formulas. In this paper we propose to extend TPTP with the built-in first class boolean type that can facilitate translation of programs with conditional statement and simplify the treatment of if-then-else and let-in constructs of TPTP.  The treatment of a built-in first class boolean type can be efficiently implemented in the Vampire theorem prover without major changes in its architecture.

ABSTRACT. Extensionality resolution is a new inference rule that helps first-order theorem provers to overcome limitations when reasoning with extensionality axioms. The inference rule naturally resembles the use of extensionality axioms in human proofs and integrates easily into the architecture of superposition-based theorem provers. The recent implementation of extensionality resolution in Vampire provides strong experimental evidence of the effectiveness of the technique. We present ongoing work on new options to control the recognition of extensionality axioms as well as the application of extensionality resolution inferences in the proof search of Vampire.