{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:16:36Z","timestamp":1783541796015,"version":"3.55.0"},"publisher-location":"Singapore","reference-count":19,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819223688","type":"print"},{"value":"9789819223695","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T00:00:00Z","timestamp":1783555200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T00:00:00Z","timestamp":1783555200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2027]]},"DOI":"10.1007\/978-981-92-2369-5_34","type":"book-chapter","created":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T19:24:59Z","timestamp":1783538699000},"page":"559-569","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Properties of\u00a0Inclusion Relationship Between Clause Sets in\u00a0Propositional Logic"],"prefix":"10.1007","author":[{"given":"Xiaomei","family":"Zhong","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hanhui","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yang","family":"Xu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,9]]},"reference":[{"issue":"3","key":"34_CR1","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1145\/321592.321603","volume":"17","author":"R Anderson","year":"1970","unstructured":"Anderson, R., Bledsoe, W.W.: A linear format for resolution with merging and a new technique for establishing completeness. J. ACM 17(3), 525\u2013534 (1970)","journal-title":"J. ACM"},{"key":"34_CR2","unstructured":"Boyer R.S.: Locking: a restriction of resolution (dissertation). University of Texas at Austin (1971)"},{"issue":"3","key":"34_CR3","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217\u2013247 (1994)","journal-title":"J. Log. Comput."},{"key":"34_CR4","unstructured":"Bin, C.: Principle of Generalized Support Set Reduction. J. Northern Jiaotong Univ. 22(2), 70\u201372 (1998) (in Chinese)"},{"key":"34_CR5","unstructured":"Ruixin, J.: Inclusion Relation between Clause Sets in Propositional Logic. Southwest Jiaotong University, Bachelor\u2019s Degree Thesis (2024) (in Chinese)"},{"key":"34_CR6","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","volume":"2","author":"R Kowaski","year":"1971","unstructured":"Kowaski, R., Kuehner, D.: Linear resolution with selection function. Artif. Intell. 2, 227\u2013260 (1971)","journal-title":"Artif. Intell."},{"key":"34_CR7","first-page":"129","volume":"4","author":"L Xuhua","year":"1979","unstructured":"Xuhua, L.: Semantic resolution of locks using lemmas - LI resolution. J. Jilin Univ. 4, 129\u2013136 (1979). (in Chinese)","journal-title":"J. Jilin Univ."},{"key":"34_CR8","first-page":"1201","volume":"16","author":"L Xuhua","year":"1985","unstructured":"Xuhua, L.: Input semilock resolution on horn sets. Chin. Sci. Bull. 16, 1201\u20131202 (1985). (in Chinese)","journal-title":"Chin. Sci. Bull."},{"key":"34_CR9","first-page":"112","volume":"2","author":"L Xuhua","year":"1987","unstructured":"Xuhua, L.: A new principle of semantic resolution. J. Jilin Univ. 2, 112\u2013117 (1987). (in Chinese)","journal-title":"J. Jilin Univ."},{"key":"34_CR10","first-page":"60","volume":"2","author":"L Xuhua","year":"1992","unstructured":"Xuhua, L.: Compatibility issues among three resolution principles. J. Softw. 2, 60\u201364 (1992). (in Chinese)","journal-title":"J. Softw."},{"key":"34_CR11","unstructured":"Xuhua, L.: Automated Reasoning Based on Resolution Method. Science Press (1994) (in Chinese)"},{"key":"34_CR12","unstructured":"Qinghua, L., Yang, X.: An Improved OL Resolution - SOL Resolution. Comput. Eng. Sci. 41(01), 102\u2013107 (2019) (in Chinese)"},{"issue":"1","key":"34_CR13","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 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"issue":"4","key":"34_CR14","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1145\/321420.321428","volume":"14","author":"JR Slagle","year":"1967","unstructured":"Slagle, J.R.: Automatic theorem proving with renamable and semantic resolution. J. ACM 14(4), 687\u2013697 (1967)","journal-title":"J. ACM"},{"key":"34_CR15","unstructured":"Shifen, X.: Research on Automated Reasoning Based on Petri Net Models. Southwest Jiaotong University, Doctoral Dissertation (2006) (in Chinese)"},{"key":"34_CR16","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)","journal-title":"Inf. Sci."},{"key":"34_CR17","doi-asserted-by":"crossref","unstructured":"Yang, X., Shuwei, C., Xiaomei, Z., Jun, L., Xingxing, H.: Towards multi-clause automated deduction and theorem generation: Constructing and applying standard contradictions. Knowledge-Based Systems,334, ID:114985 (2026)","DOI":"10.1016\/j.knosys.2025.114985"},{"key":"34_CR18","unstructured":"Jian, Z.: Satisfiability Decision of Logical Formulas: Methods, Tools, and Applications. Science Press (2000) (in Chinese)"},{"key":"34_CR19","unstructured":"Jian, Z.: Research on an Automated Theorem Proving System Based on Dynamic Multi-agent Collaborative Reasoning. Southwest Jiaotong University, Doctoral Dissertation (2021) (in Chinese)"}],"container-title":["Lecture Notes in Computer Science","Machine Learning and Knowledge Engineering for Decision Making"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-92-2369-5_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T19:25:01Z","timestamp":1783538701000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-92-2369-5_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,9]]},"ISBN":["9789819223688","9789819223695"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-981-92-2369-5_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,7,9]]},"assertion":[{"value":"9 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FLINS-ISKE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Systems and Knowledge Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sydney","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Australia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"iske2026a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2026.flins.cc","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}