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 条

[21] Persistence of Termination for Non-Overlapping Term Rewriting Systems
Iwami, Munehiro
PROCEEDINGS OF WORLD ACADEMY OF SCIENCE, ENGINEERING AND TECHNOLOGY, VOL 3, 2005, 3 : 138 - 141
[22] Persistence of termination for locally confluent overlay term rewriting systems
Iwami, M
Proceedings of the IASTED International Conference on Artificial Intelligence and Applications, Vols 1and 2, 2004, : 529 - 534
[23] COUNTEREXAMPLES TO TERMINATION FOR THE DIRECT SUM OF TERM REWRITING-SYSTEMS
TOYAMA, Y
INFORMATION PROCESSING LETTERS, 1987, 25 (03) : 141 - 143
[24] 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
[25] 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
[26] Omega-Termination is Undecidable for Totally Terminating Term Rewriting Systems
Journal of Symbolic Computation, 23 (04):
[27] Persistence of Termination for Right-Linear Overlay Term Rewriting Systems
Iwami, Munehiro
PROCEEDINGS OF WORLD ACADEMY OF SCIENCE, ENGINEERING AND TECHNOLOGY, VOL 3, 2005, 3 : 94 - 97
[28] Omega-termination is undecidable for totally terminating term rewriting systems
Geser, A
JOURNAL OF SYMBOLIC COMPUTATION, 1997, 23 (04) : 399 - 411
[29] A SUFFICIENT CONDITION FOR THE TERMINATION OF THE DIRECT SUM OF TERM REWRITING-SYSTEMS
MIDDELDORP, A
FOURTH ANNUAL SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, 1989, : 396 - 401
[30] Termination and confluence in infinitary term rewriting
Rodenburg, PH
JOURNAL OF SYMBOLIC LOGIC, 1998, 63 (04) : 1286 - 1296

← 1 2 3 4 5 →