第五章 谓词公式的永真性.ppt

《第五章 谓词公式的永真性.ppt》由会员分享，可在线阅读，更多相关《第五章 谓词公式的永真性.ppt（60页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、 第五章 谓词公式的永真性及可满足性与几个常用的重要定理第五章 谓词公式的永真性及可满足性与几个常用的重要定理5.1 永真性和可满足性5.2 常用的重要定理5.3 日常推理过程的讨5.4 假设推理过程的讨论5.5 谓词演算在程序正确性证明上的应用 习题及参考答案12/20/20221 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 5.1 永真性和可满足性 要讨论谓词演算公式永真与否（公式的真假性），首先应当分析一下任一谓词公式的真假值与公式中的那些成分有关，我们举个例子来分析这个问题：先讨论A（x），xA（x），xA（x）这三个公式的真假情况。12/20/20222 第五章 谓词公式

2、的永真性及可满足性与几个常用的重要定理 1）设谓词“A（e）”表示“e为偶数”，则A（x）意思为“x为偶数”，显然该公式的真假值随x而变化，因为该公式没有量词，所以A（x）的真假值与自由个体变元x有关。2）xAxA（x x）与）与xAxA（x x）的意思分别是“所有的个体变元x为偶数”及有一个或存在一个个体变元x为偶数，这说明这两个公式的真假值与个体域有关，而与约束个体变元x无关，因为一但个体变元的变域给定后，这两个公式的真假就确定了。例如：对个体域1，2，3，公式 xAxA（x x）意思为“所有的自然数均为偶数”故公式的值为F（假），而公式xAxA（x x）的意思是“有一（存在）一自然数为偶

3、数”，其公式的值为T（真）。12/20/20223 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 又例如对上述公式，如果给定个体域为1，3，5，7，9时 xA（x）的意思为“1，3，5，7，9这五个自然数”均为偶数，故该公式为F（假）；而对xA（x）的意思为“1，3，5，7，9中有一个为偶数，故该公式为F。由此可知，一公式的真假与个体域有关，与自由个体变元有关，而与约束个体变元无关。xA（x）再进一步的讨论，我们发现谓词公式的永真性与可满足性有以下几点，下面分别介绍：(1)与个体域有关，与约束个体变元无关。(2)与自由变元有关，当个体域取定后P取定.，很清楚 xP（x）是一个命题，而

4、Q取定后，xP（x，y）不是命题，只有当y代入特定的个体变元后，才是一个命题，比如个体域为1，2，3，4，5Q（x，y）表示“xy”，只有当y取定个体后 x Q（x，y）才是个命题才能确定真假值。12/20/20224 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 3）与命题及谓词有关，如公式 xA（x）B（y）P其中A，B是谓词及P有关的。比如个体域是2，4，6，8偶数集，若A表示“是偶数”，B表示“是4个的倍数”且取y=8，P=T，则原公式为真，而若A取为“是奇数”或P=F则原公式为假，所以说与命题及谓词有关。4）与函词有关，比如 xP（f（x），个体域为1，2，P表示“是偶数”

5、，则若f（x）定义为f（x）=x，那么 xP（f（x）为假，而若f（x）=2，那么 xP（f（x）为真，所以说与函词有关。12/20/20225 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 综上所述可得，任一谓词演算公式的真假与谓词变元，命题变元，自由个体变元，函词及个体域有关，而与约束个体变元无关。我们推扩为一般形式为：设有一谓词演算公式，其自由个体变元为x1xr；命题变元为P1Pk；函词为f1fm谓词变元为x1xh则我们将表示为（x1xh；P1Pk；f1fm；x1xr）（注意，这里不是谓词填式，因为是公式，而不是谓词）。如果对个体域I指派以I0（即其约束变元以I0为变域）对x1

6、xh分别指派以I0中的个体a1ah对P1Pk 分别指派以b1bk对f1fm 分别指派以C1Cm对X1Xr 分别指派以D1Dr则说对作了一个个体域I0中的指派。（a1ah；b1bk；C1Cm；D1Dr）。12/20/20226 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 因为的值与个体域，自由变元，函词，命题变元，谓词变元有关，所以给定一指派后，的真假值是确定的，为了讨论方便起见，今后我们将在I0中的指派（a1ah；b1bk；C1Cm；D1Dr）之下所取值记为（a1ah；b1bk；C1Cm；D1Dr）如果该值为真，则该指派称为的成真指派，如果该值为假，则该指派称为的成假指派，如果仅对

