[1]王金艳,谷文祥,覃少华,等.扩展规则方法研究综述[J].智能系统学报,2014,9(1):1-11.[doi:10.3969/j.issn.1673-4785.201308004]
WANG Jinyan,GU Wenxiang,QIN Shaohua,et al.Extension rule: a survey[J].CAAI Transactions on Intelligent Systems,2014,9(1):1-11.[doi:10.3969/j.issn.1673-4785.201308004]
点击复制
WANG Jinyan,GU Wenxiang,QIN Shaohua,et al.Extension rule: a survey[J].CAAI Transactions on Intelligent Systems,2014,9(1):1-11.[doi:10.3969/j.issn.1673-4785.201308004]
扩展规则方法研究综述
《智能系统学报》[ISSN 1673-4785/CN 23-1538/TP] 卷:
9
期数:
2014年第1期
页码:
1-11
栏目:
综述
出版日期:
2014-02-25
- Title:
- Extension rule: a survey
- Keywords:
- automated reasoning; resolution principle; extension rule; SAT; #SAT
- 分类号:
- TP181
- 摘要:
- 归结方法是自动推理的重要方法之一, 而扩展规则是与归结对称的方法, 近年来引起了研究者的广泛关注。从扩展规则的相关概念、在命题逻辑中的发展以及在一阶逻辑、描述逻辑、模态逻辑、可能性逻辑和多值逻辑中的应用3个方面论述分析了扩展规则10年来的研究现状, 重点阐述扩展规则用于求解SAT、相近SAT和#SAT问题各种算法的优缺点, 最后指出相关的研究热点与发展趋势。
- Abstract:
- 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 resolution principle. In recent years, the method has received wide attention and has achieved great progress. This paper surveys the development of the theorem proving using the extension rule for ten years from three aspects: the related 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.
- 参考文献/References:
-
[1] 殷明浩.自动推理和智能规划中若干问题研究[D].长春: 吉林大学, 2008: 1-109.YIN Minghao. The research on several issues of automated reasoning and artificial intelligent planning[D]. Changchun: Jilin University, 2008: 1-109.
[2] WOLFGANG R. The KIV system: systematic construction of verified software[C]//Proceedings of the 11th International Conference on Automated Deduction. Saratoga Springs, USA, 1992: 753-757.
[3] 吕帅,刘磊,石莲,等.基于自动推理技术的智能规划方法[J].软件学报, 2009, 20(5): 1226-1240.LU Shuai, LIU Lei, SHI Lian, et al. Artificial intelligence planning methods based on automated reasoning techniques[J]. Journal of Software, 2009, 20(5): 1226-1240.
[4] GRASTIEN A, ANBULAGAN A, RINTANEN J, et al. Diagnosis of discrete-event systems using satisfiability algorithms[C]//Proceedings of the Twenty-Second Conference on Artificial Intelligence. Vancouver, Canada, 2007: 305-310.
[5] ROBINSON J A. A machine oriented logic based on the resolution principle[J]. Computer Machine, 1965, 12(1): 23-41.
[6] DECHTER R, RISH I. Directional resolution: the Davis-Putnam procedure, revisited[C]//Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning. Bonn, Germany, 1994: 134-145.
[7] LIN Hai, SUN Jigui, ZHANG Yimin. Theorem proving based on the extension rule[J]. Journal of Automated Reasoning, 2003, 31(1): 11-21.
[8] DAVIS M, PUTNAM H. A computing procedure for quantification theory[J]. Journal of the ACM, 1960, 7(3): 201-215.
[9] DAVIS M, LOGEMANN G, LOVELAND D. A machine program for theorem-proving[J]. Communications of the ACM, 1962, 5(7): 394-397.
[10] 赖永,欧阳丹彤,蔡敦波,等.基于扩展规则的模型计数与智能规划方法[J].计算机研究与发展, 2009, 46(3): 459-469.LAI Yong, OUYANG Dantong, CAI Dunbo, et al. Model counting and planning using extension rule[J]. Journal of Computer Research and Development, 2009, 46(3): 459-469.
[11] SANG T, BEAME P, KAUTZ H. Solving Bayesian networks by weighted model counting[C]//Proceedings of the Twentieth National Conference on Artificial Intelligence. Pittsburgh, USA, 2005: 475-482.
[12] 谷文祥,李淑霞,殷明浩.隐蔽集的研究及发展[J].计算机科学, 2010, 37(3): 11-16.GU Wenxiang, LI Shuxia, YIN Minghao. Research and development in backdoor set[J]. Computer Science, 2010, 37(3): 11-16.
[13] NISHIMURA N, RAGDE P, SZEIDER S. Detecting backdoor sets with respect to Horn and binary clauses[C]//Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing. Vancouver, Canada, 2004: 96-103.
[14] MNASSON N, ZECCHINA R, KIRKPATRICK S. Determining computational complexity form characteristic’phase transitions’[J]. Nature, 1999, 400: 133-137.
[15] 林海.基于扩展规则的定理证明和知识编译[D].长春:吉林大学, 2003: 1-40.LIN Hai. Theorem proving and knowledge compilation based on the extension rule[D]. Changchun: Jilin University, 2003: 1-40.
[16] WU Xia, SUN Jigui, LU Shuai, et al. Improved propositional extension rule[C]//Proceedings of the First International Conference on Rough Sets and Knowledge Technology. Chongqing, China, 2006: 592-597.
[17] 吴瑕.基于扩展规则的定理证明的研究[D].长春:吉林大学, 2006: 1-132.WU Xia. The research on the extension rule based theorem proving[D]. Changchun: Jilin University, 2006: 1-132.
[18] 李莹,孙吉贵,吴瑕,等.基于IMOM和IBOHM启发式策略的扩展规则算法[J].软件学报, 2009, 20(6): 1521-1527.LI Ying, SUN Jigui, WU Xia, et al. Extension rule algorithms based on IMOM and IBOHM heuristics strategies[J]. Journal of Software, 2009, 20(6): 1521-1527.
[19] WU Xia, SUN Jigui, LU Shuai, et al. Propositional extension rule with reduction[J]. International Journal of Computer Science and Network Security, 2006, 6(1A): 190-197.
[20] 孙吉贵,李莹,朱兴军,等.一种新的基于扩展规则的定理证明算法[J].计算机研究与发展, 2009, 46(1): 9-14.SUN Jigui, LI Ying, ZHU Xingjun, et al. A novel theorem proving algorithm based on extension rule[J]. Journal of Computer Research and Development, 2009, 46(1): 9-14.
[21] 张立明,欧阳丹彤,白洪涛.基于半扩展规则的定理证明方法[J].计算机研究与发展, 2010, 49(7): 1522-1529.ZHANG Liming, OUYANG Dangtong, BAI Hongtao. Theorem proving algorithm based on semi-extension rule[J]. Journal of Computer Research and Development, 2010, 49(7): 1522-1529.
[22] ZHANG Liming, OUYANG Dantong, ZHAO Jian, et al. The parallel theorem proving algorithm based on semi-extension rule[J]. Applied Mathematics & Information Sciences, 2012, 6(1): 119-122.
[23] YIN Liangze, HE Fei, HUNG W N N, et al. Maxterm covering for satisfiability[J]. IEEE Transactions on Computers, 2012, 61(3): 420-426.
[24] XU Youjun, OUYANG Dantong, YE Yuxin, et al. Solving SAT problem with a revised hitting set algorithm[C]//Proceedings of the 2nd International Conference on Future Computer and Communication. Wuhan, China, 2010: 653-656.
[25] 许有军.基于扩展规则的若干SAT问题研究[D].长春:吉林大学, 2011: 1-91.XU Youjun. Research on several SAT issues based on extension rule[D]. Changchun: Jilin University, 2011: 1-91.
[26] LIN Hai, SUN Jigui. Knowledge compilation using the extension rule[J]. Journal of Automated Reasoning, 2004, 32(2): 93-102.
[27] 谷文祥,赵晓威,殷明浩.知识编译研究[J].计算机科学, 2010, 37(7): 20-26.GU Wenxiang, ZHAO Xiaowei, YIN Minghao. Knowledge compilation survey[J]. Computer Science, 2010, 37(7): 20-26.
[28] MURRAY N V, ROSENTHAL E. Duality in knowledge compilation techniques[C]//Proceedings of the 15th International Symposium on Foundations of Intelligent Systems. Saratoga Springs, USA, 2005: 182-190.
[29] 谷文祥,王金艳,殷明浩.基于MCN和MO启发式策略的扩展规则知识编译方法[J]. 计算机研究与发展, 2011, 48(11): 2064-2073.GU Wenxiang, WANG Jinyan, YIN Minghao. Knowledge compilation using extension rule based on MCN and MO heuristic strategies[J]. Journal of Computer Research and Development, 2011, 48(11): 2064-2073.
[30] 赖永.基于EPCCL理论的知识编译方法[D].长春:吉林大学, 2010: 1-46.LAI Yong. Research on the knowledge compilation method based on the EPCCL theory[D]. Changchun: Jilin University, 2010: 1-46.
[31] 刘大有,赖永,林海.C2E:一个高性能的EPCCL编译器[J].计算机学报, 2013, 36(6): 1254-1260.LIU Dayou, LAI Yong, LIN Hai. C2E: an EPCCL compiler with good performance[J]. Chinese Journal of Computers, 2013, 36(6): 1254-1260.
[32] YIN Minghao, LIN Hai, SUN Jigui. Counting models using extension rules[C]//Proceedings of the Twenty-Second National Conference on Artificial Intelligence. Vancouver, Canada, 2007: 1916-1917.
[33] 殷明浩,林海,孙吉贵.一种基于扩展规则的#SAT求解系统[J].软件学报, 2009, 20(7): 1714-1725.YIN Minghao, LIN Hai, SUN Jigui. Solving #SAT using extension rules[J]. Journal of Software, 2009, 20(7): 1714-1725.
[34] BIRNBAUM E, LOZINSKII E. The good old Davis-Putnam procedure helps counting models[J]. Journal of Artificial Intelligence Research, 1999, 10: 457-477.
[35] BACCHUS F, DALMAO S, PITASSI T. Algorithms and complexity results for #SAT and Bayesian inference[C]//Proceedings of the 44th Symposium on Foundations of Computer Science. Cambridge, USA, 2003: 340-351.
[36] 许有军,欧阳丹彤,叶育鑫,等.间接使用扩展规则求解#SAT问题[J].吉林大学学报:工学版, 2011, 41(4): 1047-1053.XU Youjun, OUYANG Dantong, YE Yuxin, et al. Solving #SAT with extension rule indirectly[J]. Journal of Jilin University: Engineering and Technology Edition, 2011, 41(4): 1047-1053.
[37] HOOKER J N, RAGO G, CHANDRU V, et al. Partial instantiation methods for inference in first-order logic[J]. Journal of Automated Reasoning, 2002, 28(4): 371-396.
[38] WU Xia, SUN Jigui, HOU Kun. Extension rule in first order logic[C]//Proceedings of the 5th International Conference on Cognitive Informatics. Beijing, China, 2006: 701-706.
[39] BAADER F, CALVANESE D, MCGUINNESS D, et al. The description logic handbook: theory, implementation and applications[M]. New York: Cambridge University Press, 2003.
[40] ZOU Tingting, LIU Lei, LU Shuai. Knowledge compilation for description logic based on concept extension rule[J]. Journal of Computational Information System, 2012, 8(6): 2409-2416.
[41] HALPERN J Y, MOSES Y. A guide to completeness and complexity for modal logics of knowledge and belief[J]. Artificial Intelligence, 1992, 54(3): 319-379.
[42] WU Xia, SUN Jigui. Destructive extension rule in proposition modal logic K[M]//LIU G R, TAN V B C, HAN X. Computational Methods. Dordrecht, The Netherlands: Springer, 2006: 1087-1091.
[43] WU Xia, SUN Jigui, LIN Hai, et al. Modal extension rule[J]. Progress in Natural Science, 2005, 15(6): 550-558.
[44] DUBOIS D, PRADE H. Possibilistic logic: a retrospective and prospective view[J]. Fuzzy Sets and Systems, 2004, 144(1): 3-23.
[45] 殷明浩,孙吉贵,林海,等.可能性扩展规则的推理和知识编译[J].软件学报, 2010, 21(11): 2826-2837.YIN Minghao, SUN Jigui, LIN Hai, et al. Possibilistic extension rules for reasoning and knowledge compilation[J]. Journal of Software, 2010, 21(11): 2826-2837.
[46] 谷文祥,郭鸿鹤,殷明浩,等.多值知识编译[J].东北师范大学学报:自然科学版, 2011, 43(4): 44-48.GU Xenxiang, GUO Honghe, YIN Minghao, et al. Compiling multi-valued knowledge base[J]. Journal of Northeast Normal University: Natural Science Edition, 2011, 43(4): 44-48.
备注/Memo
收稿日期:2013-08-07。
基金项目:国家自然科学基金资助项目(61070084, 61272535, 61163065,61370156,61165009);国家"973"计划资助项目(2012CB326403);广西自然科学基金资助项目(2013GXNSFBA019263,2012GXNSFAA053219);广西高校科研项目(2013YB029);"八桂学者"工程专项经费资助项目;广西师范大学博士启动基金资助项目.
作者简介:王金艳,女,1982年生,讲师,博士,主要研究方向为自动推理、智能规划、不确定理论。主持广西自然科学基金、广西教育厅科学技术研究项目、广西师范大学博士启动基金各1项,参与国家自然科学基金项目3项。发表学术论文10余篇,其中被SCI检索6篇;谷文祥,男,1947年生,教授,博士生导师,主要研究方向为智能规划与规划识别、形式语言与自动机理论、模糊数学及其应用。主持国家自然科学基金项目3项,发表学术论文100余篇;殷明浩,男,1979年生,副教授,博士生导师,博士,主要研究方向为自动推理、智能规划。主持和参与国家自然科学基金等项目多项,发表学术论文40余篇。
通讯作者:覃少华,男,1969年生,副教授,博士,主要研究方向为自动推理、计算机网络。主持和参与国家自然科学基金等项目多项,发表学术论文30余篇.E-mail:shqin@gxnu.edu.cn.
更新日期/Last Update:
1900-01-01