Automated Lemma Generation for Rewriting Induction with Disproof

• SHIMAZU Satoshi

  NTT Access Network Service Systems Laboratories

• AOTO Takahito

  RIEC, Tohoku University

• TOYAMA Yoshihito

  RIEC, Tohoku University

Bibliographic Information

Other Title

• 反証機能付き書き換え帰納法のための補題自動生成法
• ハンショウ キノウ ツキ カキカエ キノウホウ ノ タメ ノ ホダイ ジドウ セイセイホウ

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.

Journal

• Computer Software

  Computer Software 26 (2), 41-55, 2009

  Japan Society for Software Science and Technology

Details

• CRID: 1390001204736492288
• NII Article ID: 10025982372
• NII Book ID: AN10075819
• DOI: 10.11309/jssst.26.2_41
• NDL BIB ID: 10290049
• ISSN: 02896540
• Web Site: http://id.ndl.go.jp/bib/10290049
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I10290049
• Data Source:
  • JaLC
  • NDL
  • CiNii Articles
  • KAKEN
• Abstract License Flag: Disallowed