真
真的很烦
Unregistered / Unconfirmed
GUEST, unregistred user!
我需要源程序。谢谢。最好有注释。
举例说明:
表达式为: x { [ Roman (x)∧know(x,Marcus)]→[hate(x,Caesar) ∨ ( y ( z hate(y,z)→thinkcrazy(x,y) ) ) ] }
把任意谓词公式转化为合取范式的步骤
1. 用a→b 等价于~a∨b 这一事实删去→ .对上面给出的合式公式作此转换后得:
x { ~ [ Roman (x)∧know(x,Marcus)]
∨[hate(x,Caesar) ∨ ( y ~ ( z hate(y,z)
∨thinkcrazy(x,y) ) ] }
2. 用规则 ~(~P)=P,摩根定律(即~(a∧b)= ~a∨~b 且~(a∨b)= ~a∧~b )和量词之间的
关系(即~ x p (x)= x ~p(x)和~ x p(x)= x ~p(x) )来缩减~的辖域.对由第1步产生的
合式公式作此转换后得:
x { ~ [ Roman (x)∨know(x,Marcus)]
∨[hate(x,Caesar) ∨ ( y z ~hate(y,z))
∨thinkcrazy(x,y) ) ] }
3.把变量标准化,使得每一量词约束一个唯一变量.因为变量都是哑名,所以此过程不会
影响该合式公式的真值.例如，公式
x p(x)∨ x Q(x)
将转换为:
x p(x)∨ y Q
此步是为下一步做准备.
4.把所有量词移到该公式的左部,并且不改变它们的相对顺序.这一点是可以做到的,因
为变量名不冲突.对第2步的公式执行这一操作后得:
x y z [ ~ Roman (x)∨~know(x,Marcus)]
∨[hate(x,Caesar)∨( ~hate(y,z)∨thinkcrazy(x,y) ) ]
此时的公式称为前缀范式,即前缀是量词,后接一个无量词母式.
5.删去存在量词.含有一存在量化变量的公式断言,存在一个可代换变量的值,他使该公
式为真.通过用能产生预想值的函数替代变量便可删去量词.因为不必知道如何产生该值
,,故需对这样的每一代换建立一个新的函数名.除函数的存在性外,对他们不能做任何断
言.例如,公式
x President(x)
或转换成公式 President(s1)
其中,s1是无参函数,它能产生满足President的值
若存在量词出现在全称量词的辖域内,则满足该谓词的值,可能依赖于全称量化变量的值
.例如,在公式
x y fatherof(y,x)
中,满足fatherof和y值依赖于x的特殊值.于是,要产生的函数所带的形参数,与控制该表
达式所在辖域的全称量词数相同.这样,上例将转换成: x fatherof(s2(x),x)
如此产生的函数称为skolem函数.无参 函数有时称为skolem常量.
6.丢掉前缀.此刻剩下的所有变量都是全称量化的.因此,可以丢掉前缀,而且所用的任一
证明过程均可简单假定:它见到的任一变量都是全称量化的.于是,在第4步产生的公式应
变为:
[ ~ Roman (x)∨~know(x,Marcus)]
∨[hate(x,Caesar)∨( ~hate(y,z)∨thinkcrazy(x,y) ) ]
7.把母式转换成析取元的合取式.因为本例中没有AND,故需做的事就是利用OR的结合律
a∨(b∨c)=(a∨b)∨c ,并去掉括号,这样得到:
~ Roman (x)∨~know(x,Marcus)∨hate(x,Caesar)∨~hate(y,z)∨thinkcrazy(x,y)
然而,常常还需要利用分配律(a∧b)∨c=(a∨c)∧(b∨c) 例如,利用分配律后,公式
(winter∧wearingboots)∨ (summer∧wearingsandals)
变为:
[winter∨(summer ∧wearingsandals)]
∧ [wearingboots ∨ (summer ∧ wearingsandals)]
因为上式还有由 OR 连起来的合取元,故再应用一次分配律后得:
(winter∨summer)
∧(winter∨wearingsandals)
∧(wearingsandals ∨summer)
∧(wearingsandals∨wearingsandals)
8.称每一合取元为一独立的子句.为使一合式公式为真,从该合适公式生成出来的所有
子句合并起来以表达由原合式公式表达的相同事实集.
9.对由第8步生成出来的子句集中的变量作分离标准化也就是说,给变量重新命名,使得
任意两个子句不会有相同的变量.作这种转换主要依赖于事实:
x(p(x) ∧ Q(x))= x P(x) ∧ xQ(x)
因为每一子句是一个不同的和取元,并且所有变量都是全称量化的,所以两子句的变量之
间不存在任何关系,即使同一合式公式生成出来的两个子句亦如此.
举例说明:
表达式为: x { [ Roman (x)∧know(x,Marcus)]→[hate(x,Caesar) ∨ ( y ( z hate(y,z)→thinkcrazy(x,y) ) ) ] }
把任意谓词公式转化为合取范式的步骤
1. 用a→b 等价于~a∨b 这一事实删去→ .对上面给出的合式公式作此转换后得:
x { ~ [ Roman (x)∧know(x,Marcus)]
∨[hate(x,Caesar) ∨ ( y ~ ( z hate(y,z)
∨thinkcrazy(x,y) ) ] }
2. 用规则 ~(~P)=P,摩根定律(即~(a∧b)= ~a∨~b 且~(a∨b)= ~a∧~b )和量词之间的
关系(即~ x p (x)= x ~p(x)和~ x p(x)= x ~p(x) )来缩减~的辖域.对由第1步产生的
合式公式作此转换后得:
x { ~ [ Roman (x)∨know(x,Marcus)]
∨[hate(x,Caesar) ∨ ( y z ~hate(y,z))
∨thinkcrazy(x,y) ) ] }
3.把变量标准化,使得每一量词约束一个唯一变量.因为变量都是哑名,所以此过程不会
影响该合式公式的真值.例如，公式
x p(x)∨ x Q(x)
将转换为:
x p(x)∨ y Q
此步是为下一步做准备.
4.把所有量词移到该公式的左部,并且不改变它们的相对顺序.这一点是可以做到的,因
为变量名不冲突.对第2步的公式执行这一操作后得:
x y z [ ~ Roman (x)∨~know(x,Marcus)]
∨[hate(x,Caesar)∨( ~hate(y,z)∨thinkcrazy(x,y) ) ]
此时的公式称为前缀范式,即前缀是量词,后接一个无量词母式.
5.删去存在量词.含有一存在量化变量的公式断言,存在一个可代换变量的值,他使该公
式为真.通过用能产生预想值的函数替代变量便可删去量词.因为不必知道如何产生该值
,,故需对这样的每一代换建立一个新的函数名.除函数的存在性外,对他们不能做任何断
言.例如,公式
x President(x)
或转换成公式 President(s1)
其中,s1是无参函数,它能产生满足President的值
若存在量词出现在全称量词的辖域内,则满足该谓词的值,可能依赖于全称量化变量的值
.例如,在公式
x y fatherof(y,x)
中,满足fatherof和y值依赖于x的特殊值.于是,要产生的函数所带的形参数,与控制该表
达式所在辖域的全称量词数相同.这样,上例将转换成: x fatherof(s2(x),x)
如此产生的函数称为skolem函数.无参 函数有时称为skolem常量.
6.丢掉前缀.此刻剩下的所有变量都是全称量化的.因此,可以丢掉前缀,而且所用的任一
证明过程均可简单假定:它见到的任一变量都是全称量化的.于是,在第4步产生的公式应
变为:
[ ~ Roman (x)∨~know(x,Marcus)]
∨[hate(x,Caesar)∨( ~hate(y,z)∨thinkcrazy(x,y) ) ]
7.把母式转换成析取元的合取式.因为本例中没有AND,故需做的事就是利用OR的结合律
a∨(b∨c)=(a∨b)∨c ,并去掉括号,这样得到:
~ Roman (x)∨~know(x,Marcus)∨hate(x,Caesar)∨~hate(y,z)∨thinkcrazy(x,y)
然而,常常还需要利用分配律(a∧b)∨c=(a∨c)∧(b∨c) 例如,利用分配律后,公式
(winter∧wearingboots)∨ (summer∧wearingsandals)
变为:
[winter∨(summer ∧wearingsandals)]
∧ [wearingboots ∨ (summer ∧ wearingsandals)]
因为上式还有由 OR 连起来的合取元,故再应用一次分配律后得:
(winter∨summer)
∧(winter∨wearingsandals)
∧(wearingsandals ∨summer)
∧(wearingsandals∨wearingsandals)
8.称每一合取元为一独立的子句.为使一合式公式为真,从该合适公式生成出来的所有
子句合并起来以表达由原合式公式表达的相同事实集.
9.对由第8步生成出来的子句集中的变量作分离标准化也就是说,给变量重新命名,使得
任意两个子句不会有相同的变量.作这种转换主要依赖于事实:
x(p(x) ∧ Q(x))= x P(x) ∧ xQ(x)
因为每一子句是一个不同的和取元,并且所有变量都是全称量化的,所以两子句的变量之
间不存在任何关系,即使同一合式公式生成出来的两个子句亦如此.