Computerbeweis

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: Zunächst wird gezeigt, dass das allgemeine Problem P gilt, wenn eine andere Eigenschaft E gilt, also P auf E reduziert werden kann. Entscheidend ist dabei, dass E durch Aufzählen endlich vieler (meist sehr vieler) Fälle entschieden werden kann. Die Reduktion von P auf E ist üblicherweise ein ganz normaler, informeller mathematischer Beweis. Erst im nächsten Schritt kommt der Computer ins Spiel: Man schreibt ein Programm, das alle Fälle aufzählt (generate) und dann jeweils überprüft, ob für sie E tatsächlich gilt (test). Im Grunde wird E also durch eine Brute-Force-Methode entschieden. Aus beiden Teilen folgt dann die Behauptung P.

Einwände gegen Computerbeweise

Computerbeweise sind z. T. unter Mathematikern umstritten. Neben eher psychologischen oder hypothetischen Einwänden gibt es dabei auch ganz handfeste methodische. Ein psychologischer Einwand ist das Ideal einer kurzen, logischen Begründung, die von jedermann leicht nachvollzogen werden kann. Solche Beweise werden allerdings in der mathematischen Praxis immer seltener. Die Monsterbeweise der aktuellen mathematischen Forschung können in allen Teilen (einschließlich der benutzten Hilfssätze) von keinem einzelnen Menschen mehr nachvollzogen werden.
Eher hypothetisch ist der Einwand, dass der Compiler oder die Hardware einen Fehler haben könnte. Durch Wiederholungen auf verschiedenen Rechnern und in verschiedenen Implementierungen kann dieses Risiko beliebig minimiert werden. Methodisch problematisch ist die Frage, ob das Programm den unterliegenden Algorithmus korrekt implementiert, ob der Algorithmus in der generate-Phase alle Fälle aufzählt, und die test-Phase tatsächlich die Eigenschaft E für diesen Fall zusichert. Hier hat man also ein handfestes Programmverifikationsproblem.

Der erste bedeutende Computerbeweis war der des Vier-Farben-Satzes. Neben der Tatsache, dass die Problemreduktion als sehr unklar galt (und später erheblich verbessert werden musste), war auch das Programm sehr intransparent und nicht formal verifiziert. Ein jüngerer bedeutender Computerbeweis ist die erste Fassung der Keplerschen Vermutung.

Ein Computerbeweis ist zu unterscheiden von einem Beweis durch einen Theorembeweiser (auch Beweis-Assistent genannt). Hierbei wird ein mathematischer Beweis formalisiert, d.h. soweit in eine Folge von logischen Einzelschritten zerlegt, dass diese von einem Computerprogramm nachvollzogen werden können. Beweisprüfung ist ein universelles, nur logik-abhängiges Problem, während generate-and-test-Algorithmen problemspezifisch sind. Es gibt daher gute Gründe, warum maschinengeprüften formalen Beweisen mehr zu trauen ist als Computerbeweisen.

Für den Vier-Farben-Satz ist mittlerweile ein formaler Beweis durch Georges Gonthier vorgelegt worden, für den formalen Beweis der Keplerschen Vermutung im Rahmen des Flyspeck-Projektes [1] existieren zurzeit nur wesentliche Teile.

Einzelverweise

  1. http://code.google.com/p/flyspeck Flyspeck-project

Wikimedia Foundation.

Игры ⚽ Нужно сделать НИР?

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

  • 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

  • Theorembeweiser — 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

  • Logisches Schließen — Allgemein ist ein Beweis die gültige Herleitung der Richtigkeit (Verifikation) oder Unrichtigkeit (Falsifikation) einer Aussage aus wahren Prämissen, das heißt ein förmlicher, sich nur auf als wahr anerkannte Prämissen stützender und zumindest… …   Deutsch Wikipedia

  • 4-Farben-Problem — Der Vier Farben Satz (früher auch als Vier Farben Vermutung oder Vier Farben Problem bekannt) ist ein mathematischer Satz und besagt, dass vier Farben immer ausreichen, um eine beliebige Landkarte in der euklidischen Ebene so einzufärben, dass… …   Deutsch Wikipedia

  • 4-Farben-Satz — Der Vier Farben Satz (früher auch als Vier Farben Vermutung oder Vier Farben Problem bekannt) ist ein mathematischer Satz und besagt, dass vier Farben immer ausreichen, um eine beliebige Landkarte in der euklidischen Ebene so einzufärben, dass… …   Deutsch Wikipedia

  • Dichteste Kugelpackung — Eine dichteste Kugelpackung ist die geometrische Anordnung unendlich vieler Kugeln gleicher Größe, so dass die größtmögliche Dichte erzielt wird, also der Anteil an Leerraum minimal ist. Eine solche Anordnung ergibt sich, wenn viele Kugeln… …   Deutsch Wikipedia

  • Gonthier — ist ein männlicher Vorname und Familienname. Inhaltsverzeichnis 1 Herkunft und Bedeutung 2 Bekannte Namensträger 2.1 Vorname 2.2 Familienname …   Deutsch Wikipedia

Share the article and excerpts

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