Automated inductive theorem proving using transformations of term rewriting systems

Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)

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 recursio

Original languageEnglish
Pages (from-to)179-193
Number of pages15
JournalComputer Software
Volume32
Issue number1
Publication statusPublished - 2015 Jan 1

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Automated inductive theorem proving using transformations of term rewriting systems'. Together they form a unique fingerprint.

Cite this