面向机器人的几何代数高阶逻辑形式化理论

The robot will become the pillar industry of the world, is the focus of competition national technology and industrial fields. The traditional test, simulation verification method because the cases are imperfect, can not fully meet the verification robot high safety requirements, and thus the theorem proving has become the important guarantee means. Geometric algebra is an important achievement of the development of modern mathematics, can be used as a unified mathematical physical description language, is to describe the ideal mathematical theory of robot mechanism. This project research based on higher-order logic modeling, verify the theory and method for robot mechanism in algebraic geometry, higher order logic modeling including geometric algebra space geometric object; expression of geometric algebra and rigid body motion form; robot mechanism of formal analysis and verification method based on geometric algebra. This project will be the development of more theory of higher-order logic program library, forming the motion characteristics of the robot mechanism of formal analysis and verification of tool library, and provide theoretical and technical support for the design and application of safety of our country and international robot.

机器人即将成为世界的支柱产业，是各国科技和工业领域的竞争焦点。传统的测试、模拟等验证方法由于用例的不完备性，不能完全满足机器人高安全性的验证要求，因而定理证明成为了重要的保障手段。几何代数是现代数学发展的重要成果，可以作为数学物理的统一描述语言，是描述机器人机构的理想数学理论。本项目研究基于几何代数的机器人机构学高阶逻辑建模、验证理论和方法，包括几何代数空间的高阶逻辑建模；几何代数中几何对象以及刚体运动的形式化表达；基于几何代数的机器人机构运动特性形式化分析与验证方法。本项目将研发以上理论的高阶逻辑程序库，形成机器人机构运动特性的形式化分析与验证工具库，为我国及国际机器人的安全设计与应用提供理论和技术保障。

机器人已经成为当今世界的支柱产业，也是各国科技和工业领域的竞争焦点。传统的测试、模拟等验证方法由于用例的不完备性，不能完全满足机器人高安全性的验证要求，因而定理证明成为了重要的保障手段。几何代数是现代数学发展的重要成果，可以作为数学物理的统一描述语言，是描述机器人机构的理想数学理论。本项目研究基于几何代数的机器人机构学高阶逻辑建模、验证理论和方法，包括几何代数空间的高阶逻辑建模；几何代数中几何对象以及刚体运动的形式化表达；基于几何代数的机器人机构运动特性形式化分析与验证方法。本项目将研发以上理论的高阶逻辑程序库，形成机器人机构运动特性的形式化分析与验证工具库，为我国及国际机器人的安全设计与应用提供理论和技术保障。.几何代数是一个新兴的数学分支，它对代数与几何进行了融合与拓展，为代数理论赋予了“形”的特征，为几何理论提供了“数”的内涵，被誉为统一的数学物理描述语言。形式化几何代数能够提供更加统一和通用的形式化描述基础，是形式化数学和自动定理证明的重要进展。课题组研发的几何代数形式化定理库于2018年11月被国际最著名的定理证明系统之一HOL Light官方收录为新增形式化理论体系。这是中国研究机构的研究成果首次被HOL Light系统收录，此次发布的定理库也是国际上第一个完备的几何代数高阶逻辑形式化表示理论。该项工作共历时六年，包含33个数学定义和343个数学定理的高阶逻辑表示和机器证明。.2016年-2019年课题组按照基金计划内容展开研究，取得了良好的进展，发表学术论文17篇，其中SCI期刊论文6篇，软件学报、电子学报论文3篇、EI检索论文1篇、国际机器人顶级学术会议论文1篇；申请国家发明专利2项，获得国家发明专利授权1项；获得北京市科学技术二等奖1项（排名第一）；出版学术专著1部（几何代数的形式化与初步应用，科学出版社，2019.11，第一完成人，ISBN 978-7-03-063033-9）。