An ExpTime Tableau Method for Dealing with Nominals and Qualified Number Restrictions in Deciding the Description Logic SHOQ

• Autorzy: Nguyen L. A. , Golińska-Pilarek J.

Identyfikatory

DOI

10.3233/FI-2014-1133

• Języki publikacji: EN

Abstrakty

EN

We present the first tableau method with an EXPTIME (optimal) complexity for checking satisfiability of a knowledge base in the description logic SHOQ, which extends ALC with transitive roles, hierarchies of roles, nominals and qualified number restrictions. The complexity is measured using unary representation for numbers (in number restrictions). Our procedure is based on global caching and integer linear feasibility checking.

Słowa kluczowe

EN

automated reasoning; description logics; global state caching; integer linear feasibility

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 135, nr 4
• Strony: 433--449
• Opis fizyczny: Bibliogr. 18 poz., rys., tab.

Twórcy

autor

Nguyen L. A.

• Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warsaw, Poland
• Faculty of Information Technology, VNU University of Engineering and Technology, 144 Xuan Thuy, Hanoi, Vietnam

autor

Golińska-Pilarek J.

• Institute of Philosophy, University of Warsaw, Krakowskie Przedmieście 3, 00-927 Warsaw, Poland

Bibliografia

• [1] Faddoul, J., Haarslev, V.: Algebraic tableau reasoning for the description logic SHOQ, J. Applied Logic, 8(4), 2010, 334–355.
• [2] Farsiniamarj, N.: Combining integer programming and tableau-based reasoning: a hybrid calculus for the description logic SHQ, Master Thesis, Concordia University, 2008.
• [3] Goré, R., Nguyen, L.: ExpTime Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies, Proceedings of TABLEAUX 2007, 4548, Springer, 2007.
• [4] Goré, R., Nguyen, L.: ExpTime Tableaux for ALC Using Sound Global Caching, J. Autom. Reasoning, 50(4), 2013, 355–381.
• [5] Goré, R., Widmann, F.: Sound Global State Caching for ALC with Inverse Roles, Proceedings of TABLEAUX 2009 (M. Giese, A. Waaler, Eds.), 5607, Springer, 2009.
• [6] Goré, R., Widmann, F.: Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse, Proceedings of IJCAR 2010 (J. Giesl, R. Hähnle, Eds.), 6173, Springer, 2010.
• [7] Hladik, J., Model, J.: Tableau Systems for SHIO and SHIQ, Proceedings of DL’2004, 104, 2004.
• [8] Horrocks, I., Kutz, O., Sattler, U.: The Even More Irresistible SROIQ, Proc. of KR’2006 (P. Doherty, J. Mylopoulos, C. Welty, Eds.), AAAI Press, 2006.
• [9] Horrocks, I., Sattler, U.: Ontology Reasoning in the SHOQ(D) Description Logic, Proceedings of IJCAI’2001, Morgan Kaufmann, 2001.
• [10] Nguyen, L.: A Cut-Free ExpTime Tableau Decision Procedure for the Description Logic SHI, Proceedings of ICCCI’2011 (1), 6922, Springer, 2011 (see also the long version http://arxiv.org/abs/1106.2305).
• [11] Nguyen, L.: ExpTime Tableaux for the Description Logic SHIQ Based on Global State Caching and Integer Linear Feasibility Checking, arXiv:1205.5838, 2012.
• [12] Nguyen, L.: A Tableau Method with Optimal Complexity for Deciding the Description Logic SHIQ, Proceedings of ICCSAMA’2013, 479, Springer, 2013.
• [13] Nguyen, L., Golińska-Pilarek, J.: An ExpTime Tableau Method for Dealing with Nominals and Quantified Number Restrictions in Deciding the Description Logic SHOQ, Proceedings of CS&P’2013.
• [14] Nguyen, L., Golińska-Pilarek, J.: ExpTime Tableaux with Global Caching for the Description Logic SHOQ, arXiv:1405.7221 [cs.LO], 2014.
• [15] Pan, J., Horrocks, I.: Reasoning in the SHOQ(Dn) Description Logic, Proc. of DL’2002, 53, 2002.
• [16] Pratt, V.: A Near-Optimal Method for Reasoning about Action, J. Comp. Syst. Sci., 20(2), 1980, 231–254.
• [17] Tobies, S.: Complexity results and practical algorithms for logics in knowledge representation, Ph.D. Thesis, RWTH-Aachen, 2001.
• [18] http://owl.cs.manchester.ac.uk/navigator/.