Om

Troutorial och dokumentation

Det tar i genomsnitt ungefär en månad att lära sig använda HOL från början.Många lär sig genom de handledningar och guideböcker som nämns nedan, tillsammans med stöd från gemenskapen.

Var ska man börja?

Man bör först lära sig att interagera med HOL4. För Emacs-användare finns det en 11-sidig guide om HOL-interaktion och grundläggande bevisföring med hjälp av Emacs.Det finns också en sida med mer fullständig dokumentation av Emacs-läget. Vim-användare kanske vill konsultera dokumentationen för Vim-pluginet.

En annan bra resurs för nykomlingar är handledningen.Den ger en introduktion till systemet för nya användare samt detaljerade installationsinstruktioner.Handledningen finns också tillgänglig på italienska.

Under våren 2017 gavs en kurs för avancerade masterstudenter om HOL på KTH. Kursen var inriktad på behoven i PROSPER-projektet och försökte ge praktisk erfarenhet av HOL. Slides (skrivarvänlig version, LaTeX-källor) samt övningsblad finns tillgängliga. Mer information finns på kursens webbsida.

Det finns också en Guidebook som håller på att utarbetas och som syftar till att presentera en försiktig men omfattande redogörelse för systemet.

Det finns också en FAQ som kan hjälpa till vid felsökning.

Djupgående dokumentation

Beskrivningsmanualen ger en detaljerad beskrivning av alla HOL:s faciliteter. detta inkluderar inte bara högnivåbibliotek utan även några av de centrala ML-funktionerna i HOL:s API.

De flesta HOL-användare använder online-referenssidan för att leta upp dokumentation medan de arbetar. Observera att en lokal kopia av denna sida byggs när du installerar HOL. Den här sidan finns på HOL/help/HOLindex.html, där HOL är roten till din HOL-installation. Referensen finns också som ett PDF-dokument.

Handboken Logik (finns också på italienska) ger en detaljerad matematisk beskrivning av logik av högre ordning, så som den är implementerad i HOL. Den visar särskilt en modell för logiken och dess definitionsprinciper i ZFC:s mängdteori.