發(fā)布時間：2020-08-01 16:58

【摘要】：形式化數學是一個借助定理證明器進行數學定理機械驗證的研究方向。形式化工程數學是形式化數學技術在工程數學領域中的應用。在控制系統(tǒng)設計中的一個關鍵性數學工具是Laplace變換,它被廣泛地應用于求解線性微分方程和分析安全關鍵系統(tǒng),它也是包括飛行控制系統(tǒng)在內的許多控制算法設計和軟件設計的基礎工具。定理證明是利用計算機輔助人們進行數學定理證明,它克服了純人工證明容易出錯等缺點,已經廣泛應用于數學定理證明、集成電路和軟件驗證中,然而在飛行控制方面的形式化驗證工作十分罕見。一個典型的例子是采用SCADE系統(tǒng)進行建模、開發(fā)和驗證飛行控制軟件,雖然基于模型的方法提高了軟件生產力并且減少了軟件缺陷,但是并不能解決數學推導和飛控數學算法的可靠性驗證問題。飛行控制系統(tǒng)的設計和分析依賴于大量復雜的數學推導,為了解決這樣的問題,我們研究基于Coq定理證明器的形式化工程數學驗證技術。這一工作的大方向是在Coq中建立完善的形式化工程數學理論庫,以便支持飛行控制數學以及其他工程數學的推導驗證。本文在高階邏輯定理證明器Coq中采用極限、連續(xù)、微分、積分、復數等理論實現了Laplace變換定義的形式化,并且驗證了Laplace變換的主要性質:存在性、線性性質、復頻域位移性質、微分性質、二階微分性質、積分性質等。為了能驗證更復雜的控制系統(tǒng),本文給出了二維向量Laplace變換的形式化定義,并且驗證了向量Laplace變換基本性質。目前尚未在文獻中發(fā)現將Laplace變換形式化理論推廣到二維向量的類似工作,這一工作已經能夠有效支持實際應用中大部分控制系統(tǒng)的形式化驗證。二維Laplace變換依賴于矩陣理論,我們采用基于元組的表示方法對小規(guī)模的矩陣(2-4維)進行形式化定義并且對矩陣的運算、向量的運算以及矩陣和向量之間的運算進行形式化定義。在此基礎上,我們對這些矩陣運算的正確性以及運算性質進行形式化證明。最后我們對飛行控制系統(tǒng)、機器人控制系統(tǒng)中的一些傳遞函數的推導過程進行了形式化的描述和驗證。
【學位授予單位】：南京航空航天大學
【學位級別】：碩士
【學位授予年份】：2019
【分類號】：V249.1;TB11
【圖文】：

公式來描述系統(tǒng)及其性質，并且通過定義公理和推導規(guī)則來證傳統(tǒng)需要人工紙筆證明的數學定理和日常生活中的推理變成了它與傳統(tǒng)的數學證明是不一樣的，傳統(tǒng)證明大多數都是依靠不言一步都需要有完整的證明過程，所以整個定理證明過程中每一個步驟準確無誤。但是這也是它的缺點，有時候非常簡單的證但是計算機是能夠處理這些復雜的證明過程的。定理證明分為。定理證明的發(fā)展是從自動定理證明開始，由于其自動化的特。但是很多復雜數據類型的定理是不能夠通過自動化的方式完能處理非常有限的情況[8]。在實際應用中，大規(guī)模的控制系統(tǒng)此出現了邏輯表述能力更強的交互式定理證明[9]。交互式定理證技術，雖然不能自動推理，但是對于復雜程度不高的問題，策略[10]，比如等式自動證明策略、導數自動證明策略等。它的數學邏輯對待驗證系統(tǒng)和系統(tǒng)性質進行形式化描述（建模），然理進行一步一步證明，在證明的過程中往往會出現大量新的子我們可能會需要證明大量的中間引理對這些子目標單獨證明。

Laplace 變換在 Coq 中的形式化及其在飛控系統(tǒng)驗證中的應用oq 交互式集成開發(fā)環(huán)境 Coq 系統(tǒng)一般有兩種方法，標準的方法是在操作系統(tǒng)的命令行終端中啟動 Coq 系統(tǒng)的 linux 系統(tǒng)的終端中，或者在 cygwin 終端中，可以使用 coqto之后可以輸入 Coq 命令，如圖 2.1，命令“Require Import Reals”將會裝載用“.”結束，回車提交給系統(tǒng)執(zhí)行。在操作全部執(zhí)行完畢之后用命令“Qu

圖 2.2 CoqIde 環(huán)境明方法，定理證明的過程是反向的，就是從目標出發(fā)，尋找到達目標的擇某一個命令作用于它。Coq 系統(tǒng)會檢查使用該命令之后所需那么該命令應用成功并且將待證目標分解為一個或多個子目標的信息。對于分解出來的每一個子目標采用相同的方式進行證。CoqIde 右邊子窗口中顯示 No more subgoals，表示引理已經還得再加一條命令 Qed，它的作用是正式結束一個證明，并且便在后續(xù)的證明中調用。在證明的過程中，我們會發(fā)現并不是所以這對用戶的要求很高[5]。明過程中經常使用到的命令：. 把全稱量詞中的變量和蘊含式的左端都轉變成子目標的條件。qIde 環(huán)境的右邊窗口中，橫線上方是子目標中的條件部分，下方ption. 當待證目標已經出現在假設條件當中，直接使用假設條件

【相似文獻】

相關期刊論文 前10條

1 崔海波;;Laplace變換在偏微分方程中的應用[J];教育教學論壇;2017年04期

2 王文平;;應用Laplace變換計算兩類廣義積分[J];武漢船舶職業(yè)技術學院學報;2014年05期

3 張曉麗;;奇異p(x)-Laplace方程正解的存在性[J];赤峰學院學報(自然科學版);2014年03期

