發(fā)布時間：2023-04-20 22:28

　　自動定理證明(Automated Theorem Proving)或者機器定理證明(MechanicalTheorem Proving)是通過計算機實現(xiàn)定理證明.二十世紀(jì)五十年代以來自動定理證明一直是計算機科學(xué)的熱點之一,在數(shù)學(xué)、硬件測試與驗證、軟件生成與驗證、協(xié)議驗證、人工智能方面都得到了成功的應(yīng)用. 部分實例化方法把一階問題化為一系列命題邏輯中的可滿足性問題來解決一階邏輯的可滿足問題,檢查子句集的滿足式映射中的阻塞是該方法的關(guān)鍵.論文提出的子句搜索方法在判定子句集可滿足性的同時給出了一個模型從而得到滿足式映射.格值邏輯的不完全可比性便于描述人類的思維、判斷和決策.格值命題邏輯系統(tǒng)LP(X)于1993年建立,目前對LP(X)系統(tǒng)的自動推理研究主要是歸結(jié)方法,論文討論了它的tableau方法.常用的邏輯證明方法重點在于判定可滿足性而不能給出符合人們閱讀習(xí)慣的演繹過程.歸結(jié)方法、語義表方法、相繼式方法是定理證明中的常用方法,但是重點在于判定而不是演繹,論文探討了相干命題邏輯系統(tǒng)R的試探法實現(xiàn)和相干自然推理系統(tǒng)NR的自然推理法實現(xiàn),生成了類似于手工證明的可讀證明.具體而言論文的工作包括以下...

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

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

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 自動推理的發(fā)展簡史
    1.2 非經(jīng)典邏輯研究概況
    1.3 論文的選題和主要工作
第二章 一階子句搜索方法
    2.1 子句搜索方法
    2.2 一階子句搜索方法
    2.3 本章小結(jié)
第三章 格值命題邏輯LP(X)的自動證明
    3.1 基礎(chǔ)知識
    3.2 LP(X)的tableau方法
    3.3 LP(X)的直積分解
    3.4 本章小結(jié)
第四章 相干命題邏輯R的可讀證明
    4.1 試探法自動證明
    4.2 自然推理法自動證明
    4.3 試探法和自然推理法的混合求證
    4.4 本章小結(jié)
第五章 總結(jié)與展望
參考文獻
致謝
攻讀博士學(xué)位期間發(fā)表論文和科研情況



本文編號：3795279