{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T12:54:20Z","timestamp":1752670460074,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030681944"},{"type":"electronic","value":"9783030681951"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-68195-1_18","type":"book-chapter","created":{"date-parts":[[2021,2,22]],"date-time":"2021-02-22T00:04:27Z","timestamp":1613952267000},"page":"226-237","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Tree-Like Unit Refutations in Horn Constraint Systems"],"prefix":"10.1007","author":[{"given":"K.","family":"Subramani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Wojciechowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,2,22]]},"reference":[{"issue":"1","key":"18_CR1","doi-asserted-by":"crossref","first-page":"83","DOI":"10.3233\/FI-1981-4105","volume":"4","author":"G Ausiello","year":"1981","unstructured":"Ausiello, G., D\u2019Atri, A., Protasi, M.: Lattice theoretic ordering properties for NP-complete optimization problems. Fundam. Informaticae 4(1), 83\u201394 (1981)","journal-title":"Fundam. Informaticae"},{"issue":"3","key":"18_CR2","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/BF00252179","volume":"16","author":"P Baumgartner","year":"1996","unstructured":"Baumgartner, P.: Linear and unit-resulting refutations for horn theories. J. Autom. Reason. 16(3), 241\u2013319 (1996)","journal-title":"J. Autom. Reason."},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/j.disopt.2012.11.001","volume":"10","author":"R Chandrasekaran","year":"2013","unstructured":"Chandrasekaran, R., Subramani, K.: A combinatorial algorithm for Horn programs. Discrete Optim. 10, 85\u2013101 (2013)","journal-title":"Discrete Optim."},{"key":"18_CR4","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":"18_CR5","doi-asserted-by":"crossref","unstructured":"de Moura,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":"18_CR6","unstructured":"Duterre, B., de Moura, L.: The yices SMT solver. Technical report, SRI International (2006)"},{"issue":"124","key":"18_CR7","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":"18_CR8","volume-title":"Theory of Parameterized Preprocessing","author":"FV Fomin","year":"2019","unstructured":"Fomin, F.V., Lokshtanov, D., Saurabh, S., Zehavi, M.: Theory of Parameterized Preprocessing. Cambridge University Press, Kernelization (2019)"},{"key":"18_CR9","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":"18_CR10","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19\u201320581","author":"J Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.: Constraint logic programming: a survey. J. Log. Program. 19\u201320581, 503\u2013581 (1994)","journal-title":"J. Log. Program."},{"key":"18_CR11","unstructured":"Kann, V.: On the Approximability of NP-complete Optimization Problems. Ph.D. thesis, Royal Institute of Technology Stockholm (1992)"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Bj\u00f8rner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using Horn clauses over integers and arrays. In: Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, 27\u201330 September 2015, pp. 89\u201396 (2015)","DOI":"10.1109\/FMCAD.2015.7542257"},{"key":"18_CR13","unstructured":"Lueker, G.S.: Two NP-complete Problems in Nonnegative Integer Programming. Princeton University, Department of Electrical Engineering (1975)"},{"issue":"2&3","key":"18_CR14","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":"18_CR15","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1987","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. John Wiley and Sons, New York (1987)"},{"issue":"2","key":"18_CR16","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/s10817-009-9139-4","volume":"43","author":"K Subramani","year":"2009","unstructured":"Subramani, K.: Optimal length resolution refutations of difference constraint systems. J. Autom. Reason. (JAR) 43(2), 121\u2013137 (2009)","journal-title":"J. Autom. Reason. (JAR)"},{"issue":"7","key":"18_CR17","doi-asserted-by":"publisher","first-page":"2765","DOI":"10.1007\/s00453-019-00554-z","volume":"81","author":"K Subramani","year":"2019","unstructured":"Subramani, K., Wojciechowki, P.: A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints. Algorithmica 81(7), 2765\u20132794 (2019)","journal-title":"Algorithmica"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Veinott, A.F., LiCalzi, M.: Subextremal functions and lattice programming, July 1992. Unpublished Manuscript","DOI":"10.2139\/ssrn.877266"},{"key":"18_CR19","unstructured":"Wojciechowski, P., Subramani, K.: A certifying algorithm for checking for the presence of unit refutations in horn constraint systems. European Symposium on Programming (Submitted)"},{"issue":"3","key":"18_CR20","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0304-3975(83)90020-8","volume":"26","author":"CK Yap","year":"1983","unstructured":"Yap, C.K.: Some consequences of non-uniform conditions on uniform classes. Theor. Comput. Sci. 26(3), 287\u2013300 (1983)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Language and Automata Theory and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-68195-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,18]],"date-time":"2022-12-18T12:32:55Z","timestamp":1671366775000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-68195-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030681944","9783030681951"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-68195-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"22 February 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LATA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Language and Automata Theory and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 March 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lata2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/irdta.eu\/lata2020&2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"52","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"50% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}