比浏览器更快的访问！
14 关系: 多重集，定理机器证明，亚结构逻辑，序列，归结原理，切消定理，线性逻辑，相继式，相继式演算，计算，证明论，集合，逻辑运算符，推理规则。
多重集
多重集或多重集合是数学中的一个概念，是集合概念的推广。在一个集合中，相同的元素只能出现一次，因此只能显示出有或无的属性。在多重集之中，同一个元素可以出现多次。正式的多重集的概念大约出现在1970年代。.
定理机器证明
定理机器证明（Automated theorem proving，簡稱ATP）目前是自动推理（Automated reasoning，簡稱AR）体系中发展最好的部分，它的目的是为使用电子计算机程序来进行数学定理的证明。对于不同的数学逻辑，它能够推论出一个定理是正确的，还是不可证明的，或者错误的。 Category:数学软件.
新！!: 结构规则和定理机器证明 · 查看更多 »
亚结构逻辑
在数理逻辑中，特别是联合上证明论的时候，一些亚结构逻辑已经作为比常规系统弱的命题演算系统被介入了。同常规系统的不同之处在于它们有更少的结构规则可用：结构规则的概念是基于相继式（sequent）表达，而不是自然演绎的公式化表达。两个重要的亚结构逻辑是相干逻辑和线性逻辑。 在相继式演算中，你可以把证明的每一行写为 这里的结构规则是重写相继式左手端的Γ的规则，Γ是最初被构想为命题的字符串。这个字符串的标准解释是合取式：我们希望把相继式符号 读做 这里我们把右手端的Σ采纳为一个单一的命题C（这是直觉主义风格的相继式）;但是所有的东西都同样的适用于一般情况，因为所有的操作都发生在十字转门（turnstile）符号的左边。 因为合取是交换性和结合性的操作，相继式理论的形式架设通常包括相应的结构规则来重写相继式的Γ - 例如 演绎自 还有对应于合取特性的幂等性和单调性的进一步的结构规则：从 我们可以演绎出 还有从 我们可以演绎出，对于任何B， 在线性逻辑中有重复的假设（hypothese）'被认为'不同于单一的出现，它排除了这两个规则。而相干逻辑只排除后者的规则，因为B明显的与结论无关。 这些是结构规则的基本例子。在应用到常规命题演算的时候，这些规则是没有任何争议的。它们自然的出现于证明理论中，并在那里被首次注意到（在获得一个名字之前）。.
新！!: 结构规则和亚结构逻辑 · 查看更多 »
序列
数学上，序列是被排成一列的对象（或事件）；这样，每个元素不是在其他元素之前，就是在其他元素之后。这里，元素之间的顺序非常重要。.
归结原理
在数理逻辑和自动定理证明中（GOFAI涉及的主题），归结（resolution）是对于命题逻辑和一阶逻辑中的句子的推理规则，它导致了一种反证法的定理证明技术。.
切消定理
切消定理是确立相继式演算重要性的主要结果。它最初由格哈德·根岑在他的划时代论文《逻辑演绎研究》对分别形式化直觉逻辑和经典逻辑的系统LJ和LK做的证明。切削定理声称在相继式演算中，拥有利用了切规则的证明的任何判断，也拥有无切证明，就是说，不利用切规则的证明。 相继式是与多个句子有关的逻辑表达式，形式为"A, B, C, \ldots \vdash N, O, P"，它可以被读做"A, B, C, \ldots证明N, O, P"，并且（按Gentzen的注释）应当被理解为等价于真值函数"如果（A & B & C \ldots）那么（N or O or P）"。注意LHS（左手端）是合取（and）而RHS（右手端）是析取（or）。LHS可以有任意多个公式；在LHS为空的时候，RHS是重言式。在LK中，RHS也可以有任意数目的公式--如果没有，则LHS是个矛盾，而在LJ中，RHS只能没有或有一个公式：在右紧缩规则前面，允许RHS有多于一个公式，等价于容许排中律。注意，相继式演算是相当有表达力的框架，已经为直觉逻辑提议了允许RHS有多个公式的相继式演算，而来自Jean-Yves Girard的逻辑LC得到了RHS最多有一个公式的经典逻辑的更加自然的形式化；逻辑和结构规则的相互作用是它的关键。 "切"是在相继式演算的正规陈述中的一个规则，并等价于在其他证明论中的规则变体，给出 和 你可以推出 就是说，在推论关系中"切掉"公式"C"的出现。 切消定理声称（对于一个给定的系统）使用切规则的任何相继式证明也可以不使用这个规则来证明。如果我们认为(D, E, \ldots)是一个定理，则切消简单的声称用来证明这个定理的引理C可以被内嵌（inline）。在这个定理的证明提及引理C的时候，我们可以把它代换为C的证明。因此，切规则是可接纳的。 对于用相继式公式化的系统，分析性证明是不使用切规则的证明。这种证明典型的会很长，当然没有必要这么做。在散文《不要消除切呀!》中，George Boolos展示了可以使用切在一页中完成的推导，而它的分析性证明要耗尽宇宙的寿命来完成。 这个定理有很多丰富的推论。一旦一个系统被证明有切消定理，这个系统通常立即就是一致的。这个系统通常也有子公式性质，这是达成证明论语义的重要性质。切削是证明插值定理的最强力工具。基于归结原理的完成证明查找的可能性，导致Prolog编程语言的本质洞察，依赖于在适当的系统中接纳切规则。.
线性逻辑
在数理逻辑中，线性逻辑是拒绝“弱化”和“收缩”的结构规则的一种亚结构逻辑。对此解释是“假设是资源”:在证明中所有假设必须被消费“精确一次”。这区别于平常的逻辑比如经典逻辑或直觉逻辑，那里统治判断是“真理”，它可以按需要被自由的使用多次。例如，从命题A和A ⇒ B能按如下步骤得出结果A ∧ B.
相继式
在证明论中，相继式是对在规定演绎的演算的时候经常用到的可证明性的形式陈述。.
相继式演算
在证明论和数理逻辑中，相继式演算（又译矢列演算、矢列式演算）是众所周知的一阶逻辑（和作为它的特殊情况的命题逻辑）的演绎系统。这个系统也叫做LK系统，用以区别于后来建立的有时也叫做相继式演算的类似风格的各种其他系统。另一个给这种系统的术语是Gentzen系统。 相继式演算LK由Gerhard Gentzen介入为研究自然演绎的工具。它已经变成构造逻辑推导的非常有用的演算。它的名字得来自德语的Logischer Kalkül，意思是"逻辑演算"。相继式演算是关于这个主题的很多研究所选择的方法。.
新！!: 结构规则和相继式演算 · 查看更多 »
计算
計算（Calculation）是一種將「單一或多個的輸入值」轉換為「單一或多個的結果」的一種思考過程。 計算的定義有許多種使用方式，有相當精確的定義，例如使用各種算法進行的「算术」，也有較為抽象的定義，例如在一場競爭中「策略的計算」或是「計算」兩人之間關係的成功機率。 將7乘以8（7x8）就是一種簡單的算術。 利用布莱克-斯科尔斯模型（Black-Scholes Model）來算出財務評估中的公平價格（fair price）就是一種複雜的算術。 從投票意向計算評估出的選舉結果（民意調查）也包含了某種算術，但是提供的結果是「各種可能性的範圍」而不是單一的正確答案。.
证明论
证明论是数理逻辑的一个分支，它将数学证明表达为形式化的数学客体，从而通过数学技术来简化对他们的分析。证明通常用归纳式地定义的数据结构来表达，例如链表，盒链表，或者树，它们根据逻辑系统的公理和推理规则构造。因此，证明论本质上是语法逻辑，和本质上是语义学的模型论形相反。和模型论，公理化集合论，以及递归论一起，证明论被称为数学基础的四大支柱之一。 证明论也可视为哲学逻辑的分支，其主要兴趣在于证明论语义学的思想，该思想依赖于结构证明论的技术型想法才可行。.
集合
集合可以指：.
逻辑运算符
在形式逻辑中，逻辑运算符或逻辑联结词把语句连接成更复杂的复杂语句。例如，假设有两个逻辑命题，分别是“正在下雨”和“我在屋里”，我们可以将它们组成复杂命题“正在下雨，并且我在屋里”或“没有正在下雨”或“如果正在下雨，那么我在屋里”。一个将两个语句组成的新的语句或命题叫做复合语句或复合命题。.
新！!: 结构规则和逻辑运算符 · 查看更多 »
推理规则
在逻辑中，特别是数理逻辑中，推理规则（推论规则）是构造有效推论的方案。这些方案建立在一组叫做前提的公式和叫做结论的断言之间的语法关系。这些语法关系用于推理过程中，新的真的断言从其他已知的断言得出。规则也适用于非形式逻辑和逻辑论证，但是形式化更加困难和有争议。 按照规定，推理规则的应用纯粹是语法过程。尽管如此它必须是有效的，或者更精确地说保持有效性。为了使保持有效性的要求有意义，某种形式的语义与推理规则有关和推理规则自身的断言是必需的。对于在推理规则和和语义之间相互关系的讨论请参见命题逻辑。 命题逻辑中推理规则的显著例子是肯定前件和否定后件规则。对于一阶谓词逻辑，推理规则需要处理逻辑量词。对这种论证的更详细的描述请参见有效性。在一阶谓词逻辑中把所有推理规则作为一个单一规则来统一处理请参见一阶归结。 注意有很多不同的形式逻辑系统，每个都带有合式公式、推理规则和语义的自己的集合。参见时间逻辑、模态逻辑或直觉逻辑的实例。量子逻辑也是一种不同寻常形式的逻辑。参见证明论。在谓词演算中，需要一个补充的推理规则。它叫做普遍化。 在形式逻辑的设置（和很多有关领域）中，推理规则通常用如下形式给出： 前提#1 前提#2 ... 前提#n 结论 这个表达式声称，在某个逻辑推导期间已经获得了给定前提，同样可以认可特定结论。用来描述前提和结论二者的的精确的形式语言依赖于推导的实际上下文。在一个简单的情况下，你可以使用逻辑公式，比如 A→B A B 它是命题逻辑的肯定前件规则。推理规则通常通过使用全称变量而公式化为规则模式。在上面的规则（模式）中，A和B可以被实例化为论域（有时约定为某种受限制的子集比如命题）的任何元素，来形成推理规则的无限集合。 证明系统形成自一组规则，它们可以被链接在一起形成证明或推导。任何推导都只有一个最终结论，它是要证明或推导的陈述。如果在推导中留下了未满足的前提，则推导就是假言陈述："如果前提成立，那么结论成立"。.
重定向到这里：
結構規則。
