在高階邏輯定理證明器中研究了函數(shù)無窮遠(yuǎn)處極限的形式化建模和驗證,包括函數(shù)無窮遠(yuǎn)處極限定義的形式化模型,函數(shù)極限相關(guān)性質(zhì)的建模與驗證,有唯一性、保不等式性、絕對值函數(shù)在無窮遠(yuǎn)處的極限、極限等價性、常函數(shù)極限等.函數(shù)無窮遠(yuǎn)處極限的高階邏輯定義是利用拓?fù)錁O限方式定義的,并在實數(shù)域內(nèi)利用集合關(guān)系等驗證定理.根據(jù)集合有序關(guān)系定理驗證了唯一性.利用差值和絕對值的高階邏輯性質(zhì)驗證極限為零的屬性.變量與常數(shù)之和與積的極限高階邏輯定理也通過已驗證定理和高階邏輯策略驗證了.建立了函數(shù)極限四則運(yùn)算的高階邏輯模型,并驗證了函數(shù)極限加法、函數(shù)極限減法、函數(shù)極限乘法、函數(shù)極限與常數(shù)乘法、函數(shù)極限除法的高階邏輯定理.也建立了函數(shù)積分極限的高階邏輯形式化模型,驗證了函數(shù)積分極限上限絕對值定理、函數(shù)積分極限上限可加定理、函數(shù)積分極限上限可乘定理.在此基礎(chǔ)上,建立了拉普拉斯變換卷積定理的高階邏輯形式化建模與驗證.最后,對電阻-電感電路中的電流進(jìn)行了高階邏輯形式化建模與驗證.建立了單位階躍信號和電路中電流的高階邏輯形式化定義,并驗證了其正確性.該實例驗證表明了函數(shù)極限和相關(guān)性質(zhì)的高階邏輯形式化模型的正確性,為后續(xù)控制系統(tǒng)的...

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

【文章目錄】：
1 引言
2 高階邏輯定理證明器
3 函數(shù)極限定義的建模與驗證
4 函數(shù)極限相關(guān)性質(zhì)的建模與驗證
    4.1 基本性質(zhì)
        (1)唯一性
        (2)保不等式性
        (3)極限為零
        (4)極限等價性
        (5)常函數(shù)極限
    4.2 函數(shù)極限四則運(yùn)算的建模與驗證
        (1)函數(shù)極限加法
        (2)函數(shù)極限減法
        (3)函數(shù)極限乘法
        (4)函數(shù)極限與常數(shù)乘法
        (5)函數(shù)極限除法
    4.3 函數(shù)積分極限的高階邏輯形式化建模與驗證
        (1)正無窮函數(shù)積分上限取絕對值的建模與驗證
        (2)正無窮函數(shù)積分上限與常數(shù)之和的建模與驗證
        (3)正無窮函數(shù)積分上限與非負(fù)常數(shù)之積的建模與驗證
5拉普拉斯變換卷積定理的建模與驗證
6 RL電路電流的高階邏輯形式化建模與驗證
    (1)模型
    (2)需要驗證的性質(zhì)
    (3)形式化驗證
7 結(jié)論



本文編號：3766897