回答集編程
回答集編程是語法上類似傳統邏輯編程而語意上密切於非單調邏輯的一種聲明式編程。在傳統邏輯編程和回答集編程之間的主要區別是如何表示否定為失敗。在傳統邏輯編程中,否定為失敗指示推導失敗;在回答集編程中,它指示一個文字的一致性。
語法
編輯回答集編程由規則的集合構成,每個規則由一個頭部和一個後部構成:
規則的頭部和後部二者都是文字的集合,每個文字都是可能被否定的原子。與傳統邏輯程式相反,原子都是命題而不是一階的,並且可以使用兩種形式的否定去否定它們: 經典否定(指示為 )和否定為失敗(指示為 )。文字要麼是原子要麼是(使用經典否定)否定的原子。下面是一個例子程式:
依據第一個規則, 是真,只要 是真,並且 可以被假定為假而不產生矛盾。
語意
編輯程式的語意基於它的回答集,每個回答集都是文字集合。對於不包含否定為失敗的程式,程式的語意基於閉包和最小性的概念:
- 程式在一個文字集合下閉合,如果這個集合包含至少一個在某個規則的頭部中的文字,而總是包含在規則的體部中的所有文字。
- 文字集合是一個程式回答集,如果在這個程式閉合於的文字集合中、它(在集合的容量(containment)上)是最小化的。
如果程式包含使用否定為失敗否定的一些文字,語意要求額外的簡約概念:
- 一個程式在一個文字集合下的簡約是通過對每個規則進行下列變更而獲得的程式:
- 除去在頭部中的、使用否定為失敗否定的並且在集合中的所有文字;
- 除去在後部中的、使用否定為失敗否定的並且在集合中不包含的所有文字;
- 刪除整個規則,如果在應用完上面兩個規則之後,它仍然包含(使用否定為失敗)否定的原子。
文字集合是一個程式的回答集,如果它是這個程式在這個集合自身下的簡約的回答集。換句話說,可以通過執行下列非確定性的演算法來計算一個回答集可以:
选择文字集合 L; 计算程序 P 在 L 下的简约 PL; 如果 L 是 PL 所闭合的最小化文字集合则 输出 L
最初的文字集合 L 的選擇是非確定性的。確定 L 是否為一個回答集的演算法,首先計算程式在 L 下的簡約,並接着檢查 L 是否是這個無否定為失敗的程式的回答集。
一個回答集程式可以有零個、一個或多個回答集。一個程式蘊涵一個文字,如果它的所有的回答集都包含這個文字。
比較、複雜性和實現
編輯與 Prolog 相反,回答集程式的語意不依賴於規則的求值和原子在每個規則中的特定次序。
檢查一個程式的回答集的存在性的複雜性,和檢查一個程式是否蘊涵一個文字複雜性,範圍是從 P 到多項式層次的第二級,依賴於一個程式可以滿足也可以不滿足的一組條件(就是說分層、頭部中的析取)。
實現了回答集編程的三個系統是:smodels、dlv 和 cmodels。
參見
編輯參照
編輯- T. Eiter, N. Leone, C. Mateis, G. Pfeifer, F. Scarcello (1998). The KR System dlv: Progress Report, Comparisons and Benchmarks. In Proceedings of the Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR'98): 406-417
- V. Lifschitz (2002). Answer set programming and plan generation. Artificial Intelligence. 138(1-2): 39-54. doi:10.1016/S0004-3702(02)00186-8
- I. Niemela, P. Simons, T. Syrjanen (2000). Smodels: A System for Answer Set Programming. CoRR cs.AI/0003033
外部連結
編輯- Working group on Answer Set Programming
- The DLV Project(頁面存檔備份,存於互聯網檔案館)
- Smodels(頁面存檔備份,存於互聯網檔案館)
- CMODELS(頁面存檔備份,存於互聯網檔案館)