{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T19:41:43Z","timestamp":1725910903791},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319677286"},{"type":"electronic","value":"9783319677293"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-67729-3_14","type":"book-chapter","created":{"date-parts":[[2017,9,16]],"date-time":"2017-09-16T05:04:04Z","timestamp":1505538244000},"page":"229-247","source":"Crossref","is-referenced-by-count":2,"title":["Tableaux with Partial Caching for Hybrid PDL with Satisfaction Statements"],"prefix":"10.1007","author":[{"given":"Agathoklis","family":"Kritsimallis","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,17]]},"reference":[{"issue":"5","key":"14_CR1","doi-asserted-by":"crossref","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. Logic J. IGPL 8(5), 653\u2013679 (2000)","journal-title":"Logic J. IGPL"},{"key":"14_CR2","doi-asserted-by":"crossref","first-page":"821","DOI":"10.1016\/S1570-2464(07)80017-6","volume-title":"Handbook of Modal Logic","author":"C Areces","year":"2007","unstructured":"Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Benthem, J.V., Wolter, F. (eds.) Handbook of Modal Logic, pp. 821\u2013868. Elsevier, Amsterdam (2007)"},{"issue":"3","key":"14_CR3","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. Logic Comput. 17(3), 517\u2013554 (2007)","journal-title":"J. Logic Comput."},{"key":"14_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-0002-4","volume-title":"Hybrid Logic and its Proof-Theory","author":"T Bra\u00fcner","year":"2011","unstructured":"Bra\u00fcner, T.: Hybrid Logic and its Proof-Theory. Springer, Heidelberg (2011). doi: 10.1007\/978-94-007-0002-4"},{"issue":"2","key":"14_CR5","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":"14_CR6","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1006\/inco.1999.2852","volume":"162","author":"GD Giacomo","year":"2000","unstructured":"Giacomo, G.D., Massacci, F.: Combining deduction and model checking into tableaux and algorithms for converse-PDL. Inf. Comput. 162, 117\u2013137 (2000)","journal-title":"Inf. Comput."},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-319-08587-6_3","volume-title":"Automated Reasoning","author":"R Gor\u00e9","year":"2014","unstructured":"Gor\u00e9, R.: And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 26\u201345. Springer, Cham (2014). doi: 10.1007\/978-3-319-08587-6_3"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-14203-1_5","volume-title":"Automated Reasoning","author":"R Gor\u00e9","year":"2010","unstructured":"Gor\u00e9, R., Kupke, C., Pattinson, D., Schr\u00f6der, L.: Global caching for coalgebraic description logics. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 46\u201360. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14203-1_5"},{"issue":"4","key":"14_CR9","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/s10817-011-9243-0","volume":"50","author":"R Gor\u00e9","year":"2013","unstructured":"Gor\u00e9, R., Nguyen, L.A.: Exptime tableaux for ALC using sound global caching. J. Autom. Reason. 50(4), 355\u2013381 (2013)","journal-title":"J. Autom. Reason."},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/978-3-642-02959-2_32","volume-title":"Automated Deduction \u2013 CADE-22","author":"R Gor\u00e9","year":"2009","unstructured":"Gor\u00e9, R., Widmann, F.: An optimal on-the-fly tableau-based decision procedure for PDL-satisfiability. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 437\u2013452. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02959-2_32"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-14203-1_20","volume-title":"Automated Reasoning","author":"R Gor\u00e9","year":"2010","unstructured":"Gor\u00e9, R., Widmann, F.: Optimal and cut-free tableaux for propositional dynamic logic with converse. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 225\u2013239. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14203-1_20"},{"key":"14_CR12","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. MIT Press, Cambridge (2000)"},{"issue":"4","key":"14_CR13","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":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-642-22119-4_16","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M Kaminski","year":"2011","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, Heidelberg (2011). doi: 10.1007\/978-3-642-22119-4_16"},{"issue":"4","key":"14_CR15","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/s10817-013-9294-5","volume":"52","author":"M Kaminski","year":"2014","unstructured":"Kaminski, M., Smolka, G.: A goal-directed decision procedure for hybrid PDL. J. Autom. Reason. 52(4), 407\u2013450 (2014)","journal-title":"J. Autom. Reason."},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Kritsimallis, A.: Tableaux with partial caching for hybrid PDL with satisfaction statements (ext. ver.) (2017). https:\/\/www.academia.edu\/32581641\/Tableaux_with_Partial_Caching_for_Hybrid_PDL_with_Satisfaction_Statements","DOI":"10.1007\/978-3-319-67729-3_14"},{"key":"14_CR17","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/j.neucom.2014.05.071","volume":"146","author":"LA Nguyen","year":"2014","unstructured":"Nguyen, L.A.: Exptime tableaux with global state caching for the description logic SHIO. Neurocomputing 146, 249\u2013263 (2014)","journal-title":"Neurocomputing"},{"issue":"4","key":"14_CR18","doi-asserted-by":"crossref","first-page":"433","DOI":"10.3233\/FI-2014-1133","volume":"135","author":"LA Nguyen","year":"2014","unstructured":"Nguyen, L.A., Goli\u0144ska-Pilarek, J.: An exptime tableau method for dealing with nominals and qualified number restrictions in deciding the description logic SHOQ. Fundamenta Informaticae 135(4), 433\u2013449 (2014)","journal-title":"Fundamenta Informaticae"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Nguyen, L.A., Sza\u0142as, A.: An optimal tableau decision procedure for converse-PDL. In: KSE 2009, pp. 207\u2013214. IEEE (2009)","DOI":"10.1109\/KSE.2009.12"},{"key":"14_CR20","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0020-0190(85)90127-9","volume":"20","author":"S Passy","year":"1985","unstructured":"Passy, S., Tinchev, T.: PDL with data constants. Inf. Process. Lett. 20, 35\u201341 (1985)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"14_CR21","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/0890-5401(91)90026-X","volume":"93","author":"S Passy","year":"1991","unstructured":"Passy, S., Tinchev, T.: An essay in combinatory dynamic logic. Inf. Comput. 93(2), 263\u2013332 (1991)","journal-title":"Inf. Comput."},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Models of program logics. In: Proceedings of 20th Symposium on Foundations of Computer Science, pp. 115\u2013122. IEEE (1979)","DOI":"10.1109\/SFCS.1979.24"},{"issue":"2","key":"14_CR23","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":"14_CR24","doi-asserted-by":"crossref","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001","volume-title":"Past, Present and Future","author":"A Prior","year":"1967","unstructured":"Prior, A.: Past, Present and Future. Oxford University Press, Oxford (1967)"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/3-540-48754-9_24","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M Tzakova","year":"1999","unstructured":"Tzakova, M.: Tableau calculi for hybrid logics. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS, vol. 1617, pp. 278\u2013292. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48754-9_24"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67729-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,17]],"date-time":"2020-10-17T19:44:30Z","timestamp":1602963870000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67729-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319677286","9783319677293"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67729-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}