Uniform approximation-theoretic semantics for logic programs with external atoms

Abstract

HEX Programme sind klassische disjunktive Logikprogramme, erweitert um externe Atome und Atome höherer Stufe. Externe Atome erlauben es, beliebige Boolesche Funktionen darzustellen und ermöglichen so den Zugang zu externen Ressourcen (zB prozeduralen Programmen und Datenbanken) und die Repräsentierung unterschiedlicher Formalismen (zB DL Programme, Logikprogramme mit Aggregaten, etc.), ohne dabei die deklarative Natur der Semantik einzubüßen. Dies wurde erreicht, indem Gebrauch von der {\em FLP-Antwortmengensemantik} gemacht wurde.<br />Die wohl-fundierte- und die Antwortmengensemantik, obwohl, wie später gezeigt wurde, eng zusammenhängend, sind von Grund auf unterschiedlicher Natur. Wird eine neue Klasse von Logikprogrammen definiert, so werden, in der Regel, die entsprechenden Definitionen dieser klassischen Semantiken ``zu Fuß'' adaptiert. Die {\em Approximationstheorie} (engl.:<br />{\em approximation theory}) schlägt stattdessen einen uniformen, algebraischen Weg vor: basierend auf der Tatsache, dass alle klassichen Semantiken (zB auch die Kripke-Kleene- und Supported Semantik) durch Fixpunkte entsprechender Ein-Schritt-Ableitungsoperatoren charakterisiert werden, können, wie in der Theorie gezeigt, wohl-fundierte- und Antwortmengensemantik als Fixpunkte eines einzigen Operators charakterisiert werden. Da sich dieser Operator in der Regel leicht auf neue Programmklassen erweitern lässt, bietet die Approximationstheorie ein praktikables Werkzeug zur Adaptierung klassischer Semantiken.<br />Im ersten Teil dieser Arbeit erweitern wir den klassischen van Emden-Kowalski Operator und den klassischen Fitting Operator auf die Klasse normaler (d.h. nicht-disjunktiver) HEX Programme, und definieren (i) eine (ultimative) Kripke-Kleene-, (ii) eine (ultimative) wohl-fundierte-, und (iii) eine (ultimate 3-wertige) Antwortmengensemantik mit Hilfe der Approximationstheorie. Dadurch erhalten wir eine (ulitmative) 2-wertige Antwortmengensemantik die keine selbstbegründeten Atome enthält und eine wohl-fundierte Semantik die mit der FLP-Antwortmengensemantik kompatibel sind. Für monotone, normale HEX Programme fällt die 2-wertige Antwortmengensemantik mit der FLP-Antwortmengensemantik zusammen.<br />Für die Klasse der disjunktiven HEX Programme ist die Approximationstheorie zwar nicht direkt anwendbar, doch durch die Kombination von Ideen aus der Approximationstheorie, der Logikprogrammierung mit Aggregaten, und der disjunktiven Logikprogrammierung, definieren wir eine 2-wertige (ultimative) Antwortmengensemantik für disjunktive HEX Programme basierend auf nicht-deterministischen Operatoren. Weiters zeigen wir, dass diese Semantik folgende wünschneswerte Eigenschaften besitzt: (ultimative) Antwortmengen sind minimal, supported, und ableitbar in Form von kunstruktiven Berechnungen.<br />Die in dieser Arbeit erhaltenen Semantiken lassen sich, da HEX Programme sehr allgemein sind, auf verschiedenste, durch HEX Programme repräsentierbare, Formalismen anwenden.

HEX programs are disjunctive logic programs under so called {\em FLP-answer-set semantics} enhanced with higher-order and external atoms.<br />Since external atoms are generic in the sense that they can represent arbitrary computable Boolean functions, many formalisms (e.g., dl-programs, logic programs with aggregates, etc.) can be simulated by HEX programs.<br />For the class of classical logic programs, major semantics can be characterized in terms of fixpoints of lattice operators defining one step of logical derivation. However, for logic programs with negation, these operators may be nonmonotone, and in this case the fixpoint theory of Tarksi and Knaster is not applicable. Approximation Theory, on the other hand, is an algebraic framework for studying fixpoints of monotone and {\em nonmonotone} lattice operators, and thus extends the theory of Tarski and Knaster to the more general class of arbitrary lattice operators.<br />In the first part of the thesis we extend the classical van Emden-Kowalski operator, and the classical Fitting operator to the class of normal (i.e., disjunction-free) HEX programs, and uniformly define (i) (ultimate) Kripke-Kleene-, (ii) (ultimate) well-founded-, and (iii) (3-valued ultimate) answer-set semantics by applying Approximation Theory. As a result, we obtain well-supported 2-valued (ultimate) answer-set semantics, and well-founded semantics compatible with the standard FLP-answer-set semantics. For monotone normal HEX programs, 2-valued answer-set semantics coincide with the standard FLP-answer-set semantics.<br />In the case of disjunctive HEX programs, Approximation Theory is not directly applicable. However, by combining ideas from Approximation Theory, logic programs with aggregates, and disjunctive logic programming, we define 2-valued (ultimate) answer-set semantics of disjunctive HEX programs based on non-deterministic operators. We show that these semantics satisfy some desirable properties. Particularly, we show that (ultimate) answer sets are minimal, supported, and derivable in terms of bottom-up computations.<br />As HEX programs are generic formalisms, the obtained semantics can be applied for a range of formalisms.