Soundness of Rewriting Induction Based on an Abstract Principle

• Item type: Trans(1)
• 公開日: 2008-01-15
• タイトル: Soundness of Rewriting Induction Based on an Abstract Principle
• タイトル / 言語: en
• タイトル: Soundness of Rewriting Induction Based on an Abstract Principle
• 言語: eng
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: RIEC Tohoku University
• 著者所属(英): en
• 著者所属(英): RIEC, Tohoku University
• 著者名: Takahito, Aoto
• 著者名(英): Takahito, Aoto
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: Rewriting induction (Reddy 1990) is a method to prove inductive theorems of term rewriting systems automatically. Koike and Toyama (2000) extracted an abstract principle of rewriting induction in terms of abstract reduction systems. Based on their principle the soundness of the original rewriting induction system can be proved. It is not known however whether such an approach can be adapted also for more powerful rewriting induction systems. In this paper we give a new abstract principle that extends Koike and Toyama’s abstract principle.Using this principle we show the soundness of a rewriting induction system extended with an inference rule of simplification by conjectures. Inference rules of simplification by conjectures have been used in many rewriting induction systems. Replacement of the underlying rewriting mechanism with ordered rewriting is an important refinement of rewriting induction?with this refinement rewriting induction can handle non-orientable equations. It is shown that based on the introduced abstract principle a variant of our rewriting induction system based on ordered rewriting is sound provided that its base order is ground-total. In our system based on ordered rewriting the simplification rule extends those of the equational fragment of some major systems from the literature.
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Rewriting induction (Reddy, 1990) is a method to prove inductive theorems of term rewriting systems automatically. Koike and Toyama (2000) extracted an abstract principle of rewriting induction in terms of abstract reduction systems. Based on their principle, the soundness of the original rewriting induction system can be proved. It is not known, however, whether such an approach can be adapted also for more powerful rewriting induction systems. In this paper, we give a new abstract principle that extends Koike and Toyama’s abstract principle.Using this principle, we show the soundness of a rewriting induction system extended with an inference rule of simplification by conjectures. Inference rules of simplification by conjectures have been used in many rewriting induction systems. Replacement of the underlying rewriting mechanism with ordered rewriting is an important refinement of rewriting induction窶背ith this refinement, rewriting induction can handle non-orientable equations. It is shown that,based on the introduced abstract principle, a variant of our rewriting induction system based on ordered rewriting is sound, provided that its base order is ground-total. In our system based on ordered rewriting, the simplification rule extends those of the equational fragment of some major systems from the literature.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 49, 号 SIG1(PRO35), p. 28-38, 発行日 2008-01-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会