Vampiro (demostrador de teoremas)

Vampire es un demostrador automático de teoremas para 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 Competencia de Sistemas CADE ATP , la "copa del mundo para demostradores de teoremas", incluyendo la prestigiosa división FOF y la división de razonamiento teórico TFA. ^{[ 3 ] [ 4 ]}

El núcleo 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 de igualdad negativa se pueden simular mediante la introducción de nuevas definiciones de predicados y el plegado dinámico de dichas definiciones. También se admite una división de algoritmo de estilo DPLL . 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ías , resolución de subsunción , reescritura por igualdades de unidades ordenadas, restricciones de basicidad e irreductibilidad de términos de sustitución . El orden de reducción en los términos es el orden estándar de Knuth-Bendix .

Se utilizan diversas 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 coincidencia directa.

Aunque el núcleo del sistema solo trabaja con formas normales conjuntivas , el componente de preprocesamiento acepta un problema en la sintaxis completa de lógica de primer orden, lo clausura y realiza una serie de transformaciones útiles antes de pasar el resultado al núcleo. Cuando se demuestra un teorema, el sistema produce una prueba verificable que valida tanto la fase de clausura como la refutación de la forma normal conjuntiva .

Además de demostrar teoremas, Vampire tiene otras funcionalidades relacionadas, como la generación de interpolantes .

Los ejecutables se pueden obtener del sitio web del sistema. ^{[ 5 ]} Desde noviembre de 2020, Vampire se distribuye bajo una versión modificada de la licencia BSD de 3 cláusulas que permite explícitamente el uso comercial. Las versiones anteriores estaban disponibles bajo una licencia propietaria no comercial.

• Sitio web oficial