Handbook of Automated Reasoning

4.4 Qualified Number Restrictions

We now study reasoning in $\mathcal{A}\mathcal{L}\mathcal{C}\mathcal{Q}ℐ$ knowledge bases by exhibiting an encoding from $\mathcal{A}\mathcal{L}\mathcal{C}\mathcal{Q}ℐ$ knowledge bases to $\mathcal{A}\mathcal{L}\mathcal{C}ℱ{ℐ}_{*}$ knowledge bases [De Giacomo and Lenzerini 1995b , De Giacomo 1995]. The encoding is based on the notion of reification (see later). As the encoding is polynomial, we get as a result the EXPTIME-decidability of reasoning in $\mathcal{A}\mathcal{L}\mathcal{C}\mathcal{Q}ℐ$ knowledge bases. However, ...