Wir beschreiben die Erweiterungen des Theorembeweisers in Logik erster Ordnung Vampire, um Theoreme in der Theorie der Bitvektoren fester Größe zu beweisen, möglicherweise mit Quantoren. Es werden sowohl Details zur Erweiterung des Parsers von Vampire als auch des Argumentationsverfahren von Vampire gegeben. Wir präsentieren unsere experimentellen Ergebnisse, indem wir unseren Ansatz mit SMT-Löser vergleichen und evaluiren. Unsere Experimente berichten auch über einige Beispiele, die nur durch unseren Arbeit bewiesen werden können.
de
We describe extensions to the first-order theorem prover Vampire for proving theorems in the theory of fixed-sized bitvectors, possibly with quantifiers. Details are given on extending both the parser of Vampire as well as the theory reasoning framework of Vampire. We present our experimental results by evaluating and comparing our approach to SMT solvers. Our experiments report also on a few examples that can be solved only by our work.
