[1]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]
Copy

Extension rule: a survey

CAAI Transactions on Intelligent Systems[ISSN 1673-4785/CN 23-1538/TP] Volume: 9 Number of periods: 2014 1 Page number: 1-11 Column: 综述 Public date: 2014-02-25
Title:
Extension rule: a survey
Author(s):
WANG Jinyan1;  GU Wenxiang2; 3;  QIN Shaohua1;  YIN Minghao3
1. School of Computer Science and Information Technology, Guangxi Normal University, Guilin 541004, China;
2. Department of Basic Subjects Teaching, Changchun Architecture & Civil Engineering College, Changchun 130607, China;
3. School of Computer Science and Information Technology, Northeast Normal University, Changchun 130117, China
Keywords:
automated reasoning; resolution principle; extension rule; SAT; #SAT
CLC:
TP181
DOI:
10.3969/j.issn.1673-4785.201308004
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.
Similar References:

Memo

-

Last Update: 1900-01-01

Copyright © CAAI Transactions on Intelligent Systems