WEKO3
アイテム
PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES
https://kitami-it.repo.nii.ac.jp/records/7952
https://kitami-it.repo.nii.ac.jp/records/7952c1486ccc-4f1c-4473-88f9-99ca0d78e010
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
2013.11_Proof of Unsatisfiability of Atom Sets based on Computation by Equivalent Transformation Rules.pdf (146.7 kB)
|
|
| Item type | 学術雑誌論文 / Journal Article(1) | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2015-09-03 | |||||||||||||
| タイトル | ||||||||||||||
| タイトル | PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES | |||||||||||||
| 言語 | en | |||||||||||||
| 言語 | ||||||||||||||
| 言語 | eng | |||||||||||||
| キーワード | ||||||||||||||
| 主題Scheme | Other | |||||||||||||
| 主題 | Unsatisability | |||||||||||||
| キーワード | ||||||||||||||
| 主題Scheme | Other | |||||||||||||
| 主題 | Proof | |||||||||||||
| キーワード | ||||||||||||||
| 主題Scheme | Other | |||||||||||||
| 主題 | Equivalent transformation rule | |||||||||||||
| キーワード | ||||||||||||||
| 主題Scheme | Other | |||||||||||||
| 主題 | Induction | |||||||||||||
| 資源タイプ | ||||||||||||||
| 資源 | http://purl.org/coar/resource_type/c_6501 | |||||||||||||
| タイプ | journal article | |||||||||||||
| アクセス権 | ||||||||||||||
| アクセス権URI | open access | |||||||||||||
| 著者 |
Miura, Katsunori
× Miura, Katsunori
× Akama, Kiyoshi
× Koike, Hidekatsu
× Mabuchi, Hiroshi
|
|||||||||||||
| 著者別名 | ||||||||||||||
| 識別子Scheme | WEKO | |||||||||||||
| 識別子 | 44889 | |||||||||||||
| 識別子Scheme | KAKEN | |||||||||||||
| 識別子URI | https://nrid.nii.ac.jp/ja/nrid/1000050636587 | |||||||||||||
| 識別子 | 50636587 | |||||||||||||
| 姓名 | 三浦, 克宜 | |||||||||||||
| 言語 | ja | |||||||||||||
| 抄録 | ||||||||||||||
| 内容記述タイプ | Abstract | |||||||||||||
| 内容記述 | Equivalent Transformation (ET) rules can be used to construct correct se- quential and parallel programs, as they are inherently correct. One important method for making ET rules uses logical formulas. Among logical formulas, unsatis able con- junctions of nite 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 pro- grams. This paper proposes a method of proving unsatis ability 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 nd a new atom set based on subset relation or in- ductive structure. Since our proposed method incorporates search based on subset and inductive relations, it can be used to prove unsatis ability of various atom sets that can- not be proven by conventional methods. |
|||||||||||||
| 書誌情報 |
International Journal of Innovative Computing, Information and Control 巻 9, 号 11, p. 4419-4430, 発行日 2013-11 |
|||||||||||||
| 権利 | ||||||||||||||
| 権利情報 | c 2013 ICIC International | |||||||||||||
| 出版者 | ||||||||||||||
| 出版者 | ICIC International | |||||||||||||
| 言語 | en | |||||||||||||
| 関連サイト | ||||||||||||||
| URL | http://www.ijicic.org/contents.htm | |||||||||||||
| 著者版フラグ | ||||||||||||||
| 言語 | en | |||||||||||||
| 値 | publisher | |||||||||||||
| 出版タイプ | ||||||||||||||
| 出版タイプ | VoR | |||||||||||||
| 出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||||||||||
