On the existence of stable models of non-stratified logic programs

Abstract

In this paper we analyze the relationship between cyclic definitions and consistency in Gelfond-Lifschitz's answer sets semantics (originally defined as ‘stable model semantics’). This paper introduces a fundamental result, which is relevant for Answer Set programming, and planning. For the first time since the definition of the stable model semantics, the class of logic programs for which a stable model exists is given a syntactic characterization. This condition may have a practical importance both for defining new algorithms for checking consistency and computing answer sets, and for improving the existing systems. The approach of this paper is to introduce a new canonical form (to which any logic program can be reduced to), to focus the attention on cyclic dependencies. The technical result is then given in terms of programs in canonical form (canonical programs), without loss of generality: the stable models of any general logic program coincide (up to the language) to those of the corresponding canonical program. The result is based on identifying the cycles contained in the program, showing that stable models of the overall program are composed of stable models of suitable sub-programs, corresponding to the cycles, and on defining the Cycle Graph. Each vertex of this graph corresponds to one cycle, and each edge corresponds to one handle, which is a literal containing an atom that, occurring in both cycles, actually determines a connection between them. In fact, the truth value of the handle in the cycle where it appears as the head of a rule, influences the truth value of the atoms of the cycle(s) where it occurs in the body. We can therefore introduce the concept of a handle path, connecting different cycles. Cycles can be even, if they consist of an even number of rules, or vice versa they can be odd. Problems for consistency, as it is well-known, originate in the odd cycles. If for every odd cycle we can find a handle path with certain properties, then the existence of stable model is guaranteed. We will show that based on this results new classes of consistent programs can be defined, and that cycles and cycle graphs can be generalized to components and component graphs.