徽标
联盟百科
通讯
下载应用,请到 Google Play
新! 在您的Android™设备上下载联盟百科!
自由
比浏览器更快的访问!
 

斯科伦范式

指数 斯科伦范式

一阶逻辑的公式是Skolem 范式的,如果它的前束范式只有全称量词。一个公式可以被Skolem 化,就是说消除它的存在量词并生成最初的公式的等价可满足的公式。Skolem 化是如下(二阶的)等价的应用 Skolem 化的本质是对如下形式的公式的观察 它在某个模型中是可满足的,在这个模型必定对于所有的 有某些点y 使得 为真,并且必定存在某个函数(选择函数) 使得公式 为真。函数 f 叫做 Skolem 函数。 举例说明.

6 关系: 一阶逻辑归结原理公式前束范式选择公理模型论

一阶逻辑

一阶逻辑是使用於数学、哲学、语言学及電腦科學中的一种形式系统。 過去一百多年,一階邏輯出現過許多種名稱,包括:一阶斷言演算、低階斷言演算、量化理論或斷言逻辑(一個較不精確的用詞)。一階邏輯和命題邏輯的不同之處在於,一階邏輯有使用量化變數。一個一階邏輯,若具有由一系列量化變數、一個以上有意義的斷言字母及包含了有意義的斷言字母的純公理所組成的特定論域,即是一個一階理論。 一階邏輯和其他高階邏輯不同之處在於,高階邏輯的斷言可以有斷言或函數當做引數,且允許斷言量詞或函數量詞的(同時或不同時)存在。在一階邏輯中,斷言通常和集合相關連。在有意義的高階邏輯中,斷言則會被解釋為集合的集合。 存在許多對一階邏輯是可靠(所有可證的敘述皆為真)且完備(所有為真的敘述皆可證)的演繹系統。雖然一階邏輯的邏輯歸結只是半可判定性的,但還是有許多用於一階邏輯上的自動定理證明。一階邏輯也符合一些使其能通過證明論分析的元邏輯定理,如勒文海姆–斯科倫定理及緊緻性定理。 一階邏輯是數學基礎中很重要的一部份,因為它是公理系統的標準形式邏輯。許多常見的公理系統,如一階皮亞諾公理和包含策梅洛-弗蘭克爾集合論的公理化集合論等,都可以形式化成一階理論。然而,一階定理並沒有能力去完整描述及範疇性地建構如自然數或實數之類無限的概念。這些結構的公理系統可以由如二階邏輯之類更強的邏輯來取得。.

新!!: 斯科伦范式和一阶逻辑 · 查看更多 »

归结原理

在数理逻辑和自动定理证明中(GOFAI涉及的主题),归结(resolution)是对于命题逻辑和一阶逻辑中的句子的推理规则,它导致了一种反证法的定理证明技术。.

新!!: 斯科伦范式和归结原理 · 查看更多 »

公式

在科學中,公式是一種把資訊準確地以符号表達的方法,就像是數學公式或化學式那樣。 在數學中,廣義上的公式是指在特定的形式文法下,把數學符號組合而成之結果。 在現代化學中,一個化學式中會有元素符號、數字,可能還有別的符號如圓括號、方括號和正負符號等,用以表示在化合物中各種原子所佔之比例,以及一些性質。例如H2O 即為水的化學式,表明每個水分子包含兩個氫原子和一個氧原子。類似地,O 是指包含三個氧原子並帶有一個負電荷的臭氧分子。.

新!!: 斯科伦范式和公式 · 查看更多 »

前束范式

在谓词演算中,一个公式是前束范式的,如果它可以被写为量词在前,随后是被称为母体的无量词部分的字符串。所有经典逻辑公式都逻辑等价于某个前束范式公式。 可以用公式在如下重写规则下的逻辑等价来证实: 進一步推論可得:(可透過改寫 P \rightarrow Q 為 \lnot P \or Q 推論得出) 它们的存在对偶: 这里的 x 在 Q 中是非自由的,并注意通过这些规则的持续应用所有量词都可以移动到公式的前面。 某些证明演算只处理公式写为前束范式的理论。对于开发算术层次和分析层次这个观念是基本的。 前束范式是哥德尔证明他的哥德尔完备定理的主要工具。 Q Category:模型论.

新!!: 斯科伦范式和前束范式 · 查看更多 »

选择公理

选择公理(Axiom of Choice,縮寫AC)是数学中的一条集合论公理。这条公理声明,对所有非空指标集族 (S_i)_,总存在一个索引族 (x_i)_,对每一个 i \in I,均有 x_i \in S_i。选择公理最早于1904年,由恩斯特·策梅洛为证明良序定理而公式化完成。 非正式地說,选择公理声明:給定一些盒子(可以是無限個),每个盒子中都含有至少一个小球,那么可以作出这样一种选择,使得可从每个盒子中恰好选出一个小球。在很多情况下这样的选择可不借助选择公理;尤其是在“盒子个数有限”和“存在具體的選擇規則”(當每個盒子都恰好只有一个小球具有某項特征)这两种情况下。再举一个例子,假设有许多(甚至是无限)双鞋子,则我们可以选取每双鞋左边的鞋子构成一个具体的选择。然而,假设有无限双袜子(假设每双袜子都没有可区分的特征),在这种情况下,有效的选择只能通过选择公理得到。 尽管曾具有争议性,选择公理現在已被大多数数学家毫无保留地使用着,例如带有选择公理的策梅洛-弗兰克尔集合论(ZFC)。数学家们使用选择公理的原因是,有许多被普遍接受的数学定理,比如是吉洪诺夫定理,都需要选择公理来证明。現代的集合论学家也研究与选择公理相矛盾的公理,例如。 在一些構造性數學的理論中會避免选择公理的使用,不過也有的將选择公理包括在內。.

新!!: 斯科伦范式和选择公理 · 查看更多 »

模型论

数学上,模型论(Model theory)是从集合论的论述角度对数学概念表现(representation)的研究,或者说是对于作为数学系统基础的“模型”的研究。粗略地说,该学科假定有一些既存的数学“对象”,然后研究:当这些对象之间的一些运算或者一些关系乃至一组公理被给定时,可以相应证明出什么,以及如何证明。 比如实数理论中一个模型论概念的例子是:我们从一个任意集合开始,作为集合元素的每个个体都是一个实数,其间有一些关系和(或)函数,例如。若我们在该语言中问"∃ y (y × y.

新!!: 斯科伦范式和模型论 · 查看更多 »

重定向到这里:

Skolem函数Skolem范式斯柯伦标准型

传出传入
嘿!我们在Facebook上吧! »