{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:19Z","timestamp":1761611299601},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540612087"},{"type":"electronic","value":"9783540683681"}],"license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61208-4_15","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:19:23Z","timestamp":1330273163000},"page":"226-243","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Strong normalization for all-style LKtq"],"prefix":"10.1007","author":[{"given":"Jean-Baptiste","family":"Joinet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harold","family":"Schellinx","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lorenzo","family":"Tortora de Falco","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"issue":"3","key":"15_CR1","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J. M. Andreoli","year":"1992","unstructured":"Andreoli, J. M. (1992). Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297\u2013347.","journal-title":"Journal of Logic and Computation"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Danos, V., Joinet, J.-B., and Schellinx, H. (1993). The structure of exponentials: uncovering the dynamics of linear logic proofs. In Gottlob, G., Leitsch, A., and Mundici, D., editors, Computational Logic and Proof Theory, pages 159\u2013171. Springer Verlag. Lecture Notes in Computer Science 713.","DOI":"10.1007\/BFb0022564"},{"key":"15_CR3","unstructured":"Danos, V., Joinet, J.-B., and Schellinx, H. (1995). A new deconstructive logic: linear logic. Preprint 936, Department of Mathematics, Utrecht University. (To appear in the Journal of Symbolic Logic)."},{"key":"15_CR4","unstructured":"Danos, V., Joinet, J.-B., and Schellinx, H. (1995). LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In Girard, J.-Y., Lafont, Y., and Regnier, L., editors, Advances in Linear Logic, pages 211\u2013224. Cambridge University Press."},{"key":"15_CR5","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. (1987). Linear logic. Theoretical Computer Science, 50:1\u2013102.","journal-title":"Theoretical Computer Science"},{"key":"15_CR6","volume-title":"Nuovi problemi della logica e delta filosofia delta scienza, Volume II","author":"J.-Y. Girard","year":"1991","unstructured":"Girard, J.-Y. (1991). Quantifiers in linear logic II. In Corsi, G. and Sambin, G., editors, Nuovi problemi della logica e delta filosofia delta scienza, Volume II. CLUEB, Bologna(Italy)."},{"key":"15_CR7","unstructured":"Joinet, J.-B. (1993). Etude de la normalisation du calcul des s\u00e9quents classique \u00e0 travers la logique lin\u00e9aire. Th\u00e8se de Doctorat, Universit\u00e9 Paris VII."},{"key":"15_CR8","unstructured":"Parigot, M. (1991). Free Deduction: an analysis of computation in classical logic. In Voronkov, A., editor, Russian Conference on Logic Programming, pages 361\u2013380. Springer Verlag. Lecture Notes in Artificial Intelligence 592."},{"key":"15_CR9","unstructured":"Schellinx, H. (1994). A linear approach to modal proof theory. (To appear in H. Wansing, ed., \u2018Proof Theory of Modal Logic'. Studies in Applied Logic, Kluwer Academic Publishers."},{"key":"15_CR10","unstructured":"Schellinx, H. (1994). The Noble Art of Linear Decorating. ILLC Dissertation Series, 1994-1. Institute for Language, Logic and Computation, University of Amsterdam."},{"key":"15_CR11","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/BF00885763","volume":"12","author":"T. Tammet","year":"1994","unstructured":"Tammet, T. (1994). Proof search strategies in linear logic. Journal of Automated Reasoning, 12:273\u2013304.","journal-title":"Journal of Automated Reasoning"},{"key":"15_CR12","unstructured":"Tortora de Falco, L. (1994). Strong normalization property for heterostyle LKtq and FD. Pr\u00e9publication 53, \u00c9quipe de Logique Math\u00e9matique, Universit\u00e9 Paris VII."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61208-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T18:51:35Z","timestamp":1578509495000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61208-4_15"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540612087","9783540683681"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-61208-4_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]},"assertion":[{"value":"1 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}