AVATAR: The New Architecture for First-Order Theorem Provers

ABSTRACT. This paper describes a new architecture for first-order resolution and superposition theorem provers called AVATAR (Advanced Vampire Architecture for Theories and Resolution). Its original motivation comes from the problem well-studied in the past --- dealing with problems having clauses containing propositional variables and other clauses that can be split into components with disjoint sets of variables. Such clauses are common for problems coming from applications, for example in verification and program analysis, where many ground literals occur in the problems and even more are generated during the proof-search.

This problem was previously studied by adding various versions of splitting. The addition of splitting resulted in considerable improvements in performance of theorem provers. However, even with various versions of splitting implemented, the performance of superposition theorem provers is nowhere near SMT solvers on purely ground problems or SAT solvers on propositional problems.

This paper describes a new, revolutionary architecture for superposition theorem provers, where a superposition theorem prover is tightly integrated with a SAT or an SMT solver. Its implementation in our theorem prover Vampire resulted in drastic improvements over all previous implementation of splitting. Over four hundred TPTP problems previously unsolvable by any modern prover, including Vampire itself, have been proved, most of them with short runtimes. Many problems solved with one of 481 variants of splitting previously implemented in Vampire can also be solved with AVATAR.

We also believe that AVATAR is ideally suited for applications where reasoning with both quantifiers and theories is required.