Automatisches Problemlösen
Das automatische Problemlösen stellt ein Teilgebiet der Künstlichen Intelligenz dar, dessen Inhalt die Formalisierung von Problemen und ihre automatisierte Lösung ist. Die Formalisierung erfolgt in der Regel mittels Graphen bzw. Entscheidungsbäumen. Die Lösung eines Problems wird als ein Pfad in einem solchen Graphen bzw. Baum verstanden, der zu einem Zustand führt, der alle gewünschten Bedingungen erfüllt. Bestand zu Beginn der Forschung im Bereich des automatischen Problemlösens noch die Hoffnung auf allgemeine Problemlöseprogramme für beliebige Probleme (z. B. General Problem Solver), so schränkt man heute die Problemlösung bewusst auf relativ spezielle Problembereiche ein.
Die grundsätzliche Strategie für automatisches Problemlösen ist, einer Maschine auf rein mechanischem Wege alle Axiome und Ableitungsregeln eines formalen Systems vorzulegen und diese Maschine dann rein formal und typographisch neue Sätze beweisen zu lassen, indem durch folgerichtiges Schließen ausgehend von den Axiomen und unter Verwendung aller gültigen Ableitungsregeln neue wohlgeformte Ketten des formalen Systems erzeugt werden. Diese dann bewiesenen Sätze dürfen dann wiederum als Grundlage für weitere, noch komplexere Ableitungen verwendet werden.
Das Konzept des automatischen Problemlösens ist jedoch aufgrund von Ergebnissen der mathematischen und informationstechnischen Grundlagenforschung als ein aussichtsloses Unterfangen erkannt worden. Vor allem Arbeiten in der ersten Hälfte des 20. Jahrhunderts, die sich mit Turingmaschinen und der Unentscheidbarkeit von formalen Aussagen (Satz von Rice, Halteproblem) sowie der Unvollständigkeit formaler Aussagensysteme (Gödelscher Unvollständigkeitssatz) beschäftigen, haben prinzipielle Grenzen für das Lösen von Problemen aufgezeigt.
Jedes hinreichend mächtige formale System (hinreichend mächtig, um etwa mathematische Probleme der Zahlentheorie darstellen zu können) ist demnach notwendigerweise entweder widersprüchlich oder unvollständig. In ersterem Fall ließen sich innerhalb des Systems Aussagen der Form "Dieser Satz lässt sich nicht beweisen" erzeugen, die ganz offensichtlich einen Selbstwiderspruch enthalten. In letzterem Fall ist das System nicht mächtig genug, um alle wahren Sätze durch strikte Anwendung der Folgeregeln tatsächlich ableiten zu können, d. h., es gibt innerhalb eines solchen Systems wahre, aber unbeweisbare Aussagen; das System wird daher als unvollständig bezeichnet.
Der Unvollständigkeitssatz machte auf einen Schlag die Hoffnung der Mathematiker zunichte, alle möglichen Wahrheiten letztlich auch durch Anwendung endlich vieler Ableitungsschritte auch beweisen zu können (etwas, was auch durch einen Automaten möglich sein sollte). Eine wichtige Konsequenz des Gödelschen Satzes ist das Fehlschlagen des sogenannten Hilbertprogramms.
Siehe auch:
- Maschinengestütztes Beweisen, Eintrag in Edward N. Zalta (Hrsg.): Stanford Encyclopedia of Philosophy.