預設邏輯

預設邏輯是Ray Reiter提出的用來形式化有預設假定的推理的非單調邏輯。

預設邏輯可以表達像「預設的，某個事物是真的」的事實；相反的，標準邏輯只能表達某個事物為真或某個事物為假。這是一個問題，因為推理經常涉及在多數時候是真但不總是真的事實的推理。經典的例子是：「鳥通常會飛」。這個規則可以在標準邏輯中表達為要麼「所有鳥都會飛」，這與企鵝不會飛的事實相矛盾；要麼「除了企鵝、鴕鳥...的所有鳥都會飛」，這要求規則指定出所有的例外。預設邏輯致力於形式化像這樣的推理規則，而不需要明確提及所有的例外。

預設邏輯的語法[編輯]

預設理論是 $\langle D,W\rangle$ 對。 $W$ 是邏輯公式的集合，叫做背景理論，形式化的是確實已知的事實。 $D$ 是預設規則的集合，每個都有形式：

{\frac {Prerequisite:Justification_{1},...,Justification_{n}}{Conclusion}}

依據這種預設，如果我們相信 $Prerequisite$ （先決條件）是真的，並且每個 $Justification_{i}$ （論據）都相容於我們當前的信仰，我們導出信仰 $Conclusion$ （結論）是真的。

在 $W$ 中邏輯公式和在預設中的所有公被初始的假定為一階邏輯公式，但是它們潛在的可以是任意形式邏輯的公式。公式都是命題邏輯的情況是研究最多的。

例子[編輯]

預設規則「鳥通常會飛」被下列預設所形式化：

D=\left\{{\frac {Bird(X):Flies(X)}{Flies(X)}}\right\}

這個規則意味著，如果 $X$ 是鳥，並且可以假定它會飛，則我們得出結論它會飛。包含某些關於鳥的事實的背景理論在下面列出：

W = { Bird（禿鷲）, Bird（企鵝）, ¬ Flies（企鵝）, Flies（鷹）}。

依據這個預設規則，禿鷲會飛，因為前件Bird（禿鷲）是真的，並且論據Flies（禿鷲）與當前已知不矛盾。相反的，Bird（企鵝）不允許得出結論Flies（企鵝）:即使預設的前件Bird（企鵝）是真的，論據Flies（企鵝）與已知相矛盾。從這個背景理論和這個預設，不能得出結論Bird（鷹），因為預設規則只允許從Bird（X）推出Flies (X)，但不能反過來。從推論規則的結論推出前提是結論的一種解釋形式，這是溯因推理的目標。

常見的預設假定是不知道為真的東西都被相信是假的。這叫做封閉世界假定，並在預設邏輯中對每個事實 $F$ 使用像下列這樣的預設來形式化。

{\frac {:{\neg }F}{{\neg }F}}

例如，計算機語言Prolog在推導否定的時候，使用了某種程度的預設假定：如果否定的原子不能被證明為真，則它被假定為假。但是要注意，Prolog使用了所謂的否定為失敗：當解釋器必須求值原子 $\neg F$ 的時候，它嘗試證明 $F$ 是真，並如果這失敗了則結論為 $\neg F$ 是真。轉而在預設邏輯中，預設有 $\neg F$ 作為論據，它只能在 $\neg F$ 與當前知識一致的時候應用。

限制[編輯]

預設是無條件的或無先決條件的，如果它沒有先決條件（或者等價的說先決條件是重言式）。一個預設是正規的，如果它有等價於它的結論的一個單一論據。一個預設是超正規的，如果它是無條件的和正規的。一個預設是半正規的，如果它的所有論據都蘊涵它的結論。一個預設理論叫做無條件的、正規的、超正規的、或半正規的，如果它包含的所有預設分別都是無條件的、正規的、超正規的或半正規的。

預設邏輯的語義[編輯]

