6533b833fe1ef96bd129c22e
RESEARCH PRODUCT
The complexity of finite model reasoning in description logics
Carsten LutzUlrike SattlerLidia Tenderasubject
Deductive reasoningTheoretical computer scienceFinite satisfiabilityInverseLogic modelFinite satisfiabilitySatisfiabilityAboxDescription logicTheoretical Computer ScienceComputer Science ApplicationsConsistency (database systems)Number restrictionsTBox ALCQI-Konzept Beschreibungslogik EXPTIME-komplettDescription logicComputational Theory and Mathematicsddc:004TBox ALCQI-concept description logic EXPTIME-completeAlgorithmMathematicsInformation Systemsdescription
AbstractWe analyse the complexity of finite model reasoning in the description 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.
| year | journal | country | edition | language |
|---|---|---|---|---|
| 2005-05-01 | Information and Computation |