HOL (asistente de pruebas)

HOL ( Lógica de Orden Superior ) designa una familia de sistemas interactivos de demostración de teoremas que emplean lógicas (de orden superior) y estrategias de implementación similares. Los sistemas de esta familia siguen el enfoque LCF (Lógica para Funciones Computables), ya que se implementan como una biblioteca que define un tipo de datos abstracto de teoremas demostrados, 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 lógica de orden superior . Siempre que estas funciones se implementen correctamente, todos los teoremas demostrados en el sistema deben ser válidos. De este modo, se puede construir un sistema grande sobre un núcleo pequeño y confiable.

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, su nombre significa "Meta-Lenguaje".

Los sistemas HOL utilizan variantes de la lógica clásica de orden superior , que tiene fundamentos axiomáticos simples con pocos axiomas y una semántica bien comprendida. ^{[ 1 ]}

La lógica utilizada en los probadores HOL está estrechamente relacionada con Isabelle/HOL, ^{[ 2 ]} la lógica más utilizada de Isabelle .

Varios sistemas HOL (que comparten esencialmente la misma lógica) permanecen activos y en uso:

1. HOL4 — el único sistema actualmente mantenido y desarrollado derivado del sistema HOL88, que fue la culminación del esfuerzo de implementación original de HOL, liderado por Mike Gordon . HOL88 incluía su propia implementación de ML , que a su vez estaba implementada sobre Common Lisp . Los sistemas que siguieron a HOL88 (HOL90, hol98 y HOL4) se implementaron en Standard ML ; mientras que hol98 está acoplado a Moscow ML , HOL4 se puede construir con Moscow ML o Poly/ML . Todos vienen con grandes bibliotecas de código de demostración de teoremas que implementan automatización adicional sobre el código central muy simple. HOL4 tiene licencia BSD. ^{[ 3 ]}
2. HOL Light — una versión experimental "minimalista" de HOL que desde entonces se ha convertido en otra variante popular de HOL; sus fundamentos lógicos siguen siendo inusualmente simples. HOL Light, implementado originalmente en Caml Light , ahora usa OCaml . HOL Light está disponible bajo la nueva licencia BSD. ^{[ 4 ]}
3. ProofPower es una colección de seis herramientas diseñadas para brindar soporte especializado basado en HOL para trabajar con la notación Z en la especificación formal. La herramienta PPDaz, que permite la especificación y verificación de programas escritos en un subconjunto de Ada, anteriormente solo se distribuía bajo una licencia propietaria. Ahora, todas las herramientas están disponibles bajo la licencia GNU GPL v2.
4. HOL Zero : una implementación minimalista centrada en la confiabilidad. HOL Zero tiene licencia GNU GPL 3+. ^{[ 5 ]}
5. Candle — Una implementación de HOL Light verificada de extremo a extremo sobre CakeML. ^{[ 6 ]}

El proyecto CakeML desarrolló un compilador formalmente probado para ML. ^{[ 7 ]} Anteriormente, HOL se utilizó para desarrollar una implementación de Lisp formalmente probada que se ejecutaba en ARM, x86 y PowerPC. ^{[ 8 ]}

HOL también se utilizó para formalizar la semántica de los multiprocesadores x86 ^{[ 9 ]} así como el código máquina para las arquitecturas Power ISA y ARM . ^{[ 10 ]}

• Gordon, Michael JC (1996). "De LCF a HOL: una breve historia" . Recuperado el 11 de octubre de 2007 .

• Sitio web oficial
• Documentos que especifican la lógica básica de HOL
• Manual de descripción de HOL4 , incluye la especificación de la lógica del sistema.
• Información sobre métodos formales de la biblioteca virtual