Parallelization of Termination Checker of Term Rewriting Systems

被引：0

作者：

Ding, Rui ^{[1
]}

Sato, Haruhiko ^{[1
]}

Kurihara, Masahito ^{[1
]}

机构：

[1] Hokkaido Univ, Grad Sch Informat Sci & Technol, Sapporo, Hokkaido 0600814, Japan

来源：

INTERNATIONAL MULTICONFERENCE OF ENGINEERS AND COMPUTER SCIENTISTS, IMECS 2012, VOL I | 2012年

关键词：

Parallelization; Term rewriting system; Ter-mination checker; Multi-context rewriting induction; Lexico-graphic path order; Erlang;

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Inductive theorem proving plays an important role in the field of formal verification of systems. The rewriting induction(RI) is a method for inductive theorem proving proposed by Reddy. And the multi-context rewriting induction(MRI) proposed by Sato based on the idea of Kurihara has improved the power of RI significantly. However a large amount of termination check of term rewriting systems should be performed in the MRIt, which is becoming the efficiency bottleneck of MRI. In this paper, we propose a method of parallelizing the termination checker used in MRI based on the lexicographic path order method to improve its efficiency. And then we will discuss its efficiency based on the experiments with the system implemented in a parallel functional programming language named Erlang.

引用

页码：757 / 762

页数：6

共 50 条

[1] Parallelization of Termination Checker for Term Rewriting System
Ding, Rui
Sato, Haruhiko
Kurihara, Masahito
PROCEEDINGS 2012 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS (SMC), 2012, : 1824 - 1829
[2] Decomposable termination of composable term rewriting systems
Kurihara, Masahito, 1600, Inst of Electronics, Inf & Commun Engineers of Japan, Tokyo, Japan (E78-D):
[3] ON THE MODULARITY OF TERMINATION OF TERM REWRITING-SYSTEMS
OHLEBUSCH, E
THEORETICAL COMPUTER SCIENCE, 1994, 136 (02) : 333 - 360
[4] Operational termination of conditional term rewriting systems
Lucas, S
Marché, C
Meseguer, J
INFORMATION PROCESSING LETTERS, 2005, 95 (04) : 446 - 453
[5] PROVING TERMINATION FOR TERM REWRITING-SYSTEMS
WEIERMANN, A
LECTURE NOTES IN COMPUTER SCIENCE, 1992, 626 : 419 - 428
[6] MODULAR TERM REWRITING-SYSTEMS AND THE TERMINATION
KURIHARA, M
KAJI, I
INFORMATION PROCESSING LETTERS, 1990, 34 (01) : 1 - 4
[7] 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
[8] A LOCAL TERMINATION PROPERTY FOR TERM REWRITING-SYSTEMS
LATCH, DM
SIGAL, R
LECTURE NOTES IN COMPUTER SCIENCE, 1989, 355 : 222 - 233
[9] Modular Termination for Weak Overlapping Term Rewriting Systems
Graziani, M.
Venturini Zilli, M.
Bulletin of the European Association for Theoretical Computer Science, 1994, (53):
[10] Persistence of Termination for Term Rewriting Systems with Ordered Sorts
Iwami, Munehiro
PROCEEDINGS OF WORLD ACADEMY OF SCIENCE, ENGINEERING AND TECHNOLOGY, VOL 3, 2005, 3 : 81 - 85

← 1 2 3 4 5 →