文献

J-GLOBAL ID：201402209788872028   整理番号：14A0569355

制約付き木オートマトンにおける不用な遷移規則の発見法について

On Detecting Useless Transition Rules of Constrained Tree Automata

著者 (6件)： 中野靖大 (名古屋大 大学院情報科学研究科) ,  西田直樹 (名古屋大 大学院情報科学研究科) ,  酒井正彦 (名古屋大 大学院情報科学研究科) ,  坂部俊樹 (名古屋大 大学院情報科学研究科) ,  草刈圭一朗 (名古屋大 大学院情報科学研究科) ,  橋本健二 (名古屋大 大学院情報科学研究科)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 113  号： 489(SS2013 72-90)  ページ： 31-36  発行年： 2014年03月04日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 項の書換え完全性は,制約付き項書換え系の書換え帰納法に基づいた定理自動証明の際に何回も証明を試みられる性質である。また,対象の制約付き項書換え系についての解釈可能な項に関する十分完全性は,定理自動証明中の推論規則の適用条件を緩和させる。これらの性質は書換え可能な項の集合に関する積集合空問題に帰着でき,制約付き木オートマトンを用いた十分条件による証明法が既に提案されている。しかし,既存手法では構成される制約付き木オートマトンに,どの基底項からも到達不可能な状態が存在することがあり,そのような状態の削除が不十分であることが証明の妨げとなることが確認されている。また,そのような状態を含む不用な遷移規則の存在は,オートマトンのサイズを増大させる原因になる。本論文では,証明中で構成される制約付き木オートマトン中の不用な遷移規則を削除することで,到達不可能な状態を可能な限り削除する手法を提案する。そして,解釈可能な項に関する十分完全性の証明力を向上させる。(著者抄録)

シソーラス用語： *木オートマトン ,  *規則 ,  *発見的方法 ,  *制約条件 ,  項書換え系 ,  証明 ,  完全性 ,  オートマトン
準シソーラス用語： 推論規則 ,  *遷移規則 ,  定理自動証明

分類 (1件)： オートマトン理論  (JB04000O)

引用文献 (10件)：

• F. Baader and T. Niplow.: “Term Rewriting and All that“, Cambridge University Press, 1998.
• M. Huth and M. Ryan.: “Logic in Computer Science: Modelling and Reasoning about Systems“, Cambridge University Press, United Kingdom, 2000.
• H. Comon, M. Dauchet, R. Gilleron, F. Jacqumard, D. Lugiez, C. Loding, S. Tison and M. Tommasi.: “Tree Automata Techniques and Applications“, Available on: http://tata.gforge.inria.fr/, 2008.
• N. Nishida, F. Nomura, K. Kurahashi and M. Sakai.: “Constrained Tree Automata and their Closure Properties“, In Proc. TTATT 2012, pp. 24-34, 2012.
• N. Nishida, M. Sakai and Y. Nakano.: “On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms“, In Proc. TTATT 2013, pp. 1-10, 2013.

タイトルに関連する用語 (3件)： 制約 ,  木オートマトン ,  遷移規則