Logic Theorist ist ein 1956 von Allen Newell, Herbert A. Simon und J. C. Shaw entwickeltes Computerprogramm, das mathematische Lehrsätze durch heuristische Suche bewies, und gilt vielfach als erstes Programm, das gezielt als Künstliche Intelligenz konzipiert wurde.
Zusammenfassung
Logic Theorist sollte Sätze aus Principia Mathematica von Alfred North Whitehead und Bertrand Russell beweisen – einem monumentalen Werk zur Grundlegung der Mathematik aus formaler Logik. Das Programm bewies 38 der ersten 52 Sätze aus dem zweiten Kapitel, in einem Fall sogar mit einem eleganteren Beweis als dem Original.
Begriffsgeschichte
Newell und Simon entwickelten das Programm bei der RAND Corporation und stellten es 1956 auf der Dartmouth-Konferenz vor, wo es zu den ersten konkreten Demonstrationen maschineller Problemlösung zählte. Simon soll gegenüber Studierenden verkündet haben, er und Newell hätten „eine denkende Maschine” erfunden (eigene Übersetzung) – eine Formulierung, die die programmatischen Ambitionen des jungen Feldes prägte.
Methodische Grundlagen
Statt alle möglichen Beweisschritte erschöpfend durchzuprobieren, nutzte Logic Theorist eine Means-Ends-Heuristik: Das Programm bewertete, welcher Zwischenschritt den Abstand zum gewünschten Beweisziel am stärksten verringerte, und verfolgte bevorzugt diesen Pfad. Diese Herangehensweise – Problemlösung als gezielte, heuristisch geleitete Suche im Raum möglicher Zustände – wurde zum methodischen Grundmuster der frühen Symbolischen KI.
Anwendungsfelder
Die für Logic Theorist entwickelte Listenverarbeitungstechnik floss direkt in die Programmiersprache IPL (Information Processing Language) ein, einen wichtigen Vorläufer von Lisp. Das Programm prägte zudem die Forschungsagenda der folgenden Jahrzehnte: Newell und Simon entwickelten mit dem General Problem Solver wenige Jahre später eine verallgemeinerte Version derselben Suchstrategie für beliebige Problemklassen.
Kontroversen und Kritik
Logic Theorists Erfolg beschränkte sich auf ein eng umrissenes, formal sauberes Gebiet – mathematische Beweise mit klaren Regeln und einem eindeutigen Zielzustand. Kritiker:innen wiesen früh darauf hin, dass sich dieselbe Methode kaum auf unscharfe, alltagsweltliche Probleme übertragen ließ, was Jahrzehnte später zu grundsätzlichen Einwänden gegen den symbolischen Ansatz insgesamt führte, etwa in Rodney Brooks’ Intelligence Without Representation.
Verwandte Begriffe
- Künstliche Intelligenz – der Begriff, dessen früheste praktische Demonstration das Programm lieferte
- John McCarthy – Mitorganisator der Dartmouth-Konferenz, auf der Logic Theorist 1956 vorgestellt wurde
Quellenangaben
- Newell, Allen / Simon, Herbert A., 1956. The Logic Theory Machine: A Complex Information Processing System. IRE Transactions on Information Theory 2 (3), S. 61–79.
- McCorduck, Pamela, 1979. Machines Who Think. W. H. Freeman.