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

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

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

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