{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,17]],"date-time":"2026-02-17T12:49:49Z","timestamp":1771332589113,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540644064","type":"print"},{"value":"9783540697787","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-69778-0_13","type":"book-chapter","created":{"date-parts":[[2007,8,4]],"date-time":"2007-08-04T09:02:30Z","timestamp":1186218150000},"page":"44-59","source":"Crossref","is-referenced-by-count":14,"title":["A Tableau Calculus for Multimodal Logics and Some (Un)Decidability Results"],"prefix":"10.1007","author":[{"given":"Matteo","family":"Baldoni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laura","family":"Giordano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Martelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,7,21]]},"reference":[{"issue":"3","key":"13_CR1","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1093\/logcom\/2.3.247","volume":"2","author":"Y. Auffray","year":"1992","unstructured":"Y. Auffray and P. Enjalbert. Modal Theorem Proving: An equational viewpoint. Journal of Logic and Computation, 2(3):247\u2013297, 1992.","journal-title":"Journal of Logic and Computation"},{"key":"13_CR2","unstructured":"M. Baldoni. Normal Multimodal Logics: Automatic Deduction and Logic Programming Extension. PhD thesis, Dipartimento di Informatica, Universit\u00e0 degli Studi di Torino, 1998."},{"key":"13_CR3","unstructured":"M. Baldoni, L. Giordano, and A. Martelli. A Multimodal Logic to define Modules in Logic Programming. In Proc. of ILPS\u201993, pages 473\u2013487. The MIT Press, 1993."},{"key":"13_CR4","unstructured":"M. Baldoni, L. Giordano, and A. Martelli. A Framework for Modal Logic Programming. In Proc. of the JICSLP\u201996, pages 52\u201366. The MIT Press, 1996."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"B. Beckert and R. Gor\u00e9. Free Variable Tableaux for Propositional Modal Logics. In Proc. of TABLEAUX\u201997, volume 1227 of LNAI, pages 91\u2013106. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0027407"},{"issue":"1\u20132","key":"13_CR6","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0747-7171(87)80021-4","volume":"3","author":"R. V. Book","year":"1987","unstructured":"R. V. Book. Thue Systems as Rewriting Systems. Journal of Symbolic Computation, 3(1\u20132):39\u201368, 1987.","journal-title":"Journal of Symbolic Computation"},{"key":"13_CR7","unstructured":"L. Catach. Normal Multimodal Logics. In Proc. of the AAAI\u2019 88, pages 491\u2013495. Morgan Kaufmann, 1988."},{"issue":"4","key":"13_CR8","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/BF01880326","volume":"7","author":"L. Catach","year":"1991","unstructured":"L. Catach. TABLEAUX: A General Theorem Prover for Modal Logics. Journal of Automated Reasoning, 7(4):489\u2013510, 1991.","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"G. De Giacomo and F. Massacci. Tableaux and Algorithms for Propositional Dynamic Logic with Converse. In Proc. of CADE-15, volume 1249 of LNAI, pages 613\u2013627. Springer, 1996.","DOI":"10.1007\/3-540-61511-3_117"},{"issue":"1","key":"13_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(89)90137-0","volume":"65","author":"P. Enjalbert","year":"1989","unstructured":"P. Enjalbert and L. Fari\u00f1as del Cerro. Modal Resolution in Clausal Form. Theoretical Computer Science, 65(1):1\u201333, 1989","journal-title":"Theoretical Computer Science"},{"key":"13_CR11","unstructured":"L. Fari\u00f1as del Cerro and M. Penttonen. Grammar Logics. Logique et Analyse, 121\u2013122:123\u2013134, 1988."},{"issue":"2","key":"13_CR12","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. J. Fischer","year":"1979","unstructured":"M. J. Fischer and R. E. Ladner. Propositional Dynamic Logic of Regular Programs. Journal of Computer and System Sciences, 18(2):194\u2013211, 1979.","journal-title":"Journal of Computer and System Sciences"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"M. Fisher and R. Owens. An Introduction to Executable Modal and Temporal Logics. In Proc. of the IJCAI\u201993 Workshop on Executable Modal and Temporal Logics, volume 897 of LNAI, pages 1\u201320. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-58976-7_1"},{"key":"13_CR14","series-title":"Synthese library","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logics","author":"M. Fitting","year":"1983","unstructured":"M. Fitting. Proof Methods for Modal and Intuitionistic Logics, volume 169 of Synthese library. D. Reidel, Dordrecht, Holland, 1983."},{"key":"13_CR15","unstructured":"O. Gasquet. Optimization of deduction for multi-modal logics. In Applied Logic: How, What and Why? Kluwer Academic Publishers, 1993."},{"key":"13_CR16","unstructured":"M. Genesereth and N. Nilsson. Logical Foundations of Artificial Intelligence. Morgan Kaufmann, 1987."},{"key":"13_CR17","unstructured":"R. A. Gor\u00e9. Tableaux Methods for Modal and Temporal Logics. Technical Report TR-ARP-16-95, Automated Reasoning Project, Australian Nat. Univ., 1995."},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"G. Governatori. Labelled Tableaux for Multi-Modal Logics. In Proc. of TABLEAUX\u2019 95, volume 918 of LNAI, pages 79\u201394. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-59338-1_29"},{"key":"13_CR19","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","volume":"54","author":"J. Y. Halpern","year":"1992","unstructured":"J. Y. Halpern and Y. Moses. A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief. Artificial Intelligence, 54:319\u2013379, 1992.","journal-title":"Artificial Intelligence"},{"key":"13_CR20","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1016\/0022-0000(83)90014-4","volume":"26","author":"D. Harel","year":"1983","unstructured":"D. Harel, A. Pnueli, and J. Stavi. Propositional Dynamic Logic of Nonregular Programs. Journal of Computer and System Sciences, 26:222\u2013243, 1983.","journal-title":"Journal of Computer and System Sciences"},{"key":"13_CR21","unstructured":"J. E. Hopcroft and J. D. Ullman. Introduction to automata theory, languages, and computation. Addison-Wesley Publishing Company, 1979."},{"key":"13_CR22","unstructured":"G. E. Hughes and M. J. Cresswell. A Companion to Modal Logic. Meuthuen, 1984."},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"G. E. Hughes and M. J. Cresswell. A New Introduciton to Modal Logic. Routledge, 1996.","DOI":"10.4324\/9780203290644"},{"issue":"1","key":"13_CR24","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1093\/logcom\/5.1.93","volume":"5","author":"M. Kracth","year":"1995","unstructured":"M. Kracth. Highway to the Danger Zone. Journal of Logic and Computation, 5(1):93\u2013109, 1995.","journal-title":"Journal of Logic and Computation"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"F. Massacci. Strongly Analytic Tableaux for Normal Modal Logics. In Proc. of the CADE\u201994, volume 814 of LNAI, pages 723\u2013737. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_52"},{"key":"13_CR26","unstructured":"A. Nerode. Some Lectures on Modal Logic. In F. L. Bauer, editor, Logic, Algebra, and Computation, volume 79 of NATO ASI Series. Springer-Verlag, 1989."},{"key":"13_CR27","unstructured":"A. Nonnengart. First-Order Modal Logic Theorem Proving and Functional Simulation. In Proc. of IJCAI\u201993, pages 80\u201385, 1993."},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"H. J. Ohlbach. Optimized Translation of Multi Modal Logic into Predicate Logic. In Proc. of the Logic Programming and Automated Reasoning, volume 822 of LNAI, pages 253\u2013264. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56944-8_58"},{"issue":"1","key":"13_CR29","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1093\/jigpal\/1.1.69","volume":"1","author":"H. J. Ohlbach","year":"1993","unstructured":"H. J. Ohlbach. Translation methods for non-classical logics: An overview. Bull. of the IGPL, 1(1):69\u201389, 1993.","journal-title":"Bull. of the IGPL"},{"issue":"5","key":"13_CR30","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1093\/logcom\/1.5.691","volume":"1","author":"H.J. Ohlbach","year":"1991","unstructured":"H.J. Ohlbach. Semantics-Based Translation Methods for Modal Logics. Journal of Logic and Computation, 1(5):691\u2013746, 1991.","journal-title":"Journal of Logic and Computation"},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"M.A. Orgun and W. Ma. An overview of temporal and modal logic programming. In Proc. of the First International Conference on Temporal Logic, volume 827 of LNAI, pages 445\u2013479. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0014004"},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"J. Pitt and J. Cunningham. Distributed Modal Theorem Proving with KE. In Proc. of the TABLEAUX\u201996, volume 1071 of LNAI, pages 160\u2013176. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61208-4_11"},{"key":"13_CR33","doi-asserted-by":"crossref","unstructured":"M. Wooldridge and N. R. Jennings. Agent Theories, Architectures, and Languages: A survey. In Proc. of the ECAI-94 Workshop on Agent Theories, volume 890 of LNAI, pages 1\u201339. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-58855-8_1"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-69778-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:07:34Z","timestamp":1556737654000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-69778-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540644064","9783540697787"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-69778-0_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1998]]}}}