{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:40:16Z","timestamp":1725518416986},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_18","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"210-225","source":"Crossref","is-referenced-by-count":5,"title":["Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse"],"prefix":"10.1007","author":[{"given":"Mark","family":"Kaminski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gert","family":"Smolka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","first-page":"190","volume-title":"Proc. 15th Intl. Joint Conf. on Artificial Intelligence (IJCAI 1997)","author":"P. Balbiani","year":"1997","unstructured":"Balbiani, P., Demri, S.: Prefixed tableaux systems for modal logics with enriched languages. In: Ralescu, A.L., Shanahan, J.G. (eds.) Proc. 15th Intl. Joint Conf. on Artificial Intelligence (IJCAI 1997), pp. 190\u2013195. Morgan Kaufmann, San Francisco (1997)"},{"key":"18_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"P. Blackburn","year":"2001","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2001)"},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BF01054038","volume":"22","author":"G. Gargov","year":"1993","unstructured":"Gargov, G., Goranko, V.: Modal logic with names. Journal of Philosophical Logic\u00a022, 607\u2013636 (1993)","journal-title":"Journal of Philosophical Logic"},{"key":"18_CR4","unstructured":"Areces, C., ten Cate, B.: Hybrid logics. In: [33]"},{"issue":"1","key":"18_CR5","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1305\/ndjfl\/1093635335","volume":"31","author":"V. Goranko","year":"1990","unstructured":"Goranko, V.: Modal definability in enriched languages. Notre Dame Journal of Formal Logic\u00a031(1), 81\u2013105 (1990)","journal-title":"Notre Dame Journal of Formal Logic"},{"issue":"2","key":"18_CR6","doi-asserted-by":"publisher","first-page":"566","DOI":"10.2307\/2275293","volume":"57","author":"M. Rijke de","year":"1992","unstructured":"de Rijke, M.: The modal logic of inequality. J. Symb. Log.\u00a057(2), 566\u2013584 (1992)","journal-title":"J. Symb. Log."},{"issue":"3","key":"18_CR7","doi-asserted-by":"publisher","first-page":"1003","DOI":"10.2307\/2275109","volume":"58","author":"Y. Venema","year":"1993","unstructured":"Venema, Y.: Derivation rules as anti-axioms in modal logic. J. Symb. Log.\u00a058(3), 1003\u20131034 (1993)","journal-title":"J. Symb. Log."},{"issue":"5","key":"18_CR8","doi-asserted-by":"publisher","first-page":"653","DOI":"10.1093\/jigpal\/8.5.653","volume":"8","author":"C. Areces","year":"2000","unstructured":"Areces, C., Blackburn, P., Marx, M.: The computational complexity of hybrid temporal logics. L. J. of the IGPL\u00a08(5), 653\u2013679 (2000)","journal-title":"L. J. of the IGPL"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Fitting, M.: Modal proof theory. In: [33]","DOI":"10.1016\/S1570-2464(07)80005-X"},{"key":"18_CR10","unstructured":"Kaminski, M., Smolka, G.: Hybrid tableaux for the difference modality. In: 5th Workshop on Methods for Modalities (M4M-5) (2007)"},{"key":"18_CR11","unstructured":"Hughes, G.E., Cresswell, M.J.: An Introduction to Modal Logic. Methuen (1968)"},{"key":"18_CR12","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","volume":"54","author":"J.Y. Halpern","year":"1992","unstructured":"Halpern, J.Y., Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and belief. Artif. Intell.\u00a054, 319\u2013379 (1992)","journal-title":"Artif. Intell."},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Horrocks, I., Hustadt, U., Sattler, U., Schmidt, R.: Computational modal logic. In: [33]","DOI":"10.1016\/S1570-2464(07)80007-3"},{"issue":"3","key":"18_CR14","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1093\/logcom\/exm014","volume":"17","author":"T. Bolander","year":"2007","unstructured":"Bolander, T., Blackburn, P.: Termination for hybrid tableaus. J. Log. Comput.\u00a017(3), 517\u2013554 (2007)","journal-title":"J. Log. Comput."},{"issue":"3","key":"18_CR15","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1093\/logcom\/9.3.385","volume":"9","author":"I. Horrocks","year":"1999","unstructured":"Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. J. Log. Comput.\u00a09(3), 385\u2013410 (1999)","journal-title":"J. Log. Comput."},{"issue":"3","key":"18_CR16","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1093\/jigpal\/8.3.239","volume":"8","author":"I. Horrocks","year":"2000","unstructured":"Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for very expressive description logics. L. J. of the IGPL\u00a08(3), 239\u2013263 (2000)","journal-title":"L. J. of the IGPL"},{"issue":"3","key":"18_CR17","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10817-007-9079-9","volume":"39","author":"I. Horrocks","year":"2007","unstructured":"Horrocks, I., Sattler, U.: A tableau decision procedure for $\\mathcal{SHOIQ}$ . J. Autom. Reasoning\u00a039(3), 249\u2013276 (2007)","journal-title":"J. Autom. Reasoning"},{"key":"18_CR18","first-page":"335","volume-title":"Proc. 2nd Intl. Conf. on Principles of Knowledge Representation and Reasoning (KR 1991)","author":"B. Hollunder","year":"1991","unstructured":"Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. In: Allen, J., Fikes, R., Sandewall, E. (eds.) Proc. 2nd Intl. Conf. on Principles of Knowledge Representation and Reasoning (KR 1991), pp. 335\u2013346. Morgan Kaufmann, San Francisco (1991)"},{"key":"18_CR19","unstructured":"Calvanese, D., De Giacomo, G., Rosati, R.: A note on encoding inverse roles and functional restrictions in $\\mathcal{ALC}$ knowledge bases. In: Franconi, E., De Giacomo, G., MacGregor, R.M., Nutt, W., Welty, C.A. (eds.) Proc. 1998 Intl. Workshop on Description Logics (DL 1998). CEUR Workshop Proceedings, vol.\u00a011, pp. 69\u201371 (1998)"},{"issue":"4","key":"18_CR20","doi-asserted-by":"publisher","first-page":"1719","DOI":"10.2307\/2586808","volume":"64","author":"E. Gr\u00e4del","year":"1999","unstructured":"Gr\u00e4del, E.: On the restraining power of guards. J. Symb. Log.\u00a064(4), 1719\u20131742 (1999)","journal-title":"J. Symb. Log."},{"key":"18_CR21","first-page":"295","volume-title":"Proc. 14th Annual IEEE Symposium on Logic in Computer Science (LICS 1999)","author":"H. Ganzinger","year":"1999","unstructured":"Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: Proc. 14th Annual IEEE Symposium on Logic in Computer Science (LICS 1999), pp. 295\u2013304. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"18_CR22","series-title":"Mathematics Studies","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-0208(08)70478-X","volume-title":"Intensional and Higher-Order Modal Logic. With Applications to Montague Semantics","author":"D. Gallin","year":"1975","unstructured":"Gallin, D.: Intensional and Higher-Order Modal Logic. With Applications to Montague Semantics. Mathematics Studies, vol.\u00a019. North-Holland, Amsterdam (1975)"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Gamut, L.T.F.: Logic, Language and Meaning. In: Intensional Logic and Logical Grammar, vol. 2. The University of Chicago Press (1991)","DOI":"10.7208\/chicago\/9780226791708.001.0001"},{"key":"18_CR24","volume-title":"Type-Logical Semantics. Language, Speech, and Communication","author":"B. Carpenter","year":"1997","unstructured":"Carpenter, B.: Type-Logical Semantics. Language, Speech, and Communication. The MIT Press, Cambridge (1997)"},{"issue":"6","key":"18_CR25","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.entcs.2006.11.023","volume":"174","author":"M. Hardt","year":"2007","unstructured":"Hardt, M., Smolka, G.: Higher-order syntax and saturation algorithms for hybrid logic. Electr. Notes Theor. Comput. Sci.\u00a0174(6), 15\u201327 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"18_CR26","unstructured":"Benzm\u00fcller, C.E., Paulson, L.C.: Exploring properties of normal multimodal logics in simple type theory with LEO-II. In: Benzm\u00fcller, C.E., Brown, C.E., Siekmann, J., Statman, R. (eds.) Festschrift in Honor of Peter B. Andrews on His 70th Birthday. Studies in Logic and the Foundations of Mathematics. IFCoLog (to appear)"},{"key":"18_CR27","unstructured":"Kaminski, M., Smolka, G.: A straightforward saturation-based decision procedure for hybrid logic. In: Intl. Workshop on Hybrid Logic 2007 (HyLo 2007) (2007)"},{"issue":"6","key":"18_CR28","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1093\/logcom\/exl008","volume":"16","author":"T. Bolander","year":"2006","unstructured":"Bolander, T., Bra\u00fcner, T.: Tableau-based decision procedures for hybrid logic. J. Log. Comput.\u00a016(6), 737\u2013763 (2006)","journal-title":"J. Log. Comput."},{"key":"18_CR29","series-title":"LNCS(LNAI)","doi-asserted-by":"crossref","first-page":"723","DOI":"10.1007\/3-540-58156-1_52","volume-title":"Automated Deduction - CADE-12","author":"F. Massacci","year":"1994","unstructured":"Massacci, F.: Strongly analytic tableaux for normal modal logics. In: Bundy, A. (ed.) CADE 1994. LNCS(LNAI), vol.\u00a0814, pp. 723\u2013737. Springer, Heidelberg (1994)"},{"issue":"1","key":"18_CR30","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0004-3702(00)00070-9","volume":"124","author":"F.M. Donini","year":"2000","unstructured":"Donini, F.M., Massacci, F.: Exptime tableaux for $\\mathcal{ALC}$ . Artif. Intell.\u00a0124(1), 87\u2013138 (2000)","journal-title":"Artif. Intell."},{"key":"18_CR31","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-540-73099-6_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Gor\u00e9","year":"2007","unstructured":"Gor\u00e9, R., Nguyen, L.A.: EXPTIME tableaux with global caching for description logics with transitive roles, inverse roles and role hierarchies. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS (LNAI), vol.\u00a04548, pp. 133\u2013148. Springer, Heidelberg (2007)"},{"key":"18_CR32","unstructured":"Spaan, E.: Complexity of Modal Logics. PhD thesis, ILLC, University of Amsterdam (1993)"},{"key":"18_CR33","series-title":"Studies in Logic and Practical Reasoning","volume-title":"Handbook of Modal Logic","year":"2006","unstructured":"Blackburn, P., van Benthem, J., Wolter, F. (eds.): Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol.\u00a03. Elsevier, Amsterdam (2006)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,15]],"date-time":"2021-09-15T18:44:36Z","timestamp":1631731476000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}