帶函數(shù)的析取邏輯程序良基語義研究.pdf

1、二十世紀八十年代邏輯程序設(shè)計語言在描述性語義上取得突破性的進展-穩(wěn)定模型語義（回答集語義），為邏輯程序的研究打開了大門。回答集語義的提出使人們可以用邏輯程序表示問題，而程序的回答集作為該問題的可行解。2000年前后，各種有效的邏輯程序求解器被研制出來，推廣了邏輯程序設(shè)計語言的應(yīng)用,使回答集程序設(shè)計（Answer Set Programming,簡稱ASP）進入一個新高度。
　　之前邏輯程序的研究很少涉及函數(shù)，近幾年一些國內(nèi)外的專家

2、、學(xué)者提出了帶函數(shù)的邏輯程序的求解方法，主要通過公式化其完備化和環(huán)公式，從而計算穩(wěn)定模型。同時他們提出了消除函數(shù)的方法，即用新的變量反復(fù)替換每個函數(shù)項，同時在對應(yīng)的規(guī)則體中增加新的函數(shù)原子，從而消除原子中的函數(shù)。但檢查一個模型是否極小模型相當困難，主要原因之一是檢查一個集合是否是回答集是困難的（∑2-完全的）。
　　正規(guī)邏輯程序的良基語義是近十年邏輯程序語義解釋的一個熱點，它的一個重要作用是計算回答集的時候可以化簡程序。因此在王以

3、松等人的基礎(chǔ)上，將良基語義擴展到帶函數(shù)的析取邏輯程序中，發(fā)現(xiàn)用這種思想能夠解決帶函數(shù)析取邏輯程序穩(wěn)定模型的求解。文章中我們的主要工作（1）提出了帶函數(shù)的析取邏輯程序無基集的概念，證明了空無基集與穩(wěn)定模型之間的一一對應(yīng)關(guān)系；（2）研究了帶函數(shù)的析取邏輯程序的良基語義，證明其良基模型是完全解釋時，是其穩(wěn)定模型；（3）根據(jù)上面的結(jié)論設(shè)計了基于SAT的穩(wěn)定模型算法，證明了一個邏輯程序的模型是該程序的穩(wěn)定模型當且僅當它們對應(yīng)的一個命題公式是不可滿