About

Tutorial and Documentation

Zaczynając od zera, potrzeba średnio około miesiąca, aby zacząć komfortowo używać HOL.Wiele osób uczy się z samouczków i przewodników wymienionych poniżej, wraz ze wsparciem ze strony społeczności.

Gdzie zacząć?

Najpierw należy nauczyć się interakcji z HOL4.Dla użytkowników Emacsa, jest 11-stronicowy przewodnik po interakcji z HOL i podstawowym dowodzie przy użyciu Emacsa.Istnieje również strona z bardziej kompletną dokumentacją trybu Emacs.Użytkownicy Vim mogą chcieć zapoznać się z dokumentacją wtyczki Vim.

Innym dobrym źródłem dla nowych użytkowników jest Tutorial.Zapewnia on wprowadzenie do systemu dla nowych użytkowników, jak również szczegółowe instrukcje instalacji.Tutorial jest również dostępny w języku włoskim.

Wiosną 2017 roku w KTH odbył się kurs dla zaawansowanych studentów magisterskich na temat HOL. Kurs miał na celu zaspokojenie potrzeb projektu PROSPER i próbował dostarczyć trochę praktycznego doświadczenia z HOL. Slajdy (wersja przyjazna dla drukarki, źródła LaTeX), jak również arkusze ćwiczeń są dostępne. Więcej informacji można znaleźć na stronie kursu.

Istnieje również przewodnik (work-in-progress Guidebook), którego celem jest przedstawienie łagodnego, ale wyczerpującego opisu systemu.

Istnieje również FAQ, który może pomóc w rozwiązywaniu problemów.

Dokładna dokumentacja

Podręcznik Opis zawiera szczegółowy opis wszystkich obiektów HOL-a. Obejmuje on nie tylko biblioteki wysokiego poziomu, ale także niektóre z podstawowych funkcji ML w HOL API.

Większość użytkowników HOL-a używa strony z referencjami online do przeglądania dokumentacji podczas pracy. Zauważ, że lokalna kopia tej strony jest tworzona podczas instalacji HOL-a. Ta strona znajduje się pod adresem HOL/help/HOLindex.html, gdzie HOL jest korzeniem twojej instalacji HOL. Odniesienie istnieje również jako dokument PDF.

Podręcznik Logika (dostępny również w języku włoskim) dostarcza szczegółowego matematycznego opisu logiki wyższego rzędu, tak jak jest ona zaimplementowana w HOL. W szczególności, demonstruje model tej logiki i jej zasady definicyjne w teorii zbiorów ZFC.

.