实验三 归结原理.doc

《实验三 归结原理.doc》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、《人工智能》实验大作业实验题目：归结原理专业信息与计算科学年级姓名马昊学号指导老师时华日期2012-12-5实验三归结原理一、实验目的在本实验中，主要熟悉和掌握归结原理的基本思想和基本方法，通过实验培养了我们利用逻辑方法表示知识，并掌握采用机器推理来进行问题求解的基本方法。二、实验要求1.熟悉归结原理的基本思想和归结否证的步骤；2.本实验JAVA语言编程实现实验内容；3.利用所学的知识及实验结果，来完成实验报告的各项内容。三、实验背景知识归结原理是一种推理规则。从谓词公式转化为子句集的过程中看出，在子句集中子句之间是合取关系，其中只要有一个子句不可满足，则子句集就不可满

2、足。若一个子句集中包含空子句，则这个子句集一定是不可满足的。归结原理就是基于这一认识提出来的。他的原理就是：P->Q,Q->R则P->R由于P->Q就是￢P∨Q　　而Q->R就是￢Q∨R所以，他相当于将Q和￢Q合并。也就是说，　　P∨{∑1}与~P∨{∑2}可以归结为{∑1}∨{∑2}其中∑1,∑2是文字的集合归结否证包含以下步骤：（1）把前提或公理转换成子句形式；（2）把求证目标的否定的子句形式加到公理集合中；（3）对所有这些子句进行归结，产生它们的逻辑结果子句；（1）用产生空子句的方法来得出矛盾；（2）否定目标的否证在用于产生空子句的代换下为真。如何把前提或公理化为

3、子句形式是进行归结的前提，其过程包含如下步骤：（1）消去蕴涵符号用～P∨Q替换P→Q（2）减少否定符号的辖域每个否定符号～最多只作用在一个谓词符号上（3）对变量标准化每个变量仅受一个量词作用（4）消去存在量词若存在量词前没有全称量词，则直接消去；否则，要Skolem。化。（5）化为前束范式前束范式：一个公式，如果量词均非否定地出现在公式最前面，其辖域延伸到整个公式的末尾，且在公式中仅含有联结词～，∨，∧，则称此种形式为前束范式。前束范式=（前缀）（母式）（6）化母式为合取范式（7）消去全称量词（8）消去连接词符号∧用{A，B}替代（A∧B）（9）将分离的变元归一化四、实

4、验内容1.问题描述：四对夫妇中，王结婚时，周送了礼；周和钱是同一排球队的队员；李的爱人是陈的爱人的表哥；陈夫妇与邻居吵架时，徐、周、吴的爱人都去助战；李、徐、周结婚前住在同一宿舍，试用归结原理求王、周、钱、陈、李、徐、吴、孙几人谁和谁是夫妇。2.实验源代码：importjava.lang.*;publicclassGuessCouple2{/**数据类型*/publicclassPerson{privateStringname;privatebooleansex;privatePersonspouse;publicPerson(Stringname){this.name

5、=name;this.sex=false;this.spouse=null;}publicPerson(){name=null;sex=false;spouse=null;}publicPerson(Stringname,booleansex,Personspouse){this.name=name;this.sex=sex;this.spouse=spouse;}publicvoidsetName(Stringname){this.name=name;}publicStringgetName(){returnname;}publicvoidsetSex(boolean

6、sex){this.sex=sex;}publicbooleangetSex(){returnsex;}publicvoidsetSpouse(Personperson1){this.spouse=person1;}publicPersongetSpouse(){returnspouse;}}Person[]sortBySpouse1=newPerson[8];Person[]sortBySpouse2=newPerson[8];intx=0,y=0;Person[]sortByEqualSex1=newPerson[8];Person[]sortByEqualSex2

7、=newPerson[8];intn=0,p=0,f=0;Person[]woman=newPerson[4];Person[]man=newPerson[4];intk=0,s=0,r=0;booleansign=true;booleansign1=true;booleansign2=true;booleansign3=true;booleansign4=true;booleansign5=true;booleansign6=true;booleansign7=true;Person[]couple1=newPerson[4];Pers