{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:21:14Z","timestamp":1758979274758},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,6,10]],"date-time":"2012-06-10T00:00:00Z","timestamp":1339286400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,8]]},"DOI":"10.1007\/s10817-012-9252-7","type":"journal-article","created":{"date-parts":[[2012,6,9]],"date-time":"2012-06-09T03:55:12Z","timestamp":1339214112000},"page":"129-149","source":"Crossref","is-referenced-by-count":18,"title":["Contraction-Free Linear Depth Sequent Calculi for Intuitionistic Propositional Logic with the Subformula Property and Minimal Depth Counter-Models"],"prefix":"10.1007","volume":"51","author":[{"given":"Mauro","family":"Ferrari","sequence":"first","affiliation":[]},{"given":"Camillo","family":"Fiorentini","sequence":"additional","affiliation":[]},{"given":"Guido","family":"Fiorino","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,6,10]]},"reference":[{"key":"9252_CR1","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/978-3-642-15675-5_7","volume-title":"Logics in Artificial Intelligence, JELIA 2010, vol. 6341","author":"L Bozzato","year":"2010","unstructured":"Bozzato, L., Ferrari, M., Fiorentini, C., Fiorino, G.: A decidable constructive description logic. In: Janhunen, T., Niemel\u00e4, I. (eds.) Logics in Artificial Intelligence, JELIA 2010, vol. 6341, pp. 51\u201363. Springer, New York (2010)"},{"key":"9252_CR2","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198537793.001.0001","volume-title":"Modal Logic","author":"A Chagrov","year":"1997","unstructured":"Chagrov, A., Zakharyaschev, M.: Modal Logic. Oxford University Press, Oxford (1997)"},{"issue":"4","key":"9252_CR3","doi-asserted-by":"crossref","first-page":"1204","DOI":"10.2178\/jsl\/1203350782","volume":"72","author":"G Corsi","year":"2007","unstructured":"Corsi, G., Tassi, G.: Intuitionistic logic freed of all metarules. J. Symb. Log. 72(4), 1204\u20131218 (2007)","journal-title":"J. Symb. Log."},{"issue":"3","key":"9252_CR4","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. Symb. Log. 57(3), 795\u2013807 (1992)","journal-title":"J. Symb. Log."},{"issue":"2","key":"9252_CR5","doi-asserted-by":"crossref","first-page":"149","DOI":"10.3166\/jancl.19.149-166","volume":"19","author":"M Ferrari","year":"2009","unstructured":"Ferrari, M., Fiorentini, C., Fiorino, G.: A tableau calculus for propositional intuitionistic logic with a refined treatment of nested implications. J. Appl. Non-Class. Log. 19(2), 149\u2013166 (2009)","journal-title":"J. Appl. Non-Class. Log."},{"key":"9252_CR6","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Works of Gerhard Gentzen, pp. 68\u2013131. North-Holland, Amsterdam (1969)","DOI":"10.1016\/S0049-237X(08)70822-X"},{"issue":"1","key":"9252_CR7","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1093\/logcom\/exn067","volume":"20","author":"R Gor\u00e9","year":"2010","unstructured":"Gor\u00e9, R., Postniece, L.: Combining derivations and refutations for cut-free completeness in bi-intuitionistic logic. J. Log. Comput. 20(1), 233\u2013260 (2010)","journal-title":"J. Log. Comput."},{"key":"9252_CR8","first-page":"210","volume-title":"TABLEAUX, Lecture Notes in Computer Science, vol. 1071, pp. 210\u2013225","author":"A Heuerding","year":"1996","unstructured":"Heuerding, A., Seyfried, M., Zimmermann, H.: Efficient loop-check for backward proof search in some non-classical propositional logics. In: Miglioli, P., Moscato, U., Mundici, D., Ornaghi, M. (eds.) TABLEAUX, Lecture Notes in Computer Science, vol. 1071, pp. 210\u2013225. Springer, New York (1996)"},{"key":"9252_CR9","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/S1571-0661(05)01133-3","volume":"37","author":"S Hirokawa","year":"2000","unstructured":"Hirokawa, S., Nagano, D.: Long normal form proof search and counter-model generation. Electron. Notes Theor. Comput. Sci. 37, 11 (2000)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9252_CR10","first-page":"188","volume-title":"TABLEAUX, Lecture Notes in Computer Science, vol. 1227","author":"JM Howe","year":"1997","unstructured":"Howe, J.M.: Two loop detection mechanisms: a comparision. In: Galmiche, D. (ed.) TABLEAUX, Lecture Notes in Computer Science, vol. 1227, pp. 188\u2013200. Springer, New York (1997)"},{"issue":"1","key":"9252_CR11","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 logn)-space decision procedure for intuitionistic propositional logic. J. Log. Comput. 3(1), 63\u201375 (1993)","journal-title":"J. Log. Comput."},{"key":"9252_CR12","first-page":"696","volume-title":"IJCAR, Lecture Notes in Computer Science, vol. 2083","author":"D Larchey-Wendling","year":"2001","unstructured":"Larchey-Wendling, D., M\u00e9ry, D., Galmiche, D.: Strip: Structural sharing for efficient proof-search. In: Gor\u00e9, R., Leitsch, A., ipkow, T. (eds.) IJCAR, Lecture Notes in Computer Science, vol. 2083, pp. 696\u2013700. Springer, New York (2001)"},{"key":"9252_CR13","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/BF00881949","volume":"12","author":"P Miglioli","year":"1994","unstructured":"Miglioli, P., Moscato, U., Ornaghi, M.: An improved refutation system for intuitionistic predicate logic. J. Autom. Reason. 12, 361\u2013373 (1994)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9252_CR14","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., Ornaghi, M.: Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic. Log. J. IGPL 5(1), 145\u2013167 (1997)","journal-title":"Log. J. IGPL"},{"key":"9252_CR15","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1515\/9783110886726.225","volume-title":"Symposia Gaussiana, Conference A","author":"L Pinto","year":"1995","unstructured":"Pinto, L., Dyckhoff, R.: Loop-free construction of counter-models for intuitionistic propositional logic. In: Behara, Fritsch, Lintz (eds.) Symposia Gaussiana, Conference A, pp. 225\u2013232. Walter de Gruyter, Berlin (1995)"},{"issue":"1","key":"9252_CR16","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(79)90006-9","volume":"9","author":"R Statman","year":"1979","unstructured":"Statman, R.: Intuitionistic logic is polynomial-space complete. Theor. Comp. Sci. 9(1), 67\u201372 (1979)","journal-title":"Theor. Comp. Sci."},{"key":"9252_CR17","first-page":"109","volume-title":"CADE, Lecture Notes in Computer Science, vol. 1104","author":"A Stoughton","year":"1996","unstructured":"Stoughton, A.: Porgi: a proof-or-refutation generator for intuitionistic propositional logic. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE, Lecture Notes in Computer Science, vol. 1104, pp. 109\u2013116. Springer, New York (1996)"},{"issue":"1","key":"9252_CR18","first-page":"159","volume":"47","author":"V Svejdar","year":"2006","unstructured":"Svejdar, V.: On sequent calculi for intuitionistic propositional logic. Comment. Math. Univ. Carol. 47(1), 159\u2013173 (2006)","journal-title":"Comment. Math. Univ. Carol."},{"key":"9252_CR19","volume-title":"Cambridge Tracts in Theoretical Computer Science, vol. 43","author":"AS Troelstra","year":"1996","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic proof theory. In: Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press, Cambridge (1996)"},{"key":"9252_CR20","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1090\/trans2\/094\/02","volume-title":"Sixteen Papers on Logic and Algebra, American Mathematical Society Translations, Series 2, vol. 94","author":"NN Vorob\u2019ev","year":"1970","unstructured":"Vorob\u2019ev, N.N.: A new algorithm of derivability in a constructive calculus of statements. In: Sixteen Papers on Logic and Algebra, American Mathematical Society Translations, Series 2, vol. 94, pp. 37\u201371. American Mathematical Society, Providence (1970)"},{"key":"9252_CR21","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/978-94-017-1754-0_5","volume-title":"Handbook of Tableau Methods","author":"A Waaler","year":"1999","unstructured":"Waaler, A., Wallen, L.: Tableaux for intuitionistic logics. In: D\u2019Agostino, M., Gabbay, D.M., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 255\u2013296. Kluwer Academic, Dordrecht (1999)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9252-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-012-9252-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9252-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,25]],"date-time":"2024-04-25T04:31:18Z","timestamp":1714019478000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9252-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,10]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["9252"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9252-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6,10]]}}}