並列タイトル等Dependecy analysis on formal proofs and its applications on discovery of computational proofs
一般注記古典的存在証明からの計算的意味の抽出について、未解決問題を含む決定問題の難問に対する証明構造のケーススタディを行った。「右線形かつ強無曖昧な項書換え系は合流性を持つ」(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
研究分野：形式手法
identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/13676
一次資料へのリンクURLhttps://dspace.jaist.ac.jp/dspace/bitstream/10119/13676/1/25540003seika.pdf
連携機関・データベース国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
提供元機関・データベース北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