一個預設規則可以應用於一個理論，如果它的前件被這個理論所蘊涵，並且它的論據都一致於這個理論。預設規則的應用導致它的結論增加到這個理論。其他預設規則接著可以應用於結果的理論。當沒有預設規則可以應用於理論的時候，這個理論就叫做預設理論的擴展。預設規則可以按不同的次序應用，這可以導致不同的擴展。尼克森菱形例子是有兩個擴展的預設理論：

\left\langle \left\{{\frac {Republican(X):\neg Pacifist(X)}{\neg Pacifist(X)}},{\frac {Quaker(X):Pacifist(X)}{Pacifist(X)}}\right\},\left\{Republican(Nixon),Quaker(Nixon)\right\}\right\rangle

因為尼克森既是共和黨的人又是教友會的人，兩個預設都可以應用。但是，應用第一個預設導致尼克森是不愛好和平的人的結論。以同樣的方式，應用第二個預設我們得出尼克森是愛好和平的人，因此使第一個預設不可應用。這種特定的預設理論因此有兩個擴展，其中一個 $Pacifist(Nixon)$ 是真，而另一個 $Pacifist(Nixon)$ 是假。

預設邏輯的最初的語義基於的是函數的不動點。下面是一個等價的算法定義。如果預設包含有自由變量的公式，它被認為表示通過向所有這些變量給出一個值而得到所有預設的集合。預設 ${\frac {\alpha :\beta _{1},\ldots ,\beta _{n}}{\gamma }}$ 對命題理論 $T$ 是可應用的，如果 $T\models \alpha$ 並且所有理論 $T\cup \{\beta _{i}\}$ 是一致的。這個預設對 $T$ 的應用得到理論 $T\cup \{\gamma \}$ 。通過應用下列算法可以生成一個擴展：

T=W           /* 当前理论*/
A=0           /* 迄今应用的缺省的集合*/
 
              /* 应用一序列的缺省*/
while有个不在A中的缺省d对于T是可应用的
  增加d的结论到T
  增加d到A
 
              /* 最终的一致性检查*/
if 
  for所有缺省d in A
    T一致于d的所有论据
then
  输出T

這個算法是非確定性的，因為對於給定的理論 $T$ 有很多預設可以應用。在尼克森菱形的例子中，第一個預設的應用導致第二個預設不能應用的一個理論，反之亦然。作為結果，可以生成兩個擴展：在其中一個里尼克森是愛好和平的人和另一個里尼克森不愛好和平的人。

最終的所有已經應用的預設的論據的一致性檢查使某些理論不能有任何擴展。特別是，這發生在對於可應用的預設的所有序列這個檢查都失敗的時候。下列預設理論就沒有擴展：

\left\langle \left\{{\frac {:A(b)}{\neg A(b)}}\right\},\emptyset \right\rangle

因為 $A(b)$ 一致於預設被應用到的背景理論，所以得出結論 $A(b)$ 是假的。但是這個結果破壞了應用第一個預設所有做的假定。因此，這個理論沒有擴展。

正規的預設理論保證至少有一個擴展。進一步的，正規預設理論的擴展是相互矛盾的。

蘊涵[編輯]

預設理論可以有零個、一個或更多的擴展。從一個預設理論到一個公式的蘊涵可以用兩種方式定義：

懷疑的：一個公式被一個預設理論所蘊涵，如果它被它的所有擴展所蘊涵；

輕信的：一個公式被一個預設理論所蘊涵，如果它被它的至少一個擴展所蘊涵；

例如，尼克森菱形例子有兩個擴展，在其一中尼克森是愛好和平的人在另一個中他不是愛好和平的人。因此，Pacifist（尼克森）和 ¬ Pacifist（尼克森）都不被懷疑的蘊涵，而二者都被輕信的蘊涵。如這個例子展示的，預設理論的輕信結論可以相互矛盾。

可供選擇的語義[編輯]

預設邏輯下列可供選擇的語義都是基於同最初一樣的語法。

