Publication details

Saarland University Computer Science

Cycle Unification

Wolfgang Bibel, Steffen Hölldobler, Jörg Würtz

11th International Conference on Automated Deduction, pp. 94--108, Springer-Verlag, 1992

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 = sigmaR. 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


Legal notice, Privacy policy