论文部分内容阅读
平面并联机构运动学分析是机构学研究热点之一,平面并联机构运动学模型的构建和求解的错误会给整个系统带来灾难性损失.传统运动学分析方法难以保证模型的完备性和求解的正确性.而基于高阶逻辑的定理证明方法可以弥补传统分析方法的不足.本文以几何代数、共形几何代数的高阶逻辑表达为基础,在HOL Light定理证明器中形式化描述平面并联机构的相关数学理论,建立正向运动学高阶逻辑模型,验证正向运动学的一般性求解算法,从而确保了平面并联机构运动学分析的正确性和分析求解方法的可靠性.