Once Lemma 3.6 has been proved, it is easy to reduce the bounded domino problem to consistency. We use the standard reduction that has been applied in the DL context, e.g., in [BS99].
Proof. We define , where Tn is defined in Figure 3, captures the vertical and horizontal compatibility constraints of the domino system , and Tw enforces the initial condition. We use an atomic concept Cd for each tile . consists of the following cardinality restrictions:
The main result of this section is now an immediate consequence of Lemma 2.2, Lemma 3.7, and Corollary 3.3:
Recalling the note below the proof of Lemma 3.6, we see that the same argument also applies to if we allow binary coding of numbers.
It should be noted that it is open if the problem can be decided in , if binary coding of numbers is used, since the reduction of only yields decidability in 2- .
In the following section, we will see that, for unary coding of numbers, deciding consistency of - can be done in (Corollary 4.8). This shows that the coding of numbers indeed has an influence on the complexity of the reasoning problem. It is worth noting that the complexity of pure concept satisfiability for does not depend on the coding; the problem is -complete both for binary and unary coding of numbers [Tob00].
For unary coding, we needed both inverse roles and cardinality restrictions for the reduction. This is consistent with the fact that satisfiability for concepts with respect to TBoxes consisting of terminological axioms is still in , which can be shown by a reduction to the -complete logics [De 95] or CPDL [Pra79]. This shows that cardinality restrictions on concepts are an additional source of complexity. One reason for this might be that with cardinality restrictions no longer has the tree-model property.