扩展规则方法研究综述  

Extension rule: a survey

作　　者：王金艳[1] 谷文祥[2,3] 覃少华[1] 殷明浩[3] 

机构地区：[1]广西师范大学计算机科学与信息工程学院,广西桂林541004 [2]长春建筑学院基础教学部,吉林长春130607 [3]东北师范大学计算机科学与信息技术学院,吉林长春130117

出　　处：《智能系统学报》2014年第1期1-11,共11页CAAI Transactions on Intelligent Systems

基　　金：国家自然科学基金资助项目(61070084;61272535;61163065;61370156;61165009);国家"973"计划资助项目(2012CB326403);广西自然科学基金资助项目(2013GXNSFBA019263;2012GXNSFAA053219);广西高校科研项目(2013YB029);"八桂学者"工程专项经费资助项目;广西师范大学博士启动基金资助项目

摘　　要：归结方法是自动推理的重要方法之一,而扩展规则是与归结对称的方法,近年来引起了研究者的广泛关注。从扩展规则的相关概念、在命题逻辑中的发展以及在一阶逻辑、描述逻辑、模态逻辑、可能性逻辑和多值逻辑中的应用3个方面论述分析了扩展规则10年来的研究现状,重点阐述扩展规则用于求解SAT、相近SAT和#SAT问题各种算法的优缺点,最后指出相关的研究热点与发展趋势。The method based on the resolution principle has always been one of the important methods for automated reasoning .The theorem proving method using the extension rule is complementary to the method based on the reso-lution principle .In recent years , the method has received wide attention and has achieved great progress .This pa-per surveys the development of the theorem proving using the extension rule for ten years from three aspects ：the re-lated concepts of the extension rule , the development of the propositional logic , and the applications for first-order logic, description logic, modal logic, possibility logic and multivalue logic , in which the merits and demerits of these algorithms for solving SAT , analogous SAT and #SAT using the extension rule are mainly analyzed .Finally , the related research hotspots and developing trends are pointed out .

关 键 词：自动推理 归结方法 扩展规则 SAT #SAT 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]