文献

J-GLOBAL ID：201702226754929053   整理番号：17A0066214

直列ロボットヤコビ行列の高次論理形式化【JST・京大機械翻訳】

High-order Logic Formalization for Jacobian Matrix of a Serial Robot

著者 (6件)： Yang Xiumei (Beijing Key Laboratory of Electronic System Reliability Technology,College of Information Engineering,Capital Normal University) ,  Shi Zhiping (Beijing Key Laboratory of Electronic System Reliability Technology,College of Information Engineering,Capital Normal University) ,  Wu Aixuan (Beijing Key Laboratory of Electronic System Reliability Technology,College of Information Engineering,Capital Normal University) ,  Guan Yong (Beijing Key Laboratory of Electronic System Reliability Technology,College of Information Engineering,Capital Normal University) ,  Ye Shiwei (College of Information Science and Engineering,Graduate University of Chinese Academy of Sciences) ,  Zhang Jie (College of Information Science & Technology,Beijing University of Chemical Technology)
資料名： Xiaoxing Weixing Jisuanji Xitong  (Xiaoxing Weixing Jisuanji Xitong)
巻： 37  号： 4  ページ： 726-731  発行年： 2016年 
JST資料番号： C2136A  ISSN： 1000-1220  CODEN： XWJXEH  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 中国語 (ZH)

抄録/ポイント： ロボットヤコビ行列はロボットの運動性能を記述する重要なパラメータであり、ロボットヤコビ行列の記述、解法及び分析の正確性と信頼性を保証することは非常に重要である。しかし,従来の数値計算と計算機代数記号法は,100%の正確さと完全な解析と検証を提供することができない。高次論理定理に基づき,高信頼性と証明の完全性を証明し,運動学的スクリューと直列ロボットの正の運動学指数の数学的基礎に基づいて,直列ロボットの正方向運動学の形式的モデルを,高次論理定理証明器HOL4において確立した。スクリュー法によって記述される速度JACOBI行列を,形式的に解析し,検証した。最後に,STANFORDロボットのJACOBI行列の形式的解析を通して,本論文は形式的作業の実用性と正当性を示した。Data from the ScienceChina, LCAS. Translated by JST【JST・京大機械翻訳】

シソーラス用語： *Jacobi行列 ,  数値計算 ,  完全性 ,  数式処理 ,  定理証明 ,  *ロボット ,  信頼性
準シソーラス用語： 実用性 ,  高信頼性 ,  記号法 ,  正確性 ,  運動性能 , 【Automatic Indexing@JST】

著者キーワード (4件)： roboticjacobian matrix ,  motion screw ,  HOL4 ,  formal verification

分類 (3件)： 計算機網  (JC03000K) ,  信頼性  (KB04040H) ,  数値計算  (JE02000J)

タイトルに関連する用語 (4件)： 直列 ,  ロボット ,  ヤコビ行列 ,  論理形式