WEKO3
アイテム
ET-BASED BIDIRECTIONAL SEARCH FOR PROVING FORMULAS IN THE CLASS ES
http://hdl.handle.net/10252/00005827
http://hdl.handle.net/10252/00005827a08b133b-498b-4618-b3f3-ab1134c07ba6
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IJICIC2014-10-6 (265.7 kB)
|
|
| Item type | 学術雑誌論文 / Journal Article(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2018-09-21 | |||||
| タイトル | ||||||
| タイトル | ET-BASED BIDIRECTIONAL SEARCH FOR PROVING FORMULAS IN THE CLASS ES | |||||
| 言語 | en | |||||
| 言語 | ||||||
| 言語 | eng | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | Logical equivalence | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | Bidirectional search | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | Correctness | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | ET rule | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | Induction | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||
| 資源タイプ | journal article | |||||
| 著者 |
Miura, Katsunori
× Miura, Katsunori× Akama, Kiyoshi |
|||||
| 著者別名 | ||||||
| 識別子Scheme | WEKO | |||||
| 識別子 | 32517 | |||||
| 姓名 | 三浦, 克宜 | |||||
| 言語 | ja | |||||
| 書誌情報 |
en : International Journal of Innovative Computing, Information and Control 巻 10, 号 6, p. 1999-2009, 発行日 2014-12 |
|||||
| 出版者 | ||||||
| 出版者 | ICIC International | |||||
| 言語 | en | |||||
| ISSN / EISSN | ||||||
| 収録物識別子タイプ | PISSN | |||||
| 収録物識別子 | 1349-4198 | |||||
| 書誌ID（NCID） | ||||||
| 収録物識別子タイプ | NCID | |||||
| 収録物識別子 | AA12218449 | |||||
| 権利表記 | ||||||
| 言語 | en | |||||
| 権利情報 | ©2014 ICIC International | |||||
| テキストバージョン | ||||||
| 出版タイプ | VoR | |||||
| 出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||
| 日本十進分類法 | ||||||
| 言語 | ja | |||||
| 主題Scheme | NDC | |||||
| 主題 | 375 | |||||
| NIIサブジェクト | ||||||
| 言語 | ja | |||||
| 主題Scheme | Other | |||||
| 主題 | メディア・コミュニケーション | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | In this paper, we propose a new method for proving the correctness of Logical Equivalences (LEs) in a newly defined class called ES. Proving the correctness of LEs is important for guaranteeing the correctness of Equivalent Transformation (ET) rules made from LEs. ET rules are useful for constructing correct sequential and parallel programs. The proposed method proves the equivalence of the declarative meaning of two definite clause sets using a bidirectional search that starts from two different points simultaneously. In the proposed method, the two definite clause sets at the starting points are transformed by ET rules. The method can generate ET rules that are essential for advancing the proof along with the general unfolding rules that are given before computing the proof. Class ES is a superclass of the classes proposed in past studies and therefore covers the LEs they contain. | |||||
| 言語 | en | |||||
