TU Darmstadt - Homepage     Fachgebiet Intellektik
zur Hauptseite
    Forschung
zum Seitenende
Wir über uns
Mitarbeiter
Lehre
Forschung
Publikationen
Diplomarbeiten
Links
 
Fachgebiet Intellektik
Fachbereich Informatik
TU Darmstadt
 
 
Forschungsschwerpunkte des Fachgebiets sind Deduktion, Programmsynthese, Wissensrepräsentation, Planen, Lernen und stochastische Suche, wobei der Deduktion vom Fachgebietsleiter seit Jahrzehnten eine besondere Aufmerksamkeit gewidmet wird.


Deduktion

Konkretes Ergebnis der Forschungen in der Deduktion sind weltführende und umfangreiche Beweisersysteme wie SETHEO und KoMeT. Jüngst gesellte sich hierzu das System leanCoP, das im Gegensatz zu den genannten Mammutsystemen aus ganzen drei PROLOG Anweisungen besteht und trotzdem eine erstaunliche Leistungsfähigkeit aufweist. Alle diese universell einsetzbaren Beweiser beruhen auf der von Professor Bibel entwickelten Konnektionsmethode, die die Aufdeckung logischer Zusammenhänge mittels lokaler Formelanalyse und ohne aufwendige Schlußweisen ermöglicht.

Deduktion ist der zentrale und generische Mechanismus, mit dem sich alle Facetten der Wissensverarbeitung in allen denkbaren Anwendungsbereichen durchführen lassen. Unter dieser unbegrenzten Vielfalt möglicher Anwendungsgebiete konzentriert sich das Fachgebiet besonders auf die Programmierung und das Planen.


Programmsynthese

Es ist das Ziel aller Programmentwicklungssysteme, Programmierer von den Details der Koderstellung zu entlasten und die Zuverlässigkeit des resultierenden Kods zu garantieren. Formale Methoden ist in diesem Kontext das Schlagwort der Zeit. Unsere Gruppe verfolgt seit Jahren den Ansatz der formalen und weitgehend automatischen Synthese von effizienter Software aus beschreibenden Spezifikationen, wobei in unseren derzeitigen Bemühungen die Entwicklung von Deduktionsmechanismen für konstruktive Logiken im Vordergrund steht; aus einem automatisch gefundenen Beweis einer solchen Spezifikation samt formalisiertem Wissen über Programmierung läßt sich nämlich sofort ein garantiert korrektes Programm extrahieren. Dieser Ansatz hat zu einer weiteren Automatisierung des NuPRL Systems geführt und wurde erfolgreich in praktischen und sicherheitsrelevanten Aufgabenstellungen eingesetzt.

zum Seitenanfang

Wissensrepräsentation und Planen

Die geeignete Repräsentation von Wissen in einer systemgerechten Weise steht neben den logischen Schlußweisen von Anfang an zentral in unserem Interessenfeld. Bis heute sind hier insbesondere Fragen der Darstellung kausaler Zusammenhänge besonders im Hinblick auf eine effiziente Wissensverarbeitung verbunden mit der unabdingbaren Inferenzfähigkeit von großem Interesse. So wurden in diesem Fachgebiet erstmals befriedigende Lösungen zum bekannten Kulissenproblem (frame problem) erarbeitet, die zudem so gestaltet sind, daß sie gleichzeitig auch das Ramifikations- und Qualifikationsproblem optimal lösen.

Gegenüber allgemeinen Deduktionsaufgaben lassen sich im deduktiven Planen spezielle Problemstrukturen zur erheblichen Steigerung der Performanz der logischen Abarbeitung ausnutzen. Derartige planungsspezifische Reduktionsmechanismen, wie sie im System ProbaPla realisiert sind, haben zu beeindruckenden Beschleunigungen im Planungsprozeß geführt.


Lernen

Im Bereich des Lernens fließen derzeit die umfangreichen Ergebnisse vorheriger theoretischer Arbeiten in konkrete Aufgabenstellungen wie die Entwicklung noch flexibler Suchmaschinen für das Internet ein, die zusammen mit einer deutschen Großbank und weiteren Partnern gelöst werden.


Stochastische Suche

In allen genannten Bereichen ist unsere Forschung mit algorithmisch extrem harten kombinatorischen Problemstellungen wie dem aussagenlogischen Erfüllbarkeitsprobleme (SAT) bzw. mit Optimierungsproblemen konfrontiert. Stochastische Suchverfahren haben sich hier als erfolgreiche Werkzeuge zur Lösung erwiesen. In unserer Gruppe beschäftigen wir uns insbesondere mit ihrer empirischen Evaluierung, der Charakterisierung ihres Lösungsverhaltens und ihrer weiteren Verbesserung. Unabhängig davon arbeiten wir an den Integration solcher Suchtechniken in den deduktiven Logikapparat.


  zum Seitenanfang
  EnglishEnglish Jens Otten · Intellektik·TU Darmstadt · 23.10.2000