 | This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these messages)
|
&sq=Google&lang=en&file=File:Question_book-new.svg){kind=small}
| Original author(s) | Andrei Voronkov[1] |
|---|---|
| Developer(s) | Vampire team |
| Stable release | 4.5.1
/ 2020-07-15 |
| Repository | |
| Written in | C++ |
| Available in | Vampire Modified BSD Licence[2] |
| Type | Automated theorem proving |
| Website | vprover |
Vampire is an automatic theorem prover for first-order classical logic developed in the Department of Computer Science at the University of Manchester. Up to Version 3, it was developed by Andrei Voronkov together with Kryštof Hoder and previously with Alexandre Riazanov. Since Version 4, the development has involved a wider international team including Laura Kovacs, Giles Reger, and Martin Suda. Since 1999 it has won at least 53 trophies in the CADE ATP System Competition, the "world cup for theorem provers", including the most prestigious FOF division and the theory-reasoning TFA division.[3][4]
- ^ "History". vprover.github.io. Retrieved 24 May 2018.
- ^ "Vampire Licence (Modified BSD)". vprover.github.io. Retrieved 2 November 2022.
- ^ Riazanov, A.; Voronkov, A. (2002). "The design and implementation of VAMPIRE". AI Communications. 15 (2–3/2002): 91–110. ISSN 0921-7126.
- ^ Voronkov, A. (1995). "The anatomy of vampire". Journal of Automated Reasoning. 15 (2): 237–265. doi:10.1007/BF00881918. S2CID 1541122.