imported>Aka: https, Links optimiert, Kleinkram

2021-05-16T09:58:56Z

https, Links optimiert, Kleinkram

Neue Seite

Das '''automatische Problemlösen''' stellt ein Teilgebiet der [[Künstliche Intelligenz|Künstlichen Intelligenz]] dar, dessen Inhalt die [[Formalisierung]] von [[Problem]]en und ihre automatisierte [[Problemlösen|Lösung]] ist. Die Formalisierung erfolgt in der Regel mittels [[Graph (Graphentheorie)|Graphen]] bzw. [[Entscheidungsbaum|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ösen]]s 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 [[Axiom]]e und Ableitungsregeln eines [[formales System|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 [[Turingmaschine]]n und der [[Unentscheidbarkeit]] von formalen Aussagen ([[Satz von Rice]], [[Halteproblem]]) sowie der [[Unentscheidbarkeit|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 [[Hilbertprogramm]]s.

''Siehe auch'':
*[[Maschinengestütztes Beweisen]], {{SEP|https://plato.stanford.edu/entries/reasoning-automated/}}

[[Kategorie:Künstliche Intelligenz]]

Automatisches Problemlösen - Versionsgeschichte

imported>Aka: https, Links optimiert, Kleinkram