7、中的部分自由变元（包括自由个体变元，命题变元，函词，谓词变元）给以指派，则称为该指派的有缺指派（部分指派）。一般地在有缺指派下，不一定能得出确定的真假值，而是关于那些未作指派自由变元的函词，（函数）决定谓词演算公式的真假关键在于决定 x（x），x（x）的真假。x（x），x（x）的真假的决定方法如下：定理：对于个体域I，x（x）真，当且仅当I中各个体均使得（x）真；当且仅当I中有一个体使得（x）真。这个结论是易知的。12/20/20227 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 下面我们举例说明，给定一指派之后，如何确定公式在该指派之下所取的值。例例：求x yx y（X X（x

8、x，z z）X X（y y，z z）P P）u u（X X（x x，u u）X X（y y，u u）在（I，Z，P，X（e1，e2）=（自然数域，2，T，e1 e2）之下的值。解解：第一步，将指派代入，并化简得 x yx y（X2y2TX2y2T）u(x u y u)u(x u y u)）=x yx y（X2y2X2y2）u(x u y u)u(x u y u)）第二步,自内向外逐层求出量词带头的子公式的值，这里先求 u(x u y u)（显然该值与自由变元x，y有关），再求出整个公式的值。在求出子公式或整个公式的值时，应当对约束变元作各种可能的代入，并求出作用域在各种情况下的真假，但是必须注

9、意，作各种的可能代入时要注意的是应当是有次序的，否则，公式的真假仍不能决定，次序是什么？是公式头上指导变元的次序。对于我们这个例子公式 u(x u y u)只有一个指导变元，故不存在次序问题，只须对约束变元的各种可能情形作代入，求值即可。但整个公式的头上有二各指导变元x和y，因此存在一个次序问题，如有公式 x yP（x，y）其次序是先x后y，即按x来分各种情形，在按y来分各种情形，这样就可以求出作用域的真假了。12/20/20228 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 下面我们先求 x（xyy u）的真假情形。1）当x u时 作用域=x u y u =Ty u =y u 当

10、y u时作用域=T y u时作用域=F 2）x u时 作用域=x y y u =Fy u =T 故有，当x uy时作用域=F。其它情况时作用域=T 因此，当xy时存在u使得作用域=F。所以 u（x uy u）=F。12/20/20229 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 当 x y时，不存在u使得x uy成立。所以 u（x uy u）=T。故有，u（x uy u）=x y 将结果代入到原式中去得：x y（x2y2）x y）然后再求公式的真假值 1.当 x 2时，作用域=（x2y2）x y）=（Fy2）x y =T 2当 x2时，作用域=（x2y2）x y =（Ty2）x

11、y =y2）x y 2.1当x=1时，作用域=y21 y =T 2.2当x=0时，作用域=y20 y =T 2.2.1当y=0时，作用域=020 0=T 2.2.2当y=1时，作用域=120 1=F 2.2.3当y2时，作用域=F0 y=T12/20/202210 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 由此可知，在所给的指派之下，该公式取得真假。由此可列出下表X XY Y作用域作用域 y yx xX2X2全全T TT TT TX=1X=1全全T TT T X=0X=0Y=0Y=0T TF FY=0Y=0F FY2Y2T T12/20/202211 第五章 谓词公式的永真性及可

12、满足性与几个常用的重要定理 5.2 常用的重要定理 现在我们讨论同真假性，同永真性和同可满足性。定义定义：设有公式A及B如果对个体域I中每一指派，A与B均取得相同的真假值，则说A与B在I上同真假，如果A与B在每一个非空域上均同真假，则说A与B同真假。定理定理：如果A与B同真假，则（A）与（B）同真假，其中（A）是任含A的公式，（B）是在（A）中用B替换若干个A的结果。12/20/202212 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 在任何域中下列各公式均同真假，其中C是不含自由变元x的公式。1）xA（x）与xA（x）2）xA（x）与 xA（x）3）x（A（x）C）与 xA（x）

13、C 4）x（A（x）C）与 xA（x）C 5）x（A（x）C）与xA（x）C 6）x（A（x）C）与xA（x）C 该定理说明了对量词辖域扩张的一些等式，当然可将6对式子均可写成等式，如 x（A（x）C）与 xA（x）C可写成 x（A（x）C）与 xA（x）C等。下面仅证明（3）这个等式其它等式同理证明即可。12/20/202213 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 证明 x（A（x）C）=xA（x）C其中C内不出现个体变元。证明：证明：因为对（3）式中的C，它或为T或为F，当它为T时（3）式成立，当它为F时（3）式亦成立，故（3）式成立，证毕。12/20/202214 第

14、五章 谓词公式的永真性及可满足性与几个常用的重要定理 利用上述两个定理可以证明下面很重要的定理，为此先给出一个定义。定义：一公式如果其量词均在全式的开头，它们的作用域均延伸到整个公式的未尾，则称为该公式为前束形公式；由前束形的公式利用其真值联结词作成的公式称作准前束形公式。前束范式定理：任意一个谓词演算公式均和一个具有前束形的公式同真假（该前束形公式称为原公式的前束范式）。为什么要讨论范式呢？与命题演算类似，在谓词演算中也有范式所谓的范式就是一种标准的谓词演算公式。12/20/202215 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 一般地范式有两种，一种是前束范式，另一种为斯柯林

15、（Skolem）范式。前束范式定理说明一个公式如果它的所有量词均非否定的出现在公式的最前面，且它们的辖域一直延伸到公式之末，且公式中不出现联结词及，此中形式之公式叫前束范式，如公式 xy z（P（x）F（y，z）Q（y，z）即为具有前束范式之公式。12/20/202216 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 我们说，任一个公式均可表示为前束范式或由任一个公式化归为前束范式。方法如下：1)公式中出现的联结词，之处换以，联结词。2)利用命题演算公式 P=P （PQ）=PQ （PQ）=PQ （PQ）=PQ （PQ）=PQ）=PQ及 （x P（x）=x（P（x）（x P（x）=x（

16、P（x）将公式内否定符号深入至谓词变元前。3)利用改名，代入规则使所有的约束变元均不同并且自由变元及约束变元亦不同。12/20/202217 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 4)利用量词辖域的扩张与收缩等式即：xP（x）Q=x（p（x）Q）xP（x）Q=x（p（x）Q）x P（x）Q=x（p（x）Q）x P（x）Q=x（p（x）Q）扩大量词的辖域至整个公式。下面我们举例说明：例：将公式 （xp（x）yR（y）xF（x）化归为具有前束范式之形式。12/20/202218 第五章 谓词公式的永真性及可满足性与几个常用的重要定理解解：1）去掉联结词及根据公式PQ=PQPQ=P

17、Q原式可推导为：xPxP（x x）yRyR（y y）xFxF（x x）2）将否定符号深入至谓词变元前。根据公式（PQPQ）=PQ=PQ及及（xpxp（x x）=x x（p p（x x），），（xpxp（x x）=xpxp（x x）可推导为：（xpxp（x x）yRyR（y y）xFxF（x x）=（x x（p p（x x）y y（R R（y y）xFxF（x x）3）更改变元符号（x x（P P（x x）y y（R R（y y）xFxF（x x）=（x x（P P（x x）y y（R R（y y）zFzF（z z）4）将量词辖域扩大至整个公式（x x（P P（x x）y y（R R（y y）z

18、FzF（z z）=x y zx y z（p p（x x）R R（y y）F F（z z）12/20/202219 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 前束范式的优点在于它的量词全部集中在公式的前面，此部分可叫公式的首标。而公式的其余部分实际上是一个命题演算公式。当然，前束范式也有它的缺点，其主要缺点是前束范式的首标比较杂乱无章，全称量词与存在量词间的排序无一定规则。1920年斯柯林（Skolem）对它进行了改进，使得首标中所出现的量词均具有一定规则，即使每个存在量词均在全称量词前，这种形式叫斯柯林（Skolem）范式。如：xy z（p（x）Q（y）F（z）即为具有斯柯林（S

