The alternating fixpoint of logic programs with negation

Publisher Website
Google Scholar
Abstract
We introduce and describe the alternating fixpoint of a logic program with negation. The underlying idea is to monotonically build up a set of negative conclusions until the least fixpoint is reached, using a transformation related to the one that defines stable models, developed by Gelfand and Lifschitz. From a fixed set of negative conclusions, we can derive the positive conclusions that follow (without deriving any further negative ones), by traditional Horn clause semantics. The union of positive and negative conclusions is called the alternating fixpoint partial model. The name “alternating” was chosen because the transformation runs in two passes; the first pass transforms an underestimate of the set of negative conclusions into an (intermediate) overestimate; the second pass transforms the overestimates into a new underestimate; the composition of the two passes is monotonic.Our main theorem is that the alternating fixpoint partial model is exactly the well-founded partial model.We also show that a system is fixpoint logic, which permits rule bodies to be first order formulas but requires inductive relations to be positive within them, can be transformed straightforwardly into a normal logic program whose alternating fixpoint partial model corresponds to the least fixpoint of the fixpoint logic system. Thus alternating fixpoint logic is at least as expressive as fixpoint logic. The converse is shown to hold for finite structures.

This publication has 10 references indexed in Scilit: