CSE_E 1.0: An integrated automated theorem prover for first-order logic

Feng Cao, Yang Xu, J. Liu, Shuwei Chen, Xinran Ning

Research output: Contribution to journalArticle

1 Downloads (Pure)

Abstract

First-order logic is an important part of mathematical logic, and automated theorem proving is an interdisciplinary field of mathematics and computer science. The paper presents an automated theorem prover for first-order logic, called CSE_E 1.0, which is a combination of two provers contradiction separation extension (CSE) and E, where CSE is based on the recently-introduced multi-clause standard contradiction separation (S-CS) calculus for first-order logic and E is the well-known equational theorem prover for first-order logic based on superposition and rewriting. The motivation of the combined prover CSE_E 1.0 is to (1) evaluate the capability, applicability and generality of CSE_E , and (2) take advantage of novel multi-clause S-CS dynamic deduction of CSE and mature equality handling of E to solve more and harder problems. In contrast to other improvements of E, CSE_E 1.0 optimizes E mainly from the inference mechanism aspect. The focus of the present work is given to the description of CSE_E including its S-CS rule, heuristic strategies, and the S-CS dynamic deduction algorithm for implementation. In terms of combination, in order not to lose the capability of E and use CSE_E to solve some hard problems which are unsolved by E, CSE_E 1.0 schedules the running of the two provers in time. It runs plain E first, and if E does not find a proof, it runs plain CSE, then if it does not find a proof, some clauses inferred in the CSE run as lemmas are added to the original clause set and the combined clause set handed back to E for further proof search. CSE_E 1.0 is evaluated through benchmarks, e.g., CASC-26 (2017) and CASC-J9 (2018) competition problems (FOFdivision). Experimental results show that CSE_E 1.0 indeed enhances the performance of E to a certain extent
Original languageEnglish
Article number1142
Pages (from-to)1
Number of pages15
JournalSymmetry
Volume11
Issue number9
Publication statusPublished - 8 Sep 2019

Fingerprint Dive into the research topics of 'CSE_E 1.0: An integrated automated theorem prover for first-order logic'. Together they form a unique fingerprint.

  • Cite this