Altuğ Anis

Goethe-Universität Frankfurt am Main
Fachbereich Informatik und Mathematik
Institut für Informatik
Professur für Künstliche Intelligenz und Softwaretechnologie
Robert-Mayer-Str. 11-15
60325 Frankfurt am Main

Telefon: +49 69 798-22893
Fax: +49 69 798-28919
E-Mail: altug AT ki.informatik.uni-frankfurt.de
Homepage: http://www.ki.informatik.uni-frankfurt.de/

Algorithmen auf komprimierten Bäumen in sich selbst verflechtenden Systemen

Analyse und Implementierung von unterschiedlichen Algorithmen auf STG-komprimierten Termen.

Ausführliche Beschreibung

Ich beschäftige mich mit komprimierten Darstellungen von baumartigen Datenstrukturen, wie sie z.B. in XML, in Programmdatenstrukturen und in Reasoningsystemen verwendet werden, insbesondere mit grammatikbasierter Kompression. Für Strings verwendet man straight line programs, und für Baumstrukturen sogenannte Singleton-Tree-Grammars (STGs).
Die STGs verallgemeinern die komprimierte Darstellung von Bäumen als gerichteter Graph durch Verwendung von Baum-Kontexten.
Terme sind markierte Bäume, die man z.B. als f(a,x,g(a,b,c)) schreiben kann, wobei
f,g jeweils dreistellige Symbole sind, a,b,c Konstanten und x ein Funktionssymbol.
Da während der Verarbeitung auch sehr große Bäume auftreten können, lohnt es sich, komprimierte Bäume zu verarbeiten.
Ich untersuche und implementiere unterschiedliche Algorithmen auf diesen STG-komprimierten Termen, beispielsweise den Unifikationsalgorithmus von Robinson, und den Algorithmus von Plandowski für einen schnellen Gleichheitstest von komprimierten Strings, der auch für Bäume verwendbar ist.
Insbesondere untersuche ich Algorithmen, die das congruence closure-Verfahren auf komprimierte Terme und Gleichungen anpasst.

Beitrag zum Doktorandenkolleg

Mein Thema trägt zur effizienten Speicherung und Verarbeitung von Baumstrukturen bei, die z.B. in Expertensystemen mit automatischen Schlussverfahren vorkommen, insbesondere in SAT-Testern, die auf dem erweiterten Verfahren SMT (Satisfiability modulo theories) beruhen. 


Tags

Komprimierte Terme, Unifikation, Baumgrammatiken, Congruence Closure,Termersetzungssysteme, Baumautomaten