[Back]


Diploma and Master Theses (authored and supervised):

J. Oetsch:
"Beyond Uniform Equivalence between Answer-Set Programs: Relativisation and Projection";
Supervisor: H. Tompits; Institut für Informationssysteme, 2012; final examination: 2013-01-15.



English abstract:
This thesis deals with advanced notions of equivalence between nonmonotonic logic programs under the answer-set semantics, a topic of increasing interest because such notions form the basis for program optimisation, debugging, modular programming, and program verification.
In fact, there is extensive research in answer-set programming (ASP) dealing with different notions of equivalence between programs. Prominent among these notions is uniform equivalence which checks whether two programs have the same semantics when joined with an arbitrary set of facts. In this thesis, we study a family of more fine-grained versions of uniform equivalence, viz. relativised uniform equivalence with projection, which extends standard uniform equivalence in terms of two additional parameters: one for specifying the input alphabet and one for specifying the output alphabet for programs. In particular, the second parameter is used for projecting answer sets to a set of designated output atoms. Answer-set projection, in particular, allows to compare programs that make use of different auxiliary atoms which is important for practical programming aspects.
We introduce novel semantic characterisations for the program correspondence problems under consideration and analyse the computational complexity of deciding these problems. In the general case, deciding these problems lies on the third level of the polynomial hierarchy. There- fore, this task cannot be efficiently reduced to propositional answer-set programs itself (under the usual complexity-theoretic assumptions). However, reductions to quantified Boolean formulas (QBFs) are feasible. Indeed, we provide efficient, in fact, linear-time constructible, reductions to QBFs and discuss simplifications for certain special cases. These QBF reductions yield the basis for a prototype implementation, the system ccT, for deciding correspondence problems by using external QBF solvers. We discuss an application of ccT for verifying the correctness of students´ solutions drawn from a laboratory course on logic programming and knowledge representation at the Vienna University of Technology, employing relativised uniform equivalence with projection as the underlying program correspondence notion. We complement our investigation by discussing a performance evaluation of ccT, showing that discriminating among different back-end solvers for quantified propositional logic is a crucial issue towards optimal performance.

German abstract:
Diese Arbeit beschäftigt sich mit erweiterten Äquivalenzbegriffen für nichtmonotone logische Programme unter der Answer-Set Semantik. Dieses Thema erfreut sich zunehmendem Interesse da solche Äquivalenzbegriffe die theoretische Basis für viele Entwicklungsaufgaben wie Optimierung von Programmen, Debugging, modulares Programmieren und Verifikation bilden.
Verschiedene Äquivalenzbegriffe für Logikprogramme sind ein relevanter Forschungsschwerpunkt auf dem Gebiet der Answer-Set Programmierung (ASP). Ein prominenter Vertreter eines solchen Äquivalenzbegriffes ist uniforme Äquivalenz, welche überprüft ob zwei Programme, vereint mit einer beliebigen Menge von Fakten, die gleiche Semantik besitzen. In dieser Diplomarbeit studieren wir eine Familie von verfeinerten Versionen der uniformen Äquivalenz, nämlich relativierte uniforme Äquivalenz mit Projektion, welche gewöhnliche uniforme Äquivalenz durch zwei zusätzliche Parameter ergänzt: einen, um das Eingabealphabet der Programme zu spezifizieren, und einen, um das Ausgabealphabet festzulegen. Der zweite Parameter wird benötigt um Answer Sets auf bestimmte Ausgabeatome zu projizieren. Diese Answer-Set Projektion erlaubt es, im speziellen, Programme, die auf Hilfsatome zurückgreifen, miteinander zu vergleichen. Dieser Aspekt ist aufgrund praktischer Erfordernisse unerlässlich.
Wir führen neue semantische Charakterisierungen für die betrachtete Formen der Programmäquivalenz ein, und wir analysieren die strukturelle Berechnungskomplexität entsprechender Entscheidungsprobleme. Im allgemeinen Fall befinden sich diese Probleme auf der dritten Ebene der polynomiellen Hierarchie und können daher, unter den üblichen koplexitätstheoretischen Annahmen, nicht auf (propositionale) Answer-Set Programme selbst reduziert werden. Dennoch sind Problemreduktionen auf quantifizierte Boole´sche Formeln (QBFs) möglich. Wir beschreiben solche Reduktionen auf QBFs und diskutieren Vereinfachungen für spezielle Sonderfälle von Äquivalenzproblemen.
Die betrachteten Übersetzungen haben die Eigenschaft, dass sie immer effizient, sogar in linearer Zeit, konstruierbar sind. Diese QBF Reduktionen liefern die Basis für eine Prototyp-Implementierung in Form des Systems ccT. Der in diesem System realisierte Ansatz basiert auf der Übersetzung eines Programmkorrespondenzproblems in QBFs sowie der Verwendung externer QBF Beweiser zur Lösung der resultierenden Formeln. Wir beschreiben eine Anwendung von ccT um die Korrektheit von Programmen zu verifizieren, die als Lösungen von Studenten im Rahmen von Lehrveranstaltungen über logische Programmierung und Wissensrepräsentation an der TU Wien eingereicht wurden. Der zugrundeliegende Äquivalenzbegriff um Korrektheit zu entscheiden ist relativierte uniforme Äquivalenz mit Projektion. Schließlich komplementieren wir unsere Untersuchungen mit einer Leistungsevaluierung von ccT, welche zeigt, dass es wesentlich ist zwischen verschiedenen QBF Beweisern zu unterscheiden um eine optimale Performanz zu erreichen.

Keywords:
answer-set programming, program equivalence, nonmonotonic reasoning, quantified Boolean formulas


Electronic version of the publication:
http://publik.tuwien.ac.at/files/PubDat_217154.pdf


Created from the Publication Database of the Vienna University of Technology.