{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:18:25Z","timestamp":1725491905053},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730989"},{"type":"electronic","value":"9783540730996"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73099-6_12","type":"book-chapter","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T07:04:02Z","timestamp":1189753442000},"page":"133-148","source":"Crossref","is-referenced-by-count":23,"title":["EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Gor\u00e9","sequence":"first","affiliation":[]},{"given":"Linh Anh","family":"Nguyen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1013882326814","volume":"69","author":"F. Baader","year":"2001","unstructured":"Baader, F., Sattler, U.: An overview of tableau algorithms for description logics. Studia Logica\u00a069, 5\u201340 (2001)","journal-title":"Studia Logica"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., Massacci, F.: Combining deduction and model checking into tableaux and algorithms for Converse-PDL. Information and Computation, pp. 117\u2013137, pp. 87\u2013138 (2000)","DOI":"10.1006\/inco.1999.2852"},{"key":"12_CR3","unstructured":"Ding, Y., Haarslev, V.: Tableau caching for description logics with inverse and transitive roles. In: Proc. DL-2006: International Workshop on Description Logics, pp. 143\u2013149 (2006)"},{"key":"12_CR4","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 ALC. Artificial Intelligence\u00a0124, 87\u2013138 (2000)","journal-title":"Artificial Intelligence"},{"key":"12_CR5","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: Agostino, D. (ed.) Handbook of Tableau Methods, pp. 297\u2013396. Kluwer, Dordrecht (1999)"},{"key":"12_CR6","unstructured":"Gor\u00e9, R., Nguyen, L.A.: Optimised EXPTIME tableaux for ALC using sound global caching, propagation and cutoffs. Manuscript (2007)"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1007\/3-540-61208-4_14","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"A. Heuerding","year":"1996","unstructured":"Heuerding, A., Seyfried, M., Zimmermann, H.: Efficient loop-check for backward proof search in some non-classical logics. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol.\u00a01071, pp. 210\u2013225. Springer, Heidelberg (1996)"},{"issue":"3","key":"12_CR8","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.F.: Optimizing description logic subsumption. Journal of Logic and Computation\u00a09(3), 267\u2013293 (1999)","journal-title":"Journal of Logic and Computation"},{"issue":"3","key":"12_CR9","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1093\/logcom\/9.3.385","volume":"9","author":"I. Horrocks","year":"1999","unstructured":"Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. J. Log. Comput.\u00a09(3), 385\u2013410 (1999)","journal-title":"J. Log. Comput."},{"issue":"1","key":"12_CR10","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1023\/A:1013834410884","volume":"69","author":"L.A. Nguyen","year":"2001","unstructured":"Nguyen, L.A.: Analytic tableau systems and interpolation for the modal logics KB, KDB, K5, KD5. Studia Logica\u00a069(1), 41\u201357 (2001)","journal-title":"Studia Logica"},{"key":"12_CR11","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/BF00249258","volume":"12","author":"W. Rautenberg","year":"1983","unstructured":"Rautenberg, W.: Modal tableau calculi and interpolation. JPL\u00a012, 403\u2013423 (1983)","journal-title":"JPL"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73099-6_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:59:58Z","timestamp":1619517598000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73099-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730989","9783540730996"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73099-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}