Theorembeweiser

Theorembeweiser
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:

  • Isabelle (Theorembeweiser) — Isabelle Aktuelle Version Isabelle2011 Betriebssystem unixoide Programmier­sprache Standard ML Kategorie Theorembeweiser Lizenz …   Deutsch Wikipedia

  • 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… …   Deutsch Wikipedia

  • Beweis-Assistent — 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… …   Deutsch Wikipedia

  • Beweisassistent — 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… …   Deutsch Wikipedia

  • Theorembeweis — 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… …   Deutsch Wikipedia

  • Theorembeweisen — 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… …   Deutsch Wikipedia

  • ISABELLE — Aktuelle Version: Isabelle2008 Betriebssystem: unixoide Kategorie: Theorembeweiser Lizenz: BSD Lizenz …   Deutsch Wikipedia

  • Isabelle (Begriffsklärung) — Isabelle ist ein weiblicher Vorname, siehe Isabelle. ein isabellfarbenes Pferd, siehe Cream Gen des Pferdes. ein Theorembeweiser, siehe Isabelle (Theorembeweiser). Siehe auch Isabella (Begriffsklärung) …   Deutsch Wikipedia

  • Prolog (Programmiersprache) — Prolog Paradigmen: logisch, deklarativ, oft auch constraintbasiert Erscheinungsjahr: 1972 Designer: Alain Colmerauer Entwickler: Philippe Roussell …   Deutsch Wikipedia

  • Generation language — Quelltext eines Programms in der objektorientierten Programmiersprache Ruby. Eine Programmiersprache ist eine Notation für Computerprogramme; sie dient sowohl dazu, diese während und nach ihrer Entwicklung (Programmierung) darzustellen als auch… …   Deutsch Wikipedia

Share the article and excerpts

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