Finite Model reasoning in $\mathcal{ALCQI}$ is {\sc ExpTime}-complete
Aus International Center for Computational Logic
Finite Model reasoning in $\mathcal{ALCQI}$ is {\sc ExpTime}-complete
C. LutzC. Lutz, U.SattlerU.Sattler, L. TenderaL. Tendera
C. Lutz, U.Sattler, L. Tendera
Finite Model reasoning in $\mathcal{ALCQI}$ is {\sc ExpTime}-complete
Proceedings of the 2003 International Workshop on Description Logics ({DL2003}), CEUR-WS, 2003
Finite Model reasoning in $\mathcal{ALCQI}$ is {\sc ExpTime}-complete
Proceedings of the 2003 International Workshop on Description Logics ({DL2003}), CEUR-WS, 2003
- KurzfassungAbstract
We analyze the complexity of finite model reasoning in thedescription 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. - Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
@inproceedings{ LutSatTen-DL2003,
author = {C. {Lutz} and {U.Sattler} and L. {Tendera}},
booktitle = {Proceedings of the 2003 International Workshop on Description Logics ({DL2003})},
series = {CEUR-WS},
title = {Finite Model reasoning in $\mathcal{ALCQI}$ is {\sc ExpTime}-complete},
year = {2003},
}