正當的：同最初的語義不同之處是，如果預設使集合 $T$ 矛盾於已應用的預設的一個論據，則不應用這個預設；

簡明的：只在預設的結論沒有被 $T$ 所蘊涵的時候應用它（精確的定義更加複雜，這只是背後的想法）；

約束的：只在背景理論和所有應用的（包括這個）預設的論據和結論所構成集合是一致的時候應用它；

合理的：類似於約束的預設邏輯，但是在一致性檢查中不考慮預設的結論；

謹慎的：預設可以應用但相互衝突（像尼克森菱形的例子）的不應用。

正當的和約束的語義為所有的預設理論指派至少一個擴展。

預設邏輯的變體[編輯]

預設邏輯的下列變體同最初的語法和語義二者有所區別。

斷言變體：斷言是由一個公式和一個公式的集合構成的 $\langle p:\{r_{1},\ldots ,r_{n}\}\rangle$ 對。這種對指示 $p$ 是真，當公式 $r_{1},\ldots ,r_{n}$ 已經被假定為一致於證明 $p$ 為真的時候。一個斷言預設理論由叫做背景理論的斷言理論（斷言公式的集合）和按原始語法定義的預設的集合構成。當一個預設應用於斷言理論的時候，把由它的結論和它的論據合成的對增加到這個理論。下列語義使用了斷言理論：

積累預設邏輯
委託假定預設邏輯
准預設邏輯

弱擴展：不再檢查前件在由背景理論和已應用的預設的結論構成的理論中是否是有效的，檢查前件在將要生成的擴展中的有效性；換句話說，生成擴展的算法開始於猜測一個理論並使用它代替背景理論；從擴展生成的過程得到的結果實際上是一個擴展，只在它等價於在開始時所猜測的理論的時候。預設邏輯的這個變體在原理上與自動認識邏輯有關，在那裡理論 $\Box x\rightarrow x$ 有一種模型，在其中 $x$ 是真，只是因為假定 $\Box x$ 為真，公式 $\Box x\rightarrow x$ 支持這個初始假定。

析取預設邏輯：預設的結論是公式的集合而不是單一的公式。在應用預設的時候，至少其中一個結論被非確定性的選擇為真。

預設上的優先級：可以明確的指定預設的相對優先級；在可以應用於一個理論的預設之間，只有最高優先級的可以應用。預設邏輯的某些語義不要求明確指定優先級；而是更多特殊性（在更少情況下可應用的）預設優於更少特殊性的預設。

統計變體：統計預設對預設附加錯誤頻率的上限；換句話說，預設被假定為是不正確的推理規則，應用它的次數到了這個分數的時候。

轉換[編輯]

預設理論可以被轉換成其他邏輯的理論或反之。轉換要考慮下列條件：

結論保持：最初和轉換後的理論有同樣的（命題）結論；

忠實：這個條件有意義只在如下轉換的時候，在預設邏輯的兩個變體之間、或在預設邏輯和在其中類似於擴展的概念比如模態邏輯中模型存在的邏輯之間；一個轉換是忠實的，如果在最初和轉換後的理論的擴展（或模型）之間存在一個映射（典型的是雙射）；

模塊化：從預設邏輯到其他邏輯的轉換是模塊化的，如果預設和背景理論可以分開轉換；此外，向背景理論增加公式只導致向轉換的結果增加新公式；

同字母表：最初和轉換後的理論建立在相同的字母表之上；

多項式：轉換的運行時間和生成的理論的大小要求是最初理論的多項式。

轉換典型的要求忠實或至少是結論保持，而模塊化和同字母表的條件有時被忽略。

在命題預設邏輯和下列邏輯之間的轉換已經研究過了：

經典命題邏輯；
自動認識邏輯；
限定於被正規理論的命題預設邏輯；
預設邏輯的可作為替代的語義；
界限。

