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.