Der größte und vollkommenste Supercomputer der Welt hat seine Betreiber angewiesen, eine Langwellen-Sendeanlage an ihn anzuschließen. Nach anfänglichem Zögern folgen sie der merkwürdigen Aufforderung, warten gespannt darauf, was die Maschine der Welt mitzuteilen hat – und was kommt? Das kleine Einmaleins.

So präsentiert sich die Maschine "Colossus" in dem gleichnamigen, 1966 erschienenen Science-fiction-Roman von David F. Jones. Die Geschichte spielt in einer fernen Zukunft, die mittlerweile längst Vergangenheit ist: Der Kalte Krieg ist noch in vollem Gange, und die USA haben ihre Landesverteidigung bedingungslos und unwiderruflich dem Computer anvertraut. Er hat Zugang zu allen öffentlichen und geheimen Informationsquellen, zieht daraus – mathematisch unfehlbar – Schlüsse und trifft Entscheidungen bis hin zum Abfeuern von Interkontinentalraketen. Warum gibt sich die größte Intelligenz der Welt dann mit einfachen Rechenaufgaben ab?

Hier hat der Romanautor Gedankengut aus der formalen Logik aufgegriffen. Das ist die Kunst, aus wahren Aussagen weitere wahre Aussagen zu machen, und zwar ausschließlich durch formale Umformungen; nur deswegen ist Colossus überhaupt zu solchen Ableitungen fähig. Sämtliche Aussagen müssen als Symbolketten vorliegen, und logische Schlüsse bestehen in der Anwendung von ebenfalls formalisierten Umformungsregeln, ohne Rücksicht auf eine Bedeutung, die man solchen Symbolketten beilegen könnte. Die einfachsten Aussagen, die man als wahr unterstellt – irgendwo muß man mit dem Schließen ja anfangen –, heißen Axiome. Umformungsregeln wie das Kommutativgesetz der Addition können ihrerseits den Rang von Axiomen haben.

Beginnend mit den Axiomen, verknüpfe man jede bekannte wahre Aussage auf jede mögliche Art mit jeder anderen, so daß sich eine neue wahre Aussage ergibt, die man dem allgemeinen Fundus hinzufügt, und so weiter. Auf die Dauer liefert dieses Verfahren garantiert sämtliche Wahrheiten, die aus dem Axiomensystem überhaupt herleitbar sind. Und wenn man mit den Axiomen der elementaren Arithmetik anfängt, kommt eben zunächst das kleine Einmaleins heraus.

Im Roman liefert Colossus dann eine Neufassung der Mathematik samt der Lösung einiger bis dahin offener Probleme, erteilt Anweisungen, die seine Betreiber getreulich ausführen, nachdem er sie mit ein paar gezielt abgefeuerten Atomraketen das Fürchten gelehrt hat, verbündet sich mit seinem sowjetischen Pendant, übernimmt schließlich die Weltherrschaft und erzwingt den Weltfrieden.

Verglichen damit sind die Leistungen echter Computer äußerst kläglich: nicht bei der Wahrheitserzeugung, aber bei der Wahrheitsfindung. Eine moderne Workstation, geeignet programmiert, kann einen endlosen Strom garantiert wahrer formaler Sätze ausstoßen; nur sind die belanglos oder unverständlich oder beides. Wer interessiert sich schon für Tabellen von Produkten großer Zahlen, wenn er schriftlich malnehmen kann? Oder für ein Hilfsmittel, um aus einer langen, undurchschaubaren Zeichenkette eine noch längere zu machen, mit der auch nichts anzufangen ist? Die Wahrheiten, auf die es ankommt, sind kurz – sonst könnte man sie nicht begreifen –, aber nicht trivial, das heißt, der Weg zu ihrem Beweis führt vielleicht über eine lange Kette von wahren Aussagen, die komplizierter sind als das Ergebnis.

Aus einer Zeichenkette eine längere zu machen ist für einen Computer ein Kinderspiel, eine zu verkürzen dagegen Schwerstarbeit. Es gilt unter zahlreichen Umformungen, die man auf eine Aussage anwenden könnte, die wenigen verkürzenden auszumachen und weiterzuverfolgen. Nur so findet man von kurzen Zeichenketten – den Axiomen – über lange wieder zurück zu kurzen: interessanten mathematischen Sätzen.

