Beweis-Assistent
Redundanz Die Artikel Computerbeweis und Maschinengestütztes Beweisen überschneiden sich thematisch. Hilf mit, die Artikel besser voneinander abzugrenzen oder zu vereinigen. Beteilige dich dazu an der Diskussion über diese Überschneidungen. Bitte entferne diesen Baustein erst nach vollständiger Abarbeitung der Redundanz. Cjesch 12:47, 20. Mär. 2007 (CET)

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. 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. 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. 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 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 bis zu Problemen der Programmverifikation reicht.

Bedeutende mathematische Beweise, die durch einen Theorembeweiser überprüft wurden, sind der Beweis des Vier-Farben-Satzes durch Georges Gonthier (der den älteren Computerbeweis durch Appel und Haken ablöst), sowie der (zurzeit unvollendete) formalisierte Beweis der Keplerschen Vermutung durch das Flyspeck-project. 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.

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.

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.

Eine verfügbare Implementierung ist Isabelle.

Wichtige Beweistechniken

Weblinks

Literatur

Manfred Kerber, Michael Kohlhase: Symbolic Computation and Automated Reasoning, A K Peters, Ltd., 2001, ISBN 1568811454


Wikimedia Foundation.

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Computerbeweis — Als Computerbeweis bezeichnet man den Beweis einer Behauptung, das heißt einer mathematischen oder logischen Aussage, mit Hilfe eines Computerprogramms. Man verwendet den Begriff insbesondere für solche Beweise, die folgendes Schema aufweisen:… …   Deutsch Wikipedia

  • Alger Hiss — (* 11. November 1904 in Baltimore, Maryland; † 15. November 1996 in New York City) war ein amerikanischer Rechtsanwalt und US Regierungsbeamter, den man nach dem Zweiten Weltkrieg der Spionage bezichtigte. Wegen der Verjährung konnte man …   Deutsch Wikipedia

  • Paul Koebe — Paul Koebe, 1930 in Jena Paul Koebe (* 15. Februar 1882 in Luckenwalde; † 6. August 1945 in Leipzig) war ein deutscher Mathematiker, der sich fast ausschließlich mit Funktionentheorie beschäftigte. Inhaltsverzeichnis …   Deutsch Wikipedia

  • Heinrich Heesch — (1930) Heinrich Heesch (* 25. Juni 1906 in Kiel; † 26. Juli 1995 in Hannover) war ein deutscher Mathematiker, der sich mit Geometrie beschäftigte. Inhaltsverzeichnis …   Deutsch Wikipedia

  • Keplersche Vermutung — Die Keplersche Vermutung ist eine Vermutung über die Packung von Kugeln im dreidimensionalen euklidischen Raum. Sie besagt, dass keine Anordnung von gleich großen Kugeln eine größere mittlere Dichte aufweist als die kubisch flächenzentrierte… …   Deutsch Wikipedia

  • Ernst Zermelo — in Freiburg, 1953 Ernst Friedrich Ferdinand Zermelo [t͡sɛrˈmeːlo] (* 27. Juli 1871 in Berlin; † 21. Mai 1953 in Freiburg im Breisgau) war ein deutscher Mathematiker …   Deutsch Wikipedia

  • Zermelo — Ernst Zermelo in Freiburg, 1953 Ernst Friedrich Ferdinand Zermelo (* 27. Juli 1871 in Berlin; † 21. Mai 1953 in Freiburg im Breisgau) war ein deutscher Mathematiker. Zermelo war der Sohn eines Gymnasialprofessors und besuchte das …   Deutsch Wikipedia

  • Christos Papakyriakopoulos — (griechisch Χρίστος Παπακυριακόπουλος, * 1914 in Chalandri, Athen; † 29. Juni 1976) war ein griechischer Mathematiker, der sich mit geometrischer Topologie beschäftigte. Inhaltsverzeichnis 1 Leben 2 Wirken …   Deutsch Wikipedia

  • Carl Ludwig Siegel — in Göttingen, 1975 Carl Ludwig Siegel (* 31. Dezember 1896 in Berlin; † 4. April 1981 in Göttingen) war ein deutscher Mathematiker; sein Spezialgebiet war die Zahlentheorie. Er gilt als einer der bedeutendsten Mathematiker des 20. Jahrhu …   Deutsch Wikipedia

  • Galileo Galilei — – Porträt von Justus Sustermans, 1636 …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”