主 题: 信息系列讨论班-工程数学的形式化
报告人: 施智平 教授 (首都师范大学)
时 间: 2017-09-20 13:00-15:00
地 点: 理科1号楼1303
Abstract: 工程数学理论的形式化是应用系统形式化建模与验证的基础。本报告介绍首都师范大学形式化方法研究组在工程数学形式化方面的研究进展,包括复数、矩阵、线性空间、傅里叶变换、gauge积分、分数阶微积分等数学理论的形式化,在HOL定理证明器中开发了相应的定理库,其中复数、gauge积分定理库已开源给剑桥大学HOL4系统发布。近年来针对机器人的发展需求,研究开发了机器人数学基础——旋量代数和几何代数理论的高阶逻辑形式化,并研究机器人运动学的形式化建模与验证方法。