The doctoral dissertations of the former Helsinki University of Technology (TKK) and Aalto University Schools of Technology (CHEM, ELEC, ENG, SCI) published in electronic format are available in the electronic publications archive of Aalto University - Aaltodoc.
Aalto

Modularity in Answer Set Programs

Emilia Oikarinen

Dissertation for the degree of Doctor of Science in Technology to be presented with due permission of the Faculty of Information and Natural Sciences for public examination and debate in Auditorium T2 at Helsinki University of Technology (Espoo, Finland) on the 24th of October, 2008, at 12 noon.

Overview in PDF format (ISBN 978-951-22-9582-1)   [463 KB]
Dissertation is also available in print (ISBN 978-951-22-9581-4)

Abstract

Answer set programming (ASP) is an approach to rule-based constraint programming allowing flexible knowledge representation in variety of application areas. The declarative nature of ASP is reflected in problem solving. First, a programmer writes down a logic program the answer sets of which correspond to the solutions of the problem. The answer sets of the program are then computed using a special purpose search engine, an ASP solver. The development of efficient ASP solvers has enabled the use of answer set programming in various application domains such as planning, product configuration, computer aided verification, and bioinformatics.

The topic of this thesis is modularity in answer set programming. While modern programming languages typically provide means to exploit modularity in a number of ways to govern the complexity of programs and their development process, relatively little attention has been paid to modularity in ASP. When designing a module architecture for ASP, it is essential to establish full compositionality of the semantics with respect to the module system. A balance is sought between introducing restrictions that guarantee the compositionality of the semantics and enforce a good programming style in ASP, and avoiding restrictions on the module hierarchy for the sake of flexibility of knowledge representation.

To justify a replacement of a module with another, that is, to be able to guarantee that changes made on the level of modules do not alter the semantics of the program when seen as an entity, a notion of equivalence for modules is provided. In close connection with the development of the compositional module architecture, a transformation from verification of equivalence to search for answer sets is developed. The translation-based approach makes it unnecessary to develop a dedicated tool for the equivalence verification task by allowing the direct use of existing ASP solvers.

Translations and transformations between different problems, program classes, and formalisms are another central theme in the thesis. To guarantee efficiency and soundness of the translation-based approach, certain syntactical and semantical properties of transformations are desirable, in terms of translation time, solution correspondence between the original and the transformed problem, and locality/globality of a particular transformation.

In certain cases a more refined notion of minimality than that inherent in ASP can make program encodings more intuitive. Lifschitz' parallel and prioritized circumscription offer a solution in which certain atoms are allowed to vary or to have fixed values while others are falsified as far as possible according to priority classes. In this thesis a linear and faithful transformation embedding parallel and prioritized circumscription into ASP is provided. This enhances the knowledge representation capabilities of answer set programming by allowing the use of existing ASP solvers for computing parallel and prioritized circumscription.

This thesis consists of an overview and of the following 7 publications:

  1. Emilia Oikarinen and Tomi Janhunen. 2008. Achieving compositionality of the stable model semantics for SMODELS programs. Theory and Practice of Logic Programming, to appear.
  2. Tomi Janhunen, Emilia Oikarinen, Hans Tompits, and Stefan Woltran. 2007. Modularity aspects of disjunctive stable models. In: Chitta Baral, Gerhard Brewka, and John Schlipf (editors). Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2007). Tempe, AZ, USA. 15-17 May 2007. Springer. Lecture Notes in Artificial Intelligence, volume 4483, pages 175-187. © 2007 Springer Science+Business Media. By permission.
  3. Tomi Janhunen and Emilia Oikarinen. 2007. Automated verification of weak equivalence within the Smodels system. Theory and Practice of Logic Programming, volume 7, number 6, pages 697-744.
  4. Emilia Oikarinen and Tomi Janhunen. 2008. A translation-based approach to the verification of modular equivalence. Journal of Logic and Computation, Advance Access published, doi:10.1093/logcom/exn039.
  5. Tomi Janhunen and Emilia Oikarinen. 2004. Capturing parallel circumscription with disjunctive logic programs. In: José Júlio Alferes and João Leite (editors). Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA 2004). Lisbon, Portugal. 27-30 September 2004. Springer. Lecture Notes in Artificial Intelligence, volume 3229, pages 134-146. © 2004 Springer Science+Business Media. By permission.
  6. Emilia Oikarinen and Tomi Janhunen. 2005. CIRC2DLP – translating circumscription into disjunctive logic programming. In: Chitta Baral, Gianluigi Greco, Nicola Leone, and Giorgio Terracina (editors). Proceedings of the 8th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2005). Diamante, Italy. 5-8 September 2005. Springer. Lecture Notes in Artificial Intelligence, volume 3662, pages 405-409. © 2005 Springer Science+Business Media. By permission.
  7. Emilia Oikarinen and Tomi Janhunen. 2008. Implementing prioritized circumscription by computing disjunctive stable models. In: Danail Dochev, Marco Pistore, and Paolo Traverso (editors). Proceedings of the 13th International Conference on Artificial Intelligence: Methodology, Systems, and Applications (AIMSA 2008). Varna, Bulgaria. 4-6 September 2008. Springer. Lecture Notes in Artificial Intelligence, volume 5253, pages 167-180. © 2008 Springer Science+Business Media. By permission.

Errata of publications 2, 4 and 5

Keywords: modular program development, module theorem, stable models, compositional semantics, equivalence verification, congruence relations, parallel and prioritized circumscription, faithful transformations, answer set programming, nonmonotonic reasoning

This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.

© 2008 Helsinki University of Technology

Last update 2011-05-26