19、kolem）范式形式。12/20/202220 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 同前束范式类同，任一公式均可以化归成具有斯柯林范式形式。为了证明这一点，我们分几步来讨论，（方法）1)任一公式首先化归为前束范式。2)我们可以认为这种前束范式中无自由变元，因为如果有自由变元出现，我们可以利用公式 xP（x）P（x）及规则（x）x（x）在公式前加以对应与自由变元全称量词。3）我们还可以认为这种前束范式的首标是以存在量词为开始的，因为如果一公式A是以全称量词开始的，我们可以取一个出现于A内变元u，以及一个谓词G（u），而将公式A换以公式 u（A（G（u）G（u）此时公式与A相等

20、的，而此公式可以转换成以存在量词为开始的前束范式。4）一般地，上述前束范式如果有m个全称量词其后面跟有存在量词，我们就称此公式的极为m，如果我们能证明极为m公式与另一极为m-1公式相等，则多次应用此方法，最后便可得到斯柯林（Skolem）范式。12/20/202221 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 现在我们证明一个极为m公式可与一个极为m-1公式相等。设此公式以n个（n1）存在量词开始，其后至少跟有一个全称量词，形为：x1x1x2x2xnxn yPyP（x1x1，x2x2xnxn，y y）（）（I I）其中P（x1，x2xn，y）是一个具有前束范式形式公式，它仅含有x

21、1，x2xn，y等n+1个自由变元。设H是一个n+1元谓词，它不出现在P内，今作公式：x1x1x2x2xnxn（y y（P P（x1x1，x2x2xnxn，y y）H H（x1x1，x2x2xnxn，y y）zHzH（x1x1，x2x2xnxn，z z）需求证（I）与（II）相等，亦即由（I）可推出（II），且由（II）可推出（I）。现在我们在（II）中将P代入H便得 x1x1x2x2xnxn（y y（P P（x1x1，x2x2xnxn，y y）P P（x1x1，x2x2xnxn，y y）z Pz P（x1x1，x2x2xnxn，z z）再去掉永假部分 y y（P x1P x1，x2x2xnx

