Automated lemma generation for rewriting induction with disproof

Satoshi Shimazu, Takahito Aoto, Yoshihito Toyama

Research output: Contribution to journalArticlepeer-review

6 Citations (Scopus)

Abstract

Rewriting induction (Reddy, 1989) is an automated inductive theorem proving method for term rewriting systems. An automated lemma generation method for automated inductive theorem proving is said to be sound if it does not produce incorrect lemmas. Divergence critic (Walsh, 1996) is a well-known automated lemma generation method for the rewriting induction, but it is unsound. In this paper, we propose a sound variant of the divergence critic applicable for monomorphic term rewriting systems by incorporating sound generalization (Urso and Kounalis, 2004) in a part of its procedure. We implement these three automated lemma generation methods on a rewriting induction system with disproof to evaluate effectiveness of these methods. Our experiment reveals that the (sound) divergence critic and the sound generalization are often effective for different kinds of conjectures. Thus, the sound divergence critic can be combined with the sound generalization to obtain a more powerful automated sound lemma generation method for rewriting induction.

Original languageEnglish
Pages (from-to)41-55
Number of pages15
JournalComputer Software
Volume26
Issue number2
Publication statusPublished - 2009 Jul 29

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Automated lemma generation for rewriting induction with disproof'. Together they form a unique fingerprint.

Cite this