{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:47:10Z","timestamp":1742914030012,"version":"3.40.3"},"publisher-location":"Cham","reference-count":55,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031408748"},{"type":"electronic","value":"9783031408755"}],"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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-40875-5_3","type":"book-chapter","created":{"date-parts":[[2023,8,1]],"date-time":"2023-08-01T18:02:22Z","timestamp":1690912942000},"page":"25-43","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Solving Modal Logic Problems by\u00a0Translation to\u00a0Higher-Order Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8781-9462","authenticated-orcid":false,"given":"Alexander","family":"Steen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9120-3927","authenticated-orcid":false,"given":"Geoff","family":"Sutcliffe","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7730-5852","authenticated-orcid":false,"given":"Tobias","family":"Scholl","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3392-3093","authenticated-orcid":false,"given":"Christoph","family":"Benzm\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,8,2]]},"reference":[{"issue":"2","key":"3_CR1","doi-asserted-by":"publisher","first-page":"395","DOI":"10.2307\/2272982","volume":"37","author":"P Andrews","year":"1972","unstructured":"Andrews, P.: General models and extensionality. J. Symbolic Logic 37(2), 395\u2013397 (1972)","journal-title":"J. Symbolic Logic"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"3_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2269159","volume":"11","author":"R Barcan","year":"1946","unstructured":"Barcan, R.: A functional calculus of first order based on strict implication. J. Symbolic Logic 11, 1\u201316 (1946)","journal-title":"J. Symbolic Logic"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-030-79876-5_23","volume-title":"Automated Deduction \u2013 CADE 28","author":"A Bentkamp","year":"2021","unstructured":"Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovi\u0107, P.: Superposition for full higher-order logic. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 396\u2013412. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_23"},{"issue":"4","key":"3_CR5","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.2178\/jsl\/1102022211","volume":"69","author":"C Benzm\u00fcller","year":"2004","unstructured":"Benzm\u00fcller, C., Brown, C., Kohlhase, M.: Higher-order semantics and extensionality. J. Symbolic Logic 69(4), 1027\u20131088 (2004)","journal-title":"J. Symbolic Logic"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Miller, D.: Automation of higher-order logic. In: Gabbay, D., Siekmann, J., Woods, J. (eds.) Handbook of the History of Logic, vol. 9 - Computational Logic, pp. 215\u2013254. North Holland, Elsevier (2014)","DOI":"10.1016\/B978-0-444-51624-4.50005-8"},{"key":"3_CR7","unstructured":"Benzm\u00fcller, C., Otten, J., Raths, T.: Implementing and evaluating provers for first-order modal logics. In: De Raedt, L., et al. (eds.) Proceedings of the 20th European Conference on Artificial Intelligence, pp. 163\u2013168. Frontiers in Artificial Intelligence and Applications, IOS Press (2012)"},{"issue":"1","key":"3_CR8","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s11787-012-0052-y","volume":"7","author":"C Benzm\u00fcller","year":"2013","unstructured":"Benzm\u00fcller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Logica Univ. 7(1), 7\u201320 (2013)","journal-title":"Logica Univ."},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-45221-5_9","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Benzm\u00fcller","year":"2013","unstructured":"Benzm\u00fcller, C., Raths, T.: HOL based first-order modal logic provers. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 127\u2013136. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_9"},{"key":"3_CR10","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: The inconsistency in g\u00f6del\u2019s ontological argument: a success story for AI in metaphysics. In: Kambhampati, S. (ed.) Proceedings of the 25th International Joint Conference on Artificial Intelligence, pp. 936\u2013942. AAAI Press (2016)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-030-51074-9_16","volume-title":"Automated Reasoning","author":"A Bhayat","year":"2020","unstructured":"Bhayat, A., Reger, G.: A combinator-based superposition calculus for higher-order logic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 278\u2013296. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_16"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Blackburn, P., van Benthem, J., Wolther, F.: Handbook of Modal Logic. No. 3 in Studies in Logic and Practical Reasoning, Elsevier Science (2006)","DOI":"10.1002\/9780470996751.ch27"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2001)","DOI":"10.1017\/CBO9781107050884"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_11"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","volume-title":"Automated Reasoning","author":"CE Brown","year":"2012","unstructured":"Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 111\u2013117. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_11"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/3-540-45744-5_38","volume-title":"Automated Reasoning","author":"LF del Cerro","year":"2001","unstructured":"del Cerro, L.F., Fauthoux, D., Gasquet, O., Herzig, A., Longin, D., Massacci, F.: Lotrec: the generic tableau prover for modal and description logics. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 453\u2013458. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45744-5_38"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symbolic Logic 5, 56\u201368 (1940)","journal-title":"J. Symbolic Logic"},{"key":"3_CR18","unstructured":"van Ditmarsch, H., Halpern, J., van der Hoek, W., Kooi, B.: Handbook of Epistemic Logic. College Publications, Norcross (2015)"},{"key":"3_CR19","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: MiniSat - a SAT solver with conflict-clause minimization. In: Bacchus, F., Walsh, T. (eds.) Posters of the 8th International Conference on Theory and Applications of Satisfiability Testing (2005)"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Fitting, M., Mendelsohn, R.: First-Order Modal Logic. Kluwer (1998)","DOI":"10.1007\/978-94-011-5292-1"},{"key":"3_CR21","unstructured":"Frege, F.: Grundgesetze der Arithmetik. Jena (1893 1903"},{"key":"3_CR22","unstructured":"Garson, J.: Modal Logic. In: Zalta, E. (ed.) Stanford Encyclopedia of Philosophy. Stanford University, Stanford (2018)"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Gibbons, J., Wu, N.: Folding domain-specific languages: deep and shallow embeddings (Functional Pearl). In: Jeuring, J., Chakravarty, M. (eds.) Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pp. 339\u2013347. ACM Press (2014)","DOI":"10.1145\/2628136.2628138"},{"key":"3_CR24","unstructured":"Glei\u00dfner, T.: A Framework for Higher-Order Modal Logic Theorem Proving. Master\u2019s thesis, Freie Universit\u00e4t Berlin, Berlin, Germany (2019)"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Glei\u00dfner, T., Steen, A., Benzm\u00fcller, C.: Theorem provers for every normal modal logic. In: Eiter, T., Sands, D. (eds.) Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, pp. 14\u201330. No. 46 in EPiC Series in Computing, EasyChair Publications (2017)","DOI":"10.29007\/jsb9"},{"key":"3_CR26","unstructured":"Gordon, M., Melham, T.: Introduction to HOL, a Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265\u2013269. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0031814"},{"issue":"2","key":"3_CR28","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L Henkin","year":"1950","unstructured":"Henkin, L.: Completeness in the theory of types. J. Symbolic Logic 15(2), 81\u201391 (1950)","journal-title":"J. Symbolic Logic"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/10722086_7","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"U Hustadt","year":"2000","unstructured":"Hustadt, U., Schmidt, R.A.: MSPASS: modal reasoning by translation and first-order resolution. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS (LNAI), vol. 1847, pp. 67\u201371. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722086_7"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J.: HOL(y)Hammer: online ATP service for HOL Light (2013). arXiv:1309.4962","DOI":"10.1007\/978-3-642-39320-4_8"},{"key":"3_CR31","first-page":"83","volume":"16","author":"S Kripke","year":"1963","unstructured":"Kripke, S.: Semantical considerations on modal logic. Acta Philosophica Fennica 16, 83\u201394 (1963)","journal-title":"Acta Philosophica Fennica"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-08587-6_5","volume-title":"Automated Reasoning","author":"F Lindblad","year":"2014","unstructured":"Lindblad, F.: A focused sequent calculus for higher-order logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 61\u201375. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_5"},{"issue":"3","key":"3_CR33","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: architecture, refinements, strategies and experiments. J. Autom. Reasoning 64(3), 461\u2013484 (2020)","journal-title":"J. Autom. Reasoning"},{"key":"3_CR34","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): : 5. the rules of the game. In: Isabelle\/HOL. LNCS, vol. 2283, pp. 67\u2013104. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9_5","DOI":"10.1007\/3-540-45949-9_5"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-319-08587-6_20","volume-title":"Automated Reasoning","author":"J Otten","year":"2014","unstructured":"Otten, J.: MleanCoP: a connection prover for first-order modal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 269\u2013276. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_20"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-030-86059-2_14","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J Otten","year":"2021","unstructured":"Otten, J.: The nanoCoP 2.0 connection provers for classical, intuitionistic and modal logics. In: Das, A., Negri, S. (eds.) TABLEAUX 2021. LNCS (LNAI), vol. 12842, pp. 236\u2013249. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86059-2_14"},{"key":"3_CR37","unstructured":"Otten, J., Sutcliffe, G.: Using the TPTP language for representing derivations in tableau and connection Calculi. In: Konev, B., Schmidt, R., Schulz, S. (eds.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning, 5th International Joint Conference on Automated Reasoning, pp. 90\u2013100 (2010)"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.: PVS: combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411\u2013414. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_91"},{"key":"3_CR39","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":"3_CR40","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-642-31365-3_35","volume-title":"Automated Reasoning","author":"T Raths","year":"2012","unstructured":"Raths, T., Otten, J.: The QMLTP problem library for first-order modal logics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 454\u2013461. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_35"},{"key":"3_CR41","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-030-29436-6_29","volume-title":"Automated Deduction \u2013 CADE 27","author":"S Schulz","year":"2019","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 495\u2013507. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29"},{"issue":"4","key":"3_CR42","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1016\/j.jal.2005.10.008","volume":"4","author":"J Siekmann","year":"2006","unstructured":"Siekmann, J., Benzm\u00fcller, C., Autexier, S.: Computer Supported Mathematics with OMEGA. J. Appl. Logic 4(4), 533\u2013559 (2006)","journal-title":"J. Appl. Logic"},{"key":"3_CR43","unstructured":"Steen, A.: An extensible logic embedding tool for lightweight non-classical reasoning (2022). arXiv:2203.12352"},{"key":"3_CR44","doi-asserted-by":"publisher","unstructured":"Steen, A.: logic-embedding v1.6 (2022). https:\/\/doi.org\/10.5281\/zenodo.5913216","DOI":"10.5281\/zenodo.5913216"},{"key":"3_CR45","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-319-94205-6_8","volume-title":"Automated Reasoning","author":"A Steen","year":"2018","unstructured":"Steen, A., Benzm\u00fcller, C.: The higher-order prover leo-III. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 108\u2013116. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_8"},{"key":"3_CR46","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367\u2013373. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28"},{"key":"3_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-540-74510-5_4","volume-title":"Computer Science \u2013 Theory and Applications","author":"G Sutcliffe","year":"2007","unstructured":"Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds.) CSR 2007. LNCS, vol. 4649, pp. 6\u201322. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74510-5_4"},{"key":"3_CR48","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017)","DOI":"10.1007\/s10817-017-9407-7"},{"key":"3_CR49","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G.: The logic languages of the TPTP World. Logic J. IGPL (2022). https:\/\/doi.org\/10.1093\/jigpal\/jzac068","DOI":"10.1093\/jigpal\/jzac068"},{"issue":"1","key":"3_CR50","first-page":"1","volume":"3","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G., Benzm\u00fcller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formalized Reasoning 3(1), 1\u201327 (2010)","journal-title":"J. Formalized Reasoning"},{"key":"3_CR51","unstructured":"Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP data-exchange formats for automated theorem proving tools. In: Zhang, W., Sorge, V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, pp. 201\u2013215. No. 112 in Frontiers in Artificial Intelligence and Applications, IOS Press (2004)"},{"key":"3_CR52","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/3-540-45616-3_19","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"V Thion","year":"2002","unstructured":"Thion, V., Cerrito, S., Mayer, M.C.: A general theorem prover for quantified modal logics. In: Egly, U., Ferm\u00fcller, C.G. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 266\u2013280. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45616-3_19"},{"key":"3_CR53","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-642-33353-8_41","volume-title":"Logics in Artificial Intelligence","author":"D Tishkovsky","year":"2012","unstructured":"Tishkovsky, D., Schmidt, R.A., Khodadadi, M.: The tableau prover generator MetTeL2. In: del Cerro, L.F., Herzig, A., Mengin, J. (eds.) JELIA 2012. LNCS (LNAI), vol. 7519, pp. 492\u2013495. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33353-8_41"},{"key":"3_CR54","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-79876-5_24","volume-title":"Automated Deduction \u2013 CADE 28","author":"P Vukmirovi\u0107","year":"2021","unstructured":"Vukmirovi\u0107, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 415\u2013432. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_24"},{"key":"3_CR55","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10"}],"container-title":["Lecture Notes in Computer Science","Logic and Argumentation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-40875-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,25]],"date-time":"2024-10-25T14:06:13Z","timestamp":1729865173000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-40875-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031408748","9783031408755"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-40875-5_3","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":"2 August 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CLAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Logic and Argumentation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","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":"10 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"clar2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.zlaire.net\/zjulogai2023\/clar2023\/","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":"20","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":"11","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":"1","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":"55% - 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","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":"1","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)"}}]}}