線性邏輯

數理邏輯中,線性邏輯是拒絕弱化和收縮的結構規則的一種亞結構邏輯。對此解釋是假設是資源: 在證明中所有假設必須被消費精確一次。這區別於平常的邏輯比如經典邏輯或直覺邏輯,那裡統治判斷是真理,它可以按需要被自由的使用多次。

基本介紹

  • 中文名:線性邏輯
  • 性質:邏輯
  • 屬性:線性
  • 來自: 維客
線性邏輯
來自 維客
Jump to: navigation, search
例如,從命題 A 和 A ⇒ B 能按如下步驟得出結果 A ∧ B:
(1) 在假定 A 和 A ⇒ B 上套用肯定前件(或蘊涵除去)得到結論 B。
(2) A 和 (1) 的合取的得到結論 A ∧ B。
這經常被符號化表示為相繼式: A, A ⇒ B <math>\vdash</math> B。在上述證明中"消費"了 A 為真的事實;這種真理的"自由"通常是在形式化數學中所需要的。
但是,真理經常在套用於關於這個世界的陳述的時候太抽象或不實用。比如,假設我有一夸脫的牛奶,我能用它製作一磅乳酪。如果我決定把我的所有牛奶都製成乳酪,我就不能下結論說我有牛奶和乳酪二者! 上面的邏輯模式讓我們得到結論:牛奶, 牛奶⇒乳酪<math>\vdash</math>牛奶∧乳酪(這裡的牛奶表示命題 "我有一夸脫牛奶",等等)。普通邏輯建模這個活動失敗是由於牛奶、乳酪一般是資源:資源的數量不像真理是可以隨意使用和支配的自由事實,而是必須在所有"狀態變更"中仔細計量的。關於牛奶制乳酪活動的準確陳述是:
從一夸脫牛奶和從一夸脫牛奶轉換出一磅乳酪的過程,我們獲得一磅乳酪。
線上性邏輯中我們寫為: 牛奶, 牛奶乳酪<math>\Vdash</math>乳酪,使用了不同的連結詞(替代了 ⇒) 和不同的邏輯蘊涵符號。
線形邏輯由法國數學家 Jean-Yves Girard 在1987年提出。
[編輯]參見

相關詞條

熱門詞條

聯絡我們