Learning search heuristics for automated deduction

Viac o knihe

Viele Probleme in der Informatik, insbesondere im Bereich der Künstlichen Intelligenz (KI), werden durch suchbasierte Verfahren bearbeitet, zu denen auch die omatische Deduktion zählt. Diese Probleme gehören zu den schwierigsten Suchherausforderungen, und es ist unbestritten, dass die oft unintelligenten Suchmethoden Schwächen aufweisen, die selbst durch schnelle Rechner nicht vollständig kompensiert werden können. Früh wurde erkannt, dass Lernen eine zentrale Rolle im intelligenzbasierten Problemlösen spielt. In der omatischen Deduktion gibt es jedoch ein Defizit, während in anderen KI-Bereichen maschinelles Lernen beeindruckende Ergebnisse erzielt hat. Die Arbeit präsentiert Lernverfahren, die in der Deduktion vorteilhaft eingesetzt werden können. Das Grundprinzip dieser Verfahren besteht in der heuristischen Nutzung von Wissen aus gelösten Problemen zur Verbesserung oder Generierung von Suchheuristiken. Diese Methode bietet entscheidende Vorteile gegenüber deterministischen Ansätzen. Empirische Überprüfungen zeigen, dass nicht nur erhebliche Geschwindigkeitssteigerungen möglich sind, sondern auch Probleme gelöst werden können, die ohne Lernen unlösbar waren. Zudem werden Ansätze behandelt, um anwendbares Wissen omatisch zu entdecken und auch ungeeignetes Wissen effektiv zu nutzen, was die Benutzer entlastet. Die Prinzipien der Verfahren sind nicht nur auf die omatische Deduktion anwendbar, sondern auch für viele andere Such