{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:21:13Z","timestamp":1760080873014,"version":"3.40.3"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031435126"},{"type":"electronic","value":"9783031435133"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T00:00:00Z","timestamp":1694649600000},"content-version":"vor","delay-in-days":256,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper we investigate the Curry-Howard correspondence for constructive modal logic in light of the gap between the proof equivalences enforced by the lambda calculi from the literature and by the recently defined winning strategies for this logic.<\/jats:p><jats:p>We define a new lambda-calculus for a minimal constructive modal logic by enriching the calculus from the literature with additional reduction rules and we prove normalization and confluence for our calculus. We then provide a typing system in the style of focused proof systems allowing us to provide a unique proof for each term in normal form, and we use this result to show a one-to-one correspondence between terms in normal form and winning innocent strategies.<\/jats:p>","DOI":"10.1007\/978-3-031-43513-3_19","type":"book-chapter","created":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T14:02:36Z","timestamp":1694613756000},"page":"342-363","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Canonicity of\u00a0Proofs in\u00a0Constructive Modal Logic"],"prefix":"10.1007","author":[{"given":"Matteo","family":"Acclavio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Davide","family":"Catta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Federico","family":"Olimpieri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,14]]},"reference":[{"key":"19_CR1","doi-asserted-by":"publisher","unstructured":"Accattoli, B.: Exponentials as substitutions and the cost of cut elimination in linear logic. In: Baier, C., Fisman, D. (eds.) LICS 2022: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science, Haifa, Israel, 2\u20135 August 2022, pp. 49:1\u201349:15. ACM (2022). https:\/\/doi.org\/10.1145\/3531130.3532445","DOI":"10.1145\/3531130.3532445"},{"key":"19_CR2","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. Association for Computing Machinery, New York (2014). https:\/\/doi.org\/10.1145\/2535838.2535886","DOI":"10.1145\/2535838.2535886"},{"issue":"4","key":"19_CR3","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1007\/s10817-018-9466-4","volume":"63","author":"M Acclavio","year":"2019","unstructured":"Acclavio, M.: Proof diagrams for multiplicative linear logic: syntax and semantics. J. Autom. Reason. 63(4), 911\u2013939 (2019). https:\/\/doi.org\/10.1007\/s10817-018-9466-4","journal-title":"J. Autom. Reason."},{"key":"19_CR4","doi-asserted-by":"publisher","unstructured":"Acclavio, M., Catta, D., Olimpieri, F.: Canonicity of proofs in constructive modal logic (extended version) (2023). https:\/\/doi.org\/10.48550\/arXiv.2304.05465","DOI":"10.48550\/arXiv.2304.05465"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-030-86059-2_25","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M Acclavio","year":"2021","unstructured":"Acclavio, M., Catta, D., Stra\u00dfburger, L.: Game semantics for constructive modal logic. In: Das, A., Negri, S. (eds.) TABLEAUX 2021. LNCS (LNAI), vol. 12842, pp. 428\u2013445. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86059-2_25"},{"key":"19_CR6","unstructured":"Acclavio, M., Stra\u00dfburger, L.: Combinatorial proofs for constructive modal logic. In: Advances in Modal Logic 2022, Rennes, France (2022). https:\/\/hal.inria.fr\/hal-03909538"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/3-540-44802-0_21","volume-title":"Computer Science Logic","author":"N Alechina","year":"2001","unstructured":"Alechina, N., Mendler, M., de Paiva, V., Ritter, E.: Categorical and Kripke semantics for constructive S4 modal logic. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 292\u2013307. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_21"},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/S0168-0072(00)00032-4","volume":"107","author":"JM Andreoli","year":"2001","unstructured":"Andreoli, J.M.: Focussing and proof construction. Ann. Pure Appl. Logic 107, 131\u2013163 (2001)","journal-title":"Ann. Pure Appl. Logic"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Barendregt, H.P., Dekkers, W., Statman, R.: Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, Cambridge (2013). http:\/\/www.cambridge.org\/de\/academic\/subjects\/mathematics\/logic-categories-and-sets\/lambda-calculus-types","DOI":"10.1017\/CBO9781139032636"},{"key":"19_CR10","unstructured":"Bellin, G., De Paiva, V., Ritter, E.: Extended Curry-Howard correspondence for a basic constructive modal logic. In: Proceedings of Methods for Modalities (2001)"},{"key":"19_CR11","unstructured":"Catta, D.: Les preuves vues comme des jeux et r\u00e9ciproquement: s\u00e9mantique dialogique de langages naturel ou logiques. (Proofs as games and games as proofs: dialogical semantics of logical and natural languages). Ph.D. thesis, University of Montpellier, France (2021). https:\/\/tel.archives-ouvertes.fr\/tel-03588308"},{"key":"19_CR12","unstructured":"Chaudhuri, K., Marin, S., Stra\u00dfburger, L.: Modular focused proof systems for intuitionistic modal logics. In: Kesner, D., Pientka, B. (eds.) 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, Porto, Portugal, 22\u201326 June 2016, LIPIcs, vol. 52, pp. 16:1\u201316:18. Leibniz-Zentrum fuer Informatik (2016)"},{"issue":"1","key":"19_CR13","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Logic 44(1), 36\u201350 (1979)","journal-title":"J. Symb. Logic"},{"key":"19_CR14","doi-asserted-by":"publisher","unstructured":"Danos, V., Herbelin, H., Regnier, L.: Game semantics & abstract machines. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, 27\u201330 July 1996, pp. 394\u2013405. IEEE Computer Society (1996). https:\/\/doi.org\/10.1109\/LICS.1996.561456","DOI":"10.1109\/LICS.1996.561456"},{"key":"19_CR15","unstructured":"Das, A., Marin, S.: Brouwer meets kripke: constructivising modal logic. https:\/\/prooftheory.blog\/2022\/08\/19\/brouwer-meets-kripke-constructivising-modal-logic\/. Accessed 19 Aug 2022"},{"key":"19_CR16","doi-asserted-by":"publisher","unstructured":"Das, A., Pous, D.: Non-wellfounded proof theory for (Kleene+action)(algebras+lattices). In: Computer Science Logic (CSL), Birmingham, United Kingdom (2018). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2018.19. https:\/\/hal.archives-ouvertes.fr\/hal-01703942","DOI":"10.4230\/LIPIcs.CSL.2018.19"},{"issue":"3","key":"19_CR17","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/382780.382785","volume":"48","author":"R Davies","year":"2001","unstructured":"Davies, R., Pfenning, F.: A modal analysis of staged computation. J. ACM 48(3), 555\u2013604 (2001). https:\/\/doi.org\/10.1145\/382780.382785","journal-title":"J. ACM"},{"issue":"2","key":"19_CR18","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/S0304-3975(96)00121-1","volume":"169","author":"R Di Cosmo","year":"1996","unstructured":"Di Cosmo, R., Kesner, D.: Combining algebraic rewriting, extensional lambda calculi, and fixpoints. Theor. Comput. Sci. 169(2), 201\u2013220 (1996). https:\/\/doi.org\/10.1016\/S0304-3975(96)00121-1","journal-title":"Theor. Comput. Sci."},{"key":"19_CR19","doi-asserted-by":"publisher","first-page":"477","DOI":"10.2178\/bsl\/1067620091","volume":"9","author":"K Do\u0161en","year":"2003","unstructured":"Do\u0161en, K.: Identity of proofs based on normalization and generality. Bull. Symb. Logic 9, 477\u2013503 (2003)","journal-title":"Bull. Symb. Logic"},{"issue":"3","key":"19_CR20","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241\u2013266 (1982). https:\/\/doi.org\/10.1016\/0167-6423(83)90017-5","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"19_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1997.2627","volume":"137","author":"M Fairtlough","year":"1997","unstructured":"Fairtlough, M., Mendler, M.: Propositional lax logic. Inf. Comput. 137(1), 1\u201333 (1997)","journal-title":"Inf. Comput."},{"issue":"2","key":"19_CR22","first-page":"113","volume":"7","author":"F Fitch","year":"1948","unstructured":"Fitch, F.: Intuitionistic modal logic with quantifiers. Portugaliae Mathematica 7(2), 113\u2013118 (1948)","journal-title":"Portugaliae Mathematica"},{"key":"19_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50, 1\u2013102 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","journal-title":"Theor. Comput. Sci."},{"key":"19_CR24","volume-title":"Logic and Algebra","author":"JY Girard","year":"1996","unstructured":"Girard, J.Y.: Proof-nets\u202f: the parallel syntax for proof-theory. In: Ursini, A., Agliano, P. (eds.) Logic and Algebra. Marcel Dekker, New York (1996)"},{"key":"19_CR25","doi-asserted-by":"publisher","unstructured":"Guglielmi, A., Gundersen, T., Parigot, M.: A proof calculus which reduces syntactic bureaucracy. In: Lynch, C. (ed.) Proceedings of the 21st International Conference on Rewriting Techniques and Applications, LIPIcs, vol. 6, pp. 135\u2013150. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2010). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2010.135. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2010\/2649","DOI":"10.4230\/LIPIcs.RTA.2010.135"},{"key":"19_CR26","doi-asserted-by":"publisher","unstructured":"Heijltjes, W., Hughes, D., Stra\u00dfburger, L.: Intuitionistic proofs without syntax. In: LICS 2019\u201334th Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 1\u201313. IEEE, Vancouver (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785827. https:\/\/hal.inria.fr\/hal-02386878","DOI":"10.1109\/LICS.2019.8785827"},{"key":"19_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-540-73595-3_9","volume-title":"Automated Deduction \u2013 CADE-21","author":"S Heilala","year":"2007","unstructured":"Heilala, S., Pientka, B.: Bidirectional decision procedures for the intuitionistic propositional modal logic IS4. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 116\u2013131. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_9"},{"issue":"3","key":"19_CR28","doi-asserted-by":"publisher","first-page":"1065","DOI":"10.4007\/annals.2006.164.1065","volume":"164","author":"D Hughes","year":"2006","unstructured":"Hughes, D.: Proofs Without Syntax. Ann. Math. 164(3), 1065\u20131076 (2006). https:\/\/doi.org\/10.4007\/annals.2006.164.1065","journal-title":"Ann. Math."},{"key":"19_CR29","doi-asserted-by":"publisher","unstructured":"Hyland, J.M.E., Ong, C.L.: On full abstraction for PCF: i, ii, and III. Inf. Comput. 163(2), 285\u2013408 (2000). https:\/\/doi.org\/10.1006\/inco.2000.2917","DOI":"10.1006\/inco.2000.2917"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"Hyland, J.M.E., Ong, C.H.L.: On full abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model. Inf. Comput. 163, 285\u2013408 (2000)","DOI":"10.1006\/inco.2000.2917"},{"issue":"2","key":"19_CR31","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1017\/S0956796800001301","volume":"5","author":"CB Jay","year":"1995","unstructured":"Jay, C.B., Ghani, N.: The virtues of eta-expansion. J. Funct. Program. 5(2), 135\u2013154 (1995). https:\/\/doi.org\/10.1017\/S0956796800001301","journal-title":"J. Funct. Program."},{"key":"19_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-540-76637-7_27","volume-title":"Programming Languages and Systems","author":"Y Kakutani","year":"2007","unstructured":"Kakutani, Y.: Call-by-name and call-by-value in normal modal logic. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 399\u2013414. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-76637-7_27"},{"key":"19_CR33","doi-asserted-by":"publisher","unstructured":"Kavvos, G.A.: Dual-context calculi for modal logic. Log. Methods Comput. Sci. 16(3) (2020). https:\/\/doi.org\/10.23638\/LMCS-16(3:10)2020","DOI":"10.23638\/LMCS-16(3:10)2020"},{"key":"19_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-540-74915-8_20","volume-title":"Computer Science Logic","author":"D Kesner","year":"2007","unstructured":"Kesner, D.: The theory of calculi with explicit substitutions revisited. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 238\u2013252. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74915-8_20"},{"key":"19_CR35","doi-asserted-by":"crossref","unstructured":"Kesner, D.: A theory of explicit substitutions with safe and full composition. Log. Methods Comput. Sci. 5(3) (2009). http:\/\/arxiv.org\/abs\/0905.2539","DOI":"10.2168\/LMCS-5(3:1)2009"},{"key":"19_CR36","unstructured":"Kojima, K.: Semantical study of intuitionistic modal logics. Ph.D. thesis, Kyoto University (2012)"},{"key":"19_CR37","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983). https:\/\/doi.org\/10.1016\/0304-3975(82)90125-6","journal-title":"Theor. Comput. Sci."},{"key":"19_CR38","unstructured":"Krivine, J.: Lambda-calculus, types and models. Ellis Horwood series in computers and their applications, Masson (1993)"},{"key":"19_CR39","unstructured":"Kuznets, R., Marin, S., Stra\u00dfburger, L.: Justification logic for constructive modal logic. J. Appl. Logics IfCoLog J. Logics Appl. 8(8), 2313\u20132332 (2021). https:\/\/hal.inria.fr\/hal-01614707"},{"issue":"12","key":"19_CR40","doi-asserted-by":"publisher","first-page":"1465","DOI":"10.1016\/j.ic.2011.10.003","volume":"209","author":"M Mendler","year":"2011","unstructured":"Mendler, M., Scheele, S.: Cut-free Gentzen calculus for multimodal CK. Inf. Comput. 209(12), 1465\u20131490 (2011)","journal-title":"Inf. Comput."},{"key":"19_CR41","doi-asserted-by":"publisher","unstructured":"Meyer, J.J., Veltmanw, F.: Intelligent agents and common sense reasoning. In: Blackburn, P., Van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol. 3, pp. 991\u20131029. Elsevier (2007). https:\/\/doi.org\/10.1016\/S1570-2464(07)80021-8. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1570246407800218","DOI":"10.1016\/S1570-2464(07)80021-8"},{"key":"19_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-662-48899-7_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Miller","year":"2015","unstructured":"Miller, D., Volpe, M.: Focused labeled proof systems for modal logic. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 266\u2013280. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_19"},{"key":"19_CR43","doi-asserted-by":"publisher","DOI":"10.1007\/BF01404107","author":"GE Mints","year":"1981","unstructured":"Mints, G.E.: Closed categories and the theory of proofs. J. Soviet Math. (1981). https:\/\/doi.org\/10.1007\/BF01404107","journal-title":"J. Soviet Math."},{"key":"19_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/3-540-44622-2_29","volume-title":"Computer Science Logic","author":"AS Murawski","year":"2000","unstructured":"Murawski, A.S., Ong, C.-H.L.: Discreet games, light affine logic and PTIME computation. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 427\u2013441. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44622-2_29"},{"issue":"4","key":"19_CR45","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1017\/S0960129501003322","volume":"11","author":"F Pfenning","year":"2001","unstructured":"Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci. 11(4), 511\u2013540 (2001). https:\/\/doi.org\/10.1017\/S0960129501003322","journal-title":"Math. Struct. Comput. Sci."},{"key":"19_CR46","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October\u20131 November 1977, pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"19_CR47","unstructured":"Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Almquist and Wiksell (1965)"},{"key":"19_CR48","unstructured":"Simpson, A.: The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. thesis, University of Edinburgh (1994)"},{"key":"19_CR49","volume-title":"Lectures on the Curry-Howard Isomorphism","author":"MH S\u00f8rensen","year":"2006","unstructured":"S\u00f8rensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Elsevier, Amsterdam (2006)"},{"key":"19_CR50","unstructured":"Terese: Term rewriting systems. Cambridge University Press (2003)"},{"key":"19_CR51","unstructured":"Tubella, A.A., Stra\u00dfburger, L.: Introduction to Deep Inference (2019). https:\/\/hal.inria.fr\/hal-02390267. lecture"},{"key":"19_CR52","first-page":"433","volume":"90","author":"D Vakarelov","year":"1991","unstructured":"Vakarelov, D.: Modal logics for knowledge representation systems. Theor. Comput. Sci. 90, 433\u2013456 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"19_CR53","doi-asserted-by":"publisher","unstructured":"Valliappan, N., Ruch, F., Tom\u2019e Corti nas, C.: Normalization for fitch-style modal calculi. Proc. ACM Program. Lang. 6(ICFP), 772\u2013798 (2022). https:\/\/doi.org\/10.1145\/3547649","DOI":"10.1145\/3547649"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-43513-3_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T14:07:32Z","timestamp":1694614052000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-43513-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031435126","9783031435133"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-43513-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"14 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/tableaux2023.tableaux-ar.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"47% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3 (2.92)","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}