Otter es un probador de teoremas automatizado desarrollado por William McCune en el Laboratorio Nacional Argonne en Illinois. Otter fue el primer demostrador de teoremas de alto rendimiento ampliamente distribuido para la lógica de primer orden , y fue pionero en varias técnicas de implementación importantes. Otter es un acrónimo de Organized Techniques for Theorem-Proving and Effective Research .
Autor (es) original (es) | William McCune |
---|---|
Escrito en | C |
Tipo | Demostración automatizada de teoremas |
Sitio web | www |
Descripción
Otter se basa en la resolución y la paramodulación, restringida por ordenamientos de términos similares a los del cálculo de superposición . El probador también apoya la hiperresolución positiva y negativa y una estrategia de apoyo . La búsqueda de pruebas se basa en la saturación utilizando una versión del algoritmo de cláusula dada y está controlada por varias heurísticas. También hay metaheurísticas que determinan los parámetros de búsqueda automáticamente. [1] Otter también fue pionera en el uso de técnicas eficientes de indexación de términos para acelerar la búsqueda de socios de inferencia en grandes conjuntos de cláusulas. [2]
Otter se ha mantenido muy estable durante varios años, pero ya no se desarrolla activamente. En noviembre de 2008, la última entrada del registro de cambios estaba fechada el 14 de septiembre de 2004. Un sucesor de Otter es Prover9 .
El software es de dominio público . La Universidad de Chicago se ha negado a hacer valer 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 AGENCIA DEL MISMO [...] REPRESENTA QUE SU USO NO INFRINGIRÍA LOS DERECHOS DE PROPIEDAD PRIVADA". [3]
Según Wos y Pieper, OTTER está escrito en aproximadamente 28.000 líneas de lenguaje de programación C. [4] : 89–91
Ver también
Notas
- ^ McCune, William; Larry Wos (1997). "Nutria: las encarnaciones de la competencia CADE-13". Revista de razonamiento automatizado . 18 (2): 211–220. doi : 10.1023 / A: 1005843632307 .
- ^ McCune, William (1992). "Experimentos con indexación de árboles de discriminación e indexación de rutas para la recuperación de términos". Revista de razonamiento automatizado . 9 (2): 147-167. doi : 10.1007 / BF00245458 .
- ^ Nombre de archivo Legal en el tarball
- ^ Wos, Larry; Pieper, Gail W. (1999). "3.11 OTTER y programas de demostración de teoremas automatizados anteriores". 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 . Prensa de Rinton. ISBN 978-1589490048.
enlaces externos
- Página de inicio de la nutria
- "Manual de referencia de OTTER 3.3" (PDF) . Archivado desde el original el 13 de noviembre de 2018 . Consultado el 13 de noviembre de 2018 .CS1 maint: bot: estado de URL original desconocido ( enlace )