{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:36:54Z","timestamp":1725457014046},"publisher-location":"Berlin\/Heidelberg","reference-count":23,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540557458"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0031929","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:11:55Z","timestamp":1134281515000},"page":"146-171","source":"Crossref","is-referenced-by-count":17,"title":["Cut-elimination in logics with definitional reflection"],"prefix":"10.1007","author":[{"given":"Peter","family":"Schroeder-Heister","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","first-page":"1403","DOI":"10.2307\/2275485","volume":"56","author":"V. M. Abrusci","year":"1991","unstructured":"Abrusci, V. M. Phase semantics and sequent calculus for pure noncommutative classical linear prepositional logic. Journal of Symbolic Logic, 56 (1991), 1403\u20131451.","journal-title":"Journal of Symbolic Logic"},{"key":"10_CR2","doi-asserted-by":"crossref","first-page":"33","DOI":"10.2307\/2268439","volume":"15","author":"W. Ackermann","year":"1950","unstructured":"Ackermann, W. Widerspruchsfreier Aufbau der Logik.I. Typenfreies System ohne tertium non datur. Journal of Symbolic Logic, 15 (1950), 33\u201357.","journal-title":"Journal of Symbolic Logic"},{"key":"10_CR3","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/BF03037453","volume":"4","author":"M. Aronsson","year":"1990","unstructured":"Aronsson, M., Eriksson, L.-H., G\u00e4redal, A., Halln\u00e4s, L. & Olin, P. The programming language GCLA: A definitional appraoch to logic programming. New Generation Computing, 4 (1990), 381\u2013404.","journal-title":"New Generation Computing"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Clark, K. L. Negation as failure. In: Gallaire, H. & Minker, J. (Eds.), Logic and Data Bases, New York 1978, 293\u2013322.","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"10_CR5","doi-asserted-by":"crossref","first-page":"115","DOI":"10.2307\/2269292","volume":"7","author":"H. B. Curry","year":"1942","unstructured":"Curry, H. B. The inconsistency of certain formal logics. Journal of Symbolic Logic, 7 (1942), 115\u2013117.","journal-title":"Journal of Symbolic Logic"},{"key":"10_CR6","unstructured":"Do\u0161en, K. A historical introduction to substructural logics. In: Do\u0161en, K. & Schroeder-Heister, P. (Eds.) Substructural Logics: Proceedings of the Conference held in T\u00fcbingen, October 1990. Oxford University Press, 1992."},{"key":"10_CR7","unstructured":"Dunn, M. Consecution formulation of positive R with co-tenability and t. In: Anderson, A.R. & Belnap, N.D., Entailment: The Logic of Relevance and Necessity, Vol. I, Princeton University Press, 1975, 381\u2013391."},{"key":"10_CR8","first-page":"89","volume-title":"Extensions of Logic Programming. Second International Workshop, ELP-91, Stockholm, January 1991, Proceedings","author":"L.-H. Eriksson","year":"1992","unstructured":"Eriksson, L.-H. A finitary version of the calculus of partial inductive definitions. In: Eriksson, L.-H., Halln\u00e4s, L. & Schroeder-Heister, P. (Eds.), Extensions of Logic Programming. Second International Workshop, ELP-91, Stockholm, January 1991, Proceedings. Springer LNCS, Vol. 596, Berlin 1992, 89\u2013134."},{"key":"10_CR9","doi-asserted-by":"crossref","first-page":"92","DOI":"10.2307\/2269029","volume":"1","author":"F. B. Fitch","year":"1936","unstructured":"Fitch. F. B. A system of formal logic without an analogue to the Curry W operator. Journal of Symbolic Logic, 1 (1936), 92\u2013100.","journal-title":"Journal of Symbolic Logic"},{"key":"10_CR10","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G. Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift, 39 (1935), 176\u2013210, 405\u2013431, English Translation in: M.E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, Amsterdam: North Holland 1969, 68\u2013131.","journal-title":"Mathematische Zeitschrift"},{"key":"10_CR11","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. Linear logic. Theoretical Computer Science, 50 (1987), 1\u2013102.","journal-title":"Theoretical Computer Science"},{"key":"10_CR12","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/S0304-3975(06)80007-1","volume":"87","author":"L. Halln\u00e4s","year":"1991","unstructured":"Halln\u00e4s, L. Partial inductive definitions. Theoretical Computer Science, 87 (1991), 115\u2013142. Previous versions published as SICS Research Reports 86005 (1986) and 86005C (1988), and in: Avron, A. et al. (Eds.), Workshop on General Logic, Dept. of Computer Science, University of Edinburgh, Report ECS-LFCS-88-52 (1988).","journal-title":"Theoretical Computer Science"},{"key":"10_CR13","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1093\/logcom\/1.2.261","volume":"1","author":"L. Halln\u00e4s","year":"1990","unstructured":"Halln\u00e4s, L. & Schroeder-Heister, P. A proof-theoretic approach to logic programming. I. Clauses as rules. Journal of Logic and Computation, 1 (1990), 261\u2013283; II. Programs as definitions, ibid. 1 (1991), 635\u2013660. Previous version published at SICS Research Report 88005, 1988.","journal-title":"Journal of Logic and Computation"},{"key":"10_CR14","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1080\/00029890.1958.11989160","volume":"65","author":"J. Lambek","year":"1958","unstructured":"Lambek, J. The mathematics of sentence structure. American Mathematical Monthly, 65 (1958), 154\u2013170.","journal-title":"American Mathematical Monthly"},{"key":"10_CR15","first-page":"166","volume-title":"On the calculus of syntactic types","author":"J. Lambek","year":"1961","unstructured":"Lambek, J. On the calculus of syntactic types. In: R. Jacobson (Ed.), Proceedings of the 12th Symposium on Applied Mathematics, AMS, Providence 1961, 166\u2013178, 264\u2013265."},{"key":"10_CR16","unstructured":"Lambek, J. Logic without structural rules (Another look at cut elimination). In: Do\u0161en, K. & Schroeder-Heister, P. (Eds.) Substructural Logics: Proceedings of the Conference held in T\u00fcbingen, October 1990. Oxford University Press, 1992."},{"key":"10_CR17","unstructured":"Lambek, J. From categorial grammar to bilinear logic. In: Do\u0161en, K. & Schroeder-Heister, P. (Eds.) Substructural Logics: Proceedings of the Conference held in T\u00fcbingen, October 1990. Oxford University Press, 1992."},{"key":"10_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-01539-1","volume-title":"Einf\u00fchrung in die operative Logik und Mathematik","author":"P. Lorenzen","year":"1955","unstructured":"Lorenzen, P. Einf\u00fchrung in die operative Logik und Mathematik. Springer: Berlin 1955, 2nd ed. Berlin 1969.","edition":"2nd ed."},{"key":"10_CR19","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/S0049-237X(08)70847-4","volume-title":"Proceedings of the Second Scandinavian Logic Symposium","author":"P. Martin-L\u00f6f","year":"1971","unstructured":"Martin-L\u00f6f, P. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In: Fenstad, J. E. (Ed.), Proceedings of the Second Scandinavian Logic Symposium, North-Holland: Amsterdam 1971, 179\u2013216."},{"key":"10_CR20","unstructured":"Nadathur, G. & Miller, D. An overview of \u03bb-Prolog. In: Kowalski, R. & Bowen, K. (Eds.), Fifth International Conference on Logic Programming, MIT Press 1988, 810\u2013827."},{"key":"10_CR21","volume-title":"Relevant Logic: A Philosophical Examination of Inference","author":"S. Read","year":"1988","unstructured":"Read, S. Relevant Logic: A Philosophical Examination of Inference. Oxford: Basil Blackwell, 1988."},{"key":"10_CR22","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/BFb0038701","volume-title":"Extensions of Logic Programming. International Workshop, T\u00fcbingen, FRG, December 1989, Proceedings","author":"P. Schroeder-Heister","year":"1991","unstructured":"Schroeder-Heister, P. Hypothetical reasoning and definitional reflection in logic programming. In: P. Schroeder-Heister (Ed.), Extensions of Logic Programming. International Workshop, T\u00fcbingen, FRG, December 1989, Proceedings. Springer LNCS, Vol. 475, Berlin 1991, 327\u2013340."},{"key":"10_CR23","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/BF00296176","volume":"18","author":"J. Slaney","year":"1989","unstructured":"Slaney, J. Solution to a problem of Ono and Komori. Journal of Philosophical Logic, 18 (1989), 103\u2013111.","journal-title":"Journal of Philosophical Logic"}],"container-title":["Lecture Notes in Computer Science","Nonclassical Logics and Information Processing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0031929","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T13:45:41Z","timestamp":1586612741000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0031929"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540557458"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/bfb0031929","relation":{},"subject":[]}}