{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:33Z","timestamp":1761611193691},"publisher-location":"Berlin, Heidelberg","reference-count":53,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676973"},{"type":"electronic","value":"9783540450085"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722086_1","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T19:43:15Z","timestamp":1167421395000},"page":"1-18","source":"Crossref","is-referenced-by-count":22,"title":["Tableau Algorithms for Description Logics"],"prefix":"10.1007","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ulrike","family":"Sattler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Baader, F.: Augmenting concept languages by transitive closure of roles: An alternative to terminological cycles. In: Proc. of IJCAI 1991, Sydney, Australia (1991)"},{"issue":"1-2","key":"1_CR2","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":"1_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01051766","volume":"2","author":"F. Baader","year":"1993","unstructured":"Baader, F., B\u00fcrckert, H.-J., Nebel, B., Nutt, W., Smolka, G.: On the expressivity of feature logics with negation, functional uncertainty, and sort equations. J. of Logic, Language and Information\u00a02, 1\u201318 (1993)","journal-title":"J. of Logic, Language and Information"},{"key":"1_CR4","unstructured":"Baader, F., Hanschke, P.: A schema for integrating concrete domains into concept languages. Technical Report RR-91-10, DFKI, Kaiserslautern, Germany, An abridged version appeared in Proc. of IJCAI 1991 (1991)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/BFb0013522","volume-title":"Processing Declarative Knowledge","author":"F. Baader","year":"1991","unstructured":"Baader, F., Hollunder, B.: A terminological knowledge representation system with complete inference algorithm. In: Boley, H., Richter, M.M. (eds.) PDK 1991. LNCS, vol.\u00a0567, pp. 67\u201386. Springer, Heidelberg (1991)"},{"key":"1_CR6","first-page":"270","volume-title":"Proc. of KR 1992","author":"F. Baader","year":"1992","unstructured":"Baader, F., Hollunder, B., Nebel, B., Profitlich, H.-J., Franconi, E.: An empirical analysis of optimization techniques for terminological representation systems. In: Proc. of KR 1992, pp. 270\u2013281. Morgan Kaufmann, San Francisco (1992)"},{"issue":"3","key":"1_CR7","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1093\/logcom\/9.3.319","volume":"9","author":"F. Baader","year":"1999","unstructured":"Baader, F., Sattler, U.: Expressive number restrictions in description logics. J. of Logic and Computation\u00a09(3), 319\u2013350 (1999)","journal-title":"J. of Logic and Computation"},{"key":"1_CR8","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1613\/jair.56","volume":"1","author":"A. Borgida","year":"1994","unstructured":"Borgida, A., Patel-Schneider, P.F.: A semantics and complete algorithm for subsumption in the CLASSIC description logic. J. of Artificial Intelligence Research\u00a01, 277\u2013308 (1994)","journal-title":"J. of Artificial Intelligence Research"},{"key":"1_CR9","first-page":"247","volume-title":"Proc. of KR 1992","author":"R.J. Brachman","year":"1992","unstructured":"Brachman, R.J.: Reducing CLASSIC to practice: Knowledge representation meets reality. In: Proc. of KR 1992, pp. 247\u2013258. Morgan Kaufmann, San Francisco (1992)"},{"key":"1_CR10","unstructured":"Brachman, R.J., Levesque, H.J.: The tractability of subsumption in frame-based description languages. In: Proc. of AAAI 1984, pp. 34\u201337 (1984)"},{"volume-title":"Readings in Knowledge Representation","year":"1985","key":"1_CR11","unstructured":"Brachman, R.J., Levesque, H.J. (eds.): Readings in Knowledge Representation. Morgan Kaufmann, San Francisco (1985)"},{"issue":"2","key":"1_CR12","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1207\/s15516709cog0902_1","volume":"9","author":"R.J. Brachman","year":"1985","unstructured":"Brachman, R.J., Schmolze, J.G.: An overview of the KL-ONE knowledge representation system. Cognitive Science\u00a09(2), 171\u2013216 (1985)","journal-title":"Cognitive Science"},{"key":"1_CR13","unstructured":"Bresciani, P., Franconi, E., Tessaris, S.: Implementing and testing expressive description logics: Preliminary report. Working Notes of the 1995 Description Logics Workshop, Technical Report, RAP 07.95, Dip. di Inf. e Sist., Univ. di Roma La Sapienza\", pp. 131\u2013139, Rome, Italy (1995)"},{"key":"1_CR14","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1613\/jair.21","volume":"1","author":"M. Buchheit","year":"1993","unstructured":"Buchheit, M., Donini, F.M., Schaerf, A.: Decidable reasoning in terminological knowledge representation systems. J. of Artificial Intelligence Research\u00a01, 109\u2013138 (1993)","journal-title":"J. of Artificial Intelligence Research"},{"key":"1_CR15","unstructured":"Giacomo, G.D.: Decidability of Class-Based Knowledge Representation Formalisms. PhD thesis, Dip. di Inf. e Sist., Univ. di Roma La Sapienza (1995)"},{"key":"1_CR16","unstructured":"De Giacomo, G., Lenzerini, M.: Boosting the correspondence between description logics and propositional dynamic logics. In: Proc. of AAAI 1994, pp. 205\u2013212. AAAI Press\/The MIT Press (1994)"},{"key":"1_CR17","first-page":"411","volume-title":"Proc. of ECAI 1994","author":"G. Giacomo De","year":"1994","unstructured":"De Giacomo, G., Lenzerini, M.: Concept language with number restrictions and fixpoints, and its relationship with \u03bc-calculus. In: Cohn, A.G. (ed.) Proc. of ECAI 1994, pp. 411\u2013415. John Wiley & Sons, Chichester (1994)"},{"key":"1_CR18","first-page":"316","volume-title":"Proc. of KR 1996","author":"G. Giacomo De","year":"1996","unstructured":"De Giacomo, G., Lenzerini, M.: TBox and ABox reasoning in expressive description logics. In: Aiello, L.C., Doyle, J., Shapiro, S.C. (eds.) Proc. of KR 1996, pp. 316\u2013327. Morgan Kaufmann, San Francisco (1996)"},{"key":"1_CR19","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/0004-3702(92)90076-A","volume":"2-3","author":"F.M. Donini","year":"1992","unstructured":"Donini, F.M., Hollunder, B., Lenzerini, M., Spaccamela, A.M., Nardi, D., Nutt, W.: The complexity of existential quanti fication in concept languages. Artificial Intelligence\u00a02-3, 309\u2013327 (1992)","journal-title":"Artificial Intelligence"},{"key":"1_CR20","first-page":"151","volume-title":"Proc. of KR 1991","author":"F.M. Donini","year":"1991","unstructured":"Donini, F.M., Lenzerini, M., Nardi, D., Nutt, W.: The complexity of concept languages. In: Allen, J., Fikes, R., Sandewall, E. (eds.) Proc. of KR 1991, pp. 151\u2013162. Morgan Kaufmann, San Francisco (1991)"},{"key":"1_CR21","unstructured":"Donini, F.M., Lenzerini, M., Nardi, D., Nutt, W.: Tractable concept languages. In: Proc. of IJCAI 1991, Sydney, pp. 458\u2013463 (1991)"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Giacomo, G.D., Massacci, F.: Tableaux and algorithms for propositional dynamic logic with converse. In: Proc. of CADE 1996, pp. 613\u2013628 (1996)","DOI":"10.1007\/3-540-61511-3_117"},{"key":"1_CR23","first-page":"318","volume-title":"Proc. of KR 1992","author":"P. Hanschke","year":"1992","unstructured":"Hanschke, P.: Specifying role interaction in concept languages. In: Proc. of KR 1992, pp. 318\u2013329. Morgan Kaufmann, San Francisco (1992)"},{"key":"1_CR24","series-title":"Informatik-Fachberichte","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/978-3-642-76071-6_5","volume-title":"Proc. of GWAI 1990","author":"B. Hollunder","year":"1990","unstructured":"Hollunder, B.: Hybrid inferences in KL-ONE-based knowledge representation systems. In: Proc. of GWAI 1990. Informatik-Fachberichte, vol.\u00a0251, pp. 38\u201347. Springer, Heidelberg (1990)"},{"issue":"2-4","key":"1_CR25","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF02127745","volume":"18","author":"B. Hollunder","year":"1996","unstructured":"Hollunder, B.: Consistency checking reduced to satisfiability of concepts in terminological systems. Annals of Mathematics and Artificial Intelligence\u00a018(2-4), 133\u2013157 (1996)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"1_CR26","unstructured":"Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. In: Proc. of KR 1991, pp. 335\u2013346 (1991)"},{"key":"1_CR27","unstructured":"Hollunder, B., Nutt, W.: Subsumption algorithms for concept languages. Technical Report RR-90-04, DFKI, Kaiserslautern, Germany (1990)"},{"key":"1_CR28","unstructured":"Hollunder, B., Nutt, W., Schmidt-Schau\u00df, M.: Subsumption algorithms for concept description languages. In: Proc. of ECAI 1990, London, pp. 348\u2013353. Pitman (1990)"},{"key":"1_CR29","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/3-540-69778-0_30","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"I. Horrocks","year":"1998","unstructured":"Horrocks, I.: The FaCT system. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, pp. 307\u2013312. Springer, Heidelberg (1998)"},{"key":"1_CR30","unstructured":"Horrocks, I.: Using an expressive description logic: FaCT or fiction? In: Proc. of KR 1998, pp. 636\u2013647 (1998)"},{"issue":"3","key":"1_CR31","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1093\/logcom\/9.3.267","volume":"9","author":"I. Horrocks","year":"1999","unstructured":"Horrocks, I., Patel-Schneider, P.F.: Optimizing description logic subsumption. J. of Logic and Computation\u00a09(3), 267\u2013293 (1999)","journal-title":"J. of Logic and Computation"},{"issue":"3","key":"1_CR32","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. J. of Logic and Computation\u00a09(3), 385\u2013410 (1999)","journal-title":"J. of Logic and Computation"},{"key":"1_CR33","series-title":"Lecture Notes in Computer Science","volume-title":"Logic Programming and Automated Reasoning","author":"I. Horrocks","year":"1999","unstructured":"Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for expressive description logics. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol.\u00a01705. Springer, Heidelberg (1999)"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","volume-title":"Logic Programming and Automated Reasoning","author":"C. Lutz","year":"1999","unstructured":"Lutz, C.: Complexity of terminological reasoning revisited. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol.\u00a01705. Springer, Heidelberg (1999)"},{"key":"1_CR35","first-page":"385","volume-title":"Principles of Semantic Networks","author":"R. MacGregor","year":"1991","unstructured":"MacGregor, R.: The evolving technology of classification-based knowledge representation systems. In: Sowa, J.F. (ed.) Principles of Semantic Networks, pp. 385\u2013400. Morgan Kaufmann, San Francisco (1991)"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Mays, E., Dionne, R., Weida, R.: K-REP system overview. SIGART Bulletin\u00a02(3) (1991)","DOI":"10.1145\/122296.122310"},{"key":"1_CR37","volume-title":"Mind Design","author":"M. Minsky","year":"1981","unstructured":"Minsky, M.: A framework for representing knowledge. In: Haugeland, J. (ed.) Mind Design. The MIT Press, Cambridge (1981); Republished in [11]"},{"key":"1_CR38","series-title":"Lecture Notes in Computer Science","volume-title":"Reasoning and Revision in Hybrid Representation Systems","year":"1990","unstructured":"Nebel, B. (ed.): Reasoning and Revision in Hybrid Representation Systems. LNCS, vol.\u00a0422. Springer, Heidelberg (1990)"},{"key":"1_CR39","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0004-3702(90)90087-G","volume":"43","author":"B. Nebel","year":"1990","unstructured":"Nebel, B.: Terminological reasoning is inherently intractable. Artificial Intelligence\u00a043, 235\u2013249 (1990)","journal-title":"Artificial Intelligence"},{"key":"1_CR40","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1016\/B978-1-4832-0771-1.50018-7","volume-title":"Principles of Semantic Networks","author":"B. Nebel","year":"1991","unstructured":"Nebel, B.: Terminological cycles: Semantics and computational properties. In: Sowa, J.F. (ed.) Principles of Semantic Networks, pp. 331\u2013361. Morgan Kaufmann, San Francisco (1991)"},{"key":"1_CR41","unstructured":"Patel-Schneider, P.F.: DLP. In: Proc. of DL 1999, CEUR Electronic Workshop Proceedings, pp. 9\u201313 (1999), http:\/\/sunsite.informatik.rwth-aachen.de\/Publications\/CEUR-WS\/Vol-22\/"},{"issue":"3","key":"1_CR42","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1145\/122296.122313","volume":"2","author":"P.F. Patel-Schneider","year":"1991","unstructured":"Patel-Schneider, P.F., McGuiness, D.L., Brachman, R.J., Resnick, L.A., Borgida, A.: The CLASSIC knowledge representation system: Guiding principles and implementation rational. SIGART Bulletin\u00a02(3), 108\u2013113 (1991)","journal-title":"SIGART Bulletin"},{"issue":"3","key":"1_CR43","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/122296.122314","volume":"2","author":"C. Peltason","year":"1991","unstructured":"Peltason, C.: The BACK system - an overview. SIGART Bulletin\u00a02(3), 114\u2013119 (1991)","journal-title":"SIGART Bulletin"},{"key":"1_CR44","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1002\/bs.3830120511","volume":"12","author":"M.R. Quillian","year":"1967","unstructured":"Quillian, M.R.: Word concepts: A theory and simulation of some basic capabilities. Behavioral Science\u00a012, 410\u2013430 (1967); Republished in [11]","journal-title":"Behavioral Science"},{"key":"1_CR45","series-title":"LNAI","volume-title":"KI-96: Advances in Artificial Intelligence","author":"U. Sattler","year":"1996","unstructured":"Sattler, U.: A concept language extended with different kinds of transitive roles. In: G\u00f6rz, G., H\u00f6lldobler, S. (eds.) KI 1996. LNCS (LNAI), vol.\u00a01137. Springer, Heidelberg (1996)"},{"key":"1_CR46","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"W.J. Savitch","year":"1970","unstructured":"Savitch, W.J.: Relationship between nondeterministic and deterministic tape complexities. J. of Computer and System Science\u00a04, 177\u2013192 (1970)","journal-title":"J. of Computer and System Science"},{"key":"1_CR47","unstructured":"Schild, K.: A correspondence theory for terminological logics: Preliminary report. In: Proc. of IJCAI 1991, Sydney, Australia, pp. 466\u2013471 (1991)"},{"key":"1_CR48","first-page":"509","volume-title":"Proc. of KR 1994","author":"K. Schild","year":"1994","unstructured":"Schild, K.: Terminological cycles and the propositional \u03bc-calculus. In: Doyle, J., Sandewall, E., Torasso, P. (eds.) Proc. of KR 1994, Bonn, pp. 509\u2013520. Morgan Kaufmann, San Francisco (1994)"},{"key":"1_CR49","first-page":"421","volume-title":"Proc. of KR 1989","author":"M. Schmidt-Schau\u00df","year":"1989","unstructured":"Schmidt-Schau\u00df, M.: Subsumption in KL-ONE is undecidable. In: Brachman, R.J., Levesque, H.J., Reiter, R. (eds.) Proc. of KR 1989, pp. 421\u2013431. Morgan Kaufmann, San Francisco (1989)"},{"issue":"1","key":"1_CR50","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":"Schmidt-Schau\u00df, M., Smolka, G.: Attributive concept descriptions with complements. Artificial Intelligence\u00a048(1), 1\u201326 (1991)","journal-title":"Artificial Intelligence"},{"key":"1_CR51","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/978-94-015-8242-1_10","volume-title":"Diamonds and Defaults","author":"E. Spaan","year":"1993","unstructured":"Spaan, E.: The complexity of propositional tense logics. In: de Rijke, M. (ed.) Diamonds and Defaults, pp. 287\u2013307. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"1_CR52","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/3-540-48660-7_4","volume-title":"Automated Deduction - CADE-16","author":"S. Tobies","year":"1999","unstructured":"Tobies, S.: A PSPACE algorithm for graded modal logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 52\u201366. Springer, Heidelberg (1999)"},{"issue":"3","key":"1_CR53","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1093\/logcom\/5.3.325","volume":"5","author":"W. Hoek Van der","year":"1995","unstructured":"Van der Hoek, W., De Rijke, M.: Counting objects. J. of Logic and Computation\u00a05(3), 325\u2013345 (1995)","journal-title":"J. of Logic and Computation"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722086_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T07:47:22Z","timestamp":1556005642000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/10722086_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}