22、n，y y）P x1P x1，x2x2xnxn，y y）即得（I），故由（II）可推出（I）。12/20/202222 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 其次我们证明由（I）可推出（II）。我们由命题演算中可知 PP（QRQR）=Q=Q（PRPR）=Q=Q（PRPR）又由 x(Px(P（x x）Q Q（x x）（xPxP（x x）x Q x Q（x x）作改名我们得到如下公式：y(p(y)F(yy(p(y)F(y)()(yp(yyp(y)yF(yyF(y)应用命题计算等式，我们得到 y(p(yy(p(y)y(P(yy(P(y)F(yF(y)yF(yyF(y)在P(y)，F

23、(y)中分别代以：P P（x1x1，x2x2xnxn，y y）和）和H H（x1x1，x2x2xnxn，y y）而得到 y Py P（x1x1，x2x2xnxn，y y）y(py(p（x1x1，x2x2xnxn，y y）H H（x1x1，x2x2xnxn，y y）yHyH（x1x1，x2x2xnxn，y y）上面公式多次应用此推理规则可得：x1x1x2x2xnxn（y(py(p（x1x1，x2x2xnxn，y y）H H（x1x1，x2x2xnxn，y y）)yHyH（x1x1，x2x2xnxn，y y）由改已规则及分离规则得：x1x1x2x2xnxn（y(py(p（x1x1，x2x2xnxn

24、，y y）H H（x1x1，x2x2xnxn，y y）)zHzH（x1x1，x2x2xnxn，z z）我们再将（II）变成前束范式，它以x1x2xn，y开始，继以p（x1，x2xn，y）全称量词及存在量词，最后是全称量词 z，这个公式的级数比（I）级数少1，由此可得到证明。12/20/202223 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 斯柯林范式比前束范式更为优越，它将任一公式顺序划分三个部分，即：公式所有存在量词，命题演算公式，它使得对谓词演算的研究更为方便。下面我们讨论几个重要的定理：同命题演算类同，首先给出定义：定义定义：如果一个公式A对域I中任何指派均取得真值，则说A

25、在I中永真，如果均取得假值，则说A在I中永假，如果至少有一个指派取得真值，则说A在I中可满足，如果至少有一个指派取得假值，则说A在I中非永真。12/20/202224 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 定义定义：如果A在每个非空域中永真（永假），则说A永真（永假），如果A在某个非空域中可满足（非永真），则说A可满足（非永假）。由此定义易得下面的定理：定理定理：若A永真，则说A在I中永真；若A在I中可满足，则说A可满足。和命题演算相仿，有下面的定理成立：12/20/202225 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 定理定理：A与B同真假当且仅当AB永真。

26、AB永真当且仅当A与B均永真。AB永假当且仅当A和B均永假。除这些与命题演算相仿的定理外，还有一些与命题演算中不具备的性质。定定理理：A在I中永真当且仅当A在I中不可满足（即永假）。A在I中可满足当且仅当A在I中非永真。A永真当且仅当A不可满足，A可满足当且仅当A非永真。12/20/202226 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 定理定理：如果I，J为具有相同个数的个体域（个体可不相同），则任一公式A，A在I中永真当且仅当A在J中永真，A在I中可满足当且仅当A在J中可满足。这个定理从集合论的角度来讲，如图：A的个体域I A的个体域J A（I）=A（J）其中（I，J=1，2

27、n）IJ12/20/202227 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 证明证明：因为I，J具有相同个数的个体，所以可以在它们之间建立一一对应。设I中的个体A与J中的个体A一一对应。现在把I上的谓词作如下对应：设Ae1e2en为I上的n元谓词，则令满足下列性质的J中的n元谓词A Ae1e2en为其对应谓词。Aa1an真当且仅当Aa1an真其中各a在I中取值，个a在J中取值。再把I中指派与J中指派作如下对应；设有一个I中指派：(X1Xh；P1Pk；X1Xr)=（a1ah；P10Pk0；A1Ar）简记为：（X；P；X）=（a；p0；A）则命J中的下列指派为其对应指派（a1ah；p

28、10pk0；A1Ar）简记为：（a；p0；A）12/20/202228 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 用数学归纳去证明：（1）A（a；p0；A）=A（a；p0；A）如果A为命题变元（1）式成立。如果A为谓词填式X（x11，x1n）则有A（a；p0；A）=A（a 11，a 1n）=A（a 11，a 1n）=（a；p0；A）即（1）式成立。如果A出现下面五种形式之一。B，B1B2，B1B2，B1B2，B1B2利用归纳假设B1 ，B2均满足（1），易证A也满足（1）。如果A出现yB（X；P；A；Y）形式，根据归纳假设有：（2）B（a；p0；A；y）=B（a；p0；A；y）但

29、yB（a；p0；A；y）真，即在I中有个体b使得B（a；p0；A；b）真，根据（2）B（a；p0；A；b）真即yB（a；p0；A；y）真，故（1）成立。如果A出现yB（x；p；X；y）形式，同理可证（1）成立。因此归纳法（1）得证 由（1）可知A在I中永真（可满足）当且仅当A在J中永真（可满足）定理得证。12/20/202229 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 由本定理可见，永真性和可满足性，与个体域中的个体性质无关，仅与个体域中的个体数有关，因此今后在讨论永真性和可满足性时，我们永远以1，2，K作为具有K个个体的个体域的代表，特各K域，A在K域上永真叫做K永真，A在K

30、域上可满足叫做K可满足。定义定义：如果公式A在I中永真（可满足）当且仅当公式B在I域中永真（可满足），则说A与B在I域中同永真性（同可满足性），如果公式A永真（可满足）当且仅当公式B永真（可满足），则说A与B同永真性（同可满足性）。12/20/202230 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 定义定义：把关于公式A中的一切自由个体变元的全称（存在）量词置在A的首部，所得的公式称为A的全称（存在）封闭式。例如：设A=A=xXxX（x x，y y）yXyX（x x，y y）则A的全称封闭式为：x yx y（xXxX（x x，y y）yXyX（x x，y y）；）；A的存在封闭式

31、为：x xy y（xXxX（x x，y y）yXyX（x x，y y）；）；由定理可知：全称（存在）封闭式中是没有自由变元的。12/20/202231 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 定理定理：A与A的全称封闭式在每个域中均同永真性，A与A的存在封闭式在每个域中均同可满足性。证证：由同永真性和同可满足性的定义容易得证。12/20/202232 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 5.3日常推理过程的讨论 在上几节中我们知道命题演算及谓词演算，下面我们进一步的讨论永真推理过程与假设推理过程。命题演算与谓词演算的讨论过程中我们知道，一些新的定理的求得是根

32、据以证明的定理经过使用一系列的推导规则而得到的，这种定理的证明过程叫做推理过程。这种推理过程有一个特点，即在该过程中所出现的公式均为永真公式，（包括推理规则而得到的中间公式）这种推理过程叫永真推理过程。12/20/202233 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 但是，在日常应用中，情况就有些不同，首先，在日常应用中或在具体的科学领域中，它们不但有数理逻辑的永真公式，而且还有一些对本门学科而言的永真公式。对本门学科的基本定理，定律。如经典力学中的牛顿三大定律，化学中的门捷列夫元素周期表等，这些基本规律仅对某门学科为永真。因此，它的“永真”是具有局限性的，故它并非是数理逻辑中

33、的永真公式。其次，在讨论具体问题时，往往需要设置一些假设、前提、条件等。往往假设条件在某条件成立的情况下可推出某某结论，如集合论中有这样一个定理，一集合为无限集则它必含有与其等势真子集。此定理中“一集合为无限集”即为设置的前提与条件，而“它必含有与其等势真子集”即为推得的结论。12/20/202234 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 又例如：如果水温低于零度时就结冰，此命题中“水温低于零度”为设置前提及条件，而“水结冰”为结论，而这些假设、前提、条件均不是永真的（不管对数理逻辑而言还是对本门学科均非永真）。上述两种类型：有局限性的永真公式以及假设前提条件，在数理逻辑中统

34、称为假设前提。12/20/202235 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 在日常推理过程中，除了使用数理逻辑中的永真公式外，还将使用假设前提（它们也均认为是真的）。如前面集合论中的定理“如果一集合为无限集，它必含有与其等势真子集”在这个定理的证明过程中，假设前提：“一集合为无限集”是作为永真命题使用的，因此，日常推理过程中所出现的公式除逻辑中的永真公式外尚有假设前提（它们并非逻辑永真，但是在讨论具体问题时可以认为是真的）。这种推理过程叫假设推理过程。由于日常推理中很少使用永真推理过程，而都是使用假设推理过程的。12/20/202236 第五章 谓词公式的永真性及可满足性与

35、几个常用的重要定理 例如：前面讲述的集合论中的定理，我们令“一集合为无限集”为A，“它必含有与其等式真子集”为B，则此定理可写为AB。我们一般并不利用永真推理过程去证明AB为永真，而是将A作为永真而去证明B。这就是假设推理过程。而用这种方法所证得的结果，与用永真推理过程所证得AB为永真是否一样呢？也就是说，能否用假设推理过程去替代永真推理过程呢？回答是肯定的，它在理论上是根据推理定理，下面就介简该定理，即推理定理。12/20/202237 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 推理定理给出了永真推理过程与假设推理过程间的关系，这个定理指出了，可用假设推理过程去代替永真推理过程

36、。推理定理推理定理：设A1，A2AnB则必有 A1，A2An-1An B 推论推论：A1，A2An-1An B则必有 A1（A2（A3（AnB）为永真，关於推理证明易证。由推理定理可知，可用假设推理过程来代替永真推理过程，推理定理并给出了由假设推理转化为永真推理的方法。例如要证明Q（PQ）P）为永真公式，由推理定理可知只要证明：Q，PQ P即可。12/20/202238 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 5.4 假设推理过程的讨论 由于假设推理过程的重要性，因此，有必要对假设推理过程作较为详细的探讨，对于永真推理的过程我们比较清楚。例如例如：证明PQ=QP 证明证明PQ=

37、PQ 根据PQ=PQ =PQ根据P=P =QP 根据PQ=QP =QP 根据PQ=PQ 故我们由永真推理过程出发来研究假设推理过程，下面我们来比较一下永真推理过程与假设推理过程的区别。12/20/202239 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 首先在假设推理过程中我们允许假设前提作为永真公式出现在推理过程中，关于这一点，我们可以作假设推理过程中之特有推理规则而引入。但是，假设前提毕意不是永真公式，故在假设推理过程中，若允许假设前提作为永真公式则在使用某些推理规则时需要作一些必要的限制，同时也有必要引入一些新的推理规则，下面我们作一下详细的讨论。（1 1）我们在命题演算及谓

38、词演算中，均引入代入规则，这个规则是建立在永真公式基础上的，即对永真公式以施行代入规则，但是这个规则对假设前提不能使用，对假设前提中出现的问题，谓词不能施行代入，如果不遵守此规定则必会得出许多错误的结论来。12/20/202240 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 例如：我们已知：x x（p p（x x）Q Q（x x）x x（p p（x x）x Qx Q（x x）的逆是不成立的，也就是说：xpxp（x x）x Qx Q（x x）x x（p p（x x）Q Q（x x）不成立。但是如果我们在使用代入规则时不注意的话，则可以很容易的推出这个公式是永真公式。下面我们用错误的假

39、设推理过程的方法证明此公式为永真，并请读者注意，这个证明错在何处。12/20/202241 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 xpxp（x x）x Qx Q（x x）x x（p p（x x）Q Q（x x）（a）xPxP（x x）x Qx Q（x x）假设前提 （b）xPxP（x x）根据规则PQP （c）x x（P P（x x）Q Q（x x）对（b）使用代入规则，所以会推得的错误结论，主要是在于在（c）中不正确的使用了代入规则。12/20/202242 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 （2 2）我们引入一个新的推理规则xA（x）A（e）对于这个

40、规则我们必须作一些说明，我们知道，xA（x）表示存在一些个体使A（x）为真，我们令e就是这样的一些个体，故有A（e）为真，其中A（e）叫做根据xA（x）而作的额外假设，而e叫做额外变元，它是依赖于额外假设的自由变元，故这种自由变元的变化范围与一般自由变元不同，所以用e表示，以示区别，但是不同额外变元e的变化范围也各不相同，因此用e1ei，ei+1等以表示不同的额外变元，为了方便我们将这个规则称为：存在指定规则，并用ES表示。12/20/202243 第五章 谓词公式的永真性及可满足性与几个常用的重要定理n （3 3）对推导规则A A（x x）B B（x x）x x（A A（x x）B B（x

41、x）我们需要做两点限制：（注：该规则证明在习题中）1）对假设前提中所出现的自由变元不能使用此规则，由于规则中自由变元是任意的，而假设前提中的自由变元必须满足假设前提，故不是任意的，因此，两者是不同的，有区别的，因而此规则不能应用于假设前提中所出现的自由变元。2）由于存在指定规则的使用使得此规则在应用时还受到了一些限制。首先，对额外变元不能使用此规则，因为额外变元的变化范围是局部的，所以对额外变元e而言A（e）成立不一定对所有的x有A（x）成立。其次，如果一公式中含有额外变元，则对此公式中的自由变元间是有联系的。12/20/202244 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 例

42、如例如：我们已知 xyP（x，y）下面我们列出此错误的推倒过程，并请读者注意，错在何处？（a）xyP（x，y）假设前提 （b）yP（x，y）规则A（x）B（x）x（A（x）B（x）即（c）（d）（c）y xp（x，y）规则：（d）（e）（d）x P(x,e)规则：A（x）B（x）x（A（x）B（x）即（c）（d）所以会推的错误结论就是由于在（d）中不正确的使用了规则。12/20/202245 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 例例：试用假设推理过程方法证明：（PP（QRQR）（QPRQPR）证：由推理定理可知，只要证：（P（QR），Q，PR即可a)P假设前提b)P（QR）

43、假设前提c)QR分离规则（b），（a）（c）d)Q假设前提e)R分离规则（c），（d）（e）由此定理得证，此公式即为 P P（x x）（x x（p p（x x）Q Q（x x）Q Q（x x），），对比此例，在前面永真推理过程证明时需要十一个步骤，而在这里仅要五步就够了，由此可以看出，用假设推理方法证明比较简单方便。12/20/202246 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 利用假设推理过程方法，还可以使得谓词演算过程规律化，我们并且可将其归结如下：(1)可利用下列推导规则：全称指定规则（US）：x Ax A（x x）A A（x x）存在指定规则（ES）x Ax A（x

44、x）A A（e e）除去式中所有量词，从而可得到没有量词的公式，即命题演算公式。(2)可利用命题演算中的推理方法进行推算。(3)在得出结论前，可利用下列推理规则：全程推广规则（UG）：A A（x x）x Ax A（x x）存在推广规则（E G）：A A（x x）x Ax A（x x）12/20/202247 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 在需要的地方重新加入全程量词及存在量词，使其恢复成谓词演算公式，所要注意的是，在使用这两个规则时，特别是全称推广规则时所受到的限制。从这个过程中可以看出，可以将谓词演算的推导问题归结成命题演算问题，我们举例说明此过程。12/20/20

45、2248 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 例例：试用假设推理过程方法证明下公式：x x（P(x)QP(x)Q（x x）（xP(xxP(x)xQxQ（x）证证：由推理定理可知，只要证：x x（p p（x x）Q Q（x x），），x Px P（x x）x Qx Q（x x）（a）x x（P(x)QP(x)Q（x x）假设前提 （b）P(x)QP(x)Q（x x）US：（a）（b）（c）Xp(xXp(x)假设前提 （d）P(xP(x)US：（c）（d）（e）Q(xQ(x)分离规则（b），（d）（e）（f）x x Q(xQ(x)UG：（e）（f）由此定理得证.12/20/20

46、2249 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 又例：前面提到的三段论推理：“凡人必死，张三是人，故张三必死。”试用谓词演算公式表示。x(M（x）D（x），M（c ）D（c ）其中M（x）表示：“x是人”D（x）表示：“x必死”C表示：“张三”我们证明证明此论证的正确性：（a）x（M（x）D（x）假设前提 （b）M（c ）D（c ）US：（a）（b）（并作变元代入）（c）M（c ）假设前提 （d）D（c ）分离规则：（b）（c ）（d）12/20/202250 第五章 谓词公式的永真性及可满足性与几个常用的重要定理5.5 谓词演算在程序正确性证明上的应用 由于计算机能够代替人

47、的部分脑力劳动，所以计算机具有一定程度的“思维能力”。而数理逻辑则是研究形式逻辑推理的科学，是研究思维活动规律的科学，故两者有着本质的联系，所以，数理逻辑在计算机科学中应用极为广泛，现在我们仅就谓词演算在程序正确性证明中的应用作一简单介绍，由于现代计算机中的程序规模越来越大，复杂度越来越高，所以如何保证程序的正确性问题也就显得越来重要了。12/20/202251 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 一般人可能认为，程序正确性可通过程序的调试而获得保证其实不然，调试可以发现程序的错误，但不能保证程序的正确性，这主要由于在调试时只能选取有限次初值做有限次试验而无法保证程序动态执

48、行时所有可能出现情况的正确性。这样，要解决程序正确性问题，就不能依靠数学方法了，现在我们介绍的方法叫归纳断言法，它由弗洛特（Floyd）首先提出，此方法是目前程序正确性证明中最为流行的一种方法。这种方法基本上利用谓词演算作为讨论的工具，我们以验证除法程序正确性为例来说明此方法。12/20/202252 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 对于除法x/y我们有下面公式：x=y*q+r 我们可用过程形式将除法程序编写如下：procedure DIVIDE：comment x=y*q+r，x0，y0；q：=0；r：=x；uhile yy do begin r：=r-y；q：=q+

49、1 end end 也可以将其画成算法流程图12/20/202253 第五章 谓词公式的永真性及可满足性与几个常用的重要定理q q：=0=0r r：=x=xyryrq q：=q+1=q+1 r r：=r-y=r-y入口入口出口出口图一图一F F12/20/202254 第五章 谓词公式的永真性及可满足性与几个常用的重要定理入口入口q q：=0=0r r：=x=xyryrq q：=q+1=q+1 r r：=r-y=r-y出口出口IIIII II IA A：p p（x x，y y）:x0y0:x0y0B B：Q Q（x x，y y，q q，r r）：）：x=y*x=y*q+rr0q+rr0C C：

50、F F（x x，y y，q q，r r）：）：x=y*x=y*q+rrq+rr y y IIIIII 图图2 2 除法流程图中断言设置示意图除法流程图中断言设置示意图12/20/202255 第五章 谓词公式的永真性及可满足性与几个常用的重要定理 为了证明此程序的正确性,我们首先在其入口处A对输入的初始数据设置一个断言,此既是初始数据所要满足条件,它是一个谓词,在这里它是:p p（x,yx,y）：）：x0 x0，y0y0 在出口处C也设置一个断言，它刻划了程序执行结束时，输入变元与输出变元间所应满足的关系，它也是一个谓词，在这里它是:F F（x x，y y，q q，r r）：）：x=y*x=y