{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T13:57:02Z","timestamp":1752674222630,"version":"3.40.5"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031929311","type":"print"},{"value":"9783031929328","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-92932-8_2","type":"book-chapter","created":{"date-parts":[[2025,5,17]],"date-time":"2025-05-17T07:47:18Z","timestamp":1747468038000},"page":"18-33","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Unit Refutations in\u00a0Horn Constraint Systems"],"prefix":"10.1007","author":[{"given":"Piotr","family":"Wojciechowski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K.","family":"Subramani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,18]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Owre, S., Ruess, H., Rushby, J.M., Shankar, N.: The ICS decision procedures for embedded deduction. In: IJCAR, pp. 218\u2013222 (2004)","DOI":"10.1007\/978-3-540-25984-8_14"},{"key":"2_CR3","unstructured":"Dutertre, B., de Moura, L.: The YICES SMT solver. Technical report, SRI International (2006)"},{"issue":"124","key":"2_CR4","first-page":"1","volume":"124","author":"G Farkas","year":"1902","unstructured":"Farkas, G.: \u00dcber die Theorie der Einfachen Ungleichungen. Journal f\u00fcr die Reine und Angewandte Mathematik 124(124), 1\u201327 (1902)","journal-title":"Journal f\u00fcr die Reine und Angewandte Mathematik"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Ford, J., Shankar, N.: Formal verification of a combination decision procedure. In: CADE, pp. 347\u2013362 (2002)","DOI":"10.1007\/3-540-45620-1_29"},{"key":"2_CR6","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"MR Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman Company, San Francisco (1979)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Gupta, G.: Horn logic denotations and their applications. In: Apt, K.R., Marek, V.W., Truszczynski, M., Warren, D.S. (eds.) The Logic Programming Paradigm - A 25-Year Perspective, Artificial Intelligence, pp. 127\u2013159. Springer, Cham (1999)","DOI":"10.1007\/978-3-642-60085-2_6"},{"issue":"2\u20133","key":"2_CR8","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39(2\u20133), 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Iwama, K., Miyano, E.: Intractability of read-once resolution. In: Proceedings of the 10th Annual Conference on Structure in Complexity Theory (SCTC 1995), Los Alamitos, CA, USA, pp. 29\u201336, June 1995. IEEE Computer Society Press (1995)","DOI":"10.1109\/SCT.1995.514725"},{"issue":"4","key":"2_CR10","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1023\/A:1016339119669","volume":"36","author":"HK B\u00fcning","year":"2002","unstructured":"B\u00fcning, H.K., Zhao, X.: The complexity of read-once resolution. Ann. Math. Artif. Intell. 36(4), 419\u2013435 (2002)","journal-title":"Ann. Math. Artif. Intell."},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Musuvathi, M.: An efficient decision procedure for UTVPI constraints. In: Proceedings of the 5th International Workshop on the Frontiers of Combining Systems, Vienna, Austria, 19\u201321 September, pp. 168\u2013183. Springer, New York (2005)","DOI":"10.1007\/11559306_9"},{"issue":"1","key":"2_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0020-0190(88)90124-X","volume":"29","author":"M Minoux","year":"1988","unstructured":"Minoux, M.: LTUR: a simplified linear-time unit resolution algorithm for Horn formulae and computer implementation. Inf. Process. Lett. 29(1), 1\u201312 (1988)","journal-title":"Inf. Process. Lett."},{"issue":"2 &3","key":"2_CR13","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(90)90043-5","volume":"9","author":"VS Neiman","year":"1990","unstructured":"Neiman, V.S.: Refutation search for Horn sets by a subgoal-extraction method. J. Log. Program. 9(2 &3), 267\u2013284 (1990)","journal-title":"J. Log. Program."},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Simon, A., King, A., Howe, J.M.: Two variables per linear inequality as an abstract domain. In: Logic Based Program Synthesis and Transformation, 12th International Workshop, LOPSTR 2002, Madrid, Spain, 17\u201320 September 2002, Revised Selected Papers, pp. 71\u201389 (2002)","DOI":"10.1007\/3-540-45013-0_7"}],"container-title":["Lecture Notes in Computer Science","Algorithms and Complexity"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-92932-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,17]],"date-time":"2025-05-17T07:47:21Z","timestamp":1747468041000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-92932-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031929311","9783031929328"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-92932-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"18 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CIAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Algorithms and Complexity","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ciac2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/ciac2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}