A propos

Tutoriel et documentation

En partant de zéro, il faut en moyenne environ un mois pour être à l’aise avec HOL.De nombreuses personnes apprennent grâce aux tutoriels et aux guides mentionnés ci-dessous, ainsi qu’au soutien de la communauté.

Où commencer ?

Il faut d’abord apprendre à interagir avec HOL4.Pour les utilisateurs d’Emacs, il existe un guide de 11 pages sur l’interaction avec HOL et la preuve de base en utilisant Emacs.Il y a également une page avec une documentation plus complète du mode Emacs.Les utilisateurs de Vim pourraient souhaiter consulter la documentation du plugin Vim.

Une autre bonne ressource pour les nouveaux arrivants est le Tutoriel.Il fournit une introduction au système pour les nouveaux utilisateurs, ainsi que des instructions d’installation détaillées.Le tutoriel est également disponible en italien.

Au printemps 2017, un cours pour les étudiants de master avancés sur HOL a été donné à KTH. Le cours visait à répondre aux besoins du projet PROSPER et a essayé de fournir une certaine expérience pratique avec HOL. Les diapositives (version imprimable, sources LaTeX) ainsi que les feuilles d’exercices sont disponibles. Plus d’informations peuvent être trouvées sur la page web du cours.

Il y a aussi un Guidebook work-in-progress qui vise à présenter un compte rendu doux mais complet du système.

Il y a aussi une FAQ qui peut aider au dépannage.

Documentation approfondie

Le manuel de description fournit une description détaillée de toutes les installations de HOL.Cela inclut non seulement les bibliothèques de haut niveau, mais aussi certaines des fonctions ML de base dans l’API de HOL.

La plupart des utilisateurs de HOL utilisent la page de référence en ligne pour consulter la documentation pendant qu’ils travaillent. Notez qu’une copie locale de cette page est construite lorsque vous installez HOL. Cette page est située à HOL/help/HOLindex.html, où HOL est la racine de votre installation HOL. La référence existe également sous forme de document PDF.

Le manuel de logique (également disponible en italien) fournit une description mathématique détaillée de la logique d’ordre supérieur, telle qu’elle est implémentée dans HOL. En particulier, il démontre un modèle pour la logique et ses principes définitionnels dans la théorie des ensembles ZFC.