stringtranslate.com

HOL (asistente de pruebas)

HOL ( Lógica de orden superior ) denota una familia de sistemas interactivos de demostración 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 solo se pueden crear nuevos objetos de este tipo utilizando las funciones de la biblioteca que corresponden a reglas de inferencia de 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 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 metalenguaje para sistemas de demostración de teoremas; de hecho, el nombre significa "Metalenguaje".

Lógica subyacente

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 entendida. [1]

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

Implementaciones HOL

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 HOL original, dirigido por Mike Gordon . HOL88 incluyó su propia implementación de ML , que a su vez se implementó sobre Common Lisp . Todos los sistemas que siguieron a HOL88 (HOL90, hol98 y HOL4) se implementaron en Standard ML ; mientras que hol98 está acoplado a Moscú ML , HOL4 se puede construir con Moscú ML o Poly/ML . Todos vienen con grandes bibliotecas de código de demostración de teoremas que implementan una automatización adicional además del 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 convencional 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: una colección de herramientas diseñadas para brindar soporte especial para trabajar con la notación Z para especificaciones formales. 5 de las 6 herramientas tienen licencia GNU GPL v2. El sexto (PPDaz) tiene licencia propietaria. [5]
  4. HOL Zero: una implementación minimalista centrada en la confiabilidad. HOL Zero tiene licencia GNU GPL 3+. [6]
  5. Candle: una implementación de HOL Light verificada de extremo a extremo además de CakeML. [7]

Desarrollos de pruebas formales.

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

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

Referencias

  1. ^ 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 prueba . Serie de Lógica Aplicada. vol. 27 (Segunda ed.). Dordrecht: Editores académicos de Kluwer. ISBN 978-1-4020-0763-7.
  2. ^ Tobías Nipkow ; Markus Wenzel; Lawrence C. Paulson (2002). Isabelle/HOL: un asistente de prueba para la lógica de orden superior . Berlín, Heidelberg: Springer-Verlag. ISBN 978-3-540-45949-1.
  3. ^ "Demostración interactiva de teoremas de HOL".
  4. ^ "Luz HOL".
  5. ^ "Obtener ProofPower".
  6. ↑ Ver archivo LICENCIA en el tarball Archivado el 3 de marzo de 2012 en Wayback Machine .
  7. ^ Abrahamsson, Oskar; Myreen, Magnus O.; Kumar, Ramana; Sewell, Thomas (2022). Andrónico, junio; de Moura, Leonardo (eds.). "Vela: una implementación verificada de HOL Light". 13.ª Conferencia Internacional sobre Demostración Interactiva de Teoremas (ITP 2022) . Procedimientos internacionales de informática de Leibniz (LIPIcs). 237 . Dagstuhl, Alemania: Schloss Dagstuhl – Leibniz-Zentrum für Informatik: 3:1–3:17. doi : 10.4230/LIPIcs.ITP.2022.3 . ISBN 978-3-95977-252-5. S2CID  251323103.
  8. ^ "PastelML".
  9. ^ Magnus O. Myreen; Michael JC Gordon. Implementaciones LISP verificadas en ARM, x86 y PowerPC (PDF) . TPHOL 2009. págs.
  10. ^ Peter Sewell; Sospechar a 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. S2CID  1999974.
  11. ^ Jade Alglave ; Anthony CJ Fox; Samin Ishtiaq; Magnus O. Myreen; Sosmitir a Sarkar; Peter Sewell; Francesco Zappa Nardelli. La semántica de la potencia y el código de máquina multiprocesador ARM (PDF) . HÚMEDO 2009. págs. 13-24.

Otras lecturas

enlaces externos