We present a fixed point theorem for a class of (potentially) non-monotonic functions over specially structured complete lattices. The theorem has as a special case the Knaster-Tarski fixed point theorem when restricted to the case of monotonic functions and Kleene's theorem when the functions are additionally continuous. From the practical side, the theorem has direct applications in the semantics of negation in logic programming. In particular, it leads to a more direct and elegant proof of the least fixed point result of [Rondogiannis and W.W.Wadge, ACM TOCL 6(2): 441-467 (2005)]. Moreover, the theorem appears to have potential for possible applications outside the logic programming domain.
@cite_10: It is well known that, under certain conditions, it is possible to split logic programs under stable model semantics, that is, to divide such a program into a number of different “levels”, such that the models of the entire program can be constructed by incrementally constructing models for each level. Similar results exist for other nonmonotonic formalisms, such as auto-epistemic logic and default logic. In this work, we present a general, algebraic splitting theory for logics with a fixpoint semantics. Together with the framework of approximation theory, a general fixpoint theory for arbitrary operators, this gives us a uniform and powerful way of deriving splitting results for each logic with a fixpoint semantics. We demonstrate the usefulness of these results, by generalizing existing results for logic programming, auto-epistemic logic and default logic.
A more recent work that is also connected to our approach is reported in @cite_10 . In that paper the authors consider the case of product lattices as-well-as stratifiable operators on such lattices. In our terminology, an operator @math is stratifiable iff for all @math and for all @math , if @math then @math . The authors demonstrate @cite_10 [Theorem 3.5] that for every stratifiable operator @math it holds that every fixed point of @math can be constructed using the fixed points of a family of operators called the components of @math (intuitively, to every sublattice @math of the product lattice @math there corresponds a subfamily of the components). However, the least fixed point of @cite_10 [Theorem 3.5] is with respect to the pointwise partial order that is defined on the product lattice @math while in our case @math is not necessarily pointwise. Moreover, our construction does not only apply to product lattices but to all lattices that satisfy the axioms of Subsection . For example, the non-standard product model of Subsection does not fall within the scope of the results developed in @cite_10 .