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

• 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
• Project Status: Completed (Fiscal Year 2019)
• Budget Amount: ¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000); Fiscal Year 2019: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2018: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2017: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
• Keywords: 数理論理学 / 関係計算 / 形式証明 / 形式手法 / モデル検査 / 圏論のモナドの形式化 / Wangタイル / パターン生成 / Coq / 情報数理 / ファジィ関係データベース / 数学基礎論

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.

Academic Significance and Societal Importance of the Research Achievements

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

Research Products

• [Journal Article] A linear algorithm for Brick Wang tiling (2019)
  • Author(s): Derouet-Jourdan, A., Kaji, S. & Mizoguchi, Y.
  • Journal Title: Japan J. Indust. Appl. Math. Volume: 36 Issue: 3 Pages: 749-761
  • DOI: 10.1007/s13160-019-00369-z
  • NAID: 210000187413
  • Peer Reviewed
• [Journal Article] 論理と計算について考えた人たち, 数学セミナー, 2019年1月号, pp.57-61, 2018.12. (2018)
  • Author(s): 溝口佳寛
  • Journal Title: 数学セミナー Volume: 58 Pages: 57-61
• [Journal Article] Class dependency of fuzzy relational database using relational calculus and conditional probability (2018)
  • Author(s): M.D.Akbar Y.Mizoguchi, Adiwijaya
  • Journal Title: Journal of Phyusics: Conf. Ser. Volume: 971 Pages: 012001-012001
  • DOI: 10.1088/1742-6596/971/1/012001
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Presentation] Relational T-algebra and the category of topological spaces (2018)
  • Author(s): Y. Mizoguchi
  • Organizer: Workshop on Logic, Algebra and Category Theory: LAC2018
  • Int'l Joint Research / Invited
• [Presentation] 位相空間の圏と同型な関係T代数の圏について (2018)
  • Author(s): 阿川真士, 溝口佳寛
  • Organizer: 日本数学会2018年度年会
• [Presentation] Class dependency of fuzzy relational database using relational calculus and conditional probability (2017)
  • Author(s): M.D.Akbar Y.Mizoguchi, Adiwijaya
  • Organizer: The Internatiaonal Conference on Data and Information Science, ICoDIS2017
  • Int'l Joint Research
• [Presentation] Formal Equivalence Classes Model of Fuzzy Relational Databases Using Relational Calculus (2017)
  • Author(s): M.D.Akbar, Y.Mizoguchi
  • Organizer: International Conference on Applied Computer and Communication Technologies (ComCom)
  • Int'l Joint Research
• [Remarks] 関係計算の形式化を用いた数学とソフトウェア検証のための理論構築
  • URL: https://imi.kyushu-u.ac.jp/~ym/web/
• [Remarks] Workshop on Logic, Algebra and Category Theory
  • URL: http://www2.math.kyushu-u.ac.jp/~lac2018/