The main purpose of this chapter is to show that sets of models of ALC concepts or knowledge bases satisfy several interesting properties, which can be used to prove expressivity and decidability results. To be more precise, we will introduce the notion of bisimulation between elements of ALC interpretations, and prove that ALC concepts cannot distinguish between bisimilar elements. On the one hand, we will use this to show restrictions of the expressive power of ALC: number restrictions, inverse roles and nominals cannot be expressed within ALC. On the other hand, we will employ bisimulation invariance of ALC to show that ALC has the tree model property and satisfies closure under disjoint union of models. We will also show that ALC has the finite model property, though not as a direct consequence of bisimulation invariance. These properties will turn out to be useful in subsequent chapters and of interest to people writing knowledge bases: for example, ALC's tree model property implies that it is too weak to describe the ring structure of many chemical molecules since any ALC knowledge base trying to describe such a structure will also have acyclic models. In the present chapter, we will only use the finite model property (or rather the stronger bounded model property) to show a basic, not complexity-optimal decidability result for reasoning in ALC. For the sake of simplicity, we concentrate here on the terminological part of ALC, i.e., we consider only concepts and TBoxes, but not ABoxes.

To obtain a better intuitive view of the definitions and results introduced below, one should recall that interpretations of ALC can be viewed as graphs, with edges labelled by roles and nodes labelled by sets of concept names. More precisely, in such a graph

1. • the nodes are the elements of the interpretation and they are labeled with all the concept names to which this element belongs in the interpretation;

2. • an edge with label r between two nodes says that the corresponding two elements of the interpretation are related by the role r.