资源描述：
《前束范式推理》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、主要内容：•范式¢前束范式¢Skolem范式•推理理论¢与量词有关的规则-吴扬扬-1§2.4范式(1)•前束范式：前束词母式形为Qx…QxB(r≥0)的公式,其中:Q为量词,B不含量词的公式11rri例1:∀x∃y∀z(P(x,y)→Q(y,z))R(x,y)?(∀x)P(x)∧(∃y)Q(y)?*所有量词均非否定地出现在公式开头且量词的辖域均延伸到整个公式的末尾。¢前束析取范式¢前束合取范式¢设A为合式公式,B为前束范式,若AÙB,则称B为A的前束范式.¢存在定理：任何合式公式A都有与之等价的前束范式.-吴扬扬-2§2.4范式(2)skolem»例2：求∀x(F(
2、x)→G(x))→(∃xF(x)→∃xG(x))的前束范式.解：∀x(F(x)→G(x))→(∃xF(x)→∃xG(x))蕴涵等值式Ù┐∀x(┐F(x)∨G(x))∨(┐∃xF(x)∨∃xG(x))量词转换德摩根Ù∃x(F(x)∧┐G(x))∨(∀x┐F(x)∨∃xG(x))-①换名Ù∃x(F(x)∧┐G(x))∨∀y┐F(y)∨∃zG(z)量词扩张收缩律Ù∃x∀y∃z((F(x)∧┐G(x))∨┐F(y)∨G(z))---前束范式①Ù(∃x(F(x)∧┐G(x))∨∃xG(x))∨∀x┐F(x)∃对∨可分配Ù∃x((F(x)∧┐G(x))∨G(x))∨∀x┐F(x
3、)换名Ù∃x((F(x)∧┐G(x))∨G(x))∨∀y┐F(y)量词扩张收缩律Ù∃x∀y((F(x)∧┐G(x))∨G(x))∨┐F(y))分配律Ù∃x∀y(F(x)∨G(x)∨┐F(y))----------------前束范式3§2.4范式(3)•Skolem范式¢定义：设公式G是一个前束范式，消去G中所有的存在量词，所得到的公式称为Skolem范式。不是等价变换¢Skolem变换：消去存在量词的变换。设前束范式为Qx,…,QxB,Qx是存在量词(1≤i≤r)11rrii⑴如果Q的左边无全称量词，则用一个个体常元a来取代x在B中ii一切出现处，且该a不同于B中
4、的任何其他常元符号。⑵如果Q的左边有全称量词∀x,…,∀x，则直接用一个函数ijkf(x,…,x）来取代x在B中一切出现处，该函数符号f不同于jkiB中的任何其他函数符号。例3:求例2的Skolem范式.-吴扬扬-4§2.4范式(4)¢定理2.4.1:设A为合式公式,那么A是永假式iffA的Skolem范式是永假式。¢引理2.4.1:设C为∀x,…,∀x∃yB(x,…,x,y),1t1tC’为∀x,…,∀xB(x,…,x,f(x,…,x)),那么1t1t1tC是永假式iffC’是永假式。证明：必要性若C是永假式，但C’不是永假式，则有解释I，使C’在I下为1，即∀a
5、,…,a∈D,有B(a,…,a,f(a,…,a))为1,1tI1t1t∵f(a,…,a)∈D，1tI∴∀a,…,a∈D,有a=f(a,…,a)，使B(a,…,a,a)为1,1tI1t1t与C是永假式矛盾。充分性证明见pp.48-吴扬扬-5§2.5推理理论(1)»例题1-2»例题2»例题3•约定:A(x)表示x是A中的自由变元,A(y)表示用y取代A中自由变元x所有出现所得的结果.例:设A(x)：∀xP(x)∨Q(x)∨R(x,y),则A(y)为∀xP(x)∨Q(y)∨R(y,y)•与量词有关的规则:这些规则只能对前束范式使用！∀xA(x)¢全称指定规则US：,个体词
6、y不在A(x)约束出现(pp.50例)∴A(y)∃xA(x)c不在A(x)或其前推导中出现的个¢存在指定规则ES：,∴A(c)体符号,且A(x)中无其他自由变元A(y)¢全称推广规则UG：,若A(y)对任意的y均成立(例2.5.5)∴∀xA(x)A(c)¢存在推广规则EG：,x不在A(c)中出现∴∃xA(x)-吴扬扬-6§2.5推理理论(2)»例1:证明苏格拉底论证：∀x(M(x)→D(x)),M(a)⇒D(a)证明:(1)M(a)前提(2)∀x(M(x)→D(x))前提(3)M(a)→D(a)(2)US(4)D(a)(1)(3)假言推论例2:证明∀x(P(x)∨Q
7、(x))⇒∃x¬P(x)→∃xQ(x).证明:(1)∃x¬P(x)附加前提(2)¬P(c)(1)ES(3)∀x(P(x)∨Q(x))前提(4)P(c)∨Q(c)(3)US(5)Q(c)(2)(4)析取三段论(6)∃xQ(x)(5)EG7(7)∃x¬P(x)→∃xQ(x)CP§2.5推理理论(3)»例2的证明∀x(P(x)∨Q(x))⇒∃x¬P(x)→∃xQ(x)采用下列推导过程行吗？为什么？(1)∀x(P(x)∨Q(x))前提(2)P(c)∨Q(c)(3)US(3)∃x¬P(x)附加前提(4)¬P(c)(1)ES(5)Q(c)(2)(4)析取三段论(6)∃xQ(
