{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:18:13Z","timestamp":1725664693679},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540630456"},{"type":"electronic","value":"9783540690658"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63045-7_26","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:00:29Z","timestamp":1330297229000},"page":"258-265","source":"Crossref","is-referenced-by-count":2,"title":["Existential instantiation and strong normalization"],"prefix":"10.1007","author":[{"given":"G.","family":"Mints","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"Gentzen G.: Untersuchungen \u00fcber das logische Schliessen. Mathematische Zeitschrift, 39 (1934) 176\u2013210, 405\u2013431","journal-title":"Mathematische Zeitschrift"},{"key":"26_CR2","volume-title":"Proofs and Types","author":"J.-Y. Girard","year":"1988","unstructured":"Girard J.-Y., Lafont Y., Taylor P.: Proofs and Types, Cambridge University Press, Cambridge (1988)"},{"key":"26_CR3","unstructured":"Leivant D.: Existential instantiation in a system of natural deduction, Mathematish Centrum-ZW 13\u201373 (1973)"},{"key":"26_CR4","unstructured":"Mints G.: Lewis Systems and the System T. In Mints G.: Selected Papers in Proof Theory, North-Holland-Bibliopolis (1993), 221\u2013294 (Russian Original 1974)"},{"issue":"N3","key":"26_CR5","doi-asserted-by":"crossref","first-page":"587","DOI":"10.1070\/IM1989v032n03ABEH000782","volume":"32","author":"G. Mints","year":"1989","unstructured":"Mints G.: A Normal Form Theorem for Second-order Classical Logic with an Axiom of Choice, Math. USSR Izvestiya 32 N3 (1989) 587\u2013605","journal-title":"Math. USSR Izvestiya"},{"key":"26_CR6","unstructured":"Mints G.: Normal Deduction in the Intuitionistic Linear Logic, CSLI report, (1996)"},{"key":"26_CR7","unstructured":"Prawitz D.: Natural Deduction, Almquist and Wiksell (1965)"},{"key":"26_CR8","unstructured":"Prawitz D.: Ideas and Results in Proof Theory, In Proc. 2-nd Scand.Logic Symp., North-Holland, (1972) 235\u2013308"},{"key":"26_CR9","doi-asserted-by":"crossref","first-page":"93","DOI":"10.2307\/2266969","volume":"15","author":"W.V. Quine","year":"1950","unstructured":"Quine W.V.: On natural deduction, Journal of Symbolic Logic 15 (1950) 93\u2013102","journal-title":"Journal of Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63045-7_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:41:17Z","timestamp":1619574077000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63045-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540630456","9783540690658"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-63045-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}