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 条
  • [41] Proving Termination of Integer Term Rewriting
    Fuhs, Carsten
    Giesl, Juergen
    Pluecker, Martin
    Schneider-Kamp, Peter
    Falke, Stephan
    REWRITING TECHNIQUES AND APPLICATIONS, 2009, 5595 : 32 - +
  • [42] Tuple Interpretations for Termination of Term Rewriting
    Yamada, Akihisa
    Journal of Automated Reasoning, 2022, 66 (04): : 667 - 688
  • [43] Termination of fair computations in term rewriting
    Lucas, S
    Meseguer, J
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3835 : 184 - 198
  • [44] From Linear Term Rewriting to Graph Rewriting with Preservation of Termination
    Overbeek, Roy
    Endrullis, Jorg
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (350): : 19 - 34
  • [45] Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems
    Uchiyama, Keita
    Sakai, Masahiko
    Sakabe, Toshiki
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 204 (0C) : 21 - 34
  • [46] Termination for direct sums of left-linear complete term rewriting systems
    Toyama, Y
    Klop, JW
    Barendregt, HP
    JOURNAL OF THE ACM, 1995, 42 (06) : 1275 - 1304
  • [47] Termination for direct sums of left-linear complete term rewriting systems
    Toyama, Y.
    Klop, J.W.
    Barendregt, H.P.
    1600, (42):
  • [48] Detecting non-termination of term rewriting systems using an unfolding operator
    Payet, Etienne
    LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2007, 4407 : 194 - 209
  • [49] RELATING INNERMOST, WEAK, UNIFORM AND MODULAR TERMINATION OF TERM REWRITING-SYSTEMS
    GRAMLICH, B
    LECTURE NOTES IN ARTIFICIAL INTELLIGENCE, 1992, 624 : 285 - 296
  • [50] TERMINATION IS NOT MODULAR FOR CONFLUENT VARIABLE-PRESERVING TERM REWRITING-SYSTEMS
    OHLEBUSCH, E
    INFORMATION PROCESSING LETTERS, 1995, 53 (04) : 223 - 228
12345