4 張海霞;于洪全;;按Laplace譜半徑對圈長和階數固定的單圈圖的排序[J];大連理工大學學報;2013年01期

5 羅光;MA Yan-mei;YANG Hui-qun;;On the Laplace transform of delta function[J];Journal of Chongqing University(English Edition);2013年01期

6 趙雪菲;么煥民;;Laplace方程九點差分格式的構造及其誤差估計[J];哈爾濱師范大學自然科學學報;2011年04期

7 羅茜;孫道椿;;Laplace-Stieltjes變換的收斂性與增長性[J];華南師范大學學報(自然科學版);2010年01期

8 葉燕文;丁峰生;王三福;;利用Laplace變換計算分數階微積分[J];天水師范學院學報;2010年02期

9 任淑青;劉輝昭;;一類p(x)-Laplace方程組徑向解的存在性[J];河北工業(yè)大學學報;2008年02期

10 楊海明;何世安;鎮(zhèn)松林;蘇政鵬;;斯特林制冷機振動數學模型的Laplace變換及仿真[J];低溫與超導;2008年04期

相關會議論文 前10條

1 姜玉山;;一類p(x)-Laplace方程解的存在性[A];數學·力學·物理學·高新技術研究進展——2006（11）卷——中國數學力學物理學高新技術交叉研究會第11屆學術研討會論文集[C];2006年

2 Jing-Bo Chen;;Dispersion analysis of an average-derivative optimal scheme for Laplace-domain scalar wave equation[A];中國科學院地質與地球物理研究所2014年度（第14屆）學術年會論文匯編——油氣資源研究室[C];2015年

3 Jing-Bo Chen;;Laplace-Fourier-domain dispersion analysis of an average derivative optimal scheme for scalar-wave equation[A];中國科學院地質與地球物理研究所2014年度（第14屆）學術年會論文匯編——油氣資源研究室[C];2015年

4 Jing-Bo Chen;Shu-Hong Cao;;Comparison of two schemes for Laplace-domain 2D scalar wave equation[A];中國科學院地質與地球物理研究所2014年度（第14屆）學術年會論文匯編——油氣資源研究室[C];2015年

5 Guangsheng Chen;;The finite Yang-Laplace Transform in fractal space[A];第二屆國際計算科學與工程國際學術研討會論文集[C];2013年

6 Shi Jingchang;Yan Hong;;CUDA implementation of a Laplace solver[A];中國力學大會——2013論文摘要集[C];2013年

7 Huang Zaixing;;Generalized Young-Laplace equation based on Lagrangian field theory[A];中國力學大會——2013論文摘要集[C];2013年

8 黃劍玲;鄒輝;;基于高斯Laplace算子圖像邊緣檢測的改進[A];2007年全國開放式分布與并行計算機學術會議論文集(上冊)[C];2007年

9 陳曉;譚福錦;;三維Laplace算子與方程在不同坐標系下的刻畫[A];數學·力學·物理學·高新技術交叉研究進展——2010（13）卷[C];2010年

10 曹國鑫;劉海龍;;Young-Laplace方程在納米尺度下的有效性[A];第十四屆全國物理力學學術會議縮編文集[C];2016年

相關博士學位論文 前10條

1 王立本;（Φ_1,Φ_2）-Laplace橢圓方程組解的存在性和多重性[D];昆明理工大學;2018年

2 夏超;圖上的Laplace算子及迭代方程的研究[D];哈爾濱工業(yè)大學;2017年

3 余路娟;p(x)-Laplace方程的特征值問題和Picone等式[D];大連理工大學;2018年

4 王林峰;加權Laplace-Beltrami算子及相關問題研究[D];華東師范大學;2007年

5 Mohamed Abdulai Koroma;一類邊界層方程的Laplace Adomian混合分解近似解[D];哈爾濱工業(yè)大學;2013年

6 劉芳;幾類含無窮Laplace算子的非線性偏微分方程的解的適定性[D];南京理工大學;2013年

7 陳永剛;Laplace方程反問題的基本解方法[D];蘭州大學;2012年

8 張小玲;若干圖的Laplace譜和距離譜[D];蘭州大學;2009年

9 楊變霞;分數階Laplace算子的譜理論及其在微分方程中的應用[D];蘭州大學;2015年

10 郭二林;幾類非局部p（x）-Laplace方程解的存在性與多解性[D];蘭州大學;2013年

相關碩士學位論文 前10條

1 王艷梅;拋物p-Laplace型方程的p-Rényi熵冪凹性研究及其應用[D];山西大學;2019年

2 景新鵬;一類帶有擴散項的p-Laplace方程無窮多解和基態(tài)解的存在性[D];山西大學;2019年

3 劉鮮;一類快擴散p-Laplace方程解的整體存在、熄滅與非熄滅[D];吉林大學;2019年

4 汪一飛;Laplace變換在Coq中的形式化及其在飛控系統(tǒng)驗證中的應用[D];南京航空航天大學;2019年

5 曹輝;Laplace分布的統(tǒng)計推斷及應用[D];揚州大學;2018年

6 孔婕;大偏差理論的基本原理：Laplace原理[D];中國科學技術大學;2018年

7 宗馳;兩類（φ_1,φ_2）-Laplace差分系統(tǒng)周期解和同宿解的存在性與多重性[D];昆明理工大學;2018年

8 陸晟祺;雙圈圖的無符號1-Laplace算子譜[D];哈爾濱工業(yè)大學;2018年

9 郝亞東;基于Henstock積分的模糊Laplace變換及其應用[D];西北師范大學;2017年

10 宋文佩;Laplace-Stieltjes變換和廣義Laplace-Stieltjes變換的增長性[D];江西師范大學;2018年

本文編號：2777739