Mechanizing weak termination proving of term rewriting systems by induction

被引：0
|
作者：
Feng, S [1 ]
Cao, S [1 ]
Liu, SX [1 ]
机构：
[1] Beijing Normal Univ, Dept Comp Sci, Beijing 100875, Peoples R China
来源：
COMPUTER SCIENCE AND TECHNOLOGY IN NEW CENTURY | 2001年
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
The paper proposes an automated formal proving method for weakly terminating property in a restricted domain of a term rewriting system. The method is based on structural induction and a meta-computation model for term rewriting systems - dynamic term rewriting calculus. It can be applied to non-terminating, non-confluent and/or non-left-linear term rewriting systems. The extension of the method for proving weak termination by cover-set induction can be easily achieved.
引用
收藏
页码：15 / 19
页数：3
相关论文
共 50 条
  • [1] Mechanizing Weakly Ground Termination Proving of Term Rewriting Systems by Structural and Cover-Set Inductions
    Su Feng
    Journal of Computer Science and Technology, 2005, 20 : 496 - 513
  • [2] Mechanizing weakly ground termination proving of term rewriting systems by structural and cover-set inductions
    Feng, S
    JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2005, 20 (04) : 496 - 513
  • [3] PROVING TERMINATION FOR TERM REWRITING-SYSTEMS
    WEIERMANN, A
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 626 : 419 - 428
  • [4] Proving termination of ω rewriting systems
    Shigeta, Y
    Akama, K
    Koike, H
    Ishikawa, T
    INTERNATIONAL CONFERENCE ON COMPUTING AND INFORMATION TECHNOLOGIES : EXPLORING EMERGING TECHNOLOGIES, 2001, : 399 - 404
  • [5] Proving Termination of Integer Term Rewriting
    Fuhs, Carsten
    Giesl, Juergen
    Pluecker, Martin
    Schneider-Kamp, Peter
    Falke, Stephan
    REWRITING TECHNIQUES AND APPLICATIONS, 2009, 5595 : 32 - +
  • [6] A PATH ORDERING FOR PROVING TERMINATION OF TERM REWRITING-SYSTEMS
    KAPUR, D
    NARENDRAN, P
    SIVAKUMAR, G
    LECTURE NOTES IN COMPUTER SCIENCE, 1985, 185 : 173 - 187
  • [7] Modular Termination for Weak Overlapping Term Rewriting Systems
    Graziani, M.
    Venturini Zilli, M.
    Bulletin of the European Association for Theoretical Computer Science, 1994, (53):
  • [8] Characterizing and proving operational termination of deterministic conditional term rewriting systems
    Schernhammer, Felix
    Gramlich, Bernhard
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2010, 79 (07): : 659 - 688
  • [9] Matrix interpretations for proving termination of term rewriting
    Endrullis, Joerg
    Waldmann, Johannes
    Zantema, Hans
    JOURNAL OF AUTOMATED REASONING, 2008, 40 (2-3) : 195 - 220
  • [10] Dependency pairs for proving termination properties of conditional term rewriting systems
    Lucas, Salvador
    Meseguer, Jose
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2017, 86 (01) : 236 - 268
12345