{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T03:31:08Z","timestamp":1725593468234},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642219153"},{"type":"electronic","value":"9783642219160"}],"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-21916-0_50","type":"book-chapter","created":{"date-parts":[[2011,6,25]],"date-time":"2011-06-25T15:16:37Z","timestamp":1309014997000},"page":"465-475","source":"Crossref","is-referenced-by-count":3,"title":["Cut-Free ExpTime Tableaux for Checking Satisfiability of a\u00a0Knowledge Base in the Description Logic $\\mathcal{ALCI}$"],"prefix":"10.1007","author":[{"given":"Linh Anh","family":"Nguyen","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"50_CR1","unstructured":"Ding, Y., Haarslev, V., Wu, J.: A new mapping from $\\mathcal{ALCI}$ to $\\mathcal{ALC}$ . In: Proceedings of Description Logics (2007)"},{"key":"50_CR2","first-page":"316","volume-title":"Proceedings of KR 1996","author":"G. Giacomo De","year":"1996","unstructured":"De Giacomo, G., Lenzerini, M.: TBox and ABox reasoning in expressive description logics. In: Aiello, L.C., Doyle, J., Shapiro, S.C. (eds.) Proceedings of KR 1996, pp. 316\u2013327. Morgan Kaufmann, San Francisco (1996)"},{"key":"50_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":"50_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":"50_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":"50_CR6","unstructured":"Horrocks, I., Sattler, U.: Description logics - basics, applications, and more. In: Tutorial Given at ECAI-2002, http:\/\/www.cs.man.ac.uk\/~horrocks\/Slides\/ecai-handout.pdf"},{"issue":"1-3","key":"50_CR7","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 {ALC}. Fundamenta Informaticae\u00a093(1-3), 273\u2013288 (2009)","journal-title":"Fundamenta Informaticae"},{"key":"50_CR8","unstructured":"Nguyen, L.A.: The long version of the current paper (2011), http:\/\/www.mimuw.edu.pl\/~nguyen\/alci-long.pdf"},{"key":"50_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/978-3-642-04441-0_38","volume-title":"Computational Collective Intelligence. Semantic Web, Social Networks and Multiagent Systems","author":"L.A. Nguyen","year":"2009","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)"},{"key":"50_CR10","first-page":"207","volume-title":"Proceedings of KSE 2009","author":"L.A. Nguyen","year":"2009","unstructured":"Nguyen, L.A., Sza\u0142as, A.: An optimal tableau decision procedure for Converse-PDL. In: Nguyen, N.-T., Bui, T.-D., Szczerbicki, E., Nguyen, N.-B. (eds.) Proceedings of KSE 2009, pp. 207\u2013214. IEEE Computer Society, Los Alamitos (2009)"},{"key":"50_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-642-02959-2_31","volume-title":"Automated Deduction \u2013 CADE-22","author":"L.A. Nguyen","year":"2009","unstructured":"Nguyen, L.A., Sza\u0142as, A.: A tableau calculus for regular grammar logics with converse. In: Schmidt, R.A. (ed.) CADE-22. LNCS(LNAI), vol.\u00a05663, pp. 421\u2013436. Springer, Heidelberg (2009)"},{"issue":"1","key":"50_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":"50_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"}],"container-title":["Lecture Notes in Computer Science","Foundations of Intelligent Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21916-0_50","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,20]],"date-time":"2020-06-20T18:49:51Z","timestamp":1592678991000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21916-0_50"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642219153","9783642219160"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21916-0_50","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}