stringtranslate.com

E (Demostrador de teoremas)

E es un demostrador de teoremas de alto rendimiento para lógica de primer orden completa 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 demostradores de teoremas y ha estado entre los sistemas mejor ubicados en varias competiciones de demostración de teoremas. E fue desarrollado por Stephan Schulz, originalmente en el Grupo de Razonamiento Automatizado de la 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 demás probadores actuales, la implementación utiliza en realidad 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 se llevan a cabo muchas simplificaciones ecuacionales posibles 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 múltiples ordenamientos . [5]

E está implementado en C y es portable a la mayoría de las variantes de UNIX y al entorno Cygwin . Está disponible bajo la licencia GNU GPL . [6]

Competiciones

El probador ha tenido un buen desempeño consistente en la Competencia de Sistemas ATP de CADE , 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 de primer orden completa) y UEQ (lógica ecuacional unitaria) 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 general". [10] En el CASC-23 E de 2011 ganó la división CNF y logró segundos lugares en UEQ y LTB. [11]

Aplicaciones

E se ha integrado en varios otros demostradores de teoremas. Es, junto 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. [16]

Las aplicaciones de E incluyen razonamiento sobre grandes ontologías, [17] verificación de software, [18] y certificación de software. [19]

Referencias

  1. ^ Schulz, Stephan (2002). "E – Un demostrador de teoremas de Brainiac". Revista de comunicaciones de IA . 15 (2/3): 111–126.
  2. ^ ab Schulz, Stephan (2008). "Descripciones del sistema de participantes: E 1.0pre y EP 1.0pre". Archivado desde el original el 15 de junio de 2009. Consultado el 24 de marzo de 2009 .
  3. ^ Schulz, Stephan (2004). "Descripción del sistema: E 0,81". Razonamiento automatizado . Apuntes de clase en informática. Vol. 3097. págs. 223-228. doi :10.1007/978-3-540-25984-8_15. ISBN 978-3-540-22345-0.
  4. ^ Schulz, Stephan (2001). "Aprendizaje del conocimiento de control de búsqueda para la demostración de teoremas ecuacionales". KI 2001: Avances en inteligencia artificial . Apuntes de clase en informática. Vol. 2174. págs. 320–334. doi :10.1007/3-540-45422-5_23. ISBN 978-3-540-42612-7.
  5. ^ "noticias en el sitio web de E" . Consultado el 10 de julio de 2017 .
  6. ^ Schulz, Stephan (2008). "El demostrador del teorema de ecuaciones E" . Consultado el 24 de marzo de 2009 .
  7. ^ Sutcliffe, Geoff. "La competición del sistema CADE ATP". Archivado desde el original el 2 de marzo de 2009. Consultado el 24 de marzo de 2009 .
  8. ^ "División FOF de CASC en 2008". Archivado desde el original el 15 de junio de 2009. Consultado el 19 de diciembre de 2009 .
  9. ^ Sutcliffe, Geoff (2009). "La 4ª Competición de Sistemas Automatizados de Demostración de Teoremas de IJCAR - CASC-J4". AI Communications . 22 (1): 59–72. doi :10.3233/AIC-2009-0441 . Consultado el 16 de diciembre de 2009 .
  10. ^ Sutcliffe, Geoff (2010). "The CADE ATP System Competition". Universidad de Miami. Archivado desde el original el 29 de junio de 2010. Consultado el 20 de julio de 2010 .
  11. ^ Sutcliffe, Geoff (2011). "The CADE ATP System Competition". Universidad de Miami. Archivado desde el original el 12 de agosto de 2011. Consultado el 14 de agosto de 2011 .
  12. ^ 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 homenaje en honor al profesor Michael JC Gordon FRS : 29–30 . Consultado el 19 de diciembre de 2009 .
  13. ^ Meng, Jia; Lawrence C. Paulson (2004). Experimentos para respaldar la demostración interactiva mediante resolución . Lecture Notes in Computer Science. Vol. 3097. Springer. págs. 372–384. CiteSeerX 10.1.1.62.5009 . doi :10.1007/978-3-540-25984-8_28. ISBN .  978-3-540-22345-0.
  14. ^ Sutcliffe, Geoff; et al. (2009). La 4ª Competición del Sistema ATP de la IJCAR (PDF) . Archivado desde el original (PDF) el 17 de junio de 2009 . Consultado el 18 de diciembre de 2009 .
  15. ^ Benzmüller, Christoph; Lawrence C. Paulson; Frank Theiss; Arnaud Fietzke (2008). "LEO-II – Un demostrador automático cooperativo de teoremas para la lógica clásica de orden superior (descripción del sistema)". Razonamiento automatizado (PDF) . Apuntes de clase en informática. Vol. 5195. Springer. págs. 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 .
  16. ^ Korovin, Konstantin (2008). "iProver: un demostrador de teoremas basado en instancias para lógica de primer orden". Razonamiento automatizado . Apuntes de clase en informática. Vol. 5195. págs. 292–298. doi :10.1007/978-3-540-71070-7_24. ISBN 978-3-540-71069-1.
  17. ^ Ramachandran, Deepak; Pace Reagan; Keith Goolsbery (2005). "Investigación cíclica de primer orden: expresividad y eficiencia en una ontología de sentido común" (PDF) . Taller de la AAAI sobre contextos y ontologías: teoría, práctica y aplicaciones . AAAI.
  18. ^ Ranise, Silvio; David Déharbe (2003). "Aplicación de la demostración de teoremas de peso ligero a la depuración y verificación de programas de puntero". Notas electrónicas en informática teórica . 86 (1). 4º Taller internacional sobre demostración de teoremas de primer orden: Elsevier: 109–119. doi : 10.1016/S1571-0661(04)80656-X .{{cite journal}}: Mantenimiento de CS1: ubicación ( enlace )
  19. ^ Denney, Ewen; Bernd Fischer; Johan Schumann (2006). "Una evaluación empírica de los demostradores de teoremas automatizados en la certificación de software". Revista internacional sobre herramientas de inteligencia artificial . 15 (1): 81–107. CiteSeerX 10.1.1.163.4861 . doi :10.1142/s0218213006002576. Archivado desde el original el 24 de febrero de 2012 . Consultado el 19 de diciembre de 2009 . 

Enlaces externos