邏輯程序始于上世紀(jì)70年代初，來源于定理機(jī)器證明與人工智能的研究。在邏輯程序30年的發(fā)展中，它已經(jīng)成為了人工智能領(lǐng)域中重要的一個方向，在眾多人工智能領(lǐng)域展示著它的價值。邏輯程序語義的研究中重要的一個方面就是否定的處理。處理否定最基本的兩種方法是閉世界假定（closed world assumption）和失敗即否定原則（negation as failure）。本文所論述的非基有限失敗語義，是對于失敗即否定原則的研究。在對非基有限失敗語義的研究中，抽象解釋（abstract interpretation）方法被用于不動點(diǎn)語義的推導(dǎo)。 抽象解釋方法是一種用于近似程序語義的通用方法。其核心思想在于構(gòu)建和聯(lián)系程序的兩個不用的語義：具體語義（concrete semantics）和抽象語義（abstract semantics），抽象語義是具體語義的近似。抽象解釋方法與邏輯程序有著緊密的聯(lián)系，在邏輯程序語義的研究中有著重要的作用。 有限失敗是失敗即否定原則中重要的概念，它是指求解一個目標(biāo)所得到的SLD樹是有限且每個分支都是失敗的。最先在文獻(xiàn)中... 

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

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

【文章目錄】：
第一章 緒論
    1.1 背景
    1.2 問題的提出
    1.3 研究線索及本文工作
第二章 邏輯程序和抽象解釋
    2.1 邏輯程序基礎(chǔ)
        2.1.1 邏輯程序的語法
        2.1.2 邏輯程序的指稱語義
        2.1.3 邏輯程序的操作語義
        2.1.4 有限失敗
    2.2 抽象解釋基礎(chǔ)
第三章 可觀察行為理論
    3.1 SLD推導(dǎo)語義
        3.1.1 語義域
        3.1.2 SLD推導(dǎo)的指稱語義
        3.1.3 SLD推導(dǎo)的操作語義
        3.1.4 程序的指稱
        3.1.5 SLD推導(dǎo)的語義性質(zhì)
    3.2 可觀察行為理論
        3.2.1 可觀察行為
        3.2.2 抽象語義
        3.2.3 標(biāo)準(zhǔn)可觀察行為
        3.2.4 指稱可觀察行為
第四章 非基有限失敗的不動點(diǎn)語義
    4.1 無限推導(dǎo)的性質(zhì)
    4.2 SLD推導(dǎo)語義的擴(kuò)展
        4.2.1 基本運(yùn)算符的擴(kuò)展
        4.2.2 語義的擴(kuò)展
        4.2.3 指稱可觀察行為的修改
    4.3 非基有限失敗的不動點(diǎn)語義
        4.3.1 NGFF的可觀察行為
        4.3.2 NGFF的不動點(diǎn)語義
    4.4 抽象域的重構(gòu)
第五章 結(jié)論與展望
參考文獻(xiàn)
致謝
摘要
Abstract



本文編號：3732912