Isabelle-Befehle: Schnellreferenz für den interaktiven Theorembeweiser

Isabelle ist ein generischer, interaktiver Theorembeweiser (Proof Assistant), mit dem sich mathematische Sätze und Programmeigenschaften maschinell überprüfen lassen. Entwickelt wurde er ab Mitte der 1980er-Jahre von Lawrence C. Paulson an der University of Cambridge, aufbauend auf Robin Milners Edinburgh-LCF-System; der Name geht auf Gérard Huets Tochter zurück. Isabelle ist in Standard ML geschrieben und hat mit Isabelle/HOL (Higher-Order Logic) eine Hauptobjektlogik, in der die meisten formalen Verifikationen stattfinden.

Strukturierte Beweise mit Isar

Seit der Version von 1999 bietet Isabelle mit Isar eine strukturierte Beweissprache, die Beweise lesbar und nachvollziehbar macht:

lemma add_comm: "a + b = b + a"
proof -
  show ?thesis by (induct a) simp_all
qed

Klassische Beweisbefehle im apply-Stil: apply (rule r), apply auto, apply simp, apply (blast intro: …), abgeschlossen mit done.

Automatisierung

  • sledgehammer ruft externe automatische Beweiser (E, Vampire, Z3, Spass) auf und rekonstruiert gefundene Beweise in Isabelle — das Herzstück für produktives Arbeiten.
  • nitpick und quickcheck suchen Gegenbeispiele beziehungsweise Testinstanzen zu Behauptungen.
  • find_theorems und find_consts durchsuchen die vorhandene Wissensbasis; value und term evaluieren Ausdrücke.

Werkzeuge

isabelle build -b HOL
isabelle jedit -l HOL theory.thy
isabelle process -T theory

Das Archive of Formal Proofs (AFP) sammelt hunderte verifizierte Theorien. Berühmte Projekte auf Isabelle-Basis: der seL4-Mikrokernel und der CompCert-C-Compiler.

Verwandte Beweisassistenten sind Coq und Lean. Wer das Verhalten nebenläufiger Systeme als ausführbares Modell prüfen will, nutzt dafür TLA+; wer Prozessmodelle maschinell prüfen will, nutzt Promela mit dem Model Checker SPIN; wer automatisch nach Gegenbeispielen sucht, den Alloy Analyzer.