基於高階邏輯的分數階建模與驗證理論研究

《基於高階邏輯的分數階建模與驗證理論研究》是依託首都師範大學，由趙春娜擔任項目負責人的青年科學基金項目。

基本介紹

• 中文名：基於高階邏輯的分數階建模與驗證理論研究
• 項目類別：青年科學基金項目
• 項目負責人：趙春娜
• 依託單位：首都師範大學

項目摘要

本項目首次將分數階微積分與形式化驗證結合起來，在高階邏輯定理證明中建立分數階微積分理論體系。針對實際複雜系統，提出分數階建模方法，構建和完善分數階系統HOL推理平台，包括在形式化驗證的高階邏輯定理證明器中引入分數階微積分基本定義，驗證分數階微積分的基本運算、性質、定律等內容，建立分數階微積分理論體系，並用其檢驗分數階模型的精確性。分數階模型由於引入分數階次可以更加準確的描述實際複雜系統，分數階驗證能夠提高定理證明的完備性和準確性。本課題的研究成果將完善分數階理論體系和高階邏輯驗證理論體系，為定理驗證的廣泛套用提供基礎，對人工智慧等相關領域的發展起到積極的推動作用。

結題摘要

隨著人們對自然認識的逐步深入，發現了自然界的本質是分數階的。分數階模型可以更加準確的描述實際複雜系統。複雜系統的安全性、精準性、完備性受到更大關注。本項目首次將分數階微積分與形式化驗證結合起來。分數階建模與驗證能夠準確描述複雜系統，並在高階邏輯中證明系統正確性。提出了分數階的認知過程模型，課程評估、教育評估的分數階建模方法，城市交通流的分數階模型，以及環境污染的分數階模型。針對分數階系統高可靠性分析理論的發展需要，完成了實數二項式係數及性質的高階邏輯形式化建模與驗證、Gauge積分及性質的高階邏輯形式化建模與驗證、分數階微積分定義及性質的高階邏輯形式化建模與驗證，包括建立了分數階微積分兩種定義的高階邏輯模型，三種常用定義間的相互轉化，對分數階微積分的零階性、線性性質、分數階微積分與整數階微積分的一致性和疊加性進行了形式化驗證。提出了拉普拉斯變換的高階邏輯形式化建模與驗證，將拉氏變換的卷積定理進行高階邏輯建模及形式化驗證分析。在實際系統中套用本項目建立的定理，策略等驗證了實際系統，完成了分數階電容的形式化分析與驗證、分數階微分電路的形式化分析與驗證、直流電機的形式化驗證、反向積分電路的形式化建模與驗證、SpaceWire 解碼電路的高階邏輯形式化建模與驗證、FC元件的形式化分析與驗證、分數階PID控制器的形式化分析與驗證。研究成果完善了分數階理論體系和高階邏輯驗證理論體系，為定理驗證的廣泛套用提供基礎，對人工智慧等相關領域的發展起到積極的推動作用。發表學術論文16篇，申請發明專利2項，軟體著作權3項；獲省部級獎項3次，培養研究生5名，晉升高級職稱1人，在十餘家國內外學術刊物擔任審稿人。