Abgeschlossene Forschungsprojekte

Um Constraint-Löser in einer höheren Sprache schnell und ausreichend effizient zu spezifizieren und implementieren, wurde in der ersten Hälfte der 90er Jahre eine spezielle regelbasierte Sprache, "Constraint Handling Rules" (CHR), entwickelt. CHR kann in eine beliebige herkömmliche Programmiersprache als Bibliothek eingebettet werden. Die derzeit wichtigsten Implementierungen von CHR-Bibliotheken gibt es in Eclipse und Sicstus Prolog, zwei der in der Forschung am meisten benutzten Prolog-Systeme. Im Projekt wird die Constraint-Sprache CHR einerseits weiter untersucht, andererseits zur Implementierung von Anwendungen eingesetzt.

Teilprojekt: Konfluenz von CHR-Programmen

Die Constraint-Sprache CHR erleichtert die Implementierung von Constraint-Lösern erheblich und ermöglicht, dass Programmierer mit wenig Vorkenntnissen Constraint-Programme entwickeln. Wie es bei höheren Programmiersprachen oft der Fall ist, erweist sich die automatische Analyse und Verifikation von in der Constraint-Sprache CHR implementierten Constraint-Lösern als vielversprechend.

Eine essentielle, jedoch bei einer Regelsprache wie CHR nicht offensichtliche Eigenschaft eines Constraint-Lösers ist die Konfluenz. Sie garantiert, dass dasselbe Ergebnis berechnet wird, unabhängig davon, in welcher Reihenfolge die Constraints eintreffen und in welcher Reihenfolge die CHR-Regeln darauf angewandt werden, um sie abzuarbeiten. In diesem Projekt werden Bedingungen zur Konfluenz von CHR-Programmen und deren automatische Überprüfung untersucht. Darüber hinaus werden Verfahren entwickelt, um ein nichtkonfluentes CHR-Programm zu einem konfluenten zu vervollständigen.

Ansprechpartner: Dipl.-Inform. Slim Abdennadher

Teilprojekt: Anwendungen der Constraint-Programmierung

In diesem Teilprojekt werden Anwendungen der Constraint-Programmierung untersucht. Um die Hypothese zu überprüfen, derzufolge die Constraint-Sprache CHR auch von Programmierern ohne besonderen mathemathematische Kentnisse einsetzbar sei, werden Anwendungen bevorzugt, die den Einsatz von fortgeschrittenen numerischen Verfahren nicht erfordern. Das Hauptziel des Teilprojekts ist es, die Eignung der Constraint-Sprache CHR zur einfachen Programmierung beziehungsweise "rapid prototyping" experimentell zu belegen.

Teilprojekt: Methoden zur Generierung von endlichen Modellen und deren Anwendungen

Eine Axiomenmenge heißt erfüllbar im Endlichen, wenn sie ein endliches Modell hat. Wo Modelle von Axiomenmengen nützlich sind - etwa zur Diagnose oder Überprüfung der Korrektheit von Spezifikationen - sind oft endliche Modelle wünschenswert. Ein erstes Ziel des Teilprojektes ist es, ausgehend von der PUHR-Tableau-Methode eine korrekte und vollständige Methode für die Erfüllbarkeit im Endlichen von Axiomenmengen in Sprachen erster Stufe ohne Funktionssymbole zu entwickeln und zu implementieren.

Bislang wurde ein Verfahren spezifiziert, das korrekt und vollständig ist sowohl für die Unerfüllbarkeit - und folglich als Refutationsbeweiser eingesetzt werden kann - als auch für die Erfüllbarkeit im Endlichen. Darüber hinaus wurde das Verfahren in Prolog implementiert.

Die Anwendung der entwickelten und implementierten Methode auf Beispiele ist ein zweites Ziel des Teilprojektes. Dabei sollen vorzugsweise Anwendungen aus den Bereichen Informations- oder Expertensysteme untersucht werden. Im Hinblick auf mögliche Anwendungen etwa im Bereich Diagnose, Datenbanken oder Programm-Verifikation wäre die Erweiterung der Methode und der Implementierung auf Sprachen erster Stufe mit Funktionssysmbolen ein mögliches weiteres Ziel des Teilprojektes.

