出典:Wikipedia
出典:『Wikipedia』 (2011/06/23 02:26 UTC 版)
Vampire is an automatic theorem prover for first-order classical logic developed in the Computer Science Department of the University of Manchester by Prof. Andrei Voronkov together with Kryštof Hoder and previously with Dr. Alexandre Riazanov. So far it has won the "world cup for theorem provers" (the CADE ATP System Competition) in the most prestigious CNF (MIX) division eleven times (1999, 2001–2010).