Application of Multi-Clause Synergized Deduction in First-Order Logic Automated Theorem Proving

CAO Feng; XU Yang; CHEN Shuwei; WU Guanfeng; CHANG Wenjing

doi:10.3969/j.issn.0258-2724.20180800

Volume 55 Issue 2

Mar. 2020

Turn off MathJax

Article Contents

Abstract

References

Journal of Southwest Jiaotong University > 2020 > 55(2): 401-408, 427.

CAO Feng, XU Yang, CHEN Shuwei, WU Guanfeng, CHANG Wenjing. Application of Multi-Clause Synergized Deduction in First-Order Logic Automated Theorem Proving[J]. Journal of Southwest Jiaotong University, 2020, 55(2): 401-408, 427. doi: 10.3969/j.issn.0258-2724.20180800

Citation:

CAO Feng, XU Yang, CHEN Shuwei, WU Guanfeng, CHANG Wenjing. Application of Multi-Clause Synergized Deduction in First-Order Logic Automated Theorem Proving[J]. Journal of Southwest Jiaotong University, 2020, 55(2): 401-408, 427. doi: 10.3969/j.issn.0258-2724.20180800

Citation:

PDF( 708 KB)

Application of Multi-Clause Synergized Deduction in First-Order Logic Automated Theorem Proving

doi: 10.3969/j.issn.0258-2724.20180800

CAO Feng^{1,2
,},
XU Yang^2,3,
CHEN Shuwei^2,3,
WU Guanfeng^{2,3
,
,},
CHANG Wenjing^1,2

Received Date: 11 Sep 2018
Rev Recd Date: 01 Apr 2019

Available Online: 30 May 2019

Publish Date: 01 Apr 2020

Abstract

Abstract

First-order logic is an important branch in mathematical logic, and automated reasoning of its logical formula is one of the important research hotspots in the field of artificial intelligence. Most of the state of the art first-order logic automated theorem proving systems adopt binary resolution method. There are only two clauses involved, and therefore only a complementary pair of literals are eliminated during each resolution step. As a consequence, the resulted clause has many literals, which affects the deduction efficiency. In this paper, a multi-clause synergized deduction algorithm is proposed based on contradiction separation rule. This algorithm allows multiple clauses used in deduction, and is able to eliminate more than one complementary pairs. The clause of contradiction separation is controllable and usually has less literals, which can effectively improve the inference ability. This multi-clause synergized algorithm adjusts the deduction order of clauses according to two kinds of weights, effective deduction weight and ineffective deduction weight. Backtracking mechanism is used to search for an optimal path, and effectively plan the deduction path. The algorithm is applied to the international top prover－Eprover 2.1, and Conference on Automated Deduction 2017 competition theorems (FOF division) are set as the test object. Eprover 2.1 with multi-clause synergized deduction algorithm outperformed Eprover 2.1 and solved 8 theorems more than Eprover 2.1. It also solved 31 theorems out of the 110 theorems unsolved by Eprover 2.1, accounting for 28.2% of the total.
- mathematical logic,
- artificial intelligence,
- theorem proving,
- binary resolution,
- contradiction separation rule

FullText(HTML)

References(27)

References

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.

DAVIS M. The early history of automated deduction[J]. Handbook of Automated Reasoning, 2002, 714(3): 5-15.

PLAISTED D A. History and prospects for first-order automated deduction[C]//Proceedings of 25th International Conference on Automated Deduction. Cham: Springer, 2015: 3-28.

ROBINSON J A. The generalized resolution principle[M]//SIEKMANN J, WRIGHTSON G. Automation of Reasoning-3. Berlin Heidelberg: Springer International Publishing, 1983: 135-151.

RUBIN N, HARRISON M C. Another generalization of resolution[J]. Journal of the Association for Computing Machinery, 1978, 25(3): 341-351. doi: 10.1145/322077.322078

LU Ruzhan, LIN Kai, SUN Yongqiang. Colored resolution,pi-colored clash and its completeness[J]. Journal of Computer, 1987, 12: 18-25.

LOVELAND D W. A linear format for resolution[C]//Symposium on Automatic Demonstration. Berlin: Springer, 1970: 147-162.

LUCKHAM D. Refinements in resolution theory[C]//Symposium on Automatic Demonstration. Berlin: Springer, 1970: 163-190.