Ansprechpartnerin: Dr. Sunna Torge

Teilprojekt: Modellgenerierung in der Modallogik

Es gibt zwei grundsätzlich verschiedene Ansätze zur automatischen Deduktion in der Modallogik: erstens Tableau-Verfahren, die direkt auf den Formeln der Modallogik operieren; zweitens Verfahren, die auf einer prädikatenlogischen Darstellung operieren, in die die modallogischen Formeln vorher übersetzt werden. Der Ansatz, direkt auf den Formeln der Modallogik zu operieren statt zu übersetzen, bietet Vorteile wie Verständlichkeit des Modellgenerierungsprozesses für Anwender, die Möglichkeit, Kalküle gemäß der Semantik der "möglichen Welten", sogenannte Frame-orientierte Kalküle, zu konstruieren, sowie die mögliche Verarbeitung von Operatoren, die nicht erststufig ausdrückbar sind. Ziel des Teilprojekts ist deshalb die Entwicklung und Untersuchung von Tableau-Verfahren für die Modellgenerierung in der Modallogik.

In einer ersten Phase des Teilprojektes wurde eine Anpassung der PUHR-Tableau-Methode auf die Modallogik entwickelt und diese Anpassung in Prolog implementiert. Dabei stellte die Übertragung des Begriffes "beschränkte Quantifikation" auf die Modallogik ein interessantes, nicht unmittelbar zu lösendes Problem dar. Die übliche Annahme der wachsenden Domäne wurde nicht gemacht, so dass das entwickelte Verfahren eine große Allgemeinheit besitzt. Ein weiteres Ziel des Teilprojekts ist die Untersuchung von Anwendungen der entwickelten Methode, zum einen zur Korrektheitsprüfung von dynamischen Integritätsbedingungen und der Modellierung von Vorgangsabläufen, zum anderen zu einer Lösung des Problems der definiten Referenz (Theoretische Linguistik) sowie zur Berechnung der so genannten statischen Semantik für Logikprogramme mit Negation.

Ansprechpartner: Prof. Dr. François Bry

Teilprojekt: Generierung minimaler Modelle

Minimale Herbrand-Modelle von Klauselmengen sind in vielen Anwendungsbereichen wie etwa automatisches Theorembeweisen, Programmverifikation, Logikprogrammierung und künstliche Intelligenz nützlich. Die Standardverfahren zur Modellgenerierung liefern in der Regel nichtminimale Modelle. Ziel des Teilprojektes ist die effiziente Generierung von minimalen Modellen für Klauselmengen der Logik erster Stufe unter Anwendung von verschiedenen Suchstrategien. In einer ersten Phase des Teilprojektes wurde die PUHR-Tableau-Methode zur Generierung minimaler Modelle angepasst. Implementierungen unter Einsatz verschiedener Suchstrategien sind in Prolog entwickelt und getestet worden, die sich trotz ihrer ziemlich einfachen Einbettung in Prolog als effizient erweisen. Weitere Ansätze werden derzeit überprüft.

Ansprechpartner: Prof. Dr. François Bry und Prof. Dr. Adnan Yahya (Birzeit University, Palästina)

Teilprojekt: Indefinite Information in Datenbanken

Eine Datenbank beschreibt einen Ausschnitt der Welt. Wenn dieser nicht vollständig bekannt oder (noch) nicht vollständig festgelegt ist, dann sollte das Datenbank-Management-System in der Lage sein, "indefinite Daten" zu behandeln.

Ein typisches Einsatzgebiet für solche Datenbanken sind Anwendungen, in denen Informationen im Lauf der Zeit festgelegt werden, man aber schon vor der vollständigen Festlegung mit der Datenbank arbeiten will. Ein Beispiel ist die Erstellung von Fahrplänen: Für die verschiedenen Linien kann etwa zu einem Zeitpunkt bereits die Streckenführung und die Geschwindigkeit der Fahrzeuge festgelegt sein. Später wird die Häufigkeit der Bedienung der Linien festgelegt, und schließlich die genauen Abfahrtszeiten. Mit der Zeit kann die Anfrage "Wenn ich an der Haltestelle A zum Zeitpunkt T bin, bis wann kann ich Haltestelle B erreichen?" immer genauer beantwortet werden. Indefinite Information tritt aber auch in vielen anderen Fällen auf, etwa wenn aus Kostengründen nicht alle Daten vollständig erhoben wurden, oder bei der Vereinigung mehrerer Datenbanken (unternehmensweite Informationssysteme, Data Warehousing).

