基于目标演绎距离的一阶逻辑子句集预处理方法

doi:10.11896/jsjkx.190100004

计算机科学 ›› 2020, Vol. 47 ›› Issue (3): 217-221.doi: 10.11896/jsjkx.190100004

基于目标演绎距离的一阶逻辑子句集预处理方法

曹锋^1,3,徐扬^2,3,钟建^1,3,宁欣然^1,3

(西南交通大学信息科学与技术学院成都611756)¹;
(西南交通大学数学学院成都611756)²;
(系统可信性自动验证国家地方联合工程实验室成都610031)³

收稿日期:2019-01-02 出版日期:2020-03-15 发布日期:2020-03-30
通讯作者: 曹锋(caofeng19840301@163.com)
基金资助:
国家自然科学基金(61673320);中央高校基本科研业务费专项资金(2682017ZT12,2682018CX59,2682018ZT25)

First-order Logic Clause Set Preprocessing Method Based on Goal Deduction Distance

CAO Feng^1,3,XU Yang^2,3,ZHONG Jian^1,3,NING Xin-ran^1,3

(School of Information Science and Technology, Southwest Jiaotong University, Chengdu 611756, China)¹;
(School of Mathematics, Southwest Jiaotong University, Chengdu 611756, China)²;
(National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Chengdu 610031, China)³

Received:2019-01-02 Online:2020-03-15 Published:2020-03-30
About author:CAO Feng,born in 1984,Ph.D candidate.His main research interests include intelligent information processing and automated reasoning. XU Yang,born in 1956,Ph.D supervisor,is member of China Computer Fede-ration.His main research interests include uncertainty reasoning and automated reasoning.
Supported by:
This work was supported by the National Natural Science Foundation of China (61673320) and Fundamental Research Funds for the Central Universities (2682017ZT12, 2682018CX59, 2682018ZT25).

摘要/Abstract

摘要： 一阶逻辑定理证明是人工智能的核心基础,研究一阶逻辑自动定理证明器的相关理论和高效的算法实现具有重要的学术意义。当前一阶逻辑自动定理证明器首先通过子句集预处理约简子句集规模,然后通过演绎方法对定理进行判定。现有的应用于证明器中的子句集预处理方法普遍只从与目标子句项符号相关性角度出发,不能很好地从文字的互补对关系中体现子句间的演绎。为了在子句集预处理时从演绎的角度刻画子句间的关系,定义了目标演绎距离的概念并给出了计算方法,提出了一种基于目标演绎距离的一阶逻辑子句集预处理方法。首先对原始子句集进行包含冗余子句约简并应用纯文字删除规则,然后根据目标子句计算剩余子句集中的文字目标演绎距离、子句目标演绎距离,并最终通过设定子句演绎距离阈值来实现对子句集的进一步预处理。将该预处理方法应用于顶尖证明器Vampire,以2017年国际一阶逻辑自动定理证明器标准一阶逻辑问题组竞赛例为测试对象,在标准的300s内,加入提出的子句集预处理方法的Vampire4.1相比原始的Vampire4.1多证明4个定理,能证明10个Vampire4.1未证明的定理,占其未证明定理总数的13.5%;在证明的定理中,提出的子句集预处理方法能对77.2%的子句集进行约简,最大子句集约简规模达到51.7%。实验结果表明,提出的一阶逻辑子句集预处理方法是一种有效的方法,能有效地约简一阶逻辑子句集的规模,提高一阶逻辑自动定理证明器的证明能力。

关键词: 人工智能, 冗余子句, 演绎距离, 一阶逻辑, 子句集预处理

