HOL (Höhere Ordnungslogik) zeigt eine Familie von interaktiven sich erweisenden Lehrsatz-Systemen an, die sich teilen

ähnliche (höherwertige) Logik und Durchführungsstrategien.

Systeme in dieser Familie folgen der LCF-Annäherung, weil sie als eine Bibliothek auf einer Programmiersprache durchgeführt werden.

Diese Bibliothek führt einen abstrakten Datentyp von bewiesenen Lehrsätzen durch, so dass neue Gegenstände dieses Typs nur mit den Funktionen in der Bibliothek geschaffen werden können, die Interferenzregeln in der höherwertigen Logik entsprechen. So lange diese Funktionen richtig durchgeführt werden, müssen alle im System bewiesenen Lehrsätze gültig sein. Auf diese Weise kann ein großes System oben auf einem kleinen vertrauten Kern gebaut werden.

Systeme in der HOL Familie verwenden die ML Programmiersprache oder seine Nachfolger. ML wurde zusammen mit LCF ursprünglich entwickelt, um dem Zweck einer Metasprache für Lehrsatz-Beweis-Systeme zu dienen; tatsächlich tritt der Name für "Metasprache" ein.

Mitglieder

Es gibt vier HOL Systeme (das Teilen im Wesentlichen derselben Logik), die noch aufrechterhalten und entwickelt werden.

• Das erste, HOL4 stammt vom HOL88 System, das der Höhepunkt der ursprünglichen HOL Durchführungsanstrengung war, die von Mike Gordon geführt ist. HOL88 hat seine eigene ML Durchführung eingeschlossen, die der Reihe nach oben auf dem Allgemeinen Lispeln durchgeführt wurde. Die Durchführungen im Anschluss an HOL88 (HOL90, hol98 und HOL4) der ganze verwendete Normale ML als die Durchführungssprache. Das hol98 System wird nach Moskau ML Durchführung von Normalem ML gebunden; HOL4 kann entweder mit Moskau ML oder mit Poly/ML gebaut werden. Dieser vier Systeme wird nur HOL4 aufrechterhalten und entwickelt. Alle kommen mit großen Bibliotheken des Lehrsatz-Beweis-Codes. Diese führen Extraautomation oben auf dem sehr einfachen Kerncode durch. HOL4 ist lizenzierter BSD.
• Die zweite aktuelle Durchführung ist HOL Licht. Das hat als eine experimentelle "Minimalist"-Version von HOL angefangen. Obwohl es nachher in eine HOL andere Hauptströmungsvariante hineingewachsen ist, bleiben seine logischen Fundamente ungewöhnlich einfach. HOL Licht hat gepflegt, im Caml Licht durchgeführt zu werden, aber verwendet jetzt OCaml. HOL Licht ist laut der neuen BSD-Lizenz verfügbar.
• Die dritte aktuelle Durchführung ist ProofPower, den eine Sammlung von Werkzeugen vorgehabt hat, spezieller Unterstützung zur Verfügung zu stellen, um mit der Z Notation für die formelle Spezifizierung zu arbeiten. 5 der 6 Werkzeuge sind GNU GPL v2 lizenziert. Das sechste (PPDaz) hat eine Eigentumslizenz.
• Das vierte ist HOL Null, eine Minimalist-Durchführung hat sich auf Zuverlässigkeit konzentriert. HOL Null ist GNU GPL 3 + hat lizenziert

HOL ist ein Vorgänger von Isabelle.

Links

• HOL4 Projekteinstiegsseite
• Dokumente, die die grundlegende Logik von HOL angeben
• Das HOL4 Beschreibungshandbuch, das eine Spezifizierung der Logik des Systems einschließt.
• Virtuelle Bibliothek formelle Methode-Information