| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2014-03-11 13:30 制約付き木オートマトンにおける不用な遷移規則の発見法について ○中野靖大・西田直樹・酒井正彦・坂部俊樹・草刈圭一朗・橋本健二（名大）  SS2013-77 |
|
| 抄録 | （和） | 項の書換え完全性は，制約付き項書換え系の書換え帰納法に基づいた定理自動証明の際に何回も証明を試みられる性質である．また，対象の制約付き項書換え系についての解釈可能な項に関する十分完全性は，定理自動証明中の推論規則の適用条件を緩和させる．これらの性質は書換え可能な項の集合に関する積集合空問題に帰着でき，制約付き木オートマトンを用いた十分条件による証明法が既に提案されている．しかし，既存手法では構成される制約付き木オートマトンに，どの基底項からも到達不可能な状態が存在することがあり，そのような状態の削除が不十分であることが証明の妨げとなることが確認されている．また，そのような状態を含む不用な遷移規則の存在は，オートマトンのサイズを増大させる原因になる．本論文では，証明中で構成される制約付き木オートマトン中の不用な遷移規則を削除することで，到達不可能な状態を可能な限り削除する手法を提案する．そして，解釈可能な項に関する十分完全性の証明力を向上させる． |
| （英） | 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 / / / / / | |
| 文献情報 | 信学技報, vol. 113, no. 489, SS2013-77, pp. 31-36, 2014年3月. | |
| 資料番号 | SS2013-77 | |
| 発行日 | 2014-03-04 (SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2013-77 |
|
| 研究会情報 | |
| 研究会 | SS |
| 開催期間 | 2014-03-11 - 2014-03-12 |
| 開催地（和） | てんぷす那覇：第１・２会議室 |
| 開催地（英） | Tenbusu Naha |
| テーマ（和） | 一般 |
| テーマ（英） | Software Science |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2014-03-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | 制約付き木オートマトンにおける不用な遷移規則の発見法について |
| サブタイトル（和） | |
| タイトル（英） | On Detecting Useless Transition Rules of Constrained Tree Automata |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 制約付き項書換え系 / constrained term rewriting system |
| キーワード(2)（和/英） | 積集合空問題 / intersection emptiness problem |
| キーワード(3)（和/英） | 十分完全性 / sufficient completeness |
| キーワード(4)（和/英） | / |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 中野 靖大 / Yasuhiro Nakano / |
| 第1著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 西田 直樹 / Naoki Nishida / |
| 第2著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 酒井 正彦 / Masahiko Sakai / |
| 第3著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第4著者 氏名（和/英/ヨミ） | 坂部 俊樹 / Toshiki Sakabe / |
| 第4著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第5著者 氏名（和/英/ヨミ） | 草刈 圭一朗 / Keiichirou Kusakari / |
| 第5著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第6著者 氏名（和/英/ヨミ） | 橋本 健二 / Kenji Hashimoto / |
| 第6著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第7著者 氏名（和/英/ヨミ） | / / |
| 第7著者 所属（和/英） | (略称： ) (略称： ) |
| 第8著者 氏名（和/英/ヨミ） | / / |
| 第8著者 所属（和/英） | (略称： ) (略称： ) |
| 第9著者 氏名（和/英/ヨミ） | / / |
| 第9著者 所属（和/英） | (略称： ) (略称： ) |
| 第10著者 氏名（和/英/ヨミ） | / / |
| 第10著者 所属（和/英） | (略称： ) (略称： ) |
| 第11著者 氏名（和/英/ヨミ） | / / |
| 第11著者 所属（和/英） | (略称： ) (略称： ) |
| 第12著者 氏名（和/英/ヨミ） | / / |
| 第12著者 所属（和/英） | (略称： ) (略称： ) |
| 第13著者 氏名（和/英/ヨミ） | / / |
| 第13著者 所属（和/英） | (略称： ) (略称： ) |
| 第14著者 氏名（和/英/ヨミ） | / / |
| 第14著者 所属（和/英） | (略称： ) (略称： ) |
| 第15著者 氏名（和/英/ヨミ） | / / |
| 第15著者 所属（和/英） | (略称： ) (略称： ) |
| 第16著者 氏名（和/英/ヨミ） | / / |
| 第16著者 所属（和/英） | (略称： ) (略称： ) |
| 第17著者 氏名（和/英/ヨミ） | / / |
| 第17著者 所属（和/英） | (略称： ) (略称： ) |
| 第18著者 氏名（和/英/ヨミ） | / / |
| 第18著者 所属（和/英） | (略称： ) (略称： ) |
| 講演者 | 第1著者 |
| 発表日時 | 2014-03-11 13:30:00 |
| 発表時間 | 30分 |
| 申込先研究会 | SS |
| 資料番号 | SS2013-77 |
| 巻番号（vol） | vol.113 |
| 号番号（no） | no.489 |
| ページ範囲 | pp.31-36 |
| ページ数 | 6 |
| 発行日 | 2014-03-04 (SS) |
[研究会発表申込システムのトップページに戻る]