A Resolution Procedure for Description Logics with Nominal Schemas

  • Cong Wang
  • Pascal Hitzler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7774)


We present a polynomial resolution-based decision procedure for the recently introduced description logic \(\mathcal{ELHOV}_{n}(\sqcap)\) , which features nominal schemas as new language construct. Our algorithm is based on ordered resolution and positive superposition, together with a lifting lemma. In contrast to previous work on resolution for description logics, we have to overcome the fact that \(\mathcal{ELHOV}_{n}(\sqcap)\) does not allow for a normalization resulting in clauses of globally limited size.


Knowledge Base Description Logic Resolution Procedure Nominal Schema Clause Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baader, F., Brandt, S., Lutz, C.: Pushing the el envelope. In: Kaelbling, L.P., Saffiotti, A. (eds.) IJCAI, pp. 364–369. Professional Book Center (2005)Google Scholar
  2. 2.
    Bachmair, L., Ganzinger, H.: Ordered chaining for total orderings. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 435–450. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  3. 3.
    Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 19–99. Elsevier, MIT Press (2001)Google Scholar
  4. 4.
    Boley, H., Hallmark, G., Kifer, M., Paschke, A., Polleres, A., Reynolds, D. (eds.): RIF Core Dialect. W3C Recommendation (June 22, 2010),
  5. 5.
    Horrocks, I., Patel-Schneider, P., Boley, H., Tabet, S., Grosof, B., Dean, M.: SWRL: A Semantic Web Rule Language. W3C Member Submission (May 21, 2004),
  6. 6.
    Hustadt, U., Motik, B., Sattler, U.: Reasoning for Description Logics around SHIQ in a Resolution Framework. Tech. Rep. 3-8-04/04, FZI, Germany (2004)Google Scholar
  7. 7.
    Kazakov, Y.: Saturation-based decision procedures for extensions of the guarded fragment. Ph.D. thesis, Saarländische Universitäts- und Landesbibliothek, Postfach 151141, 66041 Saarbrücken (2005),
  8. 8.
    Kazakov, Y., Krötzsch, M., Simančík, F.: Practical reasoning with nominals in the \(\mathcal{EL}\) family of description logics. In: Brewka, G., Eiter, T., McIlraith, S.A. (eds.) Proceedings of the 13th International Conference on Principles of Knowledge Representation and Reasoning (KR 2012), pp. 264–274. AAAI Press (2012)Google Scholar
  9. 9.
    Kazakov, Y., Krötzsch, M., Simančík, F.: Concurrent classification of el ontologies (2011) (to appear)Google Scholar
  10. 10.
    Kazakov, Y., Motik, B.: A resolution-based decision procedure for \(\mathcal{SHOIQ}\). In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 662–677. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  11. 11.
    Knorr, M., Alferes, J.J., Hitzler, P.: Local closed world reasoning with description logics under the well-founded semantics. Artif. Intell. 175(9-10), 1528–1554 (2011)MathSciNetzbMATHCrossRefGoogle Scholar
  12. 12.
    Knorr, M., Martínez, D.C., Hitzler, P., Krisnadhi, A.A., Maier, F., Wang, C.: Recent advances in integrating owl and rules (technical communication). In: Krötzsch, Straccia (eds.) [18], pp. 225–228Google Scholar
  13. 13.
    Krisnadhi, A., Hitzler, P.: A tableau algorithm for description logics with nominal schema. In: Krötzsch, Straccia (eds.) [18], pp. 234–237Google Scholar
  14. 14.
    Krisnadhi, A., Maier, F., Hitzler, P.: Owl and rules. In: Polleres, A., d’Amato, C., Arenas, M., Handschuh, S., Kroner, P., Ossowski, S., Patel-Schneider, P. (eds.) Reasoning Web 2011. LNCS, vol. 6848, pp. 382–415. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  15. 15.
    Krötzsch, M.: Efficient inferencing for OWL EL. In: Janhunen, T., Niemelä, I. (eds.) JELIA 2010. LNCS (LNAI), vol. 6341, pp. 234–246. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  16. 16.
    Krötzsch, M., Maier, F., Krisnadhi, A., Hitzler, P.: A better uncle for owl: nominal schemas for integrating rules and ontologies. In: Srinivasan, S., Ramamritham, K., Kumar, A., Ravindra, M.P., Bertino, E., Kumar, R. (eds.) WWW, pp. 645–654. ACM (2011)Google Scholar
  17. 17.
    Krötzsch, M., Rudolph, S., Hitzler, P.: ELP: Tractable rules for OWL 2. In: Sheth, A.P., Staab, S., Dean, M., Paolucci, M., Maynard, D., Finin, T., Thirunarayan, K. (eds.) ISWC 2008. LNCS, vol. 5318, pp. 649–664. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  18. 18.
    Krötzsch, M., Straccia, U. (eds.): RR 2012. LNCS, vol. 7497. Springer, Heidelberg (2012)zbMATHGoogle Scholar
  19. 19.
    Martinezi, D.C., Krisnadhi, A., Maier, F., Sengupta, K., Hitzler, P.: Reconciling owl and rules. Tech. rep. Kno.e.sis Center, Wright State University, Dayton, OH, U.S.A. (2011),
  20. 20.
    Motik, B.: Reasoning in Description Logics using Resolution and Deductive Databases. Ph.D. thesis, Universität Karlsruhe (TH), Karlsruhe, Germany (January 2006)Google Scholar
  21. 21.
    Motik, B., Sattler, U., Studer, R.: Query answering for owl-dl with rules. In: McIlraith, S.A., Plexousakis, D., van Harmelen, F. (eds.) ISWC 2004. LNCS, vol. 3298, pp. 549–563. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  22. 22.
    Motik, B., Shearer, R., Horrocks, I.: Hypertableau reasoning for description logics. J. Artif. Intell. Res. (JAIR) 36, 165–228 (2009)Google Scholar
  23. 23.
    Dal Palù, A., Dovier, A., Pontelli, E., Rossi, G.: Answer set programming with constraints using lazy grounding. In: Hill, P.M., Warren, D.S. (eds.) ICLP 2009. LNCS, vol. 5649, pp. 115–129. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  24. 24.
    Rudolph, S., Krötzsch, M., Hitzler, P.: Cheap boolean role constructors for description logics. In: Hölldobler, S., Lutz, C., Wansing, H. (eds.) JELIA 2008. LNCS (LNAI), vol. 5293, pp. 362–374. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  25. 25.
    Simancik, F., Kazakov, Y., Horrocks, I.: Consequence-based reasoning beyond horn ontologies. In: Walsh, T. (ed.) IJCAI, pp. 1093–1098. IJCAI/AAAI (2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Cong Wang
    • 1
  • Pascal Hitzler
    • 1
  1. 1.Kno.e.sis CenterWright State UniversityDaytonUSA

Personalised recommendations