Stability-based Term Evaluation Method in First-order Logic

doi:10.19678/j.issn.1000-3428.0054368

Computer Engineering ›› 2019, Vol. 45 ›› Issue (11): 183-190,197. doi: 10.19678/j.issn.1000-3428.0054368

Previous Articles Next Articles

Stability-based Term Evaluation Method in First-order Logic

ZHONG Jian^a,b, XU Yang^b,c, CHEN Shuwei^b,c, HE Xingxing^b,c

a. The School of Information Science and Technology;b. National-Local Joint Engineering Laboratory of System Credibility Automatic Verification;c. School of Mathematics, Southwest Jiaotong University, Chengdu 611756, China

Received:2019-03-25 Revised:2019-06-09 Published:2019-06-22

一阶逻辑中基于稳定度的项评估方法

钟建^a,b, 徐扬^b,c, 陈树伟^b,c, 何星星^b,c

西南交通大学 a. 信息科学与技术学院;b. 系统可信性自动验证国家地方联合工程实验室;c. 数学学院, 成都 611756

作者简介:钟建(1980-),男,博士研究生,主研方向为智能信息处理、自动推理;徐扬,教授、博士生导师;陈树伟、何星星,副教授、博士。
基金资助:
国家自然科学基金（61673320）；中央高校基本科研业务费专项资金（2682018ZT10，2682018CX59）。

Abstract

Abstract: To address the complex term structure and difficult extraction of grammatical and semantic features in first-order logic,this paper analyzes the constraints and measurement rules of Herbrand semantic features of a term in text replacement.On this basis,the paper gives a definition of the stability of a term,and proposes a stability-based term evaluation method.As a heuristic strategy for text selection,this method is applied to the redundancy judgement of the clause set in Automated Theorem Prover(ATP).Results show that this method can better characterize the features of a term in first-order logic.Compared with the word selection method based on term order,its detection times are reduced by 50.8% on average,and its running time is shortened by 53.3% on average.

Key words: first-order logic, Automated Theorem Prover(ATP), term evaluation, heuristic strategy, Herbrand semantic features

摘要： 针对一阶逻辑中项结构比较复杂、语法与语义特征难以抽取的问题，基于项在文字替换过程中的Herbrand语义特征，分析其制约因素和度量规则，给出项稳定度的定义并提出一种基于稳定度的项评估方法。将所提方法作为文字选择的启发式策略，应用于自动定理证明器中子句集的归入冗余判定中，结果表明，该方法能较好地刻画一阶逻辑中的项特征，与基于项序的文字选择方法相比，其检测次数平均减少50.8%，运行时间平均缩短53.3%。

关键词: 一阶逻辑, 自动定理证明器, 项评估, 启发式策略, Herbrand语义特征

CLC Number:

V221.3

ZHONG Jian, XU Yang, CHEN Shuwei, HE Xingxing. Stability-based Term Evaluation Method in First-order Logic[J]. Computer Engineering, 2019, 45(11): 183-190,197.

钟建, 徐扬, 陈树伟, 何星星. 一阶逻辑中基于稳定度的项评估方法[J]. 计算机工程, 2019, 45(11): 183-190,197.

/ / Recommend / Download Citations

URL: http://www.ecice06.com/EN/10.19678/j.issn.1000-3428.0054368

http://www.ecice06.com/EN/Y2019/V45/I11/183

Figures/Tables 4

References

