缺省邏輯

缺省邏輯是邏輯學家Ray Reiter（英語：Ray Reiter）提出的用來形式化有缺省假定的推理的非單調邏輯。

標準邏輯只能表達某個事物為真或某個事物為假，但類似於「缺省的，某個事物是真的」的事實則可以使用缺省邏輯進行表達。推理經常會涉及到在多數時候是真但不總是真的事實，而缺省邏輯則可以解決這樣的推理問題。

經典的例子是：「鳥通常會飛」。這個規則可以在標準邏輯中表達為：要麼「所有鳥都會飛」——這與企鵝不會飛的事實相矛盾；要麼「除了企鵝、鴕鳥...的所有鳥都會飛」——這又要求規則逐一指定出所有的例外。缺省邏輯致力於將這樣的推理規則形式化，而不需要明確提及所有的例外。

缺省邏輯的語法

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

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

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

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

例子

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

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

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

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

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

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

${\displaystyle {\frac {:{\neg }F}{{\neg }F}}}$

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

限制

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

缺省邏輯的語義

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

${\displaystyle \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 }$

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

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

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

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

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

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

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

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

蘊涵

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

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

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

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

可供選擇的語義

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

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

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

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

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

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

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

缺省邏輯的變體

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

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

• 積累缺省邏輯
• 委託假定缺省邏輯
• 准缺省邏輯

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

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

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

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

轉換

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

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

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

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

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

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

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

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

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

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

複雜性

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

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

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

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

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

模型檢查：決定一個命題釋義是否是一個命題缺省理論的擴展的模型是${\displaystyle 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.