导　　师： 王能超;徐正权

学科专业： H1202

授予学位： 博士

作　　者： ;

机构地区： 华中科技大学

摘　　要： 自动推理是一门在给定知识及有关推理策略的前提下,研究用计算机帮助人们进行推理的学科.多种类逻辑及多种类谓词演算是经典一阶逻辑及其演算的重要拓展,并已经在计算机科学的诸多领域得到了广泛运用,如知识表示、程序设计语言、软件规约与验证等.与基于归结原理的经典谓词演算相比,多种类谓词演算具有更高的演绎效率.为进一步提高演绎效率与简化计算机程序设计结构,提出了一种基于归结原理的多种类谓词演算的演绎策略,即rld(rightmost linear deduction)演绎,并证明了它的完备性.实现了基于rld演绎的多种类谓词演算的一个原型系统并成功求解了著名的人工智能问题,即steamroller问题.为了在模糊逻辑中集成相似性关系并考虑其近似推理,把相似性关系看成是一种模糊相等关系,提出了一种带有相似性关系的模糊逻辑,给出了带有相似性关系的模糊逻辑的语法及语义结构.调解规则是在带有相等关系的经典谓词演算中提出的推理规则,它能够进行高效的等值推理.将调解规则拓展到了带有相似性关系的模糊逻辑谓词演算,讨论了基于归结与调解规则的近似推理.给出并证明了基于归结与调解方法的近似推理的有关属性,证明了如果子句集s中的每一个子句的真值都大于0.5,那么从s中使用归结与(或)调解规则推出的任意一个逻辑结果均是有效的.考虑到许多自动推理和问题解决系统均是基于否证法,证明了基于归结与调解规则对模糊谓词演算的完备性定理.自动推理系统的性能测试与评价是自动推理领域备受关注的问题.为进行公正的系统评价,需要一系列的评价标准以便测试者做出合理、准确、公正的评价结论.其中,问题的表示是其中主要原则之一.为了给自动推理领域提供一个统一的问题表示格式,提出了一个基于多种类逻辑的知识标记语言mskml(many-sorted knowledgemarkup language).使自动推理成为一种web服务,既可以为web用户提供自动推理服务,也可以使web用户参与自动推理系统的测试工作,从而获得更丰富的实验数据以便做出更为公正合理的系统评价.为了给web用户提供自动推理web服务,构造了一个自动推理系统prover,prover实现了基于rld演绎的多种类谓词演算,采用简单对象访问协议soap(simple object access protocol)作为服务器与web用户间的网络通信协议,并用web服务描述语言wsdl(web service description language)对系统提供的web服务加以描述.

关 键 词： 人工智能 自动推理 谓词演算 模糊逻辑 归结原理 知识标记 万维网服务

分 类 号： [TP181 TP311.1]

领　　域： [自动化与计算机技术] [自动化与计算机技术] [自动化与计算机技术] [自动化与计算机技术]