WEKO3
アイテム
制約付き項書換え系の書換え帰納法における補題等式の自動生成法
http://hdl.handle.net/2237/21169
http://hdl.handle.net/2237/211698074f77a-5d5b-41a7-a8d3-317c734ca47e
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
28_1_173.pdf (241.0 kB)
|
|
| Item type | 学術雑誌論文 / Journal Article(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2015-01-30 | |||||
| タイトル | ||||||
| タイトル | 制約付き項書換え系の書換え帰納法における補題等式の自動生成法 | |||||
| 言語 | ja | |||||
| その他のタイトル | ||||||
| その他のタイトル | Lemma Generation Method in Rewriting Induction for Constrained Term Rewriting Systems | |||||
| 言語 | en | |||||
| 著者 |
中林, 直生
× 中林, 直生× 西田, 直樹× 草刈, 圭一朗× 坂部, 俊樹× 酒井, 正彦× Nakabayashi, Naoki× Nishida, Naoki× Kusakari, Keiichirou× Sakabe, Toshiki× Sakai, Masahiko |
|||||
| アクセス権 | ||||||
| アクセス権 | open access | |||||
| アクセス権URI | http://purl.org/coar/access_right/c_abf2 | |||||
| 権利 | ||||||
| 言語 | ja | |||||
| 権利情報 | ここに掲載した著作物の利用に関する注意 本著作物の著作権は日本ソフトウェア科学会に帰属します．本著作物は著作権者である日本ソフトウェア科学会の許可のもとに掲載するものです．ご利用に当たっては「著作権法」に従うことをお願いいたします．Notice for the use of this material: The copyright of this material is retained by the Japan Society for Software Science and Technology (JSSST). This material is published on this web site with the agreement of the JSSST. Please be complied with Copyright Law of Japan if any users wish to reproduce, make derivative work, distribute or make available to the public any part or whole thereof. | |||||
| 権利 | ||||||
| 言語 | ja | |||||
| 権利情報 | 本文データは学会の許諾に基づきJ-STAGEより複製したものである。 | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | 近年，帰納的定理の証明原理の1つである書換え帰納法が制約付き項書換え系に対応するように拡張され，命令型プログラムの等価性検証に応用するための枠組みが提案された．帰納的定理の証明のためには適切な補題等式を与える必要がある場合が多いが，項書換え系においてこれまで研究が進んでいる補題生成の手法を制約付き項書換え系に対して利用するためには制約部分を扱うための拡張が必要である．本論文では，書換え規則から項の関係を定式化し，その関係に基づいて等式をより一般的な等式に変換する枠組みを提案する．さらに，制約付き項書換え系の書換え帰納法による証明手続きにその枠組みを利用した補題等式の生成・追加機能を組み込むことで，補題等式を予め記述せずに定理自動証明を試み，その有効性を検証する． | |||||
| 言語 | ja | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | Recently, the rewriting induction, which is one of induction principles for proving inductive theorems of an equational theory, has been extended to deal with constrained term rewriting systems. It has been applied to developing a method for proving equivalence of imperative programs. For proving inductive theorem, there are many cases where appropriate lemmas need to be added. To this end, several methods for lemma generation in term rewriting have been studied. However, these existing methods are not effective for cases in constrained term rewriting. In this paper, we propose a framework of lemma generation for constrained term rewriting systems, in which we formalize the correspondences of terms in divergent equations by means of given constrained rewrite rules. We also show an instance of the formalization, and show that due to the framework with the instance, there is no necessity to give lemmas in advance in the examples shown by the previous works. | |||||
| 言語 | en | |||||
| 出版者 | ||||||
| 出版者 | 日本ソフトウェア科学会 | |||||
| 言語 | ja | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| 資源タイプ | ||||||
| 資源タイプresource | http://purl.org/coar/resource_type/c_6501 | |||||
| タイプ | journal article | |||||
| 出版タイプ | ||||||
| 出版タイプ | VoR | |||||
| 出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||
| DOI | ||||||
| 関連タイプ | isVersionOf | |||||
| 識別子タイプ | DOI | |||||
| 関連識別子 | https://doi.org/10.11309/jssst.28.1_173 | |||||
| ISSN | ||||||
| 収録物識別子タイプ | PISSN | |||||
| 収録物識別子 | 0289-6540 | |||||
| 書誌情報 |
ja : コンピュータソフトウェア 巻 28, 号 1, p. 173-189, 発行日 2011-02 |
|||||
| 著者版フラグ | ||||||
| 値 | publisher | |||||
| URI | ||||||
| 識別子 | http://dx.doi.org/10.11309/jssst.28.1_173 | |||||
| 識別子タイプ | DOI | |||||
| URI | ||||||
| 識別子 | http://hdl.handle.net/2237/21169 | |||||
| 識別子タイプ | HDL | |||||
