<![CDATA[消解原理:
在我们前面所说的谓词公式,推理规则和置换合一等概念基础上我们进一步研究消解原理.
什么是消解? 我们举个例子:如果存在公式E1\/E2和另一个公式~E2\/E3,那么E1\/E3在逻辑上
就成立,这就是消解,我们称E1\/E3为E1\/E2和~E2\/E3的消解式.
在说明消解过程之前,我们先说明任意一谓词演算公式可以化成一个字句集.变换过程如下:
1.用\/和~符号消去=> 如:以~A\/B替换A=>B
2.减少否定符号的辖域,每一个否定符号只用到一个谓词符号上 如:以~A\/~B替代~(A/\B)
3.对变量标准化,在任一量词辖域内,受量词约束的变量为一哑元.应该保证每个来量词有自己
的唯一的哑元. 如:(\-/ x){P(x)=>("倒E" x)Q(x)} 标准化为 (\-/ x){P(x)=>("倒E" y)Q(y)}
4.消去存在量词
5.化为前约束
6.把母式化为合取范式 如:把A\/(B/\C)化为(A\/B)/\(A\/C)
7.消去前称量词 第4步以消去了存在量词,公式中只剩下全称量词了.
8.消去/ 9.更换变量的名称
消解推理规则:
1.假言推理:
已知:P和~P\/Q(即P=>Q)
结论:Q
2.合并:
已知:P\/Q和~P\/Q
结论:Q
3.重言式:
已知:P\/Q和~P\/~Q
结论:P\/~P和Q\/~Q
4.矛盾式:
已知:~P和P
结论:NIL
5.三段论:
已知:~P\/Q(即P=>Q)和~Q\/R(即Q=>R)
结论:~P\/R(即P=>R)
我们可以合并上面几个运算为一简单的推理规则.]]>
|
本类阅读TOP10