Es war eines der großen Logik-Rätsel des vergangenen Jahrhunderts: das Vier-Farben-Problem. Es besagt, dass vier Farben ausreichen, um die Staaten einer beliebigen Landkarte so einzufärben, dass keine zwei aneinander grenzenden Länder die gleiche Farbe bekommen. Die Regel gilt immer, aber niemand konnte sie beweisen. Bis schließlich eine Forschergruppe aus England und Frankreich einen Logik-Computer zu Hilfe nahm. Es war das erste große Mathematik-Problem, das durch einen Rechner gelöst wurde. Für die Informatik war das ein prestigeträchtiger Erfolg, betont Strother Moore von der University of Texas. Er entwickelt seit drei Jahrzehnten Computersysteme, die knifflige Probleme lösen sollen: Maschinen für logisches Denken.
"Sie sind im Wesentlichen mechanische Mathematiker, die Formeln bearbeiten wie a² + b² = c². Und sie ziehen Schlüsse aus den Formeln. Zum Beispiel, dass c dann gleich der Wurzel aus a² + b² ist. Als Leibniz im 17. Jahrhundert die Idee der formalen Logik entwickelte, hatte er genau das im Sinn: ein Zeichen-System, das menschliches Denken erklärt."
Im Grunde arbeiten Logik-Maschinen nach einem recht einfachen Prinzip: Sie bekommen einige Grundregeln – die Axiome – und eine Zielformel, die sie erreichen oder beweisen sollen. Dann versucht der Computer die Axiome so zu kombinieren, dass das gewünschte Ergebnis erreicht wird. Es geht also nicht um kreative Geistesblitze, sondern um logisches Folgern in einem eng abgesteckten Rahmen. Aber auch diese Leistung kann sehr wertvoll sein. Die Firma Intel übersah in ihrem ersten Pentium Prozessor einen winzigen Fehler in der Divisionsrechnung. Die Folge: eine riesige Rückrufaktion und fast eine halbe Milliarde Dollar Verlust.
"Zur gleichen Zeit entwickelte AMD den Prozessor K5. Und sie engagierten unsere Logikmaschinen, um die Division zu überprüfen. Und wir konnten sicherstellen, dass die Ergebnisse so waren, wie sie sein sollten."
Bei der Rechnerentwicklung werden Logik-Maschinen schon seit längerem eingesetzt. Jetzt wollen Strother Moore und seine Kollegen ein neues Anwendungsgebiet erobern.
"Wir hoffen, dass wir in die funktionelle Biologie hinein kommen. Dort wird untersucht, wie Proteine aus einem Zustand in einem anderen übergehen. Diese Übergänge könnten mit Logik-Maschinen nachvollzogen werden."
Dazu haben Informatiker des Stanford Research Institute die so genannte "Pathway Logic" entwickelt, eine spezielle Logik, um Abläufe in biologischen Systemen zu beschreiben. Damit untersuchen sie zum Beispiel die Verarbeitung bestimmter Wachstumsproteine in Zellen. Das Programm bekommt als Grundregeln alle biochemischen Umwandlungen, die bei Proteinen bekannt sind. Dann kann es Vorhersagen darüber aufstellen, ob ein bestimmtes Protein unter den vorgegebenen Bedingungen in einer Zelle produziert werden kann.
"Aber wie immer bei mathematischen Modellen – egal ob bei einer Division oder einem Protein: Nach den Vorhersagen der Mathematik darüber, was passieren soll, muss man ins Labor gehen, um in Experimenten zu überprüfen, ob das mathematische Modell auch zutrifft."
In den vergangenen Jahren sorgten immer wieder Pläne für Aufsehen, die ankündigen, wissenschaftliche Ergebnisse selbstständig von einem Computer erarbeiten zu lassen. So experimentieren Informatiker aus Großbritannien mit einer Maschine, die sie "Wissenschaftsroboter" nennen. Ein Rechner kombiniert mit einer Experimentiermaschine aus dem Biologielabor soll bestimmte Stoffwechselprozesse in Hefepilzen untersuchen. Strother Moore hält solche ambitionierten Ansätze jedoch nicht für viel versprechend.
"Für die nächsten Jahrzehnte werden die Maschinen die Menschen nur unterstützen. Selbstständige Roboter-Forscher kann ich mir noch lange Zeit nicht vorstellen."
"Sie sind im Wesentlichen mechanische Mathematiker, die Formeln bearbeiten wie a² + b² = c². Und sie ziehen Schlüsse aus den Formeln. Zum Beispiel, dass c dann gleich der Wurzel aus a² + b² ist. Als Leibniz im 17. Jahrhundert die Idee der formalen Logik entwickelte, hatte er genau das im Sinn: ein Zeichen-System, das menschliches Denken erklärt."
Im Grunde arbeiten Logik-Maschinen nach einem recht einfachen Prinzip: Sie bekommen einige Grundregeln – die Axiome – und eine Zielformel, die sie erreichen oder beweisen sollen. Dann versucht der Computer die Axiome so zu kombinieren, dass das gewünschte Ergebnis erreicht wird. Es geht also nicht um kreative Geistesblitze, sondern um logisches Folgern in einem eng abgesteckten Rahmen. Aber auch diese Leistung kann sehr wertvoll sein. Die Firma Intel übersah in ihrem ersten Pentium Prozessor einen winzigen Fehler in der Divisionsrechnung. Die Folge: eine riesige Rückrufaktion und fast eine halbe Milliarde Dollar Verlust.
"Zur gleichen Zeit entwickelte AMD den Prozessor K5. Und sie engagierten unsere Logikmaschinen, um die Division zu überprüfen. Und wir konnten sicherstellen, dass die Ergebnisse so waren, wie sie sein sollten."
Bei der Rechnerentwicklung werden Logik-Maschinen schon seit längerem eingesetzt. Jetzt wollen Strother Moore und seine Kollegen ein neues Anwendungsgebiet erobern.
"Wir hoffen, dass wir in die funktionelle Biologie hinein kommen. Dort wird untersucht, wie Proteine aus einem Zustand in einem anderen übergehen. Diese Übergänge könnten mit Logik-Maschinen nachvollzogen werden."
Dazu haben Informatiker des Stanford Research Institute die so genannte "Pathway Logic" entwickelt, eine spezielle Logik, um Abläufe in biologischen Systemen zu beschreiben. Damit untersuchen sie zum Beispiel die Verarbeitung bestimmter Wachstumsproteine in Zellen. Das Programm bekommt als Grundregeln alle biochemischen Umwandlungen, die bei Proteinen bekannt sind. Dann kann es Vorhersagen darüber aufstellen, ob ein bestimmtes Protein unter den vorgegebenen Bedingungen in einer Zelle produziert werden kann.
"Aber wie immer bei mathematischen Modellen – egal ob bei einer Division oder einem Protein: Nach den Vorhersagen der Mathematik darüber, was passieren soll, muss man ins Labor gehen, um in Experimenten zu überprüfen, ob das mathematische Modell auch zutrifft."
In den vergangenen Jahren sorgten immer wieder Pläne für Aufsehen, die ankündigen, wissenschaftliche Ergebnisse selbstständig von einem Computer erarbeiten zu lassen. So experimentieren Informatiker aus Großbritannien mit einer Maschine, die sie "Wissenschaftsroboter" nennen. Ein Rechner kombiniert mit einer Experimentiermaschine aus dem Biologielabor soll bestimmte Stoffwechselprozesse in Hefepilzen untersuchen. Strother Moore hält solche ambitionierten Ansätze jedoch nicht für viel versprechend.
"Für die nächsten Jahrzehnte werden die Maschinen die Menschen nur unterstützen. Selbstständige Roboter-Forscher kann ich mir noch lange Zeit nicht vorstellen."