Beyond uniform equivalence between answer-set programs : relativisation and projection

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. 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.<br />

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.<br />In fact, there is extensive research in answer-set programming 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.