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

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.

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

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

I. Horrocks, The FaCT System, Proc. of the 2nd Int. Conf. on Analytic Tableaux and Related Methods (TABLEAUX'98, pp.307-312, 1998.
DOI : 10.1007/3-540-69778-0_30

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

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

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

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

L. Duc, C. Lamolle, M. Curé, and O. , An EXPSPACE tableaux-based algorithm for SHOIQ, 2012.

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

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.

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