{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2021,5,7]],"date-time":"2021-05-07T23:23:47Z","timestamp":1620429827091},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028010","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T07:02:06Z","timestamp":1132642926000},"page":"115-128","source":"Crossref","is-referenced-by-count":1,"title":["Linear lower bounds and simulations in frege systems with substitutions"],"prefix":"10.1007","author":[{"given":"Maria Luisa","family":"Bonet","sequence":"first","affiliation":[]},{"given":"Nicola","family":"Galesi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,15]]},"reference":[{"key":"7_CR1","first-page":"8","volume-title":"Invited talk at the Third South American Workshop on String Processing","author":"R. A. Baeza-Yates","year":"1996","unstructured":"R. A. Baeza-Yates, R. Gavald\u00e1, G. Navarro. Bounding the Expected Length of Longest Common Subsequences and Forest. Invited talk at the Third South American Workshop on String Processing (WSP'96), Recife (Brazil), Aug. 8\u20139 1996."},{"key":"7_CR2","unstructured":"M. Bonet. Number of symbols in Frege proofs with and without the deduction rule. In Arithmetic, proof theory and computational complexity. Oxford University Press Eds. P. Clote and J. Kraji\u010dek-1992."},{"key":"7_CR3","doi-asserted-by":"crossref","first-page":"688","DOI":"10.2307\/2275228","volume":"58","author":"M. Bonet","year":"1993","unstructured":"M. Bonet, S. Buss. The deduction rule and linear and near-linear proof simulations. Journal of Symbol Logic, 58 (1993) pp. 688\u2013709.","journal-title":"Journal of Symbol Logic"},{"key":"7_CR4","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/s001530050030","volume":"34","author":"S. Buss","year":"1995","unstructured":"S. Buss. Some remarks on length of propositional proofs. Archive for Mathematical Logic. 34 (1995) pp. 377\u2013394.","journal-title":"Archive for Mathematical Logic"},{"key":"7_CR5","unstructured":"S. Buss, Lectures on proof theory. TR SOCS-96.1 School of C.S.-Mc Gill University 1996."},{"key":"7_CR6","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"S. Cook","year":"1979","unstructured":"S. Cook, R. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44 (1979) pp. 36\u201350.","journal-title":"Journal of Symbolic Logic"},{"key":"7_CR7","unstructured":"J. H. Gallier. Logic for Computer Science-Foundations of Automatic Theorem Proving. J. Wiley & Sons. 1987"},{"key":"7_CR8","doi-asserted-by":"crossref","first-page":"90","DOI":"10.2307\/2274956","volume":"55","author":"J. R. Hindley","year":"1990","unstructured":"J. R. Hindley, D. Meredith. Principal type schemes and condensed detachment. Journal of Symbolic Logic, 55 (1990) pp. 90\u2013105.","journal-title":"Journal of Symbolic Logic"},{"key":"7_CR9","unstructured":"K. Iwana, T. Pitassi. Exponential Lower bounds for the tree-like Haj\u00f3s Calculus. Manuscript1997."},{"key":"7_CR10","first-page":"137","volume":"30","author":"J. Kraji\u010dek","year":"1989","unstructured":"J. Kraji\u010dek. Speed-up for propositional Frege systems via generalizations of proofs. Commentationes Mathernaticae Universiatatis Carolinae, 30 (1989) pp. 137\u2013140.","journal-title":"Commentationes Mathernaticae Universiatatis Carolinae"},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/0168-0072(89)90012-2","volume":"41","author":"J. Kraji\u010dek","year":"1989","unstructured":"J. Kraji\u010dek. On the number of steps in proof. Annals of Pure and Applied Logic, 41 (1989) pp. 153\u2013178.","journal-title":"Annals of Pure and Applied Logic"},{"key":"7_CR12","doi-asserted-by":"crossref","first-page":"1063","DOI":"10.2307\/2274765","volume":"54","author":"J. Kraji\u010dek","year":"1989","unstructured":"J. Kraji\u010dek, P. Pudl\u00e1k. Propositional proof systems, the consistency of first order theories and the complexity of computation. Journal of Symbolic Logic, 54 (1989) pp. 1063\u20131079ia.","journal-title":"Journal of Symbolic Logic"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"M.Li, P. Vitanyi. An Introduction to Kolmogorov Complexity and its Application. Springer-Verlag 1993.","DOI":"10.1007\/978-1-4757-3860-5"},{"key":"7_CR14","first-page":"326","volume":"35","author":"V.P. Orevkov","year":"1987","unstructured":"V.P. Orevkov. Reconstruction of a proof from its scheme. Soviet Mathematics Doklady 35 (1987) pp. 326\u2013329.","journal-title":"Soviet Mathematics Doklady"},{"key":"7_CR15","unstructured":"V.P. Orevkov. On lower bounds on the lengths of proofs in propositional logic. (In Russian), in Proc, of All Union Conf. Metody Matem. v Problemach iskusstvennogo intellekta i sistematicheskoje programmirovanie, Vilnius, Vol I. 1980. pp. 142\u2013144."},{"key":"7_CR16","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1090\/S0002-9947-1973-0432416-X","volume":"177","author":"R. Parikh","year":"1973","unstructured":"R. Parikh Some results on the length of proofs. Trans. A.M.S., 177 (1973) pp. 29\u201336.","journal-title":"Trans. A.M.S."},{"key":"7_CR17","unstructured":"A. N. Prior. Formal Logic. Oxford, second edition, 1960."},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"P. Pudlak, S. Buss. How to he without being (easily) convicted and the length of proofs in propositional calculus. 8th Workshop on CSL, Kazimierz, Poland, September 1994, Springer Verlag LNCS n.995, 1995, pp. 151\u2013162.","DOI":"10.1007\/BFb0022253"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"A. Urquhart. The number of lines in Frege proof with substitution. Archive for Mathematical Logic. To appear.","DOI":"10.1007\/s001530050078"}],"container-title":["Computer Science Logic","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028010","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T02:51:39Z","timestamp":1586573499000},"score":1,"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"references-count":19,"URL":"http:\/\/dx.doi.org\/10.1007\/bfb0028010","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1998]]}}}