來源：互聯網
在數理邏輯中，線性邏輯是一種亞結構邏輯，它拒絕了傳統邏輯中的“弱化”和“收縮”結構規則。線性邏輯的核心理念是將假設視為資源，這意味著在證明過程中，所有假設必須被精確地使用一次。這與經典邏輯或直覺邏輯形成對比，后者以真理為基礎，允許多次自由使用同一真理。線性邏輯由法國數學家讓·伊夫·吉拉德（Jean-Yves Girard）于1987年提出。
基本介紹
線性邏輯
例如，從命題 A 和 A ? B 能按如下步驟得出結果 A ∧ B:
(1) 在假定 A 和 A ? B 上應用肯定前件(或蘊涵除去)得到結論 B。
(2) A 和 (1) 的合取的得到結論 A ∧ B。
這經常被符號化表示為相繼式: A, A ? B <數學>\vdash B。在上述證明中"消費"了 A 為真的事實；這種真理的"自由"通常是在形式化數學中所需要的。
但是，真理經常在應用于關于這個世界的陳述的時候太抽象或不實用。比如，假設我有一夸脫的牛奶，我能用它制作一磅奶酪。如果我決定把我的所有牛奶都制成奶酪，我就不能下結論說我有牛奶和奶酪二者。上面的邏輯模式讓我們得到結論：牛奶, 牛奶?奶酪牛奶∧奶酪(這里的牛奶表示命題 "我有一夸脫牛奶"，等等)。普通邏輯建模這個活動失敗是由于牛奶、奶酪一般是資源：資源的數量不像真理是可以隨意使用和支配的自由事實，而是必須在所有"狀態變更"中仔細計量的。關于牛奶制奶酪活動的準確陳述是:
從一夸脫牛奶和從一夸脫牛奶轉換出一磅奶酪的過程，我們獲得一磅奶酪。
在線性邏輯中我們寫為: 牛奶, 牛奶奶酪<數學>\Vdash奶酪，使用了不同的連結詞(替代了 ?) 和不同的邏輯蘊涵符號。
線形邏輯由法國數學家 Jean-Yves Girard 在1987年提出。
參考資料 >