Algorithmen und Komplexität für logische Entscheidungsprobleme und deren Anwendungen in der Wissensrepräsentation

点击翻译按钮获取中文摘要

Konkretes Ziel der zweiten Projektphase soll daher sein, verschiedene Ansätze zur Entwicklung von Entscheidungsalgorithmen für Logiken zu vergleichen und miteinander zu integrieren. Insbesondere sollen hier tableau- und automatenbasierte Verfahren für Beschreibungs- und Modallogiken sowie GF untersucht werden, mit dem Ziel einen einheitlichen algorithmischen Ansatz zu erhalten, der die Vorteile beider Verfahren aufweist. Die so erhaltenen Algorithmen sollen wieder prototypisch implementiert und evaluiert werden. Ein weiteres Ziel ist die Konstruktion effizienter Algorithmen für das Auswertungsproblem dieser Logiken. Schließlich soll für die hier betrachteten Logiken der Zusammenhang zwischen der Struktur von formeln und ihren algorithmischen Eigenschaften analysiert werden. Solche Resultate sollen einerseits dazu dienen, effizient entscheidbare Fragmente in diesen Logiken zu isolieren, sie sollen andererseits eine Basis zur Konstruktion Wahrscheinlichkeitsverteilungen von Formeln liefern, unter denen das average-case Verhalten von Entscheidungsverfahren analysiert werden kann.