{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,4]],"date-time":"2026-03-04T06:50:24Z","timestamp":1772607024524,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540735946","type":"print"},{"value":"9783540735953","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_6","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"67-83","source":"Crossref","is-referenced-by-count":41,"title":["Optimized Reasoning in Description Logics Using Hypertableaux"],"prefix":"10.1007","author":[{"given":"Boris","family":"Motik","sequence":"first","affiliation":[]},{"given":"Rob","family":"Shearer","sequence":"additional","affiliation":[]},{"given":"Ian","family":"Horrocks","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1-2","key":"6_CR1","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1016\/S0004-3702(96)00010-0","volume":"88","author":"F. Baader","year":"1996","unstructured":"Baader, F., Buchheit, M., Hollunder, B.: Cardinality Restrictions on Concepts. Artificial Intelligence\u00a088(1-2), 195\u2013213 (1996)","journal-title":"Artificial Intelligence"},{"key":"6_CR2","volume-title":"The Description Logic Handbook","author":"F. Baader","year":"2003","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F.: The Description Logic Handbook. Cambridge University Press, Cambridge (2003)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Logics in Artificial Intelligence","author":"P. Baumgartner","year":"1996","unstructured":"Baumgartner, P., Furbach, U., Niemel\u00e4, I.: Hyper Tableaux. In: Or\u0142owska, E., Alferes, J.J., Moniz Pereira, L. (eds.) JELIA 1996. LNCS, vol.\u00a01126, pp. 1\u201317. Springer, Heidelberg (1996)"},{"issue":"1","key":"6_CR4","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0004-3702(00)00070-9","volume":"124","author":"F.M. Donini","year":"2000","unstructured":"Donini, F.M., Massacci, F.: EXPTIME tableaux for ALC. Artificial Intelligence\u00a0124(1), 87\u2013138 (2000)","journal-title":"Artificial Intelligence"},{"key":"6_CR5","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. LNCS, vol.\u00a0679. Springer, Heidelberg (1993)"},{"key":"6_CR6","doi-asserted-by":"publisher","first-page":"1791","DOI":"10.1016\/B978-044450813-3\/50027-8","volume-title":"Handbook of Automated Reasoning, ch. 25","author":"C.G. Ferm\u00fcller","year":"2001","unstructured":"Ferm\u00fcller, C.G., Leitsch, A., Hustadt, U., Tammet, T.: Resolution Decision Procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 25, vol.\u00a0II, pp. 1791\u20131849. Elsevier, Amsterdam (2001)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"TABLEAUX 2007","author":"R.P. Gor\u00e9","year":"2007","unstructured":"Gor\u00e9, R.P., Nguyen, L.: EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS, vol.\u00a04548, Springer, Heidelberg (2007)"},{"key":"6_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/3-540-45744-5_59","volume-title":"Automated Reasoning","author":"V. Haarslev","year":"2001","unstructured":"Haarslev, V., M\u00f6ller, R.: RACER System Description. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 701\u2013706. Springer, Heidelberg (2001)"},{"issue":"3","key":"6_CR9","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1093\/logcom\/9.3.385","volume":"9","author":"I. Horrocks","year":"1999","unstructured":"Horrocks, I., Sattler, U.: A Description Logic with Transitive and Inverse Roles and Role Hierarchies. Journal of Logic and Computation\u00a09(3), 385\u2013410 (1999)","journal-title":"Journal of Logic and Computation"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/10721959_39","volume-title":"Automated Deduction - CADE-17","author":"I. Horrocks","year":"2000","unstructured":"Horrocks, I., Sattler, U., Tobies, S.: Reasoning with Individuals for the Description Logic SHIQ. In: McAllester, D. (ed.) Automated Deduction - CADE-17. LNCS, vol.\u00a01831, pp. 482\u2013496. Springer, Heidelberg (2000)"},{"key":"6_CR11","unstructured":"Hudek, A.K., Weddell, G.: Binary Absorption in Tableaux-Based Reasoning for Description Logics. In: Proc. DL, Windermere, UK (May 30-June 1, 2006)"},{"key":"6_CR12","unstructured":"Hustadt, U., Motik, B., Sattler, U.: Data Complexity of Reasoning in Very Expressive Description Logics. In: Proc. IJCAI 2005, pp. 466\u2013471, Edinburgh, UK (July 30-August 5, 2005)"},{"key":"6_CR13","unstructured":"Kr\u00f6tzsch, M., Rudolph, S., Hitzler, P.: Complexity Boundaries for Horn Description Logics. In: Proc. AAAI 2007, Vancouver, BC, Canada, July 22-26, 2007, AAAI Press (to appear)"},{"key":"6_CR14","unstructured":"Motik, B.: Reasoning in Description Logics using Resolution and Deductive Databases. PhD thesis, Universit\u00e4t Karlsruhe, Germany (2006)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"The Semantic Web \u2013 ISWC 2004","author":"B. Parsia","year":"2004","unstructured":"Parsia, B., Sirin, E.: Pellet: An OWL-DL Reasoner. In: McIlraith, S.A., Plexousakis, D., van Harmelen, F. (eds.) ISWC 2004. LNCS, vol.\u00a03298, Springer, Heidelberg (2004)"},{"issue":"3","key":"6_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":"Plaisted, D.A., Greenbaum, S.: A Structure-Preserving Clause Form Translation. Journal of Symbolic Logic and Computation\u00a02(3), 293\u2013304 (1986)","journal-title":"Journal of Symbolic Logic and Computation"},{"key":"6_CR17","first-page":"227","volume":"1","author":"A. Robinson","year":"1965","unstructured":"Robinson, A.: Automatic Deduction with Hyper-Resolution. Int. Journal of Computer Mathematics\u00a01, 227\u2013234 (1965)","journal-title":"Int. Journal of Computer Mathematics"},{"key":"6_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","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.) Automated Deduction \u2013 CADE-19. LNCS (LNAI), vol.\u00a02741, pp. 412\u2013426. Springer, Heidelberg (2003)"},{"key":"6_CR19","unstructured":"Tobies, S.: Complexity Results and Practical Algorithms for Logics in Knowledge Representation. PhD thesis, RWTH Aachen, Germany (2001)"},{"key":"6_CR20","unstructured":"Tsarkov, D., Horrocks, I.: Efficient Reasoning with Range and Domain Constraints. In: Proc. DL 2004, Whistler, BC, Canada (June 6-8, 2004)"},{"key":"6_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/11814771_26","volume-title":"Automated Reasoning","author":"D. Tsarkov","year":"2006","unstructured":"Tsarkov, D., Horrocks, I.: FaCT++ Description Logic Reasoner: System Description. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 292\u2013297. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:53:12Z","timestamp":1619517192000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}