{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:53Z","timestamp":1749182813512,"version":"3.41.0"},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2001,10,1]],"date-time":"2001-10-01T00:00:00Z","timestamp":1001894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,10,1]],"date-time":"2001-10-01T00:00:00Z","timestamp":1001894400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2001,10]]},"DOI":"10.1023\/a:1017515831550","type":"journal-article","created":{"date-parts":[[2002,12,29]],"date-time":"2002-12-29T22:59:26Z","timestamp":1041202766000},"page":"297-311","source":"Crossref","is-referenced-by-count":6,"title":["An O(nlog\u2009n)-SPACE Decision Procedure for the Propositional Dummett Logic"],"prefix":"10.1007","volume":"27","author":[{"given":"Guido","family":"Fiorino","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"336869_CR1","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1093\/jigpal\/7.4.447","volume":"7","author":"A. Avellone","year":"1999","unstructured":"Avellone, A., Ferrari, M. and Miglioli, P.: Duplication-free tableau calculi and related cutfree sequent calculi for the interpolable propositional intermediate logics, Logic J. IGPL\n7(4) (1999), 447\u2013480.","journal-title":"Logic J. IGPL"},{"key":"336869_CR2","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/BF01531058","volume":"4","author":"A. Avron","year":"1991","unstructured":"Avron, A.: Hypersequents, logical consequence and intermediate logics for concurrency, Ann. Math. Artificial Intelligence\n4 (1991), 225\u2013248.","journal-title":"Ann. Math. Artificial Intelligence"},{"key":"336869_CR3","doi-asserted-by":"crossref","unstructured":"Baaz, M. and Ferm\u00fcller, C. G.: Analytic calculi for projective logics, in N. V. Murray (ed.), '99, Lecture Notes in Comput. Sci. 1617, Springer, 1999, pp. 36\u201350.","DOI":"10.1007\/3-540-48754-9_8"},{"key":"336869_CR4","doi-asserted-by":"crossref","unstructured":"Chagrov, A. and Zakharyaschev, M.: Modal Logic, Oxford University Press, 1997.","DOI":"10.1093\/oso\/9780198537793.001.0001"},{"key":"336869_CR5","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1002\/malq.19890350402","volume":"35","author":"G. Corsi","year":"1989","unstructured":"Corsi, G.: A cut-free calculus for Dummett's LC quantified, Z. Math. Logik Grundlag. Math.\n35 (1989), 289\u2013301.","journal-title":"Z. Math. Logik Grundlag. Math."},{"key":"336869_CR6","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1017\/S0022481200125848","volume":"24","author":"M. Dummett","year":"1959","unstructured":"Dummett, M.: A propositional calculus with a denumerable matrix, J. Symbolic Logic\n24 (1959), 96\u2013107.","journal-title":"J. Symbolic Logic"},{"issue":"3","key":"336869_CR7","doi-asserted-by":"crossref","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic, J. Symbolic Logic\n57(3) (1992), 795\u2013807.","journal-title":"J. Symbolic Logic"},{"issue":"3","key":"336869_CR8","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1093\/jigpal\/7.3.319","volume":"7","author":"R. Dyckhoff","year":"1999","unstructured":"Dyckhoff, R.: A deterministic terminating sequent calculus for G\u00f6del-Dummett logic, Logic J. IGPL\n7(3) (1999), 319\u2013326.","journal-title":"Logic J. IGPL"},{"key":"336869_CR9","unstructured":"Fitting, M. C.: Intuitionistic Logic, Model Theory and Forcing, North-Holland, 1969."},{"key":"336869_CR10","unstructured":"G\u00f6del, K.: On the intuitionistic propositional calculus, in S. Feferman et al. (eds), Collected Works, Vol. 1, Oxford University Press, 1986."},{"key":"336869_CR11","unstructured":"Hudelmaier, J.: Bounds for Cut Elimination in Intuitionistic Propositional Logic, Ph.D. Thesis, Universit\u00e4t Tubingen, 1989."},{"key":"336869_CR12","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/BF01627506","volume":"31","author":"J. Hudelmaier","year":"1992","unstructured":"Hudelmaier, J.: Bounds for cut elimination in intuitionistic propositional logic, Arch. Math. Logic\n31 (1992), 331\u2013354.","journal-title":"Arch. Math. Logic"},{"issue":"1","key":"336869_CR13","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1093\/logcom\/3.1.63","volume":"3","author":"J. Hudelmaier","year":"1993","unstructured":"Hudelmaier, J.: An O(n log n)-SPACE decision procedure for intuitionistic propositional logic, J. Logic Comput.\n3(1) (1993), 63\u201375.","journal-title":"J. Logic Comput."},{"issue":"3","key":"336869_CR14","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R. E. Ladner","year":"1977","unstructured":"Ladner, R. E.: The computational complexity of provability in systems of modal propositional logic, SIAM J. Comput.\n6(3) (1977), 467\u2013480.","journal-title":"SIAM J. Comput."},{"key":"336869_CR15","unstructured":"Miglioli, P., Moscato, U. and Ornaghi, M.: How to avoid duplications in refutation systems for intuitionistic logic and Kuroda logic, in K. Broda, M. D'Agostino, R. Gor\u00e9, R. Johnson, and S. Reeves (eds), Theorem Proving with Analytic Tableaux and Related Methods: 3rd International Workshop, Abingdon, U.K., May 1994, pp. 169\u2013187."},{"key":"336869_CR16","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/BF00881949","volume":"12","author":"P. Miglioli","year":"1994","unstructured":"Miglioli, P., Moscato, U. and Ornaghi, M.: An improved refutation system for intuitionistic predicate logic, J. Automated Reasoning\n12 (1994), 361\u2013373.","journal-title":"J. Automated Reasoning"},{"issue":"1","key":"336869_CR17","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1093\/jigpal\/5.1.145","volume":"5","author":"P. Miglioli","year":"1997","unstructured":"Miglioli, P., Moscato, U. and Ornaghi, M.: Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic, Logic J. IGPL\n5(1) (1997), 145\u2013167.","journal-title":"Logic J. IGPL"},{"key":"336869_CR18","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(79)90006-9","volume":"9","author":"R. Statman","year":"1977","unstructured":"Statman, R.: Intuitionistic logic is polynomial-space complete, Theoret. Comput. Sci.\n9 (1977), 67\u201372.","journal-title":"Theoret. Comput. Sci."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1017515831550.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1017515831550\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1017515831550.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:39:36Z","timestamp":1749123576000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1017515831550"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,10]]},"references-count":18,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2001,10]]}},"alternative-id":["336869"],"URL":"https:\/\/doi.org\/10.1023\/a:1017515831550","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2001,10]]}}}