In answer set programming, combinatorial search problems are solved by writing logic programs the answer sets of which correspond to solutions. Such programs often contain auxiliary atoms, "defined" in terms of atoms introduced earlier. To prove that the answer sets of a program containing definitions correspond to the solutions of the prob- lem we want to solve, we need to understand how adding definitions aects the collection of answer sets. In particular, it is useful to be able to describe the eects of adding definitions to a program with nested expressions, in view of the relation of this class of programs to the in- put language of the answer set programming system smodels. In this paper we generalize the splitting set theorem to programs with nested expressions and show how this generalization can be used to prove pro- gram correctness in answer set programming. We also show that, under certain conditions, adding explicit and recursive definitions to a program with nested expressions extends its answer sets conservatively.

PS

In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), Vladimir Lifschitz and Ilkka Niemel{"a} (Eds.), pp. 114-126 2004.

@Inproceedings{sel03, title={Definitions in Answer Set Programming}, author={Selim T. Erdoğan and Vladimir Lifschitz}, booktitle={Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR)}, editor={Vladimir Lifschitz and Ilkka Niemel{"a}}, pages={114-126}, url="http://www.cs.utexas.edu/users/ai-lab?sel03", year={2004} }