| Autor: |
Kotelnikov, Evgenii, Kovács, Laura, Reger, Giles, Voronkov, Andrei |
| Rok vydání: |
2015 |
| Předmět: |
|
| Druh dokumentu: |
Working Paper |
| DOI: |
10.1145/2854065.2854071 |
| Popis: |
This paper presents new features recently implemented in the theorem prover Vampire, namely support for first-order logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also contains if-then-else and let-in expressions. We argue that presented extensions facilitate reasoning-based program analysis, both by increasing the expressivity of first-order reasoners and by gains in efficiency. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
