A METHODOLOGY FOR PROVING TERMINATION OF LOGIC PROGRAMS

被引:7
|
作者
WANG, B [1 ]
SHYAMASUNDAR, RK [1 ]
机构
[1] PENN STATE UNIV, DEPT COMP SCI, UNIVERSITY PK, PA 16802 USA
来源
JOURNAL OF LOGIC PROGRAMMING | 1994年 / 21卷 / 01期
关键词
D O I
10.1016/0743-1066(94)90004-3
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
In this paper, we describe a methodology for proving termination of logic programs. First, we introduce U-graphs as an abstraction of logic programs and establish that SLDNF derivations can be realized by instances of paths in the U-graphs. Such a relation enables us to use U-graphs for establishing the universal termination of logic programs. In our method, we associate pre- and postassertions to the nodes of the graph and order assertions to selected edges of the graph. With this as the basis, we develop a simple method for establishing the termination of logic programs. The simplicity/practicality of the method is illustrated through examples.
引用
收藏
页码:1 / 30
页数:30
相关论文
共 50 条
  • [1] METHODOLOGY FOR PROVING THE TERMINATION OF LOGIC PROGRAMS
    WANG, B
    SHYAMASUNDAR, RK
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 480 : 214 - 227
  • [2] Transformational methodology for proving termination of logic programs
    Rao, MRKK
    Kapur, D
    Shyamasundar, RK
    [J]. JOURNAL OF LOGIC PROGRAMMING, 1998, 34 (01): : 1 - 41
  • [3] A TRANSFORMATIONAL METHODOLOGY FOR PROVING TERMINATION OF LOGIC PROGRAMS
    RAO, MRKK
    KAPUR, D
    SHYAMASUNDAR, RK
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 626 : 213 - 226
  • [4] On proving left termination of constraint logic programs
    Iremia, Univ. de La Réunion
    不详
    不详
    [J]. ACM Transactions on Computational Logic, 2003, 4 (02) : 207 - 259
  • [5] Practical methods for proving termination of general logic programs
    Marchiori, E
    [J]. JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, 1996, 4 : 179 - 208
  • [6] Proving termination of input-consuming logic programs
    Smaus, JG
    [J]. LOGIC PROGRAMMING: PROCEEDINGS OF THE 1999 INTERNATIONAL CONFERENCE ON LOGIC PROGRAMMING, 1999, : 335 - 349
  • [7] PROVING TERMINATION OF LOGIC PROGRAMS BY EXPLOITING TERM PROPERTIES
    BOSSI, A
    COCCO, N
    FABRIS, M
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 494 : 153 - 180
  • [8] Proving termination for logic programs by the query-mapping pairs approach
    Lindenstrauss, N
    Sagiv, Y
    Serebrenik, A
    [J]. PROGRAM DEVELOPMENT IN COMPUTATIONAL LOGIC: A DECADE OF RESEARCH ADVANCES IN LOGIC-BASED PROGRAM DEVELOPMENT, 2004, 3049 : 453 - 498
  • [9] PROVING TERMINATION OF COMMUNICATING PROGRAMS
    PACZKOWSKI, P
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1990, 458 : 416 - 426
  • [10] Proving termination of GHC programs
    Krishna Rao M.R.K.
    Kapur D.
    Shyamasundar R.K.
    [J]. New Generation Computing, 1997, 15 (3) : 293 - 338