{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,2]],"date-time":"2026-03-02T09:45:55Z","timestamp":1772444755439,"version":"3.50.1"},"reference-count":16,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,2,1]],"date-time":"2014-02-01T00:00:00Z","timestamp":1391212800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000121","name":"Division of Mathematical Sciences","doi-asserted-by":"publisher","award":["DMS-1101228"],"award-info":[{"award-number":["DMS-1101228"]}],"id":[{"id":"10.13039\/100000121","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2014,2]]},"abstract":"<jats:p>\n            This article concerns the second-order systems U\n            <jats:sup>1<\/jats:sup>\n            <jats:sub>2<\/jats:sub>\n            and V\n            <jats:sup>1<\/jats:sup>\n            <jats:sub>2<\/jats:sub>\n            of bounded arithmetic, which have proof-theoretic strengths corresponding to polynomial-space and exponential-time computation. We formulate improved witnessing theorems for these two theories by using S\n            <jats:sup>1<\/jats:sup>\n            <jats:sub>2<\/jats:sub>\n            as a base theory for proving the correctness of the polynomial-space or exponential-time witnessing functions. We develop the theory of nondeterministic polynomial-space computation, including Savitch's theorem, in U\n            <jats:sup>1<\/jats:sup>\n            <jats:sub>2<\/jats:sub>\n            . Ko\u0142odziejczyk et al. [2011] have introduced local improvement properties to characterize the provably total NP functions of these second-order theories. We show that the strengths of their local improvement principles over U\n            <jats:sup>1<\/jats:sup>\n            <jats:sub>2<\/jats:sub>\n            and V\n            <jats:sup>1<\/jats:sup>\n            <jats:sub>2<\/jats:sub>\n            depend primarily on the topology of the underlying graph, not the number of rounds in the local improvement games. The theory U\n            <jats:sup>1<\/jats:sup>\n            <jats:sub>2<\/jats:sub>\n            proves the local improvement principle for linear graphs even without restricting to logarithmically many rounds. The local improvement principle for grid graphs with only logarithmically-many rounds is complete for the provably total NP search problems of V\n            <jats:sup>1<\/jats:sup>\n            <jats:sub>2<\/jats:sub>\n            . Related results are obtained for local improvement principles with one improvement round and for local improvement over rectangular grids.\n          <\/jats:p>","DOI":"10.1145\/2559950","type":"journal-article","created":{"date-parts":[[2014,3,4]],"date-time":"2014-03-04T13:24:59Z","timestamp":1393939499000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Improved witnessing and local improvement principles for second-order bounded arithmetic"],"prefix":"10.1145","volume":"15","author":[{"given":"Arnold","family":"Beckmann","sequence":"first","affiliation":[{"name":"Swansea University, Swansea, U.K."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samuel R.","family":"Buss","sequence":"additional","affiliation":[{"name":"University of California, San Diego, La Jolla, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,3,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219061309000847"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Arnold Beckmann and Samuel R. Buss. 2010. Characterization of definable search problems in bounded arithmetic via proof notations. In Ways of Proof Theory Ontos Verlag Heusenstamm 65--134.  Arnold Beckmann and Samuel R. Buss. 2010. Characterization of definable search problems in bounded arithmetic via proof notations. In Ways of Proof Theory Ontos Verlag Heusenstamm 65--134.","DOI":"10.1515\/9783110324907.65"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.05.053"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.03.014"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exl005"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1131313.1131318"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1131313.1131319"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.01.004"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2010.12.002"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Jan Kraj\u00ed\u010dek. 1995. Bounded Arithmetic Propositional Calculus and Complexity Theory. Cambridge University Press Cambridge UK.   Jan Kraj\u00ed\u010dek. 1995. Bounded Arithmetic Propositional Calculus and Complexity Theory. Cambridge University Press Cambridge UK.","DOI":"10.1017\/CBO9780511529948"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Jan Kraj\u00ed\u010dek. 2011. Forcing with Random Variables and Proof Complexity. Cambridge University Press Cambridge UK.  Jan Kraj\u00ed\u010dek. 2011. Forcing with Random Variables and Proof Complexity. Cambridge University Press Cambridge UK.","DOI":"10.1017\/CBO9781139107211"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.06.014"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(70)80006-X"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00107-3"},{"key":"e_1_2_1_15_1","unstructured":"Gaisi Takeuti. 1987. Proof Theory. 2nd ed. North-Holland Amsterdam.  Gaisi Takeuti. 1987. Proof Theory. 2nd ed. North-Holland Amsterdam."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-011-0240-0"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2559950","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2559950","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:10:25Z","timestamp":1750234225000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2559950"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["10.1145\/2559950"],"URL":"https:\/\/doi.org\/10.1145\/2559950","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,2]]},"assertion":[{"value":"2012-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-03-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}