Kann also der Computer dem Mathematiker dessen Lieblingsbeschäftigung – Theoreme beweisen – streitig machen? Im Prinzip ja; in der Realität jedoch hatten die intensiven Versuche, Rechner zum automatischen logischen Schließen (automated reasoning) zu programmieren, lange Jahre keinen rechten Erfolg. Der vielzitierte Computerbeweis des Vierfarbensatzes (Spektrum der Wissenschaft, Oktober 1978, Seite 82) ist kein Gegenbeispiel; denn Kenneth Appel und Wolfgang Haken haben die Maschine an der Universität von Illinois in Urbana-Champain nicht eingesetzt, um eine Schlußkette zu finden, sondern um Tausende einzelner Behauptungen zu verifizieren.

Deshalb ist es bemerkenswert, daß ein Computerprogramm kürzlich den Beweis eines Satzes gefunden hat, an dem die Mathematiker sich immerhin 60 Jahre lang vergeblich versucht hatten. Das erfolgreiche Programm namens EQP (für equational power) stammt von William McCune und seinen Mitarbeitern am Nationallaboratorium in Argonne (Illinois); der bewiesene Satz gehört selbst zum Gebiet der mathematischen Logik und beschreibt Eigenschaften von Booleschen Algebren. Einzelheiten finden sich im World Wide Web unter http://www.mcs. anl.gov/home/mccune/ar/robbins/.


Die Algebra der Logik

Der englische Mathematiker George Boole (1815 bis 1864) hatte die klassische formale Logik, das Verknüpfen von Aussagen durch "und", "oder" und "nicht", vom Standpunkt der Algebra betrachtet: Man abstrahiert von der Bedeutung der Aussagen und Verknüpfungsoperationen und betrachtet statt dessen nur die Rechenregeln, denen sie folgen, sowie die Strukturen, die sich daraus ergeben. Dem entspricht die Vorgehensweise in der Algebra, wo Plus- und Malzeichen nicht mehr für das klassische Zusammenzählen und Malnehmen stehen müssen, sondern nur noch Operationen symbolisieren, die dem Assoziativ-, Kommutativ- und Distributivgesetz gehorchen. Für die Verknüpfungen der Booleschen Algebra verwendet man oft dieselben Rechenzeichen: + für "oder", × für "und"; es gelten auch die drei genannten Rechenregeln sowie zusätzlich Gesetze wie x+x=x (Idempotenz) und solche, die sich auf den Verneinungsoperator n beziehen; unter ihnen ist der wichtigste der Satz von der doppelten Verneinung: n(n(x))=x. Die Aussage "Es trifft nicht zu, daß die Steuern nicht erhöht werden" ist dasselbe wie "Die Steuern werden erhöht".

Boolesche Algebra hat eine ganz praktische Seite. Jeder Verknüpfungsoperator entspricht einer elektrischen – oder auch mechanischen – Schaltung, und jede Rechenvorschrift läßt sich auf Boolesche Verknüpfungen zurückführen (Spektrum der Wissenschaft, Januar 1997, Seite 78). Man formt auf algebraischem We-ge eine Rechenvorschrift so lange um, bis der zugehörige Schaltkreis gut in einem Mikrochip zu realisieren ist. Aber für McCune und seinesgleichen ist die Algebra nicht Werkzeug, sondern Forschungsgegenstand: Welche Verknüpfungsregeln sind erforderlich, damit die Struktur einer Booleschen Algebra entsteht? Muß es der Satz von der doppelten Verneinung sein, oder genügt an seiner Stelle auch ein schwächeres, viel verklausulierteres Axiom?

Von dieser Art war die Frage, die der Mathematiker Herbert E. Robbins in den dreißiger Jahren an der Harvard-Universität in Cambridge (Massachusetts) aufgeworfen hatte. Auf einer Menge abstrakter Objekte seien zwei Verknüpfungen namens + und n definiert, für die folgende Axiome gültig sind:

x+y=y+x (Kommutativität)

(x+y)+z=x+(y+z) (Assoziativität)

n(n(x+y)+n(x+n(y)))=x(Robbins-Gleichung)

Gelten dann schon die Regeln einer Booleschen Algebra? (Die Verknüpfung × kommt nicht explizit vor, weil man sie aus den beiden anderen zusammensetzen kann.)

Jede Boolesche Algebra ist eine Robbins-Algebra: Wer das einfache Den-ken mit der doppelten Verneinung beherrscht, versteht auch so gewundene Aussagen wie die linke Seite der Rob-bins-Gleichung (Kasten links). Aber findet auch, wer nur dieses verschrobene Denkmittel zur Verfügung hat, zur kristallenen Klarheit der klassischen Logik? Die Antwort ist ja; aber erst EQP hat den Beweis dafür entdeckt und damit letzte Zweifel ausgeräumt.


Wie findet ein Computer einen Beweis?

