Vampire es un probador automático de teoremas para la lógica clásica de primer orden desarrollado en el Departamento de Ciencias de la Computación de la Universidad de Manchester . Hasta la versión 3, fue desarrollado por Andrei Voronkov junto con Kryštof Hoder y anteriormente con Alexandre Riazanov. Desde la Versión 4, el desarrollo ha involucrado a un equipo internacional más amplio que incluye a Laura Kovacs, Giles Reger y Martin Suda. Desde 1999 ha ganado al menos 53 trofeos en la "copa del mundo para probadores de teoremas" (la Competencia del Sistema CADE ATP ), incluida la división FOF más prestigiosa y la división TFA de razonamiento teórico. [3] [4]
El kernel de Vampire implementa los cálculos de resolución binaria ordenada y superposición para manejar la igualdad. La regla de división y la división por igualdad negativa pueden simularse mediante la introducción de nuevas definiciones de predicado y el plegado dinámico de tales definiciones. Un algoritmo de estilo DPLL división también es compatible. Se utilizan varios criterios de redundancia estándar y técnicas de simplificación para podar el espacio de búsqueda: eliminación de tautología , resolución de subsunción , reescritura por igualdades de unidades ordenadas, restricciones de basicidad e irreductibilidad de los términos de sustitución. El orden de reducción utilizado es el estándar de Knuth-Bendix .
Se utilizan varias técnicas de indexación eficientes para implementar todas las operaciones principales en conjuntos de términos y cláusulas. La especialización de algoritmos en tiempo de ejecución se utiliza para acelerar la búsqueda de coincidencias.
Aunque el núcleo del sistema funciona sólo con formas normales clausales, el componente preprocesador acepta un problema en la sintaxis lógica de primer orden completa, lo clausifica y realiza una serie de transformaciones útiles antes de pasar el resultado al núcleo. Cuando se prueba un teorema, el sistema produce una prueba verificable, que valida tanto la fase de clausificación como la refutación de la forma normal conjuntiva .
Además de probar teoremas, Vampire tiene otras funcionalidades relacionadas, como generar interpolantes .
Los ejecutables se pueden obtener en el sitio web del sistema. [5] Una versión algo desactualizada está disponible bajo la Licencia Pública General Reducida GNU como parte de Sigma KEE . [6]