Über

Tutorial und Dokumentation

Wenn man bei Null anfängt, braucht man im Durchschnitt etwa einen Monat, um sich mit HOL vertraut zu machen.Viele Leute lernen mit Hilfe der unten erwähnten Tutorials und Leitfäden, zusammen mit der Unterstützung der Gemeinschaft.

Wo fange ich an?

Man sollte zuerst lernen, mit HOL4 zu interagieren.Für Emacs-Benutzer gibt es einen 11-seitigen Leitfaden zur HOL-Interaktion und zum grundlegenden Beweisen mit Emacs.Es gibt auch eine Seite mit einer ausführlicheren Dokumentation des Emacs-Modus.Vim-Benutzer können die Dokumentation für das Vim-Plugin konsultieren.

Eine weitere gute Ressource für Neulinge ist das Tutorial.Es bietet eine Einführung in das System für neue Benutzer sowie detaillierte Installationsanweisungen.Das Tutorial ist auch auf Italienisch verfügbar.

Im Frühjahr 2017 wurde an der KTH ein Kurs für fortgeschrittene Masterstudenten über HOL gegeben. Der Kurs zielte auf die Bedürfnisse des PROSPER-Projekts ab und versuchte, einige praktische Erfahrungen mit HOL zu vermitteln. Die Folien (druckerfreundliche Version, LaTeX-Quellen) sowie die Übungsblätter sind verfügbar. Weitere Informationen sind auf der Kurs-Webseite zu finden.

Es gibt auch ein in Arbeit befindliches Handbuch, das eine sanfte, aber umfassende Darstellung des Systems bieten soll.

Es gibt auch eine FAQ, die bei der Fehlersuche helfen kann.

Gründliche Dokumentation

Das Beschreibungshandbuch bietet eine detaillierte Beschreibung aller Möglichkeiten von HOL, nicht nur der High-Level-Bibliotheken, sondern auch einiger der ML-Kernfunktionen in der HOL-API.

Die meisten HOL-Benutzer verwenden die Online-Referenzseite, um während der Arbeit in der Dokumentation nachzuschlagen. Beachten Sie, dass eine lokale Kopie dieser Seite erstellt wird, wenn Sie HOL installieren. Diese Seite befindet sich unter HOL/help/HOLindex.html, wobei HOL das Stammverzeichnis Ihrer HOL-Installation ist. Die Referenz existiert auch als PDF-Dokument.

Das Logik-Handbuch (auch auf Italienisch verfügbar) bietet eine detaillierte mathematische Beschreibung der Logik höherer Ordnung, wie sie in HOL implementiert ist. Insbesondere demonstriert es ein Modell für die Logik und ihre Definitionsprinzipien in der ZFC-Mengentheorie.