Abstract: The first-order logic theorem proving is the core foundation of artificial intelligence,it has great academic significance to study the theory and efficient algorithm implementation for first-order logic automated theorem provers.The current provers adopt clause set preprocessing approaches to reduce clause set scale,then apply inference rules to prove theorems.The existing clause set preprocessing method used in provers is generally only from the perspective of the semantic relevance to axioms and conjecture,and it can't reflect the deduction between clauses well from the complementary pairs of literals point of view.In order to describe the relationship between clauses from the perspective of deduction,the definition of goal deduction distance and the calculation method are proposed,and a first-order logic clause set preprocessing method is presented based on the proposed goal deduction distance.Firstly,the original clause set is applied with redundant clause simplification and pure literal deletion rule.Then,taking the goal clauses into consideration,the literal goal deduction distance and the clause goal deduction distance are calculated,and finally further clause set preprocessing is realized by the setting threshold of clause deduction distance.We implement the proposed clause set preprocessing method in Vampire that is the winner of the 2017 CADE ATP System Competition (CASC-26) FOF division,and apply it to solve the CASC-26 problem.Within the standard 300 seconds,the top prover Vampire4.1 with the proposed clause set preprocessing method outperforms Vampire4.1 by solving 4 theorems more than Vampire4.1,and 10 out of the 74 problems unsolved by Vampire4.1,accounting for 13.5% of the total.The proposed clause set preprocessing method has affected 77.2% of the solved theorems,and the largest reduction proportion is 51.7%.Experimental results show that the proposed first-order logic clause set preprocessing method is an effective method,which can effectively reduce the clause set scale and improve the ability of first-order logic automated theorem prover.

Key words: Artificial intelligence, Clause set preprocessing, Deduction distance, First-order logic, Redundant clause

中图分类号:

TP311

曹锋,徐扬,钟建,宁欣然. 基于目标演绎距离的一阶逻辑子句集预处理方法[J]. 计算机科学, 2020, 47(3): 217-221. https://doi.org/10.11896/jsjkx.190100004

CAO Feng,XU Yang,ZHONG Jian,NING Xin-ran. First-order Logic Clause Set Preprocessing Method Based on Goal Deduction Distance[J]. Computer Science, 2020, 47(3): 217-221. https://doi.org/10.11896/jsjkx.190100004

参考文献

[1]RIAZANOV A,VORONKOV A.The design and implementa- tion of VAMPIRE [J].AI Communications,2002,15(2):91-110.
[2]VORONKOV A.First-Order theorem proving and vampire [C]∥Proceedings of the 27th International Conference on Computer Aided Verification.London:Springer Press,2013:1-35.
[3]SCHULZ S.E-a brainiac theorem prover [J].AI Communications,2002,15(2):111-126.
[4]SCHULZ S.System Description:E 1.8[C]∥Proceedings of the 19th International Conferences on Logic for Programming,Artificial Intelligence and Reasoning.Stellenbosch:Springer Press,2013:735-743.
[5]KOROVIN K.iProver-An Instantiation-Based Theorem Prover for First-Order Logic (System Description) [J].Lecture Notes in Computer Science,2008,5195(1):292-298.
[6]PAVLOV V,SCHUKIN A,CHERKASOVA T.Exploring Automated Reasoning in First-Order Logic:Tools,Techniques and Application Areas [J].Communications in Computer & Information Science,2013,394(1):102-116.
[7]HÖfner P,STRUTH G,SUTCLIFFE G.Automated verification of refinement laws [J].Annals of Mathematics & Artificial Intelligence,2009,55(1／2):35-62.
[8]ROBINSON J A.A machine oriented logic based on the resolution principle [J].Journal of the Acm,1965,12(1):23-41.
[9]MCCUNE W.OTTER 3.3 Reference Manual [J].Office of Scien- tific & Technical Information Technical Reports,2007,11(4):217-220.
[10]DENZINGER J,KRONENBURG M,SCHULZ S.Distributed and Learning Equational Prover [J].Journal of Automated Reasoning,1997,18(2):189-198.
[11]KHASIDASHVILI Z,KOROVIN K.Predicate Elimination for Preprocessing in First-Order Theorem Proving[C]∥International Conference on Theory and Applications of Satisfiability Testing.Bordeaux:Springer Press,2016:361-372.
[12]LOVELAND D W,REED D W,WILSON D S.SATCHMORE:SATCHMO with Relevancy [J].Journal of AutomatedReaso-ning,1995,14(2):325-351.
[13]BIBEL W,SCHMITT P H.Automated Deduction－A Basis for Applications,volume III [M].Dordrecht:Kluwer Academic Publishers,1998:119-124.
[14]SUTCLIFFE G,PUZIS Y.SRASS-A Semantic Relevance Axi- om Selection System[C]∥Proceedings of the 21th International Conference on Automated Deduction.Bremen:Springer Press,2007:295-310.
[15]VORONKOV A.Sine Qua non for large theory reasoning[C]∥Proceedings of the 23th International Conference on Automated Deduction.Wroclaw:Springer Press,2011:299-314.

相关文章 15

