Parametrisierte Komplexität nichtklassischer Logiken

Nach heutigem Wissensstand ist nur sehr wenig über die parametrisierte Komplexität im Bereich Programmverifikation und künstlicher Intelligenz bekannt. In diesem Projekt wird sowohl die Parametrisierung als auch der Einfluss der Parametrisierung auf die Komplexität der wichtigen Entscheidungsprobleme, wie z.B. Erfüllbarkeit und Model Checking, untersucht. Im Bereich der nicht-monotonen Logiken werden wir Probleme des natürlichen Schließens betrachten. Darüber hinaus wollen wir Normalformen in Bezug auf die Parametrisierung finden, die die gewöhnlich hohe Komplexität dieser Probleme erklären.

Sinnvolle Parametrisierung

Wir fokussieren uns auf die Vorteile der Parametrisierung im Bereich der modal Logik, sowie der nicht-monotone Logiken, da es bis jetzt kaum Ansätze dieser Art gibt. Dabei wollen wir die Kenntnisse über die Wechselwirkungen von Parametrisierung mit den Konzepten dieser Logiken verbessern.

Klassifizierung der parametrisierten Komplexität in Bezug auf die Fragmente der temporalen und der nicht-monotonen Logiken

Es wurden bereits eine enorme Anzahl an Klassifikationen der Komplexität von Fragmenten für jede der genannten Logiken angefertigt. Bei der Klassifizierung der parametrisierten Komplexität dieser Fragmente wollen wir unser Wissen und unsere Intuition über die Wechselwirkungen von modalen, bzw. nichtmonotonen Operatoren mit Booleschen Funktionen vertiefen. Können ähnliche Beobachtungen wie z.B. in der Aussagenlogik gemacht werden?

Einfluss der Nichtmonotonie

Im letzten Projektabschnitt werden wir die Kenntnisse über die erhaltenen Klassifikationen der vorherigen Abschnitte analysieren, um eine Gesamtübersicht zu erstellen. Insbesondere werden wir uns der Frage widmen, wie das Konzept der Nichtmonotonie sich auf die Effizienz eines Problems auswirkt. Eine der wichtigsten Fragen in diesem Kontext ist, ob es eine inhärente Struktur der Erweiterungen gibt, die in Kombination mit Parametrisierungen, Ineffizienz sogar in der parametrisierten Version des Problems immer erzeugt.