在数理逻辑中，线性逻辑是拒绝“弱化”和“收缩”的结构规则的一种亚结构逻辑。对此解释是“假设是资源”:在证明中所有假设必须被消费“精确一次”。这区别于平常的逻辑比如经典逻辑或直觉逻辑，那里统治判断是“真理”，它可以按需要被自由的使用多次。例如，从命题A和A ⇒ B能按如下步骤得出结果A ∧ B:
- （1）在假定A和A ⇒ B上应用肯定前件（或蕴涵除去）得到结论B。
- （2）A和（1）的合取的得到结论A ∧ B。
这经常被符号化表示为相继式：A, A ⇒ B B。在上述证明中"消费"了A为真的事实；这种真理的"自由"通常是在形式化数学中所需要的。
但是，真理经常在应用于关于这个世界的陈述的时候太抽象或不实用。比如，假设我有一夸脱的牛奶，我能用它制作一磅奶酪。如果我决定把我的所有牛奶都制成奶酪，我就不能下结论说我有牛奶和奶酪二者! 上面的逻辑模式让我们得到结论：牛奶, 牛奶⇒奶酪牛奶∧奶酪（这里的牛奶表示命题"我有一夸脱牛奶"，等等）。普通逻辑建模这个活动失败是由于牛奶、奶酪一般是资源：资源的数量不像真理是可以随意使用和支配的自由事实，而是必须在所有"状态变更"中仔细计量的。关于牛奶制奶酪活动的准确陈述是：
- 从一夸脱牛奶和从一夸脱牛奶转换出一磅奶酪的过程，我们获得一磅奶酪。
在线性逻辑中我们写为：牛奶, 牛奶奶酪奶酪，使用了不同的连结词（替代了⇒）和不同的逻辑蕴涵符号。
线性逻辑由法国数学家让·伊夫·吉拉德（Jean-Yves Girard）在1987年提出。
参见 编辑
外部链接 编辑
- Patrick Lincoln （页面存档备份，存于互联网档案馆）'s excellent Introduction to Linear Logic（Postscript）
线性逻辑, 在数理逻辑中, 是拒绝, 弱化, 收缩, 的结构规则的一种亚结构逻辑, 对此解释是, 假设是资源, 在证明中所有假设必须被消费, 精确一次, 这区别于平常的逻辑比如经典逻辑或直觉逻辑, 那里统治判断是, 真理, 它可以按需要被自由的使用多次, 例如, 从命题a和a, b能按如下步骤得出结果a, 在假定a和a, b上应用肯定前件, 或蕴涵除去, 得到结论b, a和, 的合取的得到结论a, 这经常被符号化表示为相继式, displaystyle, vdash, 在上述证明中, 消费, 了a为真的事实, 这种. 在数理逻辑中 线性逻辑是拒绝 弱化 和 收缩 的结构规则的一种亚结构逻辑 对此解释是 假设是资源 在证明中所有假设必须被消费 精确一次 这区别于平常的逻辑比如经典逻辑或直觉逻辑 那里统治判断是 真理 它可以按需要被自由的使用多次 例如 从命题A和A B能按如下步骤得出结果A B 1 在假定A和A B上应用肯定前件 或蕴涵除去 得到结论B 2 A和 1 的合取的得到结论A B 这经常被符号化表示为相继式 A A B displaystyle vdash B 在上述证明中 消费 了A为真的事实 这种真理的 自由 通常是在形式化数学中所需要的 但是 真理经常在应用于关于这个世界的陈述的时候太抽象或不实用 比如 假设我有一夸脱的牛奶 我能用它制作一磅奶酪 如果我决定把我的所有牛奶都制成奶酪 我就不能下结论说我有牛奶和奶酪二者 上面的逻辑模式让我们得到结论 牛奶 牛奶 奶酪 displaystyle vdash 牛奶 奶酪 这里的牛奶表示命题 我有一夸脱牛奶 等等 普通逻辑建模这个活动失败是由于牛奶 奶酪一般是资源 资源的数量不像真理是可以随意使用和支配的自由事实 而是必须在所有 状态变更 中仔细计量的 关于牛奶制奶酪活动的准确陈述是 从一夸脱牛奶和从一夸脱牛奶转换出一磅奶酪的过程 我们获得一磅奶酪 在线性逻辑中我们写为 牛奶 牛奶 奶酪 displaystyle Vdash 奶酪 使用了不同的连结词 替代了 和不同的逻辑蕴涵符号 线性逻辑由法国数学家让 伊夫 吉拉德 Jean Yves Girard 在1987年提出 参见 编辑证明网络 博弈语义 直觉逻辑 可计算性逻辑 直觉主义 BHK释义 直觉类型论 经典逻辑 中间逻辑 构造性证明 Curry Howard对应 可计算性逻辑外部链接 编辑Patrick Lincoln 页面存档备份 存于互联网档案馆 s excellent Introduction to Linear Logic Postscript nbsp 这是一篇與逻辑学相關的小作品 你可以通过编辑或修订扩充其内容 查论编 取自 https zh wikipedia org w index php title 线性逻辑 amp oldid 74643131, 维基百科，wiki，书籍，书籍，图书馆，
文章
，阅读，下载，免费，免费下载，mp3，视频，mp4，3gp， jpg，jpeg，gif，png，图片，音乐，歌曲，电影，书籍，游戏，游戏。