Hispanopedia Wiki
Articulo de referencia

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 ecuacional y utiliza un parad...

Hispanopedia WikiContenido en espanolLectura gratuita

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 ecuacional y utiliza un paradigma puramente ecuacional. Se ha integrado en otros demostradores de teoremas y ha figurado entre los sistemas mejor clasificados en varias competiciones de demostración de teoremas. E fue desarrollado por Stephan Schulz, originalmente en el Grupo de Razonamiento Automatizado de la Universidad Técnica de Múnich , y actualmente en la Universidad Estatal Cooperativa de Baden-Württemberg en Stuttgart.

Sistema

El sistema se basa en el cálculo de superposición ecuacional . A diferencia de la mayoría de los demás demostradores actuales, la implementación utiliza un paradigma puramente ecuacional y simula inferencias no ecuacionales mediante inferencias de igualdad apropiadas. Las innovaciones significativas incluyen la reescritura de términos compartidos (donde se realizan 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 tipos . [ 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 demostrador ha tenido un desempeño consistentemente bueno 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 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 el "mejor sistema en 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. Junto con Vampire , SPASS , CVC4 y Z3 , constituye 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 el razonamiento sobre grandes ontologías, [ 17 ] la verificación de software, [ 18 ] y la certificación de software. [ 19 ]

Referencias

  1. ↑ Schulz, Stephan (2002). "E – Un demostrador de teoremas para genios". Journal of AI Communications . 15 (2/3): 111– 126.
  2. 1 2 Schulz, Stephan (2008). "Descripciones del sistema de participantes: E 1.0pre y EP 1.0pre" . Archivado del original el 15 de junio de 2009. Recuperado el 24 de marzo de 2009 .
  3. ↑ Schulz, Stephan (2004). "Descripción del sistema: E 0.81". Razonamiento automatizado . Notas de clase en ciencias de la computación. 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 control de búsqueda para la demostración de teoremas ecuacionales". KI 2001: Avances en inteligencia artificial . Notas de clase en ciencias de la computación. Vol. 2174. pp. 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 de teoremas ecuacionales E" . Recuperado el 24 de marzo de 2009 .
  7. ↑ Sutcliffe, Geoff. "The CADE ATP System Competition" . Archivado del original el 2 de marzo de 2009. Consultado el 24 de marzo de 2009 .
  8. ↑ "División de FOF de CASC en 2008" . Archivado del original el 15 de junio de 2009. Consultado el 19 de diciembre de 2009 .
  9. ↑ Sutcliffe, Geoff (2009). "La 4.ª competición de sistemas de demostración automática 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 del original el 29 de junio de 2010. Recuperado el 20 de julio de 2010 .
  11. ↑ Sutcliffe, Geoff (2011). "The CADE ATP System Competition" . Universidad de Miami. Archivado del original el 12 de agosto de 2011. Recuperado el 14 de agosto de 2011 .
  12. ↑ Paulson, Lawrence C. (2008). "Automatización para la prueba interactiva: técnicas, lecciones y perspectivas" (PDF) . Herramientas y técnicas para la verificación de la infraestructura del sistema: un volumen conmemorativo en honor del profesor Michael JC Gordon FRS : 29–30 . Recuperado el 19 de diciembre de 2009 .
  13. ↑ Meng, Jia; Lawrence C. Paulson ( 2004). Experimentos sobre el soporte de pruebas interactivas mediante resolución . Lecture Notes in Computer Science. Vol. 3097. Springer. pp. 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 IJCAR (PDF) . Archivado del original (PDF) el 17 de junio de 2009. Recuperado 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 lógica clásica de orden superior (Descripción del sistema)». Razonamiento automatizado (PDF) . Lecture Notes in Computer Science. Vol. 5195. Springer. pp. 162–170 . doi : 10.1007/978-3-540-71070-7_14 . ISBN   978-3-540-71069-1Archivado del 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 instanciación para lógica de primer orden». Razonamiento automatizado . Notas 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). "Ciclo de investigación 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 ligeros a la depuración y verificación de programas de punteros" . Electronic Notes in Theoretical Computer Science . 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}}: CS1 mantenimiento: ubicación ( enlace )
  19. ↑ Denney, Ewen; Bernd Fischer; Johan Schumann (2006). "Una evaluación empírica de los demostradores automáticos de teoremas 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 del original el 24 de febrero de 2012. Recuperado el 19 de diciembre de 2009 . 
  • Página de inicio E
  • El desarrollador de E