{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:47:32Z","timestamp":1781077652813,"version":"3.54.1"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,4,30]],"date-time":"2017-04-30T00:00:00Z","timestamp":1493510400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-121351 and DMS-1101228"],"award-info":[{"award-number":["CCF-121351 and DMS-1101228"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Simons Foundation Fellowship","award":["306202"],"award-info":[{"award-number":["306202"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2017,4,30]]},"abstract":"<jats:p>\n            We study consistency search problems for Frege and extended Frege proofs\u2014namely the NP search problems of finding syntactic errors in Frege and extended Frege proofs of contradictions. The input is a polynomial time function, or an oracle, describing a proof of a contradiction; the output is the location of a syntactic error in the proof. The consistency search problems for Frege and extended Frege systems are shown to be many-one complete for the provably total NP search problems of the second-order bounded arithmetic theories 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            , respectively.\n          <\/jats:p>","DOI":"10.1145\/3060145","type":"journal-article","created":{"date-parts":[[2017,6,5]],"date-time":"2017-06-05T12:50:00Z","timestamp":1496667000000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["The NP Search Problems of Frege and Extended Frege Proofs"],"prefix":"10.1145","volume":"18","author":[{"given":"Arnold","family":"Beckmann","sequence":"first","affiliation":[{"name":"Swansea University, Swansea, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3837-334X","authenticated-orcid":false,"given":"Sam","family":"Buss","sequence":"additional","affiliation":[{"name":"University of California, San Diego, La Jolla, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,6,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(99)00041-X"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1575"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2559950"},{"key":"e_1_2_1_4_1","unstructured":"Samuel R. Buss. 1986. Bounded Arithmetic. Bibliopolis Naples Italy. (Revision of the 1985 Princeton University Ph.D. dissertation.)  Samuel R. Buss. 1986. Bounded Arithmetic. Bibliopolis Naples Italy. (Revision of the 1985 Princeton University Ph.D. dissertation.)"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/28395.28409"},{"key":"e_1_2_1_6_1","volume-title":"Algorithms for Boolean formula evaluation and for tree contraction","author":"Buss Samuel R."},{"key":"e_1_2_1_7_1","volume-title":"Handbook of Proof Theory","author":"Buss Samuel R."},{"key":"e_1_2_1_8_1","volume-title":"Propositional proof complexity: An introduction","author":"Buss Samuel R."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1137\/0221046"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-69.1.1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/800116.803756"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-005-0282-2"},{"key":"e_1_2_1_13_1","volume-title":"Cook and Phuong Nguyen","author":"Stephen","year":"2010"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_2_1_15_1","volume-title":"Retrieved","author":"Goldberg Paul","year":"2016"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2003.12.003"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200610019"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(88)90046-3"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2010.12.002"},{"key":"e_1_2_1_20_1","volume-title":"Propositional Calculus and Complexity Theory","author":"Kraj\u00ed\u010dek Jan"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1082418532"},{"key":"e_1_2_1_22_1","volume-title":"Forcing with Random Variables and Proof Complexity","author":"Kraj\u00ed\u010dek Jan"},{"key":"e_1_2_1_23_1","first-page":"e15","article-title":"Consistency of circuit evaluation, extended resolution, and total NP search problems. Forum of Mathematics","volume":"4","author":"Kraj\u00ed\u010dek Jan","year":"2016","journal-title":"Sigma"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1185803628"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/FSCS.1990.89602"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(05)80063-7"},{"key":"e_1_2_1_27_1","volume-title":"Wilkie","author":"Paris Jeff B.","year":"1985"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.06.014"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq044"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3060145","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3060145","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3060145","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:03:20Z","timestamp":1750215800000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3060145"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,30]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,4,30]]}},"alternative-id":["10.1145\/3060145"],"URL":"https:\/\/doi.org\/10.1145\/3060145","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,4,30]]},"assertion":[{"value":"2016-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-06-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}