{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T02:10:19Z","timestamp":1739931019764,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642120015"},{"type":"electronic","value":"9783642120022"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12002-2_9","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T01:20:25Z","timestamp":1268011225000},"page":"114-128","source":"Crossref","is-referenced-by-count":6,"title":["Optimal Tableau Algorithms for Coalgebraic Logics"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Gor\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clemens","family":"Kupke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dirk","family":"Pattinson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"volume-title":"The Description Logic Handbook: Theory, Implementation and Applications","year":"2003","key":"9_CR1","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.): The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, Cambridge (2003)"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Chellas, B.: Modal Logic, Cambridge (1980)","DOI":"10.1017\/CBO9780511621192"},{"key":"9_CR3","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.tcs.2004.07.021","volume":"327","author":"C. C\u00eerstea","year":"2004","unstructured":"C\u00eerstea, C.: A compositional approach to defining logics for coalgebras. Theoret. Comput. Sci.\u00a0327, 45\u201369 (2004)","journal-title":"Theoret. Comput. Sci."},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-04027-6_15","volume-title":"Computer Science Logic","author":"C. C\u00eerstea","year":"2009","unstructured":"C\u00eerstea, C., Kupke, C., Pattinson, D.: EXPTIME tableaux for the coalgebraic \u03bc- calculus. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol.\u00a05771, pp. 179\u2013193. Springer, Heidelberg (2009)"},{"key":"9_CR5","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/j.tcs.2007.06.002","volume":"388","author":"C. C\u00eerstea","year":"2007","unstructured":"C\u00eerstea, C., Pattinson, D.: Modular proof systems for coalgebraic logics. Theor. Comp. Sci.\u00a0388, 83\u2013108 (2007)","journal-title":"Theor. Comp. Sci."},{"issue":"1","key":"9_CR6","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0004-3702(00)00070-9","volume":"124","author":"F. Donini","year":"2000","unstructured":"Donini, F., Massacci, F.: Exptime tableaux for $\\mathcal{ALC}$ . Artif. Intell.\u00a0124(1), 87\u2013138 (2000)","journal-title":"Artif. Intell."},{"key":"9_CR7","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about Knowledge","author":"R. Fagin","year":"1995","unstructured":"Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning about Knowledge. The MIT Press, Cambridge (1995)"},{"key":"9_CR8","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1305\/ndjfl\/1093890715","volume":"13","author":"K. Fine","year":"1972","unstructured":"Fine, K.: In so many possible worlds. Notre Dame J. Formal Logic\u00a013, 516\u2013520 (1972)","journal-title":"Notre Dame J. Formal Logic"},{"key":"9_CR9","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/978-94-017-1754-0_6","volume-title":"Handbook of Tableau Methods","author":"R. Gor\u00e9","year":"1999","unstructured":"Gor\u00e9, R.: Tableau methods for modal and temporal logics. In: D\u2019Agostino, et al. (eds.) Handbook of Tableau Methods, pp. 297\u2013396. Kluwer, Dordrecht (1999)"},{"key":"9_CR10","unstructured":"Gor\u00e9, R., Nguyen, L.: EXPTIME tableaux for $\\mathcal{ALC}$ using sound global caching. In: Calvanese, D., Franconi, E., Haarslev, V., Lembo, D., Motik, B., Turhan, A., Tessaris, S. (eds.) Proc. Description Logics 2007. CEUR Workshop Proceedings. CEUR-WS.org, vol.\u00a0250 (2007)"},{"key":"9_CR11","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.: 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":"9_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-71070-7_25","volume-title":"Automated Reasoning","author":"R. Gor\u00e9","year":"2008","unstructured":"Gor\u00e9, R., Postniece, L.: An experimental evaluation of global caching for $\\mathcal{ALC}$ (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 299\u2013305. Springer, Heidelberg (2008)"},{"key":"9_CR13","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-642-02716-1_16","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Gor\u00e9","year":"2009","unstructured":"Gor\u00e9, R., Widmann, F.: Sound global state caching for $\\mathcal{ALC}$ with inverse roles. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol.\u00a05607, pp. 205\u2013219. Springer, Heidelberg (2009)"},{"key":"9_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/3-540-45744-5_59","volume-title":"Automated Reasoning","author":"V. Haarslev","year":"2001","unstructured":"Haarslev, V., M\u00f6ller, R.: RACER system description. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 701\u2013705. Springer, Heidelberg (2001)"},{"key":"9_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":"9_CR16","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1006\/game.1999.0788","volume":"35","author":"A. Heifetz","year":"2001","unstructured":"Heifetz, A., Mongin, P.: Probabilistic logic for type spaces. Games and Economic Behavior\u00a035, 31\u201353 (2001)","journal-title":"Games and Economic Behavior"},{"key":"9_CR17","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1093\/logcom\/9.3.267","volume":"9","author":"I. Horrocks","year":"1999","unstructured":"Horrocks, I., Patel-Schneider, P.: Optimising description logic subsumption. J. Logic Comput.\u00a09, 267\u2013293 (1999)","journal-title":"J. Logic Comput."},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-36387-4_2","volume-title":"Automata, Logics, and Infinite Games","author":"R. Mazala","year":"2002","unstructured":"Mazala, R.: Infinite games. In: Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol.\u00a02500, pp. 23\u201342. Springer, Heidelberg (2002)"},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0304-3975(03)00201-9","volume":"309","author":"D. Pattinson","year":"2003","unstructured":"Pattinson, D.: Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoret. Comput. Sci.\u00a0309, 177\u2013193 (2003)","journal-title":"Theoret. Comput. Sci."},{"issue":"5","key":"9_CR20","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/j.entcs.2008.05.027","volume":"203","author":"D. Pattinson","year":"2008","unstructured":"Pattinson, D., Schr\u00f6der, L.: Admissibility of cut in coalgebraic logics. Electr. Notes Theor. Comput. Sci.\u00a0203(5), 221\u2013241 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1","key":"9_CR21","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1093\/logcom\/12.1.149","volume":"12","author":"M. Pauly","year":"2002","unstructured":"Pauly, M.: A modal logic for coalitional power in games. J. Logic Comput.\u00a012(1), 149\u2013166 (2002)","journal-title":"J. Logic Comput."},{"issue":"1-2","key":"9_CR22","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.jlap.2006.11.004","volume":"73","author":"L. Schr\u00f6der","year":"2007","unstructured":"Schr\u00f6der, L.: A finite model construction for coalgebraic modal logic. J. Log. Algebr. Program.\u00a073(1-2), 97\u2013110 (2007)","journal-title":"J. Log. Algebr. Program."},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-540-73420-8_41","volume-title":"Automata, Languages and Programming","author":"L. Schr\u00f6der","year":"2007","unstructured":"Schr\u00f6der, L., Pattinson, D.: Compositional algorithms for heterogeneous modal logics. In: Arge, L., Cachin, C., Jurdzi\u0144ski, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol.\u00a04596, pp. 459\u2013471. Springer, Heidelberg (2007)"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Schr\u00f6der, L., Pattinson, D.: PSPACE bounds for rank-1 modal logics. ACM Transactions on Computational Logics\u00a010(2) (2009)","DOI":"10.1145\/1462179.1462185"},{"key":"9_CR25","unstructured":"Schr\u00f6der, L., Pattinson, D., Kupke, C.: Nominals for everyone. In: Boutilier, C. (ed.) Proc. IJCAI 2009, pp. 917\u2013922 (2009)"},{"key":"9_CR26","series-title":"Background: computational structures","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1093\/oso\/9780198537618.003.0005","volume-title":"Handbook of logic in computer science","author":"C. Stirling","year":"1992","unstructured":"Stirling, C.: Modal and temporal logics. In: Handbook of logic in computer science. Background: computational structures, vol.\u00a02, pp. 477\u2013563. Oxford University Press, Inc., Oxford (1992)"},{"key":"9_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/11814771_26","volume-title":"Automated Reasoning","author":"D. Tsarkov","year":"2006","unstructured":"Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 292\u2013297. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12002-2_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T01:38:52Z","timestamp":1739929132000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12002-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120015","9783642120022"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12002-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}