下面将简要介绍一阶谓词逻辑的一些基本体系以及它们在人工智能领域中的应用。

1.概述

一阶谓词演算体系首先规定了标点符号、括号、逻辑联结词、常量符号集、变量符号集、n元函数符号集、n元谓词符号集、量词（全称量词∀和存在量词∃）等，并定义了谓词演算的合法表达式（原子公式、合式公式wff）和表达式的演算化简方法，以便把一般化的表达式化为标准式（合取的前束范式或析取的前束范式）来讨论。

化简结果的标准式记为F≜（Q1x1）…（Qnxn）M（x1，x2，…，xn），其中（Q1x1）…（Qnxn）为前束，代表各种量词的约束关系，M（x1，x2，…，xn）称为母式，是不包含量词符号量化的合式公式范式。

2.标准式的化简步骤

如果一个合式公式的所有量词均非否定地出现在公式的前部，而且所有的量词的约束范围均是整个公式，则这样的合式公式称为前束范式。任何一个合式公式，都可以等价地转化为一个前束范式。消去前束范式中所有的存在量词后得到的合式公式称为S范式，这一过程称作Skolem化。S范式与它的原式不一定等价，但在不可满足性方面两者是等价的。也就是说，如果原式是不可满足的，则其对应的S范式也一定是不可满足的，反之亦成立。

利用结合律、分配律等，可以将S范式转化为一个合取范式。合取范式是前束范式的一种，其母式具有如下的形式：

其中Ai（i=1，2，…，n）是由原子公式或者原子公式的否定组成的析取项，每个析取项又称为子句。一个合取范式可以用如下的子句的集合（子句集）表示：

例如（∀x）（∀y）［（P（x，y）∨¬Q（x，y））∧（¬P（x，y）∨U（x）∨V（y））∧（Q（x，y）∨¬U（y））］

就是一个合取范式，其子句集为：

任何一个合式公式，都可以通过以下9步将其化为子句集（下面举例说明将合式公式转化为子句集的方法）。

［例5-1］　（∃z）（∀x）（∃y）｛［（P（x）∨Q（x））→R（y）］∨U（z）｝

1）消蕴涵符

当公式中含有蕴涵符“→”时，首先要消去蕴涵符。

利用蕴涵等价式，有

代入式中，有

如果公式中存在多个蕴涵符，则一个一个消去，直到不存在蕴涵符为止。

2）移动否定符

如果公式中的否定符“¬”不只是作用于原子公式，则要利用德·摩根定律对公式进行变换，使得否定符只作用于原子公式。

利用德·摩根律，有¬（P（x）∨Q（x））⇒¬P（x）∧¬Q（x）

代入式中，有

3）变量换名

在一个量词的约束范围内，受该量词约束的变量用任何一个未出现的变量名替换，并不改变一个合式公式的真值。因此，不同的量词约束的变量，应使用不同的变量名。如果在公式中出现同一个变量由不同的量词约束的情况，则应将其中一个量词约束的变量换名。本例没有这种情况，故不需要换名。

4）量词左移

将所有的量词移到公式的左边，但不改变原来各量词的排列顺序，将公式化为前束范式。这也是在第3）步要进行变量改名的原因。本例已经是前束范式了，所以不需要移动。

5）消去存在量词（skolem化）

消去存在量词的方法如下：(www.daowen.com)

设（QrXr）1≤r≤n是第一个出现于（Q1X1）…（QrXr）…（QnXn）M（X1…Xr…Xn）中的存在量词，即Q1，…，Qr－1均为全称量词。

（1）若r=1，则将M（X1，…，Xn）中所有变元X1均以某个常量C代之，要求C不同于已出现在M（X1，…，Xn）中的任一常量，然后便可消去这个存在量词（Q1X1）。

（2）若1＜r≤n，（QrXr）的左边有全称量词，则在M（X1，…，Xr，…，Xn）中的Xr项用前面全称量变元相关的一个函数代替，最后消去这个存在量词，如：

∀x∀y∃Z（Q（x，y，Z）∧M（x，y，Z）），取Z=g（x，y），则有∀x∀y（Q（x，y，g（x，y））∧M（x，y，g（x，y）））。这里要求所用的函数不能在原式中重复出现。

（3）反复使用这个过程便得Skolem标准形。如上式中的g（x，y）称为Skolem函数。

如：设G=（∀x）（∃y）（∃Z）（¬P（x，y）∧（Q（x，Z）∨R（x，y，Z））

则Skolem标准函数可用下列方法求出：

①将G化成合取范式：

②消去存在量词。由于G中有量词（∀x）（∃y）（∃Z），先消（∃y）。因（∃y）的左边有（∀x），所以在M（x，y，z）中的y用f（x）代入，再消（∃Z）。因（∃Z）左有（∀x），所以在M（x，y，z）中的Z用g（x）代入，由此则有两个Skolem函数，即f（x）和g（x）。

③原式化为：

对于本例有：

对于存在量词“∃z”，由于其前面没有全称量词，所以受该存在量词约束的变量z用一个常量a代替。对于存在量词“∃y”，由于其前面有全称量词“∀x”，所以受该存在量词约束的变量y用一个Skolem函数f代替。f的变量是x，因为约束x的全称量词在约束y的存在量词的前面。

6）化为合取范式

利用结合律、分配律等，可以把S范式的母式转化为合取范式。

对于本例有：

7）隐去全称量词

经过前面的变换以后，所有的变量都受全称量词约束。所以可以将全称量词隐去，默认所有的变量都是受全称量词约束的。

对于本例有：

8）表示为子句集

在隐去全称量词以后，用“，”号代替公式中的“∧”，并用“｛”和“｝”括起来，就得到了原合适公式的子句集。

对于本例，得到的子句集如下：

该子句集含有¬P（x）∨R（f（x））∨U（a）和¬Q（x）∨R（f（x））∨U（a）两个子句。

9）变量换名

对子句集中的变量再次进行换名替换，使得不同的子句中的变量使用不同的名字。最简单的方法是加下标。对本例有：

注意：不同子句中的变量，即便是同名的，也可以代表不同的变量。

将一个合式公式化为子句集是后面将要介绍的归结法的基础。这部分内容可参考离散数学、数理逻辑等方面的书籍。