Kurzfassung

Heute zur Verfügung stehende Theorembeweiser sind zwar universell einsetzbar, sie benötigen aber häufig - wegen des großen Suchraums - schon für einfache Probleme unaktzeptable Laufzeiten. Andererseits zeigen Erfahrungen, daß für spezielle Einsatzgebiete hoch effiziente, problemangepaßte Suchheuristiken existieren. Es ist Ziel dieses Projektes, mit Verfahren des maschinellen Lernens aus früheren Beweisverfahren automatisch eine problemangepaßte Suchstrategie für ein aktuelles Problem zu...Heute zur Verfügung stehende Theorembeweiser sind zwar universell einsetzbar, sie benötigen aber häufig - wegen des großen Suchraums - schon für einfache Probleme unaktzeptable Laufzeiten. Andererseits zeigen Erfahrungen, daß für spezielle Einsatzgebiete hoch effiziente, problemangepaßte Suchheuristiken existieren. Es ist Ziel dieses Projektes, mit Verfahren des maschinellen Lernens aus früheren Beweisverfahren automatisch eine problemangepaßte Suchstrategie für ein aktuelles Problem zu erzeugen. Diese methodische Erweiterung soll die Leistungsfähigkeit von generierenden Beweisverfahren nachhaltig verbessern. Das gelernte Wissen ist seiner Natur nach unsicher, die von uns entwickelte Teamwork-Methode erlaubt es aber, mit dieser Unsicherheit umzugehen. Die erarbeiteten Konzepte für das Lernen und Anwenden von Wissen sollen am Beispiel des Gleichheitsbeweises im DISCOUNT-System erprobt werden.» weiterlesen» einklappen