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

Material type: 文書・図像類

Author: 廣川, 直

Publisher: -

Publication date: 2016-06-03

Material Format: Digital

Capacity, size, etc.: -

NDC: -

View All

Notes on use

Note (General)：: 項書換えシステムは定理自動証明や仕様記述言語の基盤理論であり、演繹や計算は等式変形による答えの網羅的な探索として実現される。そのため計算結果が必ず一意に定まることを保証する合流性は、効率な計算の実現に大切な性質である。本研究では合流性の証明手法とその応用に取り組み以下の成果を得た：（１）可換性分解、...

Search by Bookstore

Holdings of Libraries in Japan

This page shows libraries in Japan other than the National Diet Library that hold the material.

List of Cooperating Institutions and Databases

Please contact your local library for information on how to use materials or whether it is possible to request materials from the holding libraries.

other

JAIST Repository
Digital
You can check the holdings of institutions and databases with which 学術機関リポジトリデータベース（IRDB）（機関リポジトリ） is linked at the site of 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）.
JAIST Repository

Search by Bookstore

Bibliographic Record

You can check the details of this material, its authority (keywords that refer to materials on the same subject, author's name, etc.), etc.

Digital

Material Type: 文書・図像類
Title: 項書換えの合流性解析とその応用
Author/Editor: 廣川, 直
Author Heading: 廣川, 直
Publication Date: 2016-06-03
Publication Date (W3CDTF): 2016-06-03
Alternative Title: Confluence Analysis for Term Rewriting and Its Applications
Periodical title: 科学研究費助成事業研究成果報告書
Pages: 1-4
Text Language Code: jpn
Subject Heading: 項書換え
合流性
国際研究者交流
オーストリア
Target Audience: 一般
Note (General): 項書換えシステムは定理自動証明や仕様記述言語の基盤理論であり、演繹や計算は等式変形による答えの網羅的な探索として実現される。そのため計算結果が必ず一意に定まることを保証する合流性は、効率な計算の実現に大切な性質である。本研究では合流性の証明手法とその応用に取り組み以下の成果を得た：（１）可換性分解、危険対解析、Ｅ単一化に関する技法を開発・発展させ、強力な合流性解析を実現した。（２）それらの知見の応用として、定理自動証明の基盤理論である抽象完備化の正当性についての簡潔な証明、（３）さらに計算を効率的に行うための基本正規化定理を得た。 : 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
Format (IMT): application/pdf
Source: https://dspace.jaist.ac.jp/dspace/bitstream/10119/13678/1/25730004seika.pdf
https://dspace.jaist.ac.jp/dspace/bitstream/10119/13678/1/25730004seika.pdf
Access Restrictions: 限定公開
Data Provider (Database): 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
https://irdb.nii.ac.jp
Original Data Provider (Database): 北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