摘要
平面并联机构运动学分析是机构学研究热点之一,平面并联机构运动学模型的构建和求解的错误会给整个系统带来灾难性损失.传统运动学分析方法难以保证模型的完备性和求解的正确性.而基于高阶逻辑的定理证明方法可以弥补传统分析方法的不足.本文以几何代数、共形几何代数的高阶逻辑表达为基础,在HOL Light定理证明器中形式化描述平面并联机构的相关数学理论,建立正向运动学高阶逻辑模型,验证正向运动学的一般性求解算法,从而确保了平面并联机构运动学分析的正确性和分析求解方法的可靠性.
Kinematics analysis of parallel mechanisms is one of the hot issues in the research.The construction of the kinematics model of the planar parallel mechanism and the error of the solution will bring catastrophic losses to the whole system.Traditional method of kinematics analysis cannot fully ensure the completeness of the model and the correctness of the solution.Theorem proving method can make up for the shortcomings of traditional analysis methods.Firstly,based on the high order logic expression of geometric algebra and conformal geometric algebra,this paper formally describe the related mathematical theories of planar parallel mechanisms in HOL Light,then establish a higher order logic model of forward kinematics,finally formally analyze and verify a general algorithm for forward kinematics.The ultimate goal is to ensure the correctness of kinematics analyses of planar parallel mechanisms and analyze the reliability of the solution method.
作者
陈琦
王国辉
张倩颖
施智平
陈善言
关永
CHEN Qi;WANG Guo-hui;ZHANG Qian-ying;SHI Zhi-ping;CHEN Shan-yan;GUAN Yong(Beijing Engineering Research Center of High Reliable Embedded System,Capital Normal University,Beijing 100048,China)
出处
《小型微型计算机系统》
CSCD
北大核心
2020年第5期925-931,共7页
Journal of Chinese Computer Systems
基金
国家重点研发计划项目(2017YFB1301100)资助
国家自然科学基金项目(61876111,61572331,61602325,61877040)资助
北京市教委科技计划一般项目(KM20190028005)资助
科技创新服务能力建设-基本科研业务费(科研费)项目(006195305000)资助.
