Abstract
With the increasing number of applications of description logics (DLs), unsatisfiable concepts and inconsistent terminologies become quite common, especially when the knowledge bases are large and complex. Even for an experienced knowledge engineer, it can be extremely difficult to identify and resolve the origins of these unsatisfiabilities and inconsistencies. Thus it is crucial to provide services to explain how and why a result is derived. Motivated by the possibilities of applying resolution technique in first-order logic to construct explanations for description logics, we extend our previous work and present an algorithm that generates explanations for unsatisfiability and inconsistency reasoning in the description language ALC. The main advantage of our approach is that it is independent of any specific DL reasoners.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Borgida A, Franconi E, Horrocks I, McGuiness DL and Patel-Schneider PF (1999) Explaining ALC subsumption. In Proceedings of 1999 International Workshop on Description Logics. CEUR-WS.org, pp 37–44
Brachman RJ, McGuiness DL, Patel-Schneider PF, Resnick LA (1990) Living with CLASSIC: when and how to use a KL-ONE-like language. In Sowa J (ed) Principles of semantic networks. Morgan Kaufmann, San Mateo, US, pp 401–456
Baader F, Nutt W (2003) Basic description logic. In Baader F, Calvanese D, McGuinness DL, Nardi D, and Patel-Schneider PF (eds) The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge, pp 5–44
Deng X, Haarslev V, Shiri N (2005) A framework for explaining reasoning in description logics. In Proceedings of the AAAI Fall Symposium on Explanation-aware Computing. AAAI Press, Menlo Park, US, pp 55–61
De Nivelle H, De Rijke M (2003) Deciding the guarded fragments by resolution. J Symbolic Computation 35(1):21–58
Eisinger N (1991) Completeness, confluence, and related properties of clause graph resolution. Morgan Kaufmann San Francisco, US
Haarslev V, Möller R (2001) Racer system description. In T Nipkow R Gori, A Leitsch (eds) Proceedings of International Joint Conference on Automated Reasoning (IJCAR). Springer-Verlag, London, UK, pp 701–705
Hustadt U, Motik B, Sattler U (2005) Data complexity of reasoning in very expressive description logics. In Proceedings of Nineteenth International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, San Francisco, US, pp 466–471
Hustadt U, Schmidt RA (1999) Issues of decidability for description logics in the framework of resolution. In Caferra R and Salzer G (eds) Automated Deduction in Classical and Non-Classical Logics. Springer-Verlag, London, UK, pp 191–205
Horrocks I (1998) The FaCT system. In De Swart H (ed) Automated Resoning with Analytic Tableaux and Related Methods: International Con ference Tableaux. Springer-Verlag, Berlin, Germany, pp 307–312
Huang X (1994) Reconstructing proofs at the assertion level. In Bundy A (ed) Proceedings of 12th Conference on Automated Deduction. Springer-Verlag, London, UK, pp 738–752
Lingenfelder C (1996) Transformation and structuring of computer generatedproofs. Ph.D. thesis, University of Kaiserslautern
McGuinness DL and Borgida A (1995) Explaining subsumption in description logics. In Proceedings of the tenth International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, San Francisco, US, pp 816–821
Meier A (2000) TRAMP: Transformation of machine-found proofs into natural deduction proofs at the assertion level. In McAllester D (ed) Proceedings of the 17th Conference on Automated Deduction (CADE). Springer-Verlag, Berlin, Germany, pp 460–464
Nonnengart A, Rock G, Weidenbach C (1998) On generating small clause normal forms. In Kirchner C and Kirchner H (eds) Proceedings of the 15th International Conference on Automated Deduction. Springer-Verlag, London, UK, pp 397–411
Parsia B, Sirin E, Kalyanpur A (2005) Debugging OWL ontologies. In The 14th Interntional World Wide Web Conference (WWW). ACM Press, New York, US, pp 633–640
Schlobach S and Cornet R (2003) Non-standard reasoning services for the debugging of description logic terminologies. In Proceedings of the eight eenth International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, San Francisco, US, pp 355–362
WosMcCune M and Wos L (1997) Otter-the CADE-13 competition in-carnations. J Automated Reasoning 18(2):211–220
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer Science+Business Media, LLC
About this paper
Cite this paper
Deng, X., Haarslev, V., Shiri, N. (2006). Resolution Based Explanations for Reasoning in the Description Logic ALC . In: Koné, M.T., Lemire, D. (eds) Canadian Semantic Web. Semantic Web and Beyond, vol 2. Springer, Boston, MA . https://doi.org/10.1007/978-0-387-34347-1_13
Download citation
DOI: https://doi.org/10.1007/978-0-387-34347-1_13
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-29815-3
Online ISBN: 978-0-387-34347-1
eBook Packages: Computer ScienceComputer Science (R0)