N. For, L(x) with n > 0. If (? nS.C) ? L(x) then (? nS.C) ? L(x ) for all x ? ?(x) and (? nS.C) ? L (?(x)). By P15, we have {? mS

R. 1. Baader, F. Nutt, and W. , Basic Description Logics, pp.47-104, 2007.
DOI : 10.1017/CBO9780511711787.004
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.222

F. Baader, P. , and H. , A scheme for integrating concrete domains into concept languages, Proceedings of the 12th International Joint Conference on Artificial Intelligence, IJCAI-91, pp.452-457, 1991.

F. Baader and U. Sattler, An overview of tableau algorithms for description logics, Studia Logica, vol.69, issue.1, pp.5-40, 2001.
DOI : 10.1023/A:1013882326814

D. Giacomo, G. Lenzerini, and M. , Boosting the correspondence between description logics and propositional dynamic logics, Proceedings of the 12th National conference on Artificial Intelligence, pp.205-212, 1994.

F. Donini, Complexity of Reasoning, pp.105-148, 2007.
DOI : 10.1017/CBO9780511711787.005

M. J. Fischer and R. I. Ladner, Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol.18, issue.2, pp.174-211, 1979.
DOI : 10.1016/0022-0000(79)90046-1

F. M. Donini and F. M. , EXPtime tableaux for ALC, Artificial Intelligence, vol.124, issue.1, pp.87-138, 2000.
DOI : 10.1016/S0004-3702(00)00070-9

R. Goré and L. A. Nguyen, EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies, pp.133-148, 2007.
DOI : 10.1007/978-3-540-73099-6_12

V. Haarslev and R. Moller, RACER System Description, Proc. of the Int. Joint on Automated Reasoning, pp.701-705, 2001.
DOI : 10.1007/3-540-45744-5_59
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.126.6142

I. Horrocks, The FaCT system URL download, Proc. of the 2nd Int. Conf. on Analytic Tableaux and Related Methods (TABLEAUX'98), pp.307-312, 1998.

I. Horrocks, O. Kutz, and U. Sattler, The irresistible SRIQ, Proc. of the First Int. Workshop on OWL Experiences and Directions (OWLED 2005) (2005). URL download, 2006.

I. Horrocks, O. Kutz, and U. Sattler, The even more irresistible SROIQ URL download, Proc. of the 10th Int. Conf. on Principles of Knowledge Representation and Reasoning, pp.57-67, 2006.

I. Horrocks and U. Sattler, A Tableau Decision Procedure for $\mathcal{SHOIQ}$, Journal of Automated Reasoning, vol.12, issue.2, pp.249-276, 2007.
DOI : 10.1007/s10817-007-9079-9

I. Horrocks, U. Sattler, and S. Tobies, A description logic with transitive and converse roles, role hierarchies and qualifying number restrictions, LTCS-Report 99-08, 1999.

I. Horrocks, U. Sattler, and S. Tobies, Practical Reasoning for Expressive Description Logics, Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 1999.
DOI : 10.1007/3-540-48242-3_11

U. Hustadt, B. Motik, and U. Sattler, A Decomposition Rule for Decision Procedures by Resolutionbased Calculi, Proc. of the 11th Int LNAI, pp.21-35, 2004.

Y. Kazakov and B. Motik, A Resolution-Based Decision Procedure for $\mathcal{SHOIQ}$, Journal of Automated Reasoning, vol.4023, pp.89-116, 2008.
DOI : 10.1007/11814771_53

L. Duc and C. , Decidability of SHI with transitive closure of roles, Proceedings of the European Semantic Web Conference, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00793443

B. Motik, R. Shearer, and I. Horrocks, Hypertableau reasoning for description logics URL download, J. of Artificial Intelligence Research, vol.36, pp.165-228, 2009.

M. Ortiz, An automata-based algorithm for description logics around SRIQ, Proceedings of the fourth Latin American Workshop on Non-Monotonic Reasoning, 2008.

P. Patel-schneider, P. Hayes, and I. Horrocks, Owl web ontology language semantics and abstract syntax, p.3, 2004.

I. Pratt-hartmann, Complexity of the Two-Variable Fragment with Counting Quantifiers, Journal of Logic, Language and Information, vol.28, issue.4, pp.369-395, 2005.
DOI : 10.1007/s10849-005-5791-1

R. Shearer, B. Motik, and I. Horrocks, HermiT: A Highly-Efficient OWL Reasoner, Proc. of the 5th Int. Workshop on OWL: Experiences and Directions, 2008.

E. Sirin, B. Parsia, B. C. Grau, A. Kalyanpur, and Y. Katz, Pellet: A practical OWL-DL reasoner, Web Semantics: Science, Services and Agents on the World Wide Web, vol.5, issue.2, pp.51-53, 2007.
DOI : 10.1016/j.websem.2007.03.004

S. Tobies, The complexity of reasoning with cardinality restrictions and nominals in expressive description logics, Journal of Artificial Intelligence Research, vol.12, pp.199-217, 2000.

S. Tobies, Complexity results and practical algorithms for logics in knowledge representation, 2001.

D. Tsarkov and I. Horrocks, FaCT++ description logic reasoner: System description URL download, Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2006), pp.292-297, 2006.

M. Y. Vardi, Reasoning about the past with two-way automata, Proceedings of ICALP 2002, pp.628-641, 1998.
DOI : 10.1007/BFb0055090

M. Y. Vardi and P. Wolper, Automata-theoretic techniques for modal logics of programs, In: Journal of Computer and System Science, vol.32, p.183221, 1986.