| Title: | Playing with AVATAR |
| Authors: | Giles Reger, Martin Suda and Andrei Voronkov |
| Proceedings: | Vampire 2014 Proceedings |
| Editors: | Laura Kovacs and Andrei Voronkov |
| Keywords: | Vampire, AVATAR, First-Order Theorem Proving, Saturation Algorithms |
| 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. |
| Pages: | 1 |
| Talk: | Jul 23 12:30 |
| Paper: |  |