Nonmonotonic logic programs with function symbols

Abstract

Antwortmengen-Programmierung (ASP) ist ein wichtiges Paradigma zur regelbasierten deklarativen Problemlösung. ASP ist besonders gut geeignet, Probleme zu modellieren und zu lösen, welche ,,Common-sense Schließen`` beinhalten, und mit vielen Anwendungsdomänen, darunter Planen, Diagnose, Meinungsberichtigung, Konfiguration, Datenintegration, Sicherheitstechnik, Text Klassifikation, und vieles mehr. Derzeit bekannte entscheidbare Klassen von ASP Programmen und deren Implementierungen basieren hauptsächlich auf funktionsfreien Sprachen, die eine eingeschränkte Ausdruckskraft und Nachteile bei der Wissensrepräsentation haben. Sie unterbinden zum Beispiel die Modellierung von unendlichen Prozessen, unbegrenzter Zeit, und rekursiven Datenstrukturen.<br />Funktionssymbole bieten die Möglichkeit zur Erzeugung von unendlichen Domänen und Objekten, und sie erlauben eine natürlichere Repräsentation von Problemen in den zuvor genannten Bereichen. Leider macht eine uneingeschränkte Verwendung von Funktionssymbolen ASP im hohen Maße unentscheidbar. Die Hauptbeiträge dieser Dissertation sind zwei entscheidbare Fragmente von ASP, die wir FDNC and BD nennen. Die zwei Sprachen sind ausdrucksstarke Formalismen für die regelbasierte Modellierung von Anwendungen mit möglicherweise unendlichen Prozessen oder Objekten, die auch Common-sense Schließen mit nichtmonotoner Negation unterstützen. Sie können zur Lösung von Planungsproblemen angewendet werden, zur Modellierung und zum Schlussfolgern über rekursive Datenstrukturen---im Speziellen baumförmige Datenstrukturen wie HTML oder XML Dokumente---, und zur Repräsentation von Ontologien in einigen Beschreibungslogiken verwendet werden. Wir entwickeln neue Algorithmen für wichtige ASP Schlussfolgerungsprobleme und geben eine detailierte Beschreibung der Berechnungskomplexität des Schließens in allgemeinen FDNC und BD Programmen, wie auch in einer Reihe von syntaktischen Fragmenten dieser Sprachen.<br />

Answer Set Programming (ASP) is a rule-based declarative problem solving paradigm that couples Logic Programming with Nonmonotonic Reasoning. ASP is well-suited for modeling and solving problems that involve common-sense reasoning, and it has been fruitfully exploited in many application domains including planning, diagnosis, belief revision, configuration, data integration, security engineering, text classification and others.<br />Current decidable ASP frameworks and their implementations are based mainly on function-free programs whose models are finite relational structures. It is widely acknowledged that this function-free setting leads to expressiveness drawbacks, and can be inconvenient for knowledge representation, as it prohibits modeling, among others, infinite processes, indefinite time, and recursive data structures. Function symbols are a very convenient means for generating infinite domains and objects, and allow a more natural representation of problems in the above domains. Unfortunately, an unrestricted use of function symbols makes ASP highly undecidable.<br />The main contributions of this thesis are the FDNC and BD families of logic programs with function symbols, two powerful families of languages that allow for modeling in applications with potentially infinite processes or objects, accommodating common-sense reasoning through default negation. They can be applied in solving planning problems, modeling and reasoning about recursive data structures---especially, tree-shaped data, like HTML or XML documents---and to represent ontologies in some description logics. We develop novel algorithms for important ASP reasoning problems, and give a detailed account of the computational complexity of reasoning in full FDNC and BD programs, and also in a range of syntactic fragments of these languages.<br />