回答集編程背景（Answer Set Programming）

畢業設計跟的導師是研究計算機理論的，花了三個月學習符號邏輯，試圖優化一個回答集程序的求解器（Answer set solver）。比起眼花繚亂的前端框架和熱鬧的社區討論，符號邏輯就是一個挺小衆的數學領域。一講到邏輯程序就會涉及一大堆的概念 ，伴隨一大堆數理邏輯的符號，令有興趣的新手望而卻步。此篇博文能夠說是導師的博士論文的一篇讀後感，一篇回答集編程的發展史，一篇回答集程序入門簡介。詳見《提升ASP效率的若干途徑及在服務機器人上的應用》。

1.人工智能學派

一些傳統人工智能的研究者認爲，(人工)智能能夠經過符號推理形式化刻畫，這一派系的研究如今被歸類爲符號主義。此外，還有聯結主義和行爲主義。當下很火的機器學習就是屬於聯結主義，原理主要爲神經網絡及神經網絡間的鏈接機制與學習算法。行爲主義源於控制論，主要的應用是感知-動做型控制系統。比起另外兩個兄弟，符號邏輯目前的工業應用還不多，是一座數學家在構築的伊甸園。

2.回答集程序的背景

「ASP研究來源於邏輯程序和非單調推理兩個領域的交叉融合。最初，基於經典邏輯，邏輯程序定義了陳述性表達(declarative representation)的程序語言，並經過語法限制實現高效計算。以後，因爲應用的須要引入否認知識的表達，並經過失敗即否認原則進行推理。

Gelfond and Lifschitz(1 988)提出穩定模型語義(stable model semantics)，首次利用非單調推理領域的成果成功解釋失敗即否認。

隨着研究的深刻，穩定模型語義不斷被擴展，發現了不少良好的性質，它不光能解釋邏輯程序中失敗即否認，還與非單調推理中不少工做有密切聯繫，從而被承認爲一個實用的非單調推理工具和能夠表達常識知識的知識表示語言。以後，愈來愈多的人開始關注這個方向，並稱這個新領域爲回答集編程(Answer Set Programming,ASP)。「

2.1 邏輯程序

「邏輯程序起源於七十年代自動定理證實和人工智能方面的工做，其主要思想能夠用Kowalski(1979)提出的等式來解釋：

Algorithm=Logic+Control。即，算法分爲兩部分，邏輯與控制。

 

其中邏輯部分用來講明問題是什麼(what)，控制部分用來講明如何求解問題(how)。而邏輯程序的最終目標就是，程序員只須要刻畫出算法的邏輯部分，系統能夠自動求解。邏輯程序領域已經有諸如PROLOG的不少實際成果和應用。「

這種用通用方法求解問題的想法很美好，但實現起來很是艱難，推廣也一樣是一個大問題。這個工做能夠類比C++中的模板（template），爲一個複雜度高的抽象問題實現一個高效的程序，而後調用這個程序去解決簡單的問題。

 

目前，效率這一塊已經有很高效的實現，反而應用方面，卻不如預料中的普遍。成爲流行的編程語言須要有不少條件，這個語言原本就不是面向一個廣闊「市場」來設計的，天然難以作到流行。目前有中科大的服務機器人項目在應用這個語言，隨着服務機器人的發展，邏輯程序的前景至少不算窮途末路。

2.2 邏輯程序中的否認

(傳統)邏輯程序通常狀況下只能推理出正文字形式的結論，但根據實際應用的須要，經過增長額外的規則，它也能夠推出負文字形式的結論。這些額外規則中最主要的兩個是：封閉世界假設(Closed World Assumption，CWA)和失敗即否認(negation as failure，NAF)。

封閉世界假設來源於演繹數據庫，因爲數據庫中有大量事實，爲了更緊湊的表達，很天然的會假設，凡是沒有說明爲真的命題都默認爲假。

例如，當數據庫中不存在某個時刻的航班時，咱們會假設此刻沒有此航班。嚴格的說，封閉世界假設對應推理規則：

 

若是一個常原子A不是一個邏輯程序的結論(屬於其極小模型)，則推出A的否認。注意，封閉世界假設是一個非單調推理規則，即，當加入新知識後，原先推出的結論可能再也不成立。同時，因爲一階邏輯是不可斷定的，因此實際中封閉世界假設只能用在那些能夠在有限時間內判斷
出推不出的公式，由此引出失敗即否認。

 

失敗即否認對應推理規則：若是常原子A被判斷出推不出，則推出not A。一樣，失敗即否認也是一個非單調推理規則。

2.3 非單調推理
經典邏輯(命題，一階)是單調的(monotonic)：若是語句A是語句集丁的邏輯結論，則A必定是丁的任意超集的結論。即，增長新知識並不影響之前的結論。

 

而常識推理卻與此不一樣，大多數狀況下，因爲信息不徹底，知識不完備等緣由，爲了推出有用的結果，咱們不得不作一些額外的假設，例如封閉世界假設。

 

更通常的，咱們假設環境是正常的(normal)，沒有意外發生，並獲得一般狀況下結論。而當環境變化，增長新知識後，原來的假設可能再也不成立，即，發生意外，得知真實狀況再也不是一般的，此時咱們只能調整之前的結論，甚至獲得否認的結論。如下是一些常識推理的例子：

1．鳥(一般狀況下)會飛，特威蒂(tweety)是鳥，因此，特威蒂會飛。
2．鳥會飛，特威蒂是鳥，但特威蒂不會飛，因此，特威蒂不會飛。
3．鳥會飛，企鵝不會飛，特威蒂是鳥，特威蒂是企鵝，因此，特威蒂不知是否會飛。
4．企鵝是鳥，鳥會飛，企鵝不會飛，特威蒂是鳥，特威蒂是企鵝，因此，特威蒂不會飛。
5．貴格會教徒(一般狀況下)是和平主義者，共和黨人(一般狀況下)不是和平主義者，尼克松是貴格會教徒，因此，尼克松是和平主義者。
6．貴格會教徒是和平主義者，共和黨人不是和平主義者，尼克松是貴格會教徒，尼克松是共和黨人，因此，尼克松不知是不是和平主義者。

這些推理是研究常識推理一般都會列舉或考慮到的例子，其中第4項稱爲企鵝原則(Penguin Principle)，第6項稱爲尼克松菱形(Nixon Diamond)。它們能夠用來測試一個邏輯是否合理的刻畫常識推理。而上述推理充分說明了非單調推理的做用，即，ASP的其中一個良好性質。

2.4 一個簡單的ASP例子

緊接上一章：鳥(通常)會飛,但企鵝是一種不會飛的鳥。當咱們知道名爲tweety的個體的一些信息(它是小鳥,或進一步,它是企鵝)時,能夠經過ASP推理它是否會飛:

 

此程序惟一的回答集爲{penguin(tweety),bird(tweety),nfly(tweety)),即得出結論tweety不會飛。

 

若是從上面的程序中去掉事實penguin(tweety), 即只知道tweety是鳥,則新程序惟一的回答集爲{bird(tweety),fly(tweety))。

 

即在只告訴tweety是鳥的狀況,得出結論tweety會飛。該例子代表ASP能夠合理刻畫常識推理。