{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:15:49Z","timestamp":1742962549732,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466773"},{"type":"electronic","value":"9783662466780"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46678-0_29","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T09:42:21Z","timestamp":1427881341000},"page":"451-465","source":"Crossref","is-referenced-by-count":4,"title":["On the Mints Hierarchy in First-Order Intuitionistic Logic"],"prefix":"10.1007","author":[{"given":"Aleksy","family":"Schubert","sequence":"first","affiliation":[]},{"given":"Pawe\u0142","family":"Urzyczyn","sequence":"additional","affiliation":[]},{"given":"Konrad","family":"Zdanowski","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Bonevac, D.: A history of quantification. In: Logic: A History of its Central Concepts. Handbook of the History of Logic, vol.\u00a011, North Holland (2012)","DOI":"10.1016\/B978-0-444-52937-4.50002-2"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic (1997)","DOI":"10.1007\/978-3-642-59207-2"},{"key":"29_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-03359-9_6","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Bove","year":"2009","unstructured":"Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda \u2013 A functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 73\u201378. Springer, Heidelberg (2009)"},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"Burr, W.: The intuitionistic arithmetical hierarchy. In: Logic Colloquium 1999. Lecture Notes in Logic, vol.\u00a017, pp. 51\u201359. ASL (1999)","DOI":"10.1017\/9781316755921.004"},{"key":"29_CR5","unstructured":"Church, A.: Introduction to Mathematical Logic. Princeton (1944)"},{"key":"29_CR6","unstructured":"Coq Development Team. The Coq Proof Assistant Reference Manual V8.4 (March 2012), \n                      \n                        http:\/\/coq.inria.fr\/distrib\/V8.4\/refman\/"},{"issue":"1-2","key":"29_CR7","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/S0304-3975(98)00185-6","volume":"243","author":"A. Degtyarev","year":"2000","unstructured":"Degtyarev, A., Gurevich, Y., Narendran, P., Veanes, M., Voronkov, A.: Decidability and complexity of simultaneous rigid E-unification with one variable and related results. Theoretical Computer Science\u00a0243(1-2), 167\u2013184 (2000)","journal-title":"Theoretical Computer Science"},{"issue":"1-3","key":"29_CR8","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/j.tcs.2006.01.053","volume":"360","author":"G. Dowek","year":"2006","unstructured":"Dowek, G., Jiang, Y.: Eigenvariables, bracketing and the decidability of positive minimal predicate logic. Theoretical Computer Science\u00a0360(1-3), 193\u2013208 (2006)","journal-title":"Theoretical Computer Science"},{"key":"29_CR9","unstructured":"Fitting, M.: Fundamentals of Generalized Recursion Theory. Elsevier (1981)"},{"issue":"2","key":"29_CR10","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1215\/00294527-2010-014","volume":"51","author":"J. Fleischmann","year":"2010","unstructured":"Fleischmann, J.: Syntactic preservation theorems for intuitionistic predicate logic. Notre Dame Journal of Formal Logic\u00a051(2), 225\u2013245 (2010)","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"Immerman, N.: Descriptive Complexity. Springer (1999)","DOI":"10.1007\/978-1-4612-0539-5"},{"issue":"3","key":"29_CR12","doi-asserted-by":"publisher","first-page":"317","DOI":"10.2307\/2964291","volume":"23","author":"G. Kreisel","year":"1958","unstructured":"Kreisel, G.: Elementary completeness properties of intuitionistic logic with a note on negations of prenex formulae. J. Symbolic Logic\u00a023(3), 317\u2013330 (1958)","journal-title":"J. Symbolic Logic"},{"key":"29_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-540-73228-0_18","volume-title":"Typed Lambda Calculi and Applications","author":"D. Ku\u015bmierek","year":"2007","unstructured":"Ku\u015bmierek, D.: The inhabitation problem for rank two intersection types. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol.\u00a04583, pp. 240\u2013254. Springer, Heidelberg (2007)"},{"key":"29_CR14","first-page":"135","volume":"98","author":"G.E. Mints","year":"1968","unstructured":"Mints, G.E.: Solvability of the problem of deducibility in LJ for a class of formulas not containing negative occurrences of quantifiers. Steklov Inst.\u00a098, 135\u2013145 (1968)","journal-title":"Steklov Inst."},{"key":"29_CR15","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. A Proof Assistant for Higher-Order Logic. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"issue":"3","key":"29_CR16","first-page":"581","volume":"163","author":"V.P. Orevkov","year":"1965","unstructured":"Orevkov, V.P.: The undecidability in the constructive predicate calculus of the class of formulas of the form \u00ac\u00ac\u2009\u2200\u2009\u2203. Doklady AN SSSR\u00a0163(3), 581\u2013583 (1965)","journal-title":"Doklady AN SSSR"},{"key":"29_CR17","first-page":"109","volume":"60","author":"V.P. Orevkov","year":"1976","unstructured":"Orevkov, V.P.: Solvable classes of pseudoprenex formulas. Zapiski nauchnyh Seminarov LOMI\u00a060, 109\u2013170 (1976)","journal-title":"Zapiski nauchnyh Seminarov LOMI"},{"key":"29_CR18","doi-asserted-by":"crossref","first-page":"21","DOI":"10.4064\/fm-41-1-21-28","volume":"41","author":"H. Rasiowa","year":"1954","unstructured":"Rasiowa, H., Sikorski, R.: On existential theorems in non-classical functional calculi. Fundamenta Mathematicae\u00a041, 21\u201328 (1954)","journal-title":"Fundamenta Mathematicae"},{"key":"29_CR19","unstructured":"Rummelhoff, I.: Polymorphic \u03a01 Types and a Simple Approach to Propositions, Types and Sets. PhD thesis, University of Oslo (2007)"},{"key":"29_CR20","unstructured":"Schubert, A., Urzyczyn, P., Walukiewicz-Chrz\u0105szcz, D.: How hard is positive quantification? (2014), \n                      \n                        http:\/\/www.mimuw.edu.pl\/~alx\/positive2conexp.pdf"},{"key":"29_CR21","unstructured":"Schubert, A., Urzyczyn, P., Walukiewicz-Chrz\u0105szcz, D.: Positive quantification is not elementary (with restricted instantiation) (2014), \n                      \n                        http:\/\/www.mimuw.edu.pl\/~alx\/positivenonelem.pdf"},{"key":"29_CR22","doi-asserted-by":"crossref","unstructured":"S\u00f8rensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Elsevier (2006)","DOI":"10.1016\/S0049-237X(06)80005-4"},{"key":"29_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-642-02273-9_26","volume-title":"Typed Lambda Calculi and Applications","author":"P. Urzyczyn","year":"2009","unstructured":"Urzyczyn, P.: Inhabitation of low-rank intersection types. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol.\u00a05608, pp. 356\u2013370. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46678-0_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:28:05Z","timestamp":1559140085000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46678-0_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466773","9783662466780"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46678-0_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}