{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T01:20:36Z","timestamp":1768094436902,"version":"3.49.0"},"reference-count":12,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T00:00:00Z","timestamp":1763683200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T00:00:00Z","timestamp":1763683200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Comput Intell Syst"],"DOI":"10.1007\/s44196-025-01035-8","type":"journal-article","created":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T13:28:49Z","timestamp":1763731729000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["\u03941: An Automated Theorem Generator"],"prefix":"10.1007","volume":"18","author":[{"given":"Yang","family":"Xu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hailin","family":"Guo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shuwei","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,21]]},"reference":[{"key":"1035_CR1","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.W., Zhong, X.M., He, X.X.: Contradiction separation based dynamic multi-clause synergized automated deduction. Inf. Sci. 462, 93\u2013113 (2018)","journal-title":"Inf. Sci."},{"key":"1035_CR2","unstructured":"Xu, Y., Chen, S.W., Zhong, X.M., Liu, J., He, X.X.: Contradictions. Preprint at: https:\/\/arxiv.org\/abs\/2509.07026 (2025)"},{"key":"1035_CR3","unstructured":"Xu, Y., He, X.X., Chen, S.W., Liu, J., Zhong, X.M.: Dynamic deduction by contradiction separation: the standard extension algorithm. Preprint at: https:\/\/arxiv.org\/abs\/2510.08468 (2025)"},{"key":"1035_CR4","unstructured":"Xu, Y., Chen, S.W., Liu, J., Cao, F., He, X.X.: Extended triangular method: a generalized algorithm for contradiction separation based automated deduction. Preprint at: https:\/\/arxiv.org\/abs\/2510.10701 (2025)"},{"key":"1035_CR5","unstructured":"Zeng, G.Y.: Inverse and parallel automated theorem prover based on contradiction separation. Doctoral Dissertation, Southwest Jiaotong University, China (2025)"},{"key":"1035_CR6","doi-asserted-by":"publisher","DOI":"10.1016\/j.knosys.2023.111238","volume":"284","author":"GY Zeng","year":"2024","unstructured":"Zeng, G.Y., Chen, S.W., Liu, J., Xu, Y., Liu, P.Y.: A complementary ratio based clause selection method for contradiction separation dynamic deduction. Knowl.-Based Syst. 284, 111238 (2024)","journal-title":"Knowl.-Based Syst."},{"key":"1035_CR7","unstructured":"Liu, P.Y.: Study on a first-order logic automated theorem prover based on contradiction separation deduction rule. Doctoral Dissertation, Southwest Jiaotong University, China (2024)"},{"key":"1035_CR8","doi-asserted-by":"publisher","DOI":"10.1016\/j.knosys.2022.110217","volume":"261","author":"PY Liu","year":"2023","unstructured":"Liu, P.Y., Chen, S.W., Liu, J., Xu, Y., Cao, F., Wu, G.F.: An efficient contradiction separation based automated deduction algorithm for enhancing reasoning capability. Knowl.-Based Syst. 261, 110217 (2023)","journal-title":"Knowl.-Based Syst."},{"key":"1035_CR9","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/j.ins.2022.11.128","volume":"622","author":"PY Liu","year":"2023","unstructured":"Liu, P.Y., Xu, Y., Liu, J., Chen, S.W., Cao, F., Wu, G.F.: Fully reusing clause deduction algorithm based on standard contradiction separation rule. Inf. Sci. 622, 337\u2013356 (2023)","journal-title":"Inf. Sci."},{"key":"1035_CR10","unstructured":"Cao F.: Study on a first-order logic automated theorem prover based on contradiction separation deduction. Doctoral Dissertation, Southwest Jiaotong University, China (2020)"},{"key":"1035_CR11","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.W., Yi, J.: A multi-clause dynamic deduction algorithm based on standard contradiction separation rule. Inf. Sci. 566, 281\u2013299 (2021)","journal-title":"Inf. Sci."},{"issue":"2","key":"1035_CR12","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.W., Zhong, J., Wu, G.F.: A contradiction separation dynamic deduction algorithm based on optimized proof search. Int. J. Comput. Intell. Syst. 12(2), 1245\u20131254 (2019)","journal-title":"Int. J. Comput. Intell. Syst."}],"container-title":["International Journal of Computational Intelligence Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s44196-025-01035-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s44196-025-01035-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s44196-025-01035-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T02:02:19Z","timestamp":1763776939000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s44196-025-01035-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,21]]},"references-count":12,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2025,12]]}},"alternative-id":["1035"],"URL":"https:\/\/doi.org\/10.1007\/s44196-025-01035-8","relation":{},"ISSN":["1875-6883"],"issn-type":[{"value":"1875-6883","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,21]]},"assertion":[{"value":"16 September 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 October 2025","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 October 2025","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 November 2025","order":4,"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":"Competing Interests"}}],"article-number":"309"}}