{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:19:40Z","timestamp":1725567580276},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642162411"},{"type":"electronic","value":"9783642162428"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16242-8_30","type":"book-chapter","created":{"date-parts":[[2010,10,4]],"date-time":"2010-10-04T08:51:59Z","timestamp":1286182319000},"page":"417-431","source":"Crossref","is-referenced-by-count":2,"title":["Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference"],"prefix":"10.1007","author":[{"given":"Mark","family":"Kaminski","sequence":"first","affiliation":[]},{"given":"Gert","family":"Smolka","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"5","key":"30_CR1","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. IGPL\u00a08(5), 653\u2013679 (2000)","journal-title":"L. J. IGPL"},{"key":"30_CR2","doi-asserted-by":"crossref","unstructured":"Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, et al. (eds.) [4], pp. 821\u2013868","DOI":"10.1016\/S1570-2464(07)80017-6"},{"issue":"1","key":"30_CR3","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1093\/logcom\/10.1.137","volume":"10","author":"P. Blackburn","year":"2000","unstructured":"Blackburn, P.: Internalizing labelled deduction. J. Log. Comput.\u00a010(1), 137\u2013168 (2000)","journal-title":"J. Log. Comput."},{"volume-title":"Handbook of Modal Logic, Studies in Logic and Practical Reasoning","year":"2007","key":"30_CR4","unstructured":"Blackburn, P., van Benthem, J., Wolter, F. (eds.): Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol.\u00a03. Elsevier, Amsterdam (2007)"},{"key":"30_CR5","doi-asserted-by":"publisher","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)"},{"issue":"3","key":"30_CR6","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Programming\u00a02(3), 241\u2013266 (1982)","journal-title":"Sci. Comput. Programming"},{"issue":"1","key":"30_CR7","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: On branching versus linear time temporal logic. J. ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. System Sci. 194\u2013211 (1979)","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"30_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logics","author":"M. Fitting","year":"1983","unstructured":"Fitting, M.: Proof Methods for Modal and Intuitionistic Logics. Reidel, Dordrecht (1983)"},{"issue":"3","key":"30_CR10","first-page":"323","volume":"36","author":"D.M. Gabbay","year":"1970","unstructured":"Gabbay, D.M.: Selective filtration in modal logic, Part A. Semantic tableaux method. Theoria\u00a036(3), 323\u2013330 (1970)","journal-title":"Semantic tableaux method. Theoria"},{"key":"30_CR11","series-title":"LNAI","volume-title":"IJCAR 2010","year":"2010","unstructured":"Giesl, J., H\u00e4hnle, R. (eds.): IJCAR 2010. LNCS (LNAI), vol.\u00a06173. Springer, Heidelberg (2010)"},{"key":"30_CR12","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)"},{"issue":"1","key":"30_CR13","doi-asserted-by":"crossref","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. Fund. Inform.\u00a094(1), 21\u201340 (2009)","journal-title":"Fund. Inform."},{"key":"30_CR14","doi-asserted-by":"crossref","unstructured":"Gor\u00e9, R., Widmann, F.: Optimal tableaux for propositional dynamic logic with converse. In: Giesl, H\u00e4hnle (eds.) [11], pp. 225\u2013239","DOI":"10.1007\/978-3-642-14203-1_20"},{"key":"30_CR15","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. The MIT Press, Cambridge (2000)"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"Horrocks, I., Hustadt, U., Sattler, U., Schmidt, R.: Computational modal logic. In: Blackburn, et al. (eds.) [4], pp. 181\u2013245","DOI":"10.1016\/S1570-2464(07)80007-3"},{"key":"30_CR17","doi-asserted-by":"crossref","unstructured":"Kaminski, M., Smolka, G.: Clausal graph tableaux for hybrid logic with eventualities and difference. Technical report, Saarland University (2010), http:\/\/www.ps.uni-saarland.de\/Publications\/details\/KaminskiSmolka:2010:ClausalGraph.html","DOI":"10.1007\/978-3-642-16242-8_30"},{"key":"30_CR18","unstructured":"Kaminski, M., Smolka, G.: Clausal tableaux for hybrid PDL. Technical report, Saarland University (2010), http:\/\/www.ps.uni-saarland.de\/Publications\/details\/KaminskiSmolka:2010:HPDL.html"},{"key":"30_CR19","doi-asserted-by":"crossref","unstructured":"Kaminski, M., Smolka, G.: Terminating tableaux for hybrid logic with eventualities. In: Giesl, H\u00e4hnle (eds.) [11], pp. 240\u2013254","DOI":"10.1007\/978-3-642-14203-1_21"},{"key":"30_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-56922-7_9","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"1993","unstructured":"Kesten, Y., Manna, Z., McGuire, H., Pnueli, A.: A decision algorithm for full propositional temporal logic. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 97\u2013109. Springer, Heidelberg (1993)"},{"key":"30_CR21","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"S.A. Kripke","year":"1963","unstructured":"Kripke, S.A.: Semantical analysis of modal logic I: Normal modal propositional calculi. Z. Math. Logik Grundlagen Math.\u00a09, 67\u201396 (1963)","journal-title":"Z. Math. Logik Grundlagen Math."},{"key":"30_CR22","volume-title":"The \u2018Lemmon Notes\u2019: An Introduction to Modal Logic","author":"E.J. Lemmon","year":"1977","unstructured":"Lemmon, E.J., Scott, D.: The \u2018Lemmon Notes\u2019: An Introduction to Modal Logic. Blackwell, Malden (1977)"},{"issue":"1","key":"30_CR23","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z. Manna","year":"1984","unstructured":"Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM TOPLAS\u00a06(1), 68\u201393 (1984)","journal-title":"ACM TOPLAS"},{"issue":"3","key":"30_CR24","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1023\/A:1006155811656","volume":"24","author":"F. Massacci","year":"2000","unstructured":"Massacci, F.: Single step tableaux for modal logics. J. Autom. Reasoning\u00a024(3), 319\u2013364 (2000)","journal-title":"J. Autom. Reasoning"},{"key":"30_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/3-540-48340-3_29","volume-title":"Mathematical Foundations of Computer Science 1999","author":"L.A. Nguyen","year":"1999","unstructured":"Nguyen, L.A.: A new space bound for the modal logics K4, KD4 and S4. In: Kuty\u0142owski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol.\u00a01672, pp. 321\u2013331. Springer, Heidelberg (1999)"},{"key":"30_CR26","first-page":"46","volume-title":"Proc. 18th Annual Symp. on Foundations of Computer Science (FOCS 1977)","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th Annual Symp. on Foundations of Computer Science (FOCS 1977), pp. 46\u201357. IEEE Computer Society Press, Los Alamitos (1977)"},{"issue":"2","key":"30_CR27","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0022-0000(80)90061-6","volume":"20","author":"V.R. Pratt","year":"1980","unstructured":"Pratt, V.R.: A near-optimal method for reasoning about action. J. Comput. System Sci.\u00a020(2), 231\u2013254 (1980)","journal-title":"J. Comput. System Sci."},{"key":"30_CR28","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-45744-5_7","volume-title":"Automated Reasoning","author":"U. Sattler","year":"2001","unstructured":"Sattler, U., Vardi, M.Y.: The hybrid \u03bc-calculus. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 76\u201391. Springer, Heidelberg (2001)"},{"key":"30_CR29","unstructured":"Segerberg, K.: An Essay in Classical Modal Logic. No.\u00a013 in Filosofiska Studier. University of Uppsala (1971)"},{"key":"30_CR30","unstructured":"Tanabe, Y., Takahashi, K., Hagiya, M.: A decision procedure for alternation-free modal \u03bc-calculi. In: Areces, C., Goldblatt, R. (eds.) Advances in Modal Logic, vol.\u00a07, pp. 341\u2013362. College Publications (2008)"},{"issue":"3","key":"30_CR31","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s10817-007-9077-y","volume":"39","author":"D. Tsarkov","year":"2007","unstructured":"Tsarkov, D., Horrocks, I., Patel-Schneider, P.F.: Optimizing terminological reasoning for expressive description logics. J. Autom. Reasoning\u00a039(3), 277\u2013316 (2007)","journal-title":"J. Autom. Reasoning"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16242-8_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,12]],"date-time":"2020-06-12T06:18:04Z","timestamp":1591942684000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16242-8_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642162411","9783642162428"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16242-8_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}