{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T04:45:24Z","timestamp":1773809124382,"version":"3.50.1"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2022,2,23]],"date-time":"2022-02-23T00:00:00Z","timestamp":1645574400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,2,23]],"date-time":"2022-02-23T00:00:00Z","timestamp":1645574400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"crossref","award":["FA9550-19-1-0177"],"award-info":[{"award-number":["FA9550-19-1-0177"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,5]]},"DOI":"10.1007\/s10817-022-09618-2","type":"journal-article","created":{"date-parts":[[2022,2,23]],"date-time":"2022-02-23T06:12:39Z","timestamp":1645596759000},"page":"239-274","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Analyzing Read-Once Cutting Plane Proofs in Horn Systems"],"prefix":"10.1007","volume":"66","author":[{"given":"Piotr","family":"Wojciechowski","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5821-5117","authenticated-orcid":false,"given":"K.","family":"Subramani","sequence":"additional","affiliation":[]},{"given":"R.","family":"Chandrasekaran","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,2,23]]},"reference":[{"key":"9618_CR1","doi-asserted-by":"crossref","unstructured":"B\u00fcning, H.K., Wojciechowski, P.J., Subramani, K.: On the application of restricted cutting plane systems to Horn constraint systems. In: The 12th International Symposium on Frontiers of Combining Systems, London, United Kingdom,, September 4-6, 2019, Proceedings, pp. 149\u2013164 (2019)","DOI":"10.1007\/978-3-030-29007-8_9"},{"key":"9618_CR2","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."},{"issue":"2","key":"9618_CR3","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.cosrev.2010.09.009","volume":"5","author":"RM McConnell","year":"2011","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119\u2013161 (2011)","journal-title":"Comput. Sci. Rev."},{"key":"9618_CR4","unstructured":"Kratsch, D., McConnell, R.M., Mehlhorn, K., Spinrad, J.: Certifying algorithms for recognizing interval graphs and permutation graphs. In: SODA, pp. 158\u2013167 (2003)"},{"key":"9618_CR5","unstructured":"Dhiflaoui, M., Funke, S., Kwappik, C., Mehlhorn, K., Seel, M., Sch\u00f6mer, E., Schulte, R., Weber, D.: Certifying and repairing solutions to large LPS how good are LP-solvers? In: SODA, pp. 255\u2013256 (2003)"},{"issue":"15","key":"9618_CR6","doi-asserted-by":"publisher","first-page":"3216","DOI":"10.1016\/j.dam.2009.07.002","volume":"157","author":"H Kaplan","year":"2009","unstructured":"Kaplan, H., Nussbaum, Y.: Certifying algorithms for recognizing proper circular-arc graphs and unit circular-arc graphs. Discrete Appl. Math. 157(15), 3216\u20133230 (2009)","journal-title":"Discrete Appl. Math."},{"key":"9618_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2014.12.016","volume":"576","author":"K Subramani","year":"2015","unstructured":"Subramani, K., Worthington, J.: Feasibility checking in Horn constraint systems through a reduction based approach. Theor. Comput. Sci. 576, 1\u201317 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"9618_CR8","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 \u201995), pp. 29\u201336, Los Alamitos, CA, USA, June 1995. IEEE Computer Society Press","DOI":"10.1109\/SCT.1995.514725"},{"issue":"3","key":"9618_CR9","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1287\/ijoc.1.3.137","volume":"1","author":"JN Hooker","year":"1989","unstructured":"Hooker, J.N.: Input proofs and rank one cutting planes. INFORMS J. Comput. 1(3), 137\u2013145 (1989)","journal-title":"INFORMS J. Comput."},{"key":"9618_CR10","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/BFb0023767","volume-title":"Computer Science Logic","author":"JN Hooker","year":"1992","unstructured":"Hooker, J.N.: Logical Inference and Polyhedral Projection. In: B\u00f6rger, E., J\u00e4ger, G., B\u00fcning, H.K., Richter, M.M. (eds.) Computer Science Logic, pp. 184\u2013200. Springer, Berlin (1992)"},{"issue":"124","key":"9618_CR11","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":"9618_CR12","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1987","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1987)"},{"key":"9618_CR13","volume-title":"Integer and Combinatorial Optimization","author":"GL Nemhauser","year":"1999","unstructured":"Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. Wiley, New York (1999)"},{"key":"9618_CR14","unstructured":"Orponen, P., Mannila, H.: On approximation preserving reductions: Complete problems and robust measures. Technical report, Department of Computer Science, University of Helsinki (1987)"},{"key":"9618_CR15","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-1-4684-2001-2_9","volume-title":"Complexity of Computer Computations","author":"RM Karp","year":"1972","unstructured":"Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R.E., Thatcher, J.W. (eds.) Complexity of Computer Computations, pp. 85\u2013103. Plenum Press, New York (1972)"},{"issue":"3","key":"9618_CR16","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"WF Dowling","year":"1984","unstructured":"Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Log. Program. 1(3), 267\u2013284 (1984)","journal-title":"J. Log. Program."},{"key":"9618_CR17","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K.L., Rybalchenko, A.: Horn clause solvers for program verification. In: Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, pp. 24\u201351 (2015)","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"9618_CR18","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, September 27-30, 2015., pp. 89\u201396 (2015)","DOI":"10.1109\/FMCAD.2015.7542257"},{"key":"9618_CR19","doi-asserted-by":"crossref","unstructured":"Kahsai, T., Vidal, G. (eds.) Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis, HCVS 2018, Oxford, UK, 13th July 2018, volume 278 of EPTCS, (2018)","DOI":"10.4204\/EPTCS.278.0"},{"key":"9618_CR20","doi-asserted-by":"crossref","unstructured":"Bakhirkin, A., Monniaux, D.: Combining forward and backward abstract interpretation of Horn clauses. In: Static Analysis\u201424th International Symposium, SAS 2017, New York, NY, USA, August 30 - September 1, 2017, Proceedings, pp. 23\u201345 (2017)","DOI":"10.1007\/978-3-319-66706-5_2"},{"key":"9618_CR21","doi-asserted-by":"crossref","unstructured":"Fouilh\u00e9, A., Monniaux, D., P\u00e9rin, M.: Efficient generation of correctness certificates for the abstract domain of polyhedra. In: Static Analysis\u201420th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings, pp. 345\u2013365 (2013)","DOI":"10.1007\/978-3-642-38856-9_19"},{"issue":"12","key":"9618_CR22","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/2043174.2043195","volume":"54","author":"G Brewka","year":"2011","unstructured":"Brewka, G., Eiter, T., Truszczynski, M.: Answer set programming at a glance. Commun. ACM 54(12), 92\u2013103 (2011)","journal-title":"Commun. ACM"},{"issue":"3","key":"9618_CR23","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s10601-016-9257-7","volume":"22","author":"Y Lierler","year":"2017","unstructured":"Lierler, Y.: What is answer set programming to propositional satisfiability. Constraints An Int. J. 22(3), 307\u2013337 (2017)","journal-title":"Constraints An Int. J."},{"issue":"3","key":"9618_CR24","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1609\/aimag.v37i3.2671","volume":"37","author":"T Janhunen","year":"2016","unstructured":"Janhunen, T., Niemel\u00e4, I.: The answer set programming paradigm. AI Magaz. 37(3), 13\u201324 (2016)","journal-title":"AI Magaz."},{"issue":"2\u20133","key":"9618_CR25","first-page":"105","volume":"32","author":"T Schaub","year":"2018","unstructured":"Schaub, T., Woltran, S.: Answer set programming unleashed! KI 32(2\u20133), 105\u2013108 (2018)","journal-title":"KI"},{"key":"9618_CR26","unstructured":"Colmerauer, A.: Logic Programming and Its Applications. chapter Theoretical Model of PrologII, pp. 181\u2013200. Ablex Series in Artificial Intelligence. Ablex Publishing Corporation (1986)"},{"key":"9618_CR27","unstructured":"Buss, S.R.: Propositional proof complexity: An introduction. http:\/\/www.math.ucsd.edu\/~sbuss\/ResearchWeb\/marktoberdorf97\/paper.pdf"},{"issue":"3","key":"9618_CR28","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/s10817-013-9289-2","volume":"52","author":"E Alkassar","year":"2014","unstructured":"Alkassar, E., B\u00f6hme, S., Mehlhorn, K., Rizkallah, C.: A framework for the verification of certifying computations. J. Autom. Reason. 52(3), 241\u2013273 (2014)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9618_CR29","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":"9618_CR30","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"},{"issue":"2\u20133","key":"9618_CR31","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."},{"issue":"4","key":"9618_CR32","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":"9618_CR33","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.tcs.2018.02.002","volume":"729","author":"HK B\u00fcning","year":"2018","unstructured":"B\u00fcning, H.K., Wojciechowski, P.J., Subramani, K.: Finding read-once resolution refutations in systems of 2CNF clauses. Theor. Comput. Sci. 729, 42\u201356 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"9618_CR34","doi-asserted-by":"crossref","unstructured":"Szeider, S.: NP-completeness of refutability by literal-once resolution. In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, volume 2083, pp. 168\u2013181 (2001)","DOI":"10.1007\/3-540-45744-5_13"},{"key":"9618_CR35","unstructured":"B\u00fcning, H.K., Zhao, X.: Read-once unit resolution. In: Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, pp. 356\u2013369 (2003)"},{"key":"9618_CR36","doi-asserted-by":"crossref","unstructured":"B\u00fcning, H.K., Wojciechowski, P.J., Subramani, K.: Read-once resolutions in Horn formulas. In: Frontiers in Algorithmics\u201413th International Workshop, FAW 2019, Sanya, China, April 29 - May 3, 2019, Proceedings, pp. 100\u2013110 (2019)","DOI":"10.1007\/978-3-030-18126-0_9"},{"issue":"3","key":"9618_CR37","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1016\/j.tcs.2005.10.005","volume":"351","author":"MR Fellows","year":"2006","unstructured":"Fellows, M.R., Szeider, S., Wrightson, G.: On finding short resolution refutations and small unsatisfiable subsets. Theor. Comput. Sci. 351(3), 351\u2013359 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"9618_CR38","unstructured":"B\u00fcning, H.K., Wojciechowski, P.J., Subramani, K.: New results on cutting plane proofs for Horn constraint systems. In: 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, December 11-13, 2019, Bombay, India, pp. 43:1\u201343:14 (2019)"},{"key":"9618_CR39","doi-asserted-by":"crossref","unstructured":"Wojciechowski, P.J., Subramani, K.: On unit read-once resolutions and copy complexity. In: Wu, W., Zhang, Z. (eds.) Combinatorial Optimization and Applications\u201414th International Conference, COCOA 2020, Dallas, TX, USA, December 11-13, 2020, Proceedings, volume 12577 of Lecture Notes in Computer Science, pp. 273\u2013288. Springer (2020)","DOI":"10.1007\/978-3-030-64843-5_19"},{"issue":"3","key":"9618_CR40","first-page":"317","volume":"1","author":"V Kann","year":"1994","unstructured":"Kann, V.: Polynomially bounded minimization problems that are hard to approximate. Nordic J. Comput. 1(3), 317\u2013331 (1994)","journal-title":"Nordic J. Comput."},{"key":"9618_CR41","unstructured":"Tchebichef, P.: M\u00e9moire sur les nombres premiers. Journal de Math\u00e9matiques Pures et Appliqu\u00e9es, pp. 366\u2013390 (1852)"},{"key":"9618_CR42","first-page":"781","volume":"2","author":"M Agrawal","year":"2002","unstructured":"Agrawal, M., Kayal, N., Saxena, N.: PRIMES is in P. Ann. Math. 2, 781\u2013793 (2002)","journal-title":"Ann. Math."},{"key":"9618_CR43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21275-3","volume-title":"Parameterized Algorithms","author":"M Cygan","year":"2015","unstructured":"Cygan, M., Fomin, F.V., Kowalik, L., Lokshtanov, D., Marx, D., Pilipczuk, M., Pilipczuk, M., Saurabh, S.: Parameterized Algorithms. Springer, Berlin (2015)"},{"issue":"1","key":"9618_CR44","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0890-5401(92)90056-L","volume":"96","author":"P Berman","year":"1992","unstructured":"Berman, P., Schnitger, G.: On the complexity of approximating the independent set problem. Inf. Comput. 96(1), 77\u201394 (1992)","journal-title":"Inf. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09618-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09618-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09618-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,19]],"date-time":"2024-09-19T02:00:54Z","timestamp":1726711254000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09618-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2,23]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,5]]}},"alternative-id":["9618"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09618-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,2,23]]},"assertion":[{"value":"17 August 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 December 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 February 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}