{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T07:25:25Z","timestamp":1725607525126},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642239342"},{"type":"electronic","value":"9783642239359"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-23935-9_56","type":"book-chapter","created":{"date-parts":[[2011,9,12]],"date-time":"2011-09-12T11:31:55Z","timestamp":1315827115000},"page":"572-581","source":"Crossref","is-referenced-by-count":3,"title":["A Cut-Free ExpTime Tableau Decision Procedure for the Description Logic SHI"],"prefix":"10.1007","author":[{"given":"Linh Anh","family":"Nguyen","sequence":"first","affiliation":[]}],"member":"297","reference":[{"volume-title":"Description Logic Handbook","year":"2002","key":"56_CR1","unstructured":"Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): Description Logic Handbook. Cambridge University Press, Cambridge (2002)"},{"volume-title":"Handbook of Tableau Methods","year":"1999","key":"56_CR2","unstructured":"D\u2019Agostino, M., Gabbay, D.M., H\u00e4hnle, R., Posegga, J. (eds.): Handbook of Tableau Methods. Springer, Heidelberg (1999)"},{"key":"56_CR3","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.P. Gor\u00e9","year":"2007","unstructured":"Gor\u00e9, R.P., 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)"},{"key":"56_CR4","series-title":"Lecture Notes in Computer Science","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 ALC with inverse roles. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol.\u00a05607, pp. 205\u2013219. Springer, Heidelberg (2009)"},{"key":"56_CR5","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.\u00a06173, pp. 225\u2013239. Springer, Heidelberg (2010)"},{"key":"56_CR6","first-page":"57","volume-title":"Proceedings of KR 2006","author":"I. Horrocks","year":"2006","unstructured":"Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible $\\mathcal{SROIQ}$ . In: Doherty, P., Mylopoulos, J., Welty, C.A. (eds.) Proceedings of KR 2006, pp. 57\u201367. AAAI Press, Menlo Park (2006)"},{"issue":"3","key":"56_CR7","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-3","key":"56_CR8","doi-asserted-by":"crossref","first-page":"273","DOI":"10.3233\/FI-2009-0102","volume":"93","author":"L.A. Nguyen","year":"2009","unstructured":"Nguyen, L.A.: An efficient tableau prover using global caching for the description logic $\\mathcal{ALC}$ . Fundamenta Informaticae\u00a093(1-3), 273\u2013288 (2009)","journal-title":"Fundamenta Informaticae"},{"key":"56_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-642-21916-0_50","volume-title":"Foundations of Intelligent Systems","author":"L.A. Nguyen","year":"2011","unstructured":"Nguyen, L.A.: Cut-free expTime tableaux for checking satisfiability of a\u00a0knowledge base in the description logic $\\mathcal{ALCI}$ . In: Kryszkiewicz, M., Rybinski, H., Skowron, A., Ra\u015b, Z.W. (eds.) ISMIS 2011. LNCS(LNAI), vol.\u00a06804, pp. 465\u2013475. Springer, Heidelberg (2011)"},{"key":"56_CR10","unstructured":"Nguyen, L.A.: The long version of the current paper (2011), http:\/\/arxiv.org\/abs\/1106.2305"},{"key":"56_CR11","doi-asserted-by":"crossref","unstructured":"Nguyen, L.A., Sza\u0142as, A.: ExpTime tableaux for checking satisfiability of a knowledge base in the description logic $\\mathcal{ALC}$ . In: Nguyen, N.T., Kowalczyk, R., Chen, S.-M. (eds.) ICCCI 2009. LNCS(LNAI), vol.\u00a05796, pp. 437\u2013448. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-04441-0_38"},{"issue":"1","key":"56_CR12","doi-asserted-by":"crossref","first-page":"97","DOI":"10.3233\/FI-2010-299","volume":"102","author":"L.A. Nguyen","year":"2010","unstructured":"Nguyen, L.A., Sza\u0142as, A.: Checking consistency of an ABox w.r.t. global assumptions in PDL. Fundamenta Informaticae\u00a0102(1), 97\u2013113 (2010)","journal-title":"Fundamenta Informaticae"},{"key":"56_CR13","first-page":"21","volume":"1","author":"L.A. Nguyen","year":"2010","unstructured":"Nguyen, L.A., Sza\u0142as, A.: Tableaux with global caching for checking satisfiability of a knowledge base in the description logic $\\mathcal{SH}$ . T. Computational Collective Intelligence\u00a01, 21\u201338 (2010)","journal-title":"T. Computational Collective Intelligence"},{"key":"56_CR14","doi-asserted-by":"crossref","unstructured":"Nguyen, L.A., Sza\u0142as, A.: ExpTime tableau decision procedures for regular grammar logics with converse. Studia Logica\u00a098(3) (2011)","DOI":"10.1007\/s11225-011-9341-3"}],"container-title":["Lecture Notes in Computer Science","Computational Collective Intelligence. Technologies and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23935-9_56","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,23]],"date-time":"2020-06-23T17:14:39Z","timestamp":1592932479000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23935-9_56"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642239342","9783642239359"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23935-9_56","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}