# An Overview of Tableau Algorithms for Description Logics

Studia Logica - An International Journal for Symbolic Logic, no. 1 (2001): 5-40

EI

Description logics are a family of knowledge representation formalisms that are descended from semantic networks and frames via the system Kl-one. During the last decade, it has been shown that the important reasoning problems (like subsumption and satisfiability) in a great variety of description logics can be decided using tableau-like ...更多

0

• Description logics (DLs) are a family of knowledge representation languages which can be used to represent the terminological knowledge of an application domain in a structured and formally well-understood way.
• An ABox is a finite set of assertions of the form C(a) or r(a, b), where C is a concept description, r a role name, and a, b are individual names.
• Given the input description Cn, the satisfiability algorithm generates a complete and open ABox whose canonical interpretation is a binary tree of depth n, and consists of 2n+1 − 1 individuals.

• Description logics (DLs) are a family of knowledge representation languages which can be used to represent the terminological knowledge of an application domain in a structured and formally well-understood way
• The name description logics is motivated by the fact that, on the one hand, the important notions of the domain are described by concept descriptions, i.e., expressions that are built from atomic concepts and atomic roles using the concept and role constructors provided by the particular DL
• Though many of the tableau-based algorithms sketched in this paper are of optimal worst-case complexity, and provide complexity results for subsumption and satisfiability in DLs, theoretical complexity results never were the main focus of this line of DL research
• For the logics treated in Section 6.2, the exact worst-case complexity (EXPTIME) was known before the (NEXPTIME) tableau algorithms sketched above were designed
• When the first complexity results showed that all of the DLs used in systems had subsumption problems of a higher complexity, the proposed solution was either to restrict the expressive power or to employ incomplete algorithms

• For ALCQ, the idea that leads to a PSPACE-algorithm for ALCN with non-unary notation does no longer work: it is not sufficient to introduce just one successor as representative for the role successors required by at-least restrictions.
• Satisfiability of ALCQ-concept descriptions as well as consistency of ALCQ-ABoxes are PSPACE-complete problems, even if numbers are not represented in unary notation.
• Nebel (1990b) shows that this complexity can, in general, not be avoided: for the DL FL0, which allows for conjunction and value restriction only, subsumption between concept descriptions can be tested in polynomial time, whereas subsumption w.r.t. acyclic terminologies is coNP-complete.
• In order to obtain a PSPACE-algorithm for subsumption in ALC w.r.t. acyclic terminologies, one cannot first apply unfolding to the concept descriptions to be tested for subsumption since this may need exponential space.
• . Internalisation of this axiom introduces a new transitive role u, and asserts in the role hierarchy that u is a super-role of all roles occurring in C and the concept description C0 to be tested for satisfiability.
• It shows that satisfiability and subsumption of concept descriptions in SH is EXPTIME-hard.5 The tableau algorithm for SH presented in (Horrocks, 1998b) handles role hierarchies by an appropriate definition of r-successors: an individual y is called an r-successor of an individual x in an ABox A iff s(x, y) ∈ A for some sub-role s of r.
• This violates the value restriction for x1, which shows that the interpretation obtained this way is not a model of the complete and open ABox. This problem can be overcome by using equality blocking, i.e., an individual y is blocked by an individual x iff {D | D(x) ∈ A} = {D | D (y) ∈ A}.

• If the role hierarchy contains the axiom s r for a transitive role r ∈ NR+, the following concept is obviously satisfiable, but each of its models has an infinite s-path: ¬A ∃s.A ∀r.(∃s.A ( 1s−)).
• This problem can be overcome by applying the pre-completion technique, which reduces ABox consistency to satisfiability of concept descriptions.
• It turned out that implementations of these algorithms were amenable to optimisation techniques and behaved quite well in practice (Baader et al, 1994; Bresciani et al, 1995)

