E es un demostrador de teoremas de alto rendimiento para la lógica completa de primer orden con igualdad. [1] Se basa en el cálculo de superposición de ecuaciones 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 de Baden-Württemberg de Stuttgart.
Sistema
El sistema se basa en el cálculo de superposición de ecuaciones . A diferencia de la mayoría de los 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 de ecuaciones 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 de selección literal de inferencia avanzada 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 muchos ordenamientos . [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 GNU GPL . [6]
Competiciones
El prover se ha desempeñado consistentemente bien en la Competencia de sistemas 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 ganó el segundo lugar en las categorías FOF (lógica completa de primer orden) y UEQ (lógica de ecuación de unidad) y el tercer lugar (después de dos versiones de Vampire ) en CNF (lógica clausal). [9] Repitió el desempeño en FOF y CNF en 2010 y ganó un premio especial como "mejor sistema en general". [10] En el 2011 CASC-23 E ganó la división CNF y logró los segundos lugares en UEQ y LTB. [11]
Aplicaciones
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]
Referencias
- ^ Schulz, Stephan (2002). "E - un demostrador del teorema de Brainiac". Revista de comunicaciones de IA . 15 (2/3): 111–126.
- ^ a b Schulz, Stephan (2008). "Descripciones del sistema de participantes: E 1.0pre y EP 1.0pre" . Consultado el 24 de marzo de 2009 .
- ^ Schulz, Stephan (2004). "Descripción del sistema: E 0.81". Actas de la 2ª Conferencia conjunta internacional sobre razonamiento automatizado . Apuntes de conferencias en informática. Springer . LNAI 3097: 223–228. doi : 10.1007 / 978-3-540-25984-8_15 . ISBN 978-3-540-22345-0.
- ^ Schulz, Stephan (2001). "Aprendizaje de conocimientos de control de búsqueda para la demostración del teorema de ecuaciones". Actas de la Conferencia Conjunta Alemana / Austriaca sobre Inteligencia Artificial (KI-2001) . Apuntes de conferencias en informática. Springer . LNAI 2174: 320–334. doi : 10.1007 / 3-540-45422-5_23 . ISBN 978-3-540-42612-7.
- ^ "noticias en el sitio web de E" . Consultado el 10 de julio de 2017 .
- ^ Schulz, Stephan (2008). "El demostrador del teorema de la ecuación E" . Consultado el 24 de marzo de 2009 .
- ^ Sutcliffe, Geoff. "La Competencia del Sistema CADE ATP" . Archivado desde el original el 2 de marzo de 2009 . Consultado el 24 de marzo de 2009 .
- ^ División FOF de CASC en 2008
- ^ Sutcliffe, Geoff (2009). "El 4º Concurso de Sistema de Prueba de Teorema Automatizado IJCAR - CASC-J4" . Comunicaciones AI . 22 (1): 59–72. doi : 10.3233 / AIC-2009-0441 . Consultado el 16 de diciembre de 2009 .
- ^ Sutcliffe, Geoff (2010). "La Competencia del Sistema CADE ATP" . Universidad de Miami . Consultado el 20 de julio de 2010 .
- ^ Sutcliffe, Geoff (2011). "La Competencia del Sistema CADE ATP" . Universidad de Miami . Consultado el 14 de agosto de 2011 .
- ^ Paulson, Lawrence C. (2008). "Automatización para pruebas interactivas: técnicas, lecciones y perspectivas" (PDF) . Herramientas y técnicas para la verificación de la infraestructura del sistema: un Festschrift en honor al profesor Michael JC Gordon FRS : 29–30 . Consultado el 19 de diciembre de 2009 .
- ^ Meng, Jia; Lawrence C. Paulson (2004). "Experimentos de apoyo a la prueba interactiva mediante resolución". LNCS . Apuntes de conferencias en informática. Saltador. 3097 : 372–384. CiteSeerX 10.1.1.62.5009 . doi : 10.1007 / 978-3-540-25984-8_28 . ISBN 978-3-540-22345-0.
- ^ Sutcliffe, Geoff; et al. (2009). La IV Competencia del Sistema ATP de IJCAR (PDF) . Consultado el 18 de diciembre de 2009 .
- ^ Benzmüller, Christoph; Lawrence C. Paulson; Frank Theiss; Arnaud Fietzke (2008). "LEO-II - un demostrador de teorema automático cooperativo para la lógica clásica de orden superior (descripción del sistema)" (PDF) . LNCS . Apuntes de conferencias en informática. 4ª Conferencia conjunta internacional sobre razonamiento automatizado, IJCAR 2008 Sydney, Australia: Springer. 5195 : 162-170. doi : 10.1007 / 978-3-540-71070-7_14 . ISBN 978-3-540-71069-1. Archivado desde el original (PDF) el 15 de junio de 2011 . Consultado el 20 de diciembre de 2009 .Mantenimiento de CS1: ubicación ( enlace )
- ^ Korovin, Konstantin (2008). "iProver: un demostrador de teoremas basado en instancias para la lógica de primer orden (descripción del sistema)" (PDF) . LNCS . Apuntes de conferencias en informática. Saltador. 5195 : 292-298. doi : 10.1007 / 978-3-540-71070-7_24 . ISBN 978-3-540-71069-1. Consultado el 18 de diciembre de 2009 .[ enlace muerto permanente ]
- ^ Ramachandran, Deepak; Pace Reagan; Keith Goolsbery (2005). "ResearchCyc de primer orden: expresividad y eficiencia en una ontología de sentido común" (PDF) . Taller AAAI de Contextos y Ontologías: Teoría, Práctica y Aplicaciones . AAAI.
- ^ Ranise, Silvio; David Déharbe (2003). "Aplicación del teorema de peso ligero probando a depurar y verificar programas de puntero" . ENTCS . IV Taller Internacional de Demostración de Teoremas de Primer Orden: Elsevier. 86 (1): 109-119. doi : 10.1016 / S1571-0661 (04) 80656-X .Mantenimiento de CS1: ubicación ( enlace )
- ^ Denney, Ewen; Bernd Fischer; Johan Schumann (2006). "Una evaluación empírica de probadores de teoremas automatizados en la certificación de software" . Revista Internacional de Herramientas de Inteligencia Artificial . 15 (1): 81-107. CiteSeerX 10.1.1.163.4861 . doi : 10.1142 / s0218213006002576 .
enlaces externos
- E página de inicio
- Desarrollador de E