A Cut-Free ExpTime Tableau Decision Procedure for the Description Logic SHI

1. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): Description Logic Handbook. Cambridge University Press, Cambridge (2002)

   Google Scholar 

2. D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J. (eds.): Handbook of Tableau Methods. Springer, Heidelberg (1999)

   MATH  Google Scholar 

3. Goré, R.P., 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. 4548, pp. 133–148. Springer, Heidelberg (2007)

   Chapter  Google Scholar 

4. Goré, R., Widmann, F.: Sound global state caching for ALC with inverse roles. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 205–219. Springer, Heidelberg (2009)

   Chapter  Google Scholar 

5. Goré, R., Widmann, F.: Optimal and cut-free tableaux for propositional dynamic logic with converse. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 225–239. Springer, Heidelberg (2010)

   Chapter  Google Scholar 

6. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible \(\mathcal{SROIQ}\). In: Doherty, P., Mylopoulos, J., Welty, C.A. (eds.) Proceedings of KR 2006, pp. 57–67. AAAI Press, Menlo Park (2006)

   Google Scholar 

7. Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. J. Log. Comput. 9(3), 385–410 (1999)

   Article  MathSciNet  MATH  Google Scholar 

8. Nguyen, L.A.: An efficient tableau prover using global caching for the description logic \(\mathcal{ALC}\). Fundamenta Informaticae 93(1-3), 273–288 (2009)

   MathSciNet  MATH  Google Scholar 

9. Nguyen, L.A.: Cut-free expTime tableaux for checking satisfiability of a knowledge base in the description logic \(\mathcal{ALCI}\). In: Kryszkiewicz, M., Rybinski, H., Skowron, A., Raś, Z.W. (eds.) ISMIS 2011. LNCS(LNAI), vol. 6804, pp. 465–475. Springer, Heidelberg (2011)

   Chapter  Google Scholar 

10. Nguyen, L.A.: The long version of the current paper (2011), http://arxiv.org/abs/1106.2305

11. Nguyen, L.A., Szałas, A.: ExpTime tableaux for checking satisfiability of a knowledge base in the description logic \(\mathcal{ALC}\). In: Nguyen, N.T., Kowalczyk, R., Chen, S.-M. (eds.) ICCCI 2009. LNCS(LNAI), vol. 5796, pp. 437–448. Springer, Heidelberg (2009)

    Google Scholar 

12. Nguyen, L.A., Szałas, A.: Checking consistency of an ABox w.r.t. global assumptions in PDL. Fundamenta Informaticae 102(1), 97–113 (2010)

    MathSciNet  MATH  Google Scholar 

13. Nguyen, L.A., Szałas, A.: Tableaux with global caching for checking satisfiability of a knowledge base in the description logic \(\mathcal{SH}\). T. Computational Collective Intelligence 1, 21–38 (2010)

    MATH  Google Scholar 

14. Nguyen, L.A., Szałas, A.: ExpTime tableau decision procedures for regular grammar logics with converse. Studia Logica 98(3) (2011)

    Google Scholar 

Download references