标签:#逻辑演算

共 11 篇文章

域关系演算

在计算机科学中,域关系演算(DRC)是Michel Lacroix和 Alain Pirotte为关系数据模型发明的的作为声明性数据库查询语言。 在 DRC 中,“查询”有如下形式: : { | p() } 这里的 Xi 要么是一个域变量要么是一个常量,而 p() 指示一个 DRC “公式”。 查询的结果为使得这个 DRC 为真的元组 Xi 到 Xn 的集合。 域关系演算可以使用量词,同时使用与\wedge、或\vee 、非\neg (…

元组关系演算

元组演算是埃德加·科德導入的演算,是关系模型的一部分,發展目的是提供宣告式的数据库查询语言。数据库查询语言和后来的SQL中的一些靈感是由元组演算而來。SQL和原來的关系模型和演算已有許多不同,後來成為實際上的数据库查询语言標準,几乎所有的关系数据库管理系统中都會用到SQL或是其變體。後來Lacroix和Pirotte提出了接近于一阶逻辑的域演算,并证明了这两种演算和关系代数在表达能力上是等价的。若关系数据库的查询语言可以表达一種以上上述…

希尔伯特演绎系统

在逻辑特别是数理逻辑中,希尔伯特风格演绎系统是归功于弗雷格和希尔伯特的一类形式演绎系统。这种演绎系统最经常为一阶逻辑而研究,但对其他逻辑也是有价值的。 所有演绎系统都在逻辑公理和推理规则之间作出取舍平衡。希尔伯特风格的演绎系统可以刻画为选择了大量的逻辑公理模式和少(Hilbert system)量的推理规则。最常研究的希尔伯特风格演绎系统只有一个推理规则即肯定前件和几个无限公理模式。 自然演绎系统做了相反的取舍,包括了很多演绎规则但有非…

存在图

存在图是查尔斯·皮尔士发明的逻辑表达式的一种图示或可视表示法。皮尔士在1882年写了第一篇关于图形逻辑的论文,并持续开发这种方法直到1914年他故去。 图形 皮尔士提出了三个存在图系统: alpha, 同构于命题演算和两元素布尔代数; beta, 同构于所有公式都闭合的有等式的一阶逻辑; gamma, (几乎)同构于普通模态逻辑。 Alpha嵌套于beta和gamma 中。Beta不嵌套于gamma中,量化的模态逻辑超出了皮尔士的视野。…

自然演绎

在数理逻辑中,自然演绎是证明论中尝试提供象“自然”发生一样的逻辑推理形式模型的一种方式。這種方式對比於使用公理的公理系統。 动机 自然演绎来源自对共通于弗雷格、罗素和希尔伯特系统的判句公理化(希尔伯特演绎系统)的不满。这种公理化最著名使用是在罗素和怀特海的《数学原理》的数学论述中。在1926年由扬·武卡谢维奇在波兰发起的一系列研讨会提倡一种对逻辑的更加自然处理,斯坦尼斯瓦夫·亚希科夫斯基做了定义更自然的演绎的最早尝试,首先在1929年使…

相继式演算

在证明论和数理逻辑中,相继式演算(又译矢列演算、矢列式演算、序贯演算)是一阶逻辑(和作为它的特殊情况的命题逻辑)、模态逻辑等逻辑的一类。第一个相继式演算LK和LJ由格哈德·根岑(Gerhard Gentzen)在1934年/1935年引入,作为研究自然演绎的工具;它的名字得来自德语的“Logischer Kalkül”,意思是“逻辑演算”。相继式演算系统有时被称为Gentzen系统,但使用时应避免与同为Gentzen发明的证明演算自然演…

一元谓词演算

在逻辑中,一元谓词演算是所有谓词字母都是一元(就是只接受一个参数)并且没有函数字母的谓词演算。所有原子公式都有形式 P(x),这里的 P 是谓词字母而 x 是变量。 性质 向一元逻辑增加一个单一二元谓词字母将导致一个有完全谓词演算表达能力的系统。所以缺乏多元谓词严格的限定了在一元谓词演算中都能表达什么。不像完全谓词演算,这个演算是如此的弱,这个演算的一个给定公式是否有效(对于非空论域为真)是可判定性的。 因为一元谓词演算是可判定性的,它…

蕴涵命题演算

在数理逻辑中,蕴涵命题演算是只使用叫做蕴涵或条件的一个连结词的经典(二值)命题演算。用公式表达,这个二元运算被指示为“implies” “如果 ..., 则 ...”, “→”, “\rightarrow \!”等等。 作为算子的实质完备性 单独的蕴涵作为逻辑算子不是完备的,因为不能用它形成所有其他二值真值函数。但是如果有已知为假的一个命题并作为给虚假的零元连结词那样使用它,则可以定义所有其他真值函数。所以蕴涵作为算子实质上是完备的。如…

关系演算

关系演算包括元组关系演算和域关系演算,是数据库的关系模型的一部分,提供了查询数据库的声明性方式。关系演算与关系模型中的关系代数相反,因为关系代数提供的是查询数据库的过程性方式。 关系代数和关系演算是逻辑等价的:对于任何代数表达式,都有一个等价的演算表达式,反之亦然。 参考资料 参见 关系模型 关系演算 元组关系演算 域关系演算 关系代数

弗雷格命题演算

在数理逻辑中弗雷格命题演算是第一个公理化的命题演算。它由弗雷格发明,他还在1879年发明了谓词演算,作为他的二阶谓词逻辑的一部分(尽管查尔斯·桑德斯·皮尔士首次使用了术语“二阶”并独立于 Frege 开发了自己版本的谓词演算)。 它只使用两个逻辑算子: 蕴涵和否定,并且由六个公理和一个推理规则肯定前件构成。 公理 THEN-1: A→(B→A) THEN-2: (A→(B→C))→((A→B)→(A→C)) THEN-3: (A→(B→…

实体图

实体图是查尔斯·皮尔士于1880年代开始在定性逻辑的名义下开发的逻辑的图形语法的一个要素,只覆盖了逻辑的命题演算方面所关心的内容的形式化。请参见《Peirce's Collected Papers》的 3.468, 4.434, 和 4.564。 语法是: 空白页; 单一的字母,短语; 包围在叫做切的简单闭合曲线内的对象(子图)。切可以为空。 语义是: 空白页指示假; 字母,短语,子图和整个图可以为真或假; 用切包围对象等价于布尔补运算…