Despre

Tutorial și documentație

Începând de la zero, este nevoie în medie de aproximativ o lună pentru a deveni confortabil cu HOL.Mulți oameni învață din tutorialele și ghidurile menționate mai jos, împreună cu sprijinul comunității.

De unde să începi?

În primul rând ar trebui să înveți să interacționezi cu HOL4.Pentru utilizatorii Emacs, există un ghid de 11 pagini despre interacțiunea cu HOL și demonstrația de bază folosind Emacs.Există, de asemenea, o pagină cu o documentație mai completă a modului Emacs.Utilizatorii de Vim ar putea dori să consulte documentația pentru plugin-ul Vim.

O altă resursă bună pentru nou-veniți este Tutorialul.Acesta oferă o introducere în sistem pentru noii utilizatori, precum și instrucțiuni detaliate de instalare.Tutorialul este disponibil și în limba italiană.

În primăvara anului 2017, la KTH s-a ținut un curs pentru masteranzi avansați despre HOL. Cursul a vizat nevoile proiectului PROSPER și a încercat să ofere o anumită experiență practică cu HOL. Diapozitivele (versiune pentru imprimantă, surse LaTeX), precum și fișele de exerciții sunt disponibile. Mai multe informații pot fi găsite pe pagina web a cursului.

Există, de asemenea, un Ghid în curs de realizare, care își propune să prezinte o prezentare blândă, dar cuprinzătoare a sistemului.

Există, de asemenea, un FAQ care poate ajuta la depanare.

Documentație aprofundată

Manualul de descriere oferă o descriere detaliată a tuturor facilităților HOL.Aceasta include nu numai bibliotecile de nivel înalt, ci și unele dintre funcțiile ML de bază din API-ul HOL.

Majoritatea utilizatorilor HOL utilizează pagina de referință online pentru a consulta documentația în timp ce lucrează. Rețineți că o copie locală a acestei pagini este construită atunci când instalați HOL. Această pagină este localizată la HOL/help/HOLindex.html, unde HOL este rădăcina instalației HOL. Referința există și ca document PDF.

Manualul de logică (disponibil și în italiană) oferă o descriere matematică detaliată a logicii de ordin superior, așa cum este ea implementată în HOL. În special, acesta demonstrează un model pentru logică și principiile sale de definire în teoria seturilor ZFC.

.