Architektur, Modellierung und Implementierung von Computeralgebra-Systemen (Klaus)
Schwerpunkte sind dabei der Interpreter- und Compilerbau (einschließlich Kodegenerierung) und die Datenverwaltung von dynamisch erzeugten algebraischen Objekten. Desweiteren werden Untersuchungen durchgeführt, wie moderne Paradigmen (z.B. Objektorientierung, parallele Abarbeitung) in das bestehende Modell eingepaßt werden können.
Mit dem System FELIX wurde in Leipzig ein eigenes System zum symbolischen Rechnen entwickelt, mit dem man verschiedene softwaretechnische Ansätze gut untersuchen kann. Hierbei stehen experimentelle Untersuchungen zur Beschleunigung des Algorithmus zur Berechnung von Gröbnerbasen durch Parallelisierungsansätze im Mittelpunkt.
Deduktionssysteme (Herre, Neitz)
1 Selektives Backtracking in zielorientierten Kalkülen (Neitz)
Die Einschränkung des Suchraums von Beweisverfahren ist eine wichtige Fragestellung im automatischen Theorembeweisen. In dem Projekt wurden verschiedene Methoden untersucht, den Suchraum eines zielorientierten durch eine selektive Backtrackstrategie einzuschränken.
2. Konstruktive Kalküle (Herre)
Im Mittelpunkt der Untersuchungen stehen konstruktive Kalküle mit ihren vielfältigen Anwendungen im Bereich der Programmsynthese und der automatischen Planung. Konstruktive Kalküle gewinnen in der Informatik zunehmend an Bedeutung, da sie einen geeigneten Rahmen für die Beschreibung algorithmisch bedeutsamer Konzepte darstellen und einen Zusammenhang zwischen dem Beweisbegriff und dem Algorithmenbegriff herstellen. Von Bedeutung ist die Entwicklung einer Beweistheorie, die sich stärker an den strukturell-kombinatorischen Eigenschaften von Beweisdiagrammen orientiert.
Entscheidbarkeitstheorie (Herre)
Entscheidungsverfahren für formale Theorien erfassen wichtige Aspekte der algorithmischen Behandlung von Wissenbasen. Im Mittelpunkt steht die Untersuchung verschiedener Klassen von Graphen, von Theorien der linearen Ordnung sowie von geordneten Mono-Unaren.
Formale Wissensspezifikation mit Anwendungen (Herre, Dötsch)
Die formale Repräsentation und Verarbeitung von Wissen ist ein wichtiges Problem in der Informatik. Hierzu sind in den letzten Jahre verschiedene Sprachen entwickelt worden. In diesem Forschungsvorhaben wird in Zusammenarbeit mit der Forschungsgruppe von J. Treur (Freie Universtät Amsterdam) an der Weiterentwicklung derartiger Spezifikationsprachen gearbeitet. Die Sprache DESIRE soll als Rahmensystem für die Entwicklung eines Diagnosesystems in der Medizin verwendet werden. Die Arbeiten an einem modell-basierten System für die Diagnose von Stoffwechselerkrankungen erfolgt in Kooperation mit der Medizinischen Fakultät der Universität Leipzig (Prof. M. Löffler).
Grundlagen der Logische Programmierung (Herre, Wagner)
In diesem Projekt werden die theoretische Grundlagen für verallgemeinerte logische Programme mit zwei Arten von Negationen entwickelt. Für die Beschreibung der Semantik derartiger Programme wurden die stabil generierten Modelle eingeführt, die für die normalen logischen Programme den Spezialfall der stabilen Modelle umfassen. Die Forschungsergebnisse zu diesem Thema sollen für die formale Wissensspezifikation und für die Multi-Agentensysteme genutzt werden.
Modelltheorie nichtmonotoner Inferenzsysteme (Dietrich, Herre)
Allgemeines Ziel ist der Aufbau einer nicht-monotonen Modelltheorie, die die endliche Modelltheorie als Spezialfall enthält. Durch die Einführung des Begriffs eines deduktiven und semantischen Frames wurde ein allgemeiner Rahmen geschaffen, nichtmonotone Inferenzsysteme zu klassifizieren und ihre strukturellen Eigenschaften zu untersuchen. Von Bedeutung ist die Einführung verallgemeinerter Kompaktheiteigenschaften, die einen Zusammenhang zwischen einem nicht-monotonen Inferenzsystem und einem monotonen, den gewöhnlichen Kompaktheitssatz erfüllenden inferentielle Teilsystem herstellen. Die Ergebnisse dieser Forschung lassen sich auf die Semantik erweiterter logischer Programme angewenden; ein Beispiel bilden die paraminimalen Modelle.
Multi-Agentensysteme (Wagner, Ho Ngoc Duc)
In dem Forschungsvorhaben werden die logischen Grundlagen von kooperativen Informationssystemen und Multi-Agenten-Systemen untersucht und entsprechende formale Modelle entwickelt. Darauf aufbauend wird eine Logikprogrammiersprache für Multi-Agenten entwickelt. Eines der wichtigsten Ergebnisse dieses Forschungsvorhabens ist die von Dr. G. Wagner entworfene Programmiersprache "VIVA", die in Zusammenarbeit mit der Firma PDC (Prolog Development Center) implementiert wird.
Die formal-logischen Untersuchungen setzen sich auch das Ziel, die Verbindungen zwischen der Theorie der Informationssyteme, der Theorie der Glaubensrevision, der epistemischen Logik und der formalen Handlungstheorie auszuarbeiten.