Die Datenmodelle, auf denen heutige Datenbank-Managementsysteme basieren (relational, objekt-orientiert, deduktiv, etc.), unterstützen indefinite Information allenfalls ansatzweise. Mit einem solchen System müsste ein Anwendungsprogramm oder ein Anwender eine Anfrage wie die obige verschieden formulieren, je nachdem, welche Parameter des Fahrplans bereits wie genau festgelegt sind. Es ist jedoch (im Sinne deklarativer Programmierung) erstrebenswert, dass die Anfrage in allen Fällen gleich formuliert werden kann und das Datenbanksystem selbständig die geeignete Berechnungsmethode findet. Neben dieser "approximativen" Beantwortung von Anfragen, die auch an definite Datenbanken gestellt werden können, müssen verschiedene weitere Operationen unterstützt werden, wie etwa Anfragen und Updates, die sich auf den Grad der Indefinitheit beziehen.

Ziel des Teilprojekts ist die Entwicklung und Untersuchung von Techniken für die Modellierung indefiniter Information. Dabei werden Techniken aus Logik und Logikprogrammierung, aus Algebra und funktionaler Programmierung, sowie aus der Constraint-Programmierung verwendet.

Ansprechpartner: Dr. Heribert Schütz

Teilprojekt: Anfrageauswertung in Informationssystemen mit Integritätsbedingungen

Die Spezifikationen der meisten Informationssysteme, die heute eingesetzt werden, enthalten sogenannte Integritätsbedingungen, d.h. Bedingungen zum Ausschluss von "inkorrekten" oder "widersprüchlichen" Daten. Die traditionellen Ansätze zur Anfrageauswertung und Integritätsprüfung beruhen auf der Annahme, dass alle Integritätsbedingungen erfüllt sind. Wie sinnvoll diese Annahme auch erscheinen mag, entspricht sie doch selten der Praxis. Vielmehr sind in den meisten praktisch eingesetzten Informationssystemen einige Integritätsbedingungen verletzt.

Die herkömmlichen Formalisierungen der Integrität von und der Anfrageauswertung in Informationssystemen beruhen auf der klassischen Logik, so dass jede beliebige Formel aus einem widerspruchsvollen Informationssystem logisch folgt. In der Praxis aber wird oft eine andere Auslegung der Anfrageauswertung als natürlich betrachtet: Verletzen manche Daten Integritätsbedingungen, so hat dies keinen Einfluss auf Anfragen, die ohne Bezug zu diesen Daten sind. Anstatt des "globalen" Widerspruchsbegriffes der klassischen Logik wäre also für Informationssysteme mit Integritätsbedingungen ein "lokaler" Widerspruchsbegriff angebracht.

Ziel des Teilprojektes ist es, einerseits den Begriff von "lokalen Widersprüchen" zu formalisieren, andererseits eine Anfrageauswertungsmethode entsprechend der vorgeschlagenen Formalisierung zu entwickeln. Im Falle von Informationssystemen, die alle ihre Integritätsbedingungen erfüllen, sollen Formalisierung und Anfrageauswertungsmethode mit den herkömmlichen Ansätzen übereinstimmen.

Ansprechpartner: Prof. Dr. François Bry (1994 -- 1996)

Teilprojekt: Anwendungen von deduktiven Informationssystemen

