Hispanopedia Wiki
Articulo de referencia

Nutria (demostrador de teoremas)

OTTER ( Técnicas Organizadas para la Demostración de Teoremas e Investigación Efectiva [ 1 ] ) es un demostrador automático de teoremas desarrollado por William McCune en el Lab...

Hispanopedia WikiContenido en espanolLectura gratuita

OTTER ( Técnicas Organizadas para la Demostración de Teoremas e Investigación Efectiva [ 1 ] ) es un demostrador automático de teoremas desarrollado por William McCune en el Laboratorio Nacional Argonne en Illinois. Otter fue el primer demostrador de teoremas de alto rendimiento y amplia distribución para lógica de primer orden , y fue pionero en varias técnicas de implementación importantes. Otter es un acrónimo de Técnicas Organizadas para la Demostración de Teoremas e Investigación Efectiva .

Descripción

Otter se basa en la resolución y la paramodulación, con restricciones en el orden de los términos similares a las del cálculo de superposición . El probador también admite hiperresolución positiva y negativa , así como una estrategia de conjunto de soporte . La búsqueda de pruebas se basa en la saturación mediante una versión del algoritmo de cláusula dada y se controla mediante varias heurísticas. También existen metaheurísticas que determinan automáticamente los parámetros de búsqueda. [ 2 ] Otter también fue pionero en el uso de técnicas eficientes de indexación de términos para acelerar la búsqueda de socios de inferencia en conjuntos de cláusulas grandes. [ 3 ]

Otter se mantuvo muy estable durante varios años, pero ya no se desarrolla activamente. En noviembre de 2008, la última entrada en el registro de cambios databa del 14 de septiembre de 2004. El sucesor de Otter es Prover9 .

El software es de dominio público . La Universidad de Chicago ha renunciado a ejercer sus derechos de autor sobre este software, y el público puede usarlo, modificarlo y redistribuirlo (con o sin modificaciones). Sin embargo, «NI EL GOBIERNO DE LOS ESTADOS UNIDOS NI NINGUNA DE SUS AGENCIAS [...] GARANTIZAN QUE SU USO NO INFRINJA DERECHOS DE PROPIEDAD PRIVADA». [ 4 ]

Según Wos y Pieper, OTTER está escrito en aproximadamente 28.000 líneas de lenguaje de programación C. [ 5 ] : 89–91

Véase también

Notas

  1. ↑ McCune, William (2003). Manual de referencia de Otter 3.3 (PDF) . doi : 10.2172/822573 . OSTI 822573 . 
  2. ↑ McCune, William; Wos, Larry (1997). "Otter: Las encarnaciones de la competición CADE-13". Journal of Automated Reasoning . 18 (2): 211– 220. doi : 10.1023/A:1005843632307 .
  3. ↑ McCune, William (1992). "Experimentos con indexación de árboles de discriminación e indexación de rutas para la recuperación de términos". Journal of Automated Reasoning . 9 (2): 147– 167. doi : 10.1007/BF00245458 .
  4. ↑ Nombre del archivo Legal en el archivo tarball
  5. ↑ Wos, Larry; Pieper, Gail W. (1999). "3.11 OTTER y programas anteriores de demostración automática de teoremas". Un país fascinante en el mundo de la informática: su guía para el razonamiento automatizado . World Scientific. ISBN 978-9810239107.

Referencias

  • Kalman, John Arnold (febrero de 2001). Razonamiento automatizado con OTTER . Rinton Press. ISBN 978-1589490048.
  • Página principal de Otter
  • "Manual de referencia de OTTER 3.3" (PDF) . Archivado del original el 13/11/2018 . Consultado el 13/11/2018 .{{cite web}}: CS1 maint: bot: estado de la URL original desconocido ( enlace )