{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T09:33:19Z","timestamp":1743154399720,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319179957"},{"type":"electronic","value":"9783319179964"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17996-4_29","type":"book-chapter","created":{"date-parts":[[2015,4,21]],"date-time":"2015-04-21T14:35:44Z","timestamp":1429626944000},"page":"321-333","source":"Crossref","is-referenced-by-count":0,"title":["Designing a Tableau Reasoner for Description\u00a0Logics"],"prefix":"10.1007","author":[{"given":"Linh Anh","family":"Nguyen","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","volume-title":"A Semantic Web Primer","author":"G. Antoniou","year":"2004","unstructured":"Antoniou, G., van Harmelen, F.: A Semantic Web Primer. MIT Press, Cambridge (2004)"},{"key":"29_CR2","volume-title":"The description logic handbook: theory, implementation, and applications","author":"F. Baader","year":"2003","unstructured":"Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F.: The description logic handbook: theory, implementation, and applications. Cambridge University Press, New York (2003)"},{"key":"29_CR3","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":"29_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 $\\mathcal{ALC}$. Artificial Intelligence\u00a0124, 87\u2013138 (2000)","journal-title":"Artificial Intelligence"},{"issue":"1","key":"29_CR5","doi-asserted-by":"publisher","first-page":"61","DOI":"10.3166\/jancl.21.61-91","volume":"21","author":"B. Dunin-K\u0119plicz","year":"2011","unstructured":"Dunin-K\u0119plicz, B., Nguyen, L.A., Sza\u0142as, A.: Converse-PDL with regular inclusion axioms: A framework for MAS logics. Journal of Applied Non-Classical Logics\u00a021(1), 61\u201391 (2011)","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"29_CR6","unstructured":"Farsiniamarj, N.: Combining integer programming and tableau-based reasoning: a hybrid calculus for the description logic SHQ. Master\u2019s thesis, Concordia University (2008)"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-642-14203-1_39","volume-title":"Automated Reasoning","author":"B. Glimm","year":"2010","unstructured":"Glimm, B., Horrocks, I., Motik, B.: Optimized description logic reasoning via core blocking. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 457\u2013471. Springer, Heidelberg (2010)"},{"key":"29_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/11554554_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Gor\u00e9","year":"2005","unstructured":"Gor\u00e9, R., Nguyen, L.A.: A tableau calculus with automaton-labelled formulae for regular grammar logics. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol.\u00a03702, pp. 138\u2013152. Springer, Heidelberg (2005)"},{"key":"29_CR9","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.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)"},{"issue":"4","key":"29_CR10","doi-asserted-by":"publisher","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. Reasoning\u00a050(4), 355\u2013381 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"29_CR11","series-title":"LNAI","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 (LNAI), vol.\u00a05663, pp. 437\u2013452. Springer, Heidelberg (2009)"},{"key":"29_CR12","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":"29_CR13","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":"29_CR14","unstructured":"Hladik, J., Model, J.: Tableau systems for SHIO and SHIQ. In: Proc. of Description Logics 2004. CEUR Workshop Proceedings, vol.\u00a0104 (2004)"},{"key":"29_CR15","unstructured":"Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible $\\mathcal{SROIQ}$. In: Doherty, P., Mylopoulos, J., Welty, C.A. (eds.) Proc. of KR 2006, pp. 57\u201367. AAAI Press (2006)"},{"issue":"3","key":"29_CR16","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."},{"key":"29_CR17","unstructured":"Horrocks, I., Sattler, U.: Ontology reasoning in the SHOQ(D) description logic. In: Nebel, B. (ed.) Proc. of IJCAI 2001, pp. 199\u2013204. Morgan Kaufmann (2001)"},{"issue":"3","key":"29_CR18","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10817-007-9079-9","volume":"39","author":"I. Horrocks","year":"2007","unstructured":"Horrocks, I., Sattler, U.: A tableau decision procedure for $\\mathcal{SHOIQ}$. J. Autom. Reasoning\u00a039(3), 249\u2013276 (2007)","journal-title":"J. Autom. Reasoning"},{"key":"29_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/10721959_39","volume-title":"Automated Deduction - CADE-17","author":"I. Horrocks","year":"2000","unstructured":"Horrocks, I., Sattler, U., Tobies, S.: Reasoning with individuals for the description logic SHIQ. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 482\u2013496. Springer, Heidelberg (2000)"},{"issue":"4","key":"29_CR20","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/s10462-010-9197-3","volume":"35","author":"R.B. Mishra","year":"2011","unstructured":"Mishra, R.B., Kumar, S.: Semantic web reasoners and languages. Artif. Intell. Rev.\u00a035(4), 339\u2013368 (2011)","journal-title":"Artif. Intell. Rev."},{"key":"29_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/11916277_16","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"B. Motik","year":"2006","unstructured":"Motik, B., Sattler, U.: A comparison of reasoning techniques for querying large description logic ABoxes. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 227\u2013241. Springer, Heidelberg (2006)"},{"issue":"1-3","key":"29_CR22","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":"29_CR23","doi-asserted-by":"crossref","unstructured":"Nguyen, L.A.: A cut-free ExpTime tableau decision procedure for the logic extending Converse-PDL with regular inclusion axioms. arXiv:1104.0405 (2011)","DOI":"10.1007\/978-3-642-23935-9_56"},{"key":"29_CR24","unstructured":"Nguyen, L.A.: ExpTime tableaux for the description logic $\\mathcal{SHIQ}$ based on global state caching and integer linear feasibility checking. arXiv:1205.5838 (2012)"},{"key":"29_CR25","unstructured":"Nguyen, L.A.: Cut-free ExpTime tableaux for Converse-PDL extended with regular inclusion axioms. In: Proc. of KES-AMSTA 2013. Frontiers in Artificial Intelligence and Applications, vol.\u00a0252, pp. 235\u2013244. IOS Press (2013)"},{"key":"29_CR26","series-title":"SCI","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-319-00293-4_25","volume-title":"Advanced Computational Methods for Knowledge Engineering","author":"L.A. Nguyen","year":"2013","unstructured":"Nguyen, L.A.: A tableau method with optimal complexity for deciding the description logic SHIQ. In: Nguyen, N.T., van Do, T., Thi, H.A. (eds.) ICCSAMA 2013. SCI, vol.\u00a0479, pp. 331\u2013342. Springer, Heidelberg (2013)"},{"key":"29_CR27","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/j.neucom.2014.05.071","volume":"146","author":"L.A. Nguyen","year":"2014","unstructured":"Nguyen, L.A.: ExpTime tableaux with global state caching for the description logic SHIO. Neurocomputing\u00a0146, 249\u2013263 (2014)","journal-title":"Neurocomputing"},{"issue":"4","key":"29_CR28","doi-asserted-by":"crossref","first-page":"433","DOI":"10.3233\/FI-2014-1133","volume":"135","author":"L.A. 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. Fundam. Inform.\u00a0135(4), 433\u2013449 (2014)","journal-title":"Fundam. Inform."},{"key":"29_CR29","doi-asserted-by":"crossref","unstructured":"Nguyen, L.A., Goli\u0144ska-Pilarek, J.: ExpTime tableaux with global caching for the description logic SHOQ. CoRR, abs\/1405.7221 (2014)","DOI":"10.1016\/j.neucom.2014.05.071"},{"key":"29_CR30","doi-asserted-by":"crossref","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.) Proc. of KSE 2009, pp. 207\u2013214. IEEE Computer Society (2009)","DOI":"10.1109\/KSE.2009.12"},{"key":"29_CR31","series-title":"LNAI","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 2009. LNCS (LNAI), vol.\u00a05663, pp. 421\u2013436. Springer, Heidelberg (2009)"},{"issue":"2","key":"29_CR32","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0022-0000(80)90061-6","volume":"20","author":"V.R. Pratt","year":"1980","unstructured":"Pratt, V.R.: A near-optimal method for reasoning about action. J. Comp. Syst. Sci.\u00a020(2), 231\u2013254 (1980)","journal-title":"J. Comp. Syst. Sci."},{"key":"29_CR33","unstructured":"Semantic web case studies and use cases, \n                      http:\/\/www.w3.org\/2001\/sw\/sweo\/public\/UseCases\/"}],"container-title":["Advances in Intelligent Systems and Computing","Advanced Computational Methods for Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17996-4_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,22]],"date-time":"2023-02-22T12:24:41Z","timestamp":1677068681000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17996-4_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319179957","9783319179964"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17996-4_29","relation":{},"ISSN":["2194-5357","2194-5365"],"issn-type":[{"type":"print","value":"2194-5357"},{"type":"electronic","value":"2194-5365"}],"subject":[],"published":{"date-parts":[[2015]]}}}