In many cases, a logic program can be divided into two parts, so that one of them, the "bottom" part, does not refer to the predicates defined in the "top" part. The "bottom" rules can be used then for the evaluation of the predicates that they define, and the computed values can be used to simplify the "top" definitions. We discuss this idea of splitting a program in the context of the answer set semantics. The main theorem shows how computing the answer sets for a program can be simplified when the program is split into parts. The programs covered by the theorem may use both negation as failure and classical negation, and their rules may have disjunctive heads. The usefulness of the concept of splitting for the investigation of answer sets is illustrated by several applications. First, we show that a conservative extension theorem by Gelfond and Przymusinska and a theorem on the closed world assumption by Gelfond and Lifschitz are easy consequences of the splitting theorem. Second, (locally) stratified programs are shown to have a simple characterization in terms of splitting. The existence and uniqueness of an answer set for such a program can be easily derived from this characterization. Third, we relate the idea of splitting to the notion of order-consistency.

PDF

In Proceedings of International Conference on Logic Programming (ICLP), Van Hentenryck, Pascal (Eds.), pp. 23-37 1994.

@inproceedings{lif94e, title={Splitting a Logic Program}, author={Vladimir Lifschitz and Hudson Turner}, booktitle={Proceedings of International Conference on Logic Programming (ICLP)}, editor={Van Hentenryck and Pascal}, pages={23-37}, url="http://www.cs.utexas.edu/users/ai-lab?lif94e", year={1994} }