{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T13:06:43Z","timestamp":1763644003141,"version":"3.40.5"},"publisher-location":"Cham","reference-count":25,"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>This paper studies nested sequents for quantified modal logics. In particular, it considers extensions of the propositional modal logics definable by the axioms<jats:bold>D<\/jats:bold>,<jats:bold>T<\/jats:bold>,<jats:bold>B<\/jats:bold>,<jats:bold>4<\/jats:bold>, and<jats:bold>5<\/jats:bold>with varying, increasing, decreasing, and constant domains. Each calculus is proved to have good structural properties: weakening and contraction are height-preserving admissible and cut is (syntactically) admissible. Each calculus is shown to be equivalent to the corresponding axiomatic system and, thus, to be sound and complete. Finally, it is argued that the calculi are internal\u2014i.e., each sequent has a formula interpretation\u2014whenever the existence predicate is expressible in the language.<\/jats:p>","DOI":"10.1007\/978-3-031-43513-3_24","type":"book-chapter","created":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T14:02:36Z","timestamp":1694613756000},"page":"449-467","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Nested Sequents for\u00a0Quantified Modal Logics"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3214-0828","authenticated-orcid":false,"given":"Tim S.","family":"Lyon","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4021-8667","authenticated-orcid":false,"given":"Eugenio","family":"Orlandelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,9,14]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Avron, A.: The method of hypersequents in the proof theory of propositional non-classical logics. In: From Foundations to Applications: European Logic Colloquium, USA, pp. 1\u201332. Clarendon Press (2010)","DOI":"10.1093\/oso\/9780198538622.003.0001"},{"issue":"4","key":"24_CR2","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/BF00284976","volume":"11","author":"ND Belnap","year":"1982","unstructured":"Belnap, N.D.: Display logic. J. Philos. Logic 11(4), 375\u2013417 (1982). https:\/\/doi.org\/10.1007\/BF00284976","journal-title":"J. Philos. Logic"},{"key":"24_CR3","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/s00153-009-0137-3","volume":"48","author":"K Br\u00fcnnler","year":"2009","unstructured":"Br\u00fcnnler, K.: Deep sequent systems for modal logic. Arch. Math. Logic 48, 551\u2013577 (2009). https:\/\/doi.org\/10.1007\/s00153-009-0137-3","journal-title":"Arch. Math. Logic"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-642-16242-8_13","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K Br\u00fcnnler","year":"2010","unstructured":"Br\u00fcnnler, K.: How to universally close the existential rule. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 172\u2013186. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16242-8_13"},{"issue":"1","key":"24_CR5","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1002\/malq.19920380107","volume":"38","author":"R Bull","year":"1992","unstructured":"Bull, R.: Cut elimination for propositional dynamic logic without *. Math. Log. Q. 38(1), 85\u2013100 (1992). https:\/\/doi.org\/10.1002\/malq.19920380107","journal-title":"Math. Log. Q."},{"key":"24_CR6","doi-asserted-by":"publisher","unstructured":"Castilho, M., del Cerro, L., Gasquet, O., Herzig, A.: Modal tableaux with propagation rules and structural rules. Fundamenta Informaticae 32(3,4), 281\u2013297 (1997). https:\/\/doi.org\/10.3233\/FI-1997-323404","DOI":"10.3233\/FI-1997-323404"},{"issue":"2","key":"24_CR7","doi-asserted-by":"publisher","first-page":"1483","DOI":"10.2178\/jsl\/1190150295","volume":"67","author":"G Corsi","year":"2002","unstructured":"Corsi, G.: A unified completeness theorem for quantified modal logics. J. Symb. Logic 67(2), 1483\u20131510 (2002). https:\/\/doi.org\/10.2178\/jsl\/1190150295","journal-title":"J. Symb. Logic"},{"issue":"2","key":"24_CR8","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1305\/ndjfl\/1093894722","volume":"13","author":"M Fitting","year":"1972","unstructured":"Fitting, M.: Tableau methods of proof for modal logics. Notre Dame J. Formal Logic 13(2), 237\u2013247 (1972). https:\/\/doi.org\/10.1305\/ndjfl\/1093894722","journal-title":"Notre Dame J. Formal Logic"},{"issue":"3","key":"24_CR9","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1016\/j.apal.2014.11.002","volume":"166","author":"M Fitting","year":"2015","unstructured":"Fitting, M., Kuznets, R.: Modal interpolation via nested sequents. Ann. Pure Appl. Logic 166(3), 274\u2013305 (2015). https:\/\/doi.org\/10.1016\/j.apal.2014.11.002","journal-title":"Ann. Pure Appl. Logic"},{"key":"24_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-5292-1","volume-title":"First-Order Modal Logic","author":"M Fitting","year":"1998","unstructured":"Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic. Springer, Dordrecht (1998)"},{"issue":"2","key":"24_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-7(2:8)2011","volume":"7","author":"R Gor\u00e9","year":"2011","unstructured":"Gor\u00e9, R., Postniece, L., Tiu, A.: On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Logical Methods Comput. Sci. 7(2), 1\u201338 (2011). https:\/\/doi.org\/10.2168\/LMCS-7(2:8)2011","journal-title":"Logical Methods Comput. Sci."},{"issue":"1","key":"24_CR12","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/BF01053026","volume":"53","author":"R Kashima","year":"1994","unstructured":"Kashima, R.: Cut-free sequent calculi for some tense logics. Stud. Logica. 53(1), 119\u2013135 (1994). https:\/\/doi.org\/10.1007\/BF01053026","journal-title":"Stud. Logica."},{"key":"24_CR13","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"},{"issue":"1","key":"24_CR14","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1093\/logcom\/exaa078","volume":"31","author":"T Lyon","year":"2020","unstructured":"Lyon, T.: On the correspondence between nested calculi and semantic systems for intuitionistic logics. J. Log. Comput. 31(1), 213\u2013265 (2020). https:\/\/doi.org\/10.1093\/logcom\/exaa078","journal-title":"J. Log. Comput."},{"key":"24_CR15","doi-asserted-by":"publisher","unstructured":"Lyon, T.: Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents. In: Fern\u00e1ndez, M., Muscholl, A. (eds.) Annual Conference on Computer Science Logic CSL 2020, vol. 152, pp. 28:1\u201328:16. Leibniz International Proceedings in Informatics (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.28","DOI":"10.4230\/LIPIcs.CSL.2020.28"},{"key":"24_CR16","doi-asserted-by":"publisher","unstructured":"Lyon, T.: Refining labelled systems for modal and constructive logics with applications. Dissertation, Technische Universit\u00e4t Wien (2021). https:\/\/doi.org\/10.34726\/hss.2021.97064","DOI":"10.34726\/hss.2021.97064"},{"key":"24_CR17","doi-asserted-by":"publisher","unstructured":"Lyon, T.: Nested Sequents for First-Order Modal Logics via Reachability Rules. arXiv (2022, unpublished). https:\/\/doi.org\/10.48550\/arXiv.2210.00789","DOI":"10.48550\/arXiv.2210.00789"},{"key":"24_CR18","doi-asserted-by":"publisher","unstructured":"Lyon, T., Orlandelli, E.: Nested Sequents for Quantified Modal Logics. arXiv (2023). https:\/\/doi.org\/10.48550\/arXiv.2210.00789","DOI":"10.48550\/arXiv.2210.00789"},{"issue":"2","key":"24_CR19","doi-asserted-by":"publisher","first-page":"137","DOI":"10.18778\/0138-0680.48.2.04","volume":"48","author":"P Maffezioli","year":"2019","unstructured":"Maffezioli, P., Orlandelli, E.: Full cut elimination and interpolation for intuitionistic logic with existence predicate. Bull. Section Logic 48(2), 137\u2013158 (2019). https:\/\/doi.org\/10.18778\/0138-0680.48.2.04","journal-title":"Bull. Section Logic"},{"key":"24_CR20","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139003513","volume-title":"Proof Analysis: A Contribution to Hilbert\u2019s Last Problem","author":"S Negri","year":"2011","unstructured":"Negri, S., von Plato, J.: Proof Analysis: A Contribution to Hilbert\u2019s Last Problem. Cambridge University Press, Cambridge (2011)"},{"issue":"3","key":"24_CR21","doi-asserted-by":"publisher","first-page":"923","DOI":"10.1093\/logcom\/exab018","volume":"31","author":"E Orlandelli","year":"2021","unstructured":"Orlandelli, E.: Labelled calculi for quantified modal logics with definite descriptions. J. Log. Comput. 31(3), 923\u2013946 (2021). https:\/\/doi.org\/10.1093\/logcom\/exab018","journal-title":"J. Log. Comput."},{"key":"24_CR22","series-title":"Trends in Logic","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-1-4020-9084-4_3","volume-title":"Towards Mathematical Philosophy","author":"F Poggiolesi","year":"2009","unstructured":"Poggiolesi, F.: The method of tree-hypersequents for\u00a0modal\u00a0propositional\u00a0logic. In: Makinson, D., Malinowski, J., Wansing, H. (eds.) Towards Mathematical Philosophy. TL, vol. 28, pp. 31\u201351. Springer, Dordrecht (2009). https:\/\/doi.org\/10.1007\/978-1-4020-9084-4_3"},{"key":"24_CR23","unstructured":"Simpson, A.: The proof theory and semantics of intuitionistic modal logic. Dissertation, University of Edinburgh (1994). https:\/\/www.cs.cmu.edu\/~fp\/courses\/15816-s10\/papers\/Simpson94.pdf"},{"key":"24_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-22119-4_20","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A Tiu","year":"2011","unstructured":"Tiu, A.: A hypersequent system for G\u00f6del-Dummett logic with non-constant domains. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS (LNAI), vol. 6793, pp. 248\u2013262. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22119-4_20"},{"key":"24_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3208-5","volume-title":"Labelled Non-classical Logics","author":"L Vigan\u00f2","year":"2000","unstructured":"Vigan\u00f2, L.: Labelled Non-classical Logics. Springer, Heidelberg (2000)"}],"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_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,21]],"date-time":"2023-12-21T18:32:56Z","timestamp":1703183576000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-43513-3_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031435126","9783031435133"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-43513-3_24","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)"}}]}}