stringtranslate.com

HOL (asistente de pruebas)

HOL ( Higher Order Logic ) denota una familia de sistemas interactivos de demostración de teoremas que utilizan lógicas (de orden superior) y estrategias de implementación similares . Los sistemas de esta familia siguen el enfoque LCF , ya que se implementan como una biblioteca que define un tipo de datos abstracto de teoremas demostrados de modo que solo se puedan crear nuevos objetos de este tipo 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. 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 un metalenguaje para sistemas de demostración de teoremas; de hecho, el nombre significa "Meta-Language" (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 probadores 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 mantenido y desarrollado actualmente que se deriva del sistema HOL88, que fue la culminación del esfuerzo de implementación original de HOL, liderado por Mike Gordon . HOL88 incluyó su propia implementación de ML , que a su vez se implementó sobre Common Lisp . Los sistemas que siguieron a HOL88 (HOL90, hol98 y HOL4) se implementaron todos 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 convencional de HOL; sus fundamentos lógicos siguen siendo inusualmente simples. HOL Light, originalmente implementado en Caml Light , ahora utiliza 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. Cinco de las seis herramientas tienen licencia GNU GPL v2. La sexta (PPDaz) tiene una licencia propietaria. [5]
  4. HOL Zero: una implementación minimalista centrada en la confiabilidad. HOL Zero tiene licencia GNU GPL 3+. [6]
  5. Vela: una implementación de HOL Light verificada de extremo a extremo sobre CakeML. [7]

Desarrollos de prueba formal

El proyecto CakeML desarrolló un compilador probado formalmente para ML. [8] Anteriormente, HOL se utilizó para desarrollar una implementación de Lisp probada formalmente 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). Introducción a la lógica matemática y la teoría de tipos: hacia la verdad a través de la prueba . Serie de lógica aplicada. Vol. 27 (segunda edición). Dordrecht: Kluwer Academic Publishers. ISBN 978-1-4020-0763-7.
  2. ^ Tobias Nipkow ; Markus Wenzel; Lawrence C. Paulson (2002). Isabelle/HOL: Un asistente de demostración para lógica de orden superior . Berlín, Heidelberg: Springer-Verlag. ISBN 978-3-540-45949-1.
  3. ^ "Demostrador de teoremas interactivo HOL".
  4. ^ "Luz HOL".
  5. ^ "Obteniendo ProofPower".
  6. ^ Ver el archivo LICENCIA en el archivo tar Archivado el 3 de marzo de 2012 en Wayback Machine .
  7. ^ Abrahamsson, Oskar; Myreen, Magnus O.; Kumar, Ramana; Sewell, Thomas (2022). Andronick, June; de ​​Moura, Leonardo (eds.). "Candle: A Verified Implementation of HOL Light". 13.ª Conferencia internacional sobre demostración interactiva de teoremas (ITP 2022) . Leibniz International Proceedings in Informatics (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. Número de identificación del sujeto  251323103.
  8. ^ "CakeML".
  9. ^ Magnus O. Myreen; Michael JC Gordon. Implementaciones de LISP verificadas en ARM, x86 y PowerPC (PDF) . TPHOLs 2009. págs. 359–374.
  10. ^ 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. S2CID  1999974.
  11. ^ 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.

Lectura adicional

Enlaces externos