• Description logics (DLs) are a family of knowledge representation languages which can be used to represent the terminological knowledge of an application domain in a structured and formally well-understood way.
• An ABox is a finite set of assertions of the form C(a) or r(a, b), where C is a concept description, r a role name, and a, b are individual names.
• Given the input description Cn, the satisfiability algorithm generates a complete and open ABox whose canonical interpretation is a binary tree of depth n, and consists of 2n+1 − 1 individuals.
• For ALCQ, the idea that leads to a PSPACE-algorithm for ALCN with non-unary notation does no longer work: it is not sufficient to introduce just one successor as representative for the role successors required by at-least restrictions.
• Satisfiability of ALCQ-concept descriptions as well as consistency of ALCQ-ABoxes are PSPACE-complete problems, even if numbers are not represented in unary notation.
• Nebel (1990b) shows that this complexity can, in general, not be avoided: for the DL FL0, which allows for conjunction and value restriction only, subsumption between concept descriptions can be tested in polynomial time, whereas subsumption w.r.t. acyclic terminologies is coNP-complete.
• In order to obtain a PSPACE-algorithm for subsumption in ALC w.r.t. acyclic terminologies, one cannot first apply unfolding to the concept descriptions to be tested for subsumption since this may need exponential space.
• . Internalisation of this axiom introduces a new transitive role u, and asserts in the role hierarchy that u is a super-role of all roles occurring in C and the concept description C0 to be tested for satisfiability.
• It shows that satisfiability and subsumption of concept descriptions in SH is EXPTIME-hard.5 The tableau algorithm for SH presented in (Horrocks, 1998b) handles role hierarchies by an appropriate definition of r-successors: an individual y is called an r-successor of an individual x in an ABox A iff s(x, y) ∈ A for some sub-role s of r.
• This violates the value restriction for x1, which shows that the interpretation obtained this way is not a model of the complete and open ABox. This problem can be overcome by using equality blocking, i.e., an individual y is blocked by an individual x iff {D | D(x) ∈ A} = {D | D (y) ∈ A}.
• If the role hierarchy contains the axiom s r for a transitive role r ∈ NR+, the following concept is obviously satisfiable, but each of its models has an infinite s-path: ¬A ∃s.A ∀r.(∃s.A ( 1s−)).
• This problem can be overcome by applying the pre-completion technique, which reduces ABox consistency to satisfiability of concept descriptions.
• It turned out that implementations of these algorithms were amenable to optimisation techniques and behaved quite well in practice (Baader et al, 1994; Bresciani et al, 1995)

• Table1: Syntax and semantics of concept descriptions. From the modal logic point of view, roles are simply names for accessibility relations, and existential (value) restrictions correspond to diamonds (boxes) indexed by the respective accessibility relation. Thus, any ALC description can be translated into a multi-modal K formula and vice versa. For example, the description P ∃r.P ∀r.¬P corresponds to the formula p ∧ r p ∧ [r]¬p, where p is an atomic proposition corresponding to the concept name P . As pointed out by <a class="ref-link" id="cSchild_1991_a" href="#rSchild_1991_a">Schild (1991</a>), there is an obvious correspondence between the semantics of ALC and the Kripke semantics for
• Table2: Syntax and semantics of role constructors and restrictions

