|
2.2.5 建立子句集举例
 |
例1: |
| 若群F中任一元素x都有 x・x =e (单位元) 那么F是交换群。 这是个代数定理，为实现机器的自动证明，首先需给出这个定理的逻辑描述，进而化成子句形之后再作推理，这里仅限于建立起子句形。由于机器不知群的定义，所以证明之前需将有关定义的内容一一加以描述，并作为定理条件。 设论域为F，谓词P(x ,y ,z)表示x・y = z，依群的定义有  ：若
x,y∈F 则 x・y ∈F可形式描述为 (  x)(y)( z)P(x,y,z) ：若x,y,z
∈F 则(x・y)・z =x・(y・z)可形式描述为 ( x)(y)(z)(u)(v)(w)[(P(x,y,u)∧P(y,z,v)∧P(u,z,w)→P(x,v,w)) ∧(P(x,y,u)∧P(y,z,v)∧P(x,v,w)→P(u,z,w))]  ：若e
为单位元 则x・e = e・x = x 对任一x∈ F可形式描述为 ( x)(P(x,e,x)∧P(e,x,x)) ：若
x∈F 必有 x-1∈ F 使x・x-1=
x-1・x = e 成立。可形式描述为 ( x)P(x,x-1,e)∧P(x-1,x
e,))所要证明的定理B是，对x,y∈ F 如果 x・x=e 必有 x・y =y・x 可形式描述为 ( x
P(x,x,e)→(u)(v)(w)(P(u,v,w)→P(v,u,w))这样我们要证明的定理是 ∧∧∧→B为此需将 ，，，和～B
分别化成 SKOLEM 标准形，进而分别写出子句形c， , , ,S～B再求其并集，便得子句集（用到2.2.4）不难计算出  ：{P(x,y,f(x,y))}：{～P(x,y,u)
∨～P(y,z,v) ∨ ～P(u,z,w) ∨ P(x,v,w),～P(x,y,u) ∨ ～P(y,z,v) ∨～P(x,v,w) ∨ P(u, z,w)} ：{P(x,e,x),P(e,x,x)}：{P(x,x-1,e)},P(x-1,x,e)}S～B：{P(x,x,e),P(a,b,c),～P(b,a,c)} 从而S= ∪∪∪∪S～B共含有10个子句。 |
|
|
例2: |
| 证明梯形的对角线与上下底构成的内错角相等。 这是个初等几何问题，为实现机器的自动证明，像例1一样先给出逻辑描述，建立子句集。 设已给梯形的顶点依次为a ,b ,c ,d 。引入谓词 T(x ,y,u,v)表示以xy为上底，uv为下底的梯形。 P(x,y,u,v)表示x y‖u v E(x ,y ,z,u ,v ,w)表 ∠xyz=∠uvw 问题的逻辑描述和相应的子句集为 ：(x)(y)(u)(v)(T(x,y,u,v)→P(x,y,u,v))(梯形上下底平行) ：～T(x,y,u,v)∨P(x,y,u,v)：(x)(y)(u)(v)(P(x,y,u,v)→E(x,y,v,u,v,y))(平行内错角相等) ：～P(x,y,u,v)∨E(x,y,v,u,v,y)：T(a,b,c,d)
(已知)：T(a,b,c,d)B：E(a,b,d,c,d,b) (要证的结论) S～B：～E(a,b,d,c,d,b) 从而S＝ ∪∪∪∪S～B共含有10个子句。 |
|
| 例1和例2是代数和几何的定理证明问题，只要把定理描述清楚了，建立起子句集，然后作推理给出定理成立与否的证明就够了，这是一类只需回答正确与否的问题，另一类如机器人动作问题(例3)，对所做的推理要求给出一系列的动作，程序设计自动化(例4)也属这类问题。 | |
|
例3: |
| 猴子香蕉问题 已知一串香蕉挂在天花板上，猴子直接去拿是够不到的，但猴子可以走动且可以搬着梯子走动，也可以爬上梯子来达到吃香蕉的目的。对这个问题的描述，不可忽视动作的先后次序，需体现出时间概念。常用的方法是引入状态S来区分动作的先后，以不同的状态表现不同的时间，而状态间的转换由一些算子(函数)来实现。 首先引入谓词 P(x,y,z,s)表示猴子位于x处，香蕉位于y 处，梯子位于z处，相应的状态为s。或说猴子在x 处，香蕉在y 处，梯子在z处，而状态又为s时，谓词P(x,y,z,s)方为真。 R(s)表示s状态下猴子吃到香蕉。 ANS(s)表示形式谓词 ，只是为求得回答的动作序列而虚设的。 其次引入状态转移函数。 Walk (y,z,s)表示原状态s下，在walk作用下猴子从y走到z 处所建立的一个新状态。 Carry(y,z,s)表示原状态s 下，在Carry 作用下猴子搬着梯子从y走到z 处建立的一个新状态。 Climb(s) 表示原状态s下，在Climb作用下猴子爬上梯子所建立的一个新状态。 设初始状态为S0,猴子位于a,香蕉位于b ,梯子位于c。 问题可描述如下： ：(x)(y)(z)(s)(P(x,y,z,s)→P(z,y,z,walk(x,z,s)))(猴子走到梯子处) ：～P(x,y,z,s)∨(P(z,y,z,walk(x,z,s))：(x)(y)(s)(P(x,y,x,s)→P(y,y,y,carry(x,y,s)))(猴子搬着梯子到y) ：～P(x,y,x,s)∨P(y,y,y,carry(x,y,s))：(s)(P(b,b,b,s)→R(climb(s)))(猴子爬上梯子吃到香蕉) ：～P(b,b,b,s)∨R(climb(x)))：P(a,b,c,s0)：P(a,b,c,s0)B：( s)R(s)S～B：～R(s)∨ANS(s) 其中ANS(s)是人为附加的，在推理过程中ANS(s)的变量s 同R(s)的变量将作同样的变换，当证明结束时，ANS(s)中变量s便给出所要求的整个动作序列。 子句集S={ ,,,,S～B} |
|
|
例4: |
| 简单的程序综合问题 若一台计算机有寄存器a,b,c和累加器A，要求自动设计实现 (a)+(b)→c 的程序。 引入谓词 P(u,x,y,z,s)表示累加器A、寄存器a,b,c分别存入u,x,y,z时相应的状态为s。 已知的函数(机器指令)： load(x,s)表示状态s下，对任一寄存器x来说，实现(x)→A后的新状态。 add(x,s)表示状态s下，对任一寄存器x来说(x)+(A)→A后的新状态。 store(x,s)表示状态s下，对任一寄存器x来说，实现(A)→x后的新状态。 问题可描述为 ：(u)(x)(y)(z)(s)P(u,x,y,z,s)→P(x,x,y,z,load(a,s))) ((a)→A) ：～P(u,x,y,z,s)∨P(x,x,y,z,load(a,s))：(u)(x)(y)(z)(P(u,x,y,z,s)→P(u+y,x,y,z,add(b,s))) ((b)+(A)→A) ：～P(u,x,y,z,s)∨P(u+y,x,y,z,add(b,s))：(u)(x)(y)(z)(P(u,x,y,z,s)→P(u,x,y,u,store(c,s))) ((A)→c) ：～P(u,x,y,z,s)∨
P(u,x,y,u,store(c,s))：P(1,2,3,4,d)(初状态d下，累加器A与寄存器a,b,c中的数值) ：P(1,2，3,4，d)B：( u)(x)(y)(s)P(u,x,y,x+y,s)S～B：～P(u,x,y,x+y,s)∨ANS(s) 子句集S={ ,,,,S～B}除例1.2和例3.4两类问题外，另一类问题是要求就某一问题给出具体的答案(例5)。如回答是……，谁在何处 ……等，这也可以用逻辑推理来求解。 |
|
|
例5: |
| 对所有的x,y,z来说，如果y是x的父亲，z又是y的父亲，则z是x的祖父。又知每个人都有父亲，试问对某个人来说谁是他的祖父？ 引入谓词 P(x,y) 表示x是y的父亲。 Q(x,y) 表示x是y的祖父。 于是有 ：(x)(y)(z)(P(x,y)∧P(y,z)→Q(x,z))：～P
(x,y) ∨ ～P(y,z) ∨ Q(x,z)：(y)(x)P(x,y)：P(f(y),y)B：( x)(y)Q(x,y)S～B：～Q(x,y)∨ANS(x) 相应的子句集S={ ,,S～B} |