[1]	丛颖男, 王兆毓, 朱金清. 关于法律人工智能数据和算法问题的若干思考 Insights into Dataset and Algorithm Related Problems in Artificial Intelligence for Law 计算机科学, 2022, 49(4): 74-79. https://doi.org/10.11896/jsjkx.210900191
[2]	李野, 陈松灿. 基于物理信息的神经网络:最新进展与展望 Physics-informed Neural Networks:Recent Advances and Prospects 计算机科学, 2022, 49(4): 254-262. https://doi.org/10.11896/jsjkx.210500158
[3]	朝乐门, 尹显龙. 人工智能治理理论及系统的现状与趋势 AI Governance and System:Current Situation and Trend 计算机科学, 2021, 48(9): 1-8. https://doi.org/10.11896/jsjkx.210600034
[4]	景慧昀, 魏薇, 周川, 贺欣. 人工智能安全框架 Artificial Intelligence Security Framework 计算机科学, 2021, 48(7): 1-8. https://doi.org/10.11896/jsjkx.210300306
[5]	谢宸琪, 张保稳, 易平. 人工智能模型水印研究综述 Survey on Artificial Intelligence Model Watermarking 计算机科学, 2021, 48(7): 9-16. https://doi.org/10.11896/jsjkx.201200204
[6]	景慧昀, 周川, 贺欣. 针对人脸检测对抗攻击风险的安全测评方法 Security Evaluation Method for Risk of Adversarial Attack on Face Detection 计算机科学, 2021, 48(7): 17-24. https://doi.org/10.11896/jsjkx.210300305
[7]	暴雨轩, 芦天亮, 杜彦辉, 石达. 基于i_ResNet34模型和数据增强的深度伪造视频检测方法 Deepfake Videos Detection Method Based on i_ResNet34 Model and Data Augmentation 计算机科学, 2021, 48(7): 77-85. https://doi.org/10.11896/jsjkx.210300258
[8]	秦智慧, 李宁, 刘晓彤, 刘秀磊, 佟强, 刘旭红. 无模型强化学习研究综述 Overview of Research on Model-free Reinforcement Learning 计算机科学, 2021, 48(3): 180-187. https://doi.org/10.11896/jsjkx.200700217
[9]	郝娇, 惠小静, 马硕, 金明慧. 一阶逻辑中公理化真度研究 Study on Axiomatic Truth Degree in First-order Logic 计算机科学, 2021, 48(11A): 669-671. https://doi.org/10.11896/jsjkx.210200012
[10]	仝鑫, 王斌君, 王润正, 潘孝勤. 面向自然语言处理的深度学习对抗样本综述 Survey on Adversarial Sample of Deep Learning Towards Natural Language Processing 计算机科学, 2021, 48(1): 258-267. https://doi.org/10.11896/jsjkx.200500078
[11]	周蔚, 罗旭东. 一种替代性纠纷在线仲裁系统 Alternative Online Arbitration System for Dispute 计算机科学, 2020, 47(6A): 583-590. https://doi.org/10.11896/JsJkx.190900140
[12]	任仪. 基于区块链与人工智能的网络多服务器SIP信息加密系统设计 Design of Network Multi-server SIP Information Encryption System Based on Block Chain and Artificial Intelligence 计算机科学, 2020, 47(6A): 634-638. https://doi.org/10.11896/JsJkx.190600075
[13]	赵澄, 叶耀威, 姚明海. 基于金融文本情感的股票波动预测 Stock Volatility Forecast Based on Financial Text Emotion 计算机科学, 2020, 47(5): 79-83. https://doi.org/10.11896/jsjkx.190400145
[14]	王国胤, 瞿中, 赵显莲. 交叉融合的“人工智能+”学科建设探索与实践 Practical Exploration of Discipline Construction of Artificial Intelligence+ 计算机科学, 2020, 47(4): 1-5. https://doi.org/10.11896/jsjkx.200300144
[15]	王晓明,赵歆波. 阅读眼动追踪语料库的构建与应用研究综述 Survey of Construction and Application of Reading Eye-tracking Corpus 计算机科学, 2020, 47(3): 174-181. https://doi.org/10.11896/jsjkx.190800040

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

基于目标演绎距离的一阶逻辑子句集预处理方法

First-order Logic Clause Set Preprocessing Method Based on Goal Deduction Distance

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

Metrics

本文评价

推荐阅读 0