Item

Abstract

Resolution K-transformations are faithful transformations between clause sets. The aim is to remove clauses like symmetry or transitivity from a clause set in order to eliminate or reduce recursivity and circularity in this clause set. It is shown that for any set of such clauses, a resolution K-transformation is likely to exist and can be found automatically. Clause K-transformations may be applied to reduce the search space of theorem provers, to eliminate loops in logic programs, to parallelise closure computation algorithms and to support automated complexity analysis.