{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:07:46Z","timestamp":1784844466032,"version":"3.55.0"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031435126","type":"print"},{"value":"9783031435133","type":"electronic"}],"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>We present resolution calculi for the cube of classical non-normal modal logics. The calculi are based on a simple clausal form that comprises both local and global clauses. Any formula can be efficiently transformed into a small set of clauses. The calculi contain uniform rules and provide a decision procedure for all logics. Their completeness is based on a new and crucial notion of inconsistency predicate, needed to ensure the usual closure properties of maximal consistent sets. As far as we know the calculi presented here are the first resolution calculi for this class of logics.<\/jats:p>","DOI":"10.1007\/978-3-031-43513-3_18","type":"book-chapter","created":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T14:02:36Z","timestamp":1694613756000},"page":"322-341","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Resolution Calculi for\u00a0Non-normal Modal Logics"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5832-6666","authenticated-orcid":false,"given":"Dirk","family":"Pattinson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6254-3754","authenticated-orcid":false,"given":"Nicola","family":"Olivetti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9792-5346","authenticated-orcid":false,"given":"Cl\u00e1udia","family":"Nalon","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,9,14]]},"reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-16780-3_89","volume-title":"8th International Conference on Automated Deduction","author":"M Abadi","year":"1986","unstructured":"Abadi, M., Manna, Z.: Modal theorem proving. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 172\u2013189. Springer, Heidelberg (1986). https:\/\/doi.org\/10.1007\/3-540-16780-3_89"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-48660-7_13","volume-title":"Automated Deduction \u2014 CADE-16","author":"C Areces","year":"1999","unstructured":"Areces, C., de Nivelle, H., de Rijke, M.: Prefixed resolution: a resolution method for modal and description logics. In: CADE 1999. LNCS (LNAI), vol. 1632, pp. 187\u2013201. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_13"},{"issue":"2","key":"18_CR3","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0020-0190(88)90169-X","volume":"28","author":"Y Auffray","year":"1988","unstructured":"Auffray, Y.: Linear strategy for propositional modal resolution. Inf. Process. Lett. 28(2), 87\u201392 (1988)","journal-title":"Inf. Process. Lett."},{"key":"18_CR4","unstructured":"del Cerro, L.F.: Resolution modal logics. In: Proceedings of Advanced NATO Study Institute on Logics and Models for Verification and Specification of Concurrent Systems, La Colle-sur-Loup, France, pp. 46\u201378 (1984)"},{"issue":"2","key":"18_CR5","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0020-0190(82)90085-0","volume":"14","author":"LF del Cerro","year":"1982","unstructured":"del Cerro, L.F.: A simple deduction method for modal logic. Inf. Process. Lett. 14(2), 49\u201351 (1982)","journal-title":"Inf. Process. Lett."},{"key":"18_CR6","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/BF03037397","volume":"5","author":"MC Chan","year":"1987","unstructured":"Chan, M.C.: The recursive resolution method for modal logic. N. Gener. Comput. 5, 155\u2013183 (1987)","journal-title":"N. Gener. Comput."},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Chellas, B.F.: Modal Logic. Cambridge (1980)","DOI":"10.1017\/CBO9780511621192"},{"key":"18_CR8","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/0304-3975(91)90181-Z","volume":"85","author":"M Cialdea","year":"1991","unstructured":"Cialdea, M.: Resolution for some first-order modal systems. Theor. Comput. Sci. 85, 213\u2013229 (1991)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"18_CR9","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1093\/logcom\/exaa072","volume":"31","author":"T Dalmonte","year":"2021","unstructured":"Dalmonte, T., Lellmann, B., Olivetti, N., Pimentel, E.: Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity. J. Log. Comput. 31(1), 67\u2013111 (2021)","journal-title":"J. Log. Comput."},{"key":"18_CR10","unstructured":"Dalmonte, T., Olivetti, N., Negri, S.: Non-normal modal logics: bi-neighbourhood semantics and its labelled calculi. In: Bezhanishvili, G., D\u2019Agostino, G., Metcalfe, G., Studer, T. (eds.) Proceedings of the AiML 2018 (2018)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-030-51054-1_24","volume-title":"Automated Reasoning","author":"A Duarte","year":"2020","unstructured":"Duarte, A., Korovin, K.: Implementing superposition in iProver (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 388\u2013397. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_24"},{"key":"18_CR12","first-page":"1","volume":"2","author":"D Elgesem","year":"1997","unstructured":"Elgesem, D.: The modal logic of agency. Nord. J. Philos. Log. 2, 1\u201346 (1997)","journal-title":"Nord. J. Philos. Log."},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(89)90137-0","volume":"65","author":"P Enjalbert","year":"1989","unstructured":"Enjalbert, P., del Cerro, L.F.: Modal resolution in clausal form. Theor. Comput. Sci. 65, 1\u201333 (1989)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR14","unstructured":"Fitting, M.C.: Destructive Modal Resolution. CUNY Technical Report (1989)"},{"issue":"1","key":"18_CR15","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s11225-014-9556-1","volume":"103","author":"DR Gilbert","year":"2015","unstructured":"Gilbert, D.R., Maffezioli, P.: Modular sequent calculi for classical modal logics. Stud. Logica. 103(1), 175\u2013217 (2015)","journal-title":"Stud. Logica."},{"issue":"2","key":"18_CR16","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1023\/A:1015071400913","volume":"28","author":"E Giunchiglia","year":"2002","unstructured":"Giunchiglia, E., Tacchella, A., Giunchiglia, F.: SAT-based decision procedures for classical modal logics. J. Autom. Reason. 28(2), 143\u2013171 (2002)","journal-title":"J. Autom. Reason."},{"key":"18_CR17","doi-asserted-by":"publisher","unstructured":"Glei\u00dfner, T., Steen, A.: Leo-III (2022). https:\/\/doi.org\/10.5281\/zenodo.4435994. Accessed 24 July 2023","DOI":"10.5281\/zenodo.4435994"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-030-86059-2_5","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R Gor\u00e9","year":"2021","unstructured":"Gor\u00e9, R., Kikkert, C.: CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT. In: Das, A., Negri, S. (eds.) TABLEAUX 2021. LNCS (LNAI), vol. 12842, pp. 74\u201391. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86059-2_5"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-319-08587-6_25","volume-title":"Automated Reasoning","author":"R Gor\u00e9","year":"2014","unstructured":"Gor\u00e9, R., Olesen, K., Thomson, J.: Implementing tableau calculi using BDDs: BDDTab system description. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 337\u2013343. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_25"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"G\u00f6tzmann, D., Kaminski, M., Smolka, G.: Spartacus: a tableau prover for hybrid logic. Electron. Notes Theor. Comput. Sci. 262 (2010)","DOI":"10.1016\/j.entcs.2010.04.010"},{"issue":"2\u20133","key":"18_CR21","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39(2\u20133), 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"18_CR22","first-page":"151","volume":"34","author":"A Indrzejczak","year":"2005","unstructured":"Indrzejczak, A.: Sequent calculi for monotonic modal logics. Bull. Section Logic 34(3), 151\u2013164 (2005)","journal-title":"Bull. Section Logic"},{"key":"18_CR23","first-page":"189","volume":"21","author":"A Indrzejczak","year":"2011","unstructured":"Indrzejczak, A.: Admissibility of cut in congruent modal logics. Logic Log. Philos. 21, 189\u2013203 (2011)","journal-title":"Logic Log. Philos."},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-38574-2_31","volume-title":"Automated Deduction \u2013 CADE-24","author":"M Kaminski","year":"2013","unstructured":"Kaminski, M., Tebbi, T.: InKreSAT: modal reasoning via incremental reduction to SAT. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 436\u2013442. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_31"},{"key":"18_CR25","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1023\/A:1026753129680","volume":"65","author":"R Lavendhomme","year":"2000","unstructured":"Lavendhomme, R., Lucas, T.: Sequent calculi and decision procedures for weak modal systems. Stud. Logica. 65, 121\u2013145 (2000)","journal-title":"Stud. Logica."},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Lellmann, B., Pimentel, E.: Modularisation of sequent calculi for normal and non-normal modalities. ACM Trans. Comput. Logic 20(2), 7:1\u20137:46 (2019)","DOI":"10.1145\/3288757"},{"key":"18_CR27","unstructured":"McCune, W.W.: OTTER Users\u2019 Guide, Version 3.3 (2003). Argonne National Laboratory"},{"key":"18_CR28","unstructured":"McCune, W.W.: Prover9 and mace4 (2010). http:\/\/www.cs.unm.edu\/~mccune\/prover9\/. Accessed 24 July 2023"},{"key":"18_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/3-540-52335-9_55","volume-title":"COLOG-88","author":"G Mints","year":"1990","unstructured":"Mints, G.: Gentzen-type systems and resolution rules part I propositional logic. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 198\u2013231. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52335-9_55"},{"key":"18_CR30","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.jalgor.2007.04.001","volume":"62","author":"C Nalon","year":"2007","unstructured":"Nalon, C., Dixon, C.: Clausal resolution for normal modal logics. J. Algorithms 62, 117\u2013134 (2007)","journal-title":"J. Algorithms"},{"key":"18_CR31","doi-asserted-by":"crossref","unstructured":"Nalon, C., Dixon, C., Hustadt, U.: Modal resolution: proofs, layers, and refinements. ACM Trans. Comput. Logic 20(4), 23:1\u201323:38 (2019)","DOI":"10.1145\/3331448"},{"key":"18_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-319-40229-1_28","volume-title":"Automated Reasoning","author":"C Nalon","year":"2016","unstructured":"Nalon, C., Hustadt, U., Dixon, C.: KSP: a resolution-based prover for multimodal K. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 406\u2013415. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_28"},{"key":"18_CR33","doi-asserted-by":"crossref","unstructured":"Nalon, C., Hustadt, U., Dixon, C.: KSP: a resolution-based prover for multimodal K, abridged report. In: Sierra, C. (ed.) Proceedings of the IJCAI 2017, pp. 4919\u20134923. IJCAI\/AAAI Press (2017)","DOI":"10.24963\/ijcai.2017\/694"},{"issue":"3","key":"18_CR34","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/s10817-018-09503-x","volume":"64","author":"C Nalon","year":"2020","unstructured":"Nalon, C., Hustadt, U., Dixon, C.: KSP a resolution-based theorem prover for $$K_n$$: architecture, refinements, strategies and experiments. J. Autom. Reason. 64(3), 461\u2013484 (2020)","journal-title":"J. Autom. Reason."},{"key":"18_CR35","doi-asserted-by":"crossref","unstructured":"Nalon, C., Hustadt, U., Papacchini, F., Dixon, C.: Local reductions for the modal cube. In: Proceedings of the IJCAR 2022 (2022)","DOI":"10.1007\/978-3-031-10769-6_29"},{"key":"18_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-319-08587-6_24","volume-title":"Automated Reasoning","author":"C Nalon","year":"2014","unstructured":"Nalon, C., Marcos, J., Dixon, C.: Clausal resolution for modal logics of confluence. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 322\u2013336. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_24"},{"issue":"4","key":"18_CR37","first-page":"1241","volume":"4","author":"S Negri","year":"2017","unstructured":"Negri, S.: Proof theory for non-normal modal logics: the neighbourhood formalism and basic results. IfCoLog J. Appl. Log. 4(4), 1241\u20131286 (2017)","journal-title":"IfCoLog J. Appl. Log."},{"issue":"3","key":"18_CR38","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1093\/jigpal\/8.3.265","volume":"8","author":"H de Nivelle","year":"2000","unstructured":"de Nivelle, H., Schmidt, R.A., Hustadt, U.: Resolution-based methods for modal logics. Logic J. IGPL 8(3), 265\u2013292 (2000)","journal-title":"Logic J. IGPL"},{"issue":"5","key":"18_CR39","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1093\/logcom\/1.5.691","volume":"1","author":"HJ Ohlbach","year":"1990","unstructured":"Ohlbach, H.J.: Semantics-based translation methods for modal logics. J. Log. Comput. 1(5), 691\u2013746 (1990)","journal-title":"J. Log. Comput."},{"key":"18_CR40","doi-asserted-by":"crossref","unstructured":"Ohlbach, H.J., Schmidt, R.A., Hustadt, U.: Translating graded modalities into predicate logics. In: Wansing, H. (ed.) Proof Theory of Modal Logic, Applied Logic Series, vol. 2, pp. 253\u2013291. Kluwer Academic Publishers (1996)","DOI":"10.1007\/978-94-017-2798-3_14"},{"key":"18_CR41","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-319-08615-6_11","volume-title":"Deontic Logic and Normative Systems","author":"E Orlandelli","year":"2014","unstructured":"Orlandelli, E.: Proof analysis in deontic logics. In: Cariani, F., Grossi, D., Meheus, J., Parent, X. (eds.) DEON 2014. LNCS (LNAI), vol. 8554, pp. 139\u2013148. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08615-6_11"},{"issue":"1","key":"18_CR42","first-page":"139","volume":"30","author":"E Orlandelli","year":"2020","unstructured":"Orlandelli, E.: Sequent calculi and interpolation for non-normal modal and deontic logics. Logic Log. Philos. 30(1), 139\u2013183 (2020)","journal-title":"Logic Log. Philos."},{"key":"18_CR43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67149-9","volume-title":"Neighborhood Semantics for Modal Logic","author":"E Pacuit","year":"2017","unstructured":"Pacuit, E.: Neighborhood Semantics for Modal Logic. Springer, Heidelberg (2017)"},{"key":"18_CR44","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-030-79876-5_5","volume-title":"Automated Deduction \u2013 CADE 28","author":"F Papacchini","year":"2021","unstructured":"Papacchini, F., Nalon, C., Hustadt, U., Dixon, C.: Efficient local reductions to basic modal logic. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 76\u201392. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_5"},{"key":"18_CR45","first-page":"293","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.A.: A structure-preserving clause form translation. J. Log. Comput. 2, 293\u2013304 (1986)","journal-title":"J. Log. Comput."},{"issue":"1","key":"18_CR46","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"18_CR47","unstructured":"Schulz, S.: E 2.6 (2022). http:\/\/wwwlehre.dhbw-stuttgart.de\/~sschulz\/E\/Download.html. Accessed 24 July 2023"},{"key":"18_CR48","unstructured":"Sutcliff, G. (ed.): Proceedings of the 11th IJCAR ATP System Competition (CASC-J11) (2022). https:\/\/www.tptp.org\/CASC\/J11\/. Accessed 24 July 2023"},{"key":"18_CR49","unstructured":"The SPASS Team: Spass 3.9 (2016). http:\/\/www.spass-prover.org\/. Accessed 24 July 2023"},{"key":"18_CR50","unstructured":"The Vampire Team: Vampire 4.7 (2022). https:\/\/github.com\/vprover\/vampire\/releases. Accessed 24 July 2023"},{"key":"18_CR51","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/11814771_26","volume-title":"Automated Reasoning","author":"D Tsarkov","year":"2006","unstructured":"Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: system description. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 292\u2013297. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_26"},{"key":"18_CR52","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: On the complexity of epistemic reasoning. In: Proceedings of the LICS 1989, pp. 243\u2013252. IEEE Computer Society (1989)","DOI":"10.1109\/LICS.1989.39179"}],"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_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T01:12:26Z","timestamp":1730077946000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-43513-3_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031435126","9783031435133"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-43513-3_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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)"}}]}}