| 講演名 | 2014-03-11 制約付き木オートマトンにおける不用な遷移規則の発見法について 中野 靖大, 西田 直樹, 酒井 正彦, 坂部 俊樹, 草刈 圭一朗, 橋本 健二, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 項の書換え完全性は,制約付き項書換え系の書換え帰納法に基づいた定理自動証明の際に何回も証明を試みられる性質である.また,対象の制約付き項書換え系についての解釈可能な項に関する十分完全性は,定理自動証明中の推論規則の適用条件を緩和させる.これらの性質は書換え可能な項の集合に関する積集合空問題に帰着でき,制約付き本オートマトンを用いた十分条件による証明法が既に提案されている.しかし,既存手法では構成される制約付き木オートマトンに,どの基底項からも到達不可能な状態が存在することがあり,そのような状態の削除が不十分であることが証明の妨げとなることが確認されている.また,そのような状態を含む不用な遷移規則の存在は,オートマトンのサイズを増大させる原因になる.本論文では,証明中で構成される制約付き本オートマトン中の不用な遷移規則を削除することで,到達不可能な状態を可能な限り削除する手法を提案する.そして,解釈可能な項に関する十分完全性の証明力を向上させる. |
| 抄録(英) | Reduction completeness of terms is proved many times in a theorem proving method for constrained term rewriting systems which is based on rewriting induction. In addition, sufficient completeness with respect to interpretable terms enables us to relax the side conditions of some inference rules in the proving method. These two properties can be reduced to the intersection emptiness problem related to sets of reducible ground terms, and by using constrained tree automata, a proving method of these properties has already been proposed. However, constructed automata in the method may have states which are not accessible from any ground terms, and the existence of such states leads us to the failure of proofs. Moreover, the existence of useless transition rules with such states increases the size of the constructed automata. In this paper, we propose a state-reduction method to detect inaccessible states as much as possible by removing such useless transition rules, and improve the method for proving the sufficient completeness with respect to interpretable terms. |
| キーワード(和) | 制約付き項書換え系 / 積集合空問題 / 十分完全性 |
| キーワード(英) | constrained term rewriting system / intersection emptiness problem / sufficient completeness |
| 資料番号 | SS2013-77 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2014/3/4(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 制約付き木オートマトンにおける不用な遷移規則の発見法について |
| サブタイトル（和） | |
| タイトル（英） | On Detecting Useless Transition Rules of Constrained Tree Automata |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 制約付き項書換え系 / constrained term rewriting system |
| キーワード(2)（和/英） | 積集合空問題 / intersection emptiness problem |
| キーワード(3)（和/英） | 十分完全性 / sufficient completeness |
| 第 1 著者 氏名（和/英） | 中野 靖大 / Yasuhiro NAKANO |
| 第 1 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 2 著者 氏名（和/英） | 西田 直樹 / Naoki NISHIDA |
| 第 2 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 3 著者 氏名（和/英） | 酒井 正彦 / Masahiko SAKAI |
| 第 3 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 4 著者 氏名（和/英） | 坂部 俊樹 / Toshiki SAKABE |
| 第 4 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 5 著者 氏名（和/英） | 草刈 圭一朗 / Keiichirou KUSAKARI |
| 第 5 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 6 著者 氏名（和/英） | 橋本 健二 / Kenji HASHIMOTO |
| 第 6 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 発表年月日 | 2014-03-11 |
| 資料番号 | SS2013-77 |
| 巻番号（vol） | vol.113 |
| 号番号（no） | 489 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |