共形几何代数与机器人运动学的形式化

摘要 共形几何代数作为一种新的几何表示和计算系统，它为经典几何提供了简洁、直观和统一的齐性代数框架，目前在现代科技的各个领域有很广泛的应用，但是利用共形几何代数进行计算和建模分析的传统方法如数值计算方法和符号方法存在计算不精确等问题.定理证明方法是一种验证系统正确性的严密的形式化方法.在高阶逻辑证明工具HOL-Light中建立共形几何代数系统的形式化模型，提出基本代数运算、几何体表示和几何变换等理论的相关逻辑定义和性质证明.最后为了说明共形几何代数形式化的有效性和实用性，基于共形几何逻辑模型对5R串联机器人的运动学反解进行形式化建模并提出验证方案