Alternative Characterizations for Program Equivalence under Answer-Set Semantics Based on Unfounded Sets
Logic programs under answer-set semantics constitute an important tool for declarative problem solving. In recent years, two research issues received growing attention. On the one hand, concepts like loops and elementary sets have been proposed in order t
- PDF / 540,386 Bytes
- 18 Pages / 430 x 660 pts Page_size
- 26 Downloads / 184 Views
2
3
Institut f¨ur Informatik, Universit¨at Potsdam, August-Bebel-Straße 89, D-14482 Potsdam, Germany {gebser,torsten}@cs.uni-potsdam.de Institut f¨ur Informationssysteme 184/3, Technische Universit¨at Wien, Favoritenstraße 9-11, A-1040 Vienna, Austria [email protected] Institut f¨ur Informationssysteme 184/2, Technische Universit¨at Wien, Favoritenstraße 9-11, A-1040 Vienna, Austria [email protected]
Abstract. Logic programs under answer-set semantics constitute an important tool for declarative problem solving. In recent years, two research issues received growing attention. On the one hand, concepts like loops and elementary sets have been proposed in order to extend Clark’s completion for computing answer sets of logic programs by means of propositional logic. On the other hand, different concepts of program equivalence, like strong and uniform equivalence, have been studied in the context of program optimization and modular programming. In this paper, we bring these two lines of research together and provide alternative characterizations for different conceptions of equivalence in terms of unfounded sets, along with the related concepts of loops and elementary sets. Our results yield new insights into the model theory of equivalence checking. We further exploit these characterizations to develop novel encodings of program equivalence in terms of standard and quantified propositional logic, respectively.
1 Introduction Among the plethora of semantics that emerged during the nineties of the twentieth century for giving meaning to logic programs with nonmonotonic negation, two still play a major role today: firstly, the answer-set semantics, due to Gelfond and Lifschitz [1], and secondly, the well-founded semantics, due to Van Gelder, Ross, and Schlipf [2]. While the answer-set semantics adheres to a multiple intended models approach, representing the canonical instance of the answer-set programming (ASP) paradigm [3], the well-founded semantics is geared toward efficient query answering and can be seen as a skeptical approximation of the answer-set semantics. In this paper, our interest lies with the answer-set semantics of nonmonotonic logic programs. The results developed here can informally be described as linking two research issues in the context of the answer-set semantics by way of the central constituents of the well-founded semantics, viz. unfounded sets [2,4]. Let us explain this in more detail.
This work was partially supported by the Austrian Science Fund (FWF) under grant P18019.
S. Hartmann and G. Kern-Isberner (Eds.): FoIKS 2008, LNCS 4932, pp. 24–41, 2008. c Springer-Verlag Berlin Heidelberg 2008
Alternative Characterizations for Program Equivalence
25
An important concept in logic programming is Clark’s completion [5], which associates logic programs with theories of classical logic. While every answer set of a logic program P is also a model of the completion of P , the converse does not hold in general. As shown by Fages [6], a one-to-one correspondence is obtained i
Data Loading...
