occur quite frequently in logic programs, deductive databases, and - disguised as an equation - in term rewriting systems. These clauses define a cycle if the atoms and unifies with a new variant of . The obvious problem with cycles is to control the number of iterations through the cycle. In this paper we consider the cycle unification problem of unifying two literals modulo a cycle. We review the state of the art of cycle unification and give new results for a special type of cycles called unifying cycles, i.e., cycles L R for which there exists a substitution such that L = R. Altogether, these results show how the deductive process can be efficiently controlled for special classes of cycles without losing completeness.
Download PDF Show BibTeX
Login to edit