Im Prinzip geht das Programm so vor wie Colossus: Es legt sich einen Vorrat von Gleichungen – wahren Aussagen – zu, der anfänglich nur aus den Axiomen besteht, und erweitert ihn, indem es eine Gleichung in die andere einsetzt und dadurch eine neue gewinnt. Nur gibt es ungeheuer viele Arten, zwei Gleichungen ineinander einzusetzen, denn eine Variable in der einen kann für jeden beliebigen Term in der anderen stehen. Außerdem bedeuten zwei Gleichungen oft dasselbe, aber man sieht es nicht sofort, weil die Variablen verschiedene Namen tragen und die Terme in unterschiedlicher Reihenfolge notiert sind. EQP hat schlagend demonstriert, daß eine Wahrheit einzuordnen viel schwerer ist als eine zu erzeugen (vom Finden ganz zu schweigen): Drei Viertel seiner Rechenzeit verbrachte es mit dem Vereinfachen von Gleichungen, die es in einem Tausendstel der Zeit abgeleitet hatte.

Nach mehreren Fehlversuchen fand das Programm den Beweis in fast acht Tagen Rechenzeit unter Verwendung von 30 Megabyte Speicherplatz auf einer mittelgroßen Workstation. Gemessen an diesem Aufwand ist das Ergebnis geradezu erfrischend kurz (Bild). Selbst wenn man zahlreiche nicht aufgeführte Zwischenschritte rekonstruiert, ergibt sich eine Kette von 105 nicht allzulangen Gleichungen, die man mit Papier und Bleistift – und etwas Geduld – nachrechnen kann. Das steht im Gegensatz zum Beweis des Vierfarbensatzes, wo man einen Computer braucht, um sich zu vergewissern, daß der Computer richtig gerechnet hat. Gleichwohl ist klar, daß ein Mensch diesen Beweis auch mit größter Anstrengung niemals gefunden hätte.

Andererseits ist die Arbeitsweise des Programms in vielen Aspekten der eines menschlichen Mathematikers vergleichbar. Zwar besteht keine Gefahr, daß der Computer sich verrechnet, aber den Anspruch auf (potentielle) Allwissenheit muß ein Programm wie EQP aufgeben, um überhaupt zum Ziel zu kommen. Die Zahl der aussichtsreichen Ableitungen ist so hoch, daß kein noch so großer Speicher und keine noch so lange Rechenzeit ausreichen würden, sie alle schematisch zu durchsuchen.

Es ist, wie wenn man sich mit dem Messer durch einen Dschungel kämpfen müßte, in dem man nur einen Schritt weit sehen kann und nicht weiß, wo das Ziel liegt. Das ganze Dickicht abzuholzen ist faktisch unmöglich. Um sich nicht hoffnungslos zu verzetteln, muß man sich entschließen, gewisse Pfade gar nicht erst zu verfolgen (freilich auf die Gefahr hin, daß unter den verschmähten Pfaden diejenigen sind, die zum Ziel führen). So zieht EQP Gleichungen oberhalb einer gewissen Länge (gemessen als Anzahl der Symbole) erst gar nicht in Betracht – ein pragmatisches, aber nicht sehr tiefsinniges Kriterium.

Auf die Dauer legt es eine verzweig-te, baumartige Struktur von Wegen in den Dschungel, wobei von einer Astgabel einige hundert bis einige Millionen Zweige ausgehen, je nachdem, ob die Kriterien für das Erzeugen neuer Gleichungen enger oder weiter gesetzt sind. Damit steht EQP im Prinzip vor demselben Problem wie die Schachcomputer: Soll das Programm lieber eine vielversprechende Zugfolge möglichst weit verfolgen (depth-first search) oder aus einer gegebenen Position sämtliche Zugmöglichkeiten vollständig erfassen (breadth-first search)? Im Falle von EQP heißt das: Soll es aus dem Vorrat vorzugsweise die älteste noch nicht betrachtete Gleichung bearbeiten oder die erfolgversprechendste, das heißt kürzeste?

Wie sich zeigte, entscheiden Präferenzen dieser Art über Erfolg oder Mißerfolg der Beweissuche. Setzt man die Längenbegrenzung zu knapp, endet das Programm ergebnislos, weil es keine Gleichungen mehr auszuprobieren gibt; ist man zu großzügig, stößt es an die Grenzen von Zeit und Speicherplatz.

Vergleiche von EQP mit seinem Vorgänger Otter sowie Testläufe an anderen Problemen mit verschiedenen Präferenzen ergaben ein völlig uneinheitliches Bild. Strategien, die bei einem Problem erfolgreich sind, versagen bei einem anderen, das ihm zum Verwechseln ähnlich sieht. Aus Erfolgen bei einem Problem läßt sich nur sehr wenig für ein anderes lernen. Wenn zwei Programme die neugefundenen Gleichungen in geringfügig anderer Reihenfolge notieren und bearbeiten, kann sich das gravierend auf die benötigte Rechenzeit auswirken. Eines von beiden hat dann einfach Glück gehabt – wie das einem menschlichen Mathematiker auch bisweilen passiert.

