WEKO3
アイテム
Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting
http://hdl.handle.net/2237/9580
http://hdl.handle.net/2237/9580729d6567-d065-49f5-9b5c-916d2733064e
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
E88-D_n12_2715-2726.pdf (1.3 MB)
|
|
| Item type | 学術雑誌論文 / Journal Article(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2008-03-10 | |||||
| タイトル | ||||||
| タイトル | Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting | |||||
| 言語 | en | |||||
| 著者 |
KUSAKARI, Keiichirou
× KUSAKARI, Keiichirou× SAKAI, Masahiko× SAKABE, Toshiki |
|||||
| アクセス権 | ||||||
| アクセス権 | open access | |||||
| アクセス権URI | http://purl.org/coar/access_right/c_abf2 | |||||
| 権利 | ||||||
| 言語 | ja | |||||
| 権利情報 | Copyright 2005 IEICE 許諾番号 08RB0027号 | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | algebraic specification | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | simply-typed term rewriting system | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | primitive inductive theorem | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | inductive theorem | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | implicit induction method | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | Automated reasoning of inductive theorems is considered important in program verification. To verify inductive theorems automatically, several implicit induction methods like the inductionless induction and the rewriting induction methods have been proposed. In studying inductive theorems on higher-order rewritings, we found that the class of the theorems shown by known implicit induction methods does not coincide with that of inductive theorems, and the gap between them is a barrier in developing mechanized methods for disproving inductive theorems. This paper fills this gap by introducing the notion of primitive inductive theorems, and clarifying the relation between inductive theorems and primitive inductive theorems. Based on this relation, we achieve mechanized methods for proving and disproving inductive theorems. | |||||
| 言語 | en | |||||
| 出版者 | ||||||
| 出版者 | IEICE | |||||
| 言語 | ja | |||||
| 言語 | ||||||
| 言語 | eng | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||
| 資源タイプ | journal article | |||||
| 出版タイプ | ||||||
| 出版タイプ | VoR | |||||
| 出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||
| ISSN | ||||||
| 収録物識別子タイプ | PISSN | |||||
| 収録物識別子 | 0916-8532 | |||||
| 書誌情報 |
en : IEICE Transactions on Information and Systems 巻 E88-D, 号 12, p. 2715-2726, 発行日 2005-12 |
|||||
| フォーマット | ||||||
| 値 | application/pdf | |||||
| 著者版フラグ | ||||||
| 値 | publisher | |||||
| URI | ||||||
| 識別子 | http://hdl.handle.net/2237/9580 | |||||
| 識別子タイプ | HDL | |||||
