Maschinengestütztes Beweisen

Maschinengestütztes Beweisen (oder missverständlicher: Automatisches Beweisen; ein Teilgebiet der automatischen Deduktion) basiert auf der Verwendung von Computerprogrammen zur Erzeugung und Überprüfung von mathematischen Beweisen von logischen Theoremen. Im Unterschied zu Computerbeweisen wird versucht, den gesamten formalen Beweis bestehend aus Schritten und Zwischenergebnissen zu konstruieren.^[1]

Problematik und theoretische Grenzen

Die Frage, ob ein formaler Beweis jedes Theorems in einer gegebenen Logik konstruiert werden kann, heißt Entscheidungsproblem. Abhängig von der zugrundegelegten Logik kann das Entscheidungsproblem von trivial bis unlösbar variieren. Für den Fall der Aussagenlogik ist das Problem entscheidbar (d. h. ein Beweis ist immer erzeugbar, wenn das Theorem logisch gültig ist, andernfalls wird die Ungültigkeit festgestellt), allerdings NP-vollständig. Dagegen ist Prädikatenlogik erster Stufe lediglich semi-entscheidbar, das heißt unter Verwendung von unbeschränkten Zeit- und Speicherressourcen kann ein gültiges Theorem bewiesen, ein ungültiges allerdings nicht immer als solches erkannt werden. Logik höherer Stufe (HOL) ist weder entscheidbar noch (bezüglich sog. Standardmodellen) vollständig.

Automatische Theorembeweiser

Trotz dieser theoretischen Grenzen sind praktisch verwendbare Automatische Theorembeweiser (ATP's) implementiert worden, die viele schwierige Probleme in diesen Logiken lösen können.

Während Theorembeweiser Beweise für Theoreme aus Axiomen über Inferenzschritte ableiten und in irgendeiner Form mathematische Beweise nachbilden, werden bei der Modellprüfung (model checking) zumeist raffiniert implementierte Techniken benutzt, Beweiszustände brute-force aufzuzählen und Suchräume von Beweiszuständen systematisch abzusuchen. Manche Systeme sind auch Hybride, die sowohl interaktive Beweisverfahren als auch Modellprüfung einsetzen.

Interaktive Theorembeweiser

Ein einfacheres, aber verwandtes Problem ist die Beweisüberprüfung, wo für einen gegebenen formalen Beweis nachgeprüft wird, ob er ein gegebenes Theorem tatsächlich beweist. Hierfür muss lediglich jeder einzelne Beweisschritt nachgeprüft werden, was in der Regel durch einfache primitiv-rekursive Funktionen möglich ist.

Interaktive Theorembeweiser, auch Beweis-Assistenten genannt, erfordern Hinweise für die Beweissuche, die von einem menschlichen Benutzer dem Beweissystem gegeben werden müssen. Abhängig vom Automatisierungsgrad kann dann ein Theorembeweiser im Wesentlichen auf einen Beweisprüfer reduziert werden, oder selbstständig bedeutsame Teile der Beweissuche automatisch durchführen. Interaktive Beweiser werden mittlerweile für vielfältige Aufgaben eingesetzt, deren Anwendungsbereich von reiner Mathematik über theoretische Informatik bis zu praktischen Problemen der Programmverifikation reicht.

Wissenschaftliche und industrielle Anwendungen

Bedeutende mathematische Beweise, die durch interaktive Theorembeweiser überprüft wurden, sind der Beweis des Vier-Farben-Satzes durch Georges Gonthier ^[2] (der den älteren Computerbeweis durch Appel und Haken ablöst) sowie der (zurzeit unvollendete) formalisierte Beweis der Keplerschen Vermutung durch das Flyspeck-Projekt.^[3] Aber auch automatische Theorembeweiser haben mittlerweile einige interessante und schwierige Probleme lösen können, deren Lösung in der Mathematik längere Zeit unbekannt war. Allerdings sind solche Erfolge eher sporadisch, die Bearbeitung von schwierigen Problemen erfordert zumeist interaktive Theorembeweiser.

Die industrielle Verwendung von Theorembeweisern oder Modellprüfern konzentriert sich zurzeit noch schwerpunktmäßig auf die Verifikation von integrierten Schaltkreisen und Prozessoren. Seitdem Fehler mit schweren wirtschaftlichen Auswirkungen in kommerziellen Prozessoren bekannt geworden sind (siehe Pentium-FDIV-Bug), werden ihre Recheneinheiten zumeist verifiziert. In den neuesten Prozessor-Versionen von AMD, Intel und anderen sind Theorembeweiser und Modellprüfer eingesetzt worden, um viele kritische Operationen in ihnen zu beweisen. Neuerdings werden Theorembeweiser auch zunehmend für die Software-Verifikation eingesetzt; große Projekte umfassen die Teil-Verifikation von Microsofts Hyper-V^[4] oder eine weitgehenden Verifikation des L4 (Mikrokern)^[5].

Verfügbare Implementierungen

Verfügbare Implementierungen für automatische Theorembeweiser sind z.B. Simplify, Z3 oder Alt-Ergo, die auf Prädikatenlogik basieren. Verfügbare Implementierungen für interaktive Theorembeweiser sind Isabelle und Coq, die Logiken höherer Stufe (HOL bzw. CC) verwenden.

Beispiele für Beweistechniken

• Resolution
• Termersetzung
• Modellprüfung
• Induktion
• Binäre Entscheidungsdiagramme

Literatur

• Thomas C. Hales Formal Proof, 55:11, Notices of the American Mathematical Society,1370-1382, 2008.
• Georges Gonthier: Formal Proof—The Four- Color Theorem, 55:11, Notices of the American Mathematical Society, 1384-1393, 2008.
• Dirk Leinenbach, Thomas Santen: Verifying the Microsoft Hyper-V Hypervisor with VCC, in: FM 2009: Formal Methods, Lecture Notes in Computer Science Volume 5850 (2009), 806-809, 2009. DOI: 10.1007/978-3-642-05089-3_51.
• Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood: seL4: Formal Verification of an OS Kernel, in: Communications of the ACM, 53:6, 2010. DOI: 10.1145/1629575.1629596.

Einzelnachweise

1. ↑ Vgl. Übersichtsartikel von T. Hales Formal Proof.
2. ↑ Vgl. Formal Proof—The Four- Color Theorem
3. ↑ Vgl. FLYSPECK bei blogspot.
4. ↑ Verifying the Microsoft Hyper-V Hypervisor with VCC
5. ↑ seL4: Formal Verification of an OS Kernel

Weblinks

Überblicksdarstellungen

• Frederic Portoraro: Automated Reasoning, in: Stanford Encyclopedia of Philosophy (englisch, inklusive Literaturangaben)