發(fā)布時間：2022-12-18 17:23

　　交互式定理證明技術(shù)是可以應(yīng)用于大規(guī)模系統(tǒng)驗證的重要的形式化方法，近年有一些影響很廣的成功案例。但是交互式定理證明的使用難度以及對使用人員的嚴重依賴阻礙了其在工業(yè)界的發(fā)展。本文圍繞主流的交互式定理證明工具之一的Coq，總結(jié)了其應(yīng)用過程中的問題，分析了問題的原因，并在此基礎(chǔ)上從其基礎(chǔ)理論和應(yīng)用實踐兩方面入手嘗試提高Coq在實際應(yīng)用過程中的易用性。在理論方面，針對Coq在使用中對依賴類型等價關(guān)系判定能力不足的問題，對Coq基礎(chǔ)理論進行了擴展，并通過驗證擴展后理論的主要性質(zhì)，保證擴展的理論同樣可以應(yīng)用于實現(xiàn)定理證明工具。在應(yīng)用實踐方面，針對組合邏輯提出了基于Coq的驗證框架。該框架提供了對組合邏輯建模驗證的統(tǒng)一方法，也提供了面向組合邏輯驗證的擴展庫。對算術(shù)計算邏輯單元的實際驗證工作說明了該框架的可用性和易用性。本文的主要工作包含以下幾個方面： 1.擴展了Coq的基礎(chǔ)理論：歸納構(gòu)造演算。在內(nèi)涵式的歸納構(gòu)造演算等價判定的基礎(chǔ)上增加了外延式等價關(guān)系的判定能力，并且給出了擴展理論應(yīng)用于實現(xiàn)定理證明工具的機制。外延式理論是抽象表示的，并被一些約束所限制，所有滿足限制的外延式理論都可以被擴充進歸納構(gòu)... 

【文章頁數(shù)】：129 頁

【學(xué)位級別】：博士

【文章目錄】：
摘要
Abstract
主要符號對照表
第1章 緒論
    1.1 研究背景
    1.2 研究現(xiàn)狀
    1.3 研究思路
        1.3.1 定理證明技術(shù)應(yīng)用問題
        1.3.2 針對性改進方案的思路
    1.4 預(yù)備知識
        1.4.1 Coq 的理論基礎(chǔ)歸納構(gòu)造演算
        1.4.2 Coq 的語法及功能
        1.4.3 Coq 理論與工具之間的聯(lián)系
    1.5 主要貢獻
    1.6 論文結(jié)構(gòu)
第2章 Coq 基礎(chǔ)類型論 CIC 的擴展理論 CIC~ωT
    2.1 引言
        2.1.1 問題描述
        2.1.2 問題分析與解決思路
        2.1.3 工作難點及相關(guān)工作
        2.1.4 本章結(jié)構(gòu)
    2.2 CIC~ωT的定義
        2.2.1 理論的定義
        2.2.2 類型系統(tǒng)部分的定義
    2.3 CIC~ωT的主要性質(zhì)及證明
        2.3.1 匯合性
        2.3.2 相關(guān)性
        2.3.3 類型保持性
        2.3.4 語義方面的性質(zhì)
        2.3.5 類型檢查的可判定性
    2.4 本章小結(jié)
第3章 CIC~ωT語義性質(zhì)的形式化證明
    3.1 引言
        3.1.1 類型系統(tǒng)邏輯自洽性和計算中止性的證明思路
        3.1.2 深層嵌入和淺層嵌入
        3.1.3 本章結(jié)構(gòu)
    3.2 CC 模型及擴展構(gòu)造的 CIC 模型
        3.2.1 抽象模塊
        3.2.2 元模型及性質(zhì)
        3.2.3 CC 模型及性質(zhì)
        3.2.4 CIC 模型及性質(zhì)
    3.3 CIC~ωT抽象模型及性質(zhì)證明
        3.3.1 CIC~ωT模型構(gòu)造
        3.3.2 CIC~ωT模型可靠性證明
    3.4 可嵌入外延式理論實例：Presburger 算術(shù)
        3.4.1 Presburger 代數(shù)的簽名
        3.4.2 Presburger 代數(shù)的公理
    3.5 本章小結(jié)
第4章 基于 Coq 的組合邏輯驗證框架
    4.1 引言
        4.1.1 工具和領(lǐng)域選擇
        4.1.2 框架的特點
        4.1.3 本章結(jié)構(gòu)
    4.2 組合邏輯驗證框架介紹
        4.2.1 領(lǐng)域庫
        4.2.2 功能描述
        4.2.3 性質(zhì)描述
        4.2.4 證明管理
    4.3 組合邏輯驗證框架特點
        4.3.1 真實性
        4.3.2 靈活性
        4.3.3 模塊化
        4.3.4 擴展庫的豐富性和可擴展性
    4.4 本章小結(jié)
第5章 基于組合邏輯驗證框架的應(yīng)用實例
    5.1 引言
        5.1.1 基本加法器驗證的相關(guān)工作
        5.1.2 并行前綴循環(huán)進位加法器驗證的相關(guān)工作
        5.1.3 本章結(jié)構(gòu)
    5.2 Ling 加法器驗證
        5.2.1 Ling 加法器介紹
        5.2.2 框架下 Ling 加法器的驗證
        5.2.3 框架下 Ling 加法器擴展的驗證
    5.3 并行前綴加法器驗證
        5.3.1 并行前綴加法器介紹
        5.3.2 并行前綴樹的抽象模塊
        5.3.3 半具體的通用并行前綴加法器驗證
        5.3.4 具體到某種特定實現(xiàn)的并行前綴加法器驗證
    5.4 并行前綴循環(huán)進位加法器驗證
        5.4.1 并行前綴循環(huán)進位加法器結(jié)構(gòu)及基本組件介紹
        5.4.2 并行前綴循環(huán)進位加法器內(nèi)核結(jié)構(gòu)及證明
        5.4.3 并行前綴循環(huán)進位加法器正確性證明
    5.5 本章小結(jié)
第6章 結(jié)語
    6.1 工作總結(jié)
    6.2 研究展望
參考文獻
致謝
個人簡歷、在學(xué)期間發(fā)表的學(xué)術(shù)論文與研究成果



本文編號：3722456