Für viele Anwendungen im Bereich der deklarativen Wissensmodellierung sind Tableau-Verfahren besonders geeignet, da nicht nur die Inkonsistenz einer Menge festgestellt wird, sondern bei Konsistenz auch Modelle generiert werden. Diese Modelle können gegebenenfalls dann als Erklärungen oder Gegenbeispiele dienen. Zudem ist es oft recht einfach, Tableau-Verfahren an eine spezielle, durch die Anwendung geforderte Syntax anzupassen. In diesem Projekt werden Tableau-Verfahren untersucht mit dem Ziel, Sonderverfahren zu entwickeln. Dabei wird vorzugsweise die Methode der "Positive Unit Hyper Resolution (PUHR) Tableaux" untersucht.
Effiziente Modellgenerierungsverfahren, die auch bei steigender Größe der zu verarbeitenden Formelmengen keinen wesentlichen Abfall der Inferenzrate haben, sind eine Voraussetzung für den Einsatz der Modellgenerierung in realistischen Anwendungen. Ziel dieses Teilprojekts ist deshalb die Entwicklung und Untersuchung von effizienten Verfahren und Datenstrukturen für den PUHR-Tableau-Kalkül.
Bislang wurden eine Reihe von effizienzsteigernden Techniken entwickelt, implementiert und getestet: Erstens wurde die aus den Bereichen der deduktiven Datenbanken oder regelbasierten Systeme bekannte Technik des inkrementellen Vorwärtsschließens auf den PUHR-Tableau-Kalkül angepasst. Zweitens wurde eine Kompilationstechnik für den PUHR-Tableau-Kalkül mit Zielsprache Prolog entwickelt.
Momentan wird eine abstrakte Maschine entwickelt, die den Umweg über Prolog überflüssig machen soll. Darüber hinaus werden Datenstrukturen für den PUHR-Tableau-Kalkül untersucht, insbesondere die Substitutionsbäume zur Repräsentation von Term- bzw. Klauselmengen. Letztlich wird die Parallelisierung des PUHR-Tableau-Kalküls untersucht mit dem Ziel, die verschiedenen Zweige eines Tableau weitgehend unabhängig voneinander zu expandieren.
Ansprechpartner: Dipl.-Inform. Tim Geisler
Lehr- und Forschungseinheit
Institut
Universität