{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T22:58:28Z","timestamp":1773442708604,"version":"3.50.1"},"reference-count":42,"publisher":"MDPI AG","issue":"9","license":[{"start":{"date-parts":[[2019,9,8]],"date-time":"2019-09-08T00:00:00Z","timestamp":1567900800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Symmetry"],"abstract":"<jats:p>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     C S E _ 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     C S E _ E     1.0 is to (1) evaluate the capability, applicability and generality of     C S E _ 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,     C S E _ E     1.0 optimizes E mainly from the inference mechanism aspect. The focus of the present work is given to the description of     C S E _ 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     C S E _ E     to solve some hard problems which are unsolved by E,     C S E _ 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.     C S E _ E     1.0 is evaluated through benchmarks, e.g., CASC-26 (2017) and CASC-J9 (2018) competition problems (FOFdivision). Experimental results show that     C S E _ E     1.0 indeed enhances the performance of E to a certain extent.<\/jats:p>","DOI":"10.3390\/sym11091142","type":"journal-article","created":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T04:12:40Z","timestamp":1568002360000},"page":"1142","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["CSE_E 1.0: An Integrated Automated Theorem Prover for First-Order Logic"],"prefix":"10.3390","volume":"11","author":[{"given":"Feng","family":"Cao","sequence":"first","affiliation":[{"name":"School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610031, China"},{"name":"National-Local Joint Engineering Lab of System Credibility Automatic Verification, Chengdu 610031, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Xu","sequence":"additional","affiliation":[{"name":"National-Local Joint Engineering Lab of System Credibility Automatic Verification, Chengdu 610031, China"},{"name":"School of Mathematics, Southwest Jiaotong University, Chengdu 610031, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Liu","sequence":"additional","affiliation":[{"name":"National-Local Joint Engineering Lab of System Credibility Automatic Verification, Chengdu 610031, China"},{"name":"School of Computing, Ulster University, Belfast BT37 0QB , Northern Ireland, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shuwei","family":"Chen","sequence":"additional","affiliation":[{"name":"National-Local Joint Engineering Lab of System Credibility Automatic Verification, Chengdu 610031, China"},{"name":"School of Mathematics, Southwest Jiaotong University, Chengdu 610031, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xinran","family":"Ning","sequence":"additional","affiliation":[{"name":"School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610031, China"},{"name":"National-Local Joint Engineering Lab of System Credibility Automatic Verification, Chengdu 610031, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2019,9,8]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","unstructured":"Pavlov, V., Schukin, A., and Cherkasova, T. (2013, January 7\u20139). Exploring Automated Reasoning in First-Order Logic: Tools, Techniques and Application Areas. Proceedings of the 4th International Conference on Knowledge Engineering and the Semantic Web, St. Petersburg, Russia.","DOI":"10.1007\/978-3-642-41360-5_9"},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Kovacs, L., and Voronkov, A. (2009, January 22\u201329). Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering, York, UK.","DOI":"10.1007\/978-3-642-00593-0_33"},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/s10817-018-9459-3","article-title":"Amortized Complexity Verified","volume":"62","author":"Nipkow","year":"2019","journal-title":"J. Autom. Reason."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","article-title":"The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0","volume":"59","author":"Sutcliffe","year":"2017","journal-title":"J. Autom. Reason."},{"key":"ref_5","unstructured":"(2019, May 16). TSTP Solution Domains. Available online: http:\/\/www.tptp.org\/cgi-bin\/SeeTPTP?Category=Solutions."},{"key":"ref_6","unstructured":"(2019, May 16). CASC Solution Domains. Available online: http:\/\/tptp.org\/CASC\/."},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. ACM"},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., and Snyder, W. (1992, January 15\u201318). Basic paramodulation and superposition. Proceedings of the 11th International Conference on Automated Deduction, New York, NY, USA.","DOI":"10.1007\/3-540-55602-8_185"},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Siekmann, J.H., and Wrightson, G. (1983). A linear format for resolution. Automation of Reasoning 2: Classical Papers on Computational Logic, Springer.","DOI":"10.1007\/978-3-642-81955-1"},{"key":"ref_10","unstructured":"Siekmann, J.H., and Wrightson, G. (1970). The unit proof and the input proof in theorem proving. Automation of Reasoning 2: Classical Papers on Computational Logic, Springer."},{"key":"ref_11","first-page":"227","article-title":"Automatic deduction with hyper-resolution","volume":"1","author":"Robinson","year":"1965","journal-title":"Int. J. Comput. Math."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0898-1221(76)90002-X","article-title":"Complexity and related enhancements for automated theorem-proving programs","volume":"2","author":"Overbeek","year":"1976","journal-title":"Comput. Math. Appl."},{"key":"ref_13","first-page":"1","article-title":"Conflict resolution: A first-order resolution calculus with decision literals and conflict-driven clause learning","volume":"12","author":"Slaney","year":"2016","journal-title":"J. Autom. Reason."},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Reger, G., and Tishkovsky, D. (2015, January 1\u20137). Cooperating Proof Attempts. Proceedings of the 25th International Conference on Automated Deduction, Berlin, Germany.","DOI":"10.1007\/978-3-319-21401-6_23"},{"key":"ref_15","unstructured":"Schulz, S., and M\u00f6hrmann, M. (July, January 27). Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving. Proceedings of the 8th International Joint Conference on Automated Reasoning, Coimbra, Portugal."},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","article-title":"Lightweight relevance filtering for machine-generated resolution problems","volume":"7","author":"Meng","year":"2009","journal-title":"J. Appl. Log."},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Chvalovsk\u00fd, K., Jakub\u016fv, J., Suda, M., and Urban, J. (2019, January 27\u201330). ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. Proceedings of the 27th International Conference on Automated Deduction, Natal, Brazil.","DOI":"10.1007\/978-3-030-29436-6_12"},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Furbach, U., Kr\u00e4mer, T., and Schon, C. (2019, January 27\u201330). Names Are Not Just Sound and Smoke: Word Embeddings for Axiom Selection. Proceedings of the 27th International Conference on Automated Deduction, Natal, Brazil.","DOI":"10.1007\/978-3-030-29436-6_15"},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Rawson, M., and Reger, G. (2019, January 27\u201330). Old or Heavy? Decaying Gracefully with Age\/Weight Shapes. Proceedings of the 27th International Conference on Automated Deduction, Natal, Brazil.","DOI":"10.1007\/978-3-030-29436-6_27"},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Piotrowski, B., and Urban, J. (2018, January 14\u201317). ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback. Proceedings of the 9th International Joint Conference on Automated Reasoning, Oxford, UK.","DOI":"10.1007\/978-3-319-94205-6_37"},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/j.ins.2018.04.086","article-title":"Contradiction separation based dynamic multi-clause synergised automated deduction","volume":"462","author":"Xu","year":"2018","journal-title":"Inf. Sci."},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Xu, Y., Chen, S.W., Liu, J., Zhong, X.M., and He, X.X. (2018, January 21\u201324). Distinctive features of the contradiction separation based dynamic automated deduction. Proceedings of the 13th International FLINS Conference, Belfast, UK.","DOI":"10.1142\/9789813273238_0092"},{"key":"ref_23","unstructured":"Schulz, S. (2013, January 14\u201319). System description: E 1.8. Proceedings of the 19th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Stellenbosch, South Africa."},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"683","DOI":"10.3233\/AIC-150668","article-title":"The 7th IJCAR Automated Theorem Proving System Competition-CASC-J7","volume":"28","author":"Sutcliffe","year":"2015","journal-title":"AI Commun."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"607","DOI":"10.3233\/AIC-160709","article-title":"The 8th IJCAR Automated Theorem Proving System Competition-CASC-J8","volume":"29","author":"Sutcliffe","year":"2016","journal-title":"AI Commun."},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"495","DOI":"10.3233\/AIC-180773","article-title":"The 9th IJCAR Automated Theorem Proving System Competition-CASC-J9","volume":"31","author":"Sutcliffe","year":"2018","journal-title":"AI Commun."},{"key":"ref_27","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Schulz, S., Urban, J., and Vysko\u010dil, J. (2015, January 1\u20137). System Description: E.T. 0.1. Proceedings of the 25th International Conference on Automated Deduction, Berlin, Germany.","DOI":"10.1007\/978-3-319-21401-6_27"},{"key":"ref_28","unstructured":"K\u00fchlwein, D., Schulz, S., and Urban, J. (2013, January 9\u201314). E-MaLeS 1.1. Proceedings of the 24th International Conference on Automated Deduction, New York, NY, USA."},{"key":"ref_29","first-page":"91","article-title":"MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers","volume":"55","author":"Daniel","year":"2013","journal-title":"J. Autom. Reason."},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1023\/A:1005879229581","article-title":"DISCOUNT\u2014A distributed and learning equational prover","volume":"18","author":"Denzinger","year":"1997","journal-title":"J. Autom. Reason."},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1023\/A:1005843632307","article-title":"Otter\u2014The CADE-13 competition incarnations","volume":"18","author":"Mccune","year":"1997","journal-title":"J. Autom. Reason."},{"key":"ref_32","first-page":"91","article-title":"The design and implementation of vampire","volume":"15","author":"Riazanov","year":"2002","journal-title":"AI Commun."},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., and Voronkov, A. (2013, January 13\u201319). First-order theorem proving and vampire. Proceedings of the 25th International Conference on Computer Aided Verification, Saint Petersburg, Russia.","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"ref_34","unstructured":"BiereIoan, A., Kov\u00e1cs, D., and Voronkov, A. (2014, January 16\u201322). Experimenting with SAT solvers in Vampire. Proceedings of the 13th Mexican International Conference on Artificial Intelligence, Tuxtla Guti\u00e9rrez, Mexico."},{"key":"ref_35","first-page":"111","article-title":"E\u2014A brainiac theorem prover","volume":"15","author":"Schulz","year":"2002","journal-title":"AI Commun."},{"key":"ref_36","unstructured":"Korovin, K. (2008, January 12\u201315). iProver\u2014An Instantiation-Based Theorem Prover for First-Order Logic (System Description). Proceedings of the 4th International Joint Conference on Automated Reasoning, Sydney, Australia."},{"key":"ref_37","doi-asserted-by":"crossref","unstructured":"Menouer, T., and Baarir, S. (2017, January 6\u20138). Parallel Satisfiability Solver Based on Hybrid Partitioning Method. Proceedings of the 25th Euromicro International Conference on Parallel, Distributed and Network-Based Processing, Saint Petersburg, Russia.","DOI":"10.1109\/PDP.2017.70"},{"key":"ref_38","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/s10817-009-9127-8","article-title":"Formalization and implementation of modern SAT solvers","volume":"43","author":"Maric","year":"2009","journal-title":"J. Autom. Reason."},{"key":"ref_39","doi-asserted-by":"crossref","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., and Czarnecki, K. (2016, January 5\u20138). Learning Rate Based Branching Heuristic for SAT Solvers. Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing, Bordeaux, France.","DOI":"10.1007\/978-3-319-40970-2_9"},{"key":"ref_40","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L.T., and Malik, S. (2001, January 18\u201322). Chaff: Engineering an efficient SAT solver. Proceedings of the 38th Design Automation Conference, Las Vegas, NV, USA.","DOI":"10.1145\/378239.379017"},{"key":"ref_41","doi-asserted-by":"crossref","unstructured":"Lauwereins, R., and Madsen, J. (2008). BerkMin: A Fast and Robust Sat-Solver. Design, Automation, and Test in Europe, Springer.","DOI":"10.1007\/978-1-4020-6488-3"},{"key":"ref_42","doi-asserted-by":"crossref","first-page":"250","DOI":"10.2991\/ijcis.2018.125905645","article-title":"A Hybrid Learnt Clause Evaluation Algorithm for SAT Problem","volume":"12","author":"Wu","year":"2018","journal-title":"Int. J. Comput. Intell. Syst."}],"container-title":["Symmetry"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-8994\/11\/9\/1142\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T13:17:45Z","timestamp":1760188665000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-8994\/11\/9\/1142"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,8]]},"references-count":42,"journal-issue":{"issue":"9","published-online":{"date-parts":[[2019,9]]}},"alternative-id":["sym11091142"],"URL":"https:\/\/doi.org\/10.3390\/sym11091142","relation":{},"ISSN":["2073-8994"],"issn-type":[{"value":"2073-8994","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,9,8]]}}}