檢視合式公式的原始碼

{| class="wikitable" align="right"

|-

| style="background: #66CCFF" align= center|  '''<big>合式公式</big> '''

|-

|<center><img src="https://gimg2.baidu.com/image_search/src=http%3A%2F%2Ffile1.renrendoc.com%2Ffileroot2%2F2020-2%2F8%2F4d93e5c3-8dbb-44fb-98b8-385ff4cf26b8%2F4d93e5c3-8dbb-44fb-98b8-385ff4cf26b84.gif&refer=http%3A%2F%2Ffile1.renrendoc.com&app=2002&size=f9999,10000&q=a80&n=0&g=0n&fmt=auto?sec=1666102671&t=bc595648f3c05a0f92b5aabeb9078af3/400/fill/I0JBQkFCMA==/dissolve/70" width="250" ></center><small>[https://www.renrendoc.com/paper/89111094.html 圖片來自人人网图片]</small>

|-

| style="background: #66CCFF" align= center|

|-

| align= light|

|}

'''合式公式'''，又称谓词公式，是一种形式语言表达式，即形式系统中按一定规则构成的表达式。按照模型论中一种通行习惯，语言F中的合式公式定义如下：1.原子公式是合式公式； 2.若φ和ψ是合式公式，则(φ∧ψ)及(ᒣφ)是合式公式； 3.若φ是合式公式，而x是变元,则(ᗄx)φ是合式公式；4.有限次地应用1—3所得到的符号序列是合式公式。合式公式有时简称公式，如果一个公式φ中的[[自由变元]]都属于集合{x₁，x₂，…，xₑ}，则φ也可以记为φ(x₁，x₂，…，xₑ)，不含量词、自由变元的合式公式，分别称为开公式和闭公式，后者又称语句，例如R(x，y)为开公式，ᗄxR(x)是一个语句，由原子公式及联结词∧，∨，ᗄ，∃构成语句 称为正语句。

==什么是合式公式？==

(1)[[原子命题]]常项或变项是合式公式；

(2)如果A是合式公式，则（-A）也是合式公式（- 表示非）；

(3)如果A，B是合式公式，则（A*B）、（A+B）、（A < B）、（ A ~ B）也是合式公式；(此处 * 合取 + 析取 < 代表条件 ~ 代表双条件)

(4)只有有限次地应用(1)～(3)所包含的命题变元，联结词和括号的符号串才是合式公式。

个人思路QAQ：

用字符串输入(注意输入格式:在字符串首尾手动加括号)，依次扫描字符串，遇到“非法”字符跳出循环，字符串能够扫描完则为真

时间复杂度：O(n) 数据不大时，可以在1秒内完成

==“非法”字符==

（1）(*P) (+P)  (<P)  (~P)

（2） (P-)

（3） RT (两个大写字母)

（4） 括号不匹配

程序中可能会有bug，希望大佬们多多指教

这道题用递归的话，应该会更好，但我不会用，只能暴力判断了<ref>[https://blog.csdn.net/mr_liubai/article/details/78021286 合式公式的判断],CSON , --</ref>

一阶逻辑中合式公式，被递归定义如下：

(1)原子是合式公式；

(2)若A是合式公式，则(

)也是合式公式；

(3)若A，B是合式公式，则

也是合式公式；

(4)若A是合式公式，也是合式公式；

(5)只有限次地使用(1)～(4)所生成的符号串才是合式公式。

合式公式，也称谓词公式，简称为公式，为简便起见，公式的最外层括号可以省去。对于一个谓词，如果其中每一个变量都在一个量词作用之下，则它就不再是命题函数，而是一个命题了。但是，这种命题和命题逻辑中的命题还是有区别的，因为这种命题中毕竟还有变量，尽管这种变量和命题函数中的变量有所不同，因此，有必要区分这些变量。

==相关知识==

为了使一阶逻辑中命题符号化更准确和规范，以便正确进行谓词演算和推理，引进一阶逻辑中合式公式的概念．

在形式化中，将使用以下四类符号。

(1)常量符号：当论域D给出时，它可以是D中的某个元素；

(2)变量符号：当论域D给出时，它可以是D中的任何一个元素；

(3)函数符号：:的任意一个映射；

(4)谓词符号：到{1，0}的任意一个谓词。

定义1一阶逻辑中的项(item)，被递归定义如下：

(1)常量符号是项；

(2)变量符号是项；

(3)若是项；

(4)只有有限次地使用(1)、(2)、(3)所生成的符号串才是项。

例如a，b，x，y是项，也是项。

定义2设为原子公式，或简称原子。

==约束变量和自由变量==

在一个谓词公式中，变量的出现是约束的(bound)，当且仅当它出现在使用这个变量的量词作用范围(称为作用域)之内；变量的出现是自由的(free)，当且仅当它的出现不是约束的；至少有一次约束出现的变量称为约束变量(bound variable)，至少有一次自由出现的变量称为自由变量(free variable)。

例如，公式中的x的出现是约束的。而谓词R(x)中x的出现是自由的。另外，公式中y和z的出现也是自由，因此，x既是约束变量，又是自由变量，而y，z仅仅是自由变量。由此可知，公式中的某个变量既可以是约束变量，同时也可以是自由变量。此外，显然有

也即，一阶逻辑中命题的真值，与其约束变量的记号无关。

为了避免公式中有些变量既可以约束出现，又可自由出现的情形，我们可采用以下两条规则。

改名规则：将谓词公式中出现的约束变量改为另一个约束变量，这种改名必须在量词作用域内各处以及该量词符号中进行，并且改成的新约束变量要有别于改名区域中的所有其他变量。

代替规则：对公式中某变量的所有自由出现，用另一个与原公式中的其他变量符号均不同的变量符号去代替。

例如，对于公式，可使用改名规则，将约束出现的x改成u，得

或者使用代替规则，将自由出现的x用u代替，得

这样，对一阶逻辑中的任何公式，总可以通过改名规则或代替规则，使该公式中不出现某变量既是约束变量又是自由变量的情形。

由谓词公式的定义可知，若不对其中的常量符号、变量符号、函数符号和谓词符号给以具体解释，则公式是没有实在意义的。

==公式解释==

定义 在一阶逻辑中，公式G的一个解释

，是由非空论域D和对G中常量符号、函数符号、谓词符号按下列规则进行一组指定所组成：

(1)对每个常量符号，指定D中的一个元素；

(2)对每个n元函数符号，指定一个函数，即指定一个

到D的映射；

(3)对每个n元谓词符号，指定一个谓词，即指定一个

到{0，1}上的一个映射。

为统一起见，对所讨论的公式作如下规定：公式中无自由变量，或者将自由变量看作常量。于是，每个公式在任何具体解释下总表示一个命题。

==公式分类==

设G是一个谓词公式，

(1)如果存在解释是可满足的；

(2)如果所有解释为恒假的，或不可满足的；

(3)如果为恒真的。

如果一阶逻辑中的恒真(恒假)公式，要求所有解释依赖一个非空个体集合D，又集合D可以是无穷集合，而集合D的“数目”也可以有无穷多个，因此，所谓公式的“所有”解释，实际上是很难考虑的，这就使得一阶逻辑中公式的恒真、恒假性的判定异常困难。Church和Turing分别于1936年独立地证明了：对于一阶逻辑，判定问题是不可解的，即不存在一个统一的算法A，该算法与谓词公式无关，使得对一阶逻辑中的任何谓词公式G，A能够在有限步内判定公式G的类型。

但是，一阶逻辑是半可判定的，即如果谓词公式G是恒真的，有算法在有限步内检验出G的恒真性。

== 参考来源 ==

{{reflist}}

[[Category:310 數學總論]]