{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:05:21Z","timestamp":1759017921092,"version":"3.44.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032060846","type":"print"},{"value":"9783032060853","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We extend the mono-modal CEGAR-tableaux of Gor\u00e9 and Kikkert to normal multi-modal logic <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textrm{K}_{\\textrm{n}}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mtext>K<\/mml:mtext>\n                    <mml:mtext>n<\/mml:mtext>\n                  <\/mml:msub>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> \u00a0with global assumptions. We then extend these CEGAR-tableaux to multi-modal tense logic <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textrm{Kt}_{\\textrm{n}}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mtext>Kt<\/mml:mtext>\n                    <mml:mtext>n<\/mml:mtext>\n                  <\/mml:msub>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> without global assumptions by \u201ccompiling in\u201d the residuation conditions between \u201cfuture\u201d and \u201cpast\u201d modalities. Our new implementation  uses <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mathrm {C^{++}}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msup>\n                    <mml:mi>C<\/mml:mi>\n                    <mml:mrow>\n                      <mml:mo>+<\/mml:mo>\n                      <mml:mo>+<\/mml:mo>\n                    <\/mml:mrow>\n                  <\/mml:msup>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> and includes multiple optimisations which speed up proof-search. <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\texttt {CEGARBox++}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>CEGARBox<\/mml:mi>\n                    <mml:mo>+<\/mml:mo>\n                    <mml:mo>+<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> is the\u00a0best satisfiability-checker for mono-modal tense logic <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textrm{Kt}_{\\textrm{1}}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mtext>Kt<\/mml:mtext>\n                    <mml:mtext>1<\/mml:mtext>\n                  <\/mml:msub>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> but is not competitive for global assumptions.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_13","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:17Z","timestamp":1758969917000},"page":"238-257","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Improved Decision Procedures for\u00a0Multi-modal Tense Logic Using CEGAR-Tableaux"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Gor\u00e9","sequence":"first","affiliation":[]},{"given":"Cormac","family":"Kikkert","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F., Horrocks, I., Sattler, U.: Description logics. In: van Harmelen, F., Lifschitz, V., Porter, B.W. (eds.) Handbook of Knowledge Representation. Foundations of Artificial Intelligence, vol. 3, pp. 135\u2013179. Elsevier (2008)","DOI":"10.1016\/S1574-6526(07)03003-9"},{"issue":"3","key":"13_CR2","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1023\/A:1006249507577","volume":"24","author":"P Balsiger","year":"2000","unstructured":"Balsiger, P., Heuerding, A., Schwendimann, S.: A benchmark method for the propositional modal logics K, KT, S4. J. Autom. Reason. 24(3), 297\u2013317 (2000)","journal-title":"J. Autom. Reason."},{"key":"13_CR3","unstructured":"Calvanese, D., De Giacomo, G., Rosati, R.: A note on encoding inverse roles and functional restrictions in ALC knowledge bases. In: Franconi, E., De Giacomo, G., MacGregor, R.M., Nutt, W., Welty, C.A. (eds.) Proceedings of the 1998 International Workshop on Description Logics (DL 1998), IRST, Povo - Trento, Italy, 6\u20138 June 1998. CEUR Workshop Proceedings, vol. 11. CEUR-WS.org (1998)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1007\/978-3-662-48899-7_43","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K Claessen","year":"2015","unstructured":"Claessen, K., Ros\u00e9n, D.: SAT modulo intuitionistic implications. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 622\u2013637. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_43"},{"issue":"5","key":"13_CR5","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Yuan, L., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"13_CR6","unstructured":"Een, N., S\u00f6rensson, N.: http:\/\/minisat.se\/Papers.html. Accessed 10 Feb 2020"},{"key":"13_CR7","unstructured":"Geatti, L., Gigante, N., Montanari, A.: BLACK: a fast, flexible and reliable LTL satisfiability checker. In: Monica, D.D., Pozzato, G.L., Scala, E. (eds.) Proceedings of the 3rd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis hosted by the Twelfth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2021), Padua, Italy, 22 September 2021. CEUR Workshop Proceedings, vol. 2987, pp. 7\u201312. CEUR-WS.org (2021)"},{"issue":"2","key":"13_CR8","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF00173700","volume":"5","author":"G Giacomo","year":"1996","unstructured":"Giacomo, G.: Eliminating \u201cconverse\u2019\u2019 from converse PDL. J. Logic Lang. Inform. 5(2), 193\u2013208 (1996)","journal-title":"J. Logic Lang. Inform."},{"key":"13_CR9","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"},{"issue":"1","key":"13_CR10","doi-asserted-by":"publisher","first-page":"21","DOI":"10.3233\/FI-2009-115","volume":"94","author":"R Gor\u00e9","year":"2009","unstructured":"Gor\u00e9, R., Nguyen, L.A.: Clausal tableaux for multimodal logics of belief. Fundam. Inform. 94(1), 21\u201340 (2009)","journal-title":"Fundam. Inform."},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-38574-2_19","volume-title":"Automated Deduction \u2013 CADE-24","author":"R Gor\u00e9","year":"2013","unstructured":"Gor\u00e9, R., Thomson, J.: An improved BDD method for intuitionistic propositional logic: BDDIntKt system description. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 275\u2013281. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_19"},{"issue":"4","key":"13_CR12","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/BF00284976","volume":"11","author":"ND Belnap Jr","year":"1982","unstructured":"Belnap Jr, N.D.: Display logic. J. Philos. Log. 11(4), 375\u2013417 (1982)","journal-title":"J. Philos. Log."},{"issue":"1","key":"13_CR13","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. Log. 53(1), 119\u2013136 (1994)","journal-title":"Stud. Log."},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-319-26287-1_13","volume-title":"Hardware and Software: Verification and Testing","author":"J Li","year":"2015","unstructured":"Li, J., Zhu, S., Pu, G., Vardi, M.Y.: SAT-based explicit LTL reasoning. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 209\u2013224. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-26287-1_13"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Mints, G. (1990). Gentzen-type systems and resolution rules part I propositional logic. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG-88. LNCS, vol. 417, pp. 198\u2013231. Springer, Heidelberg (1988). https:\/\/doi.org\/10.1007\/3-540-52335-9_55","DOI":"10.1007\/3-540-52335-9_55"},{"key":"13_CR16","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 Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, 19\u201325 August 2017, pp. 4919\u20134923. ijcai.org (2017)","DOI":"10.24963\/ijcai.2017\/694"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1007\/978-3-031-10769-6_29","volume-title":"Automated Reasoning","author":"C Nalon","year":"2022","unstructured":"Nalon, C., Hustadt, U., Papacchini, F., Dixon, C.: Local reductions for the modal cube. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 486\u2013505. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_29"},{"key":"13_CR18","unstructured":"Pagram, T.: Using decision diagrams for modal and intuitionistic theorem proving. Honours thesis, Research School of Computer Science, The Australian National University (2015). https:\/\/github.com\/tpagram"},{"key":"13_CR19","unstructured":"Prior, A.N.: Time and Modality. Oxford University Press (1957)"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Tseytin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part II. Seminars in Mathematics, pp. 115\u2013125. Steklov Mathematical Institute (1970)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-540-92701-3_7","volume-title":"Logic and Its Applications","author":"MY Vardi","year":"2008","unstructured":"Vardi, M.Y.: From philosophical to industrial logics. In: Ramanujam, R., Sarukkai, S. (eds.) ICLA 2009. LNCS (LNAI), vol. 5378, pp. 89\u2013115. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-92701-3_7"},{"key":"13_CR22","unstructured":"Wu, M., Gor\u00e9, R.: Verified decision procedures for modal logics. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019, 9\u201312 September 2019, Portland, OR, USA. LIPIcs, vol. 141, pp. 31:1\u201331:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"}],"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-032-06085-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:19Z","timestamp":1758969919000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032060846","9783032060853"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06085-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,25]]},"assertion":[{"value":"25 September 2025","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":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/tableaux\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}