JAIST Repository >
School of Information Science >
Grants-in-aid for Scientific Research Papers >
FY 2015 >

Please use this identifier to cite or link to this item: http://hdl.handle.net/10119/13678

Title: 項書換えの合流性解析とその応用
Other Titles: Confluence Analysis for Term Rewriting and Its Applications
Authors: 廣川, 直
Authors(alternative): Hirokawa, Nao
Keywords: 項書換え
合流性
国際研究者交流
オーストリア
Issue Date: 3-Jun-2016
Abstract: 項書換えシステムは定理自動証明や仕様記述言語の基盤理論であり、演繹や計算は等式変形による答えの網羅的な探索として実現される。そのため計算結果が必ず一意に定まることを保証する合流性は、効率な計算の実現に大切な性質である。本研究では合流性の証明手法とその応用に取り組み以下の成果を得た:(1)可換性分解、危険対解析、E単一化に関する技法を開発・発展させ、強力な合流性解析を実現した。(2)それらの知見の応用として、定理自動証明の基盤理論である抽象完備化の正当性についての簡潔な証明、(3)さらに計算を効率的に行うための基本正規化定理を得た。 : 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.
Description: 若手研究(B)
研究期間:2013~2015
課題番号:25730004
研究者番号:50467122
研究分野:項書換え
Language: jpn
URI: http://hdl.handle.net/10119/13678
Appears in Collections:2015年度 (FY 2015)

Files in This Item:

File Description SizeFormat
25730004seika.pdf84KbAdobe PDFView/Open

All items in DSpace are protected by copyright, with all rights reserved.

 


Contact : Library Information Section, JAIST (ir-sys[at]ml.jaist.ac.jp)