{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T08:07:18Z","timestamp":1773821238197,"version":"3.50.1"},"reference-count":51,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"DOI":"10.13039\/501100004536","name":"Southwest Jiaotong University","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004536","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"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62206227"],"award-info":[{"award-number":["62206227"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Engineering Applications of Artificial Intelligence"],"published-print":{"date-parts":[[2026,1]]},"DOI":"10.1016\/j.engappai.2025.113073","type":"journal-article","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T06:24:41Z","timestamp":1763187881000},"page":"113073","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"P4","title":["Multilayer inverse dynamic deduction algorithm of standard contradiction separation rule based on parallel mechanism"],"prefix":"10.1016","volume":"163","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-8790-5057","authenticated-orcid":false,"given":"Guoyan","family":"Zeng","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8449-974X","authenticated-orcid":false,"given":"Guanfeng","family":"Wu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6748-1924","authenticated-orcid":false,"given":"Shuwei","family":"Chen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4931-2692","authenticated-orcid":false,"given":"Peiyao","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Xu","sequence":"additional","affiliation":[]},{"given":"Jian","family":"Zhong","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"2","key":"10.1016\/j.engappai.2025.113073_bib1","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","article-title":"Resolution theorem proving","volume":"1","author":"Bachmair","year":"2001","journal-title":"Handbook of Automated Reasoning"},{"key":"10.1016\/j.engappai.2025.113073_bib2","series-title":"Handbook of Satisfiability","first-page":"131","article-title":"Conflict-driven clause learning SAT solvers","author":"Biere","year":"2009"},{"issue":"1","key":"10.1016\/j.engappai.2025.113073_bib3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00881910","article-title":"Parallelization of deduction strategies: an analytical study","volume":"13","author":"Bonacina","year":"1994","journal-title":"J. Autom. Reasoning."},{"issue":"9","key":"10.1016\/j.engappai.2025.113073_bib4","doi-asserted-by":"crossref","first-page":"1142","DOI":"10.3390\/sym11091142","article-title":"CSE_E 1.0: an integrated automated theorem prover for first-order logic","volume":"11","author":"Cao","year":"2019","journal-title":"Symmetry"},{"key":"10.1016\/j.engappai.2025.113073_bib5","series-title":"2017 12th International confere-nce on Intelligent Systems and Knowledge Engineering (ISKE)","first-page":"1","article-title":"Some synergized clause selection strategies for contradiction separation based automated deduction","author":"Chen","year":"2017"},{"key":"10.1016\/j.engappai.2025.113073_bib6","series-title":"Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007)","first-page":"7","article-title":"Verification of C programs using automated reasoning","author":"Crocker","year":"2007"},{"key":"10.1016\/j.engappai.2025.113073_bib7","series-title":"21st International Conference on Types for Proofs and Programs","first-page":"67","article-title":"Pi-Ware: hardware description and verification in Agda","author":"Flor","year":"2016"},{"key":"10.1016\/j.engappai.2025.113073_bib8","series-title":"International Joint Conference on Automated Reasoning","first-page":"408","article-title":"Make E smart again (short paper)","author":"Goertzel","year":"2020"},{"issue":"1","key":"10.1016\/j.engappai.2025.113073_bib9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s44196-024-00726-y","article-title":"A novel conflict deduction algorithm based on contradiction separation inference rule","volume":"18","author":"Guo","year":"2025","journal-title":"Int. J. Comput. Intell. Syst."},{"key":"10.1016\/j.engappai.2025.113073_bib10","author":"Hajdu"},{"key":"10.1016\/j.engappai.2025.113073_bib11","series-title":"Handbook of Practical Logic and Automated Reasoning","author":"Harrison","year":"2009"},{"key":"10.1016\/j.engappai.2025.113073_bib12","article-title":"Machine learning for quantifier selection in cvc5","author":"Jakub\u016fv","year":"2024","journal-title":"arXiv preprint arXiv:2408.14338"},{"issue":"1","key":"10.1016\/j.engappai.2025.113073_bib13","doi-asserted-by":"crossref","first-page":"82","DOI":"10.3724\/SP.J.1001.2012.04101","article-title":"Overview on mechanized theorem proving","volume":"31","author":"Jiang","year":"2020","journal-title":"J. Softw."},{"issue":"3","key":"10.1016\/j.engappai.2025.113073_bib14","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","article-title":"Mizar 40 for mizar 40","volume":"55","author":"Kaliszyk","year":"2015","journal-title":"J. Autom. Reasoning."},{"key":"10.1016\/j.engappai.2025.113073_bib15","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1016\/j.jmateco.2016.06.005","article-title":"An introduction to mechanized reasoning","volume":"66","author":"Kerber","year":"2016","journal-title":"J. Math. Econ."},{"key":"10.1016\/j.engappai.2025.113073_bib16","series-title":"International Joint Conference on Automated Reasoning","first-page":"292","article-title":"iProver\u2013an instantiation-based theorem prover for first-order logic (system description)","author":"Korovin","year":"2008"},{"key":"10.1016\/j.engappai.2025.113073_bib17","series-title":"International Conference on Computer Aided Verification","first-page":"1","article-title":"First-order theorem proving and vampire","author":"Kov\u00e1cs","year":"2013"},{"issue":"3\u20134","key":"10.1016\/j.engappai.2025.113073_bib18","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","article-title":"Linear resolution with selection function","volume":"2","author":"Kowalski","year":"1971","journal-title":"Artif. Intell."},{"issue":"1","key":"10.1016\/j.engappai.2025.113073_bib19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00245018","article-title":"What is the inverse method?","volume":"5","author":"Lifschitz","year":"1989","journal-title":"J. Autom. Reasoning."},{"issue":"2","key":"10.1016\/j.engappai.2025.113073_bib20","doi-asserted-by":"crossref","first-page":"1793","DOI":"10.1007\/s10489-021-02469-1","article-title":"Axiom selection over large theory based on new first-order formula metrics","volume":"52","author":"Liu","year":"2022","journal-title":"Appl. Intell."},{"key":"10.1016\/j.engappai.2025.113073_bib21","doi-asserted-by":"crossref","DOI":"10.1016\/j.knosys.2022.110217","article-title":"An efficient contradiction separation based automated deduction algorithm for enhancing reasoning capability","volume":"261","author":"Liu","year":"2023","journal-title":"Knowl. Base Syst."},{"key":"10.1016\/j.engappai.2025.113073_bib22","series-title":"Parallelization in Inference Systems","first-page":"139","article-title":"Experiments with ROO, a parallel automated deduction system","author":"Lusk","year":"2005"},{"key":"10.1016\/j.engappai.2025.113073_bib23","series-title":"Doklady Akademii Nauk","first-page":"17","article-title":"An inverse method of establishing deducibility in the classical predicate calculus","author":"Maslov","year":"1964"},{"key":"10.1016\/j.engappai.2025.113073_bib24","article-title":"Otter 3.0 reference manual and guide","author":"McCune","year":"1994","journal-title":"Argonne Nat. Lab"},{"key":"10.1016\/j.engappai.2025.113073_bib25","first-page":"127","article-title":"The inverse method and first-order logic theorem proving","volume":"20","author":"Pavlov","year":"2014","journal-title":"Nonlinear Dyn. Appl."},{"issue":"2","key":"10.1016\/j.engappai.2025.113073_bib26","first-page":"181","article-title":"The inverse method application for non-classical logics. Nonlinear Phenom","volume":"18","author":"Pavlov","year":"2015","journal-title":"Complex Syst."},{"key":"10.1016\/j.engappai.2025.113073_bib27","series-title":"International Symposium on Frontiers of Combining Systems","first-page":"40","article-title":"A neurally-guided, parallel theorem prover","author":"Rawson","year":"2019"},{"key":"10.1016\/j.engappai.2025.113073_bib28","unstructured":"Reger, G., 2023. The source of Vampire downloaded on 2023. https:\/\/vprover.github.io\/download.html. (Accessed 7 October 2023)."},{"issue":"1","key":"10.1016\/j.engappai.2025.113073_bib29","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"},{"issue":"3","key":"10.1016\/j.engappai.2025.113073_bib30","first-page":"227","article-title":"Automatic deduction with hyper-resolution","volume":"1","author":"Robinson","year":"1965","journal-title":"Int. J. Comput. Math."},{"key":"10.1016\/j.engappai.2025.113073_bib31","series-title":"International Conference on Logic for Programming Artificial Intelligence and Reasoning","first-page":"735","article-title":"System description: e 1.8","author":"Schulz","year":"2013"},{"key":"10.1016\/j.engappai.2025.113073_bib32","author":"Schulz"},{"issue":"4","key":"10.1016\/j.engappai.2025.113073_bib33","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1145\/321420.321428","article-title":"Automatic theorem proving with renamable and semantic resolution","volume":"14","author":"Slagle","year":"1967","journal-title":"J. ACM"},{"key":"10.1016\/j.engappai.2025.113073_bib34","series-title":"International Conference on Automated Deduction","first-page":"28","article-title":"Parallelizing the closure computation in automated deduction","author":"Slaney","year":"1990"},{"issue":"2","key":"10.1016\/j.engappai.2025.113073_bib35","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/s10817-017-9408-6","article-title":"Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning","volume":"60","author":"Slaney","year":"2018","journal-title":"J. Autom. Reasoning."},{"key":"10.1016\/j.engappai.2025.113073_bib36","series-title":"International Joint Conference on Automated Reasoning","first-page":"659","article-title":"Vampire getting noisy: will random bits help conquer chaos?(system description)","author":"Suda","year":"2022"},{"issue":"4","key":"10.1016\/j.engappai.2025.113073_bib37","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. Reasoning."},{"key":"10.1016\/j.engappai.2025.113073_bib38","series-title":"International Joint Conference on Automated Reasoning","first-page":"30","article-title":"Stepping stones in the TPTP world","author":"Sutcliffe","year":"2024"},{"issue":"4","key":"10.1016\/j.engappai.2025.113073_bib39","doi-asserted-by":"crossref","first-page":"259","DOI":"10.3233\/AIC-210235","article-title":"The CADE-28 automated theorem proving system competition\u2013CASC-28","volume":"34","author":"Sutcliffe","year":"2022","journal-title":"AI Commun."},{"issue":"2","key":"10.1016\/j.engappai.2025.113073_bib40","doi-asserted-by":"crossref","first-page":"73","DOI":"10.3233\/AIC-220244","article-title":"The 11th IJCAR automated theorem proving system competition\u2013CASC-J11","volume":"36","author":"Sutcliffe","year":"2023","journal-title":"AI Commun."},{"issue":"4","key":"10.1016\/j.engappai.2025.113073_bib41","doi-asserted-by":"crossref","first-page":"485","DOI":"10.3233\/AIC-230325","article-title":"The CADE-29 automated theorem proving system competition\u2013CASC-29","volume":"37","author":"Sutcliffe","year":"2024","journal-title":"AI Commun."},{"key":"10.1016\/j.engappai.2025.113073_bib42","series-title":"Kurt G\u00f6del Colloquium on Computational Logic and Proof Theory","first-page":"65","article-title":"Resolution, inverse method and the sequent calculus","author":"Tammet","year":"1997"},{"key":"10.1016\/j.engappai.2025.113073_bib43","series-title":"International Conference on Automated Deduction","first-page":"538","article-title":"GKC: a reasoning system for large knowledge bases","author":"Tammet","year":"2019"},{"key":"10.1016\/j.engappai.2025.113073_bib44","series-title":"Proceedings of 25th Conference on Logic for Pro","first-page":"106","article-title":"Waste reduction: experiments in sharing clauses between runs of a portfolio of strategies (Experimental Paper)","author":"Tammet","year":"2024"},{"key":"10.1016\/j.engappai.2025.113073_bib45","series-title":"International Congress on Mathematical Software","first-page":"155","article-title":"Evaluation of automated theorem proving on the Mizar Mathematical Library","author":"Urban","year":"2010"},{"key":"10.1016\/j.engappai.2025.113073_bib46","series-title":"International Conference on Automated Deduction","first-page":"648","article-title":"Theorem proving in non-standard logics based on the inverse method","author":"Voronkov","year":"1992"},{"key":"10.1016\/j.engappai.2025.113073_bib47","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/j.ins.2018.04.086","article-title":"Contradiction separation based dynamic multi-clause synergized automated deduction","volume":"462","author":"Xu","year":"2018","journal-title":"Inf. Sci."},{"key":"10.1016\/j.engappai.2025.113073_bib48","series-title":"Data Science and Knowledge Engineering for Sensing Decision Support","first-page":"725","article-title":"Distinctive features of the contradiction separation based dynamic automated deduction","author":"Xu","year":"2018"},{"key":"10.1016\/j.engappai.2025.113073_bib49","series-title":"Intelligent Management of Data and Information in Decision Making","first-page":"97","article-title":"Inverse dynamic deduction algorithm of standard contradiction separation rule based on parallel mechanism","author":"Zeng","year":"2024"},{"key":"10.1016\/j.engappai.2025.113073_bib50","doi-asserted-by":"crossref","DOI":"10.1016\/j.knosys.2023.111238","article-title":"A complementary ratio based clause selection method for contradiction separation dynamic deduction","volume":"284","author":"Zeng","year":"2024","journal-title":"Knowl. Base Syst."},{"key":"10.1016\/j.engappai.2025.113073_bib51","series-title":"2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE)","first-page":"1","article-title":"Multi-clause synergized contradiction separation based first-order theorem prover\u2014MC-SCS","author":"Zhong","year":"2017"}],"container-title":["Engineering Applications of Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0952197625031045?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0952197625031045?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T07:08:33Z","timestamp":1773817713000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0952197625031045"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1]]},"references-count":51,"alternative-id":["S0952197625031045"],"URL":"https:\/\/doi.org\/10.1016\/j.engappai.2025.113073","relation":{},"ISSN":["0952-1976"],"issn-type":[{"value":"0952-1976","type":"print"}],"subject":[],"published":{"date-parts":[[2026,1]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Multilayer inverse dynamic deduction algorithm of standard contradiction separation rule based on parallel mechanism","name":"articletitle","label":"Article Title"},{"value":"Engineering Applications of Artificial Intelligence","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.engappai.2025.113073","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2025 Elsevier Ltd. All rights are reserved, including those for text and data mining, AI training, and similar technologies.","name":"copyright","label":"Copyright"}],"article-number":"113073"}}