Dependecy analysis on formal proofs and its applications on discovery of computational proofs

2015 Fiscal Year Final Research Report

• Project/Area Number: 25540003
• Research Category: Grant-in-Aid for Challenging Exploratory Research
• Allocation Type: Multi-year Fund
• Research Field: Theory of informatics
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: Ogawa Mizuhito 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
• Research Collaborator: Christian Sternagel インスブルック大学, ポスドク
• Project Period (FY): 2013-04-01 – 2016-03-31
• Keywords: 形式証明 / 計算的意味 / 項書換え系 / 合流性 / 構成的証明

Outline of Final Research Achievements

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.

Free Research Field

形式手法