Einen Beweisweg gezielt suchen

Eine Vermutung ist noch kein Ergebnis

Der Dartmouth-Antrag von 1955 stellt die maschinelle Beschreibung von Lernen und Intelligenz als Forschungsprogramm vor. Seine weitreichende Grundannahme ist ausdrücklich eine Vermutung. Der Antrag berichtet nicht über eine bereits erfolgreich durchgeführte Untersuchung allgemeiner Intelligenz. Der Vorschlag für das Forschungsprojekt

Logic Theorist richtet eine engere, tatsächlich prüfbare Frage an symbolische Verfahren: Wie kann ein Programm logische Beweise finden? Diese konkrete Aufgabe erlaubt es, erzeugte Schritte zu kontrollieren und Suchwege miteinander zu vergleichen, ohne zuerst eine umfassende Behauptung über sämtliche Formen menschlichen Denkens entscheiden zu müssen.

Zulässige Schritte genügen nicht zur Auswahl

Die formale Beschreibung von 1956 legt fest, wie logische Ausdrücke behandelt und bestimmte Schlussweisen angewendet werden. Solche Regeln bestimmen, welche Schritte zulässig sind. Sie legen damit noch nicht automatisch fest, welcher der vielen möglichen Schritte als Nächstes besonders nützlich wäre. Die Beschreibung der formalen Maschine

Eine frühere Museumsstation begründet eine konkrete geometrische Konstruktion. Hier tritt eine andere Schwierigkeit hinzu: Selbst bei klaren Regeln kann das Angebot möglicher Fortsetzungen sehr groß werden. Eine vollständige Aufzählung ist dann möglicherweise weit aufwendiger als der schließlich gefundene kurze Beweis.

Die Suche nutzt aussichtsreiche Wege

Newell, Shaw und Simon untersuchen Strategien, die bestimmte Möglichkeiten bevorzugen. Bereits verfügbare Sätze, Reihenfolgen und gewählte Teilaufgaben beeinflussen, welche Wege zuerst verfolgt werden. Die Kurzfassung von 1956 beschreibt solche Varianten als Gegenstand vergleichender Untersuchung. Strategien und verfügbare Ergebnisse

Eine Heuristik ist dabei eine Entscheidungshilfe für die Suche. Sie ersetzt keine logische Regel durch bloße Plausibilität. Ein bevorzugter Weg muss am Ende immer noch eine Folge zulässiger Schritte liefern. Die Unterscheidung zwischen erfolgversprechender Auswahl und gültigem Schluss hält beide Aufgaben auseinander.

Der gefundene Beweis bleibt kontrollierbar

Der empirische Bericht von 1957 zeigt konkrete Beweisfolgen und untersucht die ausgeführte Suche. Ein gefundener Beweis lässt sich Schritt für Schritt prüfen: Welche Aussage wurde verwendet, welche Regel angewendet und welches Ergebnis folgt daraus? Beweisfolge und empirische Untersuchung

Die Prüfung muss nicht dieselben Umwege wiederholen, die während der Suche durchlaufen wurden. Als eigene Denkstütze hilft der Unterschied zwischen dem Finden einer Route und dem Nachgehen einer bereits beschriebenen Route. Das Beispiel erklärt unterschiedliche Aufwände; es ist kein Beweis einer allgemeinen Aussage über jede logische Aufgabe.

Ein Abbruch entscheidet den Satz nicht

Für einen untersuchten Satz berichtet die Arbeit von einem erfolglosen Lauf auf dem JOHNNIAC unter den angegebenen Ressourcenbedingungen. Solche Versuche zeigen Grenzen der verwendeten Strategie und Ausstattung. Sie beweisen nicht, dass der Satz mit den verfügbaren logischen Regeln grundsätzlich unbeweisbar wäre. Ressourcen und erfolglose Suche

