__NOTOC__
Isabelle ist ein generischer interaktiver Theorembeweiser mit besonderem Schwerpunkt auf Higher-Order Logic (HOL). Ein wichtiger Anwendungsbereich von Isabelle ist die formale Verifizierung von Hard- und Software. Die Implementierungssprachen von Isabelle sind Standard ML und Scala. Das Basis-System unterliegt der BSD-Lizenz, während zusätzliche Komponenten unter Umständen andere Lizenzen für freie Software verwenden.
Am australischen Forschungsinstitut NICTA wurde mithilfe von Isabelle erstmals die Korrektheit eines Kernels (Secure Embedded L4 (seL4)) formal bewiesen. NICTA, 12. August 2009 pressetext.de, 17. August 2009 Bei einer Programmlänge von insgesamt 8700 Zeilen Code wurde die Korrektheit von 7500 Zeilen gezeigt; der Rest ist Boot-Code, der nur initial ausgeführt wird.Betriebssystem mit Korrektheitsbeweis. In: c’t, 19/2009, S. 50
Stand Mai 2026 wurden in Isabelle 92 von insgesamt 100 Sätzen von Freeks Liste formalisiert. Damit ist Isabelle hinter HOL Light (95 formalisierte Sätze) auf Platz 2. Dahinter kommen Lean (82 Sätze) und Rocq (80 Sätze).
Literatur Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle/HOL A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283, 2002, ISBN 3-540-43376-7. Lawrence C. Paulson: The foundation of a generic theorem prover. Journal of Automated Reasoning, Volume 5, Issue 3 (September 1989), S. 363–397, .
Weblinks Offizielle Webpräsenz Archive of Formal Proofs (Sammlung von Isabelle Beweisen)
Einzelnachweise
Kategorie:Freie Mathematik-Software Kategorie:Mathematische Logik