文献

J-GLOBAL ID：201702273745104909   整理番号：17A0267651

関数行列とその積分の高次論理形式化【JST・京大機械翻訳】

Higher-order Logic Formalization of Function Matrix and its Calculus

著者 (6件)： Yang Xiumei (Beijing Key Laboratory of Light Industrial Robot and Safety Verification,College of Information Engineering, Capital Normal University) ,  Guan Yong (Beijing Key Laboratory of Light Industrial Robot and Safety Verification,College of Information Engineering, Capital Normal University) ,  Shi Zhiping (Beijing Key Laboratory of Light Industrial Robot and Safety Verification,College of Information Engineering, Capital Normal University) ,  Wu Aixuan (Beijing Key Laboratory of Light Industrial Robot and Safety Verification,College of Information Engineering, Capital Normal University) ,  Zhang Qianying (Beijing Key Laboratory of Light Industrial Robot and Safety Verification,College of Information Engineering, Capital Normal University) ,  Zhang Jie (College of Information Science & Technology,Beijing University of Chemical Technology)
資料名： Jisuanji Kexue  (Jisuanji Kexue)
巻： 43  号： 11  ページ： 24-29  発行年： 2016年 
JST資料番号： C2530A  ISSN： 1002-137X  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 中国語 (ZH)

抄録/ポイント： 関数行列はダイナミックシステムのモデリングと解析に広く使用されている。従来の関数行列解析には,鉛筆演算,数値計算,および記号推定の方法が採用されており,これらの方法は正確で正確な結果を提供することができない。高次論理定理は,信頼性の高い形式的検証法として,上記の欠点を克服することができる。本論文では,関数ベクトルと関数行列とそれらの連続性,微分,積分の形式的定義と関連特性の論理的推論を証明するために,高次論理定理証明器HOL4において,関数ベクトルと関数行列に関する理論を定式化した。モデル関数の形式的応用のために,ロボット運動学における回転行列微分方程式の形式的検証を与えた。Data from the ScienceChina, LCAS. Translated by JST【JST・京大機械翻訳】

シソーラス用語： 連続性 ,  モデリング ,  定式化 ,  信頼性 ,  微分 ,  演算 ,  *積分 ,  微分方程式 ,  ベクトル ,  動的系 ,  定理証明 ,  数値計算
準シソーラス用語： 回転行列 ,  ロボット運動学 ,  形式的検証 , 【Automatic Indexing@JST】

著者キーワード (4件)： Function matrix ,  Calculus ,  Formal verification ,  Higher-order logic theorem proving

分類 (2件)： システム設計・解析  (IA02030D) ,  システム・制御理論一般  (IA02010H)

タイトルに関連する用語 (4件)： 関数 ,  行列 ,  積分 ,  論理形式