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


Webmaster, Wed Sep 16 10:47:00 2009