线性逻辑

✍ dations ◷ 2025-12-07 17:12:06 #线性逻辑

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

相关

呼吸中止呼吸中止、呼吸暂停（英文：Apnea）指的是呼吸完全停止。呼吸一旦终止，将不会有吸气及相关的肌肉动作且肺的体积将保持不变。端视呼吸道被锁死的程度与肺部跟外界环境的气流通气度
神经神经（英语：Nerve）是由聚集成束的神经纤维所构成。而神经纤维本身是由多个神经元细胞构成，其神经元的构造为轴突外并被神经胶质细胞所形成的髓鞘包覆。如此神经能将讯息从动物身
城市化城市化（英语：urbanization / urbanisation），又称城镇化、都市化，是指人口向城市聚集、城市规模扩大以及由此引起一系列经济社会变化的过程，其实本质是经济结构、社会结构和空间结
卡尔·林奈卡尔·冯·林奈（英语：Carl Linnaeus，瑞典语：Carl von Linné，1707年5月23日－1778年1月10日），也译为林内，受封贵族前名为卡尔·林奈乌斯（Carl Linnaeus），由于瑞典学者阶层的姓常拉丁化，又
高加索人种高加索人种（英语：Caucasian race, Caucasoid），或称欧罗巴人种，是在欧洲、北非、非洲之角、西亚、中亚、南亚、北美、南美和大洋洲的人口中常见的人种。这个术语在体质人类学中用
神学院叶史瓦（/jəˈʃiːvə/; 希伯来语：.mw-parser-output .script-hebrew,.mw-parser-output .script-Hebr{font-size:1.15em;font-family:"Ezra SIL","Ezra SIL SR","Keter Aram
普通语言学普通语言学又称做一般语言学，是对人类语言的看法和研究结果的理论概括，是研究语言的本质、发展和起源以及语言的类型和分类的语言学分支学科。普通语言学有广义和狭义之分。广
苗瑶语系苗瑶语是苗、瑶、畲等族群所使用的有共同来源的一些语言的总称。学术界对于苗瑶语的语言系属分类有不同看法：华人和中国学者多认为苗瑶语是属于汉藏语系的语族，即苗瑶语族；欧美
词形变化在语法学中，词形变化（又译作形态变化、屈折变化）（Inflection or inflexion）指单词（或词根）的变化，以导致语法功能改变，进而使其代表的意义也有所改变。印欧语屈折变化又可以分为变位
副词副词（英语：Adverb）是一类用以修饰动词或加强描绘词组或整个句子的词，修饰名词的词一般为形容词，又称限制词。一般而言，中文在一个词（通常是定语）的后面加“的”接主语或宾语，使定语成