{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T03:23:38Z","timestamp":1775705018503,"version":"3.50.1"},"reference-count":81,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2001,10,1]],"date-time":"2001-10-01T00:00:00Z","timestamp":1001894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,10,1]],"date-time":"2001-10-01T00:00:00Z","timestamp":1001894400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Studia Logica"],"published-print":{"date-parts":[[2001,10]]},"DOI":"10.1023\/a:1013882326814","type":"journal-article","created":{"date-parts":[[2003,3,20]],"date-time":"2003-03-20T21:15:11Z","timestamp":1048194911000},"page":"5-40","source":"Crossref","is-referenced-by-count":215,"title":["An Overview of Tableau Algorithms for Description Logics"],"prefix":"10.1007","volume":"69","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[]},{"given":"Ulrike","family":"Sattler","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"389692_CR1","unstructured":"Baader, F.: 1991, 'Augmenting Concept Languages by Transitive Closure of Roles: An Alternative to Terminological Cycles'. In: Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI-91). A long version appeared as DFKI-Research-Report RR-90-13, Kaiserslautern, Germany."},{"issue":"1\u20132","key":"389692_CR2","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/S0004-3702(96)00010-0","volume":"88","author":"F. Baader","year":"1996","unstructured":"Baader, F., M. Buchheit, and B. Hollunder: 1996, 'Cardinality Restrictions on Concepts'. Artificial Intelligence Journal 88(1\u20132), 195-213.","journal-title":"Artificial Intelligence Journal"},{"key":"389692_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01051766","volume":"2","author":"F. Baader","year":"1993","unstructured":"Baader, F., H.-J. B\u00fcrckert, B. Nebel, W. Nutt, and G. Smolka: 1993, 'On the Expressivity of Feature Logics with Negation, Functional Uncertainty, and Sort Equations'. Journal of Logic, Language and Information 2, 1-18.","journal-title":"Journal of Logic, Language and Information"},{"key":"389692_CR4","first-page":"109","volume":"4","author":"F. Baader","year":"1994","unstructured":"Baader, F., E. Franconi, B. Hollunder, B. Nebel, and H. Profitlich: 1994, 'An Empirical Analysis of Optimization Techniques for Terminological Representation Systems or: Making KRIS get a move on'. Applied Artificial Intelligence. Special Issue on Knowledge Base Management 4, 109-132.","journal-title":"Applied Artificial Intelligence. Special Issue on Knowledge Base Management"},{"key":"389692_CR5","series-title":"Technical Report","volume-title":"Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI-91)","author":"F. Baader","year":"1991","unstructured":"Baader, F. and P. Hanschke: 1991, 'A Schema for Integrating Concrete Domains into Concept Languages'. Technical Report RR-91-10, Deutsches Forschungszentrum f\u00fcr K\u00fcnstliche Intelligenz (DFKI), Kaiserslautern, Germany. An abridged version appeared in Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI-91)."},{"key":"389692_CR6","first-page":"67","volume":"567","author":"F. Baader","year":"1991","unstructured":"Baader, F. and B. Hollunder: 1991, 'A Terminological Knowledge Representation System with Complete Inference Algorithm'. In: Proc. of PDK'91, Vol. 567 of Lecture Notes In Artificial Intelligence. pp. 67-86, Springer-Verlag.","journal-title":"Proc. of PDK'91"},{"issue":"3","key":"389692_CR7","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1093\/logcom\/9.3.319","volume":"9","author":"F. Baader","year":"1999","unstructured":"Baader, F. and U. Sattler: 1999, 'Expressive Number Restrictions in Description Logics'. Journal of Logic and Computation 9(3), 319-350.","journal-title":"Journal of Logic and Computation"},{"key":"389692_CR8","doi-asserted-by":"crossref","unstructured":"Baader, F. and U. Sattler: 2000, 'Tableau Algorithms for Description Logics'. In: R. Dyckhoff (ed.): Proc. of the Int. Conf. on Automated Reasoning with Tableaux and Related Methods (Tableaux 2000), Vol. 1847 of Lecture Notes in Artificial Intelligence. pp. 1-18, Springer-Verlag.","DOI":"10.1007\/10722086_1"},{"key":"389692_CR9","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1016\/0022-0000(82)90018-6","volume":"25","author":"M. Ben-Ari","year":"1982","unstructured":"Ben-Ari, M., J. Y. Halpern, and A. Pnueli: 1982, 'Deterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness'. Journal of Computer and System Science 25, 402-417.","journal-title":"Journal of Computer and System Science"},{"key":"389692_CR10","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1613\/jair.56","volume":"1","author":"A. Borgida","year":"1994","unstructured":"Borgida, A. and P. F. Patel-Schneider: 1994, 'A Semantics and Complete Algorithm for Subsumption in the CLASSIC Description Logic'. Journal of Artificial Intelligence Research 1, 277-308.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"389692_CR11","unstructured":"Brachman, R. J.: 1992, '\u201cReducing\u201d CLASSIC to Practice: Knowledge Representation Meets Reality'. In: Proc. of the 3rd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-92). pp. 247-258, Morgan Kaufmann."},{"key":"389692_CR12","unstructured":"Brachman, R. J. and H. J. Levesque: 1984, 'The Tractability of Subsumption in Frame-Based Description Languages'. In: Proc. of the 4th Nat. Conf. on Artificial Intelligence (AAAI-84), pp. 34-37, AAAI Press."},{"key":"389692_CR13","unstructured":"Brachman, R. J. and H. J. Levesque (eds.): 1985, Readings in Knowledge Representation. Morgan Kaufmann."},{"issue":"2","key":"389692_CR14","first-page":"171","volume":"9","author":"R. J. Brachman","year":"1985","unstructured":"Brachman, R. J. and J. G. Schmolze: 1985, 'An Overview of the KL-ONE Knowledge Representation System'. Cognitive Science 9(2), 171-216.","journal-title":"Cognitive Science"},{"key":"389692_CR15","unstructured":"Bresciani, P., E. Franconi, and S. Tessaris: 1995, 'Implementing and Testing Expressive Description Logics: Preliminary Report'. In: A. Borgida, M. Lenzerini, D. Nardi, and B. Nebel (eds.): Working Notes of the 1995 Description Logics Workshop. pp. 131-139."},{"key":"389692_CR16","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1613\/jair.21","volume":"1","author":"M. Buchheit","year":"1993","unstructured":"Buchheit, M., F. M. Donini, and A. Schaerf: 1993, 'Decidable Reasoning in Terminological Knowledge Representation Systems'. Journal of Artificial Intelligence Research 1, 109-138.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"389692_CR17","doi-asserted-by":"crossref","unstructured":"Calvanese, D., G. De Giacomo, and M. Lenzerini: 1998a, 'On the Decidability of Query Containment under Constraints'. In: Proc. of the Seventeenth ACM SIGACT SIGMOD Sym. on Principles of Database Systems (PODS-98). pp. 149-158.","DOI":"10.1145\/275487.275504"},{"key":"389692_CR18","unstructured":"Calvanese, D., G. De Giacomo, M. Lenzerini, D. Nardi, and R. Rosati: 1998b, 'Description Logic Framework for Information Integration'. In: Proc. of the 6th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-98). pp. 2-13, Morgan Kaufmann."},{"key":"389692_CR19","unstructured":"Calvanese, D., G. De Giacomo, and R. Rosati: 1999a, 'Data Integration and Reconciliation in Data Warehousing: Conceptual Modeling and Reasoning Support'. Network and Information Systems 4(2)."},{"key":"389692_CR20","volume-title":"Handbook of Automated Reasoning","author":"D. Calvanese","year":"2001","unstructured":"Calvanese, D., G. D. Giacomo, M. Lenzerini, and D. Nardi: 2001, 'Reasoning in Expressive Description Logics'. In: A. Robinson and A. Voronkov (eds.): Handbook of Automated Reasoning. Amsterdam, NL: Elsevier Science Publishers."},{"key":"389692_CR21","doi-asserted-by":"crossref","unstructured":"Calvanese, D., M. Lenzerini, and D. Nardi: 1998c, 'Description Logics for Conceptual Data Modeling'. In: J. Chomicki and G. Saake (eds.): Logics for Databases and Information Systems. Kluwer Academic Publisher, pp. 229-264.","DOI":"10.1007\/978-1-4615-5643-5_8"},{"key":"389692_CR22","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1613\/jair.548","volume":"11","author":"D. Calvanese","year":"1999","unstructured":"Calvanese, D., M. Lenzerini, and D. Nardi: 1999b, 'Unifying Class-Based Representation Formalisms'. Journal of Artificial Intelligence Research 11, 199-240.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"389692_CR23","unstructured":"De Giacomo, G.: 1995, 'Decidability of Class-Based Knowledge Representation Formalisms'. Ph.D. thesis, Dipartimento di Informatica e Sistemistica, Universit\u00e0 diRoma \u201cLa Sapienza\u201d."},{"key":"389692_CR24","unstructured":"De Giacomo, G., F. Donini, and F. Massacci: 1996, 'EXPTIME tableaux for ALC'. In: Proc. of the 1996 Description Logic Workshop (DL'96)."},{"key":"389692_CR25","unstructured":"De Giacomo, G. and M. Lenzerini: 1994, 'Boosting the Correspondence between Description Logics and Propositional Dynamic Logics'. In: Proc. of the 12th Nat. Conf. on Artificial Intelligence (AAAI-94). pp. 205-212, AAAI Press\/The MIT Press."},{"key":"389692_CR26","unstructured":"De Giacomo, G. and M. Lenzerini: 1996, 'TBox and ABox Reasoning in Expressive Description Logics'. In: L. C. Aiello, J. Doyle, and S. C. Shapiro (eds.): Proc. of the 5th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-96). pp. 316-327, Morgan Kaufmann."},{"key":"389692_CR27","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1007\/3-540-61511-3_117","volume":"1104","author":"G. De Giacomo","year":"1996","unstructured":"De Giacomo, G. and F. Massacci: 1996, 'Tableaux and algorithms for propositional dynamic logic with converse'. In: Proc. of the 13th Conf. on Automated Deduction (CADE-96), Vol. 1104 of Lecture Notes In Artificial Intelligence. pp. 613-628, Springer-Verlag. A long versioned will appear in Information and Computation.","journal-title":"Proc. of the 13th Conf. on Automated Deduction (CADE-96)"},{"key":"389692_CR28","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1016\/0004-3702(92)90076-A","volume":"2\u20133","author":"F. M. Donini","year":"1992","unstructured":"Donini, F. M., B. Hollunder, M. Lenzerini, A. M. Spaccamela, D. Nardi, and W. Nutt: 1992, 'The Complexity of Existential Quantification in Concept Languages'. Artificial Intelligence Journal 2\u20133, 309-327.","journal-title":"Artificial Intelligence Journal"},{"key":"389692_CR29","unstructured":"Donini, F. M., M. Lenzerini, D. Nardi, and W. Nutt: 1991a, 'The Complexity of Concept Languages'. In: J. Allen, R. Fikes, and E. Sandewall (eds.): Proc. of the 2nd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-91). pp. 151-162, Morgan Kaufmann."},{"key":"389692_CR30","unstructured":"Donini, F. M., M. Lenzerini, D. Nardi, and W. Nutt: 1991b, 'Tractable Concept Languages'. In: Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI-91). pp. 458-463."},{"issue":"4","key":"389692_CR31","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1093\/logcom\/4.4.423","volume":"4","author":"F. Donini","year":"1994","unstructured":"Donini, F. M., M. Lenzerini, D. Nardi, and A. Schaerf: 1994, 'Deduction in Concept Languages: From Subsumption to Instance Checking'. Journal of Logic and Computation 4(4), 423-452.","journal-title":"Journal of Logic and Computation"},{"key":"389692_CR32","unstructured":"Donini, F. M., M. Lenzerini, D. Nardi, and A. Schaerf: 1996, 'Reasoning in Description Logics'. In: G. Brewka (ed.): Principles of Knowledge Representation, Studies in Logic, Language and Information. CSLI Publications, pp. 193-238."},{"key":"389692_CR33","series-title":"Technical Report","volume-title":"EXPTIME Tableaux for ALC","author":"F. M. Donini","year":"1999","unstructured":"Donini, F. M. and F. Massacci: 1999, 'EXPTIME Tableaux for ALC'. Technical Report 32\/99, Dipartimento di Ingegenria dell'Informazione, Universita degli studi di Siena, Italy. To appear in Artificial Intelligence."},{"key":"389692_CR34","unstructured":"Franconi, E. and G. Ng: 2000, 'The i\u00b7com Tool for Intelligent Conceptual Modelling'. In: Working Notes of the ECAI2000 Workshop on Knowledge Representation Meets Databases (KRDB2000), CEUR Electronic Workshop Proceedings."},{"key":"389692_CR35","first-page":"9","volume":"1","author":"E. Franconi","year":"1999","unstructured":"Franconi, E. and U. Sattler: 1999, 'A Data Warehouse Conceptual Data Model for Multidimensional Aggregation: a preliminary report'. Italian Association for Artificial Intelligence AI*IA Notizie 1, 9-21.","journal-title":"Italian Association for Artificial Intelligence AI*IA Notizie"},{"key":"389692_CR36","unstructured":"Haarslev, V. and R. M\u00f6ller: 1999, 'RACE System Description'. In: Proc. of the 1999 Description Logic Workshop (DL'99). pp. 130-132, CEUR Electronic Workshop Proceedings."},{"key":"389692_CR37","doi-asserted-by":"crossref","unstructured":"Haarslev, V. and R. M\u00f6ller: 2000a, 'Consistency Testing: The RACE Experience'. In: R. Dyckhoff (ed.): Proc. of the Int. Conf. on Automated Reasoning with Tableaux and Related Methods (Tableaux 2000), Vol. 1847 of Lecture Notes in Artificial Intelligence. pp. 57-61, Springer-Verlag.","DOI":"10.1007\/10722086_5"},{"key":"389692_CR38","unstructured":"Haarslev, V. and R. M\u00f6ller: 2000b, 'Expressive ABox Reasoning with Number Restrictions, Role Hierarchies, and Transitively Closed Roles'. In: Proc. of the 7th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-00). Morgan Kaufmann."},{"key":"389692_CR39","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","volume":"54","author":"J. Y. Halpern","year":"1992","unstructured":"Halpern, J. Y. and Y. Moses: 1992, 'A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief'. Artificial Intelligence Journal 54, 319-379.","journal-title":"Artificial Intelligence Journal"},{"key":"389692_CR40","unstructured":"Hanschke, P.: 1992, 'Specifying Role Interaction in Concept Languages'. In: Proc. of the 3rd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-92). pp. 318-329, Morgan Kaufmann."},{"key":"389692_CR41","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1007\/978-94-009-6259-0_10","volume-title":"Handbook of Philosophical Logic","author":"D. Harel","year":"1984","unstructured":"Harel, D.: 1984, 'Dynamic Logic'. In: Handbook of Philosophical Logic, Vol. 2. Dordrecht, Holland: D. Reidel, pp. 497-640."},{"key":"389692_CR42","first-page":"38","volume":"251","author":"B. Hollunder","year":"1990","unstructured":"Hollunder, B.: 1990, 'Hybrid Inferences in KL-ONE-based Knowledge Representation Systems'. In: Proc. of GWAI '90, Vol. 251 of Informatik-Fachberichte. pp. 38-47, Springer-Verlag.","journal-title":"Proc. of GWAI '90"},{"issue":"2-4","key":"389692_CR43","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/BF02127745","volume":"18","author":"B. Hollunder","year":"1996","unstructured":"Hollunder, B.: 1996, 'Consistency Checking Reduced to Satisfiability of Concepts in Terminological Systems'. Annals of Mathematics and Artificial Intelligence 18(2-4), 133-157.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"389692_CR44","unstructured":"Hollunder, B. and F. Baader: 1991, 'Qualifying Number Restrictions in Concept Languages'. In: Proc. of the 2nd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-91). pp. 335-346, Morgan Kaufmann."},{"key":"389692_CR45","series-title":"Technical Report","volume-title":"Subsumption Algorithms for Concept Languages","author":"B. Hollunder","year":"1990","unstructured":"Hollunder, B. and W. Nutt: 1990, 'Subsumption Algorithms for Concept Languages'. Technical Report RR-90-04, Deutsches Forschungszentrum f\u00fcr K\u00fcnstliche Intelligenz (DFKI), Kaiserslautern, Germany."},{"key":"389692_CR46","unstructured":"Hollunder, B., W. Nutt, and M. Schmidt-Schau\u03b2: 1990, 'Subsumption Algorithms for Concept Description Languages'. In: Proc. of the 9th European Conf. on Artificial Intelligence (ECAI-90). pp. 348-353, Pitman."},{"key":"389692_CR47","doi-asserted-by":"crossref","unstructured":"Horrocks, I.: 1998a, 'The FaCT System'. In: H. de Swart (ed.): Proc. of the Int. Conf. on Automated Reasoning with Tableaux and Related Methods (Tableaux-98), Vol. 1397 of Lecture Notes in Artificial Intelligence. pp. 307-312, Springer-Verlag.","DOI":"10.1007\/3-540-69778-0_30"},{"key":"389692_CR48","unstructured":"Horrocks, I.: 1998b, 'Using an Expressive Description Logic: FaCT or Fiction?'. In: Proc. of the 6th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-98). pp. 636-647, Morgan Kaufmann."},{"key":"389692_CR49","doi-asserted-by":"crossref","unstructured":"Horrocks, I.: 2000, 'Benchmark Analysis for FaCT'. In: R. Dyckhoff (ed.): Proc. of the Int. Conf. on Automated Reasoning with Tableaux and Related Methods (Tableaux 2000), Vol. 1847 of Lecture Notes in Artificial Intelligence. pp. 62-66, Springer-Verlag.","DOI":"10.1007\/10722086_6"},{"issue":"3","key":"389692_CR50","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1093\/logcom\/9.3.267","volume":"9","author":"I. Horrocks","year":"1999","unstructured":"Horrocks, I. and P. F. Patel-Schneider: 1999, 'Optimizing Description Logic Subsumption'. Journal of Logic and Computation 9(3), 267-293.","journal-title":"Journal of Logic and Computation"},{"issue":"3","key":"389692_CR51","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1093\/logcom\/9.3.385","volume":"9","author":"I. Horrocks","year":"1999","unstructured":"Horrocks, I. and U. Sattler: 1999, 'A Description Logic with Transitive and Inverse Roles and Role Hierarchies'. Journal of Logic and Computation 9(3), 385-410.","journal-title":"Journal of Logic and Computation"},{"key":"389692_CR52","doi-asserted-by":"crossref","unstructured":"Horrocks, I., U. Sattler, and S. Tobies: 1999, 'Practical Reasoning for Expressive Description Logics'. In: Proc. of the 6th Int. Conf. on Logic for Programming and Automated Reasoning (LPAR '99), Vol. 1705 of Lecture Notes In Artificial Intelligence. Springer-Verlag.","DOI":"10.1007\/3-540-48242-3_11"},{"issue":"3","key":"389692_CR53","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1093\/jigpal\/8.3.239","volume":"8","author":"I. Horrocks","year":"2000","unstructured":"Horrocks, I., U. Sattler, and S. Tobies: 2000a, 'Practical Reasoning for Very Expressive Description Logics'. Logic Journal of the IGPL 8(3), 239-264.","journal-title":"Logic Journal of the IGPL"},{"key":"389692_CR54","doi-asserted-by":"crossref","unstructured":"Horrocks, I., U. Sattler, and S. Tobies: 2000b, 'Reasoning with Individuals for the Description Logic SHIQ'. In: D. MacAllester (ed.): Proc. of the 13th Conf. on Automated Deduction (CADE-17). Springer-Verlag.","DOI":"10.1007\/10721959_39"},{"key":"389692_CR55","doi-asserted-by":"crossref","unstructured":"Lutz, C.: 1999, 'Complexity of Terminological Reasoning Revisited'. In: Proc. of the 6th Int. Conf. on Logic for Programming and Automated Reasoning (LPAR'99), Vol. 1705 of Lecture Notes In Artificial Intelligence. Springer-Verlag.","DOI":"10.1007\/3-540-48242-3_12"},{"key":"389692_CR56","unstructured":"Lutz, C. and U. Sattler: 2000, 'The Complexity of Reasoning with Boolean Modal Logic'. In: Advances in Modal Logic 2000 (AiML 2000). Leipzig, Germany."},{"key":"389692_CR57","doi-asserted-by":"crossref","unstructured":"MacGregor, R.: 1991, 'The Evolving Technology of Classification-Based Knowledge Representation Systems'. In: J. F. Sowa (ed.): Principles of Semantic Networks. Morgan Kaufmann, pp. 385-400.","DOI":"10.1016\/B978-1-4832-0771-1.50021-7"},{"key":"389692_CR58","doi-asserted-by":"crossref","unstructured":"Mays, E., R. Dionne, and R. Weida: 1991, 'K-REP System Overview'. SIGART Bulletin 2(3).","DOI":"10.1145\/122296.122310"},{"key":"389692_CR59","unstructured":"Minsky, M.: 1981, 'A Framework for Representing Knowledge'. In: J. Haugeland (ed.): Mind Design. The MIT Press. Republished in (Brachman and Levesque, 1985)."},{"key":"389692_CR60","unstructured":"Nebel, B.: 1990a, Reasoning and Revision in Hybrid Representation Systems, Vol. 422 of Lecture Notes In Artificial Intelligence. Springer-Verlag."},{"key":"389692_CR61","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0004-3702(90)90087-G","volume":"43","author":"B. Nebel","year":"1990","unstructured":"Nebel, B.: 1990b, 'Terminological Reasoning is Inherently Intractable'. Artificial Intelligence Journal 43, 235-249.","journal-title":"Artificial Intelligence Journal"},{"key":"389692_CR62","doi-asserted-by":"crossref","unstructured":"Nebel, B.: 1991, 'Terminological Cycles: Semantics and Computational Properties'. In: J. F. Sowa (ed.): Principles of Semantic Networks. Morgan Kaufmann, pp. 331-361.","DOI":"10.1016\/B978-1-4832-0771-1.50018-7"},{"key":"389692_CR63","doi-asserted-by":"crossref","unstructured":"Patel-Schneider, P.: 2000, 'TANCS-2000 Results for DLP'. In: R. Dyckhoff (ed.): Proc. of the Int. Conf. on Automated Reasoning with Tableaux and Related Methods (Tableaux 2000), Vol. 1847 of Lecture Notes in Artificial Intelligence. pp. 72-76, Springer-Verlag.","DOI":"10.1007\/10722086_8"},{"key":"389692_CR64","unstructured":"Patel-Schneider, P. F.: 1999, 'DLP'. In: Proc. of the 1999 Description Logic Workshop (DL'99). pp. 9-13, CEUR Electronic Workshop Proceedings."},{"key":"389692_CR65","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/3-540-48754-9_3","volume":"1397","author":"P. F. Patel-Schneider","year":"1999","unstructured":"Patel-Schneider, P. F. and I. Horrocks: 1999, 'DLP and FaCT'. In: Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-99), Vol. 1397 of Lecture Notes In Artificial Intelligence. pp. 19-23, Springer-Verlag.","journal-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-99)"},{"issue":"3","key":"389692_CR66","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1145\/122296.122313","volume":"2","author":"P. F. Patel-Schneider","year":"1991","unstructured":"Patel-Schneider, P. F., D. L. McGuiness, R. J. Brachman, L. A. Resnick, and A. Borgida: 1991, 'The CLASSIC Knowledge Representation System: Guiding Principles and Implementation Rational'. SIGART Bulletin 2(3), 108-113.","journal-title":"SIGART Bulletin"},{"issue":"3","key":"389692_CR67","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/122296.122314","volume":"2","author":"C. Peltason","year":"1991","unstructured":"Peltason, C.: 1991, 'The BACK System-an Overview'. SIGART Bulletin 2(3), 114-119.","journal-title":"SIGART Bulletin"},{"key":"389692_CR68","doi-asserted-by":"crossref","unstructured":"Pratt, V. R.: 1979, 'Models of Program Logic'. In: Proc. of the 20th Annual Sym. on the Foundations of Computer Science (FOCS-79). pp. 115-122.","DOI":"10.1109\/SFCS.1979.24"},{"key":"389692_CR69","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1002\/bs.3830120511","volume":"12","author":"M. R. Quillian","year":"1967","unstructured":"Quillian, M. R.: 1967, 'Word Concepts: A Theory and Simulation of Some Basic Capabilities'. Behavioral Science 12, 410-430. Republished in (Brachman and Levesque, 1985).","journal-title":"Behavioral Science"},{"key":"389692_CR70","doi-asserted-by":"crossref","unstructured":"Sattler, U.: 1996, 'A Concept Language Extended with Different Kinds of Transitive Roles'. In: G. G\u00f6rz and S. H\u00f6lldobler (eds.): Proc. of the 20th German Annual Conf. on Artificial Intelligence (KI'96), Vol. 1137 of Lecture Notes In Artificial Intelligence. Springer-Verlag.","DOI":"10.1007\/3-540-61708-6_74"},{"key":"389692_CR71","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"W. J. Savitch","year":"1970","unstructured":"Savitch, W. J.: 1970, 'Relationship between Nondeterministic and Deterministic Tape Complexities'. Journal of Computer and System Science 4, 177-192.","journal-title":"Journal of Computer and System Science"},{"key":"389692_CR72","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BF00962071","volume":"2","author":"A. Schaerf","year":"1993","unstructured":"Schaerf, A.: 1993, 'On the Complexity of the Instance Checking Problem in Concept Languages with Existential Quantification'. Journal of Intelligent Information Systems 2, 265-278.","journal-title":"Journal of Intelligent Information Systems"},{"key":"389692_CR73","unstructured":"Schild, K.: 1991, 'A Correspondence Theory for Terminological Logics: Preliminary Report'. In: Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI-91). pp. 466-471."},{"key":"389692_CR74","doi-asserted-by":"crossref","unstructured":"Schild, K.: 1994, 'Terminological Cycles and the Propositional \u00b5-Calculus'. In: J. Doyle, E. Sandewall, and P. Torasso (eds.): Proc. of the 4th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-94). pp. 509-520, Morgan Kaufmann.","DOI":"10.1016\/B978-1-4832-1452-8.50142-1"},{"key":"389692_CR75","unstructured":"Schmidt-Schau\u00df , M.: 1989, 'Subsumption in KL-ONE is Undecidable'. In: R. J. Brachman, H. J. Levesque, and R. Reiter (eds.): Proc. of the 1st Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-89). pp. 421-431, Morgan Kaufmann."},{"issue":"1","key":"389692_CR76","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(91)90078-X","volume":"48","author":"M. Schmidt-Schau\u03b2","year":"1991","unstructured":"Schmidt-Schau\u03b2, M. and G. Smolka: 1991, 'Attributive Concept Descriptions with Complements'. Artificial Intelligence Journal 48(1), 1-26.","journal-title":"Artificial Intelligence Journal"},{"key":"389692_CR77","doi-asserted-by":"crossref","unstructured":"Spaan, E.: 1993, 'The Complexity of Propositional Tense Logics'. In: M. de Rijke (ed.): Diamonds and Defaults. Kluwer Academic Publishers, pp. 287-307.","DOI":"10.1007\/978-94-015-8242-1_10"},{"key":"389692_CR78","doi-asserted-by":"crossref","unstructured":"Stirling, C.: 1992, 'Modal and Temporal Logic'. In: S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum (eds.): Handbook of Logic in Computer Science. Clarendon Press, pp. 477-563.","DOI":"10.1093\/oso\/9780198537618.003.0005"},{"key":"389692_CR79","doi-asserted-by":"crossref","unstructured":"Tobies, S.: 1999, 'A PSPACE Algorithm for Graded Modal Logic'. In: Proc. of the 13th Conf. on Automated Deduction (CADE-16), Vol. 1632 of Lecture Notes in Computer Science. Springer-Verlag.","DOI":"10.1007\/3-540-48660-7_4"},{"issue":"3","key":"389692_CR80","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1093\/logcom\/5.3.325","volume":"5","author":"W. Van der Hoek","year":"1995","unstructured":"Van der Hoek, W. and M. De Rijke: 1995, 'Counting Objects'. Journal of Logic and Computation 5(3), 325-345.","journal-title":"Journal of Logic and Computation"},{"key":"389692_CR81","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M. Y. Vardi","year":"1986","unstructured":"Vardi, M. Y. and P. Wolper: 1986, 'Automata-theoretic Techniques for Modal Logics of Programs'. Journal of Computer and System Science 32, 183-221. A preliminary version appeared in Proc. of the 16th ACM SIGACT Symp. on Theory of Computing (STOC'84).","journal-title":"Journal of Computer and System Science"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1013882326814.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1013882326814\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1013882326814.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:19:57Z","timestamp":1754630397000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1013882326814"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,10]]},"references-count":81,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,10]]}},"alternative-id":["389692"],"URL":"https:\/\/doi.org\/10.1023\/a:1013882326814","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,10]]}}}