Abstract
The question of the termination of logic programming computations is studied from a semantical point of view. To every program are associated two first order formulas. Their valid consequences are respectively the finiteness and the infiniteness SLDNF sets of the logic programs considered. The non-existence of a recursive safe computation rule leading into an infinite SLDNF computation is proved.
58 avenue de la république, 93110 Rosny-sous-bois, France
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
K. R. Apt, G. Bezem: Acyclic programs. In: P. Szeredi, D. H. D. Warren (eds.): Proceedings of the Seventh International Conference on Logic Programming. Massachussets Institute of Technology Press 1990, pp. 617–633
K. R. Apt, H. A. Blair, A. Walker: Towards a theory of declarative knowledge. In: J. Minker (ed.): Foundations of Deductive Databases and Logic Programming. Los Altos: Morgan Kaufmann 1988, pp. 89–148
K. R. Apt, R. N. Bol, J. W. Klop: On the power of subsumption and context checks. In: A. Miola (ed.): Design and Implementation of Symbolic Computation Systems. Lecture Notes in Computer Science 429. Berlin: Springer 1990, pp. 131–140
P. Balbiani: A modal semantics for the negation as failure and the closed world assumption rules. In: C. Choffrut, M. Jantzen (eds.): Eighth Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science 480. Berlin: Springer 1990, pp. 523–534
P. Balbiani: A modal semantics of negation in logic programming. Fundamente Informaticæ (to appear)
P. Balbiani: Sur la finitude des dérivations de la programmation en logique. rapport IRIT/92-3-R
M. Bezem: Characterizing termination of logic programs with level mapping. In: E. L. Lusk, R. Overbeek (eds.): Proceedings of the North American Conference on Logic Programming. Massachussets Institute of Technology Press 1989, pp. 69–80
G. Boolos: The unprovability of inconsistency. Cambridge: Cambridge University Press 1979
G. Boolos, G. Sambin: Provability: the emergence of a mathematical modality. Studia Logica, 1–23 (1991)
K. L. Clark: Negation as failure. In: H. Gallaire et J. Minker (eds.): Logic and Data Bases. New York: Plenum Press 1978, pp. 293–322
F. Denis: Contribution à l'étude des sémantiques axiomatiques de Prolog. thèse de l'université des sciences et techniques de Lille Flandres Artois, 1990
J.-L. Lassez, M. J. Maher: Closures and fairness in the semantics of programming logic. Theoretical Computer Science 29, 167–184 (1984)
J.-L. Lassez, M. J. Maher, D. A. Wolfram: A unified treatment of resolution strategies for logic programs. In: S.-A. Tarnlund (ed.): Second International Conference on Logic Programming. Uppsala: Uppsala University Press 1984, pp. 263–276
J. W. Lloyd: Foundations of logic programming. Berlin: Springer 1987
P. Odifreddi: Classical recursion theory. Amsterdam: North-Holland 1989
L.Plümer: Termination proofs for logic programs. Lecture Notes in Artificial Intelligence 446. Berlin: Springer 1990
J. C. Shepherdson: Unsolvable problems for SLDNF resolution. Journal of Logic Programming 10, 19–22 (1991)
J. D. Ullman, A. van Gelder: Efficient tests for top-down termination of logical rules. Journal of the Association for Computing Machinery 35, 345–373 (1988)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Balbiani, P. (1992). The finiteness of logic programming derivations. In: Kirchner, H., Levi, G. (eds) Algebraic and Logic Programming. ALP 1992. Lecture Notes in Computer Science, vol 632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013840
Download citation
DOI: https://doi.org/10.1007/BFb0013840
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55873-6
Online ISBN: 978-3-540-47302-2
eBook Packages: Springer Book Archive