1. Ajtai, Miklós. 1994. “The complexity of the pigeonhole principle”. Combinatorica 14: 417-433. DOI: 10.1007/BF01302964
2. Beame, Paul and Impagliazzo, Russell and and Pitassi, Toniann. 1993. “Exponential lower bounds for the pigeonhole principle” . Computational Complexity 3: 97-140. DOI: 10.1007/BF01200117
3. Beckmann, Arnold and Buss, Samuel R.2011. “Corrected upper bounds for free-cut elimina- tion”. Theoretical Computer Science 412 (39): 5433-5445 DOI: 10.1016/j.tcs.2011.05.053
4. Beckmann, Arnold and Pollett, Chris and Buss, Samuel R. 2003. “Ordinal notations and well- orderings in bounded arithmetic”. Annals of Pure and Applied Logic 120, (1–3): 197-223, DOI: 10.1016/s0168-0072(02)00066-0
5. Buss, Samuel R. 1986. Bounded Arithmetic. Napoli: Bibliopolis.
6. Buss, Samuel. 1985. “The polynomial hierarchy and intuitionistic Bounded Arithmetic” . Structure in Complexity Theory: 77-103. DOI: 10.1145/22145.22177
7. Buss, Samuel R. 1998. “An introduction to proof theory”. In Handbook of proof theory, 1-78. Amsterdam: Elsevier. DOI: 10.2307/420968
8. Buss, Samuel R. 1999. “Bounded arithmetic, proof complexity and two papers of Parikh” . Annals of Pure and Applied Logic 96 (1-3): 43-55. DOI: 10.1016/S0168-0072(98)00030-X
9. Buss, Samuel R. and Krajícek, Jan. 1994. “An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic” . Proceedings of The London Mathematical Society: 1-21. DOI: 10.1112/plms/s3-69.1.1
10. Buss, Samuel R. and Krajíček, Jan and Takeuti, Gaisi. 1993. “Provably total functions in the bounded arithmetic theories R 3 i , U 2 i , and V 2 i ” . In Proof Theory, Arithmetic, and Complexity, edited by P. Clote and J. Krajíček, 116-161. Oxford: Oxford University Press. DOI: 10.1093/oso/9780198536901.003.0006
11. Cantini, Andrea. 1996. “Asymmetric Interpretations for Bounded Theories” . Mathematical Logic Quarterly 42: 270-288. DOI: 10.1002/malq.19960420123
12. Cook, Stephen and Nguyen, Phuong. 2010. Logical Foundations of Proof Complexity . Cam- bridge: Cambridge University Press. DOI: 10.2178/bsl/1309952322
13. Cook, Stephen and Urquhart, Alisdair. 1993. “Functional interpretations of feasibly constructive arithmetic” . Annals of Pure and Applied Logic 63 (2): 103-200. DOI: 10.1016/0168-0072(93)90044-E
14. Ferreira, Fernando and Ferreira, Gilda. 2013. “Interpretability in Robinson’s Q”. The Bulletin of Symbolic Logic 19: 289-317. DOI: 10.1017/S1079898600010660
15. Girard, Jean Yves. 1987. Proof-theory and logical complexity I. Napoli: Bibliopolis.
16. Girard, Jean-Yves and Lafont, Yves and Taylor, Paul. 1989. Proofs and types. Cambridge: Cambridge University Press. DOI: 10.2307/2274726
17. Gentzen, Gerhard. 1935. “Untersuchungen über das logische Schließen” . Mathematische Zeitschrift 39: 176-210 and 405-431. DOI: 10.1007/BF01201353
18. Harnik, Victor. 1992. “Provably Total Functions of Intuitionistic Bounded Arithmetic”. The Journal of Symbolic Logic 57 (2): 466-477. DOI: 10.2307/2275282
19. Hájek, Peter and Pudlák, Pavel. 1993. Metamathematics of first order arithmetic. Berlin: Springer. DOI: 10.1007/978-3-662-22156-3
20. Herbrand, Jacques. 1930. “Recherches sur la théorie de la démonstration”. Travaux de la société des Sciences et des Lettres de Varsovie, Class III, Sciences Mathématiques et Physiques 33: 1-131. DOI: 10.3917/puf.herbr.1968.01.0035
21. Ketonen, Jussi and Solovay, Robert. 1981. “Rapidly Growing Ramsey Functions”. Annals of Mathematics 113 (2): 267-314. DOI: 10.1007/978-3-319-01315-2_8
22. Krajíček, Jan. 1995. Bounded arithmetic, propositional logic, and complexity theory. Cam- bridge: Cambridge University Press. DOI: 10.1017/CBO9780511529948
23. Parikh, Rohit. 1971. “Existence and Feasibility.” The Journal of Symbolic Logic 36 (3): 494-508. DOI: 10.2307/2269958
24. Paris, Jeff and Dimitracopoulos, Costas. 1983, “A Note on the Undefinability of Cuts”. The Journal of Symbolic Logic 48: 564-569. DOI: 10.2307/2273447
25. Razborov, Alexander A. 1993. “An equivalence between second order bounded domain bounded arithmetic and first order bounded arithmetic.” In P. Clote and J. Krajicek (editors) Arith- metic, Proof Theory and Computational Complexity 247-277. Oxford: Oxford University Press. DOI: 10.1093/oso/9780198536901.003.0012
26. Tait, William W. 1968. “Normal derivability in classical logic”. In The Syntax and Semantics of Infinitatry Languages. Lecture Notes in Mathematics 72, edited by J. Barwise, 204-236. Berlin: Springer. DOI: 10.1007/BFb0079691
27. Takeuti, Gaisi. 1987. Proof Theory. Amsterdam: North Holland (Reprint Courier Corporation, 2013).
28. Takeuti, Gaisi. 1993. “RSUV isomorphism.” In Arithmetic, Proof Theory and Computational Complexity, edited by P. Clote and J. Krajicek, 364-386. Oxford: Oxford University.
29. Troelstra, Anne S. and Schwichtenberg, Helmut. 2000. Basic proof theory. Cambridge: Cam- bridge University Press. DOI: 10.1017/cbo9781139168717
30. Verbrugge, Rineke. 1993. Efficient Metamathematics. Dissertation, Universiteit Van Amsterdam
31. Urban, Christian and Bierman, Gavin M. 2001. “Strong Normalisation of Cut-Elimination in Classical Logic.”Fundamenta Informaticae 45 (1-2): 123-155. DOI: 10.1007/3-540-45413-6_32
32. Wilkie, Alex J. and Paris, Jeff B. “On the scheme of induction for bounded arithmetic formulas”. Annals of Pure and Applied Logic 35 : 261-302. DOI: 10.1016/0168-0072(87)90066-2
33. Zambella, Domenico. 1996. “Notes on Polynomially Bounded Arithmetic”. The Journal of Symbolic Logic 61 (3): 942-966. DOI: 10.2307/2275794

Chapter Information

Bibliographic Information