{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T00:53:15Z","timestamp":1763686395040,"version":"3.37.3"},"reference-count":14,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T00:00:00Z","timestamp":1672358400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T00:00:00Z","timestamp":1672358400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,3]]},"DOI":"10.1007\/s10817-022-09653-z","type":"journal-article","created":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T10:12:20Z","timestamp":1672395140000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic"],"prefix":"10.1007","volume":"67","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0556-0723","authenticated-orcid":false,"given":"Guido","family":"Fiorino","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,30]]},"reference":[{"issue":"2","key":"9653_CR1","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1017\/S1755020315000374","volume":"9","author":"SN Art\u00ebmov","year":"2016","unstructured":"Art\u00ebmov, S.N., Protopopescu, T.: Intuitionistic epistemic logic. Rev. Symb. Log. 9(2), 266\u2013298 (2016). https:\/\/doi.org\/10.1017\/S1755020315000374","journal-title":"Rev. Symb. Log."},{"key":"9653_CR2","unstructured":"Brogi, C.P.: Curry-howard-lambek correspondence for intuitionistic belief. CoRR (2020). arXiv:2006.02417"},{"key":"9653_CR3","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":"2","key":"9653_CR4","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s10817-012-9252-7","volume":"51","author":"M Ferrari","year":"2013","unstructured":"Ferrari, M., Fiorentini, C., Fiorino, G.: Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models. J. Automated Reason. 51(2), 129\u2013149 (2013). https:\/\/doi.org\/10.1007\/s10817-012-9252-7","journal-title":"J. Automated Reason."},{"issue":"1","key":"9653_CR5","first-page":"8:1","volume":"6","author":"M Ferrari","year":"2015","unstructured":"Ferrari, M., Fiorentini, C., Fiorino, G.: An evaluation-driven decision procedure for G3i. ACM Trans. Comput. Logic 6(1), 8:1-8:37 (2015)","journal-title":"ACM Trans. Comput. Logic"},{"key":"9653_CR6","volume-title":"Intuitionistic Logic, Model Theory and Forcing","author":"M Fitting","year":"1969","unstructured":"Fitting, M.: Intuitionistic Logic, Model Theory and Forcing. North-Holland, Amsterdam (1969)"},{"issue":"1","key":"9653_CR7","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1215\/00294527-2377869","volume":"55","author":"M Fitting","year":"2014","unstructured":"Fitting, M.: Nested sequents for intuitionistic logics. Notre Dame J. Formal Log. 55(1), 41\u201361 (2014). https:\/\/doi.org\/10.1215\/00294527-2377869","journal-title":"Notre Dame J. Formal Log."},{"issue":"1","key":"9653_CR8","doi-asserted-by":"publisher","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. 3(1), 63\u201375 (1993)","journal-title":"J. Logic Comput."},{"key":"9653_CR9","doi-asserted-by":"publisher","unstructured":"Krupski, V.N., Yatmanov, A.: Sequent calculus for intuitionistic epistemic logic IEL. In: Art\u00ebmov, S.N., Nerode, A. (eds.) Logical Foundations of Computer Science\u2014International Symposium, LFCS 2016, Deerfield Beach, FL, USA, January 4\u20137, 2016. Proceedings, Lecture Notes in Computer Science, vol. 9537, pp. 187\u2013201. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-27683-0_14","DOI":"10.1007\/978-3-319-27683-0_14"},{"key":"9653_CR10","doi-asserted-by":"publisher","unstructured":"Rogozin, D.: Modal type theory based on the intuitionistic modal logic $$\\textbf{IEL}$$. In: Art\u00ebmov, S.N., Nerode, A. (eds.) Logical Foundations of Computer Science\u2014International Symposium, LFCS 2020, Deerfield Beach, FL, USA, January 4\u20137, 2020, Proceedings, Lecture Notes in Computer Science, vol. 11972, pp. 236\u2013248. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-36755-8_15","DOI":"10.1007\/978-3-030-36755-8_15"},{"key":"9653_CR11","doi-asserted-by":"publisher","unstructured":"Su, Y., Sano, K.: First-order intuitionistic epistemic logic. In: Blackburn, P., Lorini, E., Guo, M. (eds.) Logic, Rationality, and Interaction\u20147th International Workshop, LORI 2019, Chongqing, China, October 18-21, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11813, pp. 326\u2013339. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-662-60292-8_24","DOI":"10.1007\/978-3-662-60292-8_24"},{"key":"9653_CR12","volume-title":"Constructivism in Mathematics: An Introduction. Studies in Logic and the Foundations of Mathematics","author":"A Troelstra","year":"1988","unstructured":"Troelstra, A., van Dalen, D.: Constructivism in Mathematics: An Introduction. Studies in Logic and the Foundations of Mathematics, vol. 121. North-Holland, Amsterdam (1988)"},{"key":"9653_CR13","volume-title":"Basic Proof Theory","author":"A Troelstra","year":"1996","unstructured":"Troelstra, A., Schwichtenberg, H.: Basic Proof Theory, vol. 43. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge (1996)"},{"key":"9653_CR14","doi-asserted-by":"crossref","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)","DOI":"10.1090\/trans2\/094\/02"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09653-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09653-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09653-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,3]],"date-time":"2023-12-03T19:12:20Z","timestamp":1701630740000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09653-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,30]]},"references-count":14,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3]]}},"alternative-id":["9653"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09653-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2022,12,30]]},"assertion":[{"value":"4 March 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 November 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 December 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"3"}}