Starten Sie Ihre Suche...


Durch die Nutzung unserer Webseite erklären Sie sich damit einverstanden, dass wir Cookies verwenden. Weitere Informationen

Lernen von Suchheuristiken beim Theorembeweisen

Laufzeit: 01.06.1996 - 31.05.1998

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

  • Suchstrategie generierenden Beweisverfahren Teamwork-Methode DISCOUNT-System Laufzeiten

Projektteam


Jürgen Avenhaus

Beteiligte Einrichtungen