|
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/13676
|
| Title: | 形式証明の理論依存性解析とその計算可能証明発見への応用 |
| Other Titles: | Dependecy analysis on formal proofs and its applications on discovery of computational proofs |
| Authors: | 小川, 瑞史 |
| Authors(alternative): | Ogawa, Mizuhito |
| Keywords: | 形式証明
計算的意味
項書換え系
合流性
構成的証明 |
| Issue Date: | 3-Jun-2016 |
| Abstract: | 古典的存在証明からの計算的意味の抽出について、未解決問題を含む決定問題の難問に対する証明構造のケーススタディを行った。「右線形かつ強無曖昧な項書換え系は合流性を持つ」(RTA open problem 58)は、可算選択公理を用いた停止順序の存在は証明できるが、具体的な順序の構成が困難なため未解決問題である。順序の構成条件の精査と、有限リダクショングラフによる構成的証明に基づき、二つの異なる新たな部分クラスに対し、肯定的結果を得た。また、最近、散見される決定問題の難問に対する二つのyes/noをそれぞれ決定する準アルゴリズムを並行させる証明手法について、一般化の考察を進めた。 : The extraction of computational content from classical existence proof has been investigated by case study on difficult problems. One is an open problem in rewriting "a right-linear and strongly nonoverlapping term rewriting system is confluent" (RTA open problem 58). If confluent, the existence of a termination ordering is proved by the countable choice axiom. However, due to the difficulty of actual construction of the termination ordering, it remains still open. We showed positive answers to two new subclasses; one by investigating possible termination ordering structures, and another by a new method based on the finiteness of a reduction graph. As an alternative to the extraction of computational content, we investigate recent decidability proofs consisting of two semi-algorithms, of which one tries to say "yes", and another tries to say "no". They work concurrently, and the result will be eventually found by either of them. Their generalization has been observed. |
| Description: | 挑戦的萌芽研究
研究期間：2013～2015
課題番号：25540003
研究者番号：40362024
研究分野：形式手法 |
| Language: | jpn |
| URI: | http://hdl.handle.net/10119/13676 |
| Appears in Collections: | 2015年度 (FY 2015)
|
Files in This Item:
| File |
Description |
Size | Format |
|---|
| 25540003seika.pdf | | 86Kb | Adobe PDF | View/Open |
|
All items in DSpace are protected by copyright, with all rights reserved.
|
