|
JAIST Repository >
School of Information Science >
Grants-in-aid for Scientific Research Papers >
FY 2012 >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/10119/11371
|
| Title: | 非決定計算のための項書き換え理論 |
| Other Titles: | Rewriting Techniques for Non-Deterministic Computation |
| Authors: | 廣川, 直 |
| Authors(alternative): | Hirokawa, Nao |
| Keywords: | 項書換え
合流性
完備化
戦略 |
| Issue Date: | 31-May-2013 |
| Abstract: | 本研究では関数型プログラムや定理証明システムの計算モデルである項書換えシステムに対し、その基礎理論を相対停止性という性質をもとに再考した。その研究成果として、合流性に関する主要二定理（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. |
| Description: | 研究種目：若手研究（Ｂ）
研究期間：2010～2012
課題番号：22700009
研究者番号：50467122
研究分野：項書換え
科研費の分科・細目：情報学・情報学基礎 |
| Language: | jpn |
| URI: | http://hdl.handle.net/10119/11371 |
| Appears in Collections: | 2012年度 (FY 2012)
|
Files in This Item:
| File |
Description |
Size | Format |
|---|
| 22700009seika.pdf | | 200Kb | Adobe PDF | View/Open |
|
All items in DSpace are protected by copyright, with all rights reserved.
|
