Tietoa

Ohje ja dokumentaatio

Aloittaessasi tyhjästä, HOL:n käytön opetteluun menee keskimäärin noin kuukausi.Monet ihmiset oppivat alla mainituista opetusohjelmista ja oppaista sekä yhteisön tuesta.

Missä aloittaa?

Ensin pitäisi opetella toimimaan vuorovaikutuksessa HOL4:n kanssa.

Missä aloittaa?

Ensin pitäisi opetella toimimaan vuorovaikutuksessa HOL4:n kanssa.

Emacs-käyttäjiä varten on olemassa 11-sivuinen opas vuorovaikutukseen HOL:n kanssa ja perustodennäköisyyksiin HOL:lla Emacsin avulla.Siellä on myös sivu, jossa on kattavampi dokumentaatio Emacs-tilasta.Vim-käyttäjien kannattaa tutustua Vim-liitännäisen dokumentaatioon.

Toinen hyvä resurssi vasta-alkajille on Tutorial.se tarjoaa johdannon järjestelmään uusille käyttäjille sekä yksityiskohtaiset asennusohjeet.tutorial on saatavana myös italiaksi.

Keväällä 2017 KTH:lla pidettiin edistyneemmille maisteriopiskelijoille suunnattu kurssi HOL:sta. Kurssi tähtäsi PROSPER-projektin tarpeisiin ja pyrki tarjoamaan käytännön kokemusta HOL:sta. Diat (tulostinystävällinen versio, LaTeX-lähteet) sekä harjoituslomakkeet ovat saatavilla. Lisätietoa löytyy kurssin verkkosivuilta.

Tässä on myös työn alla oleva opaskirja, joka pyrkii esittämään lempeän mutta kattavan selostuksen järjestelmästä.

Tässä on myös usein kysyttyjä kysymyksiä (FAQ), jotka voivat auttaa vianetsinnässä.

Syvällinen dokumentaatio

Kuvausoppaassa on yksityiskohtainen kuvaus kaikista HOL:n mahdollisuuksista.Tämä sisältää korkean tason kirjastojen lisäksi myös joitakin HOL:n API:n keskeisiä ML-toimintoja.

Suuri osa HOL:n käyttäjistä käyttää online-referenssisivua dokumentaation etsimiseen työnsä aikana. Huomaa, että tästä sivusta rakennetaan paikallinen kopio, kun asennat HOL:n. Tämä sivu sijaitsee osoitteessa HOL/help/HOLindex.html, jossa HOL on HOL-asennuksesi juuripaikka. Viite on olemassa myös PDF-dokumenttina.

Logiikan käsikirja (saatavilla myös italiaksi) tarjoaa yksityiskohtaisen matemaattisen kuvauksen korkeamman asteen logiikasta, sellaisena kuin se on toteutettu HOL:ssa. Erityisesti se esittelee logiikan mallin ja sen määrittelyperiaatteet ZFC-joukkoteoriassa.