{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:17:23Z","timestamp":1740107843916,"version":"3.37.3"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T00:00:00Z","timestamp":1594771200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T00:00:00Z","timestamp":1594771200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61305074","61603307"],"award-info":[{"award-number":["61305074","61603307"]}],"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":["61673320"],"award-info":[{"award-number":["61673320"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"MOE (Ministry of Education in China) Project of Humanities and Social Sciences","award":["19YJCZH048"],"award-info":[{"award-number":["19YJCZH048"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Soft Comput"],"published-print":{"date-parts":[[2021,1]]},"DOI":"10.1007\/s00500-020-05136-8","type":"journal-article","created":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T08:02:45Z","timestamp":1594800165000},"page":"251-261","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["$$\\alpha $$-Paramodulation method for a lattice-valued logic $$L_nF(X)$$ with equality"],"prefix":"10.1007","volume":"25","author":[{"given":"Xingxing","family":"He","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yingfang","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,15]]},"reference":[{"issue":"2","key":"5136_CR1","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L Bachmair","year":"1995","unstructured":"Bachmair L, Ganzinger H, Lynch C, Snyder W (1995) Basic paramodulation. Inf Comput 121(2):172\u2013192","journal-title":"Inf Comput"},{"issue":"1","key":"5136_CR2","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/s10817-011-9244-z","volume":"50","author":"M Bofill","year":"2013","unstructured":"Bofill M, Rubio A (2013) Paramodulation with non-monotonic orderings and simplification. J Autom Reason 50(1):51\u201398","journal-title":"J Autom Reason"},{"issue":"4","key":"5136_CR3","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D Brand","year":"1975","unstructured":"Brand D (1975) Proving theorems with the modification method. SIAM J Comput 4(4):412\u2013430","journal-title":"SIAM J Comput"},{"issue":"2","key":"5136_CR4","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/s10817-014-9301-5","volume":"53","author":"JP Bridge","year":"2014","unstructured":"Bridge JP, Holden SB, Paulson LC (2014) Machine learning for first-order theorem proving. J Autom Reason 53(2):141\u2013172","journal-title":"J Autom Reason"},{"key":"5136_CR5","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-030-29436-6_8","volume-title":"Automated deduction\u2013CADE 27","author":"CE Brown","year":"2019","unstructured":"Brown CE, Gauthier T, Kaliszyk C, Sutcliffe G, Urban J (2019) Grunge: a grand unified atp challenge. In: Fontaine P (ed) Automated deduction\u2013CADE 27. Springer International Publishing, Cham, pp 123\u2013141"},{"issue":"2","key":"5136_CR6","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 (2019) A contradiction separation dynamic deduction algorithm based on optimized proof search. Int J Comput Intell Syst 12(2):1245\u20131254","journal-title":"Int J Comput Intell Syst"},{"key":"5136_CR7","volume-title":"Symbolic logic and mechanical theorem proving","author":"CL Chang","year":"2014","unstructured":"Chang CL, Lee RCT (2014) Symbolic logic and mechanical theorem proving. Academic press, Cambridge"},{"key":"5136_CR8","first-page":"531","volume-title":"Twenty-third international joint conference on artificial intelligence","author":"M Echenim","year":"2013","unstructured":"Echenim M, Peltier N, Tourret S (2013) An approach to abductive reasoning in equational logic. In: Rossi F (ed) Twenty-third international joint conference on artificial intelligence. AAAI Press, Beijing, pp 531\u2013537"},{"issue":"3","key":"5136_CR9","doi-asserted-by":"crossref","first-page":"579","DOI":"10.1093\/jigpal\/jzr007","volume":"20","author":"X He","year":"2012","unstructured":"He X, Liu J, Xu Y, Mart\u00ednez L, Ruan D (2012) On $$\\alpha $$-satisfiability and its $$\\alpha $$-lock resolution in a finite lattice-valued propositional logic. Log J IGPL 20(3):579\u2013588","journal-title":"Log J IGPL"},{"key":"5136_CR10","doi-asserted-by":"crossref","unstructured":"He X, Xu Y, LI Y (2016) $$\\alpha $$-Lock paramodulation for a lattice-valued first order logic $${L}_n$$F(X). In: Uncertainty modelling in knowledge engineering and decision making: proceedings of the 12th international FLINS conference, pp 477\u2013482. World Scientific","DOI":"10.1142\/9789813146976_0077"},{"key":"5136_CR11","doi-asserted-by":"crossref","unstructured":"He X, Xu Y, Liu J (2015) $$\\alpha $$-Lock paramodulation for lattice-valued propositional logic. In: 2015 10th international conference on intelligent systems and knowledge engineering (ISKE), pp 18\u201320. IEEE","DOI":"10.1109\/ISKE.2015.90"},{"issue":"4","key":"5136_CR12","doi-asserted-by":"crossref","first-page":"699","DOI":"10.1007\/s00500-011-0779-z","volume":"16","author":"X He","year":"2012","unstructured":"He X, Xu Y, Liu J, Chen S (2012) On compatibilities of $$\\alpha $$-lock resolution method in linguistic truth-valued lattice-valued logic. Soft Comput 16(4):699\u2013709","journal-title":"Soft Comput"},{"issue":"11","key":"5136_CR13","doi-asserted-by":"crossref","first-page":"2135","DOI":"10.1007\/s00500-013-1188-2","volume":"18","author":"X He","year":"2014","unstructured":"He X, Xu Y, Liu J, Chen S (2014) A unified algorithm for finding $$k$$-IESFs in linguistic truth-valued lattice-valued propositional logic. Soft Comput 18(11):2135\u20132147","journal-title":"Soft Comput"},{"issue":"7","key":"5136_CR14","doi-asserted-by":"publisher","first-page":"1274","DOI":"10.1016\/j.engappai.2011.07.003","volume":"24","author":"X He","year":"2011","unstructured":"He X, Xu Y, Liu J, Ruan D (2011) $$\\alpha $$-Lock resolution method for a lattice-valued first-order logic. Eng Appl Artif Intell 24(7):1274\u20131280","journal-title":"Eng Appl Artif Intell"},{"issue":"4","key":"5136_CR15","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1109\/TFUZZ.2003.814859","volume":"11","author":"J Liu","year":"2003","unstructured":"Liu J, Ruan D, Xu Y, Song Z (2003) A resolution-like strategy based on a lattice-valued logic. IEEE Trans Fuzzy Syst 11(4):560\u2013567","journal-title":"IEEE Trans Fuzzy Syst"},{"issue":"1","key":"5136_CR16","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1023\/A:1005784309139","volume":"21","author":"JJ Lu","year":"1998","unstructured":"Lu JJ, Murray NV, Rosenthal E (1998) A framework for automated reasoning in multiple-valued logics. J Autom Reason 21(1):39\u201367","journal-title":"J Autom Reason"},{"key":"5136_CR17","unstructured":"McCune W (2005) Release of prover9. In: Mile high conference on quasigroups, loops and nonassociative systems, Denver, Colorado"},{"key":"5136_CR18","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume":"1","author":"R Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis R, Rubio A (2001) Paramodulation-based theorem proving. Handb Autom Reason 1:371\u2013443","journal-title":"Handb Autom Reason"},{"issue":"7","key":"5136_CR19","first-page":"1596","volume":"53","author":"D Ouyang","year":"2016","unstructured":"Ouyang D, Jia F, Liu S, Zhang L (2016) An algorithm based on extension rule for solving $$\\sharp $$sat using complementary degree. J Comput Res Dev 53(7):1596\u20131604","journal-title":"J Comput Res Dev"},{"key":"5136_CR20","doi-asserted-by":"publisher","DOI":"10.2991\/978-94-91216-28-2","volume-title":"Linguistic values based intelligent information processing: theory, methods, and applications","author":"Z Pei","year":"2010","unstructured":"Pei Z, Ruan D, Liu J, Xu Y (2010) Linguistic values based intelligent information processing: theory, methods, and applications, vol 259. Springer, Berlin"},{"issue":"1","key":"5136_CR21","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1089\/big.2013.1508","volume":"1","author":"F Provost","year":"2013","unstructured":"Provost F, Fawcett T (2013) Data science and its relationship to big data and data-driven decision making. Big data 1(1):51\u201359","journal-title":"Big data"},{"key":"5136_CR22","doi-asserted-by":"crossref","unstructured":"Riazanov A, Voronkov A (2001) Vampire 1.1. In: International joint conference on automated reasoning, Springer, Berlin, pp 376\u2013380","DOI":"10.1007\/3-540-45744-5_29"},{"key":"5136_CR23","doi-asserted-by":"crossref","unstructured":"Robinson G, Wos L (1983) Paramodulation and theorem-proving in first-order theories with equality. In: Automation of Reasoning, Springer, Berlin, pp 298\u2013313","DOI":"10.1007\/978-3-642-81955-1_19"},{"issue":"1","key":"5136_CR24","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson JA (1965) A machine-oriented logic based on the resolution principle. J ACM (JACM) 12(1):23\u201341","journal-title":"J ACM (JACM)"},{"issue":"2, 3","key":"5136_CR25","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz S (2002) E-a brainiac theorem prover. AI Commun 15(2, 3):111\u2013126","journal-title":"AI Commun"},{"issue":"5\u20136","key":"5136_CR26","first-page":"373","volume":"32","author":"G Sutcliffe","year":"2019","unstructured":"Sutcliffe G (2019) The CADE-27 automated theorem proving system competition-CASC-27. AI Commun 32(5\u20136):373\u2013389","journal-title":"AI Commun"},{"issue":"1","key":"5136_CR27","first-page":"20","volume":"28","author":"Y Xu","year":"1993","unstructured":"Xu Y (1993) Lattice implication algebras. J Southwest Jiaot Univ 28(1):20\u201327","journal-title":"J Southwest Jiaot Univ"},{"key":"5136_CR28","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 (2018) Contradiction separation based dynamic multi-clause synergized automated deduction. Inf Sci 462:93\u2013113","journal-title":"Inf Sci"},{"issue":"1\u20134","key":"5136_CR29","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/S0020-0255(01)00065-2","volume":"132","author":"Y Xu","year":"2001","unstructured":"Xu Y, Ruan D, Kerre E, Liu J (2001) $$\\alpha $$-Resolution principle based on lattice-valued first-order lattice-valued logic LF(X). Inf Sci 132(1\u20134):221\u2013239","journal-title":"Inf Sci"},{"issue":"1\u20134","key":"5136_CR30","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1016\/S0020-0255(00)00069-4","volume":"130","author":"Y Xu","year":"2000","unstructured":"Xu Y, Ruan D, Kerre EE, Liu J (2000) $$\\alpha $$-Resolution principle based on lattice-valued propositional logic LP(X). Inf Sci 130(1\u20134):195\u2013223","journal-title":"Inf Sci"},{"key":"5136_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-44847-1","volume-title":"Lattice-valued logic: an alternative approach to treat fuzziness and incomparability","author":"Y Xu","year":"2003","unstructured":"Xu Y, Ruan D, Qin K, Liu J (2003) Lattice-valued logic: an alternative approach to treat fuzziness and incomparability. Springer, Heidelberg"},{"issue":"1","key":"5136_CR32","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1080\/18756891.2013.857895","volume":"7","author":"J Zhang","year":"2014","unstructured":"Zhang J, Xu Y, He X (2014) $$\\alpha $$-Generalized semantic resolution method in linguistic truth-valued propositional logic $${L}_{{V}(n\\times 2)}$$P(X). Int J Comput Intell Syst 7(1):160\u2013171","journal-title":"Int J Comput Intell Syst"},{"issue":"10","key":"5136_CR33","doi-asserted-by":"crossref","first-page":"1767","DOI":"10.1007\/s00500-012-0860-2","volume":"16","author":"X Zhong","year":"2012","unstructured":"Zhong X, Xu Y, Liu J, Chen S (2012) General form of $$\\alpha $$-resolution principle for linguistic truth-valued lattice-valued logic. Soft Comput 16(10):1767\u20131781","journal-title":"Soft Comput"},{"key":"5136_CR34","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/j.ins.2017.05.046","volume":"414","author":"L Zou","year":"2017","unstructured":"Zou L, Li X, Pan C, Liu X (2017) ($$\\alpha $$, $$\\beta $$)-Ordered linear resolution of intuitionistic fuzzy propositional logic. Inf Sci 414:329\u2013339","journal-title":"Inf Sci"}],"container-title":["Soft Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00500-020-05136-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00500-020-05136-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00500-020-05136-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:03:18Z","timestamp":1626307398000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00500-020-05136-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,15]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1]]}},"alternative-id":["5136"],"URL":"https:\/\/doi.org\/10.1007\/s00500-020-05136-8","relation":{},"ISSN":["1432-7643","1433-7479"],"issn-type":[{"type":"print","value":"1432-7643"},{"type":"electronic","value":"1433-7479"}],"subject":[],"published":{"date-parts":[[2020,7,15]]},"assertion":[{"value":"15 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Compliance with ethical standards"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"This article does not contain any studies with human participants or animals performed by any of the authors.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical approval"}}]}}