Abstract
The purpose of this paper is to establish sufficient conditions for the termination of Prolog procedures which can be checked automatically. We consider Horn clauses containing function symbols. The focus is on the question how local variables in the body of recursive procedures can be handled. The idea is to map predicates on linear inequalities which relate the sizes of the terms of solved goals. These inequalities are used to prove termination. A technique for the deduction of valid linear inequalities for predicates is described.
Research for this paper has been carried out within the EUREKA project EU 56 PROTOS.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Kowalski, R.: Logic Programming. Report, Department of Computing, Imperial College, London, 1982
van Emden, M.H., Kowalski, R., The Semantics of Predicate Logic as a programming Language, JACM 23,4,1976, 733–742
Apt, K.R., Emden, M.H., Contributions to the Theory of Logic Programming, J. ACM 29, 3(July 1982), 841–862
Vasak, Thomas, Potter, John, Characterization of Terminating Logic Programs, 1986 IEEE Symp. on Logic Programming, Vancouver
Hogger, C.J., Introduction to Logic Programming, London 1984
Vasak, T., Potter, J., Characterization of Terminating Logic Programs, 1986 Symposion on Logic Programming, Vancouver 1986
Smith, D.E., Genesereth, M.R., Ginsberg, M.L., Controlling Recursive Inference, Artificial Intelligence 30, 3,343–389
Naish, L. Automatic generation of control for logic programs, Tech. Rep. TR83/6. Dept. of Comp. Science, Univ. of Melbourne, Australia, 1983.
Aquilano, C., Barbuti, R., Bocchetti, P., Negation as Failure. Completeness of the Query Evaluation Process for Horn Clause Programs with Recursive Definitions, Journal of Automated Reasoning 2(1986), 155–170
Ricci, F., Zur Vermeidung divergenter Inferenz bei der Auswertung strukturell rekursiver Horn-Klausel-Programme, Diplomarbeit, Universität Dortmund, 1987
Ullman, J. D., van Gelder, A.,, Efficient tests for Top-Down Termination of Logical Rules, J. ACM 35, 2, April 1988, 345–373.
P. Dembinski, P., Maluszynski, J., And-Parallelism with intelligent Backtracking for annotated logic programs, Symposion on Logic Programming 1985, Boston 1985.
Mellish, C. Abstract Interpretation of Prolog programs, in: Abramsy, S., Hankin, C. (eds.), Abstract Interpretation of declarative languages, Chichester 1987
Debray, K.S., Warren, D.S., Automatic Mode Inference for Logic Programs, The Journal of Logic Programming, Vol. 5, No. 3, September 1988, 207–230
Mycroft, A., o'Keefe, R.A., A Polymorphic Type System for Prolog, Artificial Intelligence 23, 295–307
Nilsson, N.J. Problem solving methods in Artificial Intelligence, New York 1971
Plümer, L., Predicate Inequalities as a Basis for Automated Termination Proofs for Prolog Programs, Forschungsberichte der Abteilung Informatik der Universität Dortmund, 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Plümer, L. (1989). Predicate inequalities as a basis for automated termination proofs for Prolog programs. In: Börger, E., Büning, H.K., Richter, M.M. (eds) CSL '88. CSL 1988. Lecture Notes in Computer Science, vol 385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0026306
Download citation
DOI: https://doi.org/10.1007/BFb0026306
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51659-0
Online ISBN: 978-3-540-46736-6
eBook Packages: Springer Book Archive