A dynamic approach to characterizing termination of general logic programs

ACM Transactions on Computational Logic - Tập 4 Số 4 - Trang 417-430 - 2003
Yi-Dong Shen1, Jia-Huai You2, Li-Yan Yuan2, Samuel S. P. Shen2, Qiang Yang3
1Chinese Academy of Sciences, Beijing, China
2University of Alberta, Edmonton, Canada
3Simon Fraser University, Burnaby, BC, Canada

Tóm tắt

We present a new characterization of termination of general logic programs. Most existing termination analysis approaches rely on some static information about the structure of the source code of a logic program, such as modes/types, norms/level mappings, models/interargument relations, and the like. We propose a dynamic approach that employs some key dynamic features of an infinite (generalized) SLDNF-derivation, such as repetition of selected subgoals and recursive increase in term size. We also introduce a new formulation of SLDNF-trees, called generalized SLDNF-trees. Generalized SLDNF-trees deal with negative subgoals in the same way as Prolog and exist for any general logic programs.

Từ khóa


Tài liệu tham khảo

Apt K. R., 1994, A new definition of sldnf-resolution, J. Logic Program., 18, 177, 10.1016/0743-1066(94)90051-5

10.1006/inco.1993.1051

10.1016/0743-1066(93)90014-8

Bol R. N. 1991. Loop checking in logic programming. Ph.D. thesis The University of Amsterdam Amsterdam. Bol R. N. 1991. Loop checking in logic programming. Ph.D. thesis The University of Amsterdam Amsterdam.

10.1016/0304-3975(91)90004-L

10.1016/0304-3975(92)00019-N

Brodsky A., Proceedings of the Tenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems. ACM Press, Denver, 227--240

Chan D., 1988, Proceedings of the Fifth International Conference and Symposium on Logic Programming. MIT Press

10.1145/227595.227597

Clark K. L. 1978. Negation as failure. In Logic and Databases H. Gallaire and J. Minker Eds. Plenum New York 293--322. Clark K. L. 1978. Negation as failure. In Logic and Databases H. Gallaire and J. Minker Eds. Plenum New York 293--322.

Decorte S., Proceedings of the 1993 International Symposium on Logic Programming. MIT Press

10.1145/330643.330645

10.1016/S0747-7171(87)80022-6

Higman G., 1952, Ordering by divisibility in abstract algebras, Proceedings of the London Mathematical Society, 3, 326, 10.1112/plms/s3-2.1.326

ISLAB. 1998. SICStus Prolog User's Manual. Intelligent Systems Laboratory Swedish Institute of Computer Science Available from http://www.sics.se/sicstus/docs/3.7.1/html/sicstus_toc.html. ISLAB. 1998. SICStus Prolog User's Manual. Intelligent Systems Laboratory Swedish Institute of Computer Science Available from http://www.sics.se/sicstus/docs/3.7.1/html/sicstus_toc.html.

10.1016/0743-1066(89)90022-8

Lindenstrauss N., Proceedings of the Fourteenth International Conference on Logic Programming. MIT Press

Lloyd J. W. 1987. Foundations of Logic Programming. Springer-Verlag Berlin. Lloyd J. W. 1987. Foundations of Logic Programming. Springer-Verlag Berlin.

10.1016/0020-0190(92)90012-K

Martin J. C., Proceedings of the 6th International Workshop on Logic Programming Synthesis and Transformation. Springer

Plumer L. 1990a. Termination Proofs for Logic Programs. Lecture Notes in Computer Science 446 Springer-Verlag Berlin. Plumer L. 1990a. Termination Proofs for Logic Programs. Lecture Notes in Computer Science 446 Springer-Verlag Berlin.

Plumer L., 1990, Proceedings of the Seventh International Conference on Logic Programming. MIT Press

Schreye D. D., 1993, Termination of logic programs: the never-ending story, J. Logic Program., 19, 199

Schreye D. D., 1995, Deriving linear size relations for logic programs by abstract interpretation, New Generation Computing, 13, 117, 10.1007/BF03038311

Schreye D. D., Proceedings of the International Conference on Fifth Generation Computer Systems. IOS Press

Shen Y. D. Yuan L. Y. and You J. H. 2001. Loop checks for logic programs with functions. Theoretical Computer Science 266 1/2 441--461. 10.1016/S0304-3975(00)00197-3 Shen Y. D. Yuan L. Y. and You J. H. 2001. Loop checks for logic programs with functions. Theoretical Computer Science 266 1/2 441--461. 10.1016/S0304-3975(00)00197-3

10.1023/A:1020116927466

10.1145/42282.42285

10.1145/371282.371357

Verschaetse K. 1992. Static termination analysis for definite horn clause programs. Ph.D. thesis Department of Computer Science K. U. Leuven Available at http://www.cs.kuleuven. ac.be/lpai. Verschaetse K. 1992. Static termination analysis for definite horn clause programs. Ph.D. thesis Department of Computer Science K. U. Leuven Available at http://www.cs.kuleuven. ac.be/lpai.

Thông tin
Thông tin xuất bản

ACM Transactions on Computational Logic

Tập 4 Số 4

417-430

Thông tin tác giả