轉換存在與否依賴於施加那種條件。從命題預設邏輯到經典命題邏輯的轉換不能總是生成多項式大小的命題理論，除非多項式層次瓦解。到自動認識邏輯的轉換存在與否依賴於是否要求模塊性或使用相同的字母表。

複雜性[編輯]

關於預設邏輯的下列問題的計算複雜性是已知的：

擴展的存在性：決定一個命題預設理論是否有至少一個擴展是 $NP^{NP}$ -完全的；

懷疑的蘊涵：決定一個命題預設理論是否懷疑的蘊涵一個命題公式是 $co-NP^{NP}$ -完全的；

輕信的蘊涵：決定一個命題預設理論是否輕信的蘊涵一個命題公式是 $NP^{NP}$ -完全的；

擴展檢查：決定一個命題公式是否等價於一個命題預設理論的擴展是 $P^{NP[log]}$ -完全的；

模型檢查：決定一個命題釋義是否是一個命題預設理論的擴展的模型是 $NP^{NP}$ -完全的。

實現[編輯]

有兩個系統實現了預設邏輯：DeReS^{[永久失效連結]}和XRay。

參見[編輯]

引用[編輯]

G. Antoniou (1999). A tutorial on default logics. ACM Computing Surveys, 31 (4):337-359.

M. Cadoli, F. M. Donini, P. Liberatore, and M. Schaerf (2000). Space efficiency of propositional knowledge representation formalisms. Journal of Artificial Intelligence Research, 13:1-31.

P. Cholewinski, V. Marek, and M. Truszczynski (1996). Default reasoning system DeReS. In Proceedings of the Fifth International Conference on the Principles of Knowledge Representation and Reasoning（KR'96）, pages 518-528.

J. Delgrande and T. Schaub (2003). On the relation between Reiter's default logic and its (major) variants. In Seventh European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU 2003), pages 452-463.

J. P. Delgrande, T. Schaub, and W. K. Jackson (1994). Alternative approaches to default logic. Artificial Intelligence, 70:167-237.

G. Gottlob (1992). Complexity results for nonmonotonic logics. Journal of Logic and Computation, 2:397-425.

G. Gottlob (1995). Translating default logic into standard autoepistemic logic. Journal of the ACM, 42:711-740.

T. Imielinski (1987). Results on translating defaults to circumscription. Artificial Intelligence, 32:131-146.

T. Janhunen (1998). On the intertranslatability of autoepistemic, default and priority logics, and parallel circumscription. In Proceedings of the Sixth European Workshop on Logics in Artificial Intelligence（JELIA'98）, pages 216-232.

T. Janhunen (2003). Evaluating the effect of semi-normality on the expressiveness of defaults. Artificial Intelligence, 144:233-250.

P. Liberatore and M. Schaerf (1998). The complexity of model checking for propositional default logics. In Proceedings of the Thirteenth European Conference on Artificial Intelligence（ECAI'98）, pages 18-22.

W. Lukaszewicz (1988). Considerations on default logic: an alternative approach. Computational Intelligence, 4 (1):1-16.

W. Marek and M. Truszczynski (1993). Nonmonotonic Logics: Context-Dependent Reasoning. Springer.

A. Mikitiuk and M. Truszczynski (1995). Constrained and rational default logics. In Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence（IJCAI'95）, pages 1509-1517.

R. Reiter (1980). A logic for default reasoning. Artificial Intelligence, 13:81-132.

T. Schaub, S. Brüning, and P. Nicolas (1996). XRay: A prolog technology theorem prover for default reasoning: A system description. In Proceedings of the Thirteenth International Conference on Automated Deduction（CADE'96）, pages 293-297.

外部連結[編輯]

Schmidt, Charles F. Default Logic. Retrieved August 10th. 2004.

Ramsay, Allan (1999). Default Logic. Retrieved August 10th. 2004.

Defeasible reasoning （頁面存檔備份，存於網際網路檔案館）. Stanford Encyclopedia of Philosophy.