Automated inductive theorem proving using transformations of term rewriting systems

Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

研究成果: Article査読

1 被引用数 (Scopus)

抄録

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 recursio

本文言語English
ページ(範囲)179-193
ページ数15
ジャーナルComputer Software
32
1
出版ステータスPublished - 2015 1 1

ASJC Scopus subject areas

  • ソフトウェア

フィンガープリント

「Automated inductive theorem proving using transformations of term rewriting systems」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル