{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T12:23:38Z","timestamp":1742387018030},"reference-count":18,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9780387298153"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-0-387-34347-1_13","type":"book-chapter","created":{"date-parts":[[2006,9,27]],"date-time":"2006-09-27T06:16:35Z","timestamp":1159337795000},"page":"189-204","source":"Crossref","is-referenced-by-count":1,"title":["Resolution Based Explanations for Reasoning in the Description Logic ALC"],"prefix":"10.1007","author":[{"given":"Xi","family":"Deng","sequence":"first","affiliation":[]},{"given":"Volker","family":"Haarslev","sequence":"additional","affiliation":[]},{"given":"Nematollaah","family":"Shiri","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"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\u201344"},{"key":"13_CR2","first-page":"401","volume-title":"Principles of semantic networks","author":"R.J. Brachman","year":"1990","unstructured":"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\u2013456"},{"key":"13_CR3","first-page":"5","volume-title":"The Description Logic Handbook: Theory, Implementation, and Applications","author":"F. Baader","year":"2003","unstructured":"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\u201344"},{"key":"13_CR4","first-page":"55","volume-title":"Proceedings of the AAAI Fall Symposium on Explanation-aware Computing","author":"X. Deng","year":"2005","unstructured":"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\u201361"},{"issue":"1","key":"13_CR5","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0747-7171(02)00092-5","volume":"35","author":"H. Nivelle De","year":"2003","unstructured":"De Nivelle H, De Rijke M (2003) Deciding the guarded fragments by resolution. J Symbolic Computation 35(1):21\u201358","journal-title":"J Symbolic Computation"},{"key":"13_CR6","volume-title":"Completeness, confluence, and related properties of clause graph resolution","author":"N. Eisinger","year":"1991","unstructured":"Eisinger N (1991) Completeness, confluence, and related properties of clause graph resolution. Morgan Kaufmann San Francisco, US"},{"key":"13_CR7","first-page":"701","volume-title":"Proceedings of International Joint Conference on Automated Reasoning (IJCAR)","author":"V. Haarslev","year":"2001","unstructured":"Haarslev V, M\u00f6ller 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\u2013705"},{"key":"13_CR8","first-page":"466","volume-title":"Proceedings of Nineteenth International Joint Conference on Artificial Intelligence (IJCAI)","author":"U. Hustadt","year":"2005","unstructured":"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\u2013471"},{"key":"13_CR9","first-page":"191","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"U. Hustadt","year":"1999","unstructured":"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\u2013205"},{"key":"13_CR10","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/3-540-69778-0_30","volume-title":"Automated Resoning with Analytic Tableaux and Related Methods: International Con ference Tableaux","author":"I. Horrocks","year":"1998","unstructured":"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\u2013312"},{"key":"13_CR11","doi-asserted-by":"crossref","first-page":"738","DOI":"10.1007\/3-540-58156-1_53","volume-title":"Proceedings of 12th Conference on Automated Deduction","author":"X. Huang","year":"1994","unstructured":"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\u2013752"},{"key":"13_CR12","unstructured":"Lingenfelder C (1996) Transformation and structuring of computer generatedproofs. Ph.D. thesis, University of Kaiserslautern"},{"key":"13_CR13","first-page":"816","volume-title":"Proceedings of the tenth International Joint Conference on Artificial Intelligence (IJCAI)","author":"D.L. McGuinness","year":"1995","unstructured":"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\u2013821"},{"key":"13_CR14","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/10721959_37","volume-title":"Proceedings of the 17th Conference on Automated Deduction (CADE)","author":"A. Meier","year":"2000","unstructured":"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\u2013464"},{"key":"13_CR15","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/BFb0054274","volume-title":"Proceedings of the 15th International Conference on Automated Deduction","author":"A. Nonnengart","year":"1998","unstructured":"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\u2013411"},{"key":"13_CR16","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1145\/1060745.1060837","volume-title":"The 14th Interntional World Wide Web Conference (WWW)","author":"B. Parsia","year":"2005","unstructured":"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\u2013640"},{"key":"13_CR17","first-page":"355","volume-title":"Proceedings of the eight eenth International Joint Conference on Artificial Intelligence (IJCAI)","author":"S. Schlobach","year":"2003","unstructured":"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\u2013362"},{"issue":"2","key":"13_CR18","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1023\/A:1005843632307","volume":"18","author":"M. WosMcCune","year":"1997","unstructured":"WosMcCune M and Wos L (1997) Otter-the CADE-13 competition in-carnations. J Automated Reasoning 18(2):211\u2013220","journal-title":"J Automated Reasoning"}],"container-title":["Semantic Web and Beyond","Canadian Semantic Web"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-0-387-34347-1_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:48:09Z","timestamp":1619560089000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-0-387-34347-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9780387298153"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-0-387-34347-1_13","relation":{},"subject":[]}}