|
JAIST Repository >
b. 情報科学研究科・情報科学系 >
b50. 科学研究費助成事業研究成果報告書 >
2015年度 >
このアイテムの引用には次の識別子を使用してください:
http://hdl.handle.net/10119/13676
|
| タイトル: | 形式証明の理論依存性解析とその計算可能証明発見への応用 |
| その他のタイトル: | Dependecy analysis on formal proofs and its applications on discovery of computational proofs |
| 著者: | 小川, 瑞史 |
| 著者（別表記）: | Ogawa, Mizuhito |
| キーワード: | 形式証明
計算的意味
項書換え系
合流性
構成的証明 |
| 発行日: | 3-Jun-2016 |
| 抄録: | 古典的存在証明からの計算的意味の抽出について、未解決問題を含む決定問題の難問に対する証明構造のケーススタディを行った。「右線形かつ強無曖昧な項書換え系は合流性を持つ」(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. |
| 記述: | 挑戦的萌芽研究
研究期間：2013～2015
課題番号：25540003
研究者番号：40362024
研究分野：形式手法 |
| 言語: | jpn |
| URI: | http://hdl.handle.net/10119/13676 |
| 出現コレクション: | 2015年度 (FY 2015)
|
このアイテムのファイル:
| ファイル |
記述 |
サイズ | 形式 |
|---|
| 25540003seika.pdf | | 86Kb | Adobe PDF | 見る/開く |
|
当システムに保管されているアイテムはすべて著作権により保護されています。
|
