KR Conference 2012 Short Paper
- Yisong Wang
- Yan Zhang
- Yi Zhou
- Mingyi Zhang
Wang (2008) then proposed a semantic forgetting for consistent disjunctive logic programs, which preserves equivalence but not strong equivalence. They specifically indicated the importance of preserving strong equivalence in logic programming forgetting and raised this issue as a future work. Wong (2009) proposed two forgetting operators for disjunctive logic programs. Although Wong’s forgetting indeed preserves strong equivalence, it may lose the intuition of weakening under various circumstances (see Related Work for details). In addition to preserving strong equivalence, expressibility is another desired criterion for logic programming forgetting. Ideally we would expect that the result of forgetting some atoms from a logic program is still expressible by a logic program. Finally, we believe that as a way of weakening, forgetting in logic programs should obey some common intuitions shared by forgetting in classical logics. For instance, forgetting something from a logic program should lead to a weaker program in certain sense. On the other hand, such weakening should only be associated to the relevant information that has been forgotten. For this purpose, Zhang and Zhou (2009) proposed four forgetting postulates to formalize these common intuitions and showed that forgetting in classical propositional logic and modal logic S5 can be precisely captured by these postulates. Interestingly, none of previous forgetting notions in logic programs actually satisfies Zhang-Zhou’s postulates. In summary, we consider the following criteria that a forgetting notion in logic program should meet: • Expressibility. The result of forgetting in an arbitrary logic program should also be expressible via an arbitrary logic program; • Preserving strong equivalence. Two strongly equivalent programs should remain strongly equivalence after forgetting the same set of atoms; • Satisfying common intuitions of forgetting. Preferably, forgetting in logic programs should be semantically characterized by Zhang-Zhou’s four forgetting postulates. In this paper we present a comprehensive study on forgetting in the context of arbitrary logic programs (propositional theories) under answer set semantics. In our approach, a program Π is viewed as a theory of the logic of here-andthere (or simply called HT logic), then forgetting a set V of In this paper, we propose a semantic forgetting for arbitrary logic programs (or propositional theories) under answer set semantics, called HT-forgetting. The HTforgetting preserves strong equivalence in the sense that strongly equivalent logic programs will remain strongly equivalent after forgetting the same set of atoms. The result of an HT-forgetting is always expressible by a logic program, and in particular, the result of an HT-forgetting in a Horn program is expressible in a Horn program; and a representation theorem shows that HT-forgetting can be precisely characterized by Zhang-Zhou’s four forgetting postulates under the logic of here-and-there. We also reveal underlying connections between HTforgetting and classical forgetting, and provide complexity results for decision problems.