Discovery and proof of inductive theorems with multi-context reasoning systems for algebraic software

• Project/Area Number: 16K00090
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Hokkaido University
• Principal Investigator: Kurihara Masahito 北海道大学, 情報科学研究科, 教授 (50133707)
• Research Collaborator: Sato Haruhiko
• Project Period (FY): 2016-04-01 – 2019-03-31
• Project Status: Completed (Fiscal Year 2018)
• Budget Amount: ¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000); Fiscal Year 2018: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000); Fiscal Year 2017: ¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000); Fiscal Year 2016: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
• Keywords: 帰納的定理 / 定理自動証明 / 定理自動発見 / 補題生成 / 多重文脈型推論 / 代数的ソフトウェア / 項書換え系 / 帰納的定理自動証明 / 書換え帰納法 / 多重文脈推論 / 帰納的定理証明 / 補助定理 / 定理発見 / 発散鑑定 / 仕様記述・検証

Outline of Final Research Achievements

This research project uses new ideas of system structure called the multi-context reasoning system to apply them to the grand plan to develop technologies for automatic, efficient discovery and proof of a kind of mathematical theorems called inductive theorems, which play important roles in computer science and technology. To attain this purpose, we have developed software systems with new top-down and bottom-up methods for automatic generation of lemmas required in the proof of the main theorems. In addition, we have empirically shown the applicability of this technology in the field of the verification of correctness of algebraic software in software engineering.

Academic Significance and Societal Importance of the Research Achievements

ソフトウェア工学の理論的基礎分野では，作成したソフトウェアの正しさを機械的に確認する技術が重要視されている。そのため代数的にソフトウェアの仕様を記述して実装する技術が考案されており，そこではソフトウェアの正しさを数学的な帰納的定理の証明に帰着させ，それを計算機により自動的に証明するアプローチを採っている。本研究成果はそのような技術開発に対して有益な知見を提供する点に学術的意義があるとともに，最終的にはソフトウェアの正しさの保証を通じて，安心・安全な情報社会の実現に寄与し得る点に社会的意義が認められる。

Research Products

• [Journal Article] Multi-Context Automated Lemma Generation for Term Rewriting Induction with Divergence Detection (2019)
  • Author(s): Chengcheng Ji, Masahito Kurihara, Haruhiko Sato
  • Journal Title: IEICE Transactions on Information and Systems Volume: E102-D Pages: 223-238
  • NAID: 130007586588
  • Peer Reviewed
• [Presentation] Automated proof and discovery of inductive thorems with rewriting induction over multi-context reasoning systems: state-of-the-art technologies and perspectives (2018)
  • Author(s): Masahito Kurihara, Haruhiko Sato, ChengCheng Ji
  • Organizer: World Congress on Engineering and Computer Science 2018 (WCECS 2018)
  • Int'l Joint Research
• [Presentation] On Usefulness of Syntactically Complex Lemmas in Theory Exploration for Inductive Theorems (2018)
  • Author(s): Haruhiko Sato and Masahito Kurihara
  • Organizer: International MultiConference of Engineers and Computer Scientists
  • Int'l Joint Research
• [Presentation] Discovering Inductive Theorems Using Rewriting Induction (2016)
  • Author(s): Haruhiko Sato, Masahito Kurihara
  • Organizer: IEEE International Conference on Systems, Man, and Cybernetics (SMC 2016)
  • Place of Presentation: Budapest (Hungary)
  • Year and Date: 2016-10-09
  • Int'l Joint Research
• [Presentation] Lazy Evaluation Schemes for Efficient Implementation of Multi-Context Algebraic Reasoning Systems (2016)
  • Author(s): Chengcheng Ji, Masahito Kurihara
  • Organizer: Computational Logic in the Alps (CLA 2016)
  • Place of Presentation: Obergurgl (Austria)
  • Year and Date: 2016-09-05
  • Int'l Joint Research