Computer Science ›› 2020, Vol. 47 ›› Issue (3): 217-221.doi: 10.11896/jsjkx.190100004

• Artificial Intelligence • Previous Articles     Next Articles

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

CAO Feng1,3,XU Yang2,3,ZHONG Jian1,3,NING Xin-ran1,3   

  1. (School of Information Science and Technology, Southwest Jiaotong University, Chengdu 611756, China)1;
    (School of Mathematics, Southwest Jiaotong University, Chengdu 611756, China)2;
    (National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Chengdu 610031, China)3
  • 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: 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: First-order logic, Artificial intelligence, Clause set preprocessing, Deduction distance, Redundant clause

CLC Number: 

  • TP311
[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] WANG Guo-yin, QU Zhong, ZHAO Xian-lian. Practical Exploration of Discipline Construction of Artificial Intelligence+ [J]. Computer Science, 2020, 47(4): 1-5.
[2] WANG Xiao-ming,ZHAO Xin-bo. Survey of Construction and Application of Reading Eye-tracking Corpus [J]. Computer Science, 2020, 47(3): 174-181.
[3] ANG Wei-yi,BAI Chen-jia,CAI Chao,ZHAO Ying-nan,LIU Peng. Survey on Sparse Reward in Deep Reinforcement Learning [J]. Computer Science, 2020, 47(3): 182-191.
[4] LIU Ting, XU Yang, CHEN Xiu-lan. Unit Clauses and Their Complementary Literals and Redundant Clauses in Propositional Logic [J]. Computer Science, 2019, 46(8): 255-259.
[5] ZHANG Yu-qian,GU Dong-yun. Review of Computer Aided Diagnosis for Parkinson’s Tremor and Essential Tremor [J]. Computer Science, 2019, 46(7): 22-29.
[6] LIU Sheng-wa, SUN Jun-ming, GAO Xiang, WANG Min. Analysis and Establishment of Drilling Speed Prediction Model for Drilling MachineryBased on Artificial Neural Networks [J]. Computer Science, 2019, 46(6A): 605-608.
[7] CHEN Chao, QI Feng. Review on Development of Convolutional Neural Network and Its Application in Computer Vision [J]. Computer Science, 2019, 46(3): 63-73.
[8] CHENG Xian-yi,XIE Lu,ZHU Jian-xin,HU Bin,SHI Quan. Review of Generative Adversarial Network [J]. Computer Science, 2019, 46(3): 74-81.
[9] LUO Xu-dong, HUANG Qiao-juan, ZHAN Jie-yu. A Survey of Automated Negotiation and Its Fuzzy Set Based Models [J]. Computer Science, 2019, 46(12): 220-230.
[10] YAO Yan-ling. Analysis and Investigation of Research Frontiers in International Field of Artificial Intelligence in 2017 [J]. Computer Science, 2018, 45(9): 1-10.
[11] ZHAO Xing-yu, DING Shi-fei. Research on Deep Reinforcement Learning [J]. Computer Science, 2018, 45(7): 1-6.
[12] HUANG Qiao-juan, LUO Xu-dong. State-of-the-art and Development Trend of Artificial Intelligence Combined with Law [J]. Computer Science, 2018, 45(12): 1-11.
[13] LONG Hui, ZHU Ding-ju, TIAN Juan. Research on Deep Learning Used in Intelligent Robots [J]. Computer Science, 2018, 45(11A): 43-47,52.
[14] LI Shi-yu, WANG Feng, CAO Bin and MEI Qi. Application Survey of Artificial Intelligence in Neurology [J]. Computer Science, 2017, 44(Z11): 29-32, 50.
[15] LI Yue, SU Cheng, JIA Jia, XU Zhen and TIAN Rui-qiang. Analysis of Development Status of World Artificial Intelligence Based on Scientific Measurement [J]. Computer Science, 2017, 44(12): 183-187.
Full text



[1] ZHANG Chen-bin,ZHANG Yun-chun, ZHENG Yang,ZHANG Peng-cheng, LIN Sen. Malware Classification Based on Texture Fingerprint of Gray-scale Images[J]. Computer Science, 2018, 45(6A): 383 -386 .
[2] CHI Kai-kai, LIN Yi-min, LI Yan-jun and CHENG Zhen. Energy Transmitter Placement to Optimize Duty Cycle of RF Energy Harvesting Wireless Sensor Networks[J]. Computer Science, 2017, 44(3): 128 -131 .
[3] GUO Ying-ying, ZHANG Li-ping, LI Song. Group Nearest Neighbor Query Method of Line Segment in Obstacle Space[J]. Computer Science, 2018, 45(6): 172 -175,192 .
[4] QU Zhong and ZHAO Cong-mei. Anti-occlusion Adaptive-scale Object Tracking Algorithm[J]. Computer Science, 2018, 45(4): 296 -300 .
[5] LI Xiao-xin, WU Ke-song, QI Pan-pan, ZHOU Xuan and LIU Zhi-yong. Local Sphere Normalization Embedding:An Improved Scheme for PCANet[J]. Computer Science, 2018, 45(5): 238 -242, 249 .
[6] SHI Hai-zhong and SHI Yue. (V,R)-Languages[J]. Computer Science, 2014, 41(Z6): 33 -36 .
[7] WANG Xu-zhong, LIU Yan, HU Lin-mei and CHEN Jing. Building Hierarchical Topic Based on Heterogeneous Chinese Online Encyclopedia[J]. Computer Science, 2017, 44(5): 226 -231 .
[8] LIU Yong and WEI Guang-ze. Method of Semantic Annotation Based on Chinese Framework[J]. Computer Science, 2015, 42(Z6): 98 -101 .
[9] CAO Yi-qin,ZHANG Zhen and HUANG Xiao-sheng. Multi-agent System Coalition Utility Allocation Strategy Based on Loyalty[J]. Computer Science, 2014, 41(5): 235 -238 .
[10] ZHANG Jing-min and DONG Hong-bin. Optimized Negotiation Model Based on Reinforcement Learning of Medium Agent[J]. Computer Science, 2017, 44(1): 53 -59 .