OVERBEEK R, MCCHAREN J, WOS L. Complexity and related enhancements for automated theorem-proving programs[J]. Computers & Mathematics with Applications, 1976, 2(1): 1-16.

ROBINSON J A. Automatic deduction with hyper-resolution[J]. International Journal of Computing & Mathematics, 1965, 1(3): 227-234.

SLANEY J, PALEO B W. Conflict resolution:a first-order resolution calculus with decision literals and conflict-driven clause learning[J]. Journal of Automated Reasoning, 2016, 12(4): 1-24.

RIAZANOV A, VORONKOV A. The design and implementation of vampire[J]. Ai Communications, 2002, 15(2): 91-110.

VORONKOV A. First-order theorem proving and vampire[C]//Proceedings of International Conference on Computer Aided Verification. Berlin: Springer-Verlag, 2013: 1-35.

SCHULZ S. E-a brainiac theorem prover[J]. AI Com- munications, 2002, 15(2): 111-126.

SCHULZ S. System description: E 1.8[C]//Proceedings of 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Berlin: Springer-Verlag, 2013: 735-743.

BAUMGARTNER P, BAX J, WALDMANN U. Beagle－a hierarchic superposition theorem prover[C]// Proceedings of 25th International Conference on Automated Deduction. Cham: Springer, 2015: 367-377.

WEIDENBACH C, BRAHM U, HILLENBRAND T, et al. Spass version 2.0[C]//Proceedings of International Conference on Automated Deduction. Berlin: Springer-Verlag, 2002: 275-279.

VORONKOV A. AVATAR: The architecture for first-order theorem provers[C]//Proceedings of International Conference on Computer Aided Verification. Cham: Springer, 2014: 696-710.

DENZINGER J, KRONENBURG M, SCHULZ S. DISCOUNT-a distributed and learning equational prover[J]. Journal of Automated Reasoning, 1997, 18(2): 189-198. doi: 10.1023/A:1005879229581

MCCUNE W, WOS L. Otter-the CADE-13 competition incarnations[J]. Journal of Automated Reasoning, 1997, 18(2): 211-220. doi: 10.1023/A:1005843632307

REGER G, TISHKOVSKY D, VORONKOV A. Cooperating proof attempts[C]//Proceedings of 25th International Conference on Automated Deduction. Cham: Springer, 2015: 339-355.

SCHULZ S, MOHNMANN M. Performance of clause selection heuristics for saturation-based theorem proving[C]//Proceedings of 8th International Joint Conference. Cham: Springer, 2016: 330-345.

HODER K, REGER G, SUDA M, et al. Selecting the selection[C]//Proceedings of 8th International Joint Conference on Automated Reasoning. Cham: Springer, 2016: 313-329.

XU Yang, LIU Jun, CHEN Shuwei, et al. Contradiction separation based dynamic multi-clause synergized automated deduction[J]. Information Sciences, 2018, 462(5): 93-113.

XU Yang, LIU Jun, CHEN Shuwei, et al. Distinctive features of the contradiction separation based dynamic automated deduction[C]//Proceedings of 13th International FLINS Conference on Decision Making and Soft Computing. Belfast: World Scientific, 2018: 725-732.

SUTCLIFFE.G.The 7th IJCAR automated theorem proving system competition-CASC-J7[J]. AI Communications, 2015, 28(4): 683-692. doi: 10.3233/AIC-150668

SUTCLIFFE.G.The 8th IJCAR automated theorem proving system competition-CASC-J8[J]. AI Communications, 2016, 29(5): 607-619. doi: 10.3233/AIC-160709

Relative Articles

