預設邏輯

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

基本介紹

  • 中文名:預設邏輯
  • 預設邏輯是:Ray Reiter
  • 簡介:正文簡介
  • 邏輯:公式命題邏輯
預設邏輯的變體,轉換,複雜性,實現,

預設邏輯的變體

預設邏輯的下列變體同最初的語法和語義二者有所區別。
斷言變體:斷言是由一個公式和一個公式的集合構成的
對。這種對指示P是真,當公式
已經被假定為一致於證明P為真的時候。一個斷言預設理論由叫做背景理論的斷言理論(斷言公式的集合)和按原始語法定義的預設的集合構成。當一個預設套用於斷言理論的時候,把由它的結論和它的論據合成的對增加到這個理論。下列語義使用了斷言理論:
  • 積累預設邏輯
  • 委託假定預設邏輯
  • 準預設邏輯
弱擴展:不再檢查前件在由背景理論和已套用的預設的結論構成的理論中是否是有效的,檢查前件在將要生成的擴展中的有效性;換句話說,生成擴展的算法開始於猜測一個理論並使用它代替背景理論;從擴展生成的過程得到的結果實際上是一個擴展,只在它等價於在開始時所猜測的理論的時候。預設邏輯的這個變體在原理上與自動認識邏輯有關,在那裡理論
有一種模型,在其中x是真,只是因為假定
為真,公式
支持這個初始假定。
  • 析取預設邏輯:預設的結論是公式的集合而不是單一的公式。在套用預設的時候,至少其中一個結論被非確定性的選擇為真。
  • 預設上的優先權:可以明確的指定預設的相對優先權;在可以套用於一個理論的預設之間,只有最高優先權的可以套用。預設邏輯的某些語義不要求明確指定優先權;而是更多特殊性(在更少情況下可套用的)預設優於更少特殊性的預設。
  • 統計變體:統計預設對預設附加錯誤頻率的上限;換句話說,預設被假定為是不正確的推理規則,套用它的次數到了這個分數的時候。

轉換

預設理論可以被轉換成其他邏輯的理論或反之。轉換要考慮下列條件:
  • 結論保持:最初和轉換後的理論有同樣的(命題)結論;
  • 忠實:這個條件有意義只在如下轉換的時候,在預設邏輯的兩個變體之間、或在預設邏輯和在其中類似於擴展的概念比如模態邏輯中模型存在的邏輯之間;一個轉換是忠實的,如果在最初和轉換後的理論的擴展(或模型)之間存在一個映射(典型的是雙射);
  • 模組化:從預設邏輯到其他邏輯的轉換是模組化的,如果預設和背景理論可以分開轉換;此外,向背景理論增加公式只導致向轉換的結果增加新公式;
  • 同字母表:最初和轉換後的理論建立在相同的字母表之上;
  • 多項式:轉換的運行時間和生成的理論的大小要求是最初理論的多項式。
轉換典型的要求忠實或至少是結論保持,而模組化和同字母表的條件有時被忽略。
在命題預設邏輯和下列邏輯之間的轉換已經研究過了:
  • 經典命題邏輯;
  • 自動認識邏輯;
  • 限定於被正規理論的命題預設邏輯;
  • 預設邏輯的可作為替代的語義;
  • 界限。
轉換存在與否依賴於施加那種條件。從命題預設邏輯到經典命題邏輯的轉換不能總是生成多項式大小的命題理論,除非多項式層次瓦解。到自動認識邏輯的轉換存在與否依賴於是否要求模組性或使用相同的字母表。

複雜性

關於預設邏輯的下列問題的計算複雜性是已知的:
  • 擴展的存在性:決定一個命題預設理論是否有至少一個擴展是{\displaystyle NP^{NP}}-完全的;
  • 懷疑的蘊涵:決定一個命題預設理論是否懷疑的蘊涵一個命題公式是{\displaystyle co-NP^{NP}}-完全的;
  • 輕信的蘊涵:決定一個命題預設理論是否輕信的蘊涵一個命題公式是{\displaystyle NP^{NP}}-完全的;
  • 擴展檢查:決定一個命題公式是否等價於一個命題預設理論的擴展是{\displaystyle P^{NP[log]}}-完全的;
  • 模型檢查:決定一個命題釋義是否是一個命題預設理論的擴展的模型是{\displaystyle NP^{NP}}-完全的。

實現

有兩個系統實現了預設邏輯:DeReS和XRay

相關詞條

熱門詞條

聯絡我們