资源描述：
《求下列各式的斯柯伦标准形和子句集.doc》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、练习3.11、求下列各式的斯柯伦标准形和子句集。（1）┐("xP(x)→$y"zQ(y,z))（2）"x(┐E(x,0)→$y(E(y,g(x))∧"z(E(z,g(x))→E(y,z))))（3）┐("xP(x)→$yP(y))（4）（1）∧（2）∧（3）解（1）┐("xP(x)→$y"zQ(y,z))┝┥┐"xP(x)∧$y"zQ(y,z)┝┥$x┐P(x)∧$y"zQ(y,z)斯柯伦标准形：┐P(e1)∧Q(e2,z)子句集：{┐P(e1)，Q(e2,z)} （2）"x(┐E(x,0)→$y(E(y,g(x))∧"z(E(z,g(x)
2、)→E(y,z))))┝┥"x$y"z(E(x,0)∨(E(y,g(x))∧(┐E(z,g(x))∨E(y,z))))┝┥"x$y"z((E(x,0)∨E(y,g(x)))∧(E(x,0)∨┐E(z,g(x))∨E(y,z)))斯柯伦标准形：(E(x,0)∨E(f(x),g(x)))∧(E(x,0)∨┐E(z,g(x))∨E(f(x),z))子句集：{E(x,0)∨E(f(x),g(x)),E(x,0)∨┐E(z,g(x))∨E(f(x),z)}（3）┐("xP(x)→$yP(y))┝┥"xP(x)∧┐$yP(y)┝┥"xP(x)∧"y┐P
3、(y)┝┥"x"y(P(x)∧┐P(y))斯柯伦标准形：P(x)∧┐P(y)子句集：{P(x),┐P(y)} （4）（1）∧（2）∧（3）斯柯伦标准形：┐P(e1)∧Q(e2,z)∧(E(x,0)∨E(f(x),g(x)))∧(E(u,0)∨┐E(y,g(u))∨E(f(u),y))∧P(w)∧┐P(v)子句集：{┐P(e1)，Q(e2,z),E(x,0)∨E(f(x),g(x)),E(u,0)∨┐E(y,g(u))∨E(f(u),y),P(w),┐P(v)} 2、设公式A1，A2的子句集分别为S1，S2，如果S1与S2等值（表示对应的斯柯
4、伦标准形有相等的真值），问是否一定有A1与A2等值，为什么？解不一定有A1与A2等值。例如，个体域为自然数集合，A1为$yP(y)，A2为$yQ(y)，P(y)表示：y是偶数，Q(y)表示：y是负数。$yP(y)与$yQ(y)不等值，但P(e1)与Q(e2)在解释I把e1，e2确定为奇数时，却是等值的。 3、假如要利用子句集不可满足性来证明(P→Q)∧(Q→R)→(P→R)永真。试作出待证公式否定的子句集。解待证公式否定的子句集为：{┐P∨Q,┐Q∨R,P,┐Q} 4、要利用子句集不可满足性来证明例2.25的推理是正确的。试作出这一推理的否
5、定（┐（前提1∧前提2→结论））的子句集。解 5.试简述A(e/x)或A(f(y1,…,yn)/x,y1,…,yn)可以在应用消解原理的推理中代替$xA(x)或"y1…"yn$xA(x,y1,…,yn)的原因,以及选择e,f应注意的事项。解A(e/x)或A(f(y1,…,yn)/x,y1,…,yn)可以在应用消解原理的推理中代替$xA(x)或"y1…"yn$xA(x,y1,…,yn)的原因是：（1）（1） 用消解原理证明定理A或证明G┝A，是通过确认┐A和B1∧¼∧Bn∧┐A(B1,¼,Bn为G中公式)的不可满足性
6、来实现的。（2）（2） A(e/x)，A(f(y1,…,yn)/x,y1,…,yn)与$xA(x)，"y1…"yn$xA(x,y1,…,yn)的不可满足性是相同的。选择e,f应注意选择新常元和新函数符号，即在推理过程中尚未使用过的常元和函数符号。练习3.21、证明下列子句集是不可满足的。（1）S={p∨q,┐q∨r,┐p∨q,┐r}解（1）p∨q（2）┐q∨r（3）┐p∨q（4）┐r（5）┐q由（2）（4）消解得（6）p由（1）（5）消解得（7）┐p由（3）（5）消解得（8）□ （2）S={p∨q,q∨r,r∨w,
7、┐r∨┐p,┐w∨┐q,┐q∨┐r}解（1）p∨q（2）q∨r（3）r∨w（4）┐r∨┐p（5）┐w∨┐q（6）┐q∨┐r（7）┐r∨q由（1）（4）消解得（8）q由（2）（7）消解得（9）┐w由（5）（8）消解得（10）┐r由（6）（8）消解得（11）r由（3）（9）消解得（12）□由（10）（11）消解得 2、用消解原理证明下列逻辑蕴涵式。（1）(p∨q)→r┝(p→r)∧(q→r)解S={┐p∨r,┐q∨r,p∨q,p∨┐r,q∨┐r,┐r}（1）┐p∨r（2）┐q∨r（3）p∨q（4）p∨┐r（5）q∨┐r（6）┐r（7）┐p由（1
8、）（6）消解得（8）┐q由（2）（6）消解得（9）q由（3）（7）消解得（10）□由（8）（9）消解得 （2）(p→r)∧(q→r)┝(p∨q)→r解S={┐p∨r,┐q∨r,p
