## Complexity of reasoning in Description Logics

Note: the information here is (always) incomplete and updated often
 Base description logic: Attributive Language with C omplements ALC ::=   ⊥  |  T  |  A  |  ¬C  |  C ∩ D  |  C ∪ D  |  ∃R.C  |  ∀R.C

### Concept constructors:

 F – functionality2: (≤1 R) N – (unqualified) number restrictions: (≥n R), (≤n R) Q – qualified number restrictions: (≥n R.C), (≤n R.C) O – nominals: {a} or {a1, ..., an} ("one-of") μ – least fixpoint operator: μ X.C Forbid Allow complex roles5 in number restrictions6

### Role constructors:

 I – role inverse: R— ∩ – role intersection3: R ∩ S ∪ – role union: R ∪ S ¬ – role complement: ¬R   full atomic o – role chain (composition): R o S * – reflexive-transitive closure4: R* id – concept identity: id(C)

### TBox (concept axioms):

 empty TBox acyclic TBox (A ≡ C, A is a concept name; no cycles) general TBox (C ⊆ D, for arbitrary concepts C and D)

### RBox (role axioms):

 S – role transitivity: Tr(R) H – role hierarchy: R ⊆ S

 R – complex role inclusions: R o S ⊆ R, R o S ⊆ S s – some additional features (click to see them)
You have selected a Description Logic:
Complexity7 of reasoning problems8
Concept
satisfiability

ABox
consistency

Important properties of the Description Logic
Finite model
property

Tree model
property

 Notes: The letters O, I, and Q   are customary written in various orders, e.g., ALCQIO, but SHOIQ . Here we do not reflect this tradition, but rather use a uniform naming scheme. In literature, the letter F sometimes stands for feature (dis)agreement constructor (), rather than functionality (). The presence of role intersection operator is sometimes indicated by the letter R   in literature, e.g. ALCNR := ALCN(∩). Transitive closure is usually denoted as R+. The operators * and + are expressible in terms of each other via equalities: R+ = R o R* and R* = id(T) ∪ R+. Note however that the former definition is not linearly bounded. Therefore, any complexity result for a logic with + immediately implies the same result for a logic with (*,o), but not vice versa. In the selector "Allow/forbid complex roles in number restriction", a role (expression) is called complex if it contains any role operations other than inversion (i.e. inversion is harmless (with some rare exceptions, which are pointed out in the comments to those cases)). However, in literature it is usually hard or even impossible to determine whether this assumption holds by looking at the name of a logic. For instance, ALCQIreg usually abbreviates a logic where only role names and their inverses are allowed in number restrictions; whereas in the logic ALCN(o), role composition is allowed in number restrictions. To avoid this ambiguity, the selector was introduced here explicitly. In Descripion Logics with unqualified number restrictions (N), one can independently allow/forbid role operations in value restrictions (∃R.C and ∀R.C) and/or in number restrictions (≥n R). Therefore, strictly speaking, the naming of logics should look like ALC(∪,–)N(∪,o). However, in our Navigator we are only able to display logics where role constructors are either allowed in both value and number restrictions, or in value restrictions only. What holds for the remaining case (if known) is usually said in comments. Note that this distinction is redundant for logics with qualified number restrictions Q, since ∃R.C can be expressed as ≥1 R.C. Recall that if C is a complexity class (e.g., PSpace or ExpTime), then a problem Q is said to be in C if there is an algorithm that belongs to the class C and solves the problem Q (so this is an upper bound for complexity). In particular, "decidable" is an upper bound; here C is the class of all decidable problems. A problem Q is called C-hard if all problems form the class C can be polynomially reduced to the problem Q (so this is a lower bound; in particular, the problem Q can be much harder, even undecidable!). Finally, a problem Q is called C-complete if it is both C-hard and in C. For more information on Computational Complexity Theory see []. The symbol in the above table means that the author of this web page did not find in the literature any results concerning the corresponding logic. If you have any information about that logic, the author would be grateful if you send him a mail with a reference. Sometimes, you can find out the desired complexity result using this tool by adding/removing some ingredients from the logic you consider, since it is not guaranteed that whenever this tool knows the complexity of two logics, and these complexities are the same, then it knows the complexity of all logics in between. As already pointed out, this tool is always incomplete and updated frequently.

 Additional sources Here is the list of Description Logic reasoners, together with a description of their capabilities and links to their web page. Maintained by Ulrike Sattler. Here you will find 6 diagrams depicting the complexity of concept satisfiability and ABox consistency problems for logics in between ALC and SHOIQ. There are some gaps (open problems?) in those diagrams! Here you will find a description of how ABox can be eliminated in presence of nominals (i.e., in extensions of ALCO) and how TBox can be eliminated in extensions of ALCIO, SH, and ALC(∪,*). Proofs are missing (can be found in literature below).

## References

### Books

1. Cambridge University Press, 2007 (hardback), 2010 (paperback). (624 pages)
ISBN 978-0-521-15011-8 (paperback, 2010)
ISBN 978-0-521-87625-4 (hardback, 2007)
2. Cambridge University Press, 2003. (574 pages)
ISBN 978-0-521-78176-3
3. Studies in Logic and Practical Reasoning, Volume 3, Elsevier, 2007. (1231 pages)
ISBN 978-0-444-51690-9
4. Cambridge Tracts in Theoretical Computer Science, Volume 53, Cambridge University Press, 2001. (576 pages)
ISBN 978-0-521-52714-9
5. Oxford Logic Guides, Volume 35, Oxford University Press, 1997. (620 pages)
ISBN 978-0-19-853779-3
6. Addison-Wesley Publishing Company, 1994. (523 pages)
ISBN 978-0-201-53082-7

### Theses

7. Normal multimodal logics: Automatic deduction and logic programming extension [ pdf | ps.zip ]
PhD thesis, Dipartimento di Informatica, Università degli Studi di Torino, Italy, 1998.
8. Unrestricted and finite model reasoning in class-based representation formalisms [ pdf ]
PhD Thesis, Dipartimento di Informatica e Sistemistica, Università di Roma "La Sapienza", 1996.
9. Decidability of class-based knowledge representation formalisms [ pdf | ps.zip ]
PhD Thesis, Dipartimento di Informatica e Sistemistica, Università di Roma "La Sapienza", 1995.
10. The complexity of Description Logics with concrete domains [ pdf ]
PhD Thesis, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2002.
11. Konsistenz von Wissensbasen in Beschreibungslogiken mit Rollenoperatoren [ pdf | ps.zip ]
Diploma thesis, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1997. (in German)
12. Complexity results and practical algorithms for logics in knowledge representation [ pdf ]
PhD Thesis, LuFG Theoretical Computer Science, RWTH-Aachen, Germany, 2001.

### Papers   |   all abstracts |   long names of conferences

