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

• 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
• Project Status: Completed (Fiscal Year 2015)
• Budget Amount: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000); Fiscal Year 2015: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2014: ¥2,210,000 (Direct Cost: ¥1,700,000、Indirect Cost: ¥510,000); Fiscal Year 2013: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
• 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.

Research Products

• [Int'l Joint Research] Ｅｃｏｌｅ Ｐｏｌｙｔｅｑｕｅ(フランス)
• [Int'l Joint Research] 清華大学(中国)
• [Presentation] Decidability by two semi-algorithms（口頭発表） (2016)
  • Author(s): Mizuhito Ogawa
  • Organizer: 15th International Workshop on Proof, Computation, Complexity
  • Place of Presentation: ミュンヘン、ドイツ
  • Year and Date: 2016-05-05
  • Int'l Joint Research
• [Presentation] Confluence of Layered Rewrite Systems (2015)
  • Author(s): Jiaxiang Liu, Jean-Pierre Jouannaud, Mizuhito Ogawa
  • Organizer: 24th Computer Science Logic 2015 (CSL 2015), LIPICS Vol.41, pp.423-440.
  • Place of Presentation: ベルリン、ドイツ
  • Year and Date: 2015-09-07
  • Int'l Joint Research
• [Presentation] Non-E-overlapping, weakly shallow, and non-collapsing TRSs are confluent (2015)
  • Author(s): 酒井正彦、大山口通夫、小川瑞史
  • Organizer: 第25回 自動推論国際会議 (CADE-25)
  • Place of Presentation: ベルリン、ドイツ
  • Year and Date: 2015-08-01 – 2015-08-07
• [Presentation] Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent (2015)
  • Author(s): Masahiko Sakai, Michio Oyamaguchi, Mizuhito Ogawa
  • Organizer: 25th International Conference on Automated Deduction (CADE-25) 2015, Springer LNAI 9195, pp.111-126.
  • Place of Presentation: ベルリン、ドイツ
  • Year and Date: 2015-08-01
  • Int'l Joint Research
• [Presentation] Non-E-overlapping and weakly shallow TRSs are confluent（口頭発表） (2014)
  • Author(s): 酒井正彦、大山口通夫、小川瑞史
  • Organizer: 第3回 合流性ワークショップ (IWC 2014)
  • Place of Presentation: ウィーン、オーストリア
  • Year and Date: 2014-07-13
• [Remarks] AFP-Open (Isabelle/HOL形式証明アーカイブ） Open induction
  • URL: http://www.isa-afp.org/devel-entries/Open_Induction.shtml