• 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.
• Baader, F., M. Buchheit, and B. Hollunder: 1996, ‘Cardinality Restrictions on Concepts’. Artificial Intelligence Journal 88(1–2), 195–213.
• Baader, F., H.-J. Burckert, 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.
• 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.
• Baader, F. and P. Hanschke: 1991, ‘A Schema for Integrating Concrete Domains into Concept Languages’. Technical Report RR-91-10, Deutsches Forschungszentrum fur Kunstliche Intelligenz (DFKI), Kaiserslautern, Germany. An abridged version appeared in Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI-91).
• 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.
• Baader, F. and U. Sattler: 1999, ‘Expressive Number Restrictions in Description Logics’. Journal of Logic and Computation 9(3), 319–350.
• 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.
• 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.
• 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.
• Brachman, R. J.: 1992, ‘“Reducing” 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.
• Brachman, R. J. and H. J. Levesque: 1984, ‘The Tractability of Subsumption in FrameBased Description Languages’. In: Proc. of the 4th Nat. Conf. on Artificial Intelligence (AAAI-84), pp. 34–37, AAAI Press.
• Brachman, R. J. and H. J. Levesque (eds.): 1985, Readings in Knowledge Representation. Morgan Kaufmann.
• Brachman, R. J. and J. G. Schmolze: 1985, ‘An Overview of the KL-ONE Knowledge Representation System’. Cognitive Science 9(2), 171–216.
• 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.
• Buchheit, M., F. M. Donini, and A. Schaerf: 1993, ‘Decidable Reasoning in Terminological Knowledge Representation Systems’. Journal of Artificial Intelligence Research 1, 109– 138.
• 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.
• 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
• 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).
• 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.
• 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.
• Calvanese, D., M. Lenzerini, and D. Nardi: 1999b, ‘Unifying Class-Based Representation Formalisms’. Journal of Artificial Intelligence Research 11, 199–240.
• De Giacomo, G.: 1995, ‘Decidability of Class-Based Knowledge Representation Formalisms’. Ph.D. thesis, Dipartimento di Informatica e Sistemistica, Universita di Roma “La Sapienza”.
• De Giacomo, G., F. Donini, and F. Massacci: 1996, ‘EXPTIME tableaux for ALC’. In: Proc. of the 1996 Description Logic Workshop (DL’96).
• 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.
• 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.
• 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, SpringerVerlag. A long versioned will appear in Information and Computation.
• 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–3, 309–327.
• 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.
• 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.
• 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.
• 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.
• 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.
• Franconi, E. and G. Ng: 2000, ‘The i•com Tool for Intelligent Conceptual Modelling’. In: Working Notes of the ECAI2000 Workshop on Knowledge Representation Meets Databases (KRDB2000), CEUR Electronic Workshop Proceedings.
• 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.
• Haarslev, V. and R. Moller: 1999, ‘RACE System Description’. In: Proc. of the 1999 Description Logic Workshop (DL’99). pp. 130–132, CEUR Electronic Workshop Proceedings.
• Haarslev, V. and R. Moller: 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.
• Haarslev, V. and R. Moller: 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.
• 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.
• 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.
• Harel, D.: 1984, ‘Dynamic Logic’. In: Handbook of Philosophical Logic, Vol. 2.
• 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, SpringerVerlag.
• Hollunder, B.: 1996, ‘Consistency Checking Reduced to Satisfiability of Concepts in Terminological Systems’. Annals of Mathematics and Artificial Intelligence 18(2–4), 133–157.
• 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.
• Hollunder, B. and W. Nutt: 1990, ‘Subsumption Algorithms for Concept Languages’. Technical Report RR-90-04, Deutsches Forschungszentrum fur Kunstliche Intelligenz (DFKI), Kaiserslautern, Germany.
• Hollunder, B., W. Nutt, and M. Schmidt-Schauß: 1990, ‘Subsumption Algorithms for Concept Description Languages’. In: Proc. of the 9th European Conf. on Artificial Intelligence (ECAI-90). pp. 348–353, Pitman.
• 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.
• 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.
• 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.
• Horrocks, I. and P. F. Patel-Schneider: 1999, ‘Optimizing Description Logic Subsumption’. Journal of Logic and Computation 9(3), 267–293.
• 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.
• 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. SpringerVerlag.
• Horrocks, I., U. Sattler, and S. Tobies: 2000a, ‘Practical Reasoning for Very Expressive Description Logics’. Logic Journal of the IGPL 8(3), 239–264.
• 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.
• 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.
• Lutz, C. and U. Sattler: 2000, ‘The Complexity of Reasoning with Boolean Modal Logic’. In: Advances in Modal Logic 2000 (AiML 2000). Leipzig, Germany.
• 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.
• Mays, E., R. Dionne, and R. Weida: 1991, ‘K-REP System Overview’. SIGART Bulletin 2(3).
• Minsky, M.: 1981, ‘A Framework for Representing Knowledge’. In: J. Haugeland (ed.): Mind Design. The MIT Press. Republished in (Brachman and Levesque, 1985).
• Nebel, B.: 1990a, Reasoning and Revision in Hybrid Representation Systems, Vol. 422 of Lecture Notes In Artificial Intelligence. Springer-Verlag.
• Nebel, B.: 1990b, ‘Terminological Reasoning is Inherently Intractable’. Artificial Intelligence Journal 43, 235–249.
• Nebel, B.: 1991, ‘Terminological Cycles: Semantics and Computational Properties’. In: J. F. Sowa (ed.): Principles of Semantic Networks. Morgan Kaufmann, pp. 331–361.
• 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.
• Patel-Schneider, P. F.: 1999, ‘DLP’. In: Proc. of the 1999 Description Logic Workshop (DL’99). pp. 9–13, CEUR Electronic Workshop Proceedings.
• 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.
• 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.
• Peltason, C.: 1991, ‘The BACK System – an Overview’. SIGART Bulletin 2(3), 114–119.
• 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.
• 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).
• Sattler, U.: 1996, ‘A Concept Language Extended with Different Kinds of Transitive Roles’. In: G. Gorz and S. Holldobler (eds.): Proc. of the 20th German Annual Conf. on Artificial Intelligence (KI’96), Vol. 1137 of Lecture Notes In Artificial Intelligence. Springer-Verlag.
• Savitch, W. J.: 1970, ‘Relationship between Nondeterministic and Deterministic Tape Complexities’. Journal of Computer and System Science 4, 177–192.
• 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.
• 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.
• Schild, K.: 1994, ‘Terminological Cycles and the Propositional μ-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.
• Schmidt-Schauß, 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.
• Schmidt-Schauß, M. and G. Smolka: 1991, ‘Attributive Concept Descriptions with Complements’. Artificial Intelligence Journal 48(1), 1–26.
• Spaan, E.: 1993, ‘The Complexity of Propositional Tense Logics’. In: M. de Rijke (ed.): Diamonds and Defaults. Kluwer Academic Publishers, pp. 287–307.
• 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.
• 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.
• Van der Hoek, W. and M. De Rijke: 1995, ‘Counting Objects’. Journal of Logic and Computation 5(3), 325–345.
• 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).