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
some new results for a special type of cycles called
matching cycles, ie. cycles
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.