Logo Leibniz Universität Hannover
Logo:Institut für Theoretische Informatik
Logo Leibniz Universität Hannover
Logo:Institut für Theoretische Informatik
  • Zielgruppen
  • Suche
 

Erfüllbarkeitsprobleme

Das Erfüllbarkeitsproblem, also das Berechnungsproblem, von einer gegebenen aussagenlogischen Formel zu entscheiden, ob sie erfüllbar ist, ist das klassische NP-vollständige Problem, dessen Studium die Entwicklung der Komplexitätstheorie in nicht zu unterschützendem Ausmaß geprägt hat. Bekannterweise erlauben eingeschränkte Formelklassen effiziente Entscheidungsalgorithmen, z. B. die bekannten Horn-Formeln. In diesem Projekt soll die Grenze zwischen algorithmischer Nicht-Handhabbarkeit und effizienter Lösbarkeit für Erfüllbarkeitsprobleme und verwandte algorithmische Fragestellungen in verschiedenen logischen Formalismen genau bestimmt werden unter besonderer Berücksichtigung einer möglichst genauen komplexitätstheoretischen Klassifizierung der effizienten Fülle, etwa im Hinblick auf Speicherbedarf oder Parallelisierbarkeit.

Einen besonderen Schwerpunkt bei unseren Untersuchungen sollen sog. nichtmonotone Logiken spielen, die Verwendung vor allem in Bereichen wie Wissensrepräsentation, Semantic Web, Expertensysteme, etc. finden.

Methodisch sollen die Untersuchungen auf Mittel der universellen Algebra, insbesondere den Post'schen Graphen abgeschlossener Klassen von Boole'schen Funktionen, zurückgreifen.

Ausgewählte Publikationen