计算机科学 ›› 2020, Vol. 47 ›› Issue (3): 217-221.doi: 10.11896/jsjkx.190100004
曹锋1,3,徐扬2,3,钟建1,3,宁欣然1,3
CAO Feng1,3,XU Yang2,3,ZHONG Jian1,3,NING Xin-ran1,3
摘要: 一阶逻辑定理证明是人工智能的核心基础,研究一阶逻辑自动定理证明器的相关理论和高效的算法实现具有重要的学术意义。当前一阶逻辑自动定理证明器首先通过子句集预处理约简子句集规模,然后通过演绎方法对定理进行判定。现有的应用于证明器中的子句集预处理方法普遍只从与目标子句项符号相关性角度出发,不能很好地从文字的互补对关系中体现子句间的演绎。为了在子句集预处理时从演绎的角度刻画子句间的关系,定义了目标演绎距离的概念并给出了计算方法,提出了一种基于目标演绎距离的一阶逻辑子句集预处理方法。首先对原始子句集进行包含冗余子句约简并应用纯文字删除规则,然后根据目标子句计算剩余子句集中的文字目标演绎距离、子句目标演绎距离,并最终通过设定子句演绎距离阈值来实现对子句集的进一步预处理。将该预处理方法应用于顶尖证明器Vampire,以2017年国际一阶逻辑自动定理证明器标准一阶逻辑问题组竞赛例为测试对象,在标准的300s内,加入提出的子句集预处理方法的Vampire4.1相比原始的Vampire4.1多证明4个定理,能证明10个Vampire4.1未证明的定理,占其未证明定理总数的13.5%;在证明的定理中,提出的子句集预处理方法能对77.2%的子句集进行约简,最大子句集约简规模达到51.7%。实验结果表明,提出的一阶逻辑子句集预处理方法是一种有效的方法,能有效地约简一阶逻辑子句集的规模,提高一阶逻辑自动定理证明器的证明能力。
中图分类号:
[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. |
[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 |
|