13. A road-map on complexity for hybrid logics [ pdf | ]
@inproceedings{ArecesBlMarx1999, author = {Carlos Areces and Patrick Blackburn and Maarten Marx}, title = {A road-map on complexity for hybrid logics}, pages = {307--321}, editor = {J{\"o}rg Flum and Mario Rodriguez-Artalejo}, booktitle = {Proc.\ of the 13th Int.\ Workshop on Computer Science Logic (CSL 2005), 8th Annual Conf.\ of the European Association for Computer Science Logic (EACSL)}, series = {Lecture Notes in Computer Science}, volume = {1683}, publisher = {Springer}, year = {1999}, doi = {10.1007/3-540-48168-0_22}, ee = {http://dx.doi.org/10.1007/3-540-48168-0_22} }
Hybrid languages are extended modal languages which can refer to (or even quantify over) states. Such languages are better behaved proof theoretically than ordinary modal languages for they internalize the apparatus of labeled deduction. Moreover, they arise naturally in a variety of applications, including description logic and temporal reasoning. Thus it would be useful to have a map of their complexity-theoretic properties, and this paper provides one.

Our work falls into two parts. We first examine the basic hybrid language and its multi-modal and tense logical cousins. We show that the basic hybrid language (and indeed, multi-modal hybrid languages) are no more complex than ordinary uni-modal logic: all have PSpace-complete K-satisfiability problems. We then show that adding even one nominal to tense logic raises complexity from PSpace to ExpTime. In the second part we turn to stronger hybrid languages in which it is possible to bind nominals. We prove a general expressivity result showing that even the weak form of binding offered by the ↓ operator easily leads to undecidability.

In Jörg Flum and Mario Rodrígues-Artalejo, editors, Proc. of the 8th Annual Conference of the European Association for Computer Science Logic, Madrid, Spain, September 20-25, 1999, LNCS, vol. 1683, pp. 307–321, Springer, 1999.
14. Augmenting concept languages by transitive closure of roles: An alternative to terminological cycles [ pdf | ]
@inproceedings{Baader1991, author = {Franz Baader}, title = {Augmenting concept languages by transitive closure of roles: {A}n alternative to terminological cycles}, pages = {446--451}, editor = {John Mylopoulos and Raymond Reiter}, booktitle = {Proc.\ of the 12th Int.\ Joint Conf.\ on Artificial Intelligence (IJCAI'91)}, publisher = {Morgan Kaufmann}, year = {1991} }
In Baader (1990, 1990a), we have considered different types of semantics for terminological cycles in the concept language TLQ which allows only conjunction of concepts and value-restrictions. It turned out that greatest fixed-point semantics (gfp-semantics) seems to be most appropriate for cycles in this language. In the present paper we shall show that the concept defining facilities of FL0 with cyclic definitions and gfp-semantics can also be obtained in a different way. One may replace cycles by role definitions involving union, composition, and transitive closure of roles.

This proposes a way of retaining, in an extended language, the pleasant features of gfp-semantics for FLQ with cyclic definitions without running into the troubles caused by cycles in larger languages. Starting with the language ALC of Schmidt-Schauß & Smolka (1988) – which allows negation, conjunction and disjunction of concepts as well as value-restrictions and exists-in-restrictions – we shall disallow cyclic concept definitions, but instead shall add the possibility of role definitions involving union, composition, and transitive closure of roles. In contrast to other terminological KR-systems which incorporate the transitive closure operator for roles, we shall be able to give a sound and complete algorithm for concept subsumption.

In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence, Sydney, Australia, August 24-30, 1991, pp. 446-451, Morgan Kaufmann, 1991.
15. Expressive number restrictions in Description Logics [ pdf | ps.zip | ]
@article{BaaderSattler1999, author = {Franz Baader and Ulrike Sattler}, title = {Expressive number restrictions in Description Logics}, journal = {Journal of Logic and Computation}, volume = {9}, number = {3}, year = {1999}, pages = {319--350}, doi = {10.1093/logcom/9.3.319}, ee = {http://dx.doi.org/10.1093/logcom/9.3.319} }
Number restrictions are concept constructors that are available in almost all implemented Description Logic systems. However, they are mostly available only in a rather weak form, which considerably restricts their expressive power.

On the one hand, the roles that may occur in number restrictions are usually of a very restricted type, namely atomic roles or complex roles built using either intersection or inversion. In the present paper, we increase the expressive power of Description Logics by allowing for more complex roles in number restrictions. As role constructors, we consider composition of roles (which will be present in all our logics) and intersection, union, and inversion of roles in different combinations. We will present two decidability results (for the basic logic that extends ALC by number restrictions on roles with composition, and for one extension of this logic), and three undecidability results for three other extensions of the basic logic.

On the other hand, with the rather weak form of number restrictions available in implemented systems, the number of role successors of an individual can only be restricted by a fixed non-negative integer. To overcome this lack of expressiveness, we allow for variables ranging over the non-negative integers in place of the fixed numbers in number restrictions. The expressive power of this constructor is increased even further by introducing explicit quantifiers for the numerical variables. The Description Logic obtained this way turns out to have an undecidable satisfiability problem. For a restricted logic we show that concept satisfiability is decidable.

Journal of Logic and Computation, 9(3):319-350, 1999.
16. Automata can show PSpace results for Description Logics [ pdf | ]
@article{BaaderHlaPen2008, author = {Franz Baader and Jan Hladik and Rafael Pe{\~n}aloza}, title = {Automata can show {PSpace} results for Description Logics}, pages = {1045--1056}, journal = {Information and Computation, Special issue: First Int.\ Conf.\ on Language and Automata Theory and Applications (LATA 2007)}, volume = {206}, number = {9--10}, year = {2008}, doi = {10.1016/j.ic.2008.03.006}, ee = {http://dx.doi.org/10.1016/j.ic.2008.03.006} }
In the area of Description Logic (DL), both tableau-based and automata-based algorithms are frequently used to show decidability and complexity results for basic inference problems such as satisfiability of concepts. Whereas tableau-based algorithms usually yield worst-case optimal algorithms in the case of PSpace-complete logics, it is often very hard to design optimal tableau-based algorithms for ExpTime-complete DLs. In contrast, the automata-based approach is usually well-suited to prove ExpTime upper-bounds, but its direct application will usually also yield an ExpTime-algorithm for a PSpace-complete logic since the (tree) automaton constructed for a given concept is usually exponentially large. In the present paper, we formulate conditions under which an on-the-fly construction of such an exponentially large automaton can be used to obtain a PSpace-algorithm. We illustrate the usefulness of this approach by proving a new PSpace upper-bound for satisfiability of concepts with respect to acyclic terminologies in the DL SI, which extends the basic DL ALC with transitive and inverse roles.
Information and Computation, Special Issue: First Int. Conf. on Language and Automata Theory and Applications, LATA 2007, Tarragona, Spain, March 29 – April 4, 2007, 206(9-10):1045-1056, 2008.
• PSpace automata with blocking for Description Logics [ pdf ]
LTCS-Report 06-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2006.
17. Integrating Description Logics and action formalisms for reasoning about web services [ ps.zip | ]
@techreport{LTCSRep2004, author = {Franz Baader and Maja Mili{\v{c}}i{\'c} and Carsten Lutz and Ulrike Sattler and Frank Wolter}, title = {Integrating Description Logics and action formalisms for reasoning about web services}, type = {LTCS-Report}, number = {05-02}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, address = {Dresden, Germany}, year = {2005} }
Motivated by the need for semantically well-founded and algorithmically manageable formalisms for describing the functionality of Web services, we introduce an action formalism that is based on description logics (DLs), but is firmly grounded on research in the reasoning about action community. Our main contribution is an analysis of how the choice of the DL influences the complexity of standard reasoning tasks such as projection and executability, which are important for Web service discovery and composition.
LTCS-Report 05-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005.
18. A tableau calculus for multimodal logics and some (un)decidability results [ pdf | ]
@inproceedings{BaldoniTableaux98, author = {Matteo Baldoni and Laura Giordano and Alberto Martelli}, title = {A tableau calculus for multimodal logics and some (un)decidability results}, pages = {44--59}, editor = {Harrie de Swart}, booktitle = {Proc.\ of the Int.\ Conf.\ on Analytic Tableaux and Related Methods ({TABLEAUX}'98)}, series = {Lecture Notes in Artificial Intelligence}, volume = {1397}, publisher = {Springer}, year = {1998}, doi = {10.1007/3-540-69778-0_13}, ee = {http://dx.doi.org/10.1007/3-540-69778-0_13} }
In this paper we present a prefixed analytic tableau calculus for a class of normal multimodal logics and we present some results about decidability and undecidability of this class. The class is characterized by axioms of the form [t1]...[tn] → [s1]...[sm]φ, called inclusion axioms, where the ti's and sj's are constants. This class of logics, called grammar logics, was introduced for the first time by Fariñas del Cerro and Penttonen to simulate the behaviour of grammars in modal logics, and includes some well-known modal systems. The prefixed tableau method is used to prove the undecidability of modal systems based on unrestricted, context sensitive, and context free grammars. Moreover, we show that the class of modal logics, based on right-regular grammars, are decidable by means of the filtration methods, by defining an extension of the Fischer-Ladner closure.
In H. de Swart, editor, Proc. of the Int. Conf. on Analytic Tableaux and Related Methods, Oisterwijk, The Netherlands, May 5-8, 1998. LNAI, vol. 1397, pp. 44–59. Springer, 1998.
19. The undecidability of the dominoe problem [ pdf | ]
@article{Berger1966, author = {Robert Berger}, title = {The undecidability of the dominoe problem}, journal = {Memoirs of the American Mathematical Society}, volume = {66}, year = {1966}, pages = {1--72}, doi = {10.1090/memo/0066}, ee = {http://dx.doi.org/10.1090/memo/0066} }
A domino set is a finite set of square plates, the dominoes all of the same size, whose edges are marked with symbols, each plate in a different manner. Assume we have an unlimites number of copies of each type of domino. We see to assemble the copies (also called dominoes) on an infinite plane, ruled into squares the size of one domino, according to the following rules:
•  No dominoe may be rotated or reflected.
•  A domino must be placed exactly over a ruled square.
•  The symbols on adjacent domino edges must match.
•  Every square must be covered with a domino.
The domino set is called solvable if and only if the dominoes can be so assembled.

The Domino Problem deals with the class of all domino sets. It consists of deciding, for each domino set, whether or not it is solvable. We say that the Domino Problem is decidable or undecidable according to whether there exists or does not exist an algorithm which, given the specifications of an arbitrary domino set, will decide whether or not the set is solvable. This paper proves that the Domino Problem is undecidable.

, 66:1–72, 1966.
20. On the undecidability of logics with converse, nominals, recursion and counting [ pdf | ]
@article{BonattiPeron2004, author = {Piero A. Bonatti and A.Peron}, title = {On the undecidability of logics with converse, nominals, recursion and counting}, journal = {Artificial Intelligence}, volume = {158}, number = {1}, year = {2004}, pages = {75--96}, doi = {10.1016/j.artint.2004.04.012}, ee = {http://dx.doi.org/10.1016/j.artint.2004.04.012} }
The evolution of Description Logics (DLs) and Propositional Dynamic Logics produced a hierarchy of decidable logics with multiple maximal elements. It would be desirable to combine different maximal logics into one super-logic, but then inference may turn out to be undecidable. Then it is important to characterize the decidability threshold for these logics. In this perspective, an interesting open question pointed out by Sattler and Vardi [IJCAR 2001] is whether inference in a hybrid μ-calculus with restricted forms of graded modalities is decidable, and which complexity class it belongs to.

In this paper we improve a previous result [Bonatti, IJCAI 2003] and prove that this calculus and the corresponding DL μALCIOfa are undecidable. We show also that nested fixpoints are not necessary for undecidability.

Artificial Intelligence, 158(1):75–96, 2004.
21. The complexity of enriched μ-calculi [ pdf | ]
@inproceedings{BonattiLutzICALP06, author = {Piero A. Bonatti and Carsten Lutz and Aniello Murano and Moshe Y. Vardi}, title = {The complexity of enriched $\mu$-calculi}, pages = {540--551}, editor = {Michele Bugliesi and Bart Preneel and Vladimiro Sassone and Ingo Wegener}, booktitle = {Proc.\ of the 33rd Int.\ Colloquium on Automata, Languages and Programming (ICALP~2006)}, series = {Lecture Notes in Computer Science}, volume = {4052}, publisher = {Springer}, year = {2006}, doi = {10.1007/11787006_46}, ee = {http://dx.doi.org/10.1007/11787006_46} }
The fully enriched μ-calculus is the extension of the propositional μ-calculus with inverse programs, graded modalities, and nominals. While satisfiability in several expressive fragments of the fully enriched μ-calculus is known to be decidable and ExpTime-complete, it has recently been proved that the full calculus is undecidable.

In this paper, we study the fragments of the fully enriched μ-calculus that are obtained by dropping at least one of the additional constructs. We show that, in all fragments obtained in this way, satisfiability is decidable and ExpTime-complete. Thus, we identify a family of decidable logics that are maximal (and incomparable) in expressive power.

Our results are obtained by introducing two new automata models, showing that their emptiness problems are ExpTime-complete, and then reducing satisfiability in the relevant logics to this problem. The automata models we introduce are two-way graded alternating parity automata over infinite trees (2GAPT) and fully enriched automata (FEA) over infinite forests. The former are a common generalization of two incomparable automata models from the literature. The latter extend alternating automata in a similar way as the fully enriched μ-calculus extends the standard μ-calculus.

In Proc. of the 33rd Int. Colloquium on Automata, Languages and Programming, Venice, Italy, July 9-16, 2006, LNCS, vol. 4052, pp. 540-551, Springer, 2006.
22. Decidable reasoning in terminological knowledge representation systems [ pdf | ]
@article{Buchheit_etal_1993a, author = {Martin Buchheit and Francesco M. Donini and Andrea Schaerf}, title = {Decidable reasoning in terminological knowledge representation systems}, journal = {Journal of Artificial Intelligence Research}, volume = {1}, year = {1993}, pages = {109--138}, doi = {10.1613/jair.21}, ee = {http://dx.doi.org/10.1613/jair.21} }
Terminological knowledge representation systems (TKRSs) are tools for designing and using knowledge bases that make use of terminological languages (or concept languages). We analyze from a theoretical point of view a TKRS whose capabilities go beyond the ones of presently available TKRSs. The new features studied, often required in practical applications, can be summarized in three main points. First, we consider a highly expressive terminological language, called ALCNR , including general complements of concepts, number restrictions and role conjunction. Second, we allow to express inclusion statements between general concepts, and terminological cycles as a particular case. Third, we prove the decidability of a number of desirable TKRS-deduction services (like satisfiability, subsumption and instance checking) through a sound, complete and terminating calculus for reasoning in ALCNR -knowledge bases. Our calculus extends the general technique of constraint systems. As a byproduct of the proof, we get also the result that inclusion statements in ALCNR  can be simulated by terminological cycles, if descriptive semantics is adopted.
• Technical report: [ pdf ]
Research Report RR-93-10, Deutsches Forschungszentrum für Künstliche Intelligenz (DFKI), Saarbrucken (Germany), 1993.
• An abridged version appeared in Proc. of the 13th Int. Joint Conf. on Artificial Intelligence, Chambéry, France, August 28 – September 3, 1993, pp. 704-709, Morgan Kaufmann, 1993.
23. Finite model reasoning in Description Logics [ pdf | ]
@inproceedings{Calvanese1996a, author = {Diego Calvanese}, title = {Finite model reasoning in Description Logics}, pages = {292--303}, editor = {Luigia Carlucci Aiello and Jon Doyle and Stuart C. Shapiro}, booktitle = {Proc.\ of the 5th Int.\ Conf.\ on Principles of Knowledge Representation and Reasoning (KR'96)}, publisher = {Morgan Kaufmann}, year = {1996} }
For the basic Description Logics reasoning with respect to finite models amounts to reasoning with respect to arbitrary ones, but finiteness of the domain needs to be considered if expressivity is increased and the finite model property fails. Procedures for reasoning with respect to arbitrary models in very expressive Description Logics have been developed, but these are not directly applicable in the finite case. We first show that we can nevertheless capture a restricted form of finiteness and represent finite modeling structures such as lists and trees, while still reasoning with respect to arbitrary models. The main result of this paper is a procedure to reason with respect to finite models in an expressive Description Logic equipped with inverse roles, cardinality constraints, and in which arbitrary inclusions between concepts can be specified without any restriction. This provides the necessary expressivity to go beyond most semantic and object-oriented Database models, and capture several useful extensions.
In L.C.Aiello, Jon Doyle, and Stuart C. Shapiro, editors, Proc. of the 5th Int. Conf. on the Principles of Knowledge Representation and Reasoning, Cambridge, Massachusetts, USA, November 5-8, 1996, pp. 292-303, Morgan Kaufmann, 1996.
24. Reasoning in expressive Description Logics with fixpoints based on automata on infinite trees [ pdf | ]
@inproceedings{CalvaneseEtAl1999c, author = {Diego Calvanese and Giuseppe De Giacomo and Maurizio Lenzerini}, title = {Reasoning in expressive Description Logics with fixpoints based on automata on infinite trees}, pages = {84--89}, editor = {Thomas Dean}, booktitle = {Proc.\ of the 16th Int.\ Joint Conf.\ on Artificial Intelligence (IJCAI'99)}, publisher = {Morgan Kaufmann}, year = {1999} }
In the last years, the investigation on Description Logics (DLs) has been driven by the goal of applying them in several areas, such as software engineering, information systems, databases, information integration, and intelligent access to the web. The modeling requirements arising in the above areas have stimulated the need for very rich languages, including fixpoint constructs to represent recursive structures. We study a DL comprising the most general form of fixpoint constructs on concepts, all classical concept forming constructs, plus inverse roles, n-ary relations, qualified number restrictions, and inclusion assertions. We establish the ExpTime decidability of such logic by presenting a decision procedure based on a reduction to nonemptiness of alternating automata on infinite trees. We observe that this is the first decidability result for a logic combining inverse roles, number restrictions, and general fixpoints.
In Proc. of the 16th Int. Joint Conf. on Artificial Intelligence, Stockholm, Sweden, July 31 – August 6, 1999, pp. 84–89, Morgan Kaufmann, 1999.
25. Reasoning in expressive Description Logics [ pdf | ]
@incollection{HandbookARCh23, author = {Diego Calvanese and Giuseppe De Giacomo and Maurizio Lenzerini and Daniele Nardi}, title = {Reasoning in expressive Description Logics}, chapter = {23}, pages = {1581--1634}, editor = {Alan Robinson and Andrei Voronkov}, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science Publishers}, year = {2001} }
In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, pp. 1581–1634 (Chapter 23). Elsevier Science Publishers, 2001.
26. Nondeterministic Propositional Dynamic Logic with intersection is decidable [ pdf | ]
@inproceedings{Danecki1984, author = {Ryszard Danecki}, title = {Nondeterministic Propositional Dynamic Logic with intersection is decidable}, pages = {34--53}, editor = {Andrzej Skowron}, booktitle = {Proc.\ of the 5th Symposium on Computation Theory}, series = {Lecture Notes in Computer Science}, volume = {208}, publisher = {Springer}, year = {1985}, doi = {10.1007/3-540-16066-3_5}, ee = {http://dx.doi.org/10.1007/3-540-16066-3_5} }
Propositional Dynamic Logic (PDL) of [Fisher, Ladner, 1979] defines meaning of programs in terms of binary input-output relations. Basic regular operations on programs are interpreted as superposition, union, and reflexive-transitive closure of relations. The intersection, cf. [Harel 1983], is a binary program forming functor ab with the meaning given by the set-theoretical intersection of relations corresponding to programs a and b. By adding intersection of programs to PDL we obtain a programming logic called PDL with intersection. Harel [Harel 1983] has proved that the problem of whether or not a formula of PDL with intersection has a deterministic model is highly undecidable (Σ11-hard). The present paper shows that in the general case (nondeterministic models allowed) the satisfiability problem for PDL with intersection is decidable in time double exponential in the length of the formula tested. In comparison with PDL with strong loop predicate [Danecki 1984], this is more powerful and interesting example of a logic which is decidable in contrast to its deterministic case and despite the lack of finite and even tree model properties.
In A. Skowron, editor, Proc. of the 5th Symposium on Computation Theory, Zaborów, Poland, December 3-8, 1984, LNCS, vol. 208, pp. 34–53, Springer, 1985.
27. Boosting the correspondence between Description Logics and Propositional Dynamic Logics [ pdf | ]
@inproceedings{DeGiacomoLenzerini1994a, author = {Giuseppe De Giacomo and Maurizio Lenzerini}, title = {Boosting the correspondence between Description Logics and Propositional Dynamic Logics}, pages = {205--212}, editor = {Barbara Hayes-Roth and Richard E. Korf}, booktitle = {Proc.\ of the 12th Nat.\ Conf.\ on Artificial Intelligence (AAAI~1994)}, volume = {1}, publisher = {AAAI Press / The MIT Press}, year = {1994}, ee = {http://www.aaai.org/Library/AAAI/1994/aaai94-032.php} }
One of the main themes in the area of Terminological Reasoning has been to identify description logics (DLs) that are both very expressive and decidable. A recent paper by Schild showed that this issue can be profitably addressed by relying on a correspondence between DLs and propositional dynamic logics (PDL). However Schild left open three important problems, related to the translation into PDLs of functional restrictions on roles (both direct and inverse), number restrictions, and assertions on individuals. The work reported in this paper presents a solution to these problems. The results have a twofold significance. From the standpoint of DLs, we derive decidability and complexity results for some of the most expressive logics appeared in the literature, and from the standpoint of PDLs, we derive a general methodology for the representation of several forms of program determinism and for the specification of partial computations.
In Proc. of the 12th Nat. Conf. on Artificial Intelligence, Seattle, Washington, July 31 – August 4, 1994, pp. 205-212, AAAI Press / The MIT Press, 1994.
28. Eliminating “converse” from converse PDL [ pdf | ]
@article{DeGiacomoLenzerini1996a, author = {Giuseppe De Giacomo}, title = {Eliminating converse'' from converse {PDL}}, journal = {Journal of Logic, Language, and Information}, volume = {5}, number = {2}, year = {1996}, pages = {193--208}, doi = {10.1007/BF00173700}, ee = {http://dx.doi.org/10.1007/BF00173700} }
In this paper we show that it is possible to eliminate the “converse” operator from the propositional dynamic logic CPDL (Converse PDL), without compromising the soundness and completeness of inference for it. Specifically we present an encoding of CPDL formulae into PDL that eliminates the converse programs from a CPDL formula, but adds enough information so as not to destroy its original meaning with respect to satisfiability, validity, and logical implication. Notably, the resulting PDL formula is polynomially related to the original one. This fact allows one to build inference procedures for CPDL, by encoding CPDL formulae into PDL, and then running an inference procedure for PDL.
, 5(2):193–208, 1996.
29. TBox and ABox reasoning in expressive Description Logics [ pdf | ]
@inproceedings{DeGiacomoLenzerini1996, author = {Giuseppe De Giacomo and Maurizio Lenzerini}, title = {{TB}ox and {AB}ox reasoning in expressive Description Logics}, pages = {316--327}, editor = {Luigia Carlucci Aiello and Jon Doyle and Stuart C. Shapiro}, booktitle = {Proc.\ of the 5th Int.\ Conf.\ on Principles of Knowledge Representation and Reasoning (KR'96)}, publisher = {Morgan Kaufmann}, year = {1996} }
A Description Logic (DL) system is characterized by four fundamental aspects: the set of constructs used in concept and role expressions, the kind of assertions allowed in the TBox (assertions on concepts) and the ABox (assertions on individuals), and the inference mechanisms for reasoning on both the TBox and the ABox. Most of the research done in the last decade made several simplifying assumptions on the above aspects. However, the recent interest in DLs exhibited in many application areas (databases, software engineering, intelligent access to the network, planning, etc.) calls for investigating DL systems with full capabilities. The work presented in this paper represents a step in this direction. We present a sound, complete, and terminating (in worst-case ExpTime) inference procedure that solves the problem of reasoning in a DL system with the following characteristics: it comes equipped with a very expressive language, it allows the most general form of TBox assertions, and it takes into account instance assertions on both concepts and roles in the ABox.
In L.C.Aiello, Jon Doyle, and Stuart C.Shapiro, editors, Proc. of the 5th Int. Conf. on the Principles of Knowledge Representation and Reasoning, Cambridge, Massachusetts, U.S.A., November 5-8, 1996. pp. 316-327. Morgan Kaufmann, 1996.
30. A uniform framework for concept definitions in Description Logics [ pdf | ]
@article{DeGiacomoLenzerini1997, author = {Giuseppe De Giacomo and Maurizio Lenzerini}, title = {A uniform framework for concept definitions in Description Logics}, journal = {Journal of Artificial Intelligence Research}, volume = {6}, year = {1997}, pages = {87--110}, doi = {10.1613/jair.334}, ee = {http://dx.doi.org/10.1613/jair.334} }
Most modern formalisms used in Databases and Artificial Intelligence for describing an application domain are based on the notions of class (or concept) and relationship among classes. One interesting feature of such formalisms is the possibility of defining a class, i.e., providing a set of properties that precisely characterize the instances of the class. Many recent articles point out that there are several ways of assigning a meaning to a class definition containing some sort of recursion. In this paper, we argue that, instead of choosing a single style of semantics, we achieve better results by adopting a formalism that allows for different semantics to coexist. We demonstrate the feasibility of our argument, by presenting a knowledge representation formalism, the description logic μALCQ , with the above characteristics. In addition to the constructs for conjunction, disjunction, negation, quantifiers, and qualified number restrictions, μALCQ  includes special fixpoint constructs to express (suitably interpreted) recursive definitions. These constructs enable the usual frame-based descriptions to be combined with definitions of recursive data structures such as directed acyclic graphs, lists, streams, etc. We establish several properties of μALCQ , including the decidability and the computational complexity of reasoning, by formulating a correspondence with a particular modal logic of programs called the modal μ-calculus.
Journal of Artificial Intelligence Research, vol. 6, pp. 87–110, 1997.
31. The complexity of regularity in grammar logics and related modal logics [ pdf | ]
@article{DemriJLC2001, author = {Stéphane Demri}, title = {The complexity of regularity in grammar logics and related modal logics}, journal = {Journal of Logic and Computation}, volume = {11}, number = {6}, year = {2001}, pages = {933--960}, doi = {10.1093/logcom/11.6.933}, ee = {http://dx.doi.org/10.1093/logcom/11.6.933} }
A modal reduction principle of the form [i1]...[in]p → [j1]...[jn']p can be viewed as a production rule i1...inj1...jn' in a formal grammar. We study the extensions of the multimodal logic Km with m independent K modal connectives by finite addition of axiom schemes of the above form such that the associated finite set of production rules forms a regular grammar. We show that given a regular grammar G and a modal formula φ, deciding whether the formula is satisfiable in the extension of Km with axiom schemes from G can be done in deterministic exponential-time in the size of G and φ, and this problem is complete for this complexity class. Such an extension of Km is called a regular grammar logic. The proof of the exponential-time upper bound is extended to PDL-like extensions of Km and to global logical consequence and global satisfiability problems. Using an equational characterization of context-free languages, we show that by replacing the regular grammars by linear ones, the above problem becomes undecidable. The last part of the paper presents non-trivial classes of exponential time complete regular grammar logics.
Journal of Logic and Computation, 11(6):933–960, 2001.
32. A new mapping from ALCI  to ALC  [ pdf | ]
@inproceedings{DingHaWiDL2007, author = {Yu Ding and Volker Haarslev and Jiewen Wu}, title = {A new mapping from $\mathcal{ALCI}$ to $\mathcal{ALC}$}, editor = {Diego Calvanese and Enrico Franconi and Volker Haarslev and Domenico Lembo and Boris Motik and Anni-Yasmin Turhan and Sergio Tessaris}, booktitle = {Proc.\ of the 20th Int.\ Workshop on Description Logics (DL~2007)}, series = {CEUR Workshop Proceedings}, volume = {250}, publisher = {CEUR-WS.org}, year = {2007}, ee = {http://ceur-ws.org/Vol-250/paper_32.pdf} }
It is well known that a correspondence theory for description logics (DLs), propositional modal logics (MLs) and propositional dynamic logics (PDLs) was given in [Schild 1991] and that an axiomatic system for a description logic with inverse roles was presented in the same paper. Schild's paper covers what is to be discussed in this paper although his paper did not mention nominals as well as expressive roles explicitly. On the other hand, reductions to eliminate converse programs (inverse roles in DLs) are known even for full PDL (ALCI reg); the original reduction from converse PDL to PDL was in [Giacomo 1996]. Moreover, a direct tableaux method for converse PDL and further discussions on the elimination of converse programs were given in [Giacomo, Massacci, 2000]. Besides graded modalities, it was pointed out in [Giacomo 1996] that the previous reduction technique is also applicable to nominals.

This paper shares some viewpoints well made in [Giacomo 1996]. The proposed mapping process here is based on the simple idea to capture possible back-propagation caused by the use of inverse roles. This process consists of three steps, tagging, recording, polarisation, which are introduced below. Concept expressions / formulae are assumed to be in negation norm form (NNF). For simplicity, existential restrictions and universal restrictions are called modal constraints somewhere. We refer to [DL Handbook] for usual background knowledge on description logics (DLs).

In Proc. of the 2007 Int. Workshop on Description Logics, Brixen-Bressanone, near Bozen-Bolzano, Italy, June 8-10, 2007, vol. 250 in CEUR, pp. 267–274, 2007.
33. ExpTime tableaux for ALC  [ pdf | ]
@article{DoniniMassacci2000, author = {Francesco M. Donini and Fabio Massacci}, title = {ExpTime tableaux for $\mathcal{ALC}$}, journal = {Artificial Intelligence}, volume = {124}, number = {1}, year = {2000}, pages = {87--138}, doi = {10.1016/S0004-3702(00)00070-9}, ee = {http://dx.doi.org/10.1016/S0004-3702(00)00070-9} }
The last years have seen two major advances in Knowledge Representation and Reasoning. First, many interesting problems (ranging from Semi-structured Data to Linguistics) were shown to be expressible in logics whose main deductive problems are ExpTime-complete. Second, experiments in automated reasoning have substantially broadened the meaning of “practical tractability”. Instances of realistic size for PSpace-complete problems are now within reach for implemented systems.

Still, there is a gap between the reasoning services needed by the expressive logics mentioned above and those provided by the current systems. Indeed, the algorithms based on tree-automata, which are used to prove ExpTime-completeness, require exponential time and space even in simple cases. On the other hand, current algorithms based on tableau methods can take advantage of such cases, but require double exponential time in the worst case.

We propose a tableau calculus for the description logic ALC for checking the satisfiability of a concept with respect to a TBox with general axioms, and transform it into the first simple tableau-based decision procedure working in single exponential time.

To guarantee the ease of implementation, we also discuss the effects that optimizations (propositional backjumping, simplification, semantic branching, etc.) might have on our complexity result, and introduce a few optimizations ourselves.

Artificial Intelligence, 124(1):87-138, 2000.
34. Propositional Dynamic Logic of regular programs [ pdf | ]
@article{FischerLadner1979, author = {Michael J. Fischer and Richard E. Ladner}, title = {Propositional Dynamic Logic of regular programs}, journal = {Journal of Computer and System Science}, volume = {18}, number = {2}, year = {1979}, pages = {194--211}, doi = {10.1016/0022-0000(79)90046-1}, ee = {http://dx.doi.org/10.1016/0022-0000(79)90046-1} }
We introduce a fundamental propositional logical system based on modal logic for describing correctness, termination and equivalence of programs. We define a formal syntax and semantics for the propositional dynamic logic of regular programs and give several consequences of the definition. Principal conclusions are that deciding satisfiability of length n formulas requires time dn/logn for some d > 1, and that satisfiability can be decided in nondeterministic time cn for some c. We provide applications of the decision procedure to regular expressions, Ianov schemes, and classical systems of modal logic.
35. Modal environment for Boolean speculations [ pdf | ]
@incollection{Gargov_etal_1987, author = {George Gargov and Solomon Passy and Tinko Tinchev}, title = {Modal environment for {B}oolean speculations}, pages = {253--263}, editor = {Dimiter G. Skordev}, booktitle = {Mathematical Logic and Its Applications}, publisher = {Plenum Press}, year = {1987}, doi = {10.1007/978-1-4613-0897-3_17}, ee = {http://dx.doi.org/10.1007/978-1-4613-0897-3_17} }
The common form of a mathematical theorem consists in that "the truth of some properties for some objects is necessary and/or sufficient condition for other properties to hold for other objects". To formalize this, one happens to resort to Kripke modal logic K which, having in the syntax the notions of 'property' and 'necessity', appears to provide a reliable metamathematical fundament. In this paper we challenge this reliability. We propose two different approaches each claiming better formal treatment of the state of affairs. The first approach is in formalizing the notion of 'sufficiency' (which remains beyond the capacities of K), and consequently of 'sufficiency' and 'necessity' in a joint context. The second is our older idea to formalize the notion of 'object' in the same modal spirit. Having 'property, object, sufficiency, necessity', we establish some basic results and profess to properly formalize the everyday metamathematical reason.
In Dimiter G. Skordev, editor, Mathematical Logic and its Applications, Proc. of the Advanced International Summer School and Conference dedicated to the 80th anniversary of Kurt Gödel's birth, Druzhba near Varna, Bulgaria, September 24 – October 4, 1986, pp. 253-263, Plenum Press, New York, 1987.
36. PDL with intersection and converse is 2EXP-complete [ pdf | ]
@inproceedings{GoLoLuICPDL2007, author = {Stefan G{\"o}ller and Markus Lohrey and Carsten Lutz}, title = {{PDL} with intersection and converse is {2EXP}-complete}, pages = {198--212}, editor = {Helmut Seidl}, booktitle = {Proc.\ of the 10th Int.\ Conf.\ on Foundations of Software Science and Computational Structures (FoSSaCS 2007)}, series = {Lecture Notes in Computer Science}, volume = {4423}, publisher = {Springer}, year = {2007}, doi = {10.1007/978-3-540-71389-0_15}, ee = {http://dx.doi.org/10.1007/978-3-540-71389-0_15} }
We study the complexity of satisfiability in the expressive extension ICPDL of PDL (Propositional Dynamic Logic), which admits intersection and converse as program operations. Our main result is containment in 2EXP, which improves the previously known non-elementary upper bound and implies 2EXP-completeness due to an existing lower bound for PDL with intersection. The proof proceeds by showing that every satisfiable ICPDL formula has a model of tree-width at most two and then giving a reduction to the (non-)emptiness problem for alternating two-way automata on infinite trees. In this way, we also reprove in an elegant way Danecki's difficult result that satisfiability for PDL with intersection is in 2EXP.

Note: Here EXP means ExpTime, and 2EXP means ExpExpTime. (E.Z.)

In Helmut Seidl, editor, Proc. of the 10th Int. Conf. on Foundations of Software Science and Computation Structures, Braga, Portugal, 24 March – 1 April, 2007, LNCS, vol. 4423, pp. 198–212, Springer, 2007.
37. ExpTime tableaux with global caching for Description Logics
with transitive roles, inverse roles and role hierarchies
[ pdf | ]
@inproceedings{Gore_Nguyen_2007, author = {Rajeev Gor{\'e} and Linh Anh Nguyen}, title = {{ExpTime} tableaux with global caching for Description Logics with transitive roles, inverse roles and role hierarchies}, pages = {133--148}, editor = {Nicola Olivetti}, booktitle = {Proc.\ of the 16th Int.\ Conf.\ on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2007)}, series = {Lecture Notes in Computer Science}, volume = {4548}, publisher = {Springer}, year = {2007}, doi = {10.1007/978-3-540-73099-6_12}, ee = {http://dx.doi.org/10.1007/978-3-540-73099-6_12} }
The description logic SHI  extends the basic description logic ALC  with transitive roles, role hierarchies and inverse roles. The known tableau-based decision procedure for SHI  exhibit (at least) NExpTime behaviour even though SHI  is known to be ExpTime-complete. The automata-based algorithms for SHI  often yield optimal worst-case complexity results, but do not behave well in practice since good optimisations for them have yet to be found. We extend our method for global caching in ALC  to SHI  by adding analytic cut rules, thereby giving the first ExpTime tableau-based decision procedure for SHI , and showing one way to incorporate global caching and inverse roles.
In the Int. Conf. on Analytic Tableaux and Related Methods, Aix en Provence, France, July 3-6, 2007. LNCS, vol. 4548, pp. 133–148, Springer, 2007.
Note: This logic is known as SHI .
38. Two-variable logic with counting is decidable [ pdf | ps.zip | ]
@inproceedings{Gradel_etal_1997b, author = {Erich Gr{\"a}del and Martin Otto and Eric Rosen}, title = {Two-variable logic with counting is decidable}, pages = {306--317}, editor = {Glynn Winskel}, booktitle = {Proc.\ of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97)}, publisher = {IEEE Computer Society Press}, year = {1997}, doi = {10.1109/LICS.1997.614957}, ee = {http://dx.doi.org/10.1109/LICS.1997.614957} }
We prove that the satisfiability problem for C2 is decidable. C2 is first-order logic with only two variables in the presence of arbitrary counting quantifiers ∃m, m≥1. It considerably extends L2, plain first-order with only two variables, which is known to be decidable by a result of Mortimer. Unlike L2, C2 does not have the finite model property. As C2 extends L2 by expressive means for counting, significant applications arise from the fact that C2 embeds corresponding counting extensions of modal logics.
In Proc. of the 12th IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 – July 2, 1997, pp. 306-317, IEEE Computer Society Press, 1997.
39. On expressive number restrictions in Description Logics [ pdf | ]
@inproceedings{GrandiDL2001, author = {Fabio Grandi}, title = {On expressive number restrictions in Description Logics}, pages = {56--65}, editor = {Carole Goble and Deborah L. McGuinness and Ralf M{\"o}ller and Peter F. Patel-Schneider}, booktitle = {Proc.\ of the 14th Int.\ Workshop on Description Logics (DL~2001)}, series = {CEUR Workshop Proceedings}, volume = {49}, publisher = {CEUR-WS.org}, year = {2001}, ee = {http://ceur-ws.org/Vol-49/Grandi-56start.ps} }
We consider expressive Description Logics (ALCN ) allowing for number restrictions on complex roles built with combinations of role constructors. In particular, we are mainly interested in Logics (called ALCN ) allowing for the same kind of complex roles both in number and in value restrictions, which represent very expressive description languages and can be shown very useful for applications.

We investigate the computational properties of various ALCN  extensions and slightly improve the (un)decidability results following from the study published by Baader and Sattler in 1999. In particular, we will show by reduction of a domino problem that ALCN (+,∪) and ALCN (+,∩) are undecidable.

In Proc. of the 2001 Int. Workshop on Description Logics, Stanford University, California, USA, August 1-3, 2001, vol. 49 in CEUR, pp. 56–65, 2001.
40. On expressive Description Logics with composition of roles in number restrictions [ pdf | ]
@inproceedings{GrandiLPAR2002, author = {Fabio Grandi}, title = {On expressive Description Logics with composition of roles in number restrictions}, pages = {202--215}, editor = {Matthias Baaz and Andrei Voronkov}, booktitle = {Proc.\ of the 9th Int.\ Conf.\ on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR~2002)}, series = {Lecture Notes in Computer Science}, volume = {2514}, publisher = {Springer}, year = {2002}, doi = {10.1007/3-540-36078-6_14}, ee = {http://dx.doi.org/10.1007/3-540-36078-6_14} }
Description Logics are knowledge representation formalisms which have been used in a wide range of application domains. Owing to their appealing expressiveness, we consider in this paper extensions of the well-known concept language ALC allowing for number restrictions on complex role expressions. These have been first introduced by Baader and Sattler as ALCN (M) languages, with the adoption of role constructors M ⊆ {o,,∪,∩}.

In particular, as far as languages equipped with role composition are concerned, they showed in 1999 that, although ALCN(o) is decidable, the addition of other operators may easily lead to undecidability: in fact, ALCN (o,∩) and ALCN (o,,∪) were proved undecidable.

In this work, we further investigate the computational properties of the ALCN  family, aiming at narrowing the decidability gap left open by Baader and Sattler's results. In particular, we will show that ALCN (o) extended with inverse roles both in number and in value restrictions becomes undecidable, whereas it can be safely extended with qualified number restrictions without losing decidability of reasoning.

In M. Baaz, A. Voronkov, editors, Proc. of the 9th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, Tbilisi, Georgia, October 14-18, 2002. LNAI, vol. 2514, pp. 202–215, Springer, Berlin, 2002.
• Technical report: [ pdf ]
• Decidability of expressive Description Logics with role compositions (extended abstract) [ ps.zip ]
In Proc. of the 2002 Int. Workshop on Description Logics, Toulouse, France, April 19-21, 2002, vol. 53 in CEUR, 2002.
41. [ pdf | ]
@incollection{Harel1984, author = {David Harel}, title = {Dynamic Logic}, pages = {497--604}, editor = {Dov Gabbay and Franz Guenther}, booktitle = {Handbook of Philosophical Logic}, edition = {1st}, volume = {2}, publisher = {Reidel}, address = {Dordrecht, Holland}, year = {1984} }
No abstract available.
In D. Gabbay and F. Guenther, editors, Handbook of Philosophical Logic, vol. 2, pp. 497–604. Reidel, Dordrecht, Holland, 1984.
42. A tableau system for the Description Logic SHIO [ ps.zip | ]
@inproceedings{HladikIJCAR2004, author = {Jan Hladik}, title = {A tableau system for the Description Logic $\mathcal{SHIO}$}, pages = {21--25}, editor = {Ulrike Sattler}, booktitle = {Contributions to the Doctoral Programme of the 2nd Int.\ Joint Conf.\ on Automated Reasoning (IJCAR~2004)}, series = {CEUR Workshop Proceedings}, volume = {106}, publisher = {CEUR-WS.org}, year = {2004}, ee = {http://ceur-ws.org/Vol-106/05-hladik.ps} }
For the satisfiability test of description logics (DLs), there are two prominent families of algorithms with complementary advantages and disadvantages: firstly, automata-based algorithms, which translate a DL expression φ into an automaton Aφ which accepts all (abstractions of) models for φ, so that the satisfiability test for φ can be reduced to the emptiness test of Aφ; and secondly, tableau algorithms, which incrementally create a tree-shaped (pre-)model for φ using a set of rules labelling each tree node with the appropriate subformulas of φ. In short, the advantages of automata algorithms are on the theoretical side, because in many cases the proofs are very elegant and offer tight complexity bounds (in particular for ExpTime-complete logics), whereas the advantages of tableau algorithms are on the practical side, since they are well suited for implementation and optimisation. In contrast, intuitive automata algorithms usually require exponential time also in the best case, and thus an efficient implementation requires considerable modifications.

For this reason, an approach combining both advantages is highly desirable. In [3], we introduced tableau systems (TS), a framework for tableau algorithms. If a tableau algorithm can be described within this framework, the existence of an automata algorithm (and thus the ExpTime upper bound) directly follows. Moreover, only soundness and completeness of the tableau algorithm have to be proved; termination and a practical procedure to ensure termination, called a blocking test, also follows from the prerequisites of the framework.

As an example for the usefulness of this framework, we present in this paper a TS for SHIO, an expressive DL whose computational properties to the best of our knowledge have not been analysed so far. The purpose of this is two-fold: firstly, we obtain that SHIO satisfiability is ExpTime-complete and can be decided by a tableau algorithm. Secondly, the succinctness of the proofs demonstrates how our framework simplifies the design of tableau algorithms.

[3] F.Baader, J.Hladik, C.Lutz, and F.Wolter. From tableaux to automata for description logics. Fundamenta Informaticae, 57:1-33, 2003.

In Proc. of the Doctoral Programme of the 2nd Int. Joint Conf. on Automated Reasoning, Cork, Ireland, July 4-8, 2004. vol. 106 in CEUR, pp. 21-25, 2004.
43. Tableau systems for SHIO and SHIQ [ pdf | ]
@inproceedings{HladikModelDL2004, author = {Jan Hladik and J{\"o}rg Model}, title = {Tableau systems for $\mathcal{SHIO}$ and $\mathcal{SHIQ}$}, pages = {168--177}, editor = {Volker Haarslev and Ralf M{\"o}ller}, booktitle = {Proc.\ of the 17th Int.\ Workshop on Description Logics (DL~2004)}, series = {CEUR Workshop Proceedings}, volume = {104}, publisher = {CEUR-WS.org}, year = {2004}, ee = {http://ceur-ws.org/Vol-104/22Hladik-final.pdf} }
Two prominent families of algorithms for the satisfiability test of Description Logics are automata-based algorithms, which translate a concept C into an automaton AC accepting all (abstractions of) models for C, and tableau algorithms, which incrementally create a tree-shaped (pre-)model for C using a set of completion rules. In short, the advantages of automata algorithms are on the theoretical side, because in many cases the proofs are very elegant and provide tight complexity bounds (in particular for ExpTime-complete logics), whereas the advantages of tableau algorithms are on the practical side, since they are well suited for implementation and optimisation.

Thus, an approach combining both advantages is highly desirable. In [1], we introduced tableau systems (TS), a framework for tableau algorithms. From a TS for a DL L, we can derive an automata algorithm deciding satisfiability of L inputs in exponential time, and a tableau algorithm for L, including an appropriate blocking condition which ensures termination. As an application of this framework, we present in this paper tableau systems for two expressive DLs, the new DL SHIO and the well-known SHIQ. Our main results are the following: firstly, we obtain that SHIO satisfiability is ExpTime-complete and can be decided by a tableau algorithm. Secondly, we will see that although these two logics share most of their constructs, they lead to quite different TSs, which demonstrates how the capabilities of our framework can be used to capture different language properties. Thirdly, the succinctness of the proofs demonstrates how our framework simplifies the design of tableau algorithms.

In Proc. of the 2004 Int. Workshop on Description Logics, Whistler, British Columbia, Canada, June 6-8, 2004, vol. 104 in CEUR, pp. 168–177, 2004.
44. PSpace automata for Description Logics [ pdf | ]
@inproceedings{HladikPenalozaDL06, author = {Jan Hladik and Rafael Pe{\~n}aloza}, title = {PSpace automata for Description Logics}, pages = {74--85}, editor = {Bijan Parsia and Ulrike Sattler and David Toman}, booktitle = {Proc.\ of the 19th Int.\ Workshop on Description Logics (DL~2006)}, series = {CEUR Workshop Proceedings}, volume = {189}, publisher = {CEUR-WS.org}, year = {2006}, ee = {http://ceur-ws.org/Vol-189/submission_22.pdf} }
Tree automata are often used for satisfiability testing in the area of description logics, which usually yields ExpTime complexity results. We examine conditions under which this result can be improved, and we define two classes of automata, called segmentable and weakly-segmentable, for which emptiness can be decided using space logarithmic in the size of the automaton (and thus polynomial in the size of the input). The usefulness of segmentable automata is demonstrated by reproving the known PSpace result for satisfiability of ALC concepts with respect to acyclic TBoxes.
In Proc. of the 2006 Int. Workshop on Description Logics, Windermere, Lake District, UK, May 30 – June 1, 2006 vol. 189 in CEUR, pp. 74–85, 2006.
45. On the semantics of graded modalities [ pdf | ]
@article{WvanderHoek1992, author = {Wiebe van der Hoek}, title = {On the semantics of graded modalities}, journal = {Journal of Applied Non-Classical Logics}, volume = {2}, number = {1}, year = {1992}, pages = {81--123} }
We enrich propositional modal logic with operators Mn (n ∈ N) which are interpreted on Kripke structures as “there are more than n accessible worlds for which...”, thus obtaining a basic graded logic GrK. We show how some familiar concepts (such as subframes, p-morphisms, disjoint unions and filtrations) and techniques from modal model theory can be used to obtain results about expressiveness (like graded modal equivalence, correspondence and definability) for this language. On the basis of the class of linear frames we demonstrate that the expressive power of the language is considerably stronger than that of classical modal logic.

We give a class of formulas for which a first order equivalent can be systematically obtained, but also show that the set of formulas for which such an equivalence exists is in some sense a proper subset of the set of so called Sahlqvist formulas, a syntactically defined set of modal formulas for which a corresponding formula is guaranteed to exist.

Finally, we show how, combining the technique of ‘filtration’ with a notion of ‘copying’ worlds – in view of the “more than n” interpretation, one cannot simply collapse worlds – for some modal logics (GrK, GrT, ...), the finite model property (and also decidability) is obtained.

Note: graded modal logics are in fact denoted in this paper as K, T, etc. (E.Z.)

2(1):81–123, 1992.
46. The irresistible SRIQ  [ pdf | ]
@inproceedings{HorrKutzSattlerSRIQ, author = {Ian Horrocks and Oliver Kutz and Ulrike Sattler}, title = {The irresistible $\mathcal{SRIQ}$}, pages = {108--117}, editor = {Bernardo Cuenca Grau and Ian Horrocks and Bijan Parsia and Peter F. Patel-Schneider}, booktitle = {Proc.\ of the 1st Int.\ Workshop on OWL: Experiences and Directions (OWLED~2005)}, series = {CEUR Workshop Proceedings}, volume = {188}, publisher = {CEUR-WS.org}, year = {2005}, ee = {http://ceur-ws.org/Vol-188/sub20.pdf} }
Motivated primarily by medical terminology applications, the prominent DL SHIQ  has already been extended to a DL with complex role inclusion axioms of the form R o S ⊆ R or S o R ⊆ R, called RIQ , and the SHIQ  tableau algorithm has been extended to handle such inclusions.

This paper further extends RIQ  and its tableau algorithm with important expressive means that are frequently requested in ontology applications, namely with reflexive, symmetric, transitive, and irreflexive roles, disjoint roles, and the construct ∃R.Self, allowing, for instance, the definition of concepts such as a “narcissist”. Furthermore, we extend the algorithm to cover ABox reasoning extended with negated role assertions. The resulting logic is called SRIQ .

In Proc. of OWL: Experiences and Directions (Workshop), Galway, Ireland, November 11-12, 2005, vol. 188 in CEUR, pp. 108-117, 2005.
• Technical report: [ pdf ]
47. The even more irresistible SROIQ  [ pdf | ]
@inproceedings{HorrKutzSattlerSROIQ, author = {Ian Horrocks and Oliver Kutz and Ulrike Sattler}, title = {The even more irresistible $\mathcal{SROIQ}$}, pages = {57--67}, editor = {Patrick Doherty and John Mylopoulos and Christopher A. Welty}, booktitle = {Proc.\ of the 10th Int.\ Conf.\ on the Principles of Knowledge Representation and Reasoning (KR~2006)}, publisher = {AAAI Press}, year = {2006}, ee = {http://www.aaai.org/Library/KR/2006/kr06-009.php} }
We describe an extension of the description logic underlying OWL-DL, SHOIN , with a number of expressive means that we believe will make it more useful in practice. Roughly speaking, we extend SHOIN  with all expressive means that were suggested to us by ontology developers as useful additions to OWL-DL, and which, additionally, do not affect its decidability. We consider complex role inclusion axioms of the form R o S ⊆ R or S o R ⊆ R, to express propagation of one property along another one, which have proven useful in medical terminologies. Furthermore, we extend SHOIN  with reflexive, symmetric, transitive, and irreflexive roles, disjoint roles, a universal role, and constructs ∃R.Self, allowing, for instance, the definition of concepts such as a “narcissist”. Finally, we consider negated role assertions in ABoxes and qualified number restrictions. The resulting logic is called SROIQ . We present a rather elegant tableau-based reasoning algorithm: it combines the use of automata to keep track of universal value restrictions with the techniques developed for SHOIQ . We believe that SROIQ  could serve as a logical basis for possible future extensions of OWL-DL.
In Proc. of the 10th Int. Conf. on the Principles of Knowledge Representation and Reasoning, Lake District of the UK, June 2-5, 2006. pp. 57-67, AAAI Press, 2006.
• Technical report: [ pdf ]
48. A Description Logic with transitive and inverse roles and role hierarchies [ pdf | ]
@article{HorrocksSattlerSHI1999, author = {Ian Horrocks and Ulrike Sattler}, title = {A Description Logic with transitive and inverse roles and role hierarchies}, journal = {Journal of Logic and Computation}, volume = {9}, number = {3}, year = {1999}, pages = {385--410}, doi = {10.1093/logcom/9.3.385}, ee = {http://dx.doi.org/10.1093/logcom/9.3.385} }
The combination of transitive and inverse roles is important in a range of applications, and is crucial for the adequate representation of aggregated objects, allowing the simultaneous description of parts by means of the whole to which they belong and of wholes by means of their constituent parts. In this paper we present a tableaux algorithms for deciding concept satisfiability and subsumption in Description Logics that extend ALC  with both transitive and inverse roles, a role hierarchy, and functional restrictions. In contrast to earlier algorithms for similar logics, those presented here are well-suited for implementation purposes: using transitive roles and role hierarchies in place of the transitive closure of roles enables sophisticated blocking techniques to be used in place of the cut rule, a rule whose high degree of non-determinism strongly discourages its use in an implementation. As well as promising superior computational behaviour, this new approach is shown to be sufficiently powerful to allow subsumption and satisfiability with respect to a (possibly cyclic) knowledge base to be reduced to concept subsumption and satisfiability, and to support reasoning in a Description Logic that no longer has the finite model property.
Journal of Logic and Computation, 9(3):385-410, 1999.
Note: this Description Logic is now known as SHI .
49. Ontology reasoning in the SHOQ (D) Description Logic [ pdf | ]
@inproceedings{HorrSattSHOQD, author = {Ian Horrocks and Ulrike Sattler}, title = {Ontology reasoning in the $\mathcal{SHOQ}(D)$ Description Logic}, pages = {199--204}, editor = {Bernhard Nebel}, booktitle = {Proc.\ of the 17th Int.\ Joint Conf.\ on Artificial Intelligence (IJCAI~2001)}, publisher = {Morgan Kaufmann}, year = {2001} }
Ontologies are set to play a key rôle in the “Semantic Web” by providing a source of shared and precisely defined terms that can be used in descriptions of web resources. Reasoning over such descriptions will be essential if web resources are to be more accessible to automated processes. SHOQ (D) is an expressive description logic equipped with named individuals and concrete datatypes which has almost exactly the same expressive power as the latest web ontology languages (e.g., OIL and DAML+OIL). We present sound and complete reasoning services for this logic.
In B. Nebel, editor, Proc. of the 17th Int. Joint Conf. on Artificial Intelligence, Seattle, Washington, USA, August 4-10, 2001, pp. 199–204, Morgan Kaufmann, 2001.
50. Decidability of SHIQ  with complex role inclusion axioms [ pdf | ]
@article{HorrSattRIQ, author = {Ian Horrocks and Ulrike Sattler}, title = {Decidability of $\mathcal{SHIQ}$ with complex role inclusion axioms}, journal = {Artificial Intelligence}, volume = {160}, number = {1--2}, pages = {79--104}, year = {2004}, doi = {10.1016/j.artint.2004.06.002}, ee = {http://dx.doi.org/10.1016/j.artint.2004.06.002} }
Motivated by medical terminology applications, we investigate the decidability of an expressive and prominent description logic (DL), SHIQ , extended with role inclusion axioms of the form R o S ⊆ T. It is well known that a naïve such extension leads to undecidability, and thus we restrict our attention to axioms of the form R o S ⊆ R or S o R ⊆ R, which is the most important form of axioms in the applications that motivated this extension. Surprisingly, this extension is still undecidable. However, it turns out that by restricting our attention further to acyclic sets of such axioms, we regain decidability. We present a tableau-based decision procedure for this DL and report on its implementation, which promises to behave well in practice and provides important additional functionality in a medical terminology application.
Artificial Intelligence, 160(1–2):79–104, 2004.
• Note: This Description Logic is now known as RIQ .
• Short version: [ pdf ]
In Proc. of the 18th Int. Joint Conf. on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003, Morgan-Kaufmann, 2003.
• Technical report: [ pdf ]
LTCS-Report 02-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002.
51. A tableaux decision procedure for SHOIQ  [ pdf | ]
@inproceedings{HorrSattSHOIQ2005, author = {Ian Horrocks and Ulrike Sattler}, title = {A tableaux decision procedure for $\matcal{SHOIQ}$}, pages = {448--453}, editor = {Leslie Pack Kaelbling and Alessandro Saffiotti}, booktitle = {Proc.\ of the 19th Int.\ Joint Conf.\ on Artificial Intelligence (IJCAI~2005)}, publisher = {Professional Book Center}, year = {2005} }
This paper presents a tableaux decision procedure for SHOIQ , the DL underlying OWL-DL.

To the best of our knowledge, this is the first goal-directed decision procedure for SHOIQ .

Proc. of the 19th Int. Joint Conf. on Artificial Intelligence, Edinburgh, Scotland, UK, July 30 – August 5, 2005, pp. 448-453, Professional Book Center, 2005.
• Technical report: [ pdf ]
52. A PSpace-algorithm for deciding ALCNI R+-satisfiability [ ps.zip | ]
@techreport{HorrocksSattlerTobies1998, author = {Ian Horrocks and Ulrike Sattler and Stephan Tobies}, title = {A {PS}pace-algorithm for deciding $\mathcal{ALCNI}_{R^+}$-satisfiability}, institution = {LuFg Theoretical Computer Science, RWTH Aachen}, address = {Germany}, type = {LTCS-Report}, number = {98-08}, year = {1998} }
ALCNI R+ALCN  augmented with transitive and inverse roles — is an expressive Description Logic which is especially well-suited for the representation of complex, aggregated objects. Despite its expressiveness, it has been conjectured that concept satisfiability for this logic could be decided in a comparatively efficient way. In this paper we prove the correctness of this conjecture by presenting a PSpace algorithm for deciding satisfiability and subsumption of ALCNI R+-concepts. The space-efficiency of this tableau-based algorithm is due to a sophisticated guidance of the search for a solution.
LTCS-Report 98-08, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1998.
Note: this Description Logic is now known as SIN .
53. Practical reasoning for expressive Description Logics [ pdf | ]
@inproceedings{HorrocksSattlerPract1999, author = {Ian Horrocks and Ulrike Sattler and Stephan Tobies}, title = {Practical reasoning for expressive Description Logics}, pages = {161--180}, editor = {Harald Ganzinger and David A. McAllester and Andrei Voronkov}, booktitle = {Proc.\ of the 6th Int.\ Conf.\ on Logic for Programming and Automated Reasoning (LPAR'99)}, series = {Lecture Notes in Computer Science}, volume = {1705}, publisher = {Springer}, year = {1999}, doi = {10.1007/3-540-48242-3_11}, ee = {http://dx.doi.org/10.1007/3-540-48242-3_11} }
Description Logics (DLs) are a family of knowledge representation formalisms mainly characterised by constructors to build complex concepts and roles from atomic ones. Expressive role constructors are important in many applications, but can be computationally problematical. We present an algorithm that decides satisfiability of the DL ALC  extended with transitive and inverse roles, role hierarchies, and qualifying number restrictions. Early experiments indicate that this algorithm is well-suited for implementation. Additionally, we show that ALC  extended with just transitive and inverse roles is still in PSpace. Finally, we investigate the limits of decidability for this family of DLs.

E.Z.: In short: SHIQ  is decidable; SI  is in PSpace; unrestricted SHN  is undecidable.

In Harald Ganzinger, David McAllester, and Andrei Voronkov, editors, Proc. of the 6th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, Tbilisi, Georgia, September 6-10, 1999. LNAI, vol. 1705, pp. 161-180, Springer, 1999.
54. Practical reasoning for very expressive Description Logics [ pdf | ]
@article{HorrocksSattlerPract2000, author = {Ian Horrocks and Ulrike Sattler and Stephan Tobies}, title = {Practical reasoning for very expressive Description Logics}, journal = {Logic Journal of the IGPL}, volume = {8}, number = {3}, year = {2000}, pages = {239--263}, doi = {10.1093/jigpal/8.3.239}, ee = {http://dx.doi.org/10.1093/jigpal/8.3.239} }
Description Logics (DLs) are a family of knowledge representation formalisms mainly characterised by constructors to build complex concepts and roles from atomic ones. Expressive role constructors are important in many applications, but can be computationally problematical. We present an algorithm that decides satisfiability of the DL ALC  extended with transitive and inverse roles and functional restrictions with respect to general concept inclusion axioms and role hierarchies; early experiments indicate that this algorithm is well-suited for implementation. Additionally, we show that ALC  extended with just transitive and inverse roles is still in PSpace. We investigate the limits of decidability for this family of DLs, showing that relaxing the constraints placed on the kinds of roles used in number restrictions leads to the undecidability of all inference problems. Finally, we describe a number of optimisation techniques that are crucial in obtaining implementations of the decision procedures, which, despite the hight worst-case complexity of the problem, exhibit good performance with real-life problems.

E.Z.: In short: SHIQ  is decidable; SI  is in PSpace; unrestricted SHN  is undecidable.

Logic Journal of the IGPL, 8(3):239-263, 2000.
55. How many legs do I have? Non-simple roles in number restrictions revisited [ pdf | ]
@inproceedings{KazSatZolin2007, author = {Yevgeny Kazakov and Ulrike Sattler and Evgeny Zolin}, title = {How many legs do {I} have? {N}on-simple roles in number restrictions revisited}, pages = {303--317}, editor = {Nachum Dershowitz and Andrei Voronkov}, booktitle = {Proc.\ of the 14th Int.\ Conf.\ on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR~2007)}, series = {Lecture Notes in Computer Science}, volume = {4790}, publisher = {Springer}, year = {2007}, doi = {10.1007/978-3-540-75560-9_23} ee = {http://dx.doi.org/10.1007/978-3-540-75560-9_23} }
The Description Logics underpinning OWL impose a well-known syntactic restriction in order to preserve decidability: they do not allow to use non-simple roles – that is, transitive roles or their super-roles – in number restrictions. When modeling composite objects, for example in bio-medical ontologies, this restriction can pose problems.

Therefore, we take a closer look at the problem of counting over non-simple roles. On the one hand, we sharpen the known undecidability results and demonstrate that: (i) for DLs with inverse roles, counting over non-simple roles leads to undecidability even when there is only one role in the language; (ii) for DLs without inverses, two transitive and an arbitrary role are sufficient for undecidability. On the other hand, we demonstrate that counting over non-simple roles does not compromise decidability in the absence of inverse roles provided that certain restrictions on role inclusion axioms are satisfied.

E.Z.: In short:
• unrestricted SIQ  and even SIN  with TBoxes with even one role are undecidable;
• unrestricted SHQ  and even SHN  with TBoxes with just three roles (and a special RBox) are undecidable;
SHQ  with TBoxes is decidable for a large family of RBoxes.
So the question is: In your ontology, do you use a “safe” RBox, i.e., which does not destroy decidability?

In Nachum Dershowitz and Andrei Voronkov, editors, Proc. of the 14th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, Yerevan, Armenia, October 15-19, 2007. LNAI, vol. 4790, pp. 303-317, Springer, 2007.
• Technical report: Is your RBox safe? [ pdf ]
Information Management Group, School of Computer Science, The University of Manchester, UK, 2007.
56. Results on the propositional μ-calculus [ pdf | ]
@article{Kozen1983, author = {Dexter Kozen}, title = {Results on the propositional $\mu$-calculus}, journal = {Theoretical Computer Science, Special Issue: 9th Int.\ Colloquium on Automata, Languages and Programming (ICALP'82)}, volume = {27}, number = {3}, year = {1983}, pages = {333--354}, doi = {10.1016/0304-3975(82)90125-6}, ee = {http://dx.doi.org/10.1016/0304-3975(82)90125-6} }
In this paper we define and study a propositional μ-calculus Lμ, which consists essentially of propositional modal logic with a least fixpoint operator. Lμ is syntactically simpler yet strictly more expressive than Propositional Dynamic Logic (PDL). For a restricted version we give an exponential-time decision procedure, small model property, and complete deductive system, thereby subsuming the corresponding results for PDL.
Theoretical Computer Science, Special Issue: 9th Int. Colloquium on Automata, Languages and Programming, ICALP'82, Aarhus, Denmark, July 12 – 16, 1982, 27(3):333–354, 1983.
57. A finite model theorem for the propositional μ-calculus [ pdf | ]
@article{Kozen1988, author = {Dexter Kozen}, title = {A finite model theorem for the propositional $\mu$-calculus}, journal = {Studia Logica}, volume = {47}, number = {3}, year = {1988}, pages = {233--241}, doi = {10.1007/BF00370554}, ee = {http://dx.doi.org/10.1007/BF00370554} }
We prove a finite model theorem and infinitary completeness result for the propositional μ-calculus. The construction establishes a link between finite model theorems for propositional program logics and the theory of well-quasi-orders.
Studia Logica, 47(3):233–241, 1988.
58. The complexity of the graded μ-calculus [ pdf | ]
@inproceedings{KupfSatVardi2002, author = {Orna Kupferman and Ulrike Sattler and Moshe Y. Vardi}, title = {The complexity of the graded $\mu$-calculus}, pages = {423--437}, editor = {Andrei Voronkov}, booktitle = {Proc.\ of the 18th Int.\ Conf.\ on Automated Deduction (CADE-18)}, series = {Lecture Notes in Computer Science}, volume = {2392}, publisher = {Springer}, year = {2002}, doi = {10.1007/3-540-45620-1_34}, ee = {http://dx.doi.org/10.1007/3-540-45620-1_34} }
In classical logic, existential and universal quantifiers express that there exists at least one individual satisfying a formula, or that all individuals satisfy a formula. In many logics, these quantifiers have been generalized to express that, for a non-negative integer n, at least n individuals or all but n individuals satisfy a formula. In modal logics, graded modalities generalize standard existential and universal modalities in that they express, e.g., that there exist at least n accessible worlds satisfying a certain formula. Graded modalities are useful expressive means in knowledge representation; they are present in a variety of other knowledge representation formalisms closely related to modal logic.

A natural question that arises is how the generalization of the existential and universal modalities affects the decidability problem for the logic and its computational complexity, especially when the numbers in the graded modalities are coded in binary. In this paper we study the graded μ-calculus, which extends graded modal logic with fixed-point operators, or, equivalently, extends classical μ-calculus with graded modalities. We prove that the decidability problem for graded μ-calculus is ExpTime-complete – not harder than the decidability problem for μ-calculus, even when the numbers in the graded modalities are coded in binary.

E.Z.: In short, graded μ-calculus is ExpTime-complete, hence so is μALCQ .

In Proc. of Copenhagen, Denmark, July 27-30, 2002, LNCS, vol. 2392, pp. 423-437, Springer, 2002.
59. A lower complexity bound for Propositional Dynamic Logic with intersection [ pdf | ps.zip | ]
@inproceedings{LangeEXPSPACE, author = {Martin Lange}, title = {A lower complexity bound for Propositional Dynamic Logic with intersection}, pages = {133--147}, editor = {Renate A. Schmidt and Ian Pratt-Hartmann and Mark Reynolds and Heinrich Wansing}, booktitle = {Proc.\ of the 5th Int.\ Conf.\ on Advances in Modal Logic (AiML 2004)}, publisher = {King's College Publications}, year = {2005}, ee = {http://www.aiml.net/volumes/volume5/Lange.ps} }
This paper shows that satisfiability for Propositional Dynamic Logic with intersection is ExpSpace-hard. The proof uses a reduction from the word problem for alternating, exponential time bounded Turing machines.
In Renate Schmidt, Ian Pratt-Hartmann, Mark Reynolds, and Heinrich Wansing, editors, Proc. of Advances in Modal Logic, Volume 5, University of Manchester, UK, September 9-11, 2004. pp. 133–147, King's College Publications, 2005.
60. 2-ExpTime lower bounds for Propositional Dynamic Logics with intersection [ ps.zip | ]
@article{LangeLutz2005, author = {Martin Lange and Carsten Lutz}, title = {{2-ExpTime} lower bounds for Propositional Dynamic Logics with intersection}, journal = {Journal of Symbolic Logic}, volume = {70}, number = {4}, year = {2005}, pages = {1072--1086}, doi = {10.2178/jsl/1129642115}, ee = {http://dx.doi.org/10.2178/jsl/1129642115} }
In 1984, Danecki proved that satisfiability in IPDL, i.e., Propositional Dynamic Logic (PDL) extended with an intersection operator on programs, is decidable in deterministic double exponential time. Since then, the exact complexity of IPDL has remained an open problem: the best known lower bound was the ExpTime one stemming from plain PDL until, in 2004, the first author established ExpSpace-hardness. In this paper, we finally close the gap and prove that IPDL is hard for 2-ExpTime, thus 2-ExpTime-complete. We then sharpen our lower bound, showing that it even applies to IPDL without the test operator interpreted on tree structures.

E.Z.: In short, IPDL and hence ALC (∩,∪,o,*,id) is 2ExpTime-complete.

Journal of Symbolic Logic, 70(4):1072-1086, 2005.
61. An improved NExpTime-hardness result for description logic ALC
extended with inverse roles, nominals, and counting
[ ps.zip | ]
@techreport{LutzImproved2004, author = {Carsten Lutz}, title = {An improved {NExpTime}-hardness result for description logic $\mathcal{ALC}$ extended with inverse roles, nominals, and counting}, type = {LTCS-Report}, number = {05-05}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, address = {Dresden, Germany}, year = {2005} }
The Description Logic (DL) ALCIO  extends the basic propositionally closed DL ALC  with inverse roles and nominals. Reasoning with ALCIO  concept descriptions is ExpTime-complete, and the same holds for reasoning in ALCIO  with general TBoxes (aka GCIs) since TBoxes can be “internalized”: reasoning with general TBoxes can be polynomially reduced to reasoning with concept descriptions.

It is well-known that the complexity of reasoning increases if ALCIO  is extended with counting constructors: Tobies considers ALCIO  extended with a concept constructor (≤ 1 r) and proves that reasoning in the resulting DL is NExpTime-complete, both with concept descriptions and with general TBoxes. For his reduction, it is crucial that the constructor (≤ 1 r) can be applied both to atomic roles and to inverse roles. In this paper, we strengthen Tobies' result by proving NExpTime-hardness of reasoning in the description logic ALCFIO , which is obtained from ALCIO  by adding an additional sort of roles which are interpreted as partial functions. Thus, in our formalism we can only count on roles “in one direction”, while Tobies' proof requires counting in both direction. Just as in Tobies' case, our proof is by reduction of a NExpTime-complete variant of the domino problem. However, our reduction strategy is quite different from the one used by Tobies.

E.Z.: In short, ALCFIO  is NExpTime-complete, even with numbers coded in binary, and even with inverse roles not used in number restrictions.

LTCS-Report 04-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2004.
62. PDL with intersection and converse is decidable [ ps.zip | ]
@inproceedings{LutzICPDL2005, author = {Carsten Lutz}, title = {{PDL} with intersection and converse is decidable}, pages = {413--427}, editor = {C.-H. Luke Ong}, booktitle = {Proc.\ of the 19th Int.\ Workshop on Computer Science Logic (CSL 2005), 14th Annual Conf.\ of the European Association for Computer Science Logic (EACSL)}, series = {Lecture Notes in Computer Science}, volume = {3634}, publisher = {Springer}, year = {2005}, doi = {10.1007/11538363_29}, ee = {http://dx.doi.org/10.1007/11538363_29} }
In its many guises and variations, propositional dynamic logic (PDL) plays an important rôle in various areas of computer science such as databases, artificial intelligence, and computer linguistics. One relevant and powerful variation is ICPDL, the extension of PDL with intersection and converse. However, although ICPDL has several interesting applications, its computational properties have never been investigated. In this paper, we prove that ICPDL is decidable by developing a translation to the monadic second order logic of infinite trees. Our result has applications in information logic, description logic, and epistemic logic. In particular, we solve a long-standing open problem in information logic. Another virtue of our approach is that it provides a decidability proof that is more transparent than existing ones for PDL with intersection (but without converse).

E.Z.: In short, ICPDL and hence ALCI (∩,∪,o,*,id) is decidable.

In Proc. of the 14th Annual Conference of the European Association for Computer Science Logic, Oxford, UK, August 22-25, 2005, LNCS. vol. 3634, pp. 413-427, Springer, 2005.
• Technical report: [ ps.zip ]
LTCS-Report 05-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005.
63. Keys, nominals, and concrete domains [ pdf | ]
@article{LutzArecHorSat2004, author = {Carsten Lutz and Carlos Areces and Ian Horrocks and Ulrike Sattler}, title = {Keys, nominals, and concrete domains}, journal = {Journal of Artificial Intelligence Research}, volume = {23}, year = {2004}, pages = {667--726}, doi = {10.1613/jair.1542}, ee = {http://dx.doi.org/10.1613/jair.1542} }
Many description logics (DLs) combine knowledge representation on an abstract, logical level with an interface to “concrete” domains like numbers and strings with built-in predicates such as <, +, and prefix-of. These hybrid DLs have turned out to be useful in several application areas, such as providing the basis for expressive ontology languages. We propose to further extend such DLs with key constraints that allow the expression of statements like “US citizens are uniquely identified by their social security number”. Based on this idea, we introduce a number of natural description logics and perform a detailed analysis of their decidability and computational complexity. It turns out that naïve extensions with key constraints easily lead to undecidability, whereas more careful extensions yield NExpTime-complete DLs for a variety of useful concrete domains.
• Short version: [ pdf ]
In Proc. of the 18th Int. Joint Conf. on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003, pp. 349-354. Morgan Kaufmann, 2003.
• Technical report: [ pdf ]
LTCS-Report 02-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002.
64. The complexity of reasoning with Boolean modal logics [ ps.zip | ]
@inproceedings{LutzSattler2001, author = {Carsten Lutz and Ulrike Sattler}, title = {The complexity of reasoning with {B}oolean modal logics}, pages = {329--348}, editor = {Frank Wolter and Heinrich Wansing and Maarten de Rijke and Michael Zakharyaschev}, booktitle = {Proc.\ of the 3rd Int.\ Conf.\ on Advances in Modal Logic (AiML~2000)}, publisher = {World Scientific}, year = {2002} }
In this paper, we investigate the complexity of reasoning with various Boolean Modal Logics. The main results are that (i) adding negation of modal parameters to (multi-modal) K makes reasoning ExpTime-complete and (ii) adding atomic negation and conjunction to K even yields a NExpTime-complete logic. The last result is relativized by the fact that it depends on an infinite number of modal parameters to be available. If the number of modal parameters is bounded, full Boolean Modal Logic becomes ExpTime-complete.
In Frank Wolter, Heinrich Wansing, Maarten de Rijke, and Michael Zakharyaschev, editors, Proc. of Advances in Modal Logic, Volume 3, Leipzig, October 4–7, 2000. pp. 329-348, World Scientific, 2002.
• Technical report: [ ps.zip ]
LTCS-Report 00-02, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000.
65. The complexity of finite model reasoning in Description Logics [ pdf | ]
@article{LutzSattlerTendera2005, author = {Carsten Lutz and Ulrike Sattler and Lidia Tendera}, title = {The complexity of finite model reasoning in Description Logics}, journal = {Information and Computation}, volume = {199}, number = {1--2}, year = {2005}, pages = {132--171}, doi = {10.1016/j.ic.2004.11.002}, ee = {http://dx.doi.org/10.1016/j.ic.2004.11.002} }
We analyse the complexity of finite model reasoning in the description logic ALCQI , i.e., ALC  augmented with qualifying number restrictions, inverse roles, and general TBoxes. It turns out that all relevant reasoning tasks such as concept satisfiability and ABox consistency are ExpTime-complete, regardless of whether the numbers in number restrictions are coded unarily or binarily. Thus, finite model reasoning with ALCQI  is not harder than standard reasoning with ALCQI .
Information and Computation, 199(1-2):132–171, 2005.
66. Modal Logic and the two-variable fragment [ pdf | ]
@inproceedings{LutzSattlerWolter2001, author = {Carsten Lutz and Ulrike Sattler and Frank Wolter}, title = {Modal Logic and the two-variable fragment}, pages = {247--261}, editor = {Laurent Fribourg}, booktitle = {Proc.\ of the 15th Int.\ Workshop on Computer Science Logic (CSL 2001), 10th Annual Conf.\ of the European Association for Computer Science Logic (EACSL)}, series = {Lecture Notes in Computer Science}, volume = {2142}, publisher = {Springer}, year = {2001}, doi = {10.1007/3-540-44802-0_18}, ee = {http://dx.doi.org/10.1007/3-540-44802-0_18} }
We introduce a modal language L which is obtained from standard modal logic by adding the Boolean operators on accessibility relations, the identity relation, and the converse of relations. It is proved that L has the same expressive power as the two-variable fragment FO2 of first-order logic, but speaks less succinctly about relational structures: if the number of relations is bounded, then L-satisfiability is ExpTime-complete but FO2 satisfiability is NExpTime-complete. We indicate that the relation between L and FO2 provides a general framework for comparing modal and temporal languages with first-order languages.

E.Z.: In short, ALCI (∩,∪,¬,id) is ExpTime-complete (and as expressive as FO2).

Proc. of the 10th Annual Conference of the European Association for Computer Science Logic, Paris, France, September 10-13, 2001. LNCS, vol. 2142, pp.247-261, Springer, 2001.
67. PDL with negation of atomic programs [ ps.zip | ]
@article{LutzWalther2004, author = {Carsten Lutz and Dirk Walther}, title = {{PDL} with negation of atomic programs}, journal = {Journal of Applied Non-Classical Logics}, volume = {15}, number = {2}, year = {2005}, pages = {189--214}, doi = {10.3166/jancl.15.189-213}, ee = {http://dx.doi.org/10.3166/jancl.15.189-213} }
Propositional dynamic logic (PDL) is one of the most successful variants of modal logic. To make it even more useful for applications, many extensions of PDL have been considered in the literature. A very natural and useful such extension is with negation of programs. Unfortunately, as long-known, reasoning with the resulting logic is undecidable. In this paper, we consider the extension of PDL with negation of atomic programs, only. We argue that this logic is still useful, e.g. in the context of Description Logics, and prove that satisfiability is decidable and ExpTime-complete using an approach based on Büchi tree automata.
Journal of Applied Non-Classical Logics, 15(2):189–214, 2005.
• Technical report: [ ps.zip ]
LTCS-Report 03-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003.
• Short version: [ pdf ]
In Proc. of the 2nd Int. Joint Conf. on Automated Reasoning, Cork, Ireland, July 4-8, 2004. LNAI, vol. 3097, pp. 259–273, Springer, 2004.
68. Decision procedures for expressive Description Logics with intersection, composition, converse of roles and role identity [ pdf | ]
@inproceedings{Massacci2001, author = {Fabio Massacci}, title = {Decision procedures for expressive Description Logics with intersection, composition, converse of roles and role identity}, pages = {193--198}, editor = {Bernhard Nebel}, booktitle = {Proc.\ of the 17th Int.\ Joint Conf.\ on Artificial Intelligence (IJCAI~2001)}, publisher = {Morgan Kaufmann}, year = {2001} }
In the quest for expressive description logics for real-world applications, a powerful combination of constructs has so far eluded practical decision procedures: intersection and composition of roles. We propose tableau-based decision procedures for the satisfiability of logics extending ALC  with the intersection, composition, union, converse of roles and role identity. We show that
1. the satisfiability of ALC (∩,∪,o), for which a 2-ExpTime upper bound was given by tree-automata techniques, is PSpace-complete;
2. the satisfiability of ALCI (∩,∪,o,id), an open problem so far, is in NExpTime.
In Proc. of the 17th Int. Joint Conf. on Artificial Intelligence, Seattle, Washington, USA, August 4-10, 2001, pp. 193-198, Morgan Kaufmann, 2001.
69. Complexity results for first-order two-variable logic with counting [ pdf | ps.zip | ]
@article{Pacholski_etal_2000, author = {Leszek Pacholski and Wieslaw Szwast and Lidia Tendera}, title = {Complexity results for first-order two-variable logic with counting}, journal = {SIAM Journal on Computing}, volume = {29}, year = {2002}, pages = {1083--1117}, doi = {10.1137/S0097539797323005}, ee = {http://dx.doi.org/10.1137/S0097539797323005} }
Let Cp2 denote the class of first-order sentences with two variables and with additional quantifiers “there exists exactly (at most, at least) i”, for ip, and let C2 be the union of Cp2 taken over all integers p. We prove that the satisfiability problem for C12 sentences is NExpTime-complete. This strengthens the results by Grädel, Kolaitis, and Vardi [15], who showed that the satisfiability problem for the first-order two-variable logic L2 is NExpTime-complete and by Grädel, Otto, and Rosen [16], who proved the decidability of C2. Our result easily implies that the satisfiability problem for C2 is in nondeterministic, doubly exponential time. It is interesting that C12 is in NExpTime in spite of the fact that there are sentences whose minimal (and only) models are of doubly exponential size.

It is worth noticing that by a recent result of E. Grädel, M. Otto, and E. Rosen [17], extensions of two-variable logic L2 by a weak access to cardinalities through the Härtig (or equicardinality) quantifier is undecidable. The same is true for extensions of L2 by very weak forms of recursion.

The satisfiability problem for logics with a bounded number of variables has applications in artificial intelligence, notably in modal logics, where counting comes in the context of graded modalities, and in description logics, where counting can be used to express so-called number restrictions.

[15] E. Grädel, Ph. Kolaitis, and M. Vardi, On the decision problem for two-variable first-order logic. Bull. Symbolic Logic, 3 (1997), pp. 53–69.
[16] E. Grädel, M. Otto, and E. Rosen, Two-variable logic with counting is decidable. Proc. of the 12th Annual IEEE Symposium on Logic in Computer Science, 1997, pp. 306–317.
[17] E. Grädel, M. Otto, and E. Rosen, Undecidability results on two-variables logics. Proc. of the 14th Annual Symposium on Theoretical Aspects of Computer Science, LNCS, vol. 1200, Springer, Berlin, 1997.

SIAM Journal on Computing (SICOMP), vol. 29, pp. 1083-1117, 2000.
• Its Section 4 was presented at the conference:
Complexity of two-variable logic with counting [ pdf ]
In Proc. of the 12th IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 – July 2, 1997, pp.318-327, IEEE Computer Society Press, 1997.
70. Reasoning in the SHOQ (Dn) Description Logic [ pdf | ]
@inproceedings{PanHorrSHOQDn, author = {Jeff Z. Pan and Ian Horrocks}, title = {Reasoning in the $\mathcal{SHOQ}(D_n)$ Description Logic}, pages = {53--62}, editor = {Ian Horrocks and Sergio Tessaris}, booktitle = {Proc.\ of the 15th Int.\ Workshop on Description Logics (DL~2002)}, series = {CEUR Workshop Proceedings}, volume = {53}, publisher = {CEUR-WS.org}, year = {2002}, ee = {http://ceur-ws.org/Vol-53/Pan-Horrocks-shoqdn-2002.ps} }
Description Logics (DLs) are of crucial importance to the development of the Semantic Web, where their rôle is to provide formal underpinnings and automated reasoning services for Semantic Web ontology languages such as DAML+OIL. In this paper we show how the description logic SHOQ (D), which has been designed to provide such services, can be extended with n-ary datatype predicates as well as datatype number restrictions, to give SHOQ (Dn), and we present an algorithm for deciding the satisfiability of SHOQ (Dn) concepts, along with a proof of its soundness and completeness. The work is motivated by the requirement for n-ary datatype predicates in relation to “real world” properties such as size, weight and duration, in the Semantic Web applications.
In Proc. of the 2002 Int. Workshop on Description Logics, Toulouse, France, April 19-21, 2002, vol. 53 in CEUR, pp. 53–62, 2002.
71. Models of program logics [ pdf | ]
@inproceedings{Pratt1979, author = {Vaughan R. Pratt}, title = {Models of program logics}, pages = {115--122}, booktitle = {Proc.\ of the 20th Annual Symposium on Foundations of Computer Science (FoCS~'79)}, publisher = {IEEE Computer Society}, year = {1979}, doi = {10.1109/SFCS.1979.24}, ee = {http://dx.doi.org/10.1109/SFCS.1979.24} }
We briefly survey the major proposals for models of programs and show that they all lead to the same propositional theory of programs. Methods of algebraic logic dominate in the proofs. One of the connections made between the models, that involving language models, is quite counterintuitive. The common theory has already been shown to be complete in deterministic exponential time; we give here a simpler proof of the upper bound.
In Proc. of the 20th Annual IEEE Symposium on the Foundations of Computer Science, San Juan, Puerto Rico, October 29-31, 1979. pp.115-122, IEEE Computer Society, 1979.
72. Complexity of the two-variable fragment with counting quantifiers [ pdf | ]
@article{PrattHartmann_2005, author = {Ian Pratt-Hartmann}, title = {Complexity of the two-variable fragment with counting quantifiers}, journal = {Journal of Logic, Language, and Information}, volume = {14}, number = {3}, year = {2005}, pages = {369--395}, doi = {10.1007/s10849-005-5791-1}, ee = {http://dx.doi.org/10.1007/s10849-005-5791-1} }
The satisfiability and finite satisfiability problems for the two-variable fragment of first-order logic with counting quantifiers are both in NExpTime, even when counting quantifiers are coded succinctly.
, 14(3):369-395, 2005.
73. A note on graded modal logic [ ps.pdf | scan.pdf | ]
@article{MdeRijke2000Graded, author = {Maarten de Rijke}, title = {A note on graded modal logic}, journal = {Studia Logica}, volume = {64}, number = {2}, year = {2000}, pages = {271--283}, doi = {10.1007/s10849-005-5791-1}, ee = {http://dx.doi.org/10.1007/s10849-005-5791-1} }
We introduce a notion of bisimulation for graded modal logic. Using these bisimulations the model theory of graded modal logic can be developed in a uniform manner. We illustrate this by establishing the finite model property, and proving invariance and definability results.
Studia Logica, 64(2):271-283, 2000.
74. Undecidability and nonperiodicity of tilings on the plane [ pdf | ]
@article{Robinson1971, author = {Raphael Robinson}, title = {Undecidability and nonperiodicity of tilings on the plane}, journal = {Inventiones Mathematicae}, volume = {12}, number = {3}, year = {1971}, pages = {177--209}, doi = {10.1007/BF01418780}, ee = {http://dx.doi.org/10.1007/BF01418780} }
The three main objectives of the paper, and the relevant sections, are as follows.

(a) Proof that the six polygonal tiles shown on Fig. 1 allow only nonperiodic tilings of the plane. The same result is obtained for the closely related set of ten tiles.

(b) Proof that there is a set of 36 square tiles with colored edges for which the completion problem is undecidable, translation only being used. By the completion problem is meant the problem of deciding whether an arbitrary finite partial tiling of the plane can be completed.

(c) Simplified proof of Berger's theorem that the plane tiling problem is undecidable.

, 12(3):177–209, 1971.
75. The hybrid μ-calculus [ pdf | ]
@inproceedings{SattlerVardi2001, author = {Ulrike Sattler and Moshe Y. Vardi}, title = {The hybrid $\mu$-calculus}, pages = {76--91}, editor = {Rajeev Gor{\'e} and Alexander Leitsch and Tobias Nipkow}, booktitle = {Proc.\ of the 1st Int.\ Joint Conf.\ on Automated Reasoning (IJCAR~2001)}, series = {Lecture Notes in Computer Science}, volume = {2083}, publisher = {Springer}, year = {2001}, doi = {10.1007/3-540-45744-5_7}, ee = {http://dx.doi.org/10.1007/3-540-45744-5_7} }
We present an ExpTime decision procedure for the full μ-calculus (including converse programs) extended with nominals and a universal program, thus devising a new, highly expressive ExpTime logic. The decision procedure is based on tree automata, and makes explicit the problems caused by nominals and how to overcome them. Roughly speaking, we show how to reason in a logic lacking the tree model property using techniques for logics with the tree model property. The contribution of the paper is two-fold: we extend the family of ExpTime logics, and we present a technique to reason in the presence of nominals.

E.Z.: In short, μ-calculus with converse programs, universal program and nominals is in ExpTime, and hence ExpTime-complete (since μ-calculus is ExpTime-hard). Hence, concept satisfiability in μALCIO  is ExpTime-complete (even with general TBoxes, which are internalizable in presence of μ).

In R. Gore, A. Leitsch, and T. Nipkow, editors, Proc. of the 1st Int. Joint Conf. on Automated Reasoning, Siena, Italy, June 18-23, 2001. LNAI, vol. 2083, pp. 76–91, Springer, 2001.
76. Reasoning with individuals in concept languages [ pdf | ps.zip | ]
@article{Schaerf1994b, author = {Andrea Schaerf}, title = {Reasoning with individuals in concept languages}, journal = {Data and Knowledge Engineering}, volume = {13}, number = {2}, year = {1994}, pages = {141--176}, doi = {10.1016/0169-023X(94)90002-7}, ee = {http://dx.doi.org/10.1016/0169-023X(94)90002-7} }
One of the main characteristics of knowledge representation systems based on the description of concepts is the clear distinction between terminological and assertional knowledge. Although this characteristic leads to several computational and representational advantages, it usually limits the expressive power of the system. For this reason, some attempts have been done, allowing for a limited form of amalgamation between the two components and a more complex interaction between them. In particular, one of these attempts is based on letting the individuals to be referenced in the concept expressions. This is generally performed by admitting a constructor for building a concept from a set of enumerated individuals.

In this paper we investigate on the consequences of introducing constructors of this type in the concept description language. We also provide a complete reasoning procedure to deal with these constructors and we obtain some complexity results on it.

Data and Knowledge Engineering, 13(2):141-176, 1994.
77. A correspondence theory for terminological logics: Preliminary report [ pdf | ps.zip | ]
@inproceedings{Schild1991, author = {Klaus Schild}, title = {A correspondence theory for terminological logics: {P}reliminary report}, pages = {466--471}, editor = {John Mylopoulos and Raymond Reiter}, booktitle = {Proc.\ of the 12th Int.\ Joint Conf.\ on Artificial Intelligence (IJCAI~1991)}, publisher = {Morgan Kaufmann}, year = {1991} }
We show that the terminological logic ALC  comprising Boolean operations on concepts and value restrictions is a notational variant of the propositional modal logic K(m). To demonstrate the utility of the correspondence, we give two of its immediate by-products. Namely, we axiomatize ALC  and give a simple proof that subsumption in ALC  is PSpace-complete, replacing the original six-page one.

Furthermore, we consider an extension of ALC  additionally containing both the identity role and the composition, union, transitive-reflexive closure, range restriction, and inverse of roles. It turns out that this language, called TSL , is a notational variant of the propositional dynamic logic converse-PDL. Using this correspondence, we prove that it suffices to consider finite TSL -models, show that TSL -subsumption is decidable, and obtain an axiomatization of TSL .

By discovering that features correspond to deterministic programs in dynamic logic, we show that adding them to TSL  preserves decidability, although violates its finite model property. Additionally, we describe an algorithm for deciding the coherence of inverse-free TSL -concepts with features. Finally, we prove that universal implications can be expressed within TSL .

E.Z.: Note that TSL  is now known as ALCIreg. In short,
ALC  ≅ K(m),
ALCIreg  ≅ converse-PDL,
ALCIFreg  ≅ deterministic converse-PDL,
ALCIreg has FMP,
ALCIFreg  lacks FMP.

In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence, Sydney, Australia, August 24-30, 1991, pp. 466-471, Morgan Kaufmann, 1991.
78. Towards a theory of frames and rules [ pdf | ]
@techreport{Schild1989, author = {Klaus Schild}, title = {Towards a theory of frames and rules}, type = {KIT-Report}, number = {76}, institution = {Fachbereich Informatik, Technische Universit{\"a}t Berlin}, address = {Berlin, Germany}, year = {1989} }
A term definition language very similar to the terminological part of BACK is enriched with Horn-like rules and disjointness restrictions built up from arbitrary concepts possibly involving syntactic or semantic cycles. The resulting hybrid language is given a weak semantics which captures the inferences expected intuitively and allows for representing some kind of procedural knowledge. The weak semantics used is based on model theoretic grounds and, even more important, allows to prove properties of the language very easily. Moreover an algorithm is developed which is sound and and complete with respect to the weak semantics and can be characterized to be polynomially time bound for non-pathological cases.
KIT-Report 76, Fachbereich Informatik, Technische Universität Berlin, Berlin (Germany), 1989.
79. Subsumption in KL-ONE is undecidable [ pdf | ]
@inproceedings{SchmidtSchauBKLONE89, author = {Manfred Schmidt-Schau{\ss}}, title = {Subsumption in {KL-ONE} is undecidable}, pages = {421--431}, editor = {Ronald J. Brachman and Hector J. Levesque and Raymond Reiter}, booktitle = {Proc.\ of the 1st Int.\ Conf.\ on the Principles of Knowledge Representation and Reasoning (KR'89)}, publisher = {Morgan Kaufmann}, year = {1989} }
It is shown that in the frame-based language KL-ONE it is undecidable whether one concept is subsumed by another concept. In fact a rather small sublanguage of KL-ONE called ALR  is used which has only the concept forming operators conjunction, value restriction, and role value maps using only “=”. In particular, number restrictions are not used. The language ALR  can be viewed as an extension of feature terms without complements and unions, where features have sets as values instead of elements. Our result shows that there is a basic difference between feature terms and KL-ONE, since the complexity of subsumption switches from quasi-linear to undecidable if the restriction is dropped that roles are functional.
In Proc. of the 1st Int. Conf. on the Principles of Knowledge Representation and Reasoning, Toronto, Ontario, Canada, May 15-18, 1989. pp. 421–431, Morgan Kaufmann, 1989.
80. Attributive concept descriptions with complements [ pdf | ]
@article{SchmidtSchauBSmolka1991, author = {Manfred Schmidt-Schau\ss and Gert Smolka}, title = {Attributive concept descriptions with complements}, journal = {Artificial Intelligence}, volume = {48}, number = {1}, year = {1991}, pages = {1--26}, doi = {10.1016/0004-3702(91)90078-X}, ee = {http://dx.doi.org/10.1016/0004-3702(91)90078-X} }
We investigate the consequences of adding unions and complements to attributive concept descriptions employed in terminological knowledge representation languages. It is shown that deciding coherence and subsumption of such descriptions are PSpace-complete problems that can be decided with linear space.
Artificial Intelligence, 48(1):1-26, 1991.
81. An automata theoretic decision procedure for the propositional μ-calculus [ pdf | ]
@article{StreettEmerson1989, author = {Robert S. Streett and E. Allen Emerson}, title = {An automata theoretic decision procedure for the propositional $\mu$-calculus}, journal = {Information and Computation}, volume = {81}, number = {3}, year = {1989}, pages = {249--264}, doi = {10.1016/0890-5401(89)90031-X}, ee = {http://dx.doi.org/10.1016/0890-5401(89)90031-X} }
The propositional μ-calculus is a propositional logic of programs which incorporates a least fixpoint operator and subsumes the Propositional Dynamic Logic of Fischer and Ladner, the infinite looping construct of Streett, and the Game Logic of Parikh. We give an elementary time decision procedure, using a reduction to the emptiness problem for automata on infinite trees. A small model theorem is obtained as a corollary.
Information and Computation, 81(3):249–264, 1989.
• Short version appeared earlier:
The propositional μ-calculus is elementary [ pdf ]
Proc. of the 11th Int. Colloquium on Automata, Languages and Programming, Antwerp, Belgium, July 16-20, 1984. LNCS, vol. 172, pp. 465–472, Springer, 1984.
82. The complexity of reasoning with cardinality restrictions and nominals in expressive Description Logics [ pdf | ]
@article{Tobies2000, author = {Stephan Tobies}, title = {The complexity of reasoning with cardinality restrictions and nominals in expressive Description Logics}, journal = {Journal of Artificial Intelligence Research}, volume = {12}, year = {2000}, pages = {199--217}, doi = {10.1613/jair.705}, ee = {http://dx.doi.org/10.1613/jair.705} }
We study the complexity of the combination of the Description Logics ALCQ  and ALCQI  with a terminological formalism based on cardinality restrictions on concepts. These combinations can naturally be embedded into C2, the two variable fragment of predicate logic with counting quantifiers, which yields decidability in NExpTime. We show that this approach leads to an optimal solution for ALCQI , as ALCQI  with cardinality restrictions has the same complexity as C2 (NExpTime-complete). In contrast, we show that for ALCQ , the problem can be solved in ExpTime. This result is obtained by a reduction of reasoning with cardinality restrictions to reasoning with the (in general weaker) terminological formalism of general axioms for ALCQ  extended with nominals. Using the same reduction, we show that, for the extension of ALCQI  with nominals, reasoning with general axioms is a NExpTime-complete problem. Finally, we sharpen this result and show that pure concept satisfiability for ALCQI  with nominals is NExpTime-complete. Without nominals, this problem is known to be PSpace-complete.
83. The taming of converse: Reasoning about two-way computations [ pdf | ]
@inproceedings{Vardi1985, author = {Moshe Y. Vardi}, title = {The taming of converse: {R}easoning about two-way computations}, pages = {413--424}, editor = {Rohit Parikh}, booktitle = {Proc.\ of the 5th Workshop on Logics of Programs}, series = {Lecture Notes in Computer Science}, volume = {193}, publisher = {Springer}, year = {1985}, doi = {10.1007/3-540-15648-8_31}, ee = {http://dx.doi.org/10.1007/3-540-15648-8_31} }
We consider variants of propositional dynamic logic (PDL) augmented with the converse construct. Intuitively, the converse α  of a program α  is a programs whose semantics is to run a backwards. While PDL consists of assertions about weakest preconditions, the converse construct enable us to make assertions about strongest postconditions. We investigate the interaction of converse with two constructs that deal with infinite computations: loop and repeat. We show that converse-loop-PDL is decidable in exponential time, and converse-repeat-PDL is decidable in nondeterministic exponential time.
In Rohit Parikh, editor, Proc. of the 5th Workshop on Logics of Programs, Brooklyn, June 17–19, 1985, LNCS, vol. 193, pp. 413-424, Springer, 1985.
84. Reasoning about the past with two-way automata [ pdf | ]
@inproceedings{Vardi1998, author = {Moshe Y. Vardi}, title = {Reasoning about the past with two-way automata}, pages = {628--641}, editor = {Kim G. Larsen and Sven Skyum and Glynn Winskel}, booktitle = {Proc.\ of the 25th Int.\ Colloquium on Automata, Languages and Programming (ICALP'98)}, series = {Lecture Notes in Computer Science}, volume = {1443}, publisher = {Springer}, year = {1998}, doi = {10.1007/BFb0055090}, ee = {http://dx.doi.org/10.1007/BFb0055090} }
The μ-calculus can be viewed as essentially the “ultimate” program logic, as it expressively subsumes all propositional program logics, including dynamic logics, process logics, and temporal logics. It is known that the satisfiability problem for the μ-calculus is ExpTime-complete. This upper bound, however, is known for a version of the logic that has only forward modalities, which express weakest preconditions, but not backward modalities, which express strongest postconditions. Our main result in this paper is an exponential time upper bound for the satisfiability problem of the μ-calculus with both forward and backward modalities. To get this result we develop a theory of two-way alternating automata on infinite trees.

E.Z.: In short: the converse μ-calculus is ExpTime-complete. Hence, so is concept satisfiability in μALCI.

In Proc. of the 25th Int. Colloquium on Automata, Languages and Programming, Aalborg, Denmark, July 13-17, 1998. LNCS, vol. 1443, pp. 628–641, Springer, 1998.
85. Obstacles on the way to qualitative spatial reasoning with Description Logics: some undecidability results [ pdf | ]
@inproceedings{WesselDL2001, author = {Michael Wessel}, title = {Obstacles on the way to qualitative spatial reasoning with Description Logics: {S}ome undecidability results}, pages = {122--131}, editor = {Carole Goble and Deborah L. McGuinness and Ralf M{\"o}ller and Peter F. Patel-Schneider}, booktitle = {Proc.\ of the 14th Int.\ Workshop on Description Logics (DL~2001)}, series = {CEUR Workshop Proceedings}, volume = {49}, publisher = {CEUR-WS.org}, year = {2001}, ee = {http://ceur-ws.org/Vol-49/Wessel-122start.ps} }
We summarize the results we obtained on the extensions of ALC  with composition-based role inclusion axioms of the form S o T ⊆ R1  ...  Rn. A set of these role axioms is called a role box. The original motivation for this work was to develop a description logic suitable for qualitative spatial reasoning problems. We quickly define and discuss the DLs ALCRA , ALCRA(–), ALCRASG , and ALCNRASG . All but ALCRASG  are shown to be undecidable, and ALCRASG  is of limited utility, even though it is still as expressive as ALCR + . ALCRASG  has shown to be ExpTime-complete, due to associativity of role boxes, which is an important requirement.
In Proc. of the 2001 Int. Workshop on Description Logics, Stanford University, California, USA, August 1-3, 2001, vol. 49 in CEUR, pp. 122–131, 2001.
There are three accompanying technical reports:
• Obstacles on the way to spatial reasoning with Description Logics: undecidability of ALCRA(–) [ pdf ]
Technical Report FBI-HH-M-297/00, University of Hamburg, Computer Science Department, October 2000.
• Decidable and undecidable extensions of ALC with composition-based role inclusion axioms [ pdf ]
Technical Report FBI-HH-M-301/01, University of Hamburg, Computer Science Department, December 2000.
• Undecidability of ALCRA [ pdf ]
Technical Report FBI-HH-M-302/01, University of Hamburg, Computer Science Department, February 2001.

### Abbreviations for conferences

DLInternational Workshop on Description Logics
KRInternational Conference on the Principles of Knowledge Representation and Reasoning
CSLAnnual Conference of the European Association for Computer Science Logic
AAAINational Conference on Artificial Intelligence
LICSIEEE Symposium on Logic in Computer Science
LPARInternational Conference on Logic for Programming, Artificial Intelligence, and Reasoning
FOCSAnnual Symposium on the Foundations of Computer Science
IJCAIInternational Joint Conference on Artificial Intelligence
IJCARInternational Joint Conference on Automated Reasoning
ICALPInternational Colloquium on Automata, Languages and Programming
OWLEDOWL: Experiences and Directions (Workshop)
FoSSaCSInternational Conference on Foundations of Software Science and Computational Structures
TABLEAUXInternational Conference on Analytic Tableaux and Related Methods

### Abbreviations for volumes

LNCSLecture Notes in Computer Science
LNAILecture Notes in Artificial Intelligence