非決定計算のための項書き換え理論

Material type: 文書・図像類

Author: 廣川, 直

Publisher: -

Publication date: 2013-05-31

Material Format: Digital

Capacity, size, etc.: -

NDC: -

View All

Notes on use

Note (General)：: 本研究では関数型プログラムや定理証明システムの計算モデルである項書換えシステムに対し、その基礎理論を相対停止性という性質をもとに再考した。その研究成果として、合流性に関する主要二定理（Rosen の直交性と完備性）を左線形の場合に対し統一した。また極大完備化という定理証明ための新たな基盤技術を開発し...

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: 2013-05-31
Publication Date (W3CDTF): 2013-05-31
Alternative Title: Rewriting Techniques for Non-Deterministic Computation
Periodical title: 科学研究費助成事業研究成果報告書
Pages: 1-4
Text Language Code: jpn
Subject Heading: 項書換え
合流性
完備化
戦略
Target Audience: 一般
Note (General): 本研究では関数型プログラムや定理証明システムの計算モデルである項書換えシステムに対し、その基礎理論を相対停止性という性質をもとに再考した。その研究成果として、合流性に関する主要二定理（Rosen の直交性と完備性）を左線形の場合に対し統一した。また極大完備化という定理証明ための新たな基盤技術を開発した。これらの新技法を採用した強力な合流性解析ツールSaigawa と自動完備化ツールMaxcomp を開発した。 : Term rewriting is a computational model which underlies functional programming and theorem proving. In this research project we revisited its fundamental theory in the light of relative termination. As an outcome, we established a new confluence criterion that unifies two major confluence criteria (Rosen’s orthogonality and Knuth and Bendix’ completeness) for left-linear systems. Moreover, we introduced a new technique for automated deduction, dubbed maximal completion. Based on those new technologies, we developed the powerful confluence analyzer Saigawa and the fully automatic completion tool Maxcomp.
研究種目：若手研究（Ｂ）
研究期間：2010～2012
課題番号：22700009
研究者番号：50467122
研究分野：項書換え
科研費の分科・細目：情報学・情報学基礎
identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/11371
Format (IMT): application/pdf
Source: https://dspace.jaist.ac.jp/dspace/bitstream/10119/11371/1/22700009seika.pdf
https://dspace.jaist.ac.jp/dspace/bitstream/10119/11371/1/22700009seika.pdf
Access Restrictions: 限定公開
Data Provider (Database): 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
https://irdb.nii.ac.jp
Original Data Provider (Database): 北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