[1]	ZENG Guoyan, XU Yang, CHEN Shuwei, JIANG Shipan. First-Order Logic Clause Selection Method Based on Multi-criteria Decision Making[J]. Journal of Southwest Jiaotong University, 2025, 60(1): 185-193. doi: 10.3969/j.issn.0258-2724.20230023
[2]	WANG Zhonghao, GUO Xifeng, YANG Xingyu. Bearing Capacity Evaluation of Tunnel-Type Anchorage Based on Artificial Intelligent Algorithm[J]. Journal of Southwest Jiaotong University, 2021, 56(3): 534-540. doi: 10.3969/j.issn.0258-2724.20200165
[3]	WANG Keming, WANG Xia, CHENG Peng, LIU Ning, ZHANG Chuandong. Formal Method for Behavior Verification and Data Validation of Station Interlocking System[J]. Journal of Southwest Jiaotong University, 2021, 56(3): 587-593, 610. doi: 10.3969/j.issn.0258-2724.20191182
[4]	ZHU Jun, HU Ya, CAO Yungang, GUO Fangtao. Design and Implementation of Mobile Agent-Based Spatial Information Sharing Service[J]. Journal of Southwest Jiaotong University, 2011, 24(3): 427-433. doi: 10.3969/j.issn.0258-2724.2011.03.012
[5]	CHEN Xiaoqing, ZHAO Wanyu, GAOQuan, JIAShitao, ZHU Xinghua. Experimental Investigation and Design of Artificial Structures Controlling Dam-Break Floods[J]. Journal of Southwest Jiaotong University, 2011, 24(2): 228-234. doi: 10.3969/j.issn.0258-2724.2011.02.009
[6]	GAO Hongli, LI Dengwan, XU Mingheng. Intelligent Monitoring System for Screw Life Evaluation[J]. Journal of Southwest Jiaotong University, 2010, 23(5): 685-691. doi: 10.3969/j.issn.0258-2724.2010.05.006
[7]	CHEN Shuwei, XU Yang. Rules of Inference in Lattice-Valued Propositional Logic Lvpl[J]. Journal of Southwest Jiaotong University, 2006, 19(2): 256-258.
[8]	YANG Yi-ren, LIU Fei. Complex Response of an Airfoil-Store System with Structural Non-Linearity[J]. Journal of Southwest Jiaotong University, 2006, 19(1): 7-10,24.
[9]	WANG Wei, JIANG Bao-qing, XU Yang. α-Resolution Fields ofGeneralized Literals ofLogic LP(X)[J]. Journal of Southwest Jiaotong University, 2005, 18(4): 544-547.
[10]	LIUWen-li. Nernst Theorem and Entropy ofTwo DimensionalBlack Holes[J]. Journal of Southwest Jiaotong University, 2005, 18(4): 558-561.
[11]	XUGao. Simulation Model for Crowd Evacuation Based on Agent Technology[J]. Journal of Southwest Jiaotong University, 2003, 16(3): 301-303.
[12]	MENG Dan, SONG Zhen-ming, QIN Ke-yun. Algorithm of Transforming Any Formula in LF(X)into Reducible Form[J]. Journal of Southwest Jiaotong University, 2003, 16(4): 433-437.
[13]	GONGHui, QIANG Shiz-hong. Maximum Superiority Searching Method[J]. Journal of Southwest Jiaotong University, 2001, 14(3): 286-290.
[14]	PANWU-Ming, XUYANG, LITIAN-Rui. KnowledgeRePresentationandReasoningonPatternClasses[J]. Journal of Southwest Jiaotong University, 2001, 14(4): 437-439.
[15]	Yan Jifu, Li Zhi, Xiao Tijing. Application of New Binary Model Structure in Power Electronic Circuits Simulation[J]. Journal of Southwest Jiaotong University, 1999, 12(3): 305-309.

Supplements(0)

Cited By

Cited by

Periodical cited type(6)

1.	曾国艳，徐扬，陈树伟，姜世攀. 基于多属性决策的一阶逻辑子句选择方法. 西南交通大学学报. 2025(01): 185-193 . 本站查看
2.	曹锋，杨小玲，易见兵，李俊. 矛盾体分离超演绎方法及应用. 计算机应用. 2024(10): 3074-3080 .
3.	曹锋，谢燏，易见兵，李俊. 矛盾体分离单元结果演绎方法及应用. 计算机工程与科学. 2024(12): 2252-2260 .
4.	黄海，桂起权. 基于人工智能的多Agent协同辩证逻辑推理方法. 逻辑学研究. 2023(05): 81-96 .
5.	林玲瑜，曹锋，易见兵，方旺盛，李俊，吴贯锋. 基于子句活跃度和复杂度的多元动态演绎算法及应用. 计算机工程与科学. 2023(12): 2256-2264 .
6.	唐雷明，白沐尘，何星星，黎兴玉. 基于命题逻辑的完全标准矛盾体及最小标准矛盾体. 计算机科学. 2020(S2): 83-85+105 .

Other cited types(3)

Proportional views

Proportional views

通讯作者: 陈斌, bchen63@163.com

1.
沈阳化工大学材料科学与工程学院沈阳 110142

Figures(3) / Tables(2)

Get Citation

PDF

XML

Article views(618) PDF downloads(15)