書誌事項
- タイトル別名
-
- Automated Lemma Generation for Rewriting Induction with Disproof
- ハンショウ キノウ ツキ カキカエ キノウホウ ノ タメ ノ ホダイ ジドウ セイセイホウ
この論文をさがす
抄録
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.
収録刊行物
-
- コンピュータ ソフトウェア
-
コンピュータ ソフトウェア 26 (2), 41-55, 2009
日本ソフトウェア科学会
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1390001204736492288
-
- NII論文ID
- 10025982372
-
- NII書誌ID
- AN10075819
-
- NDL書誌ID
- 10290049
-
- ISSN
- 02896540
-
- データソース種別
-
- JaLC
- NDL
- CiNii Articles
- KAKEN
-
- 抄録ライセンスフラグ
- 使用不可