Rólunk

Tutorial és dokumentáció

A nulláról indulva átlagosan körülbelül egy hónapot vesz igénybe, hogy a HOL használatába beletanuljunk.Sokan az alább említett tutorialokból és útmutatókból tanulnak, a közösség támogatásával együtt.

Hol kezdjem?

Először meg kell tanulni a HOL4-mal való interakciót.Az Emacs felhasználók számára van egy 11 oldalas útmutató a HOL interakcióról és az alapvető bizonyításról az Emacs használatával.Van egy oldal az Emacs-mód teljesebb dokumentációjával is.Vim-felhasználóknak a Vim plugin dokumentációját érdemes megnézni.

Egy másik jó forrás a kezdők számára a Tutorial.Az új felhasználók számára bevezetést nyújt a rendszerbe, valamint részletes telepítési utasításokat.A tutorial olasz nyelven is elérhető.

2017 tavaszán a KTH-n egy kurzust tartottak haladó mesterhallgatóknak a HOL-ról. A kurzus a PROSPER projekt igényeit célozta meg, és igyekezett gyakorlati tapasztalatokat nyújtani a HOL-lal kapcsolatban. A diák (nyomtatóbarát változat, LaTeX források), valamint a feladatlapok elérhetők. További információk a tanfolyam weboldalán találhatók.

Egy folyamatban lévő munkafolyamatban lévő Útmutatókönyv is van, amely a rendszer szelíd, de átfogó bemutatására törekszik.

Egy GYIK is van, amely segíthet a hibaelhárításban.

Mélyreható dokumentáció

A leíró kézikönyv részletes leírást nyújt a HOL összes lehetőségéről.Ez nemcsak a magas szintű könyvtárakat tartalmazza, hanem a HOL API néhány alapvető ML-funkcióját is.

A legtöbb HOL-felhasználó az online referenciaoldalt használja a dokumentáció keresésére munka közben. Vegye figyelembe, hogy ennek az oldalnak a helyi másolata a HOL telepítésekor létrejön. Ez az oldal a HOL/help/HOLindex.html címen található, ahol HOL a HOL telepítésének gyökere. A hivatkozás PDF dokumentumként is létezik.

A Logika kézikönyv (olasz nyelven is elérhető) részletes matematikai leírást ad a magasabb rendű logikáról, ahogyan az a HOL-ban implementálva van. Különösen a logika modelljét és definíciós elveit mutatja be a ZFC halmazelméletben.