{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:49:46Z","timestamp":1743140986237,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present novel reductions of the propositional modal logics \n\"Image missing\"\n, \n\"Image missing\"\n, \n\"Image missing\"\n, \n\"Image missing\"\n and \n\"Image missing\"\n to Separated Normal Form with Sets of Modal Levels. The reductions result in smaller formulae than the well-known reductions by Kracht and allow us to use the local reasoning of the prover \n\"Image missing\"\n to determine the satisfiability of modal formulae in these logics. We show experimentally that the combination of our reductions with the prover \n\"Image missing\"\n performs well when compared with a specialised resolution calculus for these logics and with the b\u0306uilt-in reductions of the first-order prover SPASS.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_5","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"76-92","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Efficient Local Reductions to Basic Modal Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0310-7378","authenticated-orcid":false,"given":"Fabio","family":"Papacchini","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9792-5346","authenticated-orcid":false,"given":"Cl\u00e1udia","family":"Nalon","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0455-0267","authenticated-orcid":false,"given":"Ullrich","family":"Hustadt","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4610-9533","authenticated-orcid":false,"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"5_CR1","unstructured":"Balbiani, P., Demri, S.: Prefixed tableaux systems for modal logics with enriched languages. In: IJCAI 1997. pp. 190\u2013195. Morgan Kaufmann (1997)"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Balsiger, P., Heuerding, A., Schwendimann, S.: A benchmark method for the propositional modal logics K, KT, S4. J. Autom. Reasoning 24(3), 297\u2013317 (2000)","DOI":"10.1023\/A:1006249507577"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Basin, D., Matthews, S., Vigano, L.: Labelled propositional modal logics: Theory and practice. J. Log. Comput. 7(6), 685\u2013717 (1997)","DOI":"10.1093\/logcom\/7.6.685"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Paulson, L.C.: Multimodal and intuitionistic logics in simple type theory. Log. J. IGPL 18(6), 881\u2013892 (2010)","DOI":"10.1093\/jigpal\/jzp080"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Fitting, M.: Prefixed tableaus and nested sequents. Ann. Pure Appl. Log. 163(3), 291\u2013313 (2012)","DOI":"10.1016\/j.apal.2011.09.004"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Gabbay, D.M.: Decidability results in non-classical logics: Part I. Ann. Math. Log. 8, 237\u2013295 (1975)","DOI":"10.1016\/0003-4843(75)90004-2"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Gasquet, O., Herzig, A., Longin, D., Sahade, M.: LoTREC: Logical tableaux research engineering companion. In: TABLEAUX 2005. LNCS, vol. 3702, pp. 318\u2013322. Springer (2005). https:\/\/doi.org\/10.1007\/11554554_25","DOI":"10.1007\/11554554_25"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y., Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and belief. Artif. Intell. 54(3), 319\u2013379 (1992)","DOI":"10.1016\/0004-3702(92)90049-4"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Heuerding, A., J\u00e4ger, G., Schwendimann, S., Seyfried, M.: The Logics Workbench LWB: A snapshot. Euromath Bulletin 2(1), 177\u2013186 (1996)","DOI":"10.3233\/AIC-1996-9203"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Horrocks, I., Hustadt, U., Sattler, U., Schmidt, R.A.: Computational modal logic. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, chap. 4, pp. 181\u2013245. Elsevier (2006)","DOI":"10.1016\/S1570-2464(07)80007-3"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Kracht, M.: Reducing modal consequence relations. J. Log. Comput. 11(6), 879\u2013907 (2001)","DOI":"10.1093\/logcom\/11.6.879"},{"key":"5_CR12","unstructured":"Kracht, M.: Notes on the space requirements for checking satisfiability in modal logics. In: Advances in Modal Logic 4, pp. 243\u2013264. King\u2019s College Publications (2003)"},{"key":"5_CR13","unstructured":"Nalon, C.: KSB (2021), https:\/\/cic.unb.br\/~nalon\/#software"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Nalon, C., Dixon, C.: Clausal resolution for normal modal logics. J. Algorithms 62, 117\u2013134 (2007)","DOI":"10.1016\/j.jalgor.2007.04.001"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Nalon, C., Dixon, C., Hustadt, U.: Modal resolution: Proofs, layers, and refinements. ACM Trans. Comput. Log. 20(4), 23:1\u201323:38 (2019)","DOI":"10.1145\/3331448"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Nalon, C., Hustadt, U., Dixon, C.: A modal-layered resolution calculus for K. In: TABLEAUX 2015. LNCS, vol. 9323, pp. 185\u2013200. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-319-24312-2_13","DOI":"10.1007\/978-3-319-24312-2_13"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Nalon, C., Hustadt, U., Dixon, C.: KSP: A resolution-based prover for multimodal K. In: IJCAR 2016. LNCS, vol. 9706, pp. 406\u2013415. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_28","DOI":"10.1007\/978-3-319-40229-1_28"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Nalon, C., Hustadt, U., Dixon, C.: KSP: Architecture, refinements,strategies and experiments. J. Autom. Reason. 64(3), 461\u2013484(2020)","DOI":"10.1007\/s10817-018-09503-x"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Nguyen, L.A., Szalas, A.: Exptime tableau decision procedures for regular grammar logics with converse. Studia Logica 98(3), 387\u2013428 (2011)","DOI":"10.1007\/s11225-011-9341-3"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Ohlbach, H.J., Nonnengart, A., de Rijke, M., Gabbay, D.M.: Encoding two-valued nonclassical logics in classical logic. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, chap. 21, pp. 1403\u20131485. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50023-0"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Otten, J.: MleanCoP: A connection prover for first-order modal logic. In: IJCAR 2014. LNCS, vol. 8562, pp. 269\u2013276. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_20","DOI":"10.1007\/978-3-319-08587-6_20"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Pan, G., Sattler, U., Vardi, M.Y.: BDD-based decision procedures for the modal logic K. J. Appl. Non-Class. Log. 16(1\u20132), 169\u2013208 (2006)","DOI":"10.3166\/jancl.16.169-207"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Schmidt, R.A.: Decidability by resolution for propositional modal logics. J. Autom. Reasoning 22(4), 379\u2013396 (1999)","DOI":"10.1023\/A:1006043519663"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Schmidt, R.A., Hustadt, U.: The axiomatic translation principle for modal logic. ACM Trans. Comput. Log. 8(4), 19 (2007)","DOI":"10.1145\/1276920.1276921"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Schmidt, R.A., Hustadt, U.: First-order resolution methods for modal logics. In: Programming Logics: Essays in Memory of Harald Ganzinger. LNCS, vol. 7797, pp. 345\u2013391. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-37651-1_15","DOI":"10.1007\/978-3-642-37651-1_15"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Steen, A., Benzm\u00fcller, C.: The higher-order prover Leo-III. In: ECAI 2020. Frontiers in Artificial Intelligence and Applications, vol. 325, pp. 2937\u20132938. IOS Press (2020). https:\/\/doi.org\/10.3233\/FAIA200462","DOI":"10.3233\/FAIA200462"},{"key":"5_CR27","unstructured":"The SPASS Team: Spass 3.9 (2016), http:\/\/www.spass-prover.org\/"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1965\u20132013. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50029-1"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:37Z","timestamp":1625649637000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","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":"76","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":"29","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":"0","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":"38% - 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":"5","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)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}