{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T06:56:02Z","timestamp":1761807362843},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540671909"},{"type":"electronic","value":"9783540465089"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46508-1_13","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T16:02:03Z","timestamp":1186156923000},"page":"191-205","source":"Crossref","is-referenced-by-count":27,"title":["Issues of Decidability for Description Logics in the Framework of Resolution"],"prefix":"10.1007","author":[{"given":"Ullrich","family":"Hustadt","sequence":"first","affiliation":[]},{"given":"Renate A.","family":"Schmidt","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"issue":"2","key":"13_CR1","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/BF00872105","volume":"4","author":"F. Baader","year":"1994","unstructured":"F. Baader, B. Hollunder, B. Nebel, H.-J. Profitlich, and E. Franconi. An empirical analysis of optimization techniques for terminological representation systems or \u201cmaking KRIS get a move on\u201d. Applied Intelligence, 4(2):109\u2013132, 1994.","journal-title":"Applied Intelligence"},{"doi-asserted-by":"crossref","unstructured":"M. Baaz, C. Ferm\u00fcller, and A. Leitsch. A non-elementary speed-up in proof length by structural clause form transformation. In Proc. LICS\u201994, pages 213\u2013219. IEEE Computer Society Press, 1994.","key":"13_CR2","DOI":"10.1109\/LICS.1994.316070"},{"key":"13_CR3","series-title":"Research report","volume-title":"Ordered chaining calculi for first-order theories of binary relations","author":"L. Bachmair","year":"1995","unstructured":"L. Bachmair and H. Ganzinger. Ordered chaining calculi for first-order theories of binary relations. Research report MPI-I-95-2-009, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany, 1995. To appear in J. ACM."},{"key":"13_CR4","series-title":"Research report","volume-title":"A theory of resolution","author":"L. Bachmair","year":"1997","unstructured":"L. Bachmair and H. Ganzinger. A theory of resolution. Research report MPI-I-97-2-005, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany, 1997. To appear in J. A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning."},{"doi-asserted-by":"crossref","unstructured":"H. de Nivelle. A resolution decision procedure for the guarded fragment. In Proc. CADE-15, LNAI 1421, pages 191\u2013204. Springer, 1998.","key":"13_CR5","DOI":"10.1007\/BFb0054260"},{"key":"13_CR6","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1093\/logcom\/4.4.423","volume":"4","author":"F. M. Donini","year":"1994","unstructured":"F. M. Donini, M. Lenzerini, D. Nardi, and A. Schaerf. Deduction in concept languages: From subsumption to instance checking. J. Logic and Computation, 4:423\u2013452, 1994.","journal-title":"J. Logic and Computation"},{"key":"13_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-56732-1","volume-title":"Resolution Method for the Decicion Problem","author":"C. Ferm\u00fcller","year":"1993","unstructured":"C. Ferm\u00fcller, A. Leitsch, T. Tammet, and N. Zamov. Resolution Method for the Decicion Problem. LNCS 679. Springer, 1993."},{"unstructured":"H. Ganzinger, U. Hustadt, C. Meyer, and R. A. Schmidt. A resolution-based decision procedure for extensions of K4. To appear in Advances in Modal Logic, Volume 2. CSLI Publications, 1999.","key":"13_CR8"},{"issue":"2","key":"13_CR9","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1305\/ndjfl\/1040046086","volume":"37","author":"E. Hemaspaandra","year":"1996","unstructured":"E. Hemaspaandra. The price of universality. Notre Dame J. Formal Logic, 37(2):174\u2013203, 1996.","journal-title":"Notre Dame J. Formal Logic"},{"key":"13_CR10","volume-title":"Optimising Tableaux Decision Procedures for Description Logics","author":"I. Horrocks","year":"1997","unstructured":"I. Horrocks. Optimising Tableaux Decision Procedures for Description Logics. PhD thesis, University of Manchester, Manchester, UK, 1997."},{"unstructured":"U. Hustadt and R. A. Schmidt. On evaluating decision procedures for modal logic. In Proc. IJCAI\u201997, pages 202\u2013207. Morgan Kaufmann, 1997.","key":"13_CR11"},{"issue":"3","key":"13_CR12","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W. H. Joyner Jr.","year":"1976","unstructured":"W. H. Joyner Jr. Resolution strategies as decision procedures. J. ACM, 23(3):398\u2013417, 1976.","journal-title":"J. ACM"},{"key":"13_CR13","first-page":"269","volume":"1","author":"B. Kallick","year":"1968","unstructured":"B. Kallick. A decision procedure based on the resolution method. In Information Processing 68, Volume 1, pages 269\u2013275. North-Holland, 1968.","journal-title":"Information Processing 68"},{"key":"13_CR14","first-page":"141","volume":"1","author":"M. Marx","year":"1996","unstructured":"M. Marx. Mosaics and cylindric modal logic of dimension 2. In Advances in Modal Logic, Volume 1, Lecture Notes 87, pages 141\u2013156. CSLI Publications, 1996.","journal-title":"Advances in Modal Logic"},{"key":"13_CR15","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1023\/A:1005866922570","volume":"20","author":"M. Paramasivam","year":"1998","unstructured":"M. Paramasivam and D. A. Plaisted. Automated deduction techniques for classification in description logic systems. J. Automated Reasoning, 20:337\u2013364, 1998.","journal-title":"J. Automated Reasoning"},{"key":"13_CR16","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. A. Plaisted","year":"1986","unstructured":"D. A. Plaisted and S. Greenbaum. A structure-preserving clause form translation. J. Symbolic Computation, 2:293\u2013304, 1986.","journal-title":"J. Symbolic Computation"},{"unstructured":"R. A. Schmidt. Decidability by resolution for propositional modal logics. To appear in J. Automated Reasoning.","key":"13_CR17"},{"key":"13_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(91)90078-X","volume":"48","author":"M. Schmidt-Schau\u00df","year":"1991","unstructured":"M. Schmidt-Schau\u00df and G. Smolka. Attributive concept description with complements. Artifical Intelligence, 48:1\u201326, 1991.","journal-title":"Artifical Intelligence"},{"doi-asserted-by":"crossref","unstructured":"T. Tammet. Using resolution for extending KL-ONE-type languages. In Proc. CIKM\u201995, 1995.","key":"13_CR19","DOI":"10.1145\/221270.221605"},{"issue":"4","key":"13_CR20","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A. Urquhart","year":"1995","unstructured":"A. Urquhart. The complexity of propositional proofs. Bull. Symbolic Logic, 1(4):425\u2013467, 1995.","journal-title":"Bull. Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Classical and Non-Classical Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46508-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,20]],"date-time":"2019-02-20T15:52:22Z","timestamp":1550677942000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46508-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671909","9783540465089"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-46508-1_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}