{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T06:31:45Z","timestamp":1761978705778,"version":"build-2065373602"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2013,10,24]],"date-time":"2013-10-24T00:00:00Z","timestamp":1382572800000},"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":[[2014,4]]},"DOI":"10.1007\/s10817-013-9294-5","type":"journal-article","created":{"date-parts":[[2013,10,23]],"date-time":"2013-10-23T04:36:43Z","timestamp":1382503003000},"page":"407-450","source":"Crossref","is-referenced-by-count":4,"title":["A Goal-Directed Decision Procedure for Hybrid PDL"],"prefix":"10.1007","volume":"52","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","published-online":{"date-parts":[[2013,10,24]]},"reference":[{"key":"9294_CR1","doi-asserted-by":"crossref","unstructured":"Abate, P., Gor\u00e9, R., Widmann, F.: An on-the-fly tableau-based decision procedure for PDL-satisfiability. In: Areces, C., Demri, S. (eds.) M4M-5, Electron. Notes Theor. Comput. Sci., vol. 231, pp. 191\u2013209. Elsevier (2009)","DOI":"10.1016\/j.entcs.2009.02.036"},{"issue":"2","key":"9294_CR2","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(95)00182-4","volume":"155","author":"V Antimirov","year":"1996","unstructured":"Antimirov, V.: Partial derivatives of regular expressions and finite automaton constructions. Theor. Comput. Sci. 155(2), 291\u2013319 (1996)","journal-title":"Theor. Comput. Sci."},{"key":"9294_CR3","doi-asserted-by":"crossref","unstructured":"Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3, pp. 821\u2013868. Elsevier (2007)","DOI":"10.1016\/S1570-2464(07)80017-6"},{"key":"9294_CR4","unstructured":"Baader, F.: Augmenting concept languages by transitive closure of roles: an alternative to terminological cycles. Tech. Rep. RR-90-13, DFKI (1990)"},{"issue":"3","key":"9294_CR5","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M Ben-Ari","year":"1983","unstructured":"Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Inform. 20(3), 207\u2013226 (1983)","journal-title":"Acta Inform."},{"key":"9294_CR6","doi-asserted-by":"crossref","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press (2001)","DOI":"10.1017\/CBO9781107050884"},{"issue":"3","key":"9294_CR7","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":"9294_CR8","doi-asserted-by":"crossref","unstructured":"Bonatti, P.A., Lutz, C., Murano, A., Vardi, M.Y.: The complexity of enriched \u03bc-calculi. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I., (eds.) ICALP 2006, Part II. LNCS, vol. 4052, pp. 540\u2013551. Springer (2006)","DOI":"10.1007\/11787006_46"},{"issue":"2","key":"9294_CR9","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1016\/j.jlap.2008.02.004","volume":"76","author":"K Br\u00fcnnler","year":"2008","unstructured":"Br\u00fcnnler, K., Lange, M.: Cut-free systems for temporal logic. J. Log. Algebr. Program. 76(2), 216\u2013225 (2008)","journal-title":"J. Log. Algebr. Program."},{"issue":"4","key":"9294_CR10","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"JA Brzozowski","year":"1964","unstructured":"Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481\u2013494 (1964)","journal-title":"J. ACM"},{"issue":"1\u20132","key":"9294_CR11","doi-asserted-by":"crossref","first-page":"39","DOI":"10.3166\/jancl.20.39-61","volume":"20","author":"S Cerrito","year":"2010","unstructured":"Cerrito, S., Cialdea Mayer, M.: An efficient approach to nominal equalities in hybrid logic tableaux. J. Appl. Non-Class. Log. 20(1\u20132), 39\u201361 (2010)","journal-title":"J. Appl. Non-Class. Log."},{"key":"9294_CR12","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol. 131, pp. 52\u201371. Springer (1982)","DOI":"10.1007\/BFb0025774"},{"issue":"1\u20132","key":"9294_CR13","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1006\/inco.1999.2852","volume":"162","author":"G Giacomo De","year":"2000","unstructured":"De Giacomo, G., Massacci, F.: Combining deduction and model checking into tableaux and algorithms for converse-PDL. Inf. Comput. 162(1\u20132), 117\u2013137 (2000)","journal-title":"Inf. Comput."},{"key":"9294_CR14","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, pp. 995\u20131072. Elsevier (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"1","key":"9294_CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"EA Emerson","year":"1985","unstructured":"Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30(1), 1\u201324 (1985)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"9294_CR16","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA 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 33(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"issue":"1","key":"9294_CR17","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1137\/S0097539793304741","volume":"29","author":"EA Emerson","year":"1999","unstructured":"Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM J. Comput. 29(1), 132\u2013158 (1999)","journal-title":"SIAM J. Comput."},{"issue":"3","key":"9294_CR18","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/S0019-9958(84)80047-9","volume":"61","author":"EA Emerson","year":"1984","unstructured":"Emerson, E.A., Sistla, A.P.: Deciding full branching time logic. Inf. Control 61(3), 175\u2013201 (1984)","journal-title":"Inf. Control"},{"issue":"2","key":"9294_CR19","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"MJ Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"9294_CR20","doi-asserted-by":"crossref","unstructured":"Gor\u00e9, R., Widmann, F.: An optimal on-the-fly tableau-based decision procedure for PDL-satisfiability. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 437\u2013452. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_32"},{"key":"9294_CR21","doi-asserted-by":"crossref","unstructured":"Gor\u00e9, R., Widmann, F.: Optimal tableaux for propositional dynamic logic with converse. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 225\u2013239. Springer (2010)","DOI":"10.1007\/978-3-642-14203-1_20"},{"key":"9294_CR22","doi-asserted-by":"crossref","unstructured":"G\u00f6tzmann, D., Kaminski, M., Smolka, G.: Spartacus: a tableau prover for hybrid logic. In: Bolander, T., Bra\u00fcner, T. (eds.) M4M-6. Electron. Notes Theor. Comput. Sci., vol. 262, pp. 127\u2013139. Elsevier (2010)","DOI":"10.1016\/j.entcs.2010.04.010"},{"key":"9294_CR23","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. The MIT Press (2000)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"9294_CR24","first-page":"7","volume":"8","author":"KJJ Hintikka","year":"1955","unstructured":"Hintikka, K.J.J.: Form and content in quantification theory. Two papers on symbolic logic. Acta Philos. Fenn. 8, 7\u201355 (1955)","journal-title":"Acta Philos. Fenn."},{"issue":"4","key":"9294_CR25","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1016\/j.jal.2010.08.003","volume":"8","author":"G Hoffmann","year":"2010","unstructured":"Hoffmann, G.: Lightweight hybrid tableaux. J. Appl. Log. 8(4), 397\u2013408 (2010)","journal-title":"J. Appl. Log."},{"key":"9294_CR26","doi-asserted-by":"crossref","unstructured":"Hoffmann, G., Areces, C.: HTab: a terminating tableaux system for hybrid logic. In: Areces, C., Demri, S. (eds.) M4M-5. Electron. Notes Theor. Comput. Sci., vol. 231, pp. 3\u201319. Elsevier (2009)","DOI":"10.1016\/j.entcs.2009.02.026"},{"key":"9294_CR27","doi-asserted-by":"crossref","unstructured":"Horrocks, I.: Implementation and optimization techniques. In: Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F., (eds.) The Description Logic Handbook: Theory, Implementation and Applications, 2nd edn., pp. 329\u2013373. Cambridge University Press (2007)","DOI":"10.1017\/CBO9780511711787.011"},{"key":"9294_CR28","unstructured":"Horrocks, I., Sattler, U.: Ontology reasoning in the SHOQ(D) description logic. In: Nebel, B. (ed.) IJCAI 2001, pp. 199\u2013204. Morgan Kaufmann (2001)"},{"issue":"3","key":"9294_CR29","doi-asserted-by":"crossref","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 SHOIQ. J. Autom. Reasoning 39(3), 249\u2013276 (2007)","journal-title":"J. Autom. Reasoning"},{"key":"9294_CR30","doi-asserted-by":"crossref","unstructured":"Jungteerapanich, N.: A tableau system for the modal \u03bc-calculus. In: Giese, M., Waaler, A., (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 220\u2013234. Springer (2009)","DOI":"10.1007\/978-3-642-02716-1_17"},{"key":"9294_CR31","unstructured":"Kaminski, M.: Incremental decision procedures for modal logics with nominals and eventualities. Ph.D. thesis, Saarland University (2012)"},{"key":"9294_CR32","doi-asserted-by":"crossref","unstructured":"Kaminski, M., Schneider, T., Smolka, G.: Correctness and worst-case optimality of Pratt-style decision procedures for modal and hybrid logics. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 196\u2013210. Springer (2011)","DOI":"10.1007\/978-3-642-22119-4_16"},{"issue":"4","key":"9294_CR33","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. Log. Lang. Inf. 18(4), 437\u2013464 (2009)","journal-title":"J. Log. Lang. Inf."},{"key":"9294_CR34","doi-asserted-by":"crossref","unstructured":"Kaminski, M., Smolka, G.: Terminating tableaux for hybrid logic with eventualities. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 240\u2013254. Springer (2010)","DOI":"10.1007\/978-3-642-14203-1_21"},{"key":"9294_CR35","doi-asserted-by":"crossref","unstructured":"Kaminski, M., Smolka, G.: Clausal tableaux for hybrid PDL. In: van Ditmarsch, H., Duque, D.F., Goranko, V., Jamroga, W., Ojeda-Aciego, M., (eds.) M4M-7. Electron. Notes Theor. Comput. Sci., vol. 278, pp. 99\u2013113. Elsevier (2011)","DOI":"10.1016\/j.entcs.2011.10.009"},{"issue":"4","key":"9294_CR36","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1016\/S0022-0000(69)80027-9","volume":"3","author":"DM Kaplan","year":"1969","unstructured":"Kaplan, D.M.: Regular expressions and the equivalence of programs. J. Comput. Syst. Sci. 3(4), 361\u2013386 (1969)","journal-title":"J. Comput. Syst. Sci."},{"key":"9294_CR37","unstructured":"Kowalski, R.: Logic for Problem Solving. North-Holland (1979)"},{"key":"9294_CR38","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"9294_CR39","doi-asserted-by":"crossref","unstructured":"Kozen, D., Smith, F.: Kleene algebra with tests: completeness and decidability. In: van Dalen, D., Bezem, M. (eds.) CSL\u201996. LNCS, vol. 1258, pp. 244\u2013259. Springer (1996)","DOI":"10.1007\/3-540-63172-0_43"},{"key":"9294_CR40","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"SA Kripke","year":"1963","unstructured":"Kripke, S.A.: Semantical analysis of modal logic I: normal modal propositional calculi. Z. Math. Log. Grundl. Math. 9, 67\u201396 (1963)","journal-title":"Z. Math. Log. Grundl. Math."},{"issue":"4","key":"9294_CR41","doi-asserted-by":"crossref","first-page":"1072","DOI":"10.2178\/jsl\/1129642115","volume":"70","author":"M Lange","year":"2005","unstructured":"Lange, M., Lutz, C.: 2-ExpTime lower bounds for propositional dynamic logic with intersection. J. Symb. Log. 70(4), 1072\u20131086 (2005)","journal-title":"J. Symb. Log."},{"key":"9294_CR42","unstructured":"Lemmon, E.J., Scott, D.: The \u2018Lemmon Notes\u2019: An Introduction to Modal Logic. Blackwell (1977)"},{"issue":"1","key":"9294_CR43","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1093\/jigpal\/8.1.55","volume":"8","author":"O Lichtenstein","year":"2000","unstructured":"Lichtenstein, O., Pnueli, A.: Propositional temporal logics: decidability and completeness. L. J. IGPL 8(1), 55\u201385 (2000)","journal-title":"L. J. IGPL"},{"issue":"1","key":"9294_CR44","doi-asserted-by":"crossref","first-page":"97","DOI":"10.3233\/FI-2010-299","volume":"102","author":"LA Nguyen","year":"2010","unstructured":"Nguyen, L.A., Sza\u0142as, A.: Checking consistency of an ABox w.r.t. global assumptions in PDL. Fundam. Inform. 102(1), 97\u2013113 (2010)","journal-title":"Fundam. Inform."},{"key":"9294_CR45","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS \u201977, pp. 46\u201357. IEEE Computer Society Press (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"9294_CR46","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Models of program logics. In: Proc. 20th Annual Symp. on Foundations of Computer Science (FOCS\u201979), pp. 115\u2013122. IEEE Computer Society Press (1979)","DOI":"10.1109\/SFCS.1979.24"},{"issue":"2","key":"9294_CR47","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0022-0000(80)90061-6","volume":"20","author":"VR Pratt","year":"1980","unstructured":"Pratt, V.R.: A near-optimal method for reasoning about action. J. Comput. Syst. Sci. 20(2), 231\u2013254 (1980)","journal-title":"J. Comput. Syst. Sci."},{"key":"9294_CR48","unstructured":"Reynolds, M.: A faster tableau for CTL*. In: Puppis, G., Villa, T., (eds.) GandALF 2013. Electron. Proc. Theor. Comput. Sci., vol. 119, pp. 50\u201363 (2013)"},{"key":"9294_CR49","doi-asserted-by":"crossref","unstructured":"Sattler, U., Vardi, M.Y.: The hybrid \u03bc-calculus. In: Gor\u00e9, R., Leitsch, A., Nipkow, T., (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 76\u201391. Springer (2001)","DOI":"10.1007\/3-540-45744-5_7"},{"key":"9294_CR50","doi-asserted-by":"crossref","unstructured":"Schmidt, R.A., Tishkovsky, D.: A general tableau method for deciding description logics, modal logics and related first-order fragments. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 194\u2013209. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_17"},{"issue":"2","key":"9294_CR51","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/j.websem.2007.03.004","volume":"5","author":"E Sirin","year":"2007","unstructured":"Sirin, E., Parsia, B., Grau, B.C., Kalyanpur, A., Katz, Y.: Pellet: a practical OWL-DL reasoner. J. Web Semant. 5(2), 51\u201353 (2007)","journal-title":"J. Web Semant."},{"key":"9294_CR52","doi-asserted-by":"crossref","unstructured":"Tsarkov, D., Horrocks, I.: FaCT+\u2009+ description logic reasoner: system description. In: Furbach, U., Shankar, N., (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 292\u2013297. Springer (2006)","DOI":"10.1007\/11814771_26"},{"issue":"3","key":"9294_CR53","doi-asserted-by":"crossref","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 39(3), 277\u2013316 (2007)","journal-title":"J. Autom. Reasoning"},{"key":"9294_CR54","unstructured":"Widmann, F.: Tableaux-based decision procedures for fixed point logics. Ph.D. thesis, Australian National University (2010)"},{"issue":"1\u20132","key":"9294_CR55","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1\u20132), 72\u201399 (1983)","journal-title":"Inf. Control"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9294-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9294-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9294-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T18:00:14Z","timestamp":1746036014000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9294-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,10,24]]},"references-count":55,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["9294"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9294-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2013,10,24]]}}}