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.