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

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

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

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

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

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

2 王文平;;應(yīng)用Laplace變換計(jì)算兩類廣義積分[J];武漢船舶職業(yè)技術(shù)學(xué)院學(xué)報(bào);2014年05期

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

4 張海霞;于洪全;;按Laplace譜半徑對圈長和階數(shù)固定的單圈圖的排序[J];大連理工大學(xué)學(xué)報(bào);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方程九點(diǎn)差分格式的構(gòu)造及其誤差估計(jì)[J];哈爾濱師范大學(xué)自然科學(xué)學(xué)報(bào);2011年04期

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

8 葉燕文;丁峰生;王三福;;利用Laplace變換計(jì)算分?jǐn)?shù)階微積分[J];天水師范學(xué)院學(xué)報(bào);2010年02期

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

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

相關(guān)會議論文 前10條

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

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

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

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

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

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

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

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

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

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

相關(guān)博士學(xué)位論文 前10條

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

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

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

4 王林峰;加權(quán)Laplace-Beltrami算子及相關(guān)問題研究[D];華東師范大學(xué);2007年

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

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

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

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

9 楊變霞;分?jǐn)?shù)階Laplace算子的譜理論及其在微分方程中的應(yīng)用[D];蘭州大學(xué);2015年

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

相關(guān)碩士學(xué)位論文 前10條

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

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

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

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

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

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

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

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

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

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

本文編號：2777739