{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:18:41Z","timestamp":1742617121985,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540601784"},{"type":"electronic","value":"9783540447207"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60178-3_87","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:48:55Z","timestamp":1330278535000},"page":"221-252","source":"Crossref","is-referenced-by-count":0,"title":["Frege proof system and TNC\u00b0"],"prefix":"10.1007","author":[{"given":"Gaisi","family":"Takeuti","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"D. A. Mix Barrington, N. Immerman and H. Straubing, On uniform with NC1, Structure in Complexity Theory, Third Annual Conf., IEEE Computer Society Press (1988) pp. 47\u201359, to appear in J. Comp. Syst. Sci.","key":"12_CR1","DOI":"10.1109\/SCT.1988.5262"},{"unstructured":"S. R. Buss, Bounded Arithmetic, Napoli, Bibliopolis 1986.","key":"12_CR2"},{"doi-asserted-by":"crossref","unstructured":"-, The Boolean formula value problem is in ALOGTIME, In Proceedings of the 19-th Annual ACM Symposium on Theory of Computing, pp. 123\u2013131, 1987.","key":"12_CR3","DOI":"10.1145\/28395.28409"},{"key":"12_CR4","first-page":"66","volume":"52","author":"S. R. Buss","year":"1987","unstructured":"-, Polynomial size proofs of the propositional pigeonhole principle, J. Symbolic Logic 52 (1987), 66\u201392.","journal-title":"J. Symbolic Logic"},{"unstructured":"-, Algorithms for Boolean formula evaluation and for tree-contraction, In Proof Theory, Complexity and Arithmetic (P. Clote and J. Kraj\u00ed\u010dek, eds.), Oxford University Press, pp. 95\u2013115.","key":"12_CR5"},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0168-0072(91)90036-L","volume":"52","author":"S. R. Buss","year":"1991","unstructured":"-, Propositional consistency proofs, Annals of Pure and Applied Logic 52 (1991), 3\u201329.","journal-title":"Annals of Pure and Applied Logic"},{"key":"12_CR7","doi-asserted-by":"publisher","first-page":"755","DOI":"10.1137\/0221046","volume":"21","author":"S. R. Buss","year":"1992","unstructured":"S. R. Buss, S. A. Cook, A. Gupta and V. Ramachandran, An optimal parallel algorithm for formula evaluation, SIAM J. on Computing 21 (1992), 755\u2013780.","journal-title":"SIAM J. on Computing"},{"doi-asserted-by":"crossref","unstructured":"P. Clote, Sequential, machine-independent characterizations of the parallel complexity classes ALOGTIME, ACk, NCk and NC, Feasible Mathematics (S. R. Buss and P. Scott, eds.), Birkh\u00e4user, 1990, pp. 49\u201370.","key":"12_CR8","DOI":"10.1007\/978-1-4612-3466-1_4"},{"key":"12_CR9","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/BF01531023","volume":"6","author":"P. Clote","year":"1992","unstructured":"P. Clote, ALOGTIME and a conjecture of S. A. Cook, Annals of Mathematics and Artificial Intelligence 6 (1992), 57\u2013106, extended abstract in proceedings of IEEE Logic in Computer Science, Philadelphia, June 1990.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"doi-asserted-by":"crossref","unstructured":"P. Clote and G. Takeuti, First order bounded arithmetic and small boolean circuit compleity class, in Feasible Mathematics II (P. Clote and J. Remmel, eds.), Birkh\u00e4user, 1995, pp. 154\u2013218.","key":"12_CR10","DOI":"10.1007\/978-1-4612-2566-9_6"},{"doi-asserted-by":"crossref","unstructured":"S. A. Cook, Feasibly constructive proofs and the propositional calculus, Proc. 7-th ACM Symp. on the Theory of Computation (1975), 83\u201397.","key":"12_CR11","DOI":"10.1145\/800116.803756"},{"key":"12_CR12","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"S. A. Cook","year":"1977","unstructured":"S. A. Cook and R. Reckhow, The relative efficiency of propositional proof systems, J. Symbolic Logic 44 (1977), 36\u201350.","journal-title":"J. Symbolic Logic"},{"unstructured":"M. Dowd, Propositional representation of arithmetical proofs, Ph.D. Dissertation, University of Toronto, Department of Computer Science Technical Report 132\/79, April 1979.","key":"12_CR13"},{"doi-asserted-by":"crossref","unstructured":"M. Karchmer, Communication Complexity: A New Approach to Circuit Depth, The MIT Press, 1989.","key":"12_CR14","DOI":"10.7551\/mitpress\/1948.001.0001"},{"doi-asserted-by":"crossref","unstructured":"M. Karchmer and A. Wigderson, Monotone circuits for connectiveity require sur-logarithmic depth, Proc. 20-th Annual ACM symp. on Theory of Computation, ACM Press, 1988, pp. 539\u2013550.","key":"12_CR15","DOI":"10.1145\/62212.62265"},{"doi-asserted-by":"crossref","unstructured":"J. Kraj\u00ed\u010dek, On Frege and Extended Frege Proof Systems, Feasible Mathematics II (P. Clote and J. Remmel, eds.), Birkh\u00e4ser, 1995, pp. 284\u2013319.","key":"12_CR16","DOI":"10.1007\/978-1-4612-2566-9_10"},{"unstructured":"-, Bounded Arithmetic, Propositional Logic and Complexity Theory, Cambridge University Press (to appear).","key":"12_CR17"},{"key":"12_CR18","doi-asserted-by":"crossref","first-page":"1063","DOI":"10.2307\/2274765","volume":"54","author":"J. Kraj\u00ed\u010dek","year":"1989","unstructured":"J. Kraj\u00ed\u010dek and P. Publ\u00e1k, Propositional proof systems, the consistency of first order theories and the complexity of computations, J. Symbolic Logic 54 (1989), 1063\u20131079.","journal-title":"J. Symbolic Logic"},{"doi-asserted-by":"crossref","unstructured":"R. Raz and A. Wigderson, Monotone circuits for matching require linear depth, Proc. 22nd Ann. ACM Symp. on Theory of Computing (1990), 287\u2013292.","key":"12_CR19","DOI":"10.1145\/100216.100253"},{"issue":"4","key":"12_CR20","first-page":"798","volume":"281","author":"A. A. Razborov","year":"1985","unstructured":"A. A. Razborov, Lower bounds on the monotone complexity of some Boolean functions, Dokl. Akad. Nauk SSSR 281(4) (1985), 798\u2013801; English translation in: Soviet Math. Dokl. 31 (1985), 345\u2013357.","journal-title":"Dokl. Akad. Nauk SSSR"},{"unstructured":"R. A. Reckhow, On the lengths of proofs in the proposition calculus, Ph.D. Thesis 1976, Department of Computer Science, University of Toronto, Technical Report 87.","key":"12_CR21"},{"key":"12_CR22","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BF01621092","volume":"29","author":"G. Takeuti","year":"1990","unstructured":"G. Takeuti, S 3 i and V 2 i (BD), Archive for Mathematical Logic 29 (1990), 149\u2013169.","journal-title":"Archive for Mathematical Logic"},{"doi-asserted-by":"crossref","unstructured":"-, RSUV Isomorphisms, Arithmetic, Proof Theory and Computational Complexity (P. Clote and J. Kraj\u00ed\u010dek, eds.), Oxford Univ. Press, 1993, pp. 364\u2013386.","key":"12_CR23","DOI":"10.1093\/oso\/9780198536901.003.0016"},{"unstructured":"-, RSUV Isomorphisms for TAC i , TNC i and TLS (to appearArchive for Mathematical Logic).","key":"12_CR24"}],"container-title":["Lecture Notes in Computer Science","Logic and Computational Complexity"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60178-3_87.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:54:57Z","timestamp":1742597697000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60178-3_87"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540601784","9783540447207"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-60178-3_87","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}