E es un probador de teoremas de alto rendimiento para lógica completa de primer orden con igualdad. [1] Se basa en el cálculo de superposición ecuacional y utiliza un paradigma puramente ecuacional. Se ha integrado en otros probadores de teoremas y ha estado entre los sistemas mejor ubicados en varios concursos de demostración de teoremas. E es desarrollado por Stephan Schulz, originalmente en el Grupo de Razonamiento Automatizado en TU Munich , ahora en la Universidad Estatal Cooperativa Baden-Württemberg de Stuttgart.
El sistema se basa en el cálculo de superposición ecuacional . A diferencia de la mayoría de los otros probadores actuales, la implementación en realidad usa un paradigma puramente ecuacional y simula inferencias no ecuacionales a través de inferencias de igualdad apropiadas. Las innovaciones significativas incluyen la reescritura de términos compartidos (donde muchas simplificaciones ecuacionales posibles se llevan a cabo en una sola operación), [2] varias estructuras de datos de indexación de términos eficientes para acelerar las inferencias, estrategias avanzadas de selección de literales de inferencia y varios usos de técnicas de aprendizaje automático para mejorar el comportamiento de búsqueda. [2] [3] [4] Desde la versión 2.0, E admite lógica de ordenación múltiple . [5]
E está implementado en C y es portátil para la mayoría de las variantes de UNIX y el entorno Cygwin . Está disponible bajo la GNU GPL . [6]
El probador se ha desempeñado consistentemente bien en la competencia del sistema CADE ATP , ganando la categoría CNF/MIX en 2000 y terminando entre los mejores sistemas desde entonces. [7] En 2008 quedó en segundo lugar. [8] En 2009 obtuvo el segundo lugar en las categorías FOF (full first order logic) y UEQ (unit equational logic) y el tercer lugar (después de dos versiones de Vampire ) en CNF (clausal logic). [9] Repitió la actuación en FOF y CNF en 2010 y ganó un premio especial como "mejor sistema general". [10] En el 2011 CASC-23 E ganó la división CNF y logró segundos lugares en UEQ y LTB. [11]
E se ha integrado en varios otros probadores de teoremas. Es, con Vampire , SPASS , CVC4 y Z3 , el núcleo de la estrategia Sledgehammer de Isabelle . [12] [13] E también es el motor de razonamiento en SINE [14] y LEO-II [15] y se utiliza como sistema de clausificación para iProver. [dieciséis]
Las aplicaciones de E incluyen razonamiento sobre grandes ontologías, [17] verificación de software, [18] y certificación de software. [19]