Abstract
In this paper, it is shown that a translation from logic programs to conditional rewrite rules can be used in a straightforward way to check (semi-automatically) whether a program is terminating under the prolog selection rule.
This research was funded by the German Ministry for Research and Technology (BMFT) under grant ITS 9103 and by the DFG project “Redundanz” (Az. Ga 261, SPP Deduktion). The responsibility for the contents of this publication lies with the authors.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Krzysztof R. Apt and Dino Pedreschi. Studies in pure Prolog: Termination. Technical Report CS-R9048, Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands, September 1990.
George E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In H. Brakhage, editor, Automata Theory and Formal Languages, 2nd GI Conference, LNCS 33, pages 134–183, Kaiserslautern, West Germany, May 20–23, 1975. Springer-Verlag.
Hubert Comon. Solving inequations in term algebras (extended abstract). In Fifth Annual IEEE Symposium on Logic in Computer Science, pages 62–69, Philadelphia, PA, USA, June 4–7, 1990. IEEE Computer Society Press, Los Alamitos, CA, USA.
Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 6, pages 244–320. Elsevier Science Publishers B.V., Amsterdam, New York, Oxford, Tokyo, 1990.
Harald Ganzinger. Order-sorted completion: the many-sorted way. Theoretical Computer Science, 89:3–32, 1991.
Feliks Kluźniak. Type synthesis for Ground Prolog. In Jean-Louis Lassez, editor, Logic Programming, Proceedings of the Fourth International Conference, volume 2, pages 788–816, Melbourne, Australia, May 25–29, 1987. The MIT Press.
M. R. K. Krishna Rao, Deepak Kapur, and R. K. Shyamasundar. A transformational methodology for proving termination of logic programs. Draft, Computer Science Group, Tata Institute of Fundamental Research, Bombay, India, February 28, 1992. To appear in: Proceedings of the 5th Conference on Computer Science Logic 1991, LNCS, Springer-Verlag.
John Wylie Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, Heidelberg, New York, London, Paris, Tokyo, second, extended edition, 1987.
Lutz Plümer. Termination Proofs for Logic Programs. Dissertation, Universität Dortmund, Abteilung Informatik, Dortmund, Germany, 1989. Short version: Termination Proofs for Logic Programs based on Predicate Inequalities, in David H. D. Warren and Peter Szeredi, eds., Logic Programming, Proceedings of the Seventh International Conference, Jerusalem, Israel, June 18–20, 1990, pages 634–648, The MIT Press.
Alfred Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley, second, revised edition, 1951.
Jeffrey D. Ullman and Allen Van Gelder. Efficient tests for top-down termination of logical rules. Journal of the ACM, 35(2):345–373, April 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ganzinger, H., Waldmann, U. (1993). Termination proofs of well-moded logic programs via conditional rewrite systems. In: Rusinowitch, M., Rémy, JL. (eds) Conditional Term Rewriting Systems. CTRS 1992. Lecture Notes in Computer Science, vol 656. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56393-8_34
Download citation
DOI: https://doi.org/10.1007/3-540-56393-8_34
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56393-8
Online ISBN: 978-3-540-47549-1
eBook Packages: Springer Book Archive