东南大学离散数学

《东南大学离散数学》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、2.4可满足性问题与消解法可满足性问题：用于证明A是否永真用于验证逻辑蕴涵A1…AkB永真当且仅当A1…AkB永假解决方法真值表主析取范式主合取范式缺点：计算量大2.4可满足性问题与消解法无论是命题演算还是谓词演算，自然推理系统是比较便于使用的，但对于计算机实现来说，仍然过于复杂。消解法2.4可满足性问题与消解法分离规则可改为说明：该规则要求“消去两个互补文字”。“操作”特色对第二种形式作如下的推广：（1）2.4可满足性问题与消解法设C1，C2为两个简单析取式，称为子句，L1，L2是分别属于C1，C2的互补文字对，用C-L表示从子句C中删除文字L后所得的子句

2、，那么消解原理可表示为：其中C1,C2称为消解母式，L1，L2称为消解基，而(C1-L1)∨(C2-L2)称为消解结果。2.4可满足性问题与消解法例：设C1为R∨┐P∨Q，C2为P∨┐Q以P，┐P为消解基的消解结果是R∨Q∨┐Q以Q，┐Q为消解基的消解结果是R∨┐P∨P特别地，当C1，C2都是单文字子句，且互补时，C1，C2的消解结果不含有任何文字，这时我们称其消解结果是“空子句”（nil），常用符号λ表示之,空子句λ是永远无法被满足的。2.4可满足性问题与消解法定理1：设C是C1，C2的消解结果，那么C是C1和C2的逻辑结果。说明消解原理作为推理规则是适当的。作为特别情

3、况，p与┐p的消解结果是λ，λ实质上是p∧┐p的另一种表示形式,它们都是不可满足的。给定一个合取范式S，S的所有简单析取式称为S的子句集。重复使用消解规则，可以的到一个子句序列。2.4可满足性问题与消解法定义：设S为一子句集，称C是S的消解结果，如果存在一个子句序列C1，C2，…,Cn（=C），使Ci(i=1,2,…,n)或者是S中子句，或者是Ck，Cj(k,j

4、1，C2，…,Cn（=λ）是S的一个否证。若S可满足，即有某个赋值使S中所有子句为真，那么可对n归纳证明，使C1，C2，…,Cn为真，从而(Cn)=(λ)=1，导致矛盾。证：n=1时，因C1S，显然(C1)=1。设对任意k

5、.4可满足性问题与消解法例设子句集S由以下四个子句组成：（1）┐p∨q（2）p∨q（3）p∨┐q（4）┐p∨┐q证明S是不可满足的。可如下作出S的否证：（5）q由（1），（2）消解得（6）┐q由（3），（4）消解得（7）λ由（5），（6）消解得2.4可满足性问题与消解法例：求证(p→q)∧(p→r)→(p→q∧r)永真。证S为上式的否定的子句集，S由以下子句组成：（1）┐p∨q（2）┐p∨r（3）p（4）┐q∨┐r作出S的否证：（5）q由（1），（3）消解得（6）r由（2），（3）消解得（7）┐r由（4），（5）消解得（8）λ由（6），（7）消解得因此(p→q)∧(p→r

6、)→(p→q∧r)为永真式。2.4可满足性问题与消解法说明：一般命题公式都可化成等值的合取范式合取范式是不可满足的当且仅当它有否证用消解原理进行推理是完全可以用计算机来实现的。当然，如果让机器盲目地进行消解，会产生许多不必要的消解及大量未必有用的中间结果，因而效率是不高的。