Automated Inductive Theorem Proving using Transformations of Term Rewriting Systems

• SATO Koichi

  Research Institute of Electrical Communication, Tohoku University

• KIKUCHI Kentaro

  Research Institute of Electrical Communication, Tohoku University

• AOTO Takahito

  Research Institute of Electrical Communication, Tohoku University

• TOYAMA Yoshihito

  Research Institute of Electrical Communication, Tohoku University

Bibliographic Information

Other Title

• 項書き換えシステムの変換を利用した帰納的定理自動証明

Abstract

Rewriting induction (Reddy, 1989) is proposed as an automated theorem proving method on term rewriting systems. In general, rewriting induction does not work well for the term rewriting systems with tail recursion. On the other hand, context moving and splitting (Giesl, 2000) are proposed as program transformation techniques intended to facilitate automated verification for functional programs. These techniques transform tail recursive programs into simple recursive programs suitable for automated verification. In this paper, we prove that the correctness of these techniques for term rewriting systems, and show that the combination of rewriting induction and these techniques are useful in proving inductive theorems on term rewriting systems with tail recursion.

Journal

• Computer Software

  Computer Software 32 (1), 1_179-1_193, 2015

  Japan Society for Software Science and Technology

Details

• CRID: 1390001204738651392
• NII Article ID: 130004892317
• DOI: 10.11309/jssst.32.1_179
• ISSN: 02896540
• Text Lang: ja
• Data Source:
  • JaLC
  • CiNii Articles
  • KAKEN
• Abstract License Flag: Disallowed