{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,19]],"date-time":"2026-01-19T06:12:49Z","timestamp":1768803169147,"version":"3.49.0"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T00:00:00Z","timestamp":1736380800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T00:00:00Z","timestamp":1736380800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62366017"],"award-info":[{"award-number":["62366017"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62106206"],"award-info":[{"award-number":["62106206"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"General Research Project of Jiangxi Education Department","award":["GJJ200818"],"award-info":[{"award-number":["GJJ200818"]}]},{"name":"Dr. Scientific Research Fund of Jiangxi University of Science and Technology","award":["205200100060"],"award-info":[{"award-number":["205200100060"]}]},{"name":"Jiangxi Province Key Laboratory of Multidimensional Intelligent Perception and Control of China","award":["2024SSY03161"],"award-info":[{"award-number":["2024SSY03161"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Comput Intell Syst"],"DOI":"10.1007\/s44196-024-00726-y","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T15:49:33Z","timestamp":1736437773000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Novel Conflict Deduction Algorithm Based on Contradiction Separation Inference Rule"],"prefix":"10.1007","volume":"18","author":[{"given":"Hailin","family":"Guo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Feng","family":"Cao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianbing","family":"Yi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guanfeng","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weicai","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"issue":"4","key":"726_CR1","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1007\/s10817-019-09524-0","volume":"64","author":"G Moghaddam","year":"2020","unstructured":"Moghaddam, G., Padmanabhan, R., Zhang, Y.: Automated reasoning with power maps. J. Autom. Reason. 64(4), 689\u2013697 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09524-0","journal-title":"J. Autom. Reason."},{"issue":"4","key":"726_CR2","doi-asserted-by":"publisher","first-page":"818","DOI":"10.1093\/logcom\/exad013","volume":"33","author":"AH From","year":"2023","unstructured":"From, A.H., Schlichtkrull, A., Villadsen, J.: A sequent calculus for first-order logic formalized in isabelle\/hol. J. Log. Comput. 33(4), 818\u2013836 (2023). https:\/\/doi.org\/10.1093\/logcom\/exad013","journal-title":"J. Log. Comput."},{"key":"726_CR3","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L.: Symbolic computation and automated reasoning for program analysis. In: Integrated Formal Methods: 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1\u20135, 2016, Proceedings 12, pp. 20\u201327 (2016)","DOI":"10.1007\/978-3-319-33693-0_2"},{"key":"726_CR4","doi-asserted-by":"crossref","unstructured":"Gleiss, B., Suda, M.: Layered clause selection for theory reasoning: (short paper). In: Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1\u20134, 2020, Proceedings, Part I 10, pp. 402\u2013409 (2020)","DOI":"10.1007\/978-3-030-51074-9_23"},{"key":"726_CR5","doi-asserted-by":"crossref","unstructured":"Schulz, S., M\u00f6hrmann, M.: Performance of clause selection heuristics for saturation-based theorem proving. In: Automated Reasoning: 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27\u2013July 2, 2016, Proceedings 8, pp. 330\u2013345 (2016)","DOI":"10.1007\/978-3-319-40229-1_23"},{"key":"726_CR6","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/s10817-014-9301-5","volume":"53","author":"JP Bridge","year":"2014","unstructured":"Bridge, J.P., Holden, S.B., Paulson, L.C.: Machine learning for first-order theorem proving: learning to select a good heuristic. J. Autom. Reason. 53, 141\u2013172 (2014). https:\/\/doi.org\/10.1007\/s10817-014-9301-5","journal-title":"J. Autom. Reason."},{"key":"726_CR7","doi-asserted-by":"crossref","unstructured":"Reger, G., Suda, M., Voronkov, A.: Unification with abstraction and theory instantiation in saturation-based reasoning. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 3\u201322 (2018)","DOI":"10.29007\/hsh2"},{"key":"726_CR8","unstructured":"Steen, A., Sutcliffe, G., Fontaine, P., McKeown, J.: Representation, verification, and visualization of tarskian interpretations for typed first-order logic. In: LPAR 2023-24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (2023)"},{"issue":"1","key":"726_CR9","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1017\/S1755020321000198","volume":"16","author":"G Grilletti","year":"2023","unstructured":"Grilletti, G., Ciardelli, I.: Games and cardinalities in inquisitive first-order logic. Rev. Symb. Log. 16(1), 241\u2013267 (2023). https:\/\/doi.org\/10.1017\/S1755020321000198","journal-title":"Rev. Symb. Log."},{"issue":"1","key":"726_CR10","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM (JACM) 12(1), 23\u201341 (1965). https:\/\/doi.org\/10.1145\/321250.321253","journal-title":"J. ACM (JACM)"},{"key":"726_CR11","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2020.101227","volume":"67","author":"M Almakhour","year":"2020","unstructured":"Almakhour, M., Sliman, L., Samhat, A.E., Mellouk, A.: Verification of smart contracts: a survey. Pervasive Mobile Comput. 67, 101227 (2020). https:\/\/doi.org\/10.1016\/j.pmcj.2020.101227","journal-title":"Pervasive Mobile Comput."},{"key":"726_CR12","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-20(3:1)2024","author":"B Bollig","year":"2024","unstructured":"Bollig, B., Sangnier, A., Stietel, O.: On the satisfiability of local first-order logics with data. Log. Methods Comput. Sci. (2024). https:\/\/doi.org\/10.46298\/lmcs-20(3:1)2024","journal-title":"Log. Methods Comput. Sci."},{"key":"726_CR13","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: International Conference on Computer Aided Verification, pp. 1\u201335 (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"726_CR14","doi-asserted-by":"crossref","unstructured":"Schulz, S.: System description: E 1.8. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 735\u2013743 (2013)","DOI":"10.1007\/978-3-642-45221-5_49"},{"key":"726_CR15","doi-asserted-by":"crossref","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Automated Deduction\u2013CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27\u201330, 2019, Proceedings 27, pp. 495\u2013507 (2019)","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"726_CR16","doi-asserted-by":"crossref","unstructured":"Duarte, A., Korovin, K.: Implementing superposition in iprover (system description). In: Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1\u20134, 2020, Proceedings, Part II 10, pp. 388\u2013397 (2020)","DOI":"10.1007\/978-3-030-51054-1_24"},{"key":"726_CR17","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution Theorem Proving. Handbook of Automated Reasoning, vol. 1(02) (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"726_CR18","doi-asserted-by":"crossref","unstructured":"Teucke, A., Weidenbach, C.: First-order logic theorem proving and model building via approximation and instantiation. In: Frontiers of Combining Systems: 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21\u201324, 2015, Proceedings 10, pp. 85\u2013100 (2015)","DOI":"10.1007\/978-3-319-24246-0_6"},{"key":"726_CR19","unstructured":"Kotelnikov, E.: Automated theorem proving in a first-order logic with first class Boolean sort. Ph.D. thesis, Chalmers University of Technology, Gothenburg, Sweden (2016)"},{"key":"726_CR20","doi-asserted-by":"crossref","unstructured":"Rowe, R.N., F\u00e9r\u00e9e, H., Thompson, S.J., Owens, S.: Characterising renaming within Ocaml\u2019s module system: theory and implementation. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 950\u2013965 (2019)","DOI":"10.1145\/3314221.3314600"},{"key":"726_CR21","doi-asserted-by":"crossref","unstructured":"Schlichtkrull, A., Blanchette, J.C., Traytel, D.: A verified prover based on ordered resolution. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 152\u2013165 (2019)","DOI":"10.1145\/3293880.3294100"},{"key":"726_CR22","doi-asserted-by":"crossref","unstructured":"Crouse, M., Abdelaziz, I., Makni, B., Whitehead, S., Cornelio, C., Kapanipathi, P., Srinivas, K., Thost, V., Witbrock, M., Fokoue, A.: A deep reinforcement learning approach to first-order logic theorem proving. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 35, pp. 6279\u20136287 (2021)","DOI":"10.1609\/aaai.v35i7.16780"},{"key":"726_CR23","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2020.101528","volume":"105","author":"L Bellomarini","year":"2022","unstructured":"Bellomarini, L., Benedetto, D., Gottlob, G., Sallinger, E.: Vadalog: a modern architecture for automated reasoning with large knowledge graphs. Inf. Syst. 105, 101528 (2022). https:\/\/doi.org\/10.1016\/j.is.2020.101528","journal-title":"Inf. Syst."},{"key":"726_CR24","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2024.106489","volume":"186","author":"S Buss","year":"2024","unstructured":"Buss, S., Yolcu, E.: Regular resolution effectively simulates resolution. Inf. Process. Lett. 186, 106489 (2024). https:\/\/doi.org\/10.1016\/j.ipl.2024.106489","journal-title":"Inf. Process. Lett."},{"key":"726_CR25","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s10817-017-9408-6","volume":"60","author":"J Slaney","year":"2018","unstructured":"Slaney, J., Woltzenlogel Paleo, B.: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning. J. Autom. Reason. 60, 133\u2013156 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9408-6","journal-title":"J. Autom. Reason."},{"key":"726_CR26","doi-asserted-by":"crossref","unstructured":"Itegulov, D., Slaney, J., Woltzenlogel\u00a0Paleo, B.: Scavenger 0.1: a theorem prover based on conflict resolution. In: Automated Deduction\u2013CADE 26: 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6\u201311, 2017, Proceedings, pp. 344\u2013356 (2017)","DOI":"10.1007\/978-3-319-63046-5_21"},{"key":"726_CR27","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.ins.2018.04.086","volume":"462","author":"Y Xu","year":"2018","unstructured":"Xu, Y., Liu, J., Chen, S., Zhong, X., He, X.: Contradiction separation based dynamic multi-clause synergized automated deduction. Inf. Sci. 462, 93\u2013113 (2018). https:\/\/doi.org\/10.1016\/j.ins.2018.04.086","journal-title":"Inf. Sci."},{"issue":"2","key":"726_CR28","doi-asserted-by":"publisher","first-page":"1245","DOI":"10.2991\/ijcis.d.191022.002","volume":"12","author":"F Cao","year":"2019","unstructured":"Cao, F., Xu, Y., Chen, S., Zhong, J., Wu, G.: A contradiction separation dynamic deduction algorithm based on optimized proof search. Int. J. Comput. Intell. Syst. 12(2), 1245\u20131254 (2019). https:\/\/doi.org\/10.2991\/ijcis.d.191022.002","journal-title":"Int. J. Comput. Intell. Syst."},{"key":"726_CR29","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.ins.2021.03.015","volume":"566","author":"F Cao","year":"2021","unstructured":"Cao, F., Xu, Y., Liu, J., Chen, S., Yi, J.: A multi-clause dynamic deduction algorithm based on standard contradiction separation rule. Inf. Sci. 566, 281\u2013299 (2021). https:\/\/doi.org\/10.1016\/j.ins.2021.03.015","journal-title":"Inf. Sci."},{"key":"726_CR30","doi-asserted-by":"crossref","unstructured":"Xu, Y., Liu, J., Chen, S., Zhong, X.: A novel generalization of resolution principle for automated deduction. In: Uncertainty Modelling in Knowledge Engineering and Decision Making: Proceedings of the 12th International FLINS Conference, pp. 483\u2013488 (2016)","DOI":"10.1142\/9789813146976_0078"},{"key":"726_CR31","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/j.ins.2022.11.128","volume":"622","author":"P Liu","year":"2023","unstructured":"Liu, P., Xu, Y., Liu, J., Chen, S., Cao, F., Wu, G.: Fully reusing clause deduction algorithm based on standard contradiction separation rule. Inf. Sci. 622, 337\u2013356 (2023). https:\/\/doi.org\/10.1016\/j.ins.2022.11.128","journal-title":"Inf. Sci."},{"key":"726_CR32","doi-asserted-by":"publisher","DOI":"10.1016\/j.knosys.2022.110217","volume":"261","author":"P Liu","year":"2023","unstructured":"Liu, P., Chen, S., Liu, J., Xu, Y., Cao, F., Wu, G.: An efficient contradiction separation based automated deduction algorithm for enhancing reasoning capability. Knowl. Based Syst. 261, 110217 (2023). https:\/\/doi.org\/10.1016\/j.knosys.2022.110217","journal-title":"Knowl. Based Syst."},{"key":"726_CR33","doi-asserted-by":"crossref","unstructured":"Zeng, G., Xu, Y., Chen, S.: An improved contradiction separation dynamic deduction method based on complementary ratio. In: Machine Learning, Multi Agent and Cyber Physical Systems: Proceedings of the 15th International FLINS Conference (FLINS 2022), pp. 45\u201353 (2023)","DOI":"10.1142\/9789811269264_0006"},{"key":"726_CR34","doi-asserted-by":"publisher","DOI":"10.1016\/j.knosys.2023.111238","volume":"284","author":"G Zeng","year":"2024","unstructured":"Zeng, G., Chen, S., Liu, J., Xu, Y., Liu, P.: A complementary ratio based clause selection method for contradiction separation dynamic deduction. Knowl. Based Syst. 284, 111238 (2024). https:\/\/doi.org\/10.1016\/j.knosys.2023.111238","journal-title":"Knowl. Based Syst."},{"issue":"4","key":"726_CR35","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The tptp problem library and associated infrastructure. J. Autom. Reason. 59(4), 483\u2013502 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9407-7","journal-title":"J. Autom. Reason."},{"key":"726_CR36","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G.: The cade-26 automated theorem proving system competition-casc-26. AI Commun. 30(6), 419\u2013432 (2017). https:\/\/doi.org\/10.3233\/AIC-170744","DOI":"10.3233\/AIC-170744"},{"issue":"1\u20132","key":"726_CR37","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","volume":"131","author":"G Sutcliffe","year":"2001","unstructured":"Sutcliffe, G., Suttner, C.: Evaluating general purpose automated theorem proving systems. Artif. Intell. 131(1\u20132), 39\u201354 (2001). https:\/\/doi.org\/10.1016\/S0004-3702(01)00113-8","journal-title":"Artif. Intell."}],"container-title":["International Journal of Computational Intelligence Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s44196-024-00726-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s44196-024-00726-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s44196-024-00726-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T16:23:10Z","timestamp":1736439790000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s44196-024-00726-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,9]]},"references-count":37,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2025,12]]}},"alternative-id":["726"],"URL":"https:\/\/doi.org\/10.1007\/s44196-024-00726-y","relation":{},"ISSN":["1875-6883"],"issn-type":[{"value":"1875-6883","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,9]]},"assertion":[{"value":"12 November 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 December 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 January 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"4"}}