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 条

[21] On proving Cε-termination of rewriting by size-change termination
Fernández, ML
INFORMATION PROCESSING LETTERS, 2005, 93 (04) : 155 - 162
[22] MU-TERM: A tool for proving termination of context-sensitive rewriting
Lucas, S
REWRITING TECHNIQUES AND APPLICATIONS, PROCEEDINGS, 2004, 3091 : 200 - 209
[23] Parallelization of Termination Checker of Term Rewriting Systems
Ding, Rui
Sato, Haruhiko
Kurihara, Masahito
INTERNATIONAL MULTICONFERENCE OF ENGINEERS AND COMPUTER SCIENTISTS, IMECS 2012, VOL I, 2012, : 757 - 762
[24] Decomposable termination of composable term rewriting systems
Kurihara, Masahito, 1600, Inst of Electronics, Inf & Commun Engineers of Japan, Tokyo, Japan (E78-D):
[25] ON THE MODULARITY OF TERMINATION OF TERM REWRITING-SYSTEMS
OHLEBUSCH, E
THEORETICAL COMPUTER SCIENCE, 1994, 136 (02) : 333 - 360
[26] Operational termination of conditional term rewriting systems
Lucas, S
Marché, C
Meseguer, J
INFORMATION PROCESSING LETTERS, 2005, 95 (04) : 446 - 453
[27] MODULAR TERM REWRITING-SYSTEMS AND THE TERMINATION
KURIHARA, M
KAJI, I
INFORMATION PROCESSING LETTERS, 1990, 34 (01) : 1 - 4
[28] TERMINATION OF LINEAR BOUNDED TERM REWRITING SYSTEMS
Durand, Irene
Senizergues, Geraud
Sylvestre, Marc
PROCEEDINGS OF THE 21ST INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'10), 2010, 6 : 341 - 356
[29] Using Context-Sensitive Rewriting for Proving Innermost Termination of Rewriting
Alarcon, Beatriz
Lucas, Salvador
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 248 : 3 - 17
[30] PROVING INDUCTIVE THEOREMS BASED ON TERM REWRITING-SYSTEMS
HOFBAUER, D
KUTSCHE, RD
LECTURE NOTES IN COMPUTER SCIENCE, 1988, 343 : 180 - 190

← 1 2 3 4 5 →