{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T01:40:04Z","timestamp":1744249204606,"version":"3.40.4"},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,10,6]],"date-time":"2012-10-06T00:00:00Z","timestamp":1349481600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,8]]},"DOI":"10.1007\/s10817-012-9257-2","type":"journal-article","created":{"date-parts":[[2012,10,5]],"date-time":"2012-10-05T17:51:55Z","timestamp":1349459515000},"page":"197-239","source":"Crossref","is-referenced-by-count":4,"title":["A Tableau Based Decision Procedure for an Expressive Fragment of Hybrid Logic with Binders, Converse and Global Modalities"],"prefix":"10.1007","volume":"51","author":[{"given":"Serenella","family":"Cerrito","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marta","family":"Cialdea Mayer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,10,6]]},"reference":[{"key":"9257_CR1","doi-asserted-by":"crossref","unstructured":"Areces, C., Blackburn, P., Marx, M.: A road-map on complexity for hybrid logics. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) Computer Science Logic of LNCS, vol. 1683, pp. 307\u2013321. Springer (1999)","DOI":"10.1007\/3-540-48168-0_22"},{"key":"9257_CR2","doi-asserted-by":"crossref","unstructured":"Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logics, pp. 821\u2013868. Elsevier (2007)","DOI":"10.1016\/S1570-2464(07)80017-6"},{"key":"9257_CR3","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/BF01049415","volume":"4","author":"P Blackburn","year":"1995","unstructured":"Blackburn, P., Seligman, J.: Hybrid languages. J. Logic, Lang. Inf. 4, 251\u2013272 (1995)","journal-title":"J. Logic, Lang. Inf."},{"issue":"3","key":"9257_CR4","doi-asserted-by":"crossref","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. 17(3), 517\u2013554 (2007)","journal-title":"J. Log. Comput."},{"key":"9257_CR5","unstructured":"Cerrito, S., Cialdea\u00a0Mayer, M.: Nominal substitution at work with the global and converse modalities. In: Beklemishev, L., Goranko, V., Shehtman, V. (eds.) Advances in Modal Logic, vol.\u00a08, pp.\u00a057\u201374. College Publications (2010)"},{"key":"9257_CR6","doi-asserted-by":"crossref","unstructured":"Cerrito, S., Cialdea Mayer, M.: A tableaux based decision procedure for a broad class of hybrid formulae with binders. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) Automated Resoning with Analytic Tableaux and Related Methods (TABLEAUX 2011) of LNAI, vol. 6793, pp. 104\u2013118. Springer (2011)","DOI":"10.1007\/978-3-642-22119-4_10"},{"key":"9257_CR7","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., De Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: Proc. 14th Symposium on Logic in Computer Science, pp. 295\u2013305. IEEE Computer Society Press (1999)","DOI":"10.1109\/LICS.1999.782624"},{"key":"9257_CR8","doi-asserted-by":"crossref","first-page":"1719","DOI":"10.2307\/2586808","volume":"64","author":"E Gr\u00e4del","year":"1998","unstructured":"Gr\u00e4del, E.: On the restraining power of guards. J. Symb. Log. 64, 1719\u20131742 (1998)","journal-title":"J. Symb. Log."},{"key":"9257_CR9","doi-asserted-by":"crossref","unstructured":"Hirsch, C., Tobies, S.: A tableau algorithm for the clique guarded fragment. In: Wolter, F., Wansing, H., de\u00a0Rijke, M., Zakharyaschev, M. (eds.) Advances in Modal Logic, vol. 3, pp. 257\u2013277. CSLI Publications (2001)","DOI":"10.1142\/9789812776471_0014"},{"key":"9257_CR10","doi-asserted-by":"crossref","unstructured":"Hladik, J.: Implementation and evaluation of a tableau algorithm for the guarded fragment. In: Egly, U., Ferm\u00fcller, C.G. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2002) of LNAI, vol. 2381, pp. 145\u2013159. Springer (2002)","DOI":"10.1007\/3-540-45616-3_11"},{"key":"9257_CR11","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2006.11.022","volume":"174","author":"I Horrocks","year":"2007","unstructured":"Horrocks, I., Glimm, B., Sattler, U.: Hybrid logics and ontology languages. Electron. Notes Theor. Comput. Sci. 174, 3\u201314 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"4","key":"9257_CR12","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/s10849-009-9087-8","volume":"18","author":"M Kaminski","year":"2009","unstructured":"Kaminski, M., Smolka, G.: Terminating tableau systems for hybrid logic with difference and converse. J. Logic, Lang. Inf. 18(4), 437\u2013464 (2009)","journal-title":"J. Logic, Lang. Inf."},{"key":"9257_CR13","unstructured":"Marx, M.: Narcissists, stepmothers and spies. In: Proceedings of International Workshop on Description Logics (DL 2002), vol. 53. CEUR (2002)"},{"key":"9257_CR14","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/s10849-005-5787-x","volume":"14","author":"B Cate ten","year":"2005","unstructured":"ten Cate, B., Franceschet, M.: Guarded fragments with constants. J. Logic, Lang. Inf. 14, 281\u2013288 (2005)","journal-title":"J. Logic, Lang. Inf."},{"key":"9257_CR15","doi-asserted-by":"crossref","unstructured":"ten Cate, B., Franceschet, M.: On the complexity of hybrid logics with binders. In: Ong, L. (ed.) Proceedings of Computer Science Logic 2005 of LNCS, vol. 3634, pp. 339\u2013354. Springer (2005)","DOI":"10.1007\/11538363_24"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9257-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-012-9257-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9257-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T01:00:04Z","timestamp":1744246804000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9257-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,6]]},"references-count":15,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["9257"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9257-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2012,10,6]]}}}