{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T17:28:56Z","timestamp":1764782936176},"reference-count":25,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":4759,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2001,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We prove that the problem of determining the minimum propositional proof length is NP-hard to approximate within a factor of <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200011269_inline1\" \/>. These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution. Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problems of approximation of the length of proofs.<\/jats:p>","DOI":"10.2307\/2694916","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T18:03:53Z","timestamp":1146938633000},"page":"171-191","source":"Crossref","is-referenced-by-count":27,"title":["Minimum propositional proof length is NP-hard to linearly approximate"],"prefix":"10.1017","volume":"66","author":[{"given":"Michael","family":"Alekhnovich","sequence":"first","affiliation":[]},{"given":"Sam","family":"Buss","sequence":"additional","affiliation":[]},{"given":"Shlomo","family":"Moran","sequence":"additional","affiliation":[]},{"given":"Toniann","family":"Pitassi","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200011269_ref025","first-page":"505","volume-title":"Logic colloquium \u203276","author":"Statman","year":"1977"},{"key":"S0022481200011269_ref014","first-page":"36","volume":"44","author":"Cook","year":"1979","journal-title":"The relative efficiency of propositional proof systems"},{"key":"S0022481200011269_ref003","volume-title":"Approximation algorithms for NP-hard problems","author":"Arora","year":"1996"},{"key":"S0022481200011269_ref012","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2566-9_4"},{"key":"S0022481200011269_ref006","first-page":"2","article-title":"Proof checking and approximation: Towards tight results","volume":"27","author":"Bellare","year":"1996","journal-title":"SIGACT News"},{"key":"S0022481200011269_ref023","first-page":"475","volume-title":"Proceedings of the 29-th Annual ACM Symposium on Theory of Computing","author":"Raz","year":"1997"},{"key":"S0022481200011269_ref017","doi-asserted-by":"publisher","DOI":"10.1142\/S0218195999000248"},{"key":"S0022481200011269_ref013","first-page":"174","volume-title":"Proceedings of the twenty-eighth annual acm symposium on the theory of computing","author":"Clegg","year":"1996"},{"key":"S0022481200011269_ref020","doi-asserted-by":"publisher","DOI":"10.1109\/CCC.1997.612323"},{"key":"S0022481200011269_ref021","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60178-3_86"},{"key":"S0022481200011269_ref019","doi-asserted-by":"publisher","DOI":"10.1109\/SCT.1995.514725"},{"key":"S0022481200011269_ref001","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BFb0055766","volume-title":"Mathematical foundations of computer science (mfcs\u203298)","author":"Alehknovich","year":"1998"},{"key":"S0022481200011269_ref004","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-73.1.1"},{"key":"S0022481200011269_ref005","first-page":"274","volume-title":"37th annual symposium on foundations of computer science","author":"Beame","year":"1996"},{"key":"S0022481200011269_ref008","unstructured":"Bonet M. , Gavalda R. , Domingo C. , Maciel A. , and Pitassi T. , NO feasible interpolation or automatization for bounded-depth frege systems. 1998, Manuscript."},{"key":"S0022481200011269_ref009","unstructured":"Bonet M. L. , The Lengths of Propositional Proofs and the Deduction Rule, Ph.D. thesis , U.C. Berkeley, 1991."},{"key":"S0022481200011269_ref010","first-page":"264","volume-title":"Proceedings of the 38th annual symposium on foundations of computer science","author":"Bonet","year":"1997"},{"key":"S0022481200011269_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/BF02391554"},{"key":"S0022481200011269_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63307-3_70"},{"key":"S0022481200011269_ref018","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0029974"},{"key":"S0022481200011269_ref022","doi-asserted-by":"publisher","DOI":"10.1145\/185675.306789"},{"key":"S0022481200011269_ref024","unstructured":"Reckhow R. A. , On the Lengths of Proofs in the Propositional Calculus, Ph.D. thesis , Department of Computer Science, University of Toronto, 1976, Technical Report #87."},{"key":"S0022481200011269_ref015","volume-title":"Technical Report TR99-015","author":"Dinur","year":"1999"},{"key":"S0022481200011269_ref007","first-page":"294","volume-title":"Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing","author":"Bellare","year":"1993"},{"key":"S0022481200011269_ref002","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1997.1472"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200011269","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,8]],"date-time":"2019-05-08T00:45:40Z","timestamp":1557276340000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200011269\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,3]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,3]]}},"alternative-id":["S0022481200011269"],"URL":"https:\/\/doi.org\/10.2307\/2694916","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,3]]}}}