可廢止邏輯檢視原始碼討論檢視歷史
| 可廢止邏輯 |
|
可廢止邏輯是Donald Nute提出的用來形式化可廢止推理的非單調邏輯。[1]
簡介
可廢止邏輯是Donald Nute提出的用來形式化可廢止推理的非單調邏輯。在缺省邏輯中，有三種不同類型的命題： 硬性規則：指定一個事實總是另一個事實的結論； 可廢止規則：指定一個事實典型的是另一個事實的結論； 廢止者：指定對可廢止規則的例外。 可以在可廢止規則和廢止者上給出優先級。在演繹期間，硬性規則總是應用，而可廢止規則只能在沒有更高優先級的廢止者指定它不能用的時候應用。 常識（英語：Common knowledge）、普遍知識（General knowledge）或基本知識（Essential knowledge）是指普通社會上智力正常的人應有的知識。
非單調邏輯
非單調邏輯（英語：Non-monotonic logic）是（在前提的集合和單一的句子之間的）推論關係不是單調遞增的形式邏輯。 與單調推理（經典邏輯）相對，非單調推理是指知識庫加入新知識後，原有的推論會被推翻的邏輯。也就是說，知識庫的推論不隨着知識增長而增長，即非單調遞增。這時，必須使用某種正確的維持機制，確保推理繼續進行。因此，非單調推理多是在知識不完全的情況下發生的。 多數形式邏輯都有單調性的推論關係，就是說，如果一個句子可以從前提的集合中推理出來，則它也可以從把這個前提集合作為子集包含的任何前提集合中推理出來，這意味着向理論增加一個公式永不引起它的推論集合的減小。在直覺上，單調性指示出學習一些新知識不能減小已知知識的集合。單調邏輯不能處理各種推理任務比如缺省推理（事實可以是已知的，只是因為缺乏反面的證據）、溯因推理（事實只按最合適的解釋演繹出來）、關於知識的推理（在事實變成已知的時候，對一個事實的無知必須被撤消），和信念修正（新知識可以和舊信念矛盾。） 目前對於非單調推理的研究一般有兩種途徑： 一種方法認為經典邏輯對於研究非單調推理明顯有不足的地方，因此最好是建立新的語義機制跟邏輯系統。在此基礎上進行非單調推理的研究以解決一些問題，例如Reiter的缺省邏輯和Moore的自動認識邏輯，還有擴充邏輯程序（英語：extended logic program）。 另一種觀點與此正好相反，堅持這種觀點的人認為，在經典邏輯框架下研究非單調推理是完全可行的，關鍵是怎麼使用經典邏輯。例如封閉世界假設，McCarthy的限定推理（Circumscription）和Poole提出的假設推理（default reasoning）。
缺省邏輯
缺省邏輯是Ray Reiter提出的用來形式化有缺省假定的推理的非單調邏輯。 缺省邏輯可以表達像「缺省的，某個事物是真的」的事實；相反的，標準邏輯只能表達某個事物為真或某個事物為假。這是一個問題，因為推理經常涉及在多數時候是真但不總是真的事實的推理。經典的例子是：「鳥通常會飛」。這個規則可以在標準邏輯中表達為要麼「所有鳥都會飛」，這與企鵝不會飛的事實相矛盾；要麼「除了企鵝、鴕鳥...的所有鳥都會飛」，這要求規則指定出所有的例外。缺省邏輯致力於形式化像這樣的推理規則，而不需要明確提及所有的例外。
可廢止推理
可廢止推理是對推理形式的研究，它儘管令人信服，卻不如演繹推理那麼形式化和嚴格。它已經在哲學中，和最近在人工智能中討論過了。 其他演繹推理的替代者包括歸納推理和逆推推理。它們在傳統上不被術語「可廢止推理」所覆蓋。