论文部分内容阅读
在机器人迅速发展的时代,人机协作型机器人安全性问题是人们关注的焦点.机器人逆运动学的建模与求解是决定其安全性的必要因素之一.旋量法是一种机器人逆运动学建模的常用方法,它可以解决传统D-H参数法的奇异性问题.然而,在建模过程中,旋量法会因人为因素或软件系统缺陷导致模型出现漏洞,从而威胁操作人员安全.因此,本文在旋量高阶逻辑定理证明库的基础上,实现了指数积和Paden-Kahan子问题(subprob-R)等数学理论的高阶逻辑表达,在交互式定理证明器HOLLight中对6R型协作型机器人逆运动学建模与求解过程