Affiliations: Department of Computer Science, K.U. Leuven,
Celestijnlaan 200A, B-3001 Leuven, Belgium. E-mail: {joost.vennekens,johan,maartenm,marcd}@cs.kuleuven.be
Abstract: We study the transformation of "predicate
introduction" in non-monotonic logics. By this, we mean the act
of replacing a complex formula by a newly defined predicate. From a knowledge
representation perspective, such transformations can be used to eliminate
redundancy or to simplify a theory. From a more practical point of view, they
can also be used to transform a theory into a normal form imposed by certain
inference programs or theorems. In this paper, we study predicate introduction
in the algebraic framework of "approximation theory";
this is a fixpoint theory for nonmonotone operators that generalizes all main
semantics of various non-monotonic logics, including logic programming, default
logic and autoepistemic logic. We prove an abstract, algebraic equivalence
result in this framework. This can then be used to show that, in logic
programming, certain transformations are equivalence preserving under, among
others, both the stable and well-founded semantics. Based on this result, we
develop a general method of eliminating universal quantifiers in the bodies of
rules. Our work is, however, also applicable beyond logic programming. In a
companion paper, we demonstrate this, by using the same algebraic results to
derive a transformation which reduces the nesting depth of the modal operator K
in autoepistemic logic.
