对机器人碰撞检测方法进行形式化验证, 以球体和胶囊体形式化模型为基础, 构建基本几何体单元之间最短距离和机器人碰撞的高阶逻辑模型, 证明其相关属性及碰撞条件, 建立机器人碰撞检测方法基础定理库, 为多机系统碰撞检测算法可靠性与稳定性的验证提供技术支撑和验证框架...基于以上分析, 在设计实现一个机器人碰撞检测算法时, 如何保障它的正确性和可靠性?...通过形式化技术, 构建机器人几何体单元之间的最短距离和机器人碰撞模型, 形式化验证其相关属性以及机器人碰撞条件, 建立机器人碰撞检测方法定理证明库, 为实现多机系统的碰撞检测算法的可靠性与稳定性验证提供技术支撑和方法参考...针对该问题, 本文在定理证明器中建立了机器人碰撞检测方法基础定理库并对机器人碰撞检测方法进行了形式化建模与验证, 为实现多机系统碰撞检测算法的可靠性和稳定性验证提供了技术支撑和验证框架.2.背景知识HOL-Light..., 通常可将其关节、连杆、末端执行器等基本几何体单元简化为长方体、胶囊体、球体等形状, 进而通过利用计算基本几何体简化模型的碰撞检测方法, 达到减少计算量的目的.