{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T01:24:10Z","timestamp":1755221050376,"version":"3.43.0"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2000,12,1]],"date-time":"2000-12-01T00:00:00Z","timestamp":975628800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,12,1]],"date-time":"2000-12-01T00:00:00Z","timestamp":975628800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Synthese"],"published-print":{"date-parts":[[2000,12]]},"DOI":"10.1023\/a:1005244027724","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T16:13:47Z","timestamp":1040487227000},"page":"385-416","source":"Crossref","is-referenced-by-count":2,"title":["Looking From The Inside And From The Outside"],"prefix":"10.1007","volume":"125","author":[{"given":"A.","family":"Carbone","sequence":"first","affiliation":[]},{"given":"S.","family":"Semmes","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"261884_CR1","volume-title":"Conformal Invariants: Topics in Geometric Function Theory","author":"L. Ahlfors","year":"1973","unstructured":"Ahlfors, L.: 1973, Conformal Invariants: Topics in Geometric Function Theory, McGraw-Hill, New York."},{"key":"261884_CR2","doi-asserted-by":"crossref","DOI":"10.1515\/9781400874538","volume-title":"Riemann Surfaces","author":"L. Ahlfors","year":"1960","unstructured":"Ahlfors, L. and L. Sario: 1960, Riemann Surfaces, Princeton University Press, Princeton."},{"key":"261884_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3951-0","volume-title":"Differential Forms in Algebraic Topology","author":"R. Bott","year":"1982","unstructured":"Bott, R. and L. Tu: 1982, Differential Forms in Algebraic Topology, Springer-Verlag, Berlin."},{"key":"261884_CR4","doi-asserted-by":"crossref","first-page":"916","DOI":"10.2307\/2273826","volume":"52","author":"S. Buss","year":"1987","unstructured":"Buss, S.: 1987, 'Polynomial Size Proofs of the Propositional Pigeonhole Principle', Journal of Symbolic Logic\n52, 916\u201327.","journal-title":"Journal of Symbolic Logic"},{"key":"261884_CR5","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0168-0072(91)90059-U","volume":"53","author":"S. Buss","year":"1991","unstructured":"Buss, S.: 1991, 'The Undecidability of k-Provability', Annals of Pure and Applied Logic\n53, 75\u2013102.","journal-title":"Annals of Pure and Applied Logic"},{"key":"261884_CR6","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/S0168-0072(96)00019-X","volume":"83","author":"A. Carbone","year":"1997","unstructured":"Carbone, A.: 1997, 'Interpolants, Cut Elimination and Flow Graphs for the Propositional Calculus', Annals of Pure and Applied Logic\n83, 249\u201399.","journal-title":"Annals of Pure and Applied Logic"},{"key":"261884_CR7","doi-asserted-by":"crossref","first-page":"2049","DOI":"10.1090\/S0002-9947-99-02300-4","volume":"352","author":"A. Carbone","year":"2000","unstructured":"Carbone, A.: 2000a, 'Cycling in Proofs and Feasibility', Transactions of the American Mathematical Society\n352, 2049\u20132075.","journal-title":"Transactions of the American Mathematical Society"},{"key":"261884_CR8","unstructured":"Carbone, A.: 2000b, 'Some Combinatorics behind Proofs', (submitted)."},{"key":"261884_CR9","doi-asserted-by":"crossref","unstructured":"Carbone, A.: 2000c, 'Asymptotic Cyclic Expansion and Bridge Groups of Formal Proofs', (submitted).","DOI":"10.1006\/jabr.2000.8700"},{"key":"261884_CR10","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1090\/S0273-0979-97-00715-5","volume":"34","author":"A. Carbone","year":"1997","unstructured":"Carbone, A. and S. Semmes: 1997, 'Making Proofs Without Modus Ponens: An Introduction to the Combinatorics and Complexity of Cut Elimination', Bulletin of the American Mathematical Society\n34, 131\u201359.","journal-title":"Bulletin of the American Mathematical Society"},{"key":"261884_CR11","first-page":"85","volume-title":"Collegium Logicum","author":"A. Carbone","year":"1999","unstructured":"Carbone, A. and S. Semmes: 1999, 'Propositional Proofs via Combinatorial Geometry and the Search for Symmetry', in Collegium Logicum, Annals of the Kurt-G\u00f6del-Society, Volume 3, pp. 85\u201398, Institute for Computer Science AS CR, Prague."},{"key":"261884_CR12","volume-title":"A Graphic Apology for Symmetry and Implicitness \u2013 Combinatorial Complexity of Proofs, Languages, and Geometric Constructions","author":"A. Carbone","year":"2000","unstructured":"Carbone, A. and S. Semmes: 2000, A Graphic Apology for Symmetry and Implicitness \u2013 Combinatorial Complexity of Proofs, Languages, and Geometric Constructions, forthcoming, Oxford University Press, Oxford."},{"key":"261884_CR13","volume-title":"Information, Randomness & Incompleteness \u2013 Papers on Algorithmic Information Theory","author":"G. Chaitin","year":"1987","unstructured":"Chaitin, G.: 1987, Information, Randomness & Incompleteness \u2013 Papers on Algorithmic Information Theory, World Scientific, Singapore."},{"key":"261884_CR14","doi-asserted-by":"crossref","DOI":"10.1142\/1861","volume-title":"Information-Theoretic Incompleteness","author":"G. Chaitin","year":"1992","unstructured":"Chaitin, G.: 1992, Information-Theoretic Incompleteness, World Scientific, Singapore."},{"key":"261884_CR15","volume-title":"Noncommutative Geometry","author":"A. Connes","year":"1994","unstructured":"Connes, A.: 1994, Noncommutative Geometry, Academic Press, New York."},{"key":"261884_CR16","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"S. Cook","year":"1979","unstructured":"Cook, S. and R. Reckhow: 1979, 'The Relative Efficiency of Propositional Proof Systems', Journal of Symbolic Logic\n44, 36\u201350.","journal-title":"Journal of Symbolic Logic"},{"key":"261884_CR17","doi-asserted-by":"crossref","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: 1957, 'Three Uses of the Herbrand-Gentzen Theorem in RelatingModel Theory and Proof Theory', Journal of Symbolic Logic\n22, 269\u201385.","journal-title":"Journal of Symbolic Logic"},{"key":"261884_CR18","doi-asserted-by":"crossref","DOI":"10.1201\/9781439865699","volume-title":"Word Processing in Groups","author":"D. Epstein","year":"1992","unstructured":"Epstein, D., J. Cannon, D. Holt, M. Paterson, and W. Thurston: 1992, Word Processing in Groups, Jones and Bartlett, Boston."},{"key":"261884_CR19","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"M. Garey","year":"1979","unstructured":"Garey, M. and D. Johnson: 1979, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, New York."},{"key":"261884_CR20","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"Gentzen, G.: 1934, 'Untersuchungen \u00fcber das Logische Schlie\u00dfen I-II', Mathematische Zeitschrift\n39, 176\u2013210, 405\u201331.","journal-title":"Mathematische Zeitschrift"},{"key":"261884_CR21","volume-title":"The Collected Papers of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"Gentzen, G.: 1969, in M. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam."},{"key":"261884_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: 1987a, 'Linear Logic', Theoretical Computer Science\n50, 1\u2013102.","journal-title":"Theoretical Computer Science"},{"key":"261884_CR23","volume-title":"Proof Theory and Logical Complexity","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: 1987b, Proof Theory and Logical Complexity, Bibliopolis, Napoli."},{"key":"261884_CR24","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1090\/conm\/092\/1003197","volume-title":"Categories in Computer Science and Logic","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y.: 1989a, 'Towards a Geometry of Interaction', in J. Gray and A. Scedrov (eds), Categories in Computer Science and Logic, American Mathematical Society, Providence, pp. 69\u2013108."},{"key":"261884_CR25","first-page":"221","volume-title":"Logic Colloquium '88","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y.: 1989b, 'Geometry of Interaction I: Interpretation of System F', in R. Ferro, C. Bonotto, S. Valentini, and A. Zanardo (eds), Logic Colloquium '88, North Holland, Amsterdam, pp. 221\u201360."},{"key":"261884_CR26","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/3-540-52335-9_49","volume-title":"COLOG-88","author":"J.-Y. Girard","year":"1990","unstructured":"Girard, J.-Y.: 1990, 'Geometry of Interaction II: Deadlock-Free Algorithms', in P. Martin-L\u00f6f and G. Mints (eds), COLOG-88, Springer-Verlag, Berlin, pp. 76\u201393."},{"key":"261884_CR27","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1017\/CBO9780511629150.017","volume-title":"Advances in Linear Logic","author":"J.-Y. Girard","year":"1995","unstructured":"Girard, J.-Y.: 1995, 'Geometry of Interaction III: Accommodating the Additives', in J.-Y. Girard, Y. Lafont, and L. Regnier (eds), Advances in Linear Logic, Cambridge University Press, Cambridge, pp. 329\u201389."},{"key":"261884_CR28","first-page":"1","volume-title":"Geometric Group Theory","author":"M. Gromov","year":"1993","unstructured":"Gromov, M.: 1993, 'Asymptotic Invariants of Infinite Groups', in G. Niblo and M. Roller (eds), Geometric Group Theory, Volume 2, Cambridge University Press, Cambridge, pp. 1\u2013295."},{"key":"261884_CR29","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A.: 1985, 'The Intractability of Resolution', Theoretical Computer Science\n39, 297\u2013308.","journal-title":"Theoretical Computer Science"},{"key":"261884_CR30","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-9855-7","volume-title":"Lectures on Boolean Algebras","author":"P. Halmos","year":"1974","unstructured":"Halmos, P.: 1974, Lectures on Boolean Algebras, Springer-Verlag, Berlin."},{"key":"261884_CR31","first-page":"67","volume-title":"Handbook of Theoretical Computer Science, Volume A: Algorithms and Complexity","author":"D. Johnson","year":"1990","unstructured":"Johnson, D.: 1990, 'A Catalog of Complexity Classes', in J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Volume A: Algorithms and Complexity, Elsevier and MIT Press, Amsterdam and Cambridge, MA, pp. 67\u2013161."},{"key":"261884_CR32","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511623929","volume-title":"Complex Algebraic Curves","author":"F. Kirwan","year":"1992","unstructured":"Kirwan, F.: 1992, Complex Algebraic Curves, Cambridge University Press, Cambridge."},{"issue":"5","key":"261884_CR33","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1109\/TIT.1968.1054210","volume":"14","author":"A. Kolmogorov","year":"1968","unstructured":"Kolmogorov, A.: 1968, 'Logical Basis for Information Theory and Probability Theory', IEEE Transactions on Information Theory\n14(5), 662\u201364.","journal-title":"IEEE Transactions on Information Theory"},{"key":"261884_CR34","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4752-4","volume-title":"Elliptic Functions","author":"S. Lang","year":"1987","unstructured":"Lang, S.: 1987, Elliptic Functions, Springer-Verlag, Berlin."},{"key":"261884_CR35","first-page":"187","volume-title":"Handbook of Theoretical Computer Science, Volume A: Algorithms and Complexity","author":"M. Li","year":"1990","unstructured":"Li, M. and P. Vit\u00e1nyi: 1990, 'Kolmogorov Complexity and its Applications', in J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Volume A: Algorithms and Complexity, Elsevier and MIT Press, Amsterdam and Cambridge, MA, pp. 187\u2013254."},{"key":"261884_CR36","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4939-9063-4","volume-title":"A Basic Course in Algebraic Topology","author":"W. Massey","year":"1991","unstructured":"Massey, W.: 1991, A Basic Course in Algebraic Topology, Springer-Verlag, Berlin."},{"key":"261884_CR37","doi-asserted-by":"crossref","first-page":"2337","DOI":"10.1007\/BF01629444","volume":"20","author":"V. Orevkov","year":"1982","unstructured":"Orevkov, V.: 1982, 'Lower Bounds for Increasing Complexity of Derivations after Cut Elimination', Journal of Soviet Mathematics\n20, 2337\u2013350.","journal-title":"Journal of Soviet Mathematics"},{"key":"261884_CR38","doi-asserted-by":"crossref","DOI":"10.1090\/mmono\/128","volume-title":"Complexity of Proofs and Their Transformations in Axiomatic Theories","author":"V. Orevkov","year":"1993","unstructured":"Orevkov, V.: 1993, in A. Bochman (trans.), D. Louvish (ed.), Complexity of Proofs and Their Transformations in Axiomatic Theories, American Mathematical Society, Providence."},{"key":"261884_CR39","doi-asserted-by":"crossref","first-page":"494","DOI":"10.2307\/2269958","volume":"36","author":"R. Parikh","year":"1971","unstructured":"Parikh, R.: 1971, 'Existence and Feasibility in Arithmetic', Journal of Symbolic Logic\n36, 494\u2013508.","journal-title":"Journal of Symbolic Logic"},{"key":"261884_CR40","doi-asserted-by":"crossref","first-page":"98","DOI":"10.2307\/2266510","volume":"14","author":"J. Robinson","year":"1949","unstructured":"Robinson, J.: 1949, 'Definability and Decision Problems in Arithmetic', Journal of Symbolic Logic\n14, 98\u2013114.","journal-title":"Journal of Symbolic Logic"},{"key":"261884_CR41","volume-title":"Functional Analysis","author":"W. Rudin","year":"1991","unstructured":"Rudin, W.: 1991, Functional Analysis, McGraw-Hill, New York."},{"key":"261884_CR42","doi-asserted-by":"crossref","first-page":"425","DOI":"10.2307\/1969485","volume":"54","author":"J.-P. Serre","year":"1951","unstructured":"Serre, J.-P.: 1951, 'Homologie Singuli\u00e8re des Espaces Fibr\u00e9s', Annals of Mathematics\n54, 425\u2013505.","journal-title":"Annals of Mathematics"},{"key":"261884_CR43","volume-title":"Introduction to Topology and Modern Analysis","author":"G. Simmons","year":"1963","unstructured":"Simmons, G.: 1963, Introduction to Topology and Modern Analysis, McGraw-Hill, New York."},{"key":"261884_CR44","unstructured":"Statman, R.: 1974, Structural Complexity of Proofs, doctoral dissertation, Stanford University."},{"key":"261884_CR45","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0003-4843(78)90011-6","volume":"15","author":"R. Statman","year":"1978","unstructured":"Statman, R.: 1978, 'Bounds for Proof-Search and Speed-Up in the Predicate Calculus', Annals of Mathematical Logic\n15, 225\u201387.","journal-title":"Annals of Mathematical Logic"},{"key":"261884_CR46","first-page":"104","volume":"75","author":"R. Statman","year":"1979","unstructured":"Statman, R.: 1979, 'Lower bounds on Herbrand's Theorem', Proceedings of the American Mathematical Society\n75, 104\u20137.","journal-title":"Proceedings of the American Mathematical Society"},{"key":"261884_CR47","volume-title":"Singular Integrals and Differentiability Properties of Functions","author":"E. Stein","year":"1970","unstructured":"Stein, E.: 1970, Singular Integrals and Differentiability Properties of Functions, Princeton University Press, Princeton."},{"key":"261884_CR48","volume-title":"Proof Theory","author":"G. Takeuti","year":"1975","unstructured":"Takeuti, G.: 1975, Proof Theory, North-Holland, Amsterdam."},{"key":"261884_CR49","first-page":"234","volume":"8","author":"G. Tseitin","year":"1968","unstructured":"Tseitin, G.: 1968, 'Complexity of a Derivation in the Propositional Calculus', Zap. Nauchn. Sem. Leningrad Otd. Mat. Inst. Akad. Nauk SSSR\n8, 234\u201359.","journal-title":"Zap. Nauchn. Sem. Leningrad Otd. Mat. Inst. Akad. Nauk SSSR"},{"key":"261884_CR50","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"Urquhart, A.: 1987, 'Hard Examples for Resolution', Journal of the Association for Computing Machinery\n34, 209\u201319.","journal-title":"Journal of the Association for Computing Machinery"},{"volume-title":"Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics","year":"1990","key":"261884_CR51","unstructured":"van Leeuwen, J. (ed.): 1990, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Elsevier and MIT Press, Amsterdam and Cambridge, MA."}],"container-title":["Synthese"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005244027724.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005244027724\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005244027724.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:57:00Z","timestamp":1754632620000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005244027724"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,12]]},"references-count":51,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2000,12]]}},"alternative-id":["261884"],"URL":"https:\/\/doi.org\/10.1023\/a:1005244027724","relation":{},"ISSN":["0039-7857","1573-0964"],"issn-type":[{"type":"print","value":"0039-7857"},{"type":"electronic","value":"1573-0964"}],"subject":[],"published":{"date-parts":[[2000,12]]}}}