About

Tutorial e documentazione

Partendo da zero, ci vuole in media circa un mese per prendere confidenza con HOL.Molte persone imparano dai tutorial e dalle guide menzionate qui sotto, insieme al supporto della comunità.

Da dove cominciare?

Prima si dovrebbe imparare ad interagire con HOL4.Per gli utenti di Emacs, c’è una guida di 11 pagine all’interazione con HOL e alla dimostrazione di base usando Emacs.C’è anche una pagina con una documentazione più completa della modalità Emacs.Gli utenti Vim potrebbero voler consultare la documentazione per il plugin Vim.

Un’altra buona risorsa per i nuovi arrivati è il Tutorial.Esso fornisce un’introduzione al sistema per i nuovi utenti, così come istruzioni dettagliate per l’installazione.Il tutorial è disponibile anche in italiano.

Nella primavera 2017 è stato tenuto al KTH un corso per studenti master avanzati su HOL. Il corso mirava alle esigenze del progetto PROSPER e ha cercato di fornire alcune esperienze pratiche con HOL. Le diapositive (versione stampabile, fonti LaTeX) così come i fogli di esercizi sono disponibili. Maggiori informazioni possono essere trovate sulla pagina web del corso.

C’è anche una Guida in corso d’opera che mira a presentare un resoconto gentile ma completo del sistema.

C’è anche una FAQ che può aiutare nella risoluzione dei problemi.

Documentazione approfondita

Il manuale di descrizione fornisce una descrizione dettagliata di tutte le strutture di HOL, che include non solo le librerie di alto livello, ma anche alcune delle funzioni di base di ML nelle API di HOL.

La maggior parte degli utenti di HOL usa la pagina di riferimento online per cercare la documentazione mentre lavora. Si noti che una copia locale di questa pagina viene costruita quando si installa HOL. Questa pagina si trova a HOL/help/HOLindex.html, dove HOL è la radice della tua installazione di HOL. Il riferimento esiste anche come documento PDF.

Il manuale Logic (disponibile anche in italiano) fornisce una dettagliata descrizione matematica della logica di ordine superiore, come è implementata in HOL. In particolare, dimostra un modello per la logica e i suoi principi definitori nella teoria degli insiemi ZFC.