Sobre

Tutorial e Documentação

Começar do zero, leva em média cerca de um mês para se tornar confortável usando o HOL.Muitas pessoas aprendem com os tutoriais e guias mencionados abaixo, juntamente com o apoio da comunidade.

Onde começar?

A pessoa deve primeiro aprender a interagir com o HOL4.Para os utilizadores do Emacs, existe um guia de 11 páginas para a interacção com o HOL e provas básicas utilizando o Emacs.Há também uma página com documentação mais completa do modo Emacs. Os usuários do Emacs podem consultar a documentação do plugin Vim.

Outro bom recurso para recém-chegados é o Tutorial. Ele fornece uma introdução ao sistema para novos usuários, bem como instruções detalhadas de instalação. O tutorial também está disponível em italiano.

Na primavera de 2017 foi dado um curso para alunos de mestrado avançado sobre a HOL no KTH. O curso visou as necessidades do projecto PROSPER e tentou proporcionar alguma experiência prática com a HOL. Os slides (versão para impressão, fontes LaTeX), assim como as folhas de exercícios estão disponíveis. Mais informações podem ser encontradas na página web do curso.

Há também um guia de trabalho em progresso que visa apresentar um relato gentil mas abrangente do sistema.

Há também um FAQ que pode ajudar na resolução de problemas.

Documentação aprofundada

O manual de Descrição fornece uma descrição detalhada de todas as instalações da HOL. Isto inclui não só bibliotecas de alto nível, mas também algumas das principais funções ML na HOL API.

A maioria dos utilizadores da HOL utiliza a página de referência online para consultar a documentação enquanto trabalham. Note que uma cópia local desta página é construída quando você instala o HOL. Esta página está localizada em HOL/help/HOLindex.html, onde HOL é a raiz da sua instalação da HOL. A referência também existe como um documento PDF.

O manual de lógica (também disponível em italiano) fornece uma descrição matemática detalhada da lógica de ordem superior, uma vez que é implementada no HOL. Em particular, ele demonstra um modelo para a lógica e seus princípios definitivos na teoria do conjunto ZFC.