Toward a formal proofs and automated verifications of discrete mathematics

离散数学的形式化证明和自动验证

• 批准号: 25610034
• 负责人: MIZOGUCHI Yoshihiro
• 金额: $ 2.33万
• 依托单位: Kyushu University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Challenging Exploratory Research
• 财政年份: 2013
• 资助国家: 日本
• 起止时间: 2013-04-01 至 2015-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-25610034/
• 关键词: 数理論理学; 数学の形式化; 検証可能証明; ソフトウェア検証; 離散数学; 計算理論; 形式証明; 定理証明検証; Coq; 証明支援系; 定理証明器; 有限オートマトン; Isabelle; Mizar

项目成果

論理と計算セミナー

逻辑与计算研讨会

Formal Proofs for Automata and Sticker Systems

自动机和贴纸系统的形式证明

• DOI: 10.1109/candar.2013.100
• 发表时间: 2014
• 期刊: Proc. of 1st International Workshop on Computing and Networking
• 作者: H.Tanaka;I.Sakashita;S.Inokuchi;Y.Mizoguchi
• 通讯作者: Y.Mizoguchi

A Mathematica module for Conformal Geometric Algebra

共形几何代数的 Mathematica 模块

• 发表时间: 2014
• 作者: M.Kondo;T.Matsuo
• 通讯作者: T.Matsuo

Theory of Automata, Abstraction and Applications

自动机理论、抽象及其应用

• 发表时间: 2014
• 期刊: A Mathematical Approach to Research Problems of Science and Technology, Mathematis for Industry
• 作者: Y.Mizoguchi

組合せ数学セミナー

组合数学研讨会