搜索
智能科学与技术系人工智能课程改革与建设第五讲经典人工智能技术——推理与搜索TraditionalTechnologyofAI中南大学刘丽珏2011智能科学与技术系本讲授课要点讲授基于符号主义的经典人工智能技术。符号主义的研究以知识为核心。知识的表示是问题求解的基础，但单纯介绍知识表示容易让学生感觉枯燥，且无法直观理解其作用，可考虑将表示与求解放在一起讲授，例如：谓词逻辑表示与推理技术状态空间表示与搜索技术宜用问题带出内容，通过问题引发学生思考：“这样的问题机器能解决吗？可以怎么做？”以增加兴趣。智能科学与技术系引言——经典人工智能出色的老式人工智能（GoodOldFashionedAI，GOFAI）——哲学家约翰.豪格兰德一个用规则和事实来程序化的高速数字计算机可能表现出智力行为——图灵人类是借助事实与规则来产生智力行为的经典人工智能技术主要以符号表示、符号处理为实现智能的主要手段，推理和搜索是其中的核心技术智能科学与技术系5.1自动推理证明机器真的能够自动推理吗？自动推理证明的发展史谓词逻辑消解原理智能科学与技术系5.1.1机器真的能够自动推理吗？5个房间问题有5间不同颜色的房间，每间住个不同国籍的人，每人有自己喜欢的饮料、香烟和宠物。已知信息：1.英国人在红房间中2.西班牙人有一条狗3.挪威人住在左边第一间房里4.黄房间中的人在抽库尔斯牌香烟5.抽切斯菲尔德牌香烟的人是养了一只狐狸的人的邻居6.挪威人住在蓝房间隔壁7.抽温斯顿牌香烟的人有一只蜗牛8.抽幸运牌香烟的人喝橘子汁9.乌克兰人喝茶10.日本人抽国会牌香烟11.抽库尔斯牌烟的房间在有匹马的房间隔壁12.绿房间中的人喝咖啡13.绿房间在白房间的左边14.中间房间的人喝牛奶问题：斑马在哪个房间中？哪个房间中的人喝水？智能科学与技术系自动推理示例：5个房间问题房间号12345颜色国籍香烟饮料宠物挪威人牛奶咖啡库尔斯马英国人水橘子汁西班牙幸运狗茶乌克兰日本人国会温斯顿切斯菲尔德蜗牛狐狸斑马3.挪威人住在左边第一间房里6.挪威人住在蓝房间旁边14.中间房间的人喝牛奶12.绿房间中的人喝咖啡14.绿房间在白房间的左边1.英国人在红房间中4.黄房间中的人在抽库尔斯牌香烟11.抽库尔斯牌烟的房间在有匹马的房间隔壁8.抽幸运香烟的人喝橘子汁9.乌克兰人喝茶2.西班牙人有一条狗8.抽幸运牌香烟的人喝橘子汁9.乌克兰人喝茶10.日本人抽国会牌香烟7.抽温斯顿牌香烟的人有一只蜗牛5.抽切斯菲尔德牌香烟的人的是养了一只狐狸的人的邻居机器真的能自动完成这样的推理吗？智能科学与技术系自动推理示例domainsID=symbolHOUSE=h(ID,NO)HLIST=referenceHOUSE*NO=integerNOLIST=NO*CHARLIST=CHAR*CHARLISTS=CHARLIST*predicatesnondetermsolvenondetermcandidate(HLIST,HLIST,HLIST,HLIST,HLIST)nondetermperm(HLIST)nondetermconstraints(HLIST,HLIST,HLIST,HLIST,HLIST)nondetermpermutation(NOLIST,NOLIST)nondetermdelete(NO,NOLIST,NOLIST)member(HOUSE,HLIST)nondetermnext(NO,NO)nondetermlleft(NO,NO)clausessolve():-constraints(Colours,Drinks,Nationalities,Cigarettes,Pets),candidate(Colours,Drinks,Nationalities,Cigarettes,Pets),member(h(water,WaterHouse),Drinks),member(h(WaterColour,WaterHouse),Colours),member(h(zebra,ZebraHouse),Pets),member(h(ZebraColour,ZebraHouse),Colours),write(Theydrinkwaterinthe,WaterColour,house\n),write(Thezebraliveinthe,ZebraColour,house\n).candidate(L1,L2,L3,L4,L5):-perm(L1),perm(L2),perm(L3),perm(L4),perm(L5).perm([h(_,A),h(_,B),h(_,C),h(_,D),h(_,E)]):-permutation([A,B,C,D,E],[1,2,3,4,5]).constraints(Colours,Drinks,Nationalities,Cigarettes,Pets):-member(h(englishman,H1),Nationalities),member(h(red,H1),Colours),member(h(spaniard,H2),Nationalities),member(h(dog,H2),Pets),member(h(norwegian,1),Nationalities),member(h(kools,H3),Cigarettes),member(h(yellow,H3),Colours),member(h(chesterfields,H4),Cigarettes),next(H4,H5),member(h(fox,H5),Pets),member(h(norwegian,H6),Nationalities),next(H6,H7),member(h(blue,H7),Colours),member(h(winston,H8),Cigarettes),member(h(snails,H8),Pets),member(h(lucky_strike,H9),Cigarettes),member(h(orange_juice,H9),Drinks),member(h(ukrainian,H10),Nationalities),member(h(tea,H10),Drinks),member(h(japanese,H11),Nationalities),member(h(parliaments,H11),Cigarettes),member(h(kools,H12),Cigarettes),next(H12,H13),member(h(horse,H13),Pets),member(h(coffee,H14),Drinks),member(h(green,H14),Colours),member(h(green,H15),Colours),lleft(H16,H15),member(h(ivory,H16),Colours),member(h(milk,3),Drinks).permutation([],[]).permutation([A|X],Y):-delete(A,Y,Y1),permutation(X,Y1).delete(A,[A|X],X).delete(A,[B|X],[B|Y]):-delete(A,X,Y).member(A,[A|_]):-!.member(A,[_|X]):-member(A,X).next(X,Y):-lleft(X,Y).next(X,Y):-lleft(Y,X).lleft(1,2).lleft(2,3).lleft(3,4).lleft(4,5).goalsolve.求解智能科学与技术系5.1.2自动推理证明的发展史笛卡尔莱布尼茨自动证明的提出笛卡尔、莱布尼茨（17世纪）萌发了用机械系统实现定理证明的想法把一类数学问题当作一个整体，建立统一的证明过程，按照规定的程序步骤机械地进行下去，在有限步骤之后判断出定理的正确性智能科学与技术系自动证明的发展由于传统的兴趣和应用的价值，初等几何问题的自动求解成为数学机械化的研究焦点。希尔伯特希尔伯特20世纪初，在他的名著《几何基础》中给出了一条可以对一类几何命题进行判定的定理。希尔伯特对命题的要求太高，当时仅能解决很少的一类几何定理的机器证明，却是历史上第一个关于某类几何命题的机械化检验方法的定理。智能科学与技术系自动证明的发展塔斯基塔斯基（波兰）1950年，证明了：“一切初等几何和初等代数范围的命题都可以用机械方法判定”为几何定理的机器证明开拓了一条利用代数方法的途径方法太复杂，即使用高速计算机也证明不了稍难的几何定理智能科学与技术系自动证明的发展艾伦.纽厄尔纽厄尔,西蒙和肖1956年,发表了论文《逻辑理论机》(LTM)认为LTM不仅是计算机智力的有力证明，也是人类认知本质的证明1957年开发了最早的AI程序设计语言IPL语言1960年，成功地合作开发了“通用问题求解系统”GPS(GeneralProblemSolver)赫伯特.西蒙智能科学与技术系自动证明的发展—王浩王浩美籍华裔王浩（1921—1995）数学家、逻辑学家、计算机科学家、哲学家。简历生于山东济南市1943年毕业于西南联合大学数学系1945年毕业于清华大学研究生院哲学系1948年获哈佛大学哲学博士学位1954-1956年在牛津大学任高级教职1961-1967年任哈佛大学教授1967-1991年任洛克菲勒大学逻辑学教授20世纪50年代初当选美国科学院院士及不列颠科学院外籍院士。智能科学与技术系自动证明的发展—王浩王浩美籍华裔王浩（1921—1995）l953年起开始计算机理论与机器证明的研究。他敏锐地感觉到被认为过分讲究形式的精确又十分繁琐而无任何实际用处的数理逻辑，可以在计算机领域发挥极好的作用。1959年，采用“王浩算法”用计算机证明了罗素、怀海德的巨著《数学原理》中的几百条有关命题逻辑的定理，仅用了9分钟（vs10年），宣告了用计算机进行定理证明的可能性，第一次明确提出“走向数学的机械化”。智能科学与技术系自动证明的发展—王浩美籍华裔王浩1983年，获国际人工智能联合会“数学定理机械证明里程碑奖”，表彰他在数学定理机械证明研究领域的开创性贡献。1972年以后，王浩数次回国讲学。1985年兼任北京大学教授；1986年兼任清华大学教授。新中国成立之初，公开发表演说表示对新中国的支持。1972年回国时曾受周恩来总理的接见。1973年撰写了《访问中国的沉思》，赞美新中国，被报纸与杂志广泛刊载。为此，他受到了许多攻击。他热爱祖国和中华民族的精神值得人们学习与称道。智能科学与技术系自动证明的发展1977年，美国年轻的数学家阿佩尔等在高速电子计算机上耗费1200小时的计算时间，证明了著名的“四色定理”，人类百年悬而未决的疑问最终被圆满解决了。这一成就轰动一时，成为机器定理证明的一个典范。智能科学与技术系属于中国的自动证明方法—吴方法著名数学家吴文俊中国科学院数学与系统科学研究院研究员、中国科学院院士、第三世界科学院院士1919年出生于上海1940年毕业于交通大学数学系1949年获法国国家博士学位1951年回到祖国，任北京大学数学系的教授1956年与华罗庚、钱学森同台领取国家自然科学奖一等奖；38岁时当选为中国科学院学部委员1993年获得陈嘉庚数理科学奖1994年获首届求是科技基金会杰出科学家奖1997年获Herbrand自动推理杰出成就奖2001年获国家最高科学技术奖智能科学与技术系属于中国的自动证明方法—吴方法吴文俊1984年出版专著《几何定理机器证明的基本原理》，利用中国古典数学的成就，提出具有中国特色的定理自动证明方法，被国际上誉为“吴氏方法”。1985年发表论文“关于代数方程组的零点”—吴文俊消元法，即“吴氏公式”。2010年5月4日，国际小行星中心发布公报通知国际社会，将国际永久编号为第7683号的小行星永久命名为“吴文俊星”。智能科学与技术系如何实现自动推理证明？逻辑方法是自动证明中常用的方法如何进行逻辑推