{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,19]],"date-time":"2025-11-19T09:24:04Z","timestamp":1763544244223},"reference-count":51,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[1999,3,1]],"date-time":"1999-03-01T00:00:00Z","timestamp":920246400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":5252,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[1999,3]]},"DOI":"10.1016\/s0168-0072(98)00030-x","type":"journal-article","created":{"date-parts":[[2003,4,23]],"date-time":"2003-04-23T19:00:04Z","timestamp":1051124404000},"page":"43-55","source":"Crossref","is-referenced-by-count":7,"title":["Bounded arithmetic, proof complexity and two papers of Parikh"],"prefix":"10.1016","volume":"96","author":[{"given":"Samuel R.","family":"Buss","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0168-0072(98)00030-X_BIB1","series-title":"Arithmetic, Proof Theory, and Computational Complexity","first-page":"30","article-title":"Kreisel's conjecture for L\u22031","author":"Baaz","year":"1993"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB2","article-title":"On spectra","author":"Bennett","year":"1962"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB3_1","series-title":"Bounded Arithmetic","author":"Buss","year":"1986"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB3_2","unstructured":"Revision of 1985 Princeton University Ph.D. Thesis."},{"key":"10.1016\/S0168-0072(98)00030-X_BIB5","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0168-0072(91)90059-U","article-title":"The undecidability of k-provability","volume":"53","author":"Buss","year":"1991","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB6","doi-asserted-by":"crossref","first-page":"737","DOI":"10.2307\/2275906","article-title":"On G\u00f6del's theorems on lengths of proofs I: number of lines and speedup for arithmetics","volume":"59","author":"Buss","year":"1994","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB7","doi-asserted-by":"crossref","first-page":"562","DOI":"10.1305\/ndjfl\/1093635928","article-title":"Provable fixed points in I\u03940 + \u03a91","volume":"32","author":"Carbone","year":"1991","journal-title":"Notre Dame J. Formal Logic"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB8","series-title":"IHES preprint","article-title":"Cycling in proofs, feasibility and no speed-up for nonstandard arithmetic","author":"Carbone","year":"1996"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB9","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1002\/malq.19900360107","article-title":"Much shorter proofs: a bimodal investigation","volume":"36","author":"Carbone","year":"1990","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB10","series-title":"Proc. 7th Annual ACM Symp. on Theory of Computing","first-page":"83","article-title":"Feasibly constructive proofs and the propositional calculus","author":"Cook","year":"1975"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB11","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1002\/malq.19880340307","article-title":"Provable fixed points","volume":"34","author":"de Jongh","year":"1988","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB12","series-title":"Computation Theory: 5th Symp.","first-page":"58","article-title":"Correctness of inconsistent theories with notions of feasibility","author":"Dragalin","year":"1985"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB13","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/0168-0072(88)90015-2","article-title":"A unification algorithm for second order monadic terms","volume":"39","author":"Farmer","year":"1988","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB14","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0168-0072(91)90015-E","article-title":"A unification-theoretic method for investigating the k-provability problem","volume":"51","author":"Farmer","year":"1991","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB15_1","series-title":"Ergebnisse eines Mathematischen Kolloquiums","first-page":"23","article-title":"\u00dcber die L\u00e4nge von Beweisen","author":"G\u00f6del","year":"1936"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB15_2","first-page":"396","volume":"vol. 1","author":"G\u00f6del","year":"1986"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB16","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","article-title":"The undecidability of the second-order unification problem","volume":"13","author":"Goldfarb","year":"1981","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0168-0072(98)00030-X_BIB17","series-title":"Metamathematics of First-order Arithmetic","author":"H\u00e1jek","year":"1993"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB18","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1016\/S0019-9958(78)90257-7","article-title":"The bounded arithmetic hierarchy","volume":"36","author":"Harrow","year":"1978","journal-title":"Inform. and Control"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB19","article-title":"Recherches sur la th\u00e9orie de la d\u00e9monstration","author":"Herbrand","year":"1930"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB20","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/BF01746515","article-title":"Context-free languages and rudimentary attributes","volume":"3","author":"Jones","year":"1969","journal-title":"Math. Systems Theory"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB21","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/0168-0072(89)90012-2","article-title":"On the number of steps in proofs","volume":"41","author":"Kraj\u00ed\u010dek","year":"1989","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB22","series-title":"Propositional Calculus and Complexity Theory","article-title":"Bounded Arithmetic","author":"Kraj\u00ed\u010dek","year":"1995"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB23","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/BF01625836","article-title":"The number of proof lines and the size of proofs in first-order logic","volume":"27","author":"Kraj\u00ed\u010dek","year":"1988","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB24","series-title":"Proc. 19th Annual Symp. on Foundations of Computer Science","first-page":"193","article-title":"Model theoretic aspects of computational complexity","author":"Lipton","year":"1978"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB25","series-title":"Logic Symposia","first-page":"81","article-title":"On the length of proofs in a formal system of recursive arithmetic","volume":"vol. 891","author":"Miyatake","year":"1980"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB26","doi-asserted-by":"crossref","first-page":"115","DOI":"10.21099\/tkbjm\/1496158798","article-title":"On the length of proofs in formal systems","volume":"4","author":"Miyatake","year":"1980","journal-title":"Tsukuba J. Math."},{"key":"10.1016\/S0168-0072(98)00030-X_BIB27","series-title":"Predicative Arithmetic","author":"Nelson","year":"1986"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB28_1","first-page":"282","article-title":"Rudimentary predicates and Turing computations","volume":"195","author":"Nepomnja\u0161\u010di\u012d","year":"1970","journal-title":"Dokl. Akad. Nauk SSSR"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB28_2","first-page":"1462","volume":"11","year":"1970","journal-title":"Sov. Math. Dokl."},{"key":"10.1016\/S0168-0072(98)00030-X_BIB29_1","first-page":"326","article-title":"Reconstruction of a proof from its scheme","volume":"35","author":"Orevkov","year":"1987","journal-title":"Sov. Math. Dok."},{"key":"10.1016\/S0168-0072(98)00030-X_BIB29_2","first-page":"313","volume":"293","author":"Orevkov","year":"1987","journal-title":"Dokl. Akad. Nauk."},{"key":"10.1016\/S0168-0072(98)00030-X_BIB30","series-title":"Complexity of Proofs and Their Transformations in Axiomatic Theories","author":"Orevkov","year":"1991"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB31","doi-asserted-by":"crossref","first-page":"494","DOI":"10.2307\/2269958","article-title":"Existence and feasibility in arithmetic","volume":"36","author":"Parikh","year":"1971","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB32","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1090\/S0002-9947-1973-0432416-X","article-title":"Some results on the lengths of proofs","volume":"177","author":"Parikh","year":"1973","journal-title":"Trans. Amer. Math. Soc."},{"key":"10.1016\/S0168-0072(98)00030-X_BIB33","first-page":"394","article-title":"Introductory Note to 1936(a)","volume":"vol. 1","author":"Parikh","year":"1986"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB34","first-page":"317","article-title":"Truth definitions for \u03940 formulae, Logic and Algorithmic","volume":"vol. 30","author":"Paris","year":"1982","journal-title":"L'Enseignement Mathematique Monographie"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB35","first-page":"317","article-title":"Counting problems in bounded arithmetic, Methods in Mathematical Logic","volume":"vol. 1130","author":"Paris","year":"1985"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB36","doi-asserted-by":"crossref","first-page":"423","DOI":"10.2307\/2274231","article-title":"Cuts, consistency statements and interpretation","volume":"50","author":"Pudl\u00e1k","year":"1985","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB37","doi-asserted-by":"crossref","first-page":"235","DOI":"10.2307\/2272636","article-title":"Sets of theorems with short proofs","volume":"39","author":"Richardson","year":"1974","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB38","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/S0168-0072(98)00030-X_BIB39","series-title":"Mathematics Foundations of Computer Science","first-page":"562","article-title":"A logical approach to the problem \u201cP = NP?\u201d","volume":"vol. 88","author":"Sazanov","year":"1980"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB40","series-title":"Mathematics Foundations of Computer Science","first-page":"383","article-title":"On existence of complete predicate calculus in matemathematics without exponentiation","volume":"vol. 118","author":"Sazanov","year":"1981"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB41","article-title":"Subalgebras of diagonalizable algebras of theories containing arithmetic","volume":"323","author":"Shavrukov","year":"1993"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB42","series-title":"Theory of Formal Systems","author":"Smullyan","year":"1961"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB43","series-title":"Model Theory of Algebra and Arithmetic","first-page":"363","article-title":"Applications of complexity theory to \u03a30-definability problems in arithmetic","volume":"vol. 834","author":"Wilkie","year":"1979"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB44","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1016\/0168-0072(87)90066-2","article-title":"On the scheme of induction for bounded arithmetic formulas","volume":"35","author":"Wilkie","year":"1987","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB45","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1137\/0207018","article-title":"Rudimentary predicates and relative computation","volume":"7","author":"Wrathall","year":"1978","journal-title":"SIAM J. Comput."},{"key":"10.1016\/S0168-0072(98)00030-X_BIB46","series-title":"Intuitionism and Proof Theory","first-page":"1","article-title":"The ultra-intuitionistic criticism and the antitraditional program for foundations of mathematics","author":"Yessenin-Volpin","year":"1970"},{"key":"10.1016\/S0168-0072(98)00030-X_BIB47","doi-asserted-by":"crossref","first-page":"195","DOI":"10.21099\/tkbjm\/1496158386","article-title":"A theorem on the formalized arithmetic with function symbols\/and +","volume":"1","author":"Yukami","year":"1977","journal-title":"Tsukuba J. Math."},{"key":"10.1016\/S0168-0072(98)00030-X_BIB48","doi-asserted-by":"crossref","first-page":"69","DOI":"10.21099\/tkbjm\/1496158505","article-title":"A note on a formalized arithmetic with function symbols\/and +","volume":"2","author":"Yukami","year":"1978","journal-title":"Tsukuba J. Math"}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S016800729800030X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S016800729800030X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T22:29:06Z","timestamp":1556404146000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S016800729800030X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,3]]},"references-count":51,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[1999,3]]}},"alternative-id":["S016800729800030X"],"URL":"https:\/\/doi.org\/10.1016\/s0168-0072(98)00030-x","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[1999,3]]}}}