{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:04:37Z","timestamp":1747544677646},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_13","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T20:53:07Z","timestamp":1194641587000},"page":"187-201","source":"Crossref","is-referenced-by-count":4,"title":["Prefixed Resolution: A Resolution Method for Modal and Description Logics"],"prefix":"10.1007","author":[{"given":"Carlos","family":"Areces","sequence":"first","affiliation":[]},{"given":"Hans","family":"de Nivelle","sequence":"additional","affiliation":[]},{"given":"Maarten","family":"de Rijke","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"issue":"1","key":"13_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00302639","volume":"6","author":"Y. Auffray","year":"1990","unstructured":"Y. Auffray, P. Enjalbert, and J. Hebrard. Strategies for modal resolution: results and problems. Journal of Automated Reasoning, 6(1):1\u201338, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR2","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. Profitlich, and E. Franconi. An empirical analysis of optimization techniques for terminological representation systems or: Making KRIS get a move on. Journal of Applied Intelligence, 4:109\u2013132, 1994.","journal-title":"Journal of Applied Intelligence"},{"key":"13_CR3","unstructured":"P. Blackburn. Internalizing labeled deduction. Technical Report CLAUS-Report 102, Computerlinguistik, Universit\u00e4t des Saarlandes, 1998."},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1023\/A:1018988913388","volume":"24","author":"P. Blackburn","year":"1998","unstructured":"P. Blackburn and M. Tzakova. Hybridizing concept languages. Annals of Mathematics and Artificial Intelligence, 24:23\u201349, 1998.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"13_CR5","unstructured":"R. Brachman and H. Levesque. The tractability of subsumption in frame-based description languages. In AAAI-84, pages 34\u201337, 1984."},{"issue":"2","key":"13_CR6","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0364-0213(85)80014-8","volume":"9","author":"R. Brachman","year":"1985","unstructured":"R. Brachman and J. Schmolze. An overview of the KL-ONE knowledge representation system. Cognitive Science, 9(2):171\u2013216, 1985.","journal-title":"Cognitive Science"},{"key":"13_CR7","unstructured":"D. Calvanese, G. De Giacomo, and M. Lenzerini. Conjunctive query containment in description logics with n-ary relations. In Proc. of DL-97, pages 5\u20139, June 1997."},{"key":"13_CR8","volume-title":"Ordering refinements of resolution","author":"H. Nivelle de","year":"1994","unstructured":"H. de Nivelle. Ordering refinements of resolution. PhD thesis, Technische Universiteit Delft, Delft. The Netherlands, October 1994."},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"H. de Nivelle and M. de Rijke. Resolution decides the guarded fragment. Submitted for journal publication, 1998.","DOI":"10.1007\/BFb0054260"},{"key":"13_CR10","unstructured":"M. de Rijke. Restricted description languages. Unpublished, 1998."},{"issue":"4","key":"13_CR11","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1093\/logcom\/4.4.423","volume":"4","author":"F. Donini","year":"1994","unstructured":"F. Donini, M. Lenzerini, D. Nardi, and A. Schaerf. Deduction in concept languages: from subsumption to instance checking. Journal of Logic and Computation, 4(4):423\u2013452, 1994.","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"13_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(89)90137-0","volume":"65","author":"P. Enjalbert","year":"1989","unstructured":"P. Enjalbert and L. Fari\u00f1as del Cerro. Modal resolution in clausal form. Theoretical Computer Science, 65(1):1\u201333, 1989.","journal-title":"Theoretical Computer Science"},{"key":"13_CR13","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0020-0190(82)90085-0","volume":"14","author":"L. Fari\u00f1as del Cerro","year":"1982","unstructured":"L. Fari\u00f1as del Cerro. A simple deduction method for modal logic. Information Processing Letters, 14:49\u201351, April 1982.","journal-title":"Information Processing Letters"},{"key":"13_CR14","series-title":"LNAI","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-56732-1","volume-title":"Resolution methods for the decision problem","author":"C. Ferm\u00fcller","year":"1993","unstructured":"C. Ferm\u00fcller, A. Leitsch, T. Tammet, and N. Zamov. Resolution methods for the decision problem. Springer-Verlag, Berlin, 1993. LNAI."},{"key":"13_CR15","unstructured":"I. Horrocks and P. Patel-Schneider. Optimising description logic subsumption. Submitted to the Journal of Logic and Computation, 1998."},{"key":"13_CR16","unstructured":"U. Hustadt and R. Schmidt. Issues of decidability for description logics. Unpublished, 1998."},{"key":"13_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1090\/trans2\/143\/01","volume":"143","author":"G. Mints","year":"1989","unstructured":"G. Mints. Resolution calculi for modal logics. American Mathematical Society Translations, 143:1\u201314, 1989.","journal-title":"American Mathematical Society Translations"},{"key":"13_CR18","unstructured":"K. Schild. A correspondence theory for terminological logics. In Proc. of the 12th IJCAI, pages 466\u2013471, 1991."},{"key":"13_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(91)90078-X","volume":"48","author":"M. Schmidt-Schauss","year":"1991","unstructured":"M. Schmidt-Schauss and G. Smolka. Attributive concept descriptions with complements. Artificial Intelligence, 48:1\u201326, 1991.","journal-title":"Artificial Intelligence"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"T. Tammet. Using resolution for extending KL-ONE-type languages. In Proc. of the 4th CIKM. ACM Press, November 1995.","DOI":"10.1145\/221270.221605"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,28]],"date-time":"2020-04-28T00:30:47Z","timestamp":1588033847000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}