HOL ( Lógica de orden superior ) denota una familia de sistemas interactivos de prueba de teoremas que utilizan lógicas y estrategias de implementación similares (de orden superior) . Los sistemas de esta familia siguen el enfoque LCF , ya que se implementan como una biblioteca que define un tipo de datos abstractos de teoremas probados, de modo que los nuevos objetos de este tipo solo pueden crearse utilizando las funciones de la biblioteca que corresponden a las reglas de inferencia en orden superior. lógica . Siempre que estas funciones se implementen correctamente, todos los teoremas probados en el sistema deben ser válidos. Como tal, se puede construir un sistema grande sobre un kernel de confianza pequeño.
Diseñada por | Michael JC Gordon |
---|---|
Licencia | Licencia BSD modificada (3 cláusulas) |
Extensiones de nombre de archivo | .sml |
Sitio web | hol-teorema-prover |
Los sistemas de la familia HOL utilizan ML o sus sucesores. ML se desarrolló originalmente junto con LCF como un metalenguaje para sistemas de demostración de teoremas; de hecho, el nombre significa "Meta-Lenguaje".
Lógica subyacente
Los sistemas HOL utilizan variantes de la lógica clásica de orden superior , que tiene bases axiomáticas simples con pocos axiomas y semántica bien entendida. [1]
La lógica utilizada en los probadores de HOL está estrechamente relacionada con Isabelle / HOL, [2] la lógica más utilizada de Isabelle .
Miembros de la familia de probadores HOL
Hay cuatro sistemas HOL (que comparten esencialmente la misma lógica) que aún se mantienen y desarrollan.
- El primero, HOL4, proviene del sistema HOL88, que fue la culminación del esfuerzo de implementación de HOL original, dirigido por Mike Gordon . HOL88 incluyó su propia implementación de ML, que a su vez se implementó sobre Common Lisp . Todas las implementaciones que siguieron a HOL88 (HOL90, hol98 y HOL4) utilizaron ML estándar como lenguaje de implementación. El sistema hol98 está vinculado a la implementación del ML estándar de Moscú ; HOL4 se puede construir con Moscow ML o Poly / ML . De estos cuatro sistemas, solo se está manteniendo y desarrollando HOL4. Todos vienen con grandes bibliotecas de código de prueba de teoremas. Estos implementan una automatización adicional además del código central muy simple. HOL4 tiene licencia BSD. [3]
- La segunda implementación actual es HOL Light . Esto comenzó como una versión experimental "minimalista" de HOL. Aunque posteriormente se ha convertido en otra variante HOL convencional, sus fundamentos lógicos siguen siendo inusualmente simples. HOL Light solía implementarse en Caml Light , pero ahora usa OCaml . HOL Light está disponible bajo la nueva licencia BSD. [4]
- La tercera implementación actual es ProofPower, una colección de herramientas diseñadas para proporcionar soporte especial para trabajar con la notación Z para la especificación formal. 5 de las 6 herramientas tienen licencia GNU GPL v2. El sexto (PPDaz) tiene una licencia propietaria. [5]
- El cuarto es HOL Zero , una implementación minimalista centrada en la confiabilidad. HOL Zero tiene licencia GNU GPL 3+. [6]
Aunque HOL es un predecesor de Isabelle , varios derivados de HOL como HOL4 y HOL Light permanecen activos y en uso.
Desarrollos de pruebas formales seleccionados
El proyecto CakeML [7] desarrolló un compilador probado formalmente para ML. Anteriormente, HOL se utilizó para desarrollar una implementación LISP probada formalmente que se ejecuta en ARM, x86 y PowerPC. [8]
HOL también se utilizó para desarrollar semántica formal para multiprocesadores x86, [9] así como semántica de código de máquina para arquitecturas Power ISA y ARM . [10]
Referencias
- ^ Andrews, Peter B (2002). Una introducción a la lógica matemática y la teoría de tipos: a la verdad a través de la demostración . Serie de lógica aplicada. 27 (Segunda ed.). Dordrecht: Kluwer Academic Publishers. ISBN 978-1-4020-0763-7.
- ^ Tobias Nipkow ; Markus Wenzel; Lawrence C. Paulson (2002). Isabelle / HOL: Asistente de pruebas para lógica de orden superior . Berlín, Heidelberg: Springer-Verlag. ISBN 978-3-540-45949-1.
- ^ "Demostrador de teoremas interactivo HOL" .
- ^ "Luz HOL" .
- ^ "Obteniendo ProofPower" .
- ^ Ver archivo de LICENCIA en el tarball. Archivado el 3 de marzo de 2012 en Wayback Machine .
- ^ "CakeML" .
- ^ Magnus O. Myreen; Michael JC Gordon. Implementaciones LISP verificadas en ARM, x86 y PowerPC (PDF) . TPHOLs 2009. págs. 359–374.
- ^ Peter Sewell; Susmit Sarkar; Scott Owens; Francesco Zappa Nardelli; Magnus O. Myreen (2010). "x86-TSO: un modelo de programador riguroso y utilizable para multiprocesadores x86" (PDF) . Comunicaciones de la ACM . 53 (7): 89–97. doi : 10.1145 / 1785414.1785443 .
- ^ Jade Alglave; Anthony CJ Fox; Samin Ishtiaq; Magnus O. Myreen; Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli. La semántica de la potencia y el código de máquina multiprocesador ARM (PDF) . DAMP 2009. págs. 13-24.
Otras lecturas
- Gordon, Michael JC (1996). "De LCF a HOL: una breve historia" . Consultado el 11 de octubre de 2007 .
enlaces externos
- Página de inicio del proyecto HOL4
- Documentos que especifican la lógica básica de HOL
- El manual de descripción de HOL4 , que incluye una especificación de la lógica del sistema.
- Información de métodos formales de la biblioteca virtual