Over

Tutorial en Documentatie

Van nul af aan beginnen, duurt het gemiddeld ongeveer een maand om vertrouwd te raken met HOL.Veel mensen leren het van de hieronder genoemde tutorials en handleidingen, samen met de steun van de gemeenschap.

Waar te beginnen?

Met HOL4 moet men eerst leren omgaan.Voor Emacs gebruikers is er een 11 pagina’s tellende gids voor HOL interactie en basis bewijzen met Emacs.Er is ook een pagina met meer volledige documentatie van de Emacs-modus.Vim-gebruikers zouden de documentatie voor de Vim-plugin kunnen raadplegen.

Een andere goede bron voor nieuwkomers is de Tutorial.Het biedt een inleiding tot het systeem voor nieuwe gebruikers, evenals gedetailleerde installatie-instructies.De tutorial is ook beschikbaar in het Italiaans.

In het voorjaar van 2017 werd een cursus voor gevorderde masterstudenten over HOL gegeven aan de KTH. De cursus was gericht op de behoeften van het PROSPER project en probeerde enige hands-on ervaring met HOL te bieden. Zowel de slides (printervriendelijke versie, LaTeX bronnen) als de oefenbladen zijn beschikbaar. Meer informatie is te vinden op de webpagina van de cursus.

Er is ook een werk-in-uitvoering Guidebook dat probeert een zachte maar uitgebreide uiteenzetting van het systeem te geven.

Er is ook een FAQ die kan helpen bij het oplossen van problemen.

Diepgaande documentatie

De Description manual geeft een gedetailleerde beschrijving van alle faciliteiten van HOL. Dit omvat niet alleen de high-level libraries, maar ook een aantal van de kern ML functies in de HOL API.

De meeste HOL gebruikers gebruiken de online referentie pagina om documentatie op te zoeken terwijl ze werken. Merk op dat een lokale kopie van deze pagina wordt gebouwd wanneer u HOL installeert. Deze pagina bevindt zich op HOL/help/HOLindex.html, waarbij HOL de root van uw HOL-installatie is. De referentie bestaat ook als PDF document.

De Logic handleiding (ook beschikbaar in het Italiaans) geeft een gedetailleerde wiskundige beschrijving van hogere-orde logica, zoals deze is geïmplementeerd in HOL. In het bijzonder demonstreert het een model voor de logica en zijn definitionele principes in ZFC set theory.