We now study reasoning in $\mathcal{A}\mathcal{L}\mathcal{C}\mathcal{Q}\mathcal{I}$ knowledge bases by exhibiting an encoding from $\mathcal{A}\mathcal{L}\mathcal{C}\mathcal{Q}\mathcal{I}$ knowledge bases to $\mathcal{A}\mathcal{L}\mathcal{C}\mathcal{F}{\mathcal{I}}_{*}$ 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}\mathcal{I}$ knowledge bases. However, ...

Start Free Trial

No credit card required