在数理逻辑中，线性逻辑是一种亚结构逻辑，它拒绝了传统逻辑中的“弱化”和“收缩”结构规则。线性逻辑的核心理念是将假设视为资源，这意味着在证明过程中，所有假设必须被精确地使用一次。这与经典逻辑或直觉逻辑形成对比，后者以真理为基础，允许多次自由使用同一真理。线性逻辑由法国数学家让·伊夫·吉拉德（Jean-Yves Girard）于1987年提出。

线性逻辑

例如，从命题 A 和 A ⇒ B 能按如下步骤得出结果 A ∧ B:

(1) 在假定 A 和 A ⇒ B 上应用肯定前件(或蕴涵除去)得到结论 B。

(2) A 和 (1) 的合取的得到结论 A ∧ B。

这经常被符号化表示为相继式: A, A ⇒ B \u003c数学\u003e\vdash\u003c/math\u003e B。在上述证明中"消费"了 A 为真的事实；这种真理的"自由"通常是在形式化数学中所需要的。

但是，真理经常在应用于关于这个世界的陈述的时候太抽象或不实用。比如，假设我有一夸脱的牛奶，我能用它制作一磅奶酪。如果我决定把我的所有牛奶都制成奶酪，我就不能下结论说我有牛奶和奶酪二者。上面的逻辑模式让我们得到结论：牛奶, 牛奶⇒奶酪\u003cmath\u003e\vdash\u003c/math\u003e牛奶∧奶酪(这里的牛奶表示命题 "我有一夸脱牛奶"，等等)。普通逻辑建模这个活动失败是由于牛奶、奶酪一般是资源：资源的数量不像真理是可以随意使用和支配的自由事实，而是必须在所有"状态变更"中仔细计量的。关于牛奶制奶酪活动的准确陈述是:

从一夸脱牛奶和从一夸脱牛奶转换出一磅奶酪的过程，我们获得一磅奶酪。

在线性逻辑中我们写为: 牛奶, 牛奶奶酪\u003c数学\u003e\Vdash\u003c/math\u003e奶酪，使用了不同的连结词(替代了 ⇒) 和不同的逻辑蕴涵符号。

线形逻辑由法国数学家 Jean-Yves Girard 在1987年提出。