{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:22:54Z","timestamp":1762100574218},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_53","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T11:44:21Z","timestamp":1160048661000},"page":"662-677","source":"Crossref","is-referenced-by-count":11,"title":["A Resolution-Based Decision Procedure for $\\mathcal{SHOIQ}$"],"prefix":"10.1007","author":[{"given":"Yevgeny","family":"Kazakov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Boris","family":"Motik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"53_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1007\/3-540-44802-0_36","volume-title":"Computer Science Logic","author":"A. Armando","year":"2001","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: Uniform Derivation of Decision Procedures by Superposition. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 549\u2013563. Springer, Heidelberg (2001)"},{"volume-title":"The Description Logic Handbook: Theory, Implementation and Applications","year":"2003","key":"53_CR2","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, Cambridge (2003)"},{"key":"53_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"53_CR4","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning, ch. 2","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution Theorem Proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 2, vol.\u00a01, pp. 19\u201399. Elsevier, Amsterdam (2001)"},{"issue":"2","key":"53_CR5","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic Paramodulation. Information and Computation\u00a0121(2), 172\u2013192 (1995)","journal-title":"Information and Computation"},{"key":"53_CR6","series-title":"Lecture Notes in Computer Science","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":"Ferm\u00fcller, C., Tammet, T., Zamov, N., Leitsch, A.: Resolution Methods for the Decision Problem. In: Ferm\u00fcller, C., Tammet, T., Leitsch, A., Zamov, N. (eds.) Resolution Methods for the Decision Problem. LNCS, vol.\u00a0679, Springer, Heidelberg (1993)"},{"key":"53_CR7","first-page":"295","volume-title":"Proc. LICS 1999","author":"H. Ganzinger","year":"1999","unstructured":"Ganzinger, H., de Nivelle, H.: A Superposition Decision Procedure for the Guarded Fragment with Equality. In: Proc. LICS 1999, Trento, Italy, July 2\u20135, 1999, pp. 295\u2013305. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"53_CR8","unstructured":"Haarslev, V., Timmann, M., M\u00f6ller, R.: Combining Tableaux and Algebraic Methods for Reasoning with Qualified Number Restrictions. In: Proc. DL 2001. CEUR Workshop Proceedings, Stanford, CA, USA, August 1\u20133, 2001, vol.\u00a049 (2001)"},{"key":"53_CR9","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A.: The Intractability of Resolution. Theorerical Computer Science\u00a039, 297\u2013308 (1985)","journal-title":"Theorerical Computer Science"},{"key":"53_CR10","first-page":"448","volume-title":"Proc. IJCAI 2005","author":"I. Horrocks","year":"2005","unstructured":"Horrocks, I., Sattler, U.: A Tableaux Decision Procedure for SHOIQ. In: Proc. IJCAI 2005, Edinburgh, UK, July 30\u2013August 5 2005, pp. 448\u2013453. Morgan Kaufmann, San Francisco (2005)"},{"key":"53_CR11","first-page":"152","volume-title":"Proc. KR 2004","author":"U. Hustadt","year":"2004","unstructured":"Hustadt, U., Motik, B., Sattler, U.: Reducing SHIQ Description Logic to Disjunctive Datalog Programs. In: Proc. KR 2004, Whistler, Canada, June 2\u20135, 2004, pp. 152\u2013162. AAAI Press, Menlo Park (2004)"},{"issue":"3","key":"53_CR12","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W.H. Joyner Jr.","year":"1976","unstructured":"Joyner Jr., W.H.: Resolution Strategies as Decision Procedures. Journal of the ACM\u00a023(3), 398\u2013417 (1976)","journal-title":"Journal of the ACM"},{"key":"53_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-25984-8_7","volume-title":"Automated Reasoning","author":"Y. Kazakov","year":"2004","unstructured":"Kazakov, Y., de Nivelle, H.: A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 122\u2013136. Springer, Heidelberg (2004)"},{"key":"53_CR14","unstructured":"Motik, B.: Reasoning in Description Logics using Resolution and Deductive Databases. PhD thesis, Univesit\u00e4t Karlsruhe, Germany (2006)"},{"issue":"4","key":"53_CR15","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. Nieuwenhuis","year":"1995","unstructured":"Nieuwenhuis, R., Rubio, A.: Theorem Proving with Ordering and Equality Constrained Clauses. Journal of Symbolic Computation\u00a019(4), 312\u2013351 (1995)","journal-title":"Journal of Symbolic Computation"},{"issue":"3","key":"53_CR16","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1093\/jigpal\/8.3.265","volume":"8","author":"H. Nivelle De","year":"2000","unstructured":"De Nivelle, H., Schmidt, R.A., Hustadt, U.: Resolution-Based Methods for Modal Logics. Logic Journal of the IGPL\u00a08(3), 265\u2013292 (2000)","journal-title":"Logic Journal of the IGPL"},{"key":"53_CR17","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/B978-044450813-3\/50008-4","volume-title":"Handbook of Automated Reasoning, ch. 6","author":"A. Nonnengart","year":"2001","unstructured":"Nonnengart, A., Weidenbach, C.: Computing Small Clause Normal Forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 6, vol.\u00a0I, pp. 335\u2013367. Elsevier, Amsterdam (2001)"},{"issue":"4","key":"53_CR18","doi-asserted-by":"publisher","first-page":"1083","DOI":"10.1137\/S0097539797323005","volume":"29","author":"L. Pacholski","year":"2000","unstructured":"Pacholski, L., Szwast, W., Tendera, L.: Complexity Results for First-Order Two-Variable Logic with Counting. SIAM Journal on Computing\u00a029(4), 1083\u20131117 (2000)","journal-title":"SIAM Journal on Computing"},{"issue":"3","key":"53_CR19","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/s10849-005-5791-1","volume":"14","author":"I. Pratt-Hartmann","year":"2005","unstructured":"Pratt-Hartmann, I.: Complexity of the Two-Variable Fragment with Counting Quantifiers. Journal of Logic, Language and Information\u00a014(3), 369\u2013395 (2005)","journal-title":"Journal of Logic, Language and Information"},{"key":"53_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-540-45085-6_36","volume-title":"Automated Deduction \u2013 CADE-19","author":"R.A. Schmidt","year":"2003","unstructured":"Schmidt, R.A., Hustadt, U.: A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 412\u2013426. Springer, Heidelberg (2003)"},{"key":"53_CR21","unstructured":"Tobies, S.: Complexity Results and Practical Algorithms for Logics in Knowledge Representation. PhD thesis, RWTH Aachen, Germany (2001)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_53.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:27:37Z","timestamp":1619494057000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/11814771_53","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}