Theory of relational calculus for formal verification of mathematics and software programs.

2019 Fiscal Year Final Research Report

• Project/Area Number: 17K05346
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Foundations of mathematics/Applied mathematics
• Research Institution: Kyushu University
• Principal Investigator: Mizoguchi Yoshihiro 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
• Project Period (FY): 2017-04-01 – 2020-03-31
• Keywords: 数理論理学 / 関係計算 / 形式証明 / 形式手法 / モデル検査 / 圏論のモナドの形式化

Outline of Final Research Achievements

The purpose of our research is to construct a foundamental theory of mathematical logic and discrete mathematics, which supports the reliable software developments. In particular, we use mathematical proofs using relational calculations. We consider formal proofs that can be automatically verified by a computer. Basic axioms of relational calculus and axioms of the Dedekind category are formalized using the Coq proof assistant system. Further, we implemented tactics of accumulating basic lemmas and automatic proofs for a combination of morphisms. Our results including formalized basic lemmas of the Coq system have been released with an introductory document, as well as the certificate collections with concrete examples.

Free Research Field

理論計算機科学

Academic Significance and Societal Importance of the Research Achievements

本研究は高信頼ソフトウェア開発の基礎となる数理論理学や離散数学、特に計算機による自動検証可能な形式証明を意識した関係計算による証明を用いた数学体系を拡げることである。
近年の計算機能力、および、定理証明支援系ソフトウェアの進歩により、数値計算、数式処理計算のみならず、論理計算についても自動検証可能になり、四色定理、ケプラー予想など,計算機でしか厳密に検証出来ない数学定理の証明も発表されるようになっている。このような背景のもと本研究では論理計算を内包する関係計算に主眼を置いた数学理論の再構築、形式証明データベースの作成など、自動検証可能な数学理論体系を提案するものである。