Designing a Tableau Reasoner for Description Logics

1. Antoniou, G., van Harmelen, F.: A Semantic Web Primer. MIT Press, Cambridge (2004)

   Google Scholar 

2. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F.: The description logic handbook: theory, implementation, and applications. Cambridge University Press, New York (2003)

   MATH  Google Scholar 

3. Baader, F., Sattler, U.: An overview of tableau algorithms for description logics. Studia Logica 69, 5–40 (2001)

   Article  MathSciNet  MATH  Google Scholar 

4. Donini, F., Massacci, F.: ExpTime tableaux for \(\mathcal{ALC}\). Artificial Intelligence 124, 87–138 (2000)

   Article  MathSciNet  MATH  Google Scholar 

5. Dunin-Kęplicz, B., Nguyen, L.A., Szałas, A.: Converse-PDL with regular inclusion axioms: A framework for MAS logics. Journal of Applied Non-Classical Logics 21(1), 61–91 (2011)

   Article  MathSciNet  MATH  Google Scholar 

6. Farsiniamarj, N.: Combining integer programming and tableau-based reasoning: a hybrid calculus for the description logic SHQ. Master’s thesis, Concordia University (2008)

   Google Scholar 

7. Glimm, B., Horrocks, I., Motik, B.: Optimized description logic reasoning via core blocking. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 457–471. Springer, Heidelberg (2010)

   Chapter  Google Scholar 

8. Goré, R., Nguyen, L.A.: A tableau calculus with automaton-labelled formulae for regular grammar logics. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 138–152. Springer, Heidelberg (2005)

   Chapter  Google Scholar 

9. Goré, R., 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 

10. Goré, R., Nguyen, L.A.: ExpTime tableaux for ALC using sound global caching. J. Autom. Reasoning 50(4), 355–381 (2013)

    Article  MathSciNet  MATH  Google Scholar 

11. Goré, R., Widmann, F.: An optimal on-the-fly tableau-based decision procedure for PDL-satisfiability. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 437–452. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

12. 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 

13. 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 

14. Hladik, J., Model, J.: Tableau systems for SHIO and SHIQ. In: Proc. of Description Logics 2004. CEUR Workshop Proceedings, vol. 104 (2004)

    Google Scholar 

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

    Google Scholar 

16. 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 

17. Horrocks, I., Sattler, U.: Ontology reasoning in the SHOQ(D) description logic. In: Nebel, B. (ed.) Proc. of IJCAI 2001, pp. 199–204. Morgan Kaufmann (2001)

    Google Scholar 

18. Horrocks, I., Sattler, U.: A tableau decision procedure for \(\mathcal{SHOIQ}\). J. Autom. Reasoning 39(3), 249–276 (2007)

    Article  MathSciNet  MATH  Google Scholar 

19. Horrocks, I., Sattler, U., Tobies, S.: Reasoning with individuals for the description logic SHIQ. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 482–496. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

20. Mishra, R.B., Kumar, S.: Semantic web reasoners and languages. Artif. Intell. Rev. 35(4), 339–368 (2011)

    Article  Google Scholar 

21. Motik, B., Sattler, U.: A comparison of reasoning techniques for querying large description logic ABoxes. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 227–241. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

22. 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 

23. Nguyen, L.A.: A cut-free ExpTime tableau decision procedure for the logic extending Converse-PDL with regular inclusion axioms. arXiv:1104.0405 (2011)

    Google Scholar 

24. Nguyen, L.A.: ExpTime tableaux for the description logic \(\mathcal{SHIQ}\) based on global state caching and integer linear feasibility checking. arXiv:1205.5838 (2012)

    Google Scholar 

25. Nguyen, L.A.: Cut-free ExpTime tableaux for Converse-PDL extended with regular inclusion axioms. In: Proc. of KES-AMSTA 2013. Frontiers in Artificial Intelligence and Applications, vol. 252, pp. 235–244. IOS Press (2013)

    Google Scholar 

26. Nguyen, L.A.: A tableau method with optimal complexity for deciding the description logic SHIQ. In: Nguyen, N.T., van Do, T., Thi, H.A. (eds.) ICCSAMA 2013. SCI, vol. 479, pp. 331–342. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

27. Nguyen, L.A.: ExpTime tableaux with global state caching for the description logic SHIO. Neurocomputing 146, 249–263 (2014)

    Article  Google Scholar 

28. Nguyen, L.A., Golińska-Pilarek, J.: An ExpTime tableau method for dealing with nominals and qualified number restrictions in deciding the description logic SHOQ. Fundam. Inform. 135(4), 433–449 (2014)

    MathSciNet  MATH  Google Scholar 

29. Nguyen, L.A., Golińska-Pilarek, J.: ExpTime tableaux with global caching for the description logic SHOQ. CoRR, abs/1405.7221 (2014)

    Google Scholar 

30. Nguyen, L.A., Szałas, A.: An optimal tableau decision procedure for Converse-PDL. In: Nguyen, N.-T., Bui, T.-D., Szczerbicki, E., Nguyen, N.-B. (eds.) Proc. of KSE 2009, pp. 207–214. IEEE Computer Society (2009)

    Google Scholar 

31. Nguyen, L.A., Szałas, A.: A tableau calculus for regular grammar logics with converse. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 421–436. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

32. Pratt, V.R.: A near-optimal method for reasoning about action. J. Comp. Syst. Sci. 20(2), 231–254 (1980)

    Article  MathSciNet  MATH  Google Scholar 

33. Semantic web case studies and use cases, http://www.w3.org/2001/sw/sweo/public/UseCases/

Download references