項書換えの合流性解析とその応用

• 資料種別: 文書・図像類
• タイトル: 項書換えの合流性解析とその応用
• 著者・編者: 廣川, 直
• 著者標目: 廣川, 直
• 出版年月日等: 2016-06-03
• 出版年（W3CDTF）: 2016-06-03
• 並列タイトル等: Confluence Analysis for Term Rewriting and Its Applications
• タイトル（掲載誌）: 科学研究費助成事業研究成果報告書
• 掲載ページ: 1-4
• 本文の言語コード: jpn
• 件名標目: 項書換え; 合流性; 国際研究者交流; オーストリア
• 対象利用者: 一般
• 一般注記: 項書換えシステムは定理自動証明や仕様記述言語の基盤理論であり、演繹や計算は等式変形による答えの網羅的な探索として実現される。そのため計算結果が必ず一意に定まることを保証する合流性は、効率な計算の実現に大切な性質である。本研究では合流性の証明手法とその応用に取り組み以下の成果を得た：（１）可換性分解、危険対解析、Ｅ単一化に関する技法を開発・発展させ、強力な合流性解析を実現した。（２）それらの知見の応用として、定理自動証明の基盤理論である抽象完備化の正当性についての簡潔な証明、（３）さらに計算を効率的に行うための基本正規化定理を得た。 : Term rewriting is a fundamental computational model that underlies automated theorem proving and algebraic specification languages. In applications, deduction or computation is usually performed as an exhaustive search of normal forms. Therefore, for efficient computation, confluence that guarantees uniqueness of normal forms is considered as one of the most important properties in the area of rewriting. The main outcomes of our project are three: (1) We developed effective confluence analysis based on commutative decomposition, critical pair analysis, and E-unification. As applications of confluence analysis, (2) we obtained a simple proof for correctness of abstract completion which is a theoretical foundation of automated theorem proving, and also (3) a basic normalization theorem that enables us to effectively compute a normal form of basic terms.; 若手研究(B); 研究期間：2013～2015; 課題番号：25730004; 研究者番号：50467122; 研究分野：項書換え; identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/13678
• オンライン閲覧公開範囲: 限定公開
• 連携機関・データベース: 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）; https://irdb.nii.ac.jp
• 提供元機関・データベース: 北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