Abstract
Two-literal clauses of the form L ← 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←R for which there exists a substitution σ such that σL=R or L=σR. Altogether, these results show how the deductive process can be efficiently controlled for special classes of cycles without losing completeness.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
W. Bibel. Automated Theorem Proving. Vieweg Verlag, Braunschweig, 2 edition, 1987.
W. Bibel. Advanced topics in automated deduction. In R. Nossum, editor, Fundamentals of Artificial Intelligence II, pages 41–59. Springer, LNCS 345, 1988.
W. Bibel. Perspectives on automated deduction. In R. S. Boyer, editor, Automated Reasoning: Essays in Honor of Woody Bledsoe, pages 77–104. Kluwer Academic, Utrecht, 1991.
W. Bibel, S. Hölldobler, and J. Würtz. Cycle unification. Technical Report AIDA-91-15, FG Intellektik, FB Informatik, TH Darmstadt, 1991.
M. Dauchet. Simulation of a Turing machine by a left-linear rewrite rule. In Proceedings of the Conference on Rewriting Techniques and Applications, pages 109–120. Springer, LNCS 355, 1989.
N. Dershowitz and J.-P. Jouannaud. Notations for rewriting. EATCS Bulletin, 43:162–172, 1991.
P. Devienne. Weighted graphs: A tool for studying the halting problem and time complexity in term rewriting systems and logic programming. Journal of Theoretical Computer Science, 75:157–215, 1990.
E. Eder. Properties of substitutions and unifications. Journal of Symbolic Computation, 1:31–46, 1985.
J. W. Lloyd. Foundations of Logic Programming. Springer, 1984.
J. Minker and J.-M. Nicolas. On recursive axioms in deductive databases. Information Systems, 8(1):1–13, 1983.
H. J. Ohlbach. Abstraction tree indexing for terms. In L. C. Aiello, editor, Proceedings of the European Conference on Artificial Intelligence, pages 479–484, 1990.
H. J. Ohlbach. Compilation of recursive two-literal clauses into unification algorithms. In P. Jorrand and V. Sgurev, editors, Proceedings of the AIMSA, pages 13–22, 1990.
H. J. Ohlbach and G. Wrightson. Solving a problem in relevance logic with an automated theorem prover. In R. E. Shostak, editor, Proceedings of the Conference on Automated Deduction, pages 496–508. Springer, LNCS 170, 1984.
F. Pfenning. Single axioms in the implicational propositional calculus. In E. Lusk and R. Overbeek, editors, Proceedings of the Conference on Automated Deduction, pages 710–713. Springer, LNCS 310, 1988.
J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12:23–41, 1965.
M. Schmidt-Schauß. Implication of clauses is undecidable. Journal of Theoretical Computer Science, 59:287–296, 1988.
D. De Schreye, K. Verschaetse, and M. Bruynooghe. A practical technique for detecting non-terminating queries for a restricted class of Horn clauses, using directed, weighted graphs. In Proceedings of the International Conference on Logic Programming, pages 649–663, 1990.
J. H. Siekmann. Unification theory. Journal of Symbolic Computation, 7:207–274, 1989.
M. E. Stickel. Automated deduction by theory resolution. Journal of Automated Reasonsing, 1:333–356, 1985.
L. Vielle. Recursive query processing: The power of logic. Technical Report TR-KB-17, European Computer-Industry Research Center, 1987.
L. Wos. The problem of finding a strategy to control binary paramodulation. Journal of Automated Reasonsing, pages 101–107, 1988.
J. Würtz. Unifying cycles. Technical report, Deutsches Forschungszentrum für Künstliche Intelligenz, 1992. To appear.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bibel, W., Hölldobler, S., Würtz, J. (1992). Cycle unification. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_158
Download citation
DOI: https://doi.org/10.1007/3-540-55602-8_158
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55602-2
Online ISBN: 978-3-540-47252-0
eBook Packages: Springer Book Archive