[1] 陈钢,于林宇,裘宗燕,等.基于逻辑的形式化验证方法:进展及应用[J].北京大学学报(自然科学版),2016,52(2):363-373.
[2] 杨世瀚,吴尽昭,丁广泓,等.模拟与混合信号电路的形式化验证[J].计算机工程,2016,42(8):34-38.
[3] 陶钧.基于定理证明的数字系统验证研究[D].杭州:浙江大学,2013.
[4] BECKERT B,HÄHNLE R.Reasoning and verification:state of the art and current trends[J].IEEE Intelligent Systems,2014,29(1):20-29.
[5] 彭宁.关于计算机网络通信协议验证技术的探讨[J].计算机产品与流通,2019(3):44.
[6] 陈丽娜,黄宏斌,邓苏.基于点的FO-POMDP值迭代方法研究[J].计算机工程,2013,39(10):217-220.
[7] D'SILVA V,KROENING D,WEISSENBACHER G.A survey of automated techniques for formal software verification[J].IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,2008,27(7):1165-1178.
[8] 胡凯.智能合约的形式化验证方法[J].信息安全研究,2016,2(12):1080-1089.
[9] ROBINSON J A.A machine-oriented logic based on the resolution principle[EB/OL].[2019-02-26].http://pdfs.semanticscholar.org/6903/4fde66514c1b8fbfe43801d65380d01e3a94.pdf.
[10] BUSS S,JOHANNSEN J.On linear resolution[J].Journal on Satisfiability,Boolean Modeling and Computation,2017,10(8):23-35.
[11] SCHULZ S.E-a brainiac theorem prover[J].AI Communications,2002,15(2/3):111-126.
[12] KALISZYK C,URBAN J,VYSKOCIL J.Efficient semantic features for automated reasoning over large theories[C]//Proceedings of International Conference on Artificial Intelligence.[S.l.]:AAAI Press,2015:3084-3090.
[13] SCHULZ S,HRMANN M.Performance of clause selection heuristics for saturation-based theorem proving[C]//Proceedings of International Joint Conference on Automated Reasoning.Berlin,Germany:Springer,2016:330-345.
[14] JAKǓBU V J,URBAN J.Hierarchical invention of theorem proving strategies[J].AI Communications,2018,31(3):237-250.
[15] BRIDGE J P,HOLDEN S B,PAULSON L C.Machine learning for first-order theorem proving[J].Journal of Automated Reasoning,2014,53(2):141-172.
[16] BLANCHETTE J C,GREENAWAY D,KALISZYK C,et al.A learning-based fact selector for Isabelle/HOL[J].Journal of Automated Reasoning,2016,57(3):219-244.
[17] KUCIK A S,KOROVIN K.Premise selection with neural networks and distributed representation of features[EB/OL].[2019-02-26].https://arxiv.org/pdf/1807.10268.pdf.
[18] SEKAR R,RAMAKRISHNAN I V,VORONKOV A.Term indexing[M]//ROBINSON A J A,VORONKOV A.Handbook of automated reasoning.Amsterdam,Holland:Elsevier,2001.
[19] GRAF P.Substitution tree indexing[C]//Proceedings of International Conference on Rewriting Techniques and Applications.Berlin,Germany:Springer,1995:117-131.
[20] KNUTH D E,BENDIX P B.Simple word problems in universal algebras[J].Computational Problems in Abstract Algebra,1970,22:263-297.
[21] LÖCHNER B.Things to know when implementing KBO[J].Journal of Automated Reasoning,2006,36(4):289-310.
[22] DERSHOWITZ N.Orderings for term-rewriting systems[J].Theoretical Computer Science,1982,17(3):279-301.
[23] RIAZANOV A,VORONKOV A.Vampire 1.1(system description)[C]//Proceedings of the 1st International Joint Conference on Automated Reasoning.Berlin,Germany:Springer,2001:376-380.
[24] KOROVIN K.iProver-an instantiation-based theorem prover for first-order logic(system description)[J].Automated Reasoning,2008,34:292-298.
[25] DERSHOWITZ N.Termination of rewriting[J].Journal of Symbolic Computation,1987,3(1):69-115.
[26] GENESERETH M,KAO E.Herbrand semantics[EB/OL].[2019-03-10].http://logic.stanford.edu/herbrand/herbrand.html.
[27] 刘叙华.基于归结方法的自动推理[M].北京:科学出版社,1994.
[28] ROBINSON A J A,VORONKOV A.Handbook of automated reasoning[M].Amsterdam,Holland:Elsevier,2001.
[29] GANZINGER H.Chapter 2-resolution theorem proving[M].Amsterdam,Holland:Elsevier,2001.
[30] 张家锋,徐扬,曹发生.格值一阶逻辑中α-语义归结方法的相容性[J].辽宁工程技术大学学报(自然科学版),2016,35(11):1335-1340.
[31] The CADE ATP system competition[EB/OL].[2019-03-10].http://www.cs.miami.edu/~tptp/CASC/.

Please choose a citation manager

Content to export