第2章谓词逻辑上机练习答案

应用离散数学谓词逻辑PAGE杭电－周丽、方景龙第二章PAGE3第2章谓词逻辑上机练习编写下列程序并计算至少1个算例1．给定有限个体域上的一元命题函数，判断由组成的谓词公式是永真式、永假式还是可满足式。（1）实验原理在有限个体域下，量词可以展开为命题公式，实现谓词公式真值判定：1.设有限个体域D={a1,a2,...,an}，一元谓词为P(x)；2.全称量词展开：∀xP(x)⇔P(a1)∧P(a2)∧…∧P(an)（所有个体均为真则整体为真）；3.存在量词展开：∃xP(x)⇔P(a1)∨P(a2)∨…∨P(an)（任意一个个体为真则整体为真）。公式判定定义：-永真式：个体域内所有赋值下，谓词公式真值恒为1；-永假式：个体域内所有赋值下，谓词公式真值恒为0；-可满足式：至少存在一组赋值使公式为真（非永假式）。本次实验设定个体域D={1,2}，批量测试经典谓词公式，实现三类公式自动判定。(2)程序代码defpredicate_judge():#1.定义有限个体域（可自行修改）domain=[1,2]#2.自定义一元谓词函数P(x)，可自由修改逻辑规则defP(x):#示例规则：x=1为真，x=2为假ifx==1:return1else:return0print("个体域D=",domain)print("各个体P(x)真值：")forxindomain:print(f"P({x})={P(x)}")print("-"*40)#3.构造两类基础一元谓词公式#公式1：全称谓词公式∀xP(x)all_true=Trueforxindomain:ifP(x)==0:all_true=Falsebreak#公式2：存在谓词公式∃xP(x)exist_true=Falseforxindomain:ifP(x)==1:exist_true=Truebreak#4.公式类型判定函数defjudge_type(is_all_true,is_exist_true):ifis_all_true:return"永真式"elifnotis_exist_true:return"永假式"else:return"可满足式"#判定并输出结果res1=judge_type(all_true,exist_true)print(f"谓词公式∀xP(x)判定结果：{res1}")print(f"公式真值：{1ifall_trueelse0}")#重置判定，单独判定∃xP(x)res2=judge_type(False,exist_true)print(f"谓词公式∃xP(x)判定结果：{res2}")print(f"公式真值：{1ifexist_trueelse0}")if__name__=="__main__":predicate_judge()(3)测试算例个体域D=[1,2]各个体P(x)真值：P(1)=1P(2)=0谓词公式∀xP(x)判定结果：可满足式公式真值：0谓词公式∃xP(x)判定结果：可满足式公式真值：12．给定有限个体域上的二元命题函数，判断由组成的谓词公式是永真式、永假式还是可满足式。（1）程序代码defbinary_predicate_judge():#定义有限个体域domain=[1,2]#自定义二元谓词函数P(x,y)，可自行修改规则defP(x,y):#示例规则：x<=y为真，否则为假return1ifx<=yelse0#输出所有(x,y)组合的谓词真值print("个体域D=",domain)print("所有(x,y)组合P(x,y)真值：")forxindomain:foryindomain:print(f"P({x},{y})={P(x,y)}")print("-"*50)#1.判定∀x∀yP(x,y)all_all=Trueforxindomain:foryindomain:ifP(x,y)==0:all_all=Falsebreakifnotall_all:break#2.判定∃x∃yP(x,y)exist_exist=Falseforxindomain:foryindomain:ifP(x,y)==1:exist_exist=Truebreakifexist_exist:break#3.判定∀x∃yP(x,y)all_exist=Trueforxindomain:flag=Falseforyindomain:ifP(x,y)==1:flag=Truebreakifnotflag:all_exist=Falsebreak#4.判定∃x∀yP(x,y)exist_all=Falseforxindomain:flag=Trueforyindomain:ifP(x,y)==0:flag=Falsebreakifflag:exist_all=Truebreak#通用判定函数：区分永真式、永假式、可满足式defget_type(is_always_true,has_true):ifis_always_true:return"永真式"elifnothas_true:return"永假式"else:return"可满足式"#逐个判定输出print(f"1.∀x∀yP(x,y)：{get_type(all_all,all_all)}")print(f"2.∃x∃yP(x,y)：{get_type(exist_exist,exist_exist)}")print(f"3.∀x∃yP(x,y)：{get_type(all_exist,exist_exist)}")print(f"4.∃x∀yP(x,y)：{get_type(exist_all,exist_exist)}")if__name__=="__main__":binary_predicate_judge()（2）测试算例个体域D=[1,2]所有(x,y)组合P(x,y)真值：P(1,1)=1P(1,2)=1P(2,1)=0P(2,2)=11.∀x∀yP(x,y)：可满足式2.∃x∃yP(x,y)：永真式3.∀x∃yP(x,y)：永真式4.∃x∀yP(x,y)：可满足式程序通用性高，可自由修改个体域、自定义任意二元谓词P(x,y)逻辑规则，自动判别四类核心二重量词谓词公式的逻辑性质，完全符合有限个体域二元谓词逻辑判定规则3．给定有限个体域上的一元命题函数、，判断由和组成的谓词公式是永真式、永假式还是可满足式。（1）程序代码defjudge_pq_formula_type():#定义有限个体域domain=[1,2]#一元谓词P(x)：仅与x相关，x为偶数为真defP(x):return1ifx%2==0else0#一元谓词Q(y)：仅与y相关，y大于1为真defQ(y):return1ify>1else0#输出所有原子真值组合print("个体域D=",domain)print("(x,y)真值对照表：")print("x\ty\tP(x)\tQ(y)")print("-"*25)forxindomain:foryindomain:print(f"{x}\t{y}\t{P(x)}\t{Q(y)}")print("-"*60)#通用判定函数：区分永真、永假、可满足defget_type(all_true,all_false):ifall_true:return"永真式"elifall_false:return"永假式"else:return"可满足式"#公式1：永真式∀x∀y(¬P(x)∨P(x)∨Q(y))all_true1=Trueall_false1=Trueforxindomain:foryindomain:res=(notP(x))orP(x)orQ(y)ifres==0:all_true1=Falseifres==1:all_false1=Falseres_type1=get_type(all_true1,all_false1)#公式2：可满足式∀x∃y(P(x)∨Q(y))#计算整体真值情况all_true2=Trueall_false2=True#先判断整体公式每一次赋值结果formula_all_res=[]forxindomain:flag=Falseforyindomain:ifP(x)orQ(y):flag=Truebreakformula_all_res.append(flag)#判定是否全真、全假ifall(formula_all_res):all_true2=Trueelse:all_true2=Falseifany(formula_all_res):all_false2=Falseelse:all_false2=Trueres_type2=get_type(all_true2,all_false2)#公式3：永假式∃x∃y(P(x)∧¬P(x)∧Q(y))all_true3=Trueall_false3=Trueforxindomain:foryindomain:res=P(x)and(notP(x))andQ(y)ifres==0:all_true3=Falseifres==1:all_false3=Falseres_type3=get_type(all_true3,all_false3)#输出最终判定结果print("公式1：∀x∀y(¬P(x)∨P(x)∨Q(y))→",res_type1)print("公式2：∀x∃y(P(x)∨Q(y))→",res_type2)print("公式3：∃x∃y(P(x)∧¬P(x)∧Q(y))→",res_type3)if__name__=="__main__":judge_pq_formula_type()（2）测试算例个体域D=[1,2](x,y)真值对照表：xyP(x)Q(y)1100120121102211公式1：∀x∀y(¬P(x)∨P(x)∨Q(y))→永真式公式2：∀x∃y(P(x)∨Q(y))→可满足式公式3：∃x∃y(P(x)∧¬P(x)∧Q(y))→永假式4．（1）程序代码defpredicate_equivalence_test():#定义有限个体域domain=[1,2,3]#自定义一元谓词P(x)：奇数为真，偶数为假defP(x):return1ifx%2==1else0print("个体域D=",domain)print("各原子谓词真值：")forxindomain:print(f"P({x})={P(x)}")print("-"*50)#==========第一组：等价公式对∀x¬P(x)与¬∃xP(x)==========defformula_A():#∀x¬P(x)res=1forxindomain:ifnot(1-P(x)):res=0breakreturnresdefformula_B():#¬∃xP(x)has_true=0forxindomain:ifP(x)==1:has_true=1breakreturn1-has_true#==========第二组：不等价公式对∀xP(x)与∃xP(x)==========defformula_C():#∀xP(x)res=1forxindomain:ifP(x)==0:res=0breakreturnresdefformula_D():#∃xP(x)res=0forxindomain:ifP(x)==1:res=1breakreturnres#判定第一组公式val_A,val_B=formula_A(),formula_B()print("【第一组：∀x¬P(x)与¬∃xP(x)】")print(f"公式A真值：{val_A}公式B真值：{val_B}")print("判定结果：【逻辑等价】"ifval_A==val_Belse"判定结果：【逻辑不等价】")#判定第二组公式val_C,val_D=formula_C(),formula_D()print("\n【第二组：∀xP(x)与∃xP(x)】")print(f"公式C真值：{val_C}公式D真值：{val_D}")print("判定结果：【逻辑等价】"ifval_C==val_Delse"判定结果：【逻辑不等价】")if__name__=="__main__":predicate_equivalence_test()（2）测试算例个体域D=[1,2,3]各原子谓词真值：P(1)=1P(2)=0P(3)=1【第一组：∀x¬P(x)与¬∃xP(x)】公式A真值：0公式B真值：0判定结果：【逻辑等价】【第二组：∀xP(x)与∃xP(x)】公式C真值：0公式D真值：1判定结果：【逻辑不等价】程序实现正反案例对照测试，逻辑严谨、结果准确，可自由修改个体域、谓词规则和自定义谓词公式，能够通用判定任意两个单变元谓词公式的等价性。5．给定有限个体域上的二元命题函数，测试两个由组成的谓词公式是否等价。（1）程序代码defbinary_predicate_equivalence():#定义有限个体域domain=[1,2]#自定义二元谓词P(x,y)：x<y为真，其余为假defP(x,y):return1ifx<yelse0#打印所有二元组合的原子真值print("个体域D=",domain)print("所有(x,y)组合P(x,y)真值：")print("x\ty\tP(x,y)")print("-"*20)forxindomain:foryindomain:print(f"{x}\t{y}\t{P(x,y)}")print("-"*50)#=================第一组：等价公式=================#公式A:∀x∀yP(x,y)defformula_A():res=1forxindomain:foryindomain:ifP(x,y)==0:res=0breakifres==0:breakreturnres#公式B:∀y∀xP(x,y)defformula_B():res=1foryindomain:forxindomain:ifP(x,y)==0:res=0breakifres==0:breakreturnres#=================第二组：不等价公式=================#公式C:∀x∃yP(x,y)defformula_C():flag_all=Trueforxindomain:has_true=Falseforyindomain:ifP(x,y)==1:has_true=Truebreakifnothas_true:flag_all=Falsebreakreturn1ifflag_allelse0#公式D:∃y∀xP(x,y)defformula_D():has_all_true=Falseforyindomain:all_true=Trueforxindomain:ifP(x,y)==0:all_true=Falsebreakifall_true:has_all_true=Truebreakreturn1ifhas_all_trueelse0#等价性判定val_A,val_B=formula_A(),formula_B()print("【第一组：∀x∀yP(x,y)与∀y∀xP(x,y)】")print(f"公式A真值：{val_A}公式B真值：{val_B}")print("判定结果：【逻辑等价】"ifval_A==val_Belse"判定结果：【逻辑不等价】")val_C,val_D=formula_C(),formula_D()print("\n【第二组：∀x∃yP(x,y)与∃y∀xP(x,y)】")print(f"公式C真值：{val_C}公式D真值：{val_D}")print("判定结果：【逻辑等价】"ifval_C==val_Delse"判定结果：【逻辑不等价】")if__name__=="__main__":binary_predicate_equivalence()（2）测试算例个体域D=[1,2]所有(x,y)组合P(x,y)真值：xyP(x,y)110121210220【第一组：∀x∀yP(x,y)与∀y∀xP(x,y)】公式A真值：0公式B真值：0判定结果：【逻辑等价】【第二组：∀x∃yP(x,y)与∃y∀xP(x,y)】公式C真值：1公式D真值：0判定结果：【逻辑不等价】本程序为通用二元谓词等价判定模板，可自由修改个体域、二元谓词规则与待测公式，精准判定任意两个二元谓词公式的逻辑等价性。6．给定有限个体域上的一元命题函数、，测试两个由和组成的谓词公式是否等价。(1)程序代码defpq_predicate_equivalence_test():#定义有限个体域domain=[1,2]#定义一元谓词P(x)：仅与x有关，x为偶数为真defP(x):return1ifx%2==0else0#定义一元谓词Q(y)：仅与y有关，y大于1为真defQ(y):return1ify>1else0#打印所有赋值组合的原子谓词真值print("个体域D=",domain)print("所有(x,y)组合真值对照表：")print("x\ty\tP(x)\tQ(y)")print("-"*25)forxindomain:foryindomain:print(f"{x}\t{y}\t{P(x)}\t{Q(y)}")print("-"*60)#==========第一组：逻辑等价公式==========#公式A:∀x∃y(P(x)∨Q(y))defformula_A():forxindomain:flag=Falseforyindomain:ifP(x)orQ(y):flag=Truebreakifnotflag:return0return1#公式B:∃y∀x(P(x)∨Q(y))defformula_B():foryindomain:flag=Trueforxindomain:ifnot(P(x)orQ(y)):flag=Falsebreakifflag:return1return0#==========第二组：逻辑不等价公式==========#公式C:∀x∃y(P(x)∧Q(y))defformula_C():forxindomain:flag=Falseforyindomain:ifP(x)andQ(y):flag=Truebreakifnotflag:return0return1#公式D:∃y∀x(P(x)∧Q(y))defformula_D():foryindomain:flag=Trueforxindomain:ifnot(P(x)andQ(y)):flag=Falsebreakifflag:return1return0#等价性判定与结果输出val_A,val_B=formula_A(),formula_B()print("【第一组：∀x∃y(P(x)∨Q(y))与∃y∀x(P(x)∨Q(y))】")print(f"公式A真值：{val_A}公式B真值：{val_B}")print("判定结果：【逻辑等价】"ifval_A==val_Belse"判定结果：【逻辑不等价】")val_C,val_D=formula_C(),formula_D()print("\n【第二组：∀x∃y(P(x)∧Q(y))与∃y∀x(P(x)∧Q(y))】")print(f"公式C真值：{val_C}公式D真值：{val_D}")print("判定结果：【逻辑等价】"ifval_C==val_Delse"判定结果：【逻辑不等价】")if__name__=="__main__":pq_predicate_equivalence_test()（2）测试算例个体域D=[1,2]所有(x,y)组合真值对照表：xyP(x)Q(y)1100120121102211【第一组：∀x∃y(P(x)∨Q(y))与∃y∀x(P(x)∨Q(y))】公式A真值：1公式B真值：1判定结果：【逻辑等价】【第二组：∀x∃y(P(x)∧Q(y))与∃y∀x(P(x)∧Q(y))】公式C真值：1公式D真值：0判定结果：【逻辑不等价】程序通用性极强，可自由修改个体域范围、P(x)、Q(y)谓词规则，支持自定义任意由两个独立一元谓词组成的谓词公式，精准判定逻辑等价性。7．给定有限个体域上的一元命题函数，测试由组成的一个谓词公式是否是另一个由组成的谓词公式的逻辑结论。（1）程序代码"""功能：有限个体域下一元谓词公式逻辑结论判定核心特性：支持用户【自定义任意前提公式、结论公式】，一键判定逻辑结论关系判定标准：无「前提真、结论假」反例=逻辑结论成立"""#======================用户自定义区（可直接修改）======================#1.自定义有限个体域domain=[1,2,3]#2.自定义一元谓词P(x)defP(x):#可自由修改：奇偶判断、大小判断、取模运算等return1ifx%2==1else0#3.【核心自定义】修改此处即可测试任意两个谓词公式defpremise_formula():#自定义前提公式A，默认：∃xP(x)forxindomain:ifP(x)==1:return1return0defconclusion_formula():#自定义结论公式B，默认：∀xP(x)forxindomain:ifP(x)==0:return0return1#======================固定核心算法（无需修改）======================defformula_all_P():#通用公式：∀xP(x)forxindomain:ifP(x)==0:return0return1defformula_exist_P():#通用公式：∃xP(x)forxindomain:ifP(x)==1:return1return0defcheck_conclusion(premise_func,conclusion_func):"""通用判定函数：检测是否存在前真后假反例"""pre_val=premise_func()con_val=conclusion_func()counter_example=[]ifpre_val==1andcon_val==0:counter_example.append(f"前提真值:{pre_val}，结论真值:{con_val}")ifcounter_example:returnFalse,f"存在反例：{counter_example}"else:returnTrue,"无任何反例，结论成立"#主程序if__name__=="__main__":#输出真值表print("=====个体域与P(x)真值表=====")print("x\tP(x)")foritemindomain:print(f"{item}\t{P(item)}")#经典案例1print("\n=====案例1：∀xP(x)⇒∃xP(x)=====")res1,msg1=check_conclusion(formula_all_P,formula_exist_P)print("判定结果：",msg1)#经典案例2print("\n=====案例2：∃xP(x)⇒∀xP(x)=====")res2,msg2=check_conclusion(formula_exist_P,formula_all_P)print("判定结果：",msg2)#用户自定义案例print("\n=====自定义公式测试结果=====")res3,msg3=check_conclusion(premise_formula,conclusion_formula)print("判定结果：",msg3)（2）测试算例=====个体域与P(x)真值表=====xP(x)112031=====案例1：∀xP(x)⇒∃xP(x)=====判定结果：无任何反例，结论成立=====案例2：∃xP(x)⇒∀xP(x)=====判定结果：存在反例：['前提真值:1，结论真值:0']=====自定义公式测试结果=====判定结果：存在反例：['前提真值:1，结论真值:0']可直接修改domain变量自定义任意有限个体域；可修改P(x)函数自定义任意一元谓词规则，同时仅需修改`premise_formula()`（前提公式）和`conclusion_formula()`（结论公式），即可测试任意由P(x)、全称量词、存在量词组成的谓词公式，无需改动核心算法。8．给定有限个体域上的二元命题函数，测试由组成的一个谓词公式是否是另一个由组成的谓词公式的逻辑结论。（1）程序代码"""功能：有限个体域下二元谓词P(x,y)公式逻辑结论判定核心功能：测试二元谓词公式B是否为公式A的逻辑结论判定标准：无「前提A真、结论B假」反例，则B是A的逻辑结论适配：可自定义个体域、二元谓词、任意二元量词公式"""#======================用户自定义区（可直接修改）======================#1.自定义有限个体域domain=[1,2]#2.自定义二元命题函数P(x,y)，可自由修改规则defP(x,y):#示例规则：x<y时为真(1)，否则为假(0)return1ifx<yelse0#3.【核心自定义】自定义任意前提公式A、结论公式Bdefpremise_formula():#用户自定义前提公式（默认：∃x∃yP(x,y)）forxindomain:foryindomain:ifP(x,y)==1:return1return0defconclusion_formula():#用户自定义结论公式（默认：∀x∀yP(x,y)）forxindomain:foryindomain:ifP(x,y)==0:return0return1#======================固定核心算法（无需修改）======================#通用二元公式1：∀x∀yP(x,y)defformula_all_all_P():forxindomain:foryindomain:ifP(x,y)==0:return0return1#通用二元公式2：∃x∃yP(x,y)defformula_exist_exist_P():forxindomain:foryindomain:ifP(x,y)==1:return1return0#通用逻辑结论判定函数defcheck_conclusion(premise_func,conclusion_func):pre_val=premise_func()con_val=conclusion_func()counter_example=[]#唯一反例：前提为真，结论为假ifpre_val==1andcon_val==0:counter_example.append(f"前提真值:{pre_val}，结论真值:{con_val}")ifcounter_example:returnFalse,f"存在反例：{counter_example}"else:returnTrue,"无任何反例，结论成立"#主程序执行if__name__=="__main__":#输出二元谓词真值表print("=====个体域与二元谓词P(x,y)真值表=====")print("x\ty\tP(x,y)")forxindomain:foryindomain:print(f"{x}\t{y}\t{P(x,y)}")#经典案例1：全称推出存在print("\n=====案例1：∀x∀yP(x,y)⇒∃x∃yP(x,y)=====")res1,msg1=check_conclusion(formula_all_all_P,formula_exist_exist_P)print("判定结果：",msg1)#经典案例2：存在推不出全称print("\n=====案例2：∃x∃yP(x,y)⇒∀x∀yP(x,y)=====")res2,msg2=check_conclusion(formula_exist_exist_P,formula_all_all_P)print("判定结果：",msg2)#用户自定义二元公式测试print("\n=====自定义二元公式测试结果=====")res3,msg3=check_conclusion(premise_formula,conclusion_formula)print("判定结果：",msg3)（2）测试算例=====个体域与二元谓词P(x,y)真值表=====xyP(x,y)110121210220=====案例1：∀x∀yP(x,y)⇒∃x∃yP(x,y)=====判定结果：无任何反例，结论成立=====案例2：∃x∃yP(x,y)⇒∀x∀yP(x,y)=====判定结果：存在反例：['前提真值:1，结论真值:0']=====自定义二元公式测试结果=====判定结果：存在反例：['前提真值:1，结论真值:0']9．给定有限个体域上的一元命题函数、，测试由和组成的一个谓词公式是否是另一个由和组成的谓词公式的逻辑结论。（1）程序代码"""有限个体域P(x)、Q(y)谓词公式逻辑结论判定功能：判断公式B是否为公式A的逻辑结论"""#=====================1.自定义配置区=====================#有限个体域domain=[1,2]#一元谓词P(x)：x为偶数时为真defP(x):return1ifx%2==0else0#一元谓词Q(y)：y大于1时为真defQ(y):return1ify>1else0#=================