掃一掃
關注中圖網
官方微博
>
哈密頓力學理論的形式化與機器人動力學形式化分析
本類五星書更多>
-
>
貨幣大歷史:金融霸權與大國興衰六百年
-
>
(精)方力鈞作品圖錄
-
>
《藏書報》2021合訂本
-
>
(精)中國當代書畫名家作品集·范碩:書法卷+繪畫卷(全2卷)
-
>
(噴繪樓閣版)女主臨朝:武則天的權力之路
-
>
書里掉出來一只狼+狼的故事-全2冊
-
>
奇思妙想創意玩具書(精裝4冊)
哈密頓力學理論的形式化與機器人動力學形式化分析 版權信息
- ISBN：9787030532046
- 條形碼：9787030532046 ; 978-7-03-053204-6
- 裝幀：一般膠版紙
- 冊數：暫無
- 重量：暫無
- 所屬分類：
哈密頓力學理論的形式化與機器人動力學形式化分析 內容簡介
本書系統深入地研究了辛幾何理論、哈密頓動力學的公理化體系，并以四自由度串聯機器人為例，研究了基于哈密頓動力學系統的形式化分析與驗證方法的應用，為機器人動力學的安全設計提供了形式化驗證理論和技術手段。全書主要內容包括：哈密頓模型的幾何基礎——辛流形空間的形式化、哈密頓模型和拉格朗日模型的勒讓德映射關系的形式化、哈密頓方程的形式化和機器人動力學的形式化建模與分析。內容涉及交互式定理證明、機器人、形式化驗證等人工智能領域。 本書可作為機器定理證明、機器人學、形式化方法、理論計算機科學及軟件工程等領域科研人員和工程技術人員的參考書，也可作為高等院校相關專業高年級本科生和研究生的學習用書。
哈密頓力學理論的形式化與機器人動力學形式化分析 目錄
目錄
序
前言
第1章緒論1
1.1研究意義1
1.2研究現狀3
1.2.1分析力學3
1.2.2形式化數學4
1.2.3機器人形式化驗證6
1.3主要內容和貢獻7
1.3.1主要研究內容7
1.3.2主要貢獻9
1.4本書組織結構9
1.5交互式定理證明器HOL Light10
參考文獻11
第2章辛幾何形式化16
2.1辛向量空間的形式化16
2.1.1辛空間與歐氏空間的異同17
2.1.2辛內積形式化定義與性質形式化證明17
2.1.3辛向量空間的形式化建模與驗證19
2.1.4辛空間基底性質形式化證明20
2.2辛變換矩陣的形式化23
2.2.1辛變換的形式化定義及其判定定理的證明策略23
2.2.2分塊矩陣相關理論的形式化25
2.2.3單位辛矩陣性質的形式化29
2.3辛群的形式化30
2.3.1辛群形式化建模31
2.3.2辛群判定定理及其證明策略32
2.4本章小結36
參考文獻36
第3章勒讓德變換形式化38
3.1勒讓德變換原理38
3.2一元函數勒讓德變換形式化模型及固有屬性的證明策略41
3.3多元函數勒讓德變換的形式化建模44
3.3.1完全勒讓德變換的形式化模型及固有屬性證明策略44
3.3.2部分勒讓德變換的形式化模型及固有屬性證明策略49
3.4本章小結58
參考文獻58
第4章哈密頓力學系統形式化59
4.1哈密頓函數的形式化建模60
4.1.1構造力學函數數據類型60
4.1.2從拉格朗日函數到哈密頓函數形式化模型的構建63
4.1.3哈密頓函數物理意義的形式化驗證67
4.2哈密頓正則方程的形式化建模70
4.2.1哈密頓函數微分相關定理形式化描述70
4.2.2哈密頓正則方程的形式化建模及證明策略73
4.3泊松括號與泊松定理的形式化87
4.3.1泊松括號形式化描述及其性質形式化證明87
4.3.2泊松定理形式化驗證94
4.4本章小結96
參考文獻96
第5章串聯機器人哈密頓動力學形式化建模與驗證98
5.1SCARA四自由度機器人哈密頓函數形式化建模98
5.2SCARA四自由度機器人哈密頓正則方程形式化建模105
5.3機器人動力學形式化建模與驗證過程111
5.4本章小結123
參考文獻123
第6章總結與展望125
6.1主要工作和創新點125
6.2下一步工作與展望126
序
前言
第1章緒論1
1.1研究意義1
1.2研究現狀3
1.2.1分析力學3
1.2.2形式化數學4
1.2.3機器人形式化驗證6
1.3主要內容和貢獻7
1.3.1主要研究內容7
1.3.2主要貢獻9
1.4本書組織結構9
1.5交互式定理證明器HOL Light10
參考文獻11
第2章辛幾何形式化16
2.1辛向量空間的形式化16
2.1.1辛空間與歐氏空間的異同17
2.1.2辛內積形式化定義與性質形式化證明17
2.1.3辛向量空間的形式化建模與驗證19
2.1.4辛空間基底性質形式化證明20
2.2辛變換矩陣的形式化23
2.2.1辛變換的形式化定義及其判定定理的證明策略23
2.2.2分塊矩陣相關理論的形式化25
2.2.3單位辛矩陣性質的形式化29
2.3辛群的形式化30
2.3.1辛群形式化建模31
2.3.2辛群判定定理及其證明策略32
2.4本章小結36
參考文獻36
第3章勒讓德變換形式化38
3.1勒讓德變換原理38
3.2一元函數勒讓德變換形式化模型及固有屬性的證明策略41
3.3多元函數勒讓德變換的形式化建模44
3.3.1完全勒讓德變換的形式化模型及固有屬性證明策略44
3.3.2部分勒讓德變換的形式化模型及固有屬性證明策略49
3.4本章小結58
參考文獻58
第4章哈密頓力學系統形式化59
4.1哈密頓函數的形式化建模60
4.1.1構造力學函數數據類型60
4.1.2從拉格朗日函數到哈密頓函數形式化模型的構建63
4.1.3哈密頓函數物理意義的形式化驗證67
4.2哈密頓正則方程的形式化建模70
4.2.1哈密頓函數微分相關定理形式化描述70
4.2.2哈密頓正則方程的形式化建模及證明策略73
4.3泊松括號與泊松定理的形式化87
4.3.1泊松括號形式化描述及其性質形式化證明87
4.3.2泊松定理形式化驗證94
4.4本章小結96
參考文獻96
第5章串聯機器人哈密頓動力學形式化建模與驗證98
5.1SCARA四自由度機器人哈密頓函數形式化建模98
5.2SCARA四自由度機器人哈密頓正則方程形式化建模105
5.3機器人動力學形式化建模與驗證過程111
5.4本章小結123
參考文獻123
第6章總結與展望125
6.1主要工作和創新點125
6.2下一步工作與展望126
展開全部
哈密頓力學理論的形式化與機器人動力學形式化分析 節選
第1章緒論 1.1研究意義 動力學是經典物理學的基石之一，主要研究能量、力以及它們與物體的平衡、變形或運動的關系，同時也是很多數學理論的發源地。動力學問題在自然界和工程實踐中無處不在，是許多工程學科的理論基礎。諸如，航空航天、機器人、火車、武器等所有與運動和力相關的學科和工業都以動力學為基礎[1]。 動力學主要包括牛頓力學、拉格朗日力學和哈密頓力學三個體系。牛頓力學又稱矢量力學，求解時需已知所有作用力的大小、方向以及作用點與剛體質心的位置關系，因此很難建模復雜的動力學系統。拉格朗日力學則是將力學體系從以力為基本概念的矢量力學形式，改變為以能量為基本概念的標量分析力學形式，奠定了分析力學的基礎，為把力學理論推廣應用到物理學其他領域開辟了道路。哈密頓力學研究以 “正則變量 ”描述力學系統的運動規律，該理論體系能夠發展出多種變換理論和積分方法，并在其他物理學諸如電磁波、熱擴散、量子力學和相對論等重要理論領域均有廣泛應用，同時架起了從經典力學到近代物理學的橋梁。 關于動力學問題的研究，通常通過分析、簡化、抽象成物理模型，再建立動力學方程，即動力學建模，然后分析動力學方程的解及其性質，*后通過工程實現成為動力學系統。基于以上分析，在設計實現一個經典的動力學系統時，如何保障它的動力學建模、分析求解和設計實現的正確性和可靠性呢？傳統的動力學建模與分析方法主要包括紙筆演算、數值計算和計算機代數系統。紙筆演算的方法耗時耗力，容易引入人為錯誤 [2]；計算機數值計算方法指利用計算機軟件進行動力學的數值計算，這樣的軟件包括 Maple、Mathmetica、MATLAB等，但它們只能給出待解問題的數值解，無法給出問題的內在邏輯性質；計算機代數系統比如 Mathmetica能夠高效進行符號代數運算，但是邊界條件、奇異表達簡化方面的處理具有缺陷，此外龐大的符號計算程序也不能排除程序漏洞的存在。 機器人是動力學分析與建模的典型應用，動力學分析是機器人設計和控制的中間橋梁，動力學系統的建模與設計的錯誤可能導致災難性后果。未來的世界是人機共處的世界，機器人在為人類帶來巨大便利的同時也帶來了安全隱患。作為能夠自主運動的機器，機器人故障引發的事故時有發生。 1978年 9月，日本廣島一間工廠的切割機器人將一名值班工人當作鋼板切割造成慘案 [3]；2014年 1月，嫦娥三號玉兔月球車因機構控制出現故障而一度進入休眠 [4]；2015年 7月 1日，一名 22歲的技術工在大眾汽車包納塔爾工廠中被一臺機器人意外傷害致死 [5]； 2016年 11月 18日在第十八屆中國國際高新技術成果交易會，有一臺服務機器人突然發生故障，在沒有指令的前提下打砸展臺玻璃，導致部分展臺破壞，同時有路人受傷 [5，6]。2018年 9月 10日上午，蕪湖經濟開發區內一企業員工在給搬運機器人換刀具時，被突然啟動的機器人夾住，雖被救下送醫，但因傷勢過重，不治身亡。2018年 12月 5日，美國新澤西州的亞馬遜倉庫一個自動化機器人意外刺穿噴霧罐發生一起防熊噴霧泄漏事故，事故導致有 24人被送醫院救治。機器人安全隱患已經成為機器人特別是人機交互機器人應用普及的巨大障礙。人們開始意識到傳統的測試仿真等驗證方法已經不能滿足安全攸關機器人的正確性、安全性驗證要求 [7，8]。 傳統的動力學驗證主要基于測試與仿真方法，由于測試用例與仿真用例受限，測試與仿真方法均無法完全覆蓋所有可能驗證路徑，所以，這些傳統的非完備性驗證手段已經無法滿足安全攸關系統的動力學設計對正確性和安全性的要求。而定理證明形式化驗證方法是一種完備的驗證手段，可以發現傳統方法難于發現的系統缺陷，能夠提高整個系統的安全性和魯棒性驗證質量。 以精確和完備性為主要優點的形式化驗證方法逐漸成為安全攸關系統正確性驗證的重要手段，并在計算機軟硬件驗證中取得成功 [9-11]。近年來，通過形式化驗證技術提升機器人的正確性和安全性逐漸成為研究熱點 [12-14]。一些國際上廣泛認可的安全標準如 IEC61508等將形式化驗證作為達到高安全等級的必選項 [15]。 2011年，美國國家科學基金會提出未來重點支持與人協作機器人的研究工作，而且如何保障與人協作的安全性是研究重點。 2013年，美國政府發布 A Roadmap for U.S. Robotics的白皮書，提出未來五十年發展重點將從因特網轉移到機器人產業 [16]，并**次提出了將形式化驗證方法應用于可靠性、安全性高的機器人領域。因此，把動力學的建模和分析求解過程用數理邏輯表示，并進行嚴格的推理和證明，能夠*大限度地確保系統設計的正確性和可靠性。 數學理論的形式化是指用數理邏輯語言描述或建模數學理論，包括數學概念的形式化定義、定理的形式化表示和證明。使用定理證明的基礎是數學理論的邏輯表示—–形式化數學，國際上主流的定理證明器，如 HOL4[17]、HOL Light[18-20]、 Isabella/HOL [21]、COQ[22]、PVS [23，24]等，均包含了很多基礎的數學理論邏輯程序庫，比如集合論、實分析、向量代數、矩陣理論等，但是目前還沒有與動力學理論相關的公理化體系和定理庫，這就嚴重制約了機器證明在機器人動力系統、導航、自動控制等領域的廣泛應用。 建立動力學的形式化理論定理證明庫是動力系統形式化建模與分析的基礎。基于辛幾何理論的哈密頓力學是系統動力學分析的重要工具之一 [25]。辛幾何理論不僅使求解更方便，而且物理意義清晰明確，在科學研究和工程實踐中得到廣泛應用。 綜上所述，基于形式化數學的定理證明方法在機器人和計算機等安全攸關系統的設計驗證中具有重要的理論意義和應用價值。鑒于此，本書聚焦動力學理論的形式化建模和證明理論的研究，設計實現哈密頓動力學的高階邏輯定理庫，為動力學系統的形式化分析與驗證提供方法和工具支持。 1.2研究現狀 本書主要研究哈密頓動力學的高階邏輯形式化及其在機器人動力學系統形式化驗證中的應用，因此本節將從分析力學、形式化數學以及機器人形式化驗證等幾個方面介紹研究發展的歷程和現狀。 1.2.1分析力學 分析力學以廣義坐標為描述質點系的變量，以*小作用原理為基石，發展了虛位移原理和達朗貝爾原理，運用數學分析方法研究宏觀現象中的力學問題。近 20年來，又發展出用近代微分幾何的觀點來研究非平直空間的流形上連續變量和高度非線性力學的原理和方法。它廣泛用于結構分析、機器動力學與振動、航天力學、多剛體系統和機器人動力學等工程技術領域，也可推廣應用于連續介質力學和相對論力學 [26，27]。分析力學是適合于研究宏觀現象的力學體系，研究對象是剛體或質點系。它闡述了力學的普遍原理，由這些原理出發導出質點系的基本運動微分方程，并研究這些方程本身以及它們的積分方法。質點系可視為宏觀物體組成的力學系統的理想模型，如剛體、彈性體、流體以及它們的綜合體都可看作質點系，質點數可由一到無窮。工程上的力學問題大多數是約束的質點系，由于約束方程類型的不同，從而形成了不同的力學系統。分析力學分為拉格朗日力學和哈密頓力學 [28，29]。前者以拉格朗日量刻畫力學系統，其運動方程稱為拉格朗日方程；后者以哈密頓量刻畫力學系統，其運動方程為哈密頓正則方程。由拉格朗日和哈密頓所奠基的分析力學是一門已經成熟發展了的學科。和目前興起的種種新學科相比，它確實顯得傳統，但由于其可準確、深刻地描述現存物理學的動力學本質，所以其價值還在與日俱增。 拉格朗日是分析力學的創立者，在其名著《分析力學》中 ，他發展了達朗貝爾和歐拉等人的研究成果，建立起拉格朗日方程，把力學體系的運動方程從以力為基本概念的牛頓形式，轉變為以能量為基本概念的分析力學形式 [30，31]，為現代動力學理論的發展奠定了基礎，也對近代數學和物理學發展起到了巨大的推動作用。利用拉格朗日**類方程解決系統的動力學問題，與矢量動力學的一般方法一樣，盡管建立方程比較容易，但其求解規模很大。拉格朗日第二類方程從獨立坐標出發，利用純數學分析方法，將用獨立坐標描述的動力學方程用統一的原理與公式進行表達，克服了在矢量動力學中建立這種方程依賴技巧的缺點，但此時建立的拉格朗日方程是一個多維二階偏微分方程，求解難度相對較大。同時，方程中的拉格朗日函數表示動能與勢能之差，雖具有能量量綱，但卻存在物理意義并不明確的不足。 哈密頓體系在多維位置和動量 (p， q)構成的相空間即辛空間中研究完整系統的力學問題，把分析力學推進一步。 1843年，哈密頓推得的用廣義坐標和廣義動量聯合表示的動力學方程，稱為正則方程 [32]。哈密頓正則方程將拉格朗日方程由 n個二階偏微分方程降階為 2n個一階的偏微分方程，求解規模與難度下降顯著。另外，方程中的哈密頓函數表示動能與勢能之和，即表示系統的機械能，因此，物理意義更加清晰。1894年，赫茲提出將約束和系統分成完整的和非完整的兩大類，從此開始非完整系統分析力學的研究。經典力學基本定理用辛幾何的語言就表示為 “一切哈密頓體系的動力演化都使辛度量保持不變，即都是辛正則變換 ” [33-35]。 1984年，馮康在微分幾何和微分方程國際會議上發表的論文《差分格式與辛幾何》[36，37]，首次系統地提出哈密頓方程和哈密頓算法，提出從辛幾何內部系統構成算法來研究其性質的途徑，從而開創了哈密頓算法這一新領域，這是計算物理、計算力學和計算數學相互結合滲透的前沿領域。 1.2.2形式化數學 數學以精確的語言和清晰的論證規則著稱，被認為是可以自證正確性的科學，但是數學論著中的錯誤卻不在少數 [38]。Lecat在 1935年發表的書中用 130頁的篇幅匯集了 1900年以前主要數學家犯的錯誤； 1879年發表的四色定理的**個證明于十年后發現是錯誤的； Wiles關于費馬大定理的證明被審稿人發現有錯誤，Wiles和學生花了一年時間來糾正； 1998年，Hales關于開普勒猜想的證明長達 300頁和 4萬行計算機代碼 (非形式化代碼 )，數學領域頂級期刊 Annals of Mathematics委托 12位審稿人用整整 4年時間審閱證明，*后只給出 99%可能是正確的結論，主編非常擔憂，認為這樣的情況會越來越多 [39]。形式化數學通過計算機對數學理論進行形式化描述，可以對數學證明的正確性進行檢查和驗證，確保數學證明本身的正確性，同時可以建立一個包含數學定義、定理和證明的形式化數學庫 [40，41]作為證明新理論的工作基礎。 形式化數學的核心主要包括邏輯語言、證明工具和形式化數學庫三部分 [42]。 Wiedijk[43]認為，形式化數學是數學發展歷史上的第三次革命。形式化數學可以幫助數學家檢查證明的正確性，從而構建更加可靠的數學理論，同時也構建了計算機可以理解的數學知識庫。它不僅是機器定理證明的基礎，同時也是計算機軟硬件系統形式化驗證的基礎，因此，形式化數學已經成為基礎科學的重要研究領域。 形式化數學早期*著名的案例是 1996年 McCune使用完全自動定理證明器 EQP給出了 Robbins猜想的機器證明 [39]。
書友推薦
- >
朝聞道
- >
中國人在烏蘇里邊疆區:歷史與人類學概述
- >
苦雨齋序跋文-周作人自編集
- >
姑媽的寶刀
- >
唐代進士錄
- >
推拿
- >
史學評論
- >
詩經-先民的歌唱
本類暢銷
