{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:03:33Z","timestamp":1777125813184,"version":"3.51.4"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2005,7,18]],"date-time":"2005-07-18T00:00:00Z","timestamp":1121644800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2005,8]]},"DOI":"10.1007\/s00153-005-0282-2","type":"journal-article","created":{"date-parts":[[2005,7,18]],"date-time":"2005-07-18T09:46:45Z","timestamp":1121680005000},"page":"711-749","source":"Crossref","is-referenced-by-count":19,"title":["Quantified propositional calculus and a second-order theory for NC1"],"prefix":"10.1007","volume":"44","author":[{"given":"Stephen","family":"Cook","sequence":"first","affiliation":[]},{"given":"Tsuyoshi","family":"Morioka","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,7,18]]},"reference":[{"key":"282_CR1","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/S0168-0072(99)00041-X","volume":"103","author":"Arai","year":"2000","unstructured":"Arai, T.: A bounded arithmetic AID for Frege systems. Ann. Pure Appl. Logic 103, 155\u2013199 (2000)","journal-title":"Ann. Pure Appl. Logic"},{"key":"282_CR2","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1016\/0022-0000(90)90022-D","volume":"41","author":"Barrington","year":"1990","unstructured":"Barrington, D.A.M., Immerman, N., Straubing, H.: On Uniformity within NC1. J. Comput. Syst. Sci. 41, 274\u2013306 (1990)","journal-title":"J. Comput. Syst. Sci."},{"key":"282_CR3","unstructured":"Buss, : Bounded Arithmetic. Bibliopolis, 1986"},{"key":"282_CR4","doi-asserted-by":"crossref","unstructured":"Buss, : The Boolean formula value problem is in ALOGTIME. Proceedings of the 19th Annual ACM Symposium on Theory of Computing (STOC\u201987). 1987, pp. 123\u2013131","DOI":"10.1145\/28395.28409"},{"key":"282_CR5","doi-asserted-by":"crossref","unstructured":"Buss, S.: Axiomatizations and conservation results for fragments of bounded arithmetic. In: Logic and Computation, Proceedings of a Workshop held at Carnegie Mellon University. AMS, 1990, pp. 57\u201384","DOI":"10.1090\/conm\/106\/1057816"},{"key":"282_CR6","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0168-0072(91)90036-L","volume":"52","author":"Buss","year":"1991","unstructured":"Buss, S.: Propositional consistency proofs. Ann. Pure Appl. Logic 52, 3\u201329 (1991)","journal-title":"Ann. Pure Appl. Logic"},{"key":"282_CR7","doi-asserted-by":"crossref","unstructured":"Buss, S.: Algorithms for Boolean formula evaluation and for tree-contraction. In: P. Clote, J. Krajicek (eds.), Proof Theory, Complexity, and Arithmetic. Oxford University Press, 1993, pp. 95\u2013115","DOI":"10.1093\/oso\/9780198536901.003.0005"},{"key":"282_CR8","doi-asserted-by":"crossref","unstructured":"Buss, S.: First-order proof theory of arithmetic. In: S. Buss (ed.), Handbook of Proof Theory. Elsevier, 1998, pp. 79\u2013147. Available on line at http:\/\/www.math.ucsd.edu\/~sbuss\/ResearchWeb\/","DOI":"10.1016\/S0049-237X(98)80017-7"},{"key":"282_CR9","doi-asserted-by":"crossref","unstructured":"Buss, : An introduction to proof theory. In: S. Buss (ed.), Handbook of Proof Theory. Elsevier, 1998, pp. 1\u201378. Available on line at http:\/\/www.math.ucsd.edu\/~sbuss\/ResearchWeb\/","DOI":"10.1016\/S0049-237X(98)80016-5"},{"key":"282_CR10","unstructured":"Buss, S.: 2003. Personnal communication"},{"key":"282_CR11","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BF01845704","volume":"35","author":"Buss","year":"1996","unstructured":"Buss, S., Clote, P.: Cutting planes, connectivity, and threshold logic. Arch. Math. Logic 35, 33\u201362 (1996)","journal-title":"Arch. Math. Logic"},{"key":"282_CR12","first-page":"1","volume":"60","author":"Buss","year":"3","unstructured":"Buss, S., Krajicek, J.: An application of Boolean complexity to separation problems in bounded arithmetic. The Proceedings of the London Mathematical Society 60 (3), 1\u201321 (1994)","journal-title":"The Proceedings of the London Mathematical Society"},{"key":"282_CR13","doi-asserted-by":"crossref","first-page":"1095","DOI":"10.2307\/2586729","volume":"63","author":"Chiari","year":"1998","unstructured":"Chiari, M., Krajicek, J.: Witnessing functions in bounded arithmetic and search problems. The J. Symbolic Logic 63, 1095\u20131115 (1998)","journal-title":"The J. Symbolic Logic"},{"key":"282_CR14","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/BF01531023","volume":"6","author":"Clote","year":"1990","unstructured":"Clote, P.: ALOGTIME and a conjecture of S.A. Cook. Ann. Math. Art. Intell. 6, 57\u2013106 (1990). Extended abstract in Proc. 13th IEEE Symposium on Logic in Computer Science, 1990","journal-title":"A. Cook. Ann. Math. Art. Intell."},{"key":"282_CR15","doi-asserted-by":"crossref","unstructured":"Clote, P. Sequential, machine-independent characterizations of the parallel complexity classes AlogTIME,ACk,NCk and NC. In: S. Buss, P. Scott (eds), Feasible Mathematics. Birkhauser, 1990, pp. 49\u201369","DOI":"10.1007\/978-1-4612-3466-1_4"},{"key":"282_CR16","unstructured":"Cook, S.: Csc 2429 course notes: Proof complexity and bounded arithmetic, 2002. Available from the web at http:\/\/www.cs.toronto.edu\/~sacook\/csc2429h\/+"},{"key":"282_CR17","unstructured":"Cook, : Theories for complexity classes and their propositional translations. In: J. Krajicek (ed.), Complexity of Computations and Proofs. Quaderni di Matematica, 2003, pp. 175\u2013227"},{"key":"282_CR18","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/S0168-0072(03)00056-3","volume":"124","author":"Cook","year":"2003","unstructured":"Cook, S., Kolokolova, A.: A second-order system for polytime reasoning based on Gr\u00e4del\u2019s theorem. Ann. Pure Appl. Logic 124, 193\u2013231 (2003)","journal-title":"Ann. Pure Appl. Logic"},{"key":"282_CR19","unstructured":"Cook, S., Thapen, N.: The strength of replacement in weak arithmetic. ACM Transactions on Computational Logic. 2005, pp. 1\u201316 (in Press)"},{"key":"282_CR20","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"Cook","year":"1","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symbolic Logic 44 (1), 36\u201350 (1977)","journal-title":"J. Symbolic Logic"},{"key":"282_CR21","doi-asserted-by":"crossref","unstructured":"Immerman, N.: Descriptive Complexity. Springer, 1999","DOI":"10.1007\/978-1-4612-0539-5"},{"key":"282_CR22","doi-asserted-by":"crossref","unstructured":"Johnson, D.S.: A catalog of complexity classes. In: J. van Leewen (ed.), Handbook of Theoretical Computer Science. Elsevier Science Publishers, 1990, pp. 67\u2013161","DOI":"10.1016\/B978-0-444-88071-0.50007-2"},{"key":"282_CR23","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0022-0000(88)90046-3","volume":"37","author":"Johnson","year":"1988","unstructured":"Johnson, D.S., Papadimitriou, C.H., Yannakakis, M.: How easy is local search? J. Comput. Syst. Sci. 37, 79\u2013100 (1988)","journal-title":"Comput. Syst. Sci."},{"key":"282_CR24","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1016\/0168-0072(90)90023-U","volume":"48","author":"Kraj\u00ed\u010dek","year":"1990","unstructured":"Kraj\u00ed\u010dek, J.: Exponentiation and second-order bounded arithmetic. Ann. Pure Appl. Logic 48, 261\u2013276 (1990)","journal-title":"Ann. Pure Appl. Logic"},{"key":"282_CR25","doi-asserted-by":"crossref","first-page":"587","DOI":"10.1090\/S0002-9947-1993-1124169-X","volume":"338","author":"Krajicek","year":"2","unstructured":"Krajicek, J.: Fragments of Bounded Arithmetic and Bounded Query Classes. Transactions of the American Mathematical Society 338 (2), 587\u2013598 (1993)","journal-title":"Transactions of the American Mathematical Society"},{"key":"282_CR26","doi-asserted-by":"crossref","unstructured":"Kraj\u00ed\u010dek, J.: Bounded Arithmetic, Propositional Logic and Computational Complexity. Cambridge University Press, 1995","DOI":"10.1017\/CBO9780511529948"},{"key":"282_CR27","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1002\/malq.19900360106","volume":"36","author":"Kraj\u00ed\u010dek","year":"1990","unstructured":"Kraj\u00ed\u010dek, J., Pudl\u00e1k, P.: Quantified propositional calculi and fragments of bounded arithmetic. Zeitschrift f. Mathematische Logik u. Grundlagen d. Mathematik 36, 29\u201346 (1990)","journal-title":"Zeitschrift f. Mathematische Logik u. Grundlagen d. Mathematik"},{"key":"282_CR28","unstructured":"Morioka, : Logical approaches to the complexity of search problems: Proof complexity, quantified propositional calculus, and bounded arithmetic. PhD thesis, Department of Computer Science, University of Toronto, 2005"},{"key":"282_CR29","unstructured":"Nguyen, P.: Proving that VNC1 is finitely axiomatizable. unpublished note, 2004"},{"key":"282_CR30","unstructured":"Pitassi, T.: Using hardness to prove Frege lower bounds, 2002. A seminar at the Fields Institute for Research in Mathematical Sciences, Toronto, Canada"},{"key":"282_CR31","doi-asserted-by":"crossref","unstructured":"Pollett, C.: A propositional proof systems for Ri2. In: P. Beame, S. Buss (eds.), Proof Complexity and Feasible Arithmetics, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, The American Mathematical Society, 1997, pp. 253\u2013278","DOI":"10.1090\/dimacs\/039\/14"},{"key":"282_CR32","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/S0168-0072(99)00008-1","volume":"100","author":"Pollett","year":"1999","unstructured":"Pollett, C.: Structure and Definability in General Bounded Arithmetic Theories. Ann. Pure Appl. Logic 100, 189\u2013245 (1999)","journal-title":"Ann. Pure Appl. Logic"},{"key":"282_CR33","unstructured":"Razborov, A.A.: An equivalence between second order bounded domain bounded arithmetic and first order bounded arithmetic. In: P. Clote, J. Krajicek (eds.), Arithmetic, Proof Theory and Computational Complexity. Oxford University Press, 1993, pp. 247\u201377"},{"key":"282_CR34","unstructured":"Skelley, A.: Personal communication., 2002"},{"key":"282_CR35","unstructured":"Takeuti, G.: Proof Theory. Elsevier Science Publisers, second edition, 1987"},{"key":"282_CR36","doi-asserted-by":"crossref","unstructured":"Takeuti, G.: RSUV isomorphism. In: P. Clote, J. Krajicek (eds.), Arithmetic, Proof Theory and Computational Complexity. Oxford University Press, 1993, pp. 364\u201386","DOI":"10.1093\/oso\/9780198536901.003.0016"},{"key":"282_CR37","doi-asserted-by":"crossref","first-page":"942","DOI":"10.2307\/2275794","volume":"61","author":"Zambella","year":"3","unstructured":"Zambella, D.: Notes on polynomially bounded arithmetic. J. Symbolic Logic 61 (3), 942\u2013966 (1996)","journal-title":"J. Symbolic Logic"}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-005-0282-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00153-005-0282-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-005-0282-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,27]],"date-time":"2024-01-27T22:40:48Z","timestamp":1706395248000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00153-005-0282-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,7,18]]},"references-count":37,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2005,8]]}},"alternative-id":["282"],"URL":"https:\/\/doi.org\/10.1007\/s00153-005-0282-2","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,7,18]]}}}