Andere Reihenfolgen oder bereits bekannte Hilfssätze können den Suchaufwand verändern. Auch eine abgeschätzte Dauer vollständiger Aufzählung ist von einer tatsächlich gemessenen Laufzeit zu unterscheiden. Ein präziser Ergebnisbericht nennt deshalb Aufgabe, Voraussetzungen, Strategie und Abbruchgrund gemeinsam.

Entwurf, Ausführung und Deutung trennen

Der erste ausführliche Text von 1956 beschreibt zunächst eine formale Maschine. Der spätere empirische Bericht behandelt ausgeführte Computeruntersuchungen. Diese Stufen dürfen nicht so zusammengeschoben werden, als dokumentierte jede frühe Beschreibung bereits denselben fertigen Rechnerlauf. Der Status der frühen Beschreibung Der spätere Versuchsbericht

Nimm eine klare Unterscheidung mit: Die Heuristik wählt einen Suchweg, die Regeln tragen den Beweis, und die Messung beschreibt den Aufwand eines konkreten Laufs. Daraus entsteht ein überprüfbares Forschungsergebnis. Eine pauschale Gleichsetzung mit menschlichem Verständnis oder eine allgemeine Erfolgsquote folgt daraus noch nicht.

Begriffe verstehen

Quellen und Nachweise

Die Quellen sind den Aussagen im Text zugeordnet. Originalstudien, Sammlungstexte und eigene Einordnung erfüllen unterschiedliche Aufgaben. Einige Fachtexte sind beim Verlag nur teilweise frei zugänglich.

1. Ausgeführte Suche, Beweisfolgen und Ressourcen

   Allen Newell, J. Clifford Shaw und Herbert A. Simon: Empirical Explorations with the Logic Theory Machine. 1957.

   Keine Volllektüre des vollständigen Aufsatzes behauptet. Ein begrenzter erfolgloser JOHNNIAC-Lauf ist kein Unbeweisbarkeitsnachweis; Abschätzung und gemessene Laufzeit getrennt.

   ← Zur Textstelle 1: Der gefundene Beweis bleibt kontrollierbar← Zur Textstelle 2: Ein Abbruch entscheidet den Satz nicht← Zur Textstelle 3: Entwurf, Ausführung und Deutung trennen
2. Strategien und Reihenfolgen als Untersuchungsgegenstand

   Allen Newell, J. Clifford Shaw und Herbert A. Simon: Empirical Exploration of the Logic Theory Machine. Kurzfassung P-951-A, 10. Oktober 1956.

   Vollständige Kurzfassung, kein vollständiger empirischer Aufsatz. Gedächtnis, Reihenfolge und Programmvarianten sind getrennte Bedingungen.

   ← Zur Textstelle: Die Suche nutzt aussichtsreiche Wege
3. Der zunächst formale Entwurf der Logic Theory Machine

   Allen Newell und Herbert A. Simon: The Logic Theory Machine: A Complex Information Processing System. IRE Transactions on Information Theory, 1956, S. 61–79.

   Die frühe Beschreibung ist zunächst eine formale Maschine. Shaw und der spätere ausgeführte Versuch werden getrennt berücksichtigt.

   ← Zur Textstelle 1: Zulässige Schritte genügen nicht zur Auswahl← Zur Textstelle 2: Entwurf, Ausführung und Deutung trennen
4. Ein Forschungsantrag mit ausdrücklich formulierter Vermutung

   John McCarthy, Marvin Minsky, Nathaniel Rochester und Claude Shannon: A Proposal for the Dartmouth Summer Research Project on Artificial Intelligence. 31. August 1955.

   Vorschlag für 1956, kein Bericht über einen bereits nachgewiesenen Erfolg oder eine einheitliche tatsächlich anwesende Gruppe.

   ← Zur Textstelle: Eine Vermutung ist noch kein Ergebnis

Redaktion: Benjamin Metzig. Text und Quellen am 8. September 2026 geprüft. Generative KI diente als Werkzeug für Text und Bild.