Maschinengestütztes Beweisen

Theorembeweisen (auch: maschinengestütztes Beweisen, oder mißverstä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. Abhängig von der zugrundegelegten Logik kann das Entscheidungsproblem eines Theorems 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), allerdings NP-vollständig, d.h. nur Algorithmen mit exponentiellen Zeitverbrauch sind bekannt. Dagegen ist Prädikatenlogik lediglich semi-entscheidbar, d.h. unter Verwendung von unbeschränkten Zeit- und Speicherresourcen kann ein gültiges Theorem bewiesen, ein ungültiges allerdings als solches nicht immer erkannt werden. Trotz dieser theoretischen Grenzen sind praktische Theorembeweiser implementiert worden, die viele schwierige Probleme in diesen Logiken lösen können.

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 muß lediglich jeder einzelne Beweisschritt nachgeprüft werden, was in der Regel durch einfache primitiv rekursive Funktionen möglich ist.

Interaktive Theorembeweiser 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 bis zu Problemen der Programm Verifikation reicht; 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 eher interaktive Theorembeweiser.

Während Theorembeweiser Beweise für Theoreme aus Axiomen über Inferenzschritte ableiten und in irgend einer Form mathematische Beweise nachbilden, benutzen Modellprüfverfahren(Model Checking) zumeist raffiniert implementierte Techniken, 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 Model Checking einsetzen.

Die industrielle Verwendung von Theorembeweisern oder Model Checkern konzentriert sich zur Zeit noch schwerpunktmäßig auf die Verifikation von integrierten Schaltkreisen und Prozessoren. Seitdem Fehler mit schweren kommerziellen 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 Model Checker eingesetzt worden, um viele kritische Operationen in ihnen korrekt zu beweisen.

Wichtige Beweistechniken

Verfügbare Implementierungen

[ACL2]
[Coq]
[Isabelle]
[HOL]
[MetaPRL]
[Mizar], ein Referenzbeweiser für eine Mathematische Zeitschrift
[Otter]
[PVS]
[Simplify]
[SPASS]

Mehr Informationen können von der [Systembeschreibungensliste] oder von der [TPTP library], einer Liste von Beweisproblemen für automatische Beweisprozeduren bezogen werden.