HOL steht für Higher-Order Logic (Logik höherer Stufe) und bezeichnet zugleich eine Familie interaktiver Beweisassistenten, die auf das LCF-System (Logic for Computable Functions, Robin Milner, Edinburgh 1970er) zurückgehen. Kernidee: Ein minimaler, vertrauenswürdiger Kernel akzeptiert nur Schlussfolgerungen, die durch elementare Regeln abgesichert sind — jedes Theorem ist damit maschinell geprüft.
Die HOL-Familie
- HOL4 ist der aktiv weiterentwickelte Hauptnachkomme, läuft auf Poly/ML, Lizenz BSD, mit dem Build-Werkzeug Holmake.
- HOL Light (John Harrison, Cambridge/Microsoft) ist ein minimalistischer OCaml-Fork mit sehr kleinem Kernel (~400 Zeilen) — extrem hohe Vertrauenswürdigkeit.
- Isabelle/HOL ist der bekannteste Abkömmling der HOL-Ideen: Isabelle nutzt eine generische Logik-Infrastruktur und darauf aufgesetzt die HOL-Logik.
Arbeiten im Goalstack
poly # Poly/ML-REPL starten
Holmake # HOL4-Theorien bauen (make-Ersatz)
g `1 + 1 = 2`; # Goal setzen (Backticks um das Ziel)
e (REWRITE_TAC []);# Taktik anwenden
e (DECIDE_TAC); # arithmetische Entscheidungsprozedur
top_thm(); # bewiesenes Theorem anzeigenTypische Taktiken: REWRITE_TAC (mit Theoremen umschreiben), STRIP_TAC (Annahmen/Hüllen auflösen), GEN_TAC (Allquantor einführen), MESON_TAC/METIS_TAC (Prädikatenlogik-Suche), DECIDE_TAC/TAUT_TAC (Arithmetik/Aussagenlogik), Induct_on (strukturelle Induktion).
Einordnung
HOL beweist Korrektheitseigenschaften interaktiv — im Gegensatz zu Plattformen, die Beweise weitgehend automatisieren: Why3 verteilt Proof Obligations an Beweiser, und Coq, Lean und PVS verfolgen ähnliche Ansätze. In Verifikationsketten wie Frama-C mit ACSL-Spezifikationen übernimmt ein interaktiver Assistent die Ziele, die automatische Beweiser nicht schließen.
Verwandte Grundlagen: Isabelle-Befehle, Coq-Befehle, Lean-Befehle.