Enscheidungsverfahren und Modellbildung: Fuzzy-Logiken

Automatisches Beweisen (Automated Reasoning) wird oft nur im engen Sinn von "Suche nach Beweisen gültiger Formeln" verstanden. Die meisten Anwendungen dieses Gebietes profitieren jedoch von Systemen die auch folgende Eigenschaften aufweisen: 1. Das Beweisprogramm sollte - für möglichst große, syntaktisch charakterisierbare Klassen von Formeln - terminieren, auch wenn kein Beweis für die Input-Formel existiert. 2. Das Programm sollte für nicht beweisbare Formeln (soweit möglich) eine Beschreibung eines entsprechenden Gegenmodells ausgeben. Die eng verwandten Forschungsgebiete Beweissuchbasierte Entscheidungsverfahren und Automatische Modellbildung haben diese beiden Fragestellungen im Visier. In beiden Gebieten wurden für den Bereich der klassischen Logik bereits substantielle Fortschritte erzielt. Die (oft exklusive) Konzentration auf klassische Logik - speziell im Fall der automatischen Modellbildung - steht im Widerspruch zur zunehmenden Bedeutung nicht-klassischer Logiken in vielen Bereichen der Informatik. Insbesonders ist bekannt, dass die klassische (zweiwertige) Logik schlecht zur Formalisierung des Schließens mit vagen Begriffen und Informationen geeignet ist. Es ist kaum sinnvoll zu bestreiten, dass die Maschinerie der Fuzzy-Logik für so wichtige Aufgaben wie die Formalisierung von natürlichsprachlichen Prädikaten, für die Repräsentation vager Information und das Schließen mit unscharfen Begriffen in Einsatz gebracht werden muss. Erst jüngst wurde eine solide und breite mathematische Basis für die Deduktion in diversen Systemen der Fuzzy-Logik erarbeitet. Es sind gerade die genannten deduktionsorientierten Aufgaben der Fuzzy-Logik deren Lösung Programmsysteme verlangt, die nicht nur die Beweissuche unterstützen, sondern auch geeignet sind logische Gültigkeit algorithmisch zu entscheiden und die Information über (Gegen-)Modelle liefern können, falls die Beweissuche scheitert. Entsprechend zielt dieses Projekt auf die Entwicklung beweissuchbasierter Entscheidungsverfahren und von Algorithmen zur Modellbildung für die wichtigsten Systeme der Fuzzy-Logik ab. Darüberhinaus werden anlaloge Probleme auch für verwandte Logiksysteme untersucht werden.

Fuzzy-Logiken sind mathematische Werkzeuge zur Modellierung von formalem Schließen mit vagen Informationen und Konzepten. Nicht zuletzt die rapide Zunahme der Bedeutung des Internets als gleichsam universelle, aber weitgehend natürlich-sprachliche und daher oft vage Informationsquelle begründet das Interesse an mathematischen Erkenntnissen zu verschiedensten Fuzzy-Logiken und insbesondere an Algorithmen, sogenannten Entscheidungsprozeduren, die es erlauben, automatisch festzustellen, ob logische Konsequenzbeziehungen zwischen gegebenen Formeln der einzelnen Logiken bestehen oder nicht. Im Rahmen dieses Projektes wurden eine Reihe von Beweisverfahren zu den wichtigsten Fuzzy-Logiken vor allem in Hinblick auf ihre Brauchbarkeit als Basis für Entscheidungsverfahren analysiert. Als ein Hauptergebnis wurde ein Kalkül entwickelt, der erstmalig erlaubt, formale, analytische Beweise in den drei grundlegenden propositionalen Fuzzy-Logiken -- Lukasiewicz-Logik, Gödel-Logik und Produktlogik -- auf uniforme Weise systematisch zu entwickeln. Dieser Kalkül besitzt außerdem eine Reihe weiterer günstiger Eigenschaften, die ihn als eine gute Grundlage für Entscheidungsverfahren ausweisen. Insbesondere wurden auch Kalkülvarianten entwickelt, die systematische Beweissuche mit nachweisbar optimalem rechnerischem Aufwand zulassen. Über die erwähnten Entscheidungsverfahren hinausgehend wurde auch folgende Fragestellung erfolgreich angegangen: Wenn ein vollständiges (fuzzy-logisches) Beweissystem terminiert, ohne einen Beweis gefunden zu haben, was lässt sich dann über konkrete Gegenmodelle aussagen? Detaillierte Antworten konnten vor allem für die Gödel-Logik erzielt werden; das ist jene Fuzzy-Logik, die auf einfachst mögliche Weise das Konzept repräsentiert, dass Aussagen im Allgemeinen nicht nur einfachhin definitiv wahr oder definitiv falsch sind, sondern vielmehr nach dem im Prinzip beliebigen Grad ihrer jeweiligen Wahrheit geordnet und verglichen werden können. Als ein weiterer Schwerpunkt der erzielten Forschungsergebnisse rücken formale Dialogspiele in den Vordergrund, die in enger Verbindung zu den erwähnten Beweiskalkülen stehen und auf direkte Weise erlauben, den systematischen Umgang mit logisch komplexer, aber vager Information zu modellieren. Dabei wurde sichtbar, dass es eine Reihe konkurrierender Konzepte der Vagheit im Auge zu behalten gilt. Die systematische Analyse von Dialogspielen in diesem Zusammenhang wird im Brennpunkt nachfolgender Forschungsprojekte stehen.