# Intellektik: Technical report 91-15

## Cycle Unification

### W. Bibel and S. Hölldobler and J. Würtz

Two-literal clauses of the form $L\!\leftarrow\!R\/$ 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 $L\/$ and
$R\/$ are weakly unifiable, ie.\ if $L\/$ unifies with a new variant of $R\/$.
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 $\,G\,$ and $\,F\,$
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 $\,L\!\leftarrow\!R\,$ for which there exists a
substitution $\,\sigma\,$ such that $\,\sigma L = R\,$ or $\,L = \sigma R\,$.
Altogether, these results show how the deductive process can be
efficiently controlled for special classes of cycles without losing
completeness.