WEKO3
アイテム
PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES
http://hdl.handle.net/10252/00005828
http://hdl.handle.net/10252/0000582800b15984-e095-41ee-9ef3-14bf07b39e20
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IJICIC2013-9-11 (687.9 kB)
|
|
| Item type | 学術雑誌論文 / Journal Article(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2018-09-21 | |||||
| タイトル | ||||||
| タイトル | PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES | |||||
| 言語 | en | |||||
| 言語 | ||||||
| 言語 | eng | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | Unsatisability | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | Proof | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | Equivalent transformation rule | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | Induction | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||
| 資源タイプ | journal article | |||||
| 著者 |
Miura, Katsunori
× Miura, Katsunori× Akama, Kiyoshi× Koike, Hidekatsu× Mabuchi, Hiroshi |
|||||
| 著者別名 | ||||||
| 識別子Scheme | WEKO | |||||
| 識別子 | 32521 | |||||
| 姓名 | 三浦, 克宜 | |||||
| 言語 | ja | |||||
| 書誌情報 |
en : International Journal of Innovative Computing, Information and Control 巻 9, 号 11, p. 4419-4430, 発行日 2013-11 |
|||||
| 出版者 | ||||||
| 出版者 | ICIC International | |||||
| 言語 | en | |||||
| ISSN / EISSN | ||||||
| 収録物識別子タイプ | PISSN | |||||
| 収録物識別子 | 1349-4198 | |||||
| 書誌ID（NCID） | ||||||
| 収録物識別子タイプ | NCID | |||||
| 収録物識別子 | AA12218449 | |||||
| 権利表記 | ||||||
| 言語 | en | |||||
| 権利情報 | ©2013 ICIC International | |||||
| テキストバージョン | ||||||
| 出版タイプ | VoR | |||||
| 出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||
| 日本十進分類法 | ||||||
| 言語 | ja | |||||
| 主題Scheme | NDC | |||||
| 主題 | 375 | |||||
| NIIサブジェクト | ||||||
| 言語 | ja | |||||
| 主題Scheme | Other | |||||
| 主題 | メディア・コミュニケーション | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | Equivalent Transformation (ET) rules can be used to construct correct sequential and parallel programs, as they are inherently correct. One important method for making ET rules uses logical formulas. Among logical formulas, unsatisfiable conjunctions of finite atoms, each of which is represented by an atom set in this paper, are especially useful for making many ET rules that are used for constructing efficient programs. This paper proposes a method of proving unsatisfiability of an atom set based on computation by ET rules. The proposed method is recursive, in the sense that, during proving the given atom set, it may find a new atom set based on subset relation or inductive structure. Since our proposed method incorporates search based on subset and inductive relations, it can be used to prove unsatisfiability of various atom sets that cannot be proven by conventional methods. | |||||
| 言語 | en | |||||
