An analysis of the equational properties of the well-founded fixed point

TL;DR

This paper investigates the logical properties of the well-founded fixed point operation, revealing which algebraic axioms it satisfies within the framework of iteration theories, with implications for logic programming semantics.

Contribution

It provides a detailed analysis of the equational properties of the well-founded fixed point, identifying which axioms of iteration theories it fulfills and which it does not.

Findings

Satisfies several iteration theory axioms

Does not satisfy all iteration theory axioms

Enhances understanding of semantics in logic programming

Abstract

Well-founded fixed points have been used in several areas of knowledge representation and reasoning and to give semantics to logic programs involving negation. They are an important ingredient of approximation fixed point theory. We study the logical properties of the (parametric) well-founded fixed point operation. We show that the operation satisfies several, but not all of the equational properties of fixed point operations described by the axioms of iteration theories.