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.