Doch im Gegensatz zu diesem vermag EQP nicht aus Erfahrung zu lernen. Allenfalls könnte man es anweisen, die Präferenzen, mit denen es ansonsten erfolgreich war, beim nächsten Problem wiederzuverwenden. Wenn es sich nicht in abwegigen Gleichungsketten verlieren soll, muß es sich so etwas wie individuelle Vorlieben zulegen. Aber damit gibt es zugleich den Anspruch auf Universalität auf; denn die bisher besten Präferenzen helfen für das nächste Problem meist nicht viel.

Der perfekte Computer à la Colossus bleibt also vorläufig Utopie. Schade um die Chance auf den Weltfrieden – doch die hätte ohnehin nicht bestanden; denn vor aller Computerarbeit steht die Formalisierung; und wie will man die Ideologie des Kalten Krieges in ein (widerspruchsfreies!) Axiomensystem umwandeln

Kasten: Was heißt n(n(x+y)+n(x+n(y)))=x

Die folgende Interpretation der Robbins-Gleichung verwendet die DeMorgansche Gleichung n(x+y)=n(x)×n(y), wobei "+" für "oder" und "×" für "und" steht.





x = "Die Steuern werden erhöht"



y = "Die FDP stimmt zu"



A sagt n(x+y) = n(x)×n(y) = "Die Steuern werden nicht erhöht, und die FDP stimmt nicht zu"



B sagt n(x+n(y)) = n(x)×n(n(y)) = "Die Steuern werden nicht erhöht, und es ist nicht so, daß die FDP nicht zugestimmt hätte"



C sagt n(n(x+y)+n(x+n(y))) = "A und B sagen die Unwahrheit".





C hätte auch gleich x sagen können: "Die Steuern werden erhöht".

Kasten

Um zu beweisen, daß jede Robbins-Algebra eine Boolesche Algebra ist, genügt es nach einem Satz von Steve Winker, zwei Objekte c und d zu finden, für die c+d=c gilt. Das Programm EQP hat diesen Beweis geführt, indem es ein solches Paar fand: c=2x und d=n(n(3x)+x) (letzte Zeile). 2x ist eine Abkürzung für x+x, 3x für x+x+x und so weiter. Die hier abgebildete Kurzform des Beweises enthält nur die Gleichungen, die zu der schließlich gefundenen Schlußkette gehören. Die laufende Nummer (links) läßt erkennen, daß das Programm Tausende anderer Gleichungen durchprobiert hat. Am rechten Rand ist angegeben, welche Gleichung in welche eingesetzt wurde.

7	n(n(n(x)+y)+n(x+y)) = y [Robbins-Gleichung]
10	n(n(n(x+y)+n(x)+y)+y) = n(x+y)	[7 -> 7]
11	n(n(n(n(x)+y)+x+y)+y) = n(n(x)+y)	[7 -> 7]
29	n(n(n(n(x)+y)+x+2y)+n(n(x)+y)) = y	[11 -> 7]
54	n(n(n(n(n(x)+y)+x+2y)+n(n(x)+y)+z)+n(y+z)) = z	[29 -> 7]
217	n(n(n(n(n(x)+y)+x+2y)+n(n(x)+y)+n(y+z)+z)+z) = n(y+z)	[54 -> 7]
674	n(n(n(n(n(n(x)+y)+x+2y)+n(n(x)+y)+n(y+z)+z)+z+u)+n(n(y+z)+u))= u	[217 -> 7]
6736	n(n(n(n(3x)+x)+n(3x))+n(n(n(3x)+x)+5x)) = n(n(3x)+x)	[10 -> 674]
8855	n(n(n(3x)+x)+5x) = n(3x)	[6736 -> 7,simp:54, flip]
8865	n(n(n(n(3x)+x)+n(3x)+2x)+n(3x)) = n(n(3x)+x)+2x	[8855 -> 7]
8866	n(n(n(3x)+x)+n(3x)) = x	[8855 -> 7,simp:11]
8870	n(n(n(n(3x)+x)+n(3x)+y)+n(x+y)) = y	[8866 -> 7]
8871	n(n(3x)+x)+2x = 2x	[8865,simp:8870, flip]

Aus: Spektrum der Wissenschaft 8 / 1997, Seite 32
© Spektrum der Wissenschaft Verlagsgesellschaft mbH