子句选择是自动定理证明器(ATP)的核心部分,通过优化子句选择方法能够提升ATP的能力和效率。当前,传统基于属性优先级的逐一筛选方法虽然能够实现子句选择,但难以对子句进行全面评估,并且缺乏灵活性。因此,提出基于AHP_TOPSIS的子句动...子句选择是自动定理证明器(ATP)的核心部分,通过优化子句选择方法能够提升ATP的能力和效率。当前,传统基于属性优先级的逐一筛选方法虽然能够实现子句选择,但难以对子句进行全面评估,并且缺乏灵活性。因此,提出基于AHP_TOPSIS的子句动态选择方法。该方法通过层次分析法(AHP)计算子句各个属性的权重,再利用权重结果结合逼近理想解排序法(TOPSIS)对子句进行评估排序,从而为子句选择提供依据。在AHP中,考虑到子句属性的动态变化,引入阶段感知与平滑过渡的方法,使得判断矩阵能够根据推导进程动态调整,将AHP拓展为动态AHP。同时,根据上述子句选择方法实现相应的算法,并将算法应用于一阶逻辑定理证明器CSE(Contradiction Separation Extension)中形成新的证明器CSE_AT。利用该证明器对2021—2024年的TPTP(Thousands of Problems for Theorem Provers)问题库中的一阶逻辑问题进行测试,实验结果表明,CSE_AT比CSE多证明了22个定理,且CSE_AT证明的大部分定理的Rating值集中在[0.6,0.9]。可见,基于AHP_TOPSIS的子句动态选择方法能够优化演绎路径,从而提升证明器的证明能力。展开更多
A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown...A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained.展开更多
This paper resolved an open problem proposed by A .P. Stolboushkin and M .A. Taitslin. We studied the expressibility of first order dynamic logic, and constructed infinite recursive program classes K_1 , K_2, …, RG ...This paper resolved an open problem proposed by A .P. Stolboushkin and M .A. Taitslin. We studied the expressibility of first order dynamic logic, and constructed infinite recursive program classes K_1 , K_2, …, RG K_1 K_2 … RF, such that L (RG)<L (K_1)<L (K_2) < … < L (RF), where RG, RF are regular program class and finitely generated recursively enumerable program class respectively, and L (K) is the first order dynamic logic of program class K.展开更多
I. INTRODUCTION The exploration for a unified basis of the combinatory logic and the predicate calculus will promote laying a strict and thorough mathematical foundation of the programming language possessing itself o...I. INTRODUCTION The exploration for a unified basis of the combinatory logic and the predicate calculus will promote laying a strict and thorough mathematical foundation of the programming language possessing itself of the functional and logic paradigms. The purpose of this note, proceeding from the algebraic oersoective, is to formulize the first-order mathematical展开更多
文摘子句选择是自动定理证明器(ATP)的核心部分,通过优化子句选择方法能够提升ATP的能力和效率。当前,传统基于属性优先级的逐一筛选方法虽然能够实现子句选择,但难以对子句进行全面评估,并且缺乏灵活性。因此,提出基于AHP_TOPSIS的子句动态选择方法。该方法通过层次分析法(AHP)计算子句各个属性的权重,再利用权重结果结合逼近理想解排序法(TOPSIS)对子句进行评估排序,从而为子句选择提供依据。在AHP中,考虑到子句属性的动态变化,引入阶段感知与平滑过渡的方法,使得判断矩阵能够根据推导进程动态调整,将AHP拓展为动态AHP。同时,根据上述子句选择方法实现相应的算法,并将算法应用于一阶逻辑定理证明器CSE(Contradiction Separation Extension)中形成新的证明器CSE_AT。利用该证明器对2021—2024年的TPTP(Thousands of Problems for Theorem Provers)问题库中的一阶逻辑问题进行测试,实验结果表明,CSE_AT比CSE多证明了22个定理,且CSE_AT证明的大部分定理的Rating值集中在[0.6,0.9]。可见,基于AHP_TOPSIS的子句动态选择方法能够优化演绎路径,从而提升证明器的证明能力。
基金This work was partially supported by the National Natural Science Foundationof China (Grant No. 69833020) the National High Technology Development Program of China (Grant No. 2002AA144050)the National Grand Fundamental Research 973 Program of China
文摘A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained.
基金Supported by HTP863 the fund of Beijing laboratory of cognitive science
文摘This paper resolved an open problem proposed by A .P. Stolboushkin and M .A. Taitslin. We studied the expressibility of first order dynamic logic, and constructed infinite recursive program classes K_1 , K_2, …, RG K_1 K_2 … RF, such that L (RG)<L (K_1)<L (K_2) < … < L (RF), where RG, RF are regular program class and finitely generated recursively enumerable program class respectively, and L (K) is the first order dynamic logic of program class K.
基金Project supported by the National High Technique Planning Foundation
文摘I. INTRODUCTION The exploration for a unified basis of the combinatory logic and the predicate calculus will promote laying a strict and thorough mathematical foundation of the programming language possessing itself of the functional and logic paradigms. The purpose of this note, proceeding from the algebraic oersoective, is to formulize the first-order mathematical
