Acerca de

Tutoriales y documentación

Comenzando desde cero, se tarda una media de un mes en sentirse cómodo utilizando HOL.Mucha gente aprende con los tutoriales y guías que se mencionan a continuación, junto con el apoyo de la comunidad.

¿Por dónde empezar?

Primero hay que aprender a interactuar con HOL4.Para los usuarios de Emacs, hay una guía de 11 páginas sobre la interacción con HOL y las pruebas básicas usando Emacs.También hay una página con documentación más completa del modo Emacs.Los usuarios de Vim podrían consultar la documentación del plugin de Vim.

Otro buen recurso para los recién llegados es el Tutorial.Proporciona una introducción al sistema para los nuevos usuarios, así como instrucciones detalladas de instalación.El tutorial también está disponible en italiano.

En la primavera de 2017 se impartió en el KTH un curso para estudiantes de máster avanzado sobre HOL. El curso tenía como objetivo las necesidades del proyecto PROSPER y trató de proporcionar algo de experiencia práctica con HOL. Las diapositivas (versión para imprimir, fuentes LaTeX) así como las hojas de ejercicios están disponibles. Se puede encontrar más información en la página web del curso.

También hay una Guía en proceso de elaboración que pretende presentar una descripción suave pero completa del sistema.

También hay un FAQ que puede ayudar a solucionar problemas.

Documentación en profundidad

El manual de Descripción proporciona una descripción detallada de todas las facilidades de HOL. Esto incluye no sólo las bibliotecas de alto nivel, sino también algunas de las funciones principales de ML en la API de HOL.

La mayoría de los usuarios de HOL utilizan la página de referencia en línea para buscar documentación mientras trabajan. Tenga en cuenta que una copia local de esta página se construye cuando se instala HOL. Esta página se encuentra en HOL/help/HOLindex.html, donde HOL es la raíz de su instalación de HOL. La referencia también existe como un documento PDF.

El manual de Lógica (también disponible en italiano) proporciona una descripción matemática detallada de la lógica de orden superior, tal como se implementa en HOL. En particular, muestra un modelo para la lógica y sus principios de definición en la teoría de conjuntos ZFC.