半扩展规则下分解的定理证明方法
|
摘要
基于扩展规则的定理证明方法在一定意义上是与归结原理对偶的方法,通过子句集能否推导出所有极大项来判定可满足性.IER(improved extension rule)算法是不完备的算法,在判定子句集子空间不可满足时,并不能判定子句集的满足性,算法还需重新调用ER(extension rule)算法,降低了算法的求解效率.通过对子句集的极大项空间的研究,给出了子句集的极大项空间分解后子空间的求解方法.通过对扩展规则的研究,给出了极大项部分空间可满足性判定方法 PSER(partial semi-extension rule).在IER算法判定子空间不可满足时,可以调用PSER算法判定子空间对应的补空间的可满足性,从而得到子句集的可满足性,避免了不能判定极大项子空间可满足性时需重新调用ER算法的缺点,使得IER算法更完备.在此基础上,还提出DPSER(degree partial semi-extension rule)定理证明方法.实验结果表明:所提出的DPSER和IPSER的执行效率较基于归结的有向归结算法DR、IER及NER算法有明显的提高.
The extension rule based theorem proving methods are inverse methods to resolution in a sense that they check the satisfiability by determining whether all the maximum terms of the clause set can be deduced. IER(improved extension rule) algorithm is incomplete as it cannot determine the satisfiability of the clause set when the subspace of the clause set is unsatisfiable. In this condition, calling ER(extension rule) algorithms is still needed. After a thorough investigation on the maximum terms space of the clause set, this paper develops a decomposition method for decomposing the maximum terms space of the clause set. The study on extension rule also results in the PSER(partial semi-extension rule) algorithm for determining the satisfiability of a partial space of the maximum terms. When the IER determines the subspace is unsatisfiable, PSER can be used to determine the satisfiability of the complementary space, thereby, the satisfiability of the clause set can be obtained. Based on the above progress, this paper further introduces DPSER(degree partial semi-extension rule) theorem proving method. Results show that the proposed DPSER and IPSER outperform both the directional resolution algorithm DR and the extension rule based algorithms IER and NER.
The extension rule based theorem proving methods are inverse methods to resolution in a sense that they check the satisfiability by determining whether all the maximum terms of the clause set can be deduced. IER(improved extension rule) algorithm is incomplete as it cannot determine the satisfiability of the clause set when the subspace of the clause set is unsatisfiable. In this condition, calling ER(extension rule) algorithms is still needed. After a thorough investigation on the maximum terms space of the clause set, this paper develops a decomposition method for decomposing the maximum terms space of the clause set. The study on extension rule also results in the PSER(partial semi-extension rule) algorithm for determining the satisfiability of a partial space of the maximum terms. When the IER determines the subspace is unsatisfiable, PSER can be used to determine the satisfiability of the complementary space, thereby, the satisfiability of the clause set can be obtained. Based on the above progress, this paper further introduces DPSER(degree partial semi-extension rule) theorem proving method. Results show that the proposed DPSER and IPSER outperform both the directional resolution algorithm DR and the extension rule based algorithms IER and NER.
引文
[1]Zhou JP,Yin MH,Zhou CG.New worst-case upper bound for#2-sat and#3-sat with the number of clauses as parameter.In:Proc.of the AAAI 2010.Atlanta:AAAI Press,2010.217-222.http://www.aaai.org/ocs/index.php/AAAI/AAAI10/paper/view/1672
[2]Giampaolo B,Paulson LC.Accountability protocols:Formalized and verified.ACM Trans.on Information and System Security,2006,9(2):138-161.[doi:10.1145/1151414.1151416]
[3]Rintanen J,Heljanko K,Niemel I.Parallel encodings of classical planning as satisfiability.In:Proc.of the 9th European Conf.on Logics in Artificial Intelligence.Lisbon:Springer-Verlag,2004.27-30.[doi:10.1007/978-3-540-30227-8_27]
[4]Grastien A,Anbulagan N,Rintanen J,Kelareva E.Diagnosis of discrete-event systems using satisfiability algorithms.In:Proc.of the 22nd Conf.on Artificial Intelligence(AAAI 2007).Vancouver:AAAI Press,2007.305-310.
[5]Rintanen J,Grastien A.Diagnosability testing with satisfiability algorithms.In:Proc.of the 20th Int’l Joint Conf.on Artificial Intelligence(IJCAI 2007).Hyderabad:Morgan Kaufmann Publishers,2007.532-537.[doi:10.1016/j.tcs.2006.08.002]
[6]Henry K,Bart S.Unifying SAT-based and graph-based planning.In:Proc.of the 16th Int’l Joint Conf.on Artificial Intelligence(IJCAI’99).Morgan Kaufmann Publishers,1999.318-325.http://dl.acm.org/citation.cfm?id=1624218.1624265
[7]Henry AK.Deconstructing planning as satisfiability.In:Proc.of the 21th National Conf.on Artificial Intelligence(AAAI 2006).Boston:AAAI Press,2006.1524-1526.http://dl.acm.org/citation.cfm?id=1597348.1597432
[8]Myla A.TAME:Using PVS strategies for special-purpose theorem proving.Annals Mathematics and Artificial Intelligence,2000,29(1-4):139-181.[doi:10.1023/A:1018913028597]
[9]Bruno B.An efficient cryptographic protocol verifier based on prolog rules.In:Proc.of the 14th IEEE Computer Security Foundations Workshop(CSFW 2014).Cape Breton:IEEE Computer Society Press,2001.82-96.[doi:10.1109/CSFW.2001.930138]
[10]Yannick C,Laurent V.Automated unbounded verification of security protocols.In:Proc.of the Computer-Aided Verification Conf.(CAV 2002).Paris:Kluwer Academic,2002.324-337.http://dl.acm.org/citation.cfm?id=647771.734411
[11]Alessandro A,Luca C.SAT-Based model-checking for security protocols analysis.Int’l Journal of Information Security,2008,7(1):3-32.[doi:10.1007/s10207-007-0041-y]
[12]Wang XH,Liu XH.Generalized resolution.Chinese Journal of Computers,1982,5(2):81-92(in Chinese with English abstract).
[13]孙吉贵,刘叙华.广义线性半锁归结.科学通报,1992,37(19):1812-1814.
[14]Fitting M.First-Order Logic and Automated Theorem Proving.New York:Springer-Verlag,1990.http://dl.acm.org/citation.cfm?id=78167
[15]Liu Q,Sun JG.A Boolean pruning method for improving Tableau reasoning efficiency in first-order many-valued logic.Chinese Journal of Computers,2003,26(9):1165-1170(in Chinese with English abstract).
[16]Liu Q,Sun JG,Cui ZM.A method of simplifying many-valued generalized quantifiers tableau rules based on boolean pruning.Chinese Journal of Computers,2005,28(9):1514-1518(in Chinese with English abstract).
[17]Lin H,Sun JG,Zhang YM.Theorem proving based on the extension rule.Journal of Automated Reasoning,2003,31:11-21.[doi:10.1023/A:1027339205632]
[18]Wu X,Sun JG,Lin H,Feng SS.Modal extension rule.Progress in Natural Science,2005,15(6):550-558.
[19]Lai Y,Ouyang DT,Cai DB,LüS.Model counting and planning using extension rule model counting and planning using extension rule.Journal of Computer Research and Development,2009,46(3):459-469(in Chinese with English abstract).
[20]Yin MH,Sun JG,Wu X.Possibilistic extension rules for reasoning and knowledge compilation.Ruan Jian Xue Bao/Journal of Software,2010,21(11):2826-2837(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/3690.htm[doi:10.3724/SP.J.1001.2010.03690]
[21]Sun JG,Li Y,Zhu XJ,LüS.A novel theorem proving algorithm based on extension rule.Journal of Computer Research and Development,2009,14(1):9-14(in Chinese with English abstract).
[22]Gu WX,Wang JY,Yin MH.Knowledge compilation using extension rule based on MCN and MO heuristic strategies.Journal of Computer Research and Development,2011,48(11):2064-2073.
[23]Li Y,Sun JG,Wu X,Zhu XJ.Extension rule methods based on IMOM and IBOHM heuristics.Ruan Jian Xue Bao/Journal of Software,2009,20(6):1521-1527(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/3420.htm[doi:10.3724/SP.J.1001.2009.03420]
[24]Murray NV,Rosenthal E.Duality in knowledge compilation techniques.In:Proc.of the Int’l Symp.on Methodologies for Intelligent Systems.New York:Springer-Verlag,2005.182-190.[doi:10.1007/11425274_19]
[25]Sun JG,Yang FJ,Ouyang DT,Li ZS.Discrete Math.Beijing:High Education Press,2002(in Chinese).
[26]Joao MS.The impact of branching heuristics in propositional satisfiability algorithms.In:Proc.of the 9th Portuguese Conf.on Artificial Intelligence.New York:Springer-Verlag,1999.62-74.
[27]Dechter R,Rish I.Directional resolution:The davis-putnam procedure,revisited.In:Proc.of the 4th Int’l Conf.on Principles of KR&R.Bonn:Morgan Kaufmann Publishers,1994.134-145.[doi:10.1.1.1.8317]
[12]王湘浩,刘叙华.广义归结.计算机学报,1982,5(2):81-92.
[15]刘全,孙吉贵.提高一阶多值逻辑Tableau推理效率的布尔剪枝方法.计算机学报,2003,26(9):1165-1170.
[16]刘全,孙吉贵,崔志明.基于布尔剪枝的多值广义量词Tableau推理规则简化方法.计算机学报,2005,28(9):1514-1518.
[19]赖永,欧阳丹彤,蔡敦波,吕帅.基于扩展规则的模型计数与智能规划方法.计算机研究与发展,2009,46(3):459-469.
[20]殷明浩,孙吉贵,林海,吴瑕.基于可能性扩展规则的推理和知识编译.软件学报,2010,21(11):2826-2837.http://www.jos.org.cn/1000-9825/3690.htm[doi:10.3724/SP.J.1001.2010.03690]
[21]孙吉贵,李莹,朱兴军,吕帅.一种新的基于扩展规则的定理证明算法.计算机研究与发展,2009,14(1):9-14.
[22]谷文祥,王金艳,殷明浩.基于MCN和MO启发式策略的扩展规则知识编译方法.计算机研究与发展,2011,48(11):2064-2073.
[23]李莹,孙吉贵,吴瑕,朱兴军.基于IMOM和IBOHM启发式策略的扩展规则算法.软件学报,2009,20(6):1521-1527.http://www.jos.org.cn/1000-9825/3420.htm[doi:10.3724/SP.J.1001.2009.03420]
[25]孙吉贵,杨凤杰,欧阳丹彤,李占山.离散数学.北京:高等教育出版社,2002.
[2]Giampaolo B,Paulson LC.Accountability protocols:Formalized and verified.ACM Trans.on Information and System Security,2006,9(2):138-161.[doi:10.1145/1151414.1151416]
[3]Rintanen J,Heljanko K,Niemel I.Parallel encodings of classical planning as satisfiability.In:Proc.of the 9th European Conf.on Logics in Artificial Intelligence.Lisbon:Springer-Verlag,2004.27-30.[doi:10.1007/978-3-540-30227-8_27]
[4]Grastien A,Anbulagan N,Rintanen J,Kelareva E.Diagnosis of discrete-event systems using satisfiability algorithms.In:Proc.of the 22nd Conf.on Artificial Intelligence(AAAI 2007).Vancouver:AAAI Press,2007.305-310.
[5]Rintanen J,Grastien A.Diagnosability testing with satisfiability algorithms.In:Proc.of the 20th Int’l Joint Conf.on Artificial Intelligence(IJCAI 2007).Hyderabad:Morgan Kaufmann Publishers,2007.532-537.[doi:10.1016/j.tcs.2006.08.002]
[6]Henry K,Bart S.Unifying SAT-based and graph-based planning.In:Proc.of the 16th Int’l Joint Conf.on Artificial Intelligence(IJCAI’99).Morgan Kaufmann Publishers,1999.318-325.http://dl.acm.org/citation.cfm?id=1624218.1624265
[7]Henry AK.Deconstructing planning as satisfiability.In:Proc.of the 21th National Conf.on Artificial Intelligence(AAAI 2006).Boston:AAAI Press,2006.1524-1526.http://dl.acm.org/citation.cfm?id=1597348.1597432
[8]Myla A.TAME:Using PVS strategies for special-purpose theorem proving.Annals Mathematics and Artificial Intelligence,2000,29(1-4):139-181.[doi:10.1023/A:1018913028597]
[9]Bruno B.An efficient cryptographic protocol verifier based on prolog rules.In:Proc.of the 14th IEEE Computer Security Foundations Workshop(CSFW 2014).Cape Breton:IEEE Computer Society Press,2001.82-96.[doi:10.1109/CSFW.2001.930138]
[10]Yannick C,Laurent V.Automated unbounded verification of security protocols.In:Proc.of the Computer-Aided Verification Conf.(CAV 2002).Paris:Kluwer Academic,2002.324-337.http://dl.acm.org/citation.cfm?id=647771.734411
[11]Alessandro A,Luca C.SAT-Based model-checking for security protocols analysis.Int’l Journal of Information Security,2008,7(1):3-32.[doi:10.1007/s10207-007-0041-y]
[12]Wang XH,Liu XH.Generalized resolution.Chinese Journal of Computers,1982,5(2):81-92(in Chinese with English abstract).
[13]孙吉贵,刘叙华.广义线性半锁归结.科学通报,1992,37(19):1812-1814.
[14]Fitting M.First-Order Logic and Automated Theorem Proving.New York:Springer-Verlag,1990.http://dl.acm.org/citation.cfm?id=78167
[15]Liu Q,Sun JG.A Boolean pruning method for improving Tableau reasoning efficiency in first-order many-valued logic.Chinese Journal of Computers,2003,26(9):1165-1170(in Chinese with English abstract).
[16]Liu Q,Sun JG,Cui ZM.A method of simplifying many-valued generalized quantifiers tableau rules based on boolean pruning.Chinese Journal of Computers,2005,28(9):1514-1518(in Chinese with English abstract).
[17]Lin H,Sun JG,Zhang YM.Theorem proving based on the extension rule.Journal of Automated Reasoning,2003,31:11-21.[doi:10.1023/A:1027339205632]
[18]Wu X,Sun JG,Lin H,Feng SS.Modal extension rule.Progress in Natural Science,2005,15(6):550-558.
[19]Lai Y,Ouyang DT,Cai DB,LüS.Model counting and planning using extension rule model counting and planning using extension rule.Journal of Computer Research and Development,2009,46(3):459-469(in Chinese with English abstract).
[20]Yin MH,Sun JG,Wu X.Possibilistic extension rules for reasoning and knowledge compilation.Ruan Jian Xue Bao/Journal of Software,2010,21(11):2826-2837(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/3690.htm[doi:10.3724/SP.J.1001.2010.03690]
[21]Sun JG,Li Y,Zhu XJ,LüS.A novel theorem proving algorithm based on extension rule.Journal of Computer Research and Development,2009,14(1):9-14(in Chinese with English abstract).
[22]Gu WX,Wang JY,Yin MH.Knowledge compilation using extension rule based on MCN and MO heuristic strategies.Journal of Computer Research and Development,2011,48(11):2064-2073.
[23]Li Y,Sun JG,Wu X,Zhu XJ.Extension rule methods based on IMOM and IBOHM heuristics.Ruan Jian Xue Bao/Journal of Software,2009,20(6):1521-1527(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/3420.htm[doi:10.3724/SP.J.1001.2009.03420]
[24]Murray NV,Rosenthal E.Duality in knowledge compilation techniques.In:Proc.of the Int’l Symp.on Methodologies for Intelligent Systems.New York:Springer-Verlag,2005.182-190.[doi:10.1007/11425274_19]
[25]Sun JG,Yang FJ,Ouyang DT,Li ZS.Discrete Math.Beijing:High Education Press,2002(in Chinese).
[26]Joao MS.The impact of branching heuristics in propositional satisfiability algorithms.In:Proc.of the 9th Portuguese Conf.on Artificial Intelligence.New York:Springer-Verlag,1999.62-74.
[27]Dechter R,Rish I.Directional resolution:The davis-putnam procedure,revisited.In:Proc.of the 4th Int’l Conf.on Principles of KR&R.Bonn:Morgan Kaufmann Publishers,1994.134-145.[doi:10.1.1.1.8317]
[12]王湘浩,刘叙华.广义归结.计算机学报,1982,5(2):81-92.
[15]刘全,孙吉贵.提高一阶多值逻辑Tableau推理效率的布尔剪枝方法.计算机学报,2003,26(9):1165-1170.
[16]刘全,孙吉贵,崔志明.基于布尔剪枝的多值广义量词Tableau推理规则简化方法.计算机学报,2005,28(9):1514-1518.
[19]赖永,欧阳丹彤,蔡敦波,吕帅.基于扩展规则的模型计数与智能规划方法.计算机研究与发展,2009,46(3):459-469.
[20]殷明浩,孙吉贵,林海,吴瑕.基于可能性扩展规则的推理和知识编译.软件学报,2010,21(11):2826-2837.http://www.jos.org.cn/1000-9825/3690.htm[doi:10.3724/SP.J.1001.2010.03690]
[21]孙吉贵,李莹,朱兴军,吕帅.一种新的基于扩展规则的定理证明算法.计算机研究与发展,2009,14(1):9-14.
[22]谷文祥,王金艳,殷明浩.基于MCN和MO启发式策略的扩展规则知识编译方法.计算机研究与发展,2011,48(11):2064-2073.
[23]李莹,孙吉贵,吴瑕,朱兴军.基于IMOM和IBOHM启发式策略的扩展规则算法.软件学报,2009,20(6):1521-1527.http://www.jos.org.cn/1000-9825/3420.htm[doi:10.3724/SP.J.1001.2009.03420]
[25]孙吉贵,杨凤杰,欧阳丹彤,李占山.离散数学.北京:高等教育出版社,2002.
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |