A Tableau Decision Procedure for $\mathcal{SHOIQ}$

Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F., (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge, MA (2003)

Baader, F., Hanschke, P.: A schema for integrating concrete domains into concept languages. In: Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI’91), pp. 452–457 (1991)

Baader, F., Hollunder, B.: A terminological knowledge representation system with complete inference algorithms. In: Proceedings of the First International Workshop on Processing Declarative Knowledge. Lecture Notes in Computer Science, vol. 572, pp. 67–85. Springer, Berlin Heidelberg New York (1991)

Baader, F., Sattler, U.: An overview of tableau algorithms for description logics. Stud. Log. 69(1), 5–40 (2001)

Bechhofer, S., van Harmelen, F., Hendler, J., Horrocks, I., McGuinness, D.L., Patel-Schneider, P.F., Stein, L.A.: OWL Web ontology language reference. W3C Recommendation. Available at http://www.w3.org/TR/owl-ref/ (2004)

Blackburn, P., Seligman, J.: Hybrid languages. J. Logic Lang. Inf. 4, 251–272 (1995)

Brachman, R.J., McGuinness, D.L., Patel-Schneider, P.F., Resnick, L.A., Borgida, A.: Living with CLASSIC: when and how to use a KL-ONE-like language. In: Sowa, J.F. (ed.) Principles of Semantic Networks, pp. 401–456. Morgan Kaufmann, Los Altos, CA (1991)

Bresciani, P., Franconi, E., Tessaris, S.: Implementing and testing expressive description logics: preliminary report. In: Proceedings of the 1995 Description Logic Workshop (DL’95), pp. 131–139 (1995)

Buchheit, M., Donini, F.M., Schaerf, A.: Decidable reasoning in terminological knowledge representation systems. J. Artif. Intell. Res. 1, 109–138 (1993)

Calvanese, D., De Giacomo, G., Lenzerini, M., Nardi, D., Rosati, R.: Description logic framework for information integration. In: Proceedings of the 6th International Conference on Principles of Knowledge Representation and Reasoning (KR’98), pp. 2–13. Morgan Kaufmann, Los Altos, CA (1998)

De Giacomo, G.: Decidability of class-based knowledge representation formalisms. Ph.D. Thesis, Dipartimento di Informatica e Sistemistica, Università di Roma “La Sapienza” (1995)

De Giacomo, G., Lenzerini, M.: Boosting the correspondence between description logics and propositional dynamic logics (extended abstract). In: Proceedings of the 12th National Conference on Artificial Intelligence (AAAI-94). AAAI Press, Menlo Park, CA (1994)

De Giacomo, G., Lenzerini, M.: TBox and ABox reasoning in expressive description logics. In: Proceedings of the 5th International Conference on the Principles of Knowledge Representation and Reasoning (KR’96), pp. 316–327. Morgan Kaufmann, Los Altos, CA (1996)

Donini, F.M., Lenzerini, M., Nardi, D.: Using terminological reasoning in hybrid systems. AI Commun. – Eur. J. Artif. Intell. 3(3), 128–138 (1990)

Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194–211 (1979)

Gardiner, T., Tsarkov, D., Horrocks, I.: Framework for an automated comparison of description logic reasoners. In: Proceedings of the 2006 International Semantic Web Conference (ISWC 2006). Lecture Notes in Computer Science, vol. 4273, pp. 654–667. Springer, Berlin Heidelberg New York (2006)

Grädel, E.: Why are modal logics so robustly decidable? In: Paun, G., Rozenberg, G., Salomaa, A. (eds.) Current Trends in Theoretical Computer Science: Entering the 21st Century, pp. 393–408. World Scientific, Singapore (2001)

Haarslev, V., Möller, R.,: The description logic $\mathcal{ALCNH}_{R+}$ extended with concrete domains: a practically motivated approach. In: Proceedings of the International Joint Conference on Automated Reasoning (IJCAR 2001). Lecture Notes in Artificial Intelligence, vol. 2083, pp. 29–44. Springer, Berlin Heidelberg New York (2001a)

Haarslev, V., Möller, R.: RACER System description. In: Proceedings of the International Joint Conference on Automated Reasoning (IJCAR 2001). Lecture Notes in Artificial Intelligence, vol. 2083, pp. 701–705. Springer, Berlin Heidelberg New York (2001b)

Hladik, J., Model, J.: Tableau systems for $\mathcal{SHIO}$ and $\mathcal{SHIQ}$ . In: Proceedings of the 2004 Description Logic Workshop (DL 2004). CEUR. Available from ceur-ws.org (2004)

Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. Technical Report RR-91-03, Deutsches Forschungszentrum für Künstliche Intelligenz (DFKI), Kaiserslautern (Germany). An abridged version appeared in Proceedings of the 2nd International Conference on the Principles of Knowledge Representation and Reasoning (KR’91) (1991)

Horrocks, I., Patel-Schneider, P.F.: FaCT and DLP: Automated reasoning with analytic tableaux and related methods. In: Proceedings of the 2nd International Conference on Analytic Tableaux and Related Methods (TABLEAUX’98). Lecture Notes in Artificial Intelligence, vol. 1397, pp. 27–30. Springer, Berlin Heidelberg New York (1998)

Horrocks, I., Patel-Schneider, P.F.: Optimizing description logic subsumption. J. Log. Comput. 9(3), 267–293 (1999)

Horrocks, I., Patel-Schneider, P.F., van Harmelen, F.: From $\mathcal{SHIQ}$ and RDF to OWL: the making of a web ontology language. J. Web Semantics 1(1), 7–26 (2003)

Horrocks, I., Sattler, U.: Ontology reasoning in the $\mathcal{SHOQ}$ (D) description logic. In: Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI 2001), pp. 199–204. Morgan Kaufmann, Los Altos, CA (2001)

Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for expressive description logics. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR’99). Lecture Notes in Artificial Intelligence, vol. 1705, pp. 161–180. Springer, Berlin Heidelberg New York (1999)

Horrocks, I., Sattler, U., Tobies, S.: Reasoning with individuals for the description logic $\mathcal{SHIQ}$ . In: McAllester, D. (ed.) Proceedings of the 17th International Conference on Automated Deduction (CADE 2000). Lecture Notes in Computer Science, vol. 1831, pp. 482–496. Springer, Berlin Heidelberg New York (2000)

McGuinness, D.L., Wright, J.R.: An industrial strength description logic-based configuration platform. IEEE Intell. Syst. 69–77 (1998)

Pacholski, L., Szwast, W., Tendera, L.: Complexity of two-variable logic with counting. In: Proceedings of the 12th IEEE Symposium on Logic in Computer Science (LICS’97), pp. 318–327. IEEE Computer Society Press, Los Alamitos, CA (1997)

Pan, J., Horrocks, I.: Web ontology reasoning with datatype groups. In: Fensel, D., Sycara, K., Mylopoulos, J. (eds.) Proc. of the 2003 International Semantic Web Conference (ISWC 2003). Lecture Notes in Computer Science, vol. 2870, pp. 47–63. Springer, Berlin Heidelberg New York (2003)

Patel-Schneider, P.F., Owsnicki-Klew, B., Kobsa, A., Guarino, N., MacGregor, R., Mark, W.S., McGuinness, D., Nebel, B., Schmiedel, A., Yen, J.: Term subsumption languages in knowledge representation. AI Mag. 11(2), 16–23 (1990)

Schaerf, A.: Reasoning with individuals in concept languages. Data Knowl. Eng. 13(2), 141–176 (1994)

Schild, K.: A correspondence theory for terminological logics: preliminary report. In: Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI’91), pp. 466–471. Morgan Kaufmann, Los Altos, CA (1991)

Sirin, E., Grau, B.C., Parsia, B.: From wine to water: optimizing description logic reasoning for nominals. In: Proceedings of the 10th International Conference on Principles of Knowledge Representation and Reasoning (KR 2006), pp. 90–99. AAAI Press (2006)

Sirin, E., Parsia, B., Cuenca, B. Grau, Kalyanpur, A., Katz, Y.: Pellet: a practical OWL-DL reasoner. J. Web Semantics 5(2), 51–53 (2007)

Tobies, S.: The complexity of reasoning with cardinality restrictions and nominals in expressive description logics. J. Artif. Intell. Res. 12, 199–217 (2000)

Tobies, S.: Complexity results and practical algorithms for logics in knowledge representation. Ph.D. thesis, LuFG Theoretical Computer Science, RWTH-Aachen, Germany (2001)

Tsarkov, D., Horrocks, I.: Ordering heuristics for description logic reasoning. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI 2005), pp. 609–614. Morgan Kaufmann, Los Altos (2005)

Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: system description. In: Proceedings of the International Joint Conference on Automated Reasoning (IJCAR 2006). Lecture Notes in Artificial Intelligence, vol. 4130, pp. 292–297. Springer, Berlin Heidelberg New York (2006)

Vardi, M.Y.: Why is modal logic so robustly decidable. In: DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 31, pp. 149–184. American Mathematical Society, Providence, RI (1997)