The Alternating Fixpoint of Logic Programs with NegationAbstract: "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. From a fixed set of negative conclusions, we can derive the positive conclusions that follow (without deriving further any negative ones), by traditional Horn clause semantics. The union of positive and negative conclusins 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 overestimate into a new underestimate; the composition of the two passes is monotonic. |
Common terms and phrases
AFP model alternating fixpoint logic alternating fixpoint partial atoms auxiliary relation conjunction of literals database defined Definition elementary simplification existential subformula expressive power false finite structures fixpoint logic IFP fixpoint partial model globally negative relations globally positive graph ground terms Herbrand base Herbrand universe Horn clause IDB relations inductive fixpoint logic inductive hypothesis infinite infinite descending chain instantiated rule least fixpoint Lemma limit ordinal literal is true logical consequence semantics Moschovakis negation as failure negative IDB literal negative literals negative subgoals normal logic program order formulas order rule bodies partial interpretation positive literals Proof recursive replaced subformula rule for q(t Schlipf set of literals set of negative set of positive Sp(Ã Sp(I Sp(J+ Sp(Ŵ stability transformation stable models stratified programs stratified semantics strict successor ordinal total model Tp(I transitive closure tuple unfounded set well-founded partial model well-founded semantics