• Deduktionsbasierte reaktive Dokumente

  In diesem Teilprojekt werden Deduktionsmethoden eingesetzt zur Spezifikation und Auswertung von elektronischen Formularen. Ein elektronisches Formular wird als "reaktives Dokument" angesehen, wenn sich seine Darstellung am Bildschirm den eingetragenen Daten anpasst. So werden z. B. Folgefragen nur dann sichtbar, wenn sie relevant sind. Darüber hinaus sollen symbolische Bedingungen und Ergänzungsregeln deklarativ spezifizierbar sein und automatisch überprüft werden, wie numerische Beziehungen bei Tabellenkalkulations-Software.

  Die reaktiven Dokumente werden in der Sprache Java-Script entwickelt, um den Einsatz des Forschungsprototyps als Intranet-Anwendung zu Testzwecken zu erleichtern.

  Ansprechpartner: Prof. Dr. François Bry

• Vorgangsablaufmodellierung

  Der Einsatz von deklarativen Modellierungsformalismen und von deduktiven Berechnungsmethoden wird am Beispiel der Vorgänge zur Verwaltung von Ordnungswidrigkeiten im Staßenverkehr untersucht. Da sich der Ablauf von Behörde zu Behörde sogar im selben Bundesland unterscheidet und sich dieser Ablauf auch zeitlich oft ändert, wird die Ablauflogik in Form von Regeln spezifiziert, die zur Laufzeit innerhalb eines regelbasierten Systems interpretiert werden. Durch eine regelbasierte Modellierung werden Anpassung und Wartung erleichtert.

  Die Anwendung wird in Zusammenarbeit mit SOFTCON IT-Service GmbH untersucht.

  Ansprechpartner: Prof. Dr. François Bry und Michel Dorochevsky (SOFTCON IT-Service GmbH)

Projekt: Integration funktionaler und logischer Programmierung (1996--1999)

Im Bereich deklarativer Programmierung haben sich zwei komplementäre Paradigmen etabliert: Die Logikprogrammierung mit ihrem Hauptvertreter Prolog, und die funktionale Programmierung mit Sprachen wie etwa ML und Haskell. Trotz ähnlicher Zielsetzung und teilweise gleichen Methoden bleibt der Austausch zwischen beiden Programmierparadigmen spärlich. Einige Programmiersprachen jedoch verbinden die beiden Programmierparadigmen, unter anderem die Sprache Curry. Curry wird international aktiv weiterentwickelt und bietet eine standardisierte Plattform für Forschung, Lehre und Anwendung funktional-logischer Sprachen.

Im Projekt werden die folgenden Aspekte untersucht:

Projekt: Visualisierung von Kalkülen und Zustandsübergangssystemen (1994 -- 1996)

Inferenzmotoren für wissensbasierte Systeme sind im wesentlichen Implementierungen von logischen Kalkülen. Diese dienen dazu, aus einer als Spezifikation dienenden Formelmenge der zugrundeliegenden Logik weitere Formeln abzuleiten, die in bestimmten semantischen Beziehungen zur Spezifikation stehen. Für viele Zwecke ist es wünschenswert, die Ableitungen mit geeigneten graphischen Werkzeugen übersichtlich darstellen und analysieren zu können: Als Hilfe bei der Suche nach Fehlern in der Spezifikation oder im Ableitungsverfahren, zum Vergleich verschiedener Inferenzmotoren, zur Erklärung der Ableitungen oder zum Einsatz in der Lehre.

Ziel des Projekts ist die Entwicklung und Untersuchung von Hilfsmitteln für derartige Zwecke. Einfache Trace-Komponenten reichen dafür nicht aus. Damit kann zwar eine Flut von Informationen über die einzelnen Ableitungsschritte erzeugt werden, die aber zu zahlreich und zu "feinkörnig" und ohne geeignete Abstraktionsmöglichkeiten praktisch nutzlos sind.

Beteiligung an Forschungsprojekten von anderen Fakultäten der Universität München

Die Lehr- und Forschungseinheit "Programmier- und Modellierungssprachen" unterstützt andere Fakultäten der Ludwig-Maximilians-Universität (LMU) durch Informatik-Dienstleistungen. Derzeit geschieht dies in folgenden Forschungsprojekten:

Forschungsprojekt "Computergestützte Regelinduktionsexperimente" an der Fakultät für Psychologie und Pädagogik (1997--1998)