线性逻辑

✍ dations ◷ 2024-11-05 19:00:00 #线性逻辑

在数理逻辑中，线性逻辑是拒绝“弱化”和“收缩”的结构规则的一种亚结构逻辑。对此解释是“假设是资源”:在证明中所有假设必须被消费“精确一次”。这区别于平常的逻辑比如经典逻辑或直觉逻辑，那里统治判断是“真理”，它可以按需要被自由的使用多次。例如，从命题A和A ⇒ B能按如下步骤得出结果A ∧ B:这经常被符号化表示为相继式：A, A ⇒ B ⊢ {displaystyle vdash } B。在上述证明中"消费"了A为真的事实；这种真理的"自由"通常是在形式化数学中所需要的。但是，真理经常在应用于关于这个世界的陈述的时候太抽象或不实用。比如，假设我有一夸脱的牛奶，我能用它制作一磅奶酪。如果我决定把我的所有牛奶都制成奶酪，我就不能下结论说我有牛奶和奶酪二者! 上面的逻辑模式让我们得到结论：牛奶, 牛奶⇒奶酪 ⊢ {displaystyle vdash } 牛奶∧奶酪（这里的牛奶表示命题"我有一夸脱牛奶"，等等）。普通逻辑建模这个活动失败是由于牛奶、奶酪一般是资源：资源的数量不像真理是可以随意使用和支配的自由事实，而是必须在所有"状态变更"中仔细计量的。关于牛奶制奶酪活动的准确陈述是：在线性逻辑中我们写为：牛奶, 牛奶奶酪 ⊩ {displaystyle Vdash } 奶酪，使用了不同的连结词（替代了⇒）和不同的逻辑蕴涵符号。线性逻辑由法国数学家Jean-Yves Girard在1987年提出。

相关

AAT艺术与建筑索引典（英语：Art & Architecture Thesaurus，AAT）是一个用来描述关于艺术、建筑和物质文化项目的受控词表。AAT收录各种通用术语，如“大教堂”，但不收录专有名词，如“圣母
注射注射（英文：Injection）俗称打针，是一种利用注射器与针头穿过皮肤，并将液体送入身体内的方法。是一种给药途径，注射所预期的作用位置，不一定是受注射的位置。目前有多种不同的注射方
叶蜂叶蜂总科（学名：Tenthredinoidea）是广腰亚目下的一个大总科，于全球包括了至少7000种品种，特别是分布广泛的叶蜂科。目前已知的幼虫均为植食性，有些种类被视为害虫的一种。叶蜂为小
小支气管小支气管是空气由鼻或口到肺的肺气泡之间的通道，而分支下层不再包含软骨或腺体。小支气管是支气管的分支。小支气管具有微丝血管。Template:Lower respiratory system anatom
空间分析空间分析是指利用拓扑关系、几何关系或地理属性等来研究事物的一种技术。严格上说空间分析指的并不是一种技术，而是一系列使用不同的分析手段并应用于各个领域的一系列技术，许
共价半径共价半径定义为由共价键结合的两个原子核之间距离的一半，单位通常使用皮米(pm)或埃(Å)。He、Ne、Ar等原子无共价半径数据，因至今未合成其任何共价化合物。同周期元素的单键共
20,22-Desmolasen/an/an/an/an/an/an/an/an/an/a胆固醇侧链裂合酶（英语：Cholesterol side-chain cleavage enzyme，CYP11A1或P450scc，其中“scc”是“side-chain 侧链”“cleavage 裂解”的缩写）
不可知论不可知论（英语：Agnosticism），或称不可知主义，是一种哲学观点，认为形而上学的一些问题，例如是否有来世、鬼神、天主是否存在等，是不为人知或者根本无法知道的想法或理论。不可知论者
哈雷迪哈雷迪犹太教（希伯来语：.mw-parser-output .script-hebrew,.mw-parser-output .script-Hebr{font-size:1.15em;font-family:"Ezra SIL","Ezra SIL SR","Keter Aram Tsova","Ta
iThe Language Instinct: How the Mind Creates Language《语言本能－探索人类语言进化的奥秘》（英语：The Language Instinct: How the Mind Creates Language）是加拿大–美国认知科学家史迪芬·平克于1994